метасистемная лестница - презентация

1 Глава 2. Представление множеств

2 Супер- компиляция scp Специализация программ Приложения супер компиляции, в том числе Базовые понятия и методы мета вычислений int, SR, ptr Инверсное вычисление ura Окрестностный анализ nan Приложения мета вычислений Иные методы Иные приложения [2] Л.В.Парменова «Метавычисления и их применения. Суперкомпиляция» [1] С.М.Абрамов «Метавычисления и их применения» Область возможных новых исследований Окрестностное тестирование Реализация нестандартных семантик Инверсное программирование Методы мета вычислений Структура курса

3 Представление множеств µ Проблема подбора (выбора) способов представления множества Подход, традиционный для математики { 2n + 1 | n 0 } µ { (5 cos φ, 5 sin φ) | 0 φ π/2 } Для языка TSG µ ((CONS A.1 E.2), RESTR[A.1 :=/=: A]) µ ((CONS A.1 A.2), RESTR[A.1 :=/=: A.2])

4 Обзор главы µ Вводятся средства конструктивного представления множеств для языка TSG, исследуются и обосновываются их свойства µ Конфигурационные переменные (c- переменные), двух типов (для языка TSG): A.index, E.index µ Рестрикции: системы неравенств, задающих дополнительные ограничения на допустимые значения ca-переменных

5 Обзор главы µ SR-выражение (cx,rs) представляет множество : = { cx/.s | s FVS(cx,rs) } где s подстановка, (/.) операция применения подстановки s к cx, FVS(cx,rs) множество полных допустимых для (cx,rs) подстановок

6 Обзор главы µ Частные случаи SR-выражений: классы и L-классы представляют множества данных языка TSG конфигурации представляют множества состояний вычисления TSG- программ над данными и т.п.

7 Обзор главы µ Подстановки для получения элементов представленного множества и для сужения множеств µ Сужения либо подстановка, либо рестрикция (дополнение к имеющимся ограничениям на значения c- переменных) µ Суперпозиция для подстановок (сужений)

8 Обзор главы µ Разбиение пара (c 1, c 2 ) элементарных сужений:, =, = Ø µ Операция unify отождествления двух списков c-выражений

9 Обзор главы Отношение () частичного порядка на множестве SR-выражений: sr 1 sr 2, если sr 1 является результатом выполнения некоторого числа сужений sr 2. Свойство: sr 1 sr 2 µ Каноническая форма (canon C) записи класса C и его свойства: = множество { canon C* | C C* } канонических форм надклассов класса C конечно для любого класса C

10 Конфигурационные переменные, с-выражения µ ca-var::= (CVA c-var-name) µ ce-var::= (CVE c-var-name) µ c-var-name::= integer пояснить! µ ca-expr::= a-val | ca-var µ ce-expr::= ca-expr | ce-var | (CONS ce-expr 1 ce-expr 2 )

11 2.1 Конфигурационные переменные µ A.index сокращение для (CVA index) µ E.index сокращение для (CVE index) µ Области значений ca- и ce-переменных µ Области значений ca- и ce-выражений

12 2.2 С-связи, с-среды, с-состояния µ состояние: (t, [var 1 := val 1,...var n := val n ]) µ обобщенное состояние: (t, [var 1 := cexp 1,...var n := cexp n ])

13 2.3 Неравенства, рестрикции с-переменных µ restr::= INCONSISTENT | RESTR [ineq 1,... ineq n ] 0n µ ineq::= ca-expr :: ca-expr µ Все виды неравенств: А.1 :: А А.1 :: А.2А.1 :: А.1 А :: B A :: А.1 А :: A µ Частные случаи неравенств: противоречие, тавтология µ Отметить противоречия и тавтологии

14 2.3 Неравенства, рестрикции с-переменных µ isContradiction, isTautology :: InEq -> Bool µ isContradiction (left :=/=: right) = (left == right) µ isTautology (ATOM a :=/=: ATOM b)= (a /= b) isTautology (left :=/=: right)= False µ Неравенство неупорядоченная пара! µ instance Eq InEq where (l1:=/=:r1) == (l2:=/=:r2) | (l1==l2) && (r1==r2)= True | (l1==r2) && (r1==l2)= True | otherwise= False

15 2.3 Неравенства, рестрикции с-переменных µ cleanRestr :: Restr -> Restr cleanRestr INCONSISTENT = INCONSISTENT cleanRestr (RESTR ineqs) = INCONSISTENT, if any isContradiction ineqs cleanRestr (RESTR ineqs) = RESTR (nub(filter (not.isTautology) ineqs)) µ Gofer (диалект Haskell-я)

16 2.3 Неравенства, рестрикции с-переменных µ cleanRestr :: Restr -> Restr cleanRestr INCONSISTENT= INCONSISTENT cleanRestr (RESTR ineqs) | any isContradiction ineqs= INCONSISTENT | otherwise= RESTR (nub(filter (not.isTautology) ineqs)) µ instance UPDATE Restr where INCONSISTENT +. _= INCONSISTENT _ +. INCONSISTENT= INCONSISTENT (RESTR r1) +. (RESTR r2)= cleanRestr (RESTR (r1 ++ r2))

17 2.4 C-конструкции atom cvar (CONS ce 1 ce 2 ) [ce 1,... ce n ] pvar:=ce [cbind 1,... cbind n ] (term, cenv) ce 1 :: ce 2 [ineq 1,... ineq n ] RESTR ineqs INCONSISTENT (cx, rs) SR-база cx c-выражение ce список c-выражений ces c-связь cbind c-среда cenv c-состояние cst неравенство ineq список неравенств ineqs рестрикция rs SR-выражение

18 2.5 cvars µ Для любой c-конструкции cx список c- переменных, входящих в cx, мы будем обозначать cvars cx µ Непосредственно из определения синтаксиса SR-баз следует, что если в SR-базе нет ни одной c-переменной, то она является соответствующим объектом языка TSG

19 2.5 cvars µ class CVARS a where cvars :: a -> [CExp] µ instance CVARS CExp where cvars (ATOM _ )= [ ] cvars _)= [cvar] cvars _)= [cvar] cvars (CONS h t)= nub ((cvars h)++(cvars t)) µ instance CVARS CBind where cvars (pvar := cx) = cvars cx

20 2.5 cvars µ instance CVARS InEq where cvars (ax :=/=: bx) = nub ((cvars ax)++(cvars bx)) µ instance CVARS Restr where cvars INCONSISTENT = [] cvars (RESTR ineqs) = cvars ineqs µ instance (CVARS a, CVARS b) => CVARS (a, b) where cvars (ax, bx) = nub ((cvars ax)++(cvars bx)) µ instance CVARS c => CVARS [c] where cvars cxs = nub (concat (map (cvars) cxs))

21 2.6. Подстановки Подстановки и представление множеств в математике. C= { 2n+1 | n1 } Подстановка, как средство построения сужений и разбиений множества:s 1 = { n 2k } s 2 = { n 2k+1 } C 1 = C /. s 1 = { 4k+1 | k1 } C 2 = C /. s 2 = { 4k+3 | k0 } Подстановка, как средство получения элемента множества: s 0 = { n 2 } (2n+1) /. s 0 = 5 элемент множества [n1] /. s 0 = [21] тавтология

22 2.6. Подстановки µ subst::= [c-sbind 1,... sbind n ] 0n µ c-sbind::= ca-var :-> ca-expr | ce-var :-> ce-expr µ Дополнительно потребуем все левые части различны µ Список всех c-переменных, которым subst ставит в соответствие некоторое значение: dom subst µ dom :: Subst -> [CExp] dom subst = [ cvar | (cvar :-> _ )

23 2.7. Применение подстановки instance APPLY CExp Subst where (ATOM a) /.s= ATOM a (CONS h t)/.s= CONS (h/.s) (t/.s) cvar /.s= cvar, if cvar notElem dom s cvar /.s = head [ cexp | (cv:->cexp)

24 2.7. Применение подстановки µ instance APPLY InEq Subst where (l:=/=:r) /. subst = (l/.subst) :=/=: (r/.subst) µ instance APPLY CBind Subst where (pvar := cexpr) /. subst = pvar := (cexpr/.subst) µ instance APPLY a subst => APPLY [a] subst where cxs /. subst = map (/.subst) cxs

25 2.7. Применение подстановки µ instance (APPLY a subst, APPLY b subst) => APPLY (a,b) subst where (ax,bx) /. subst = ( (ax/.subst), (bx/.subst) ) µ instance APPLY Restr Subst where INCONSISTENT /. subst= INCONSISTENT (RESTR ineqs) /. subst= cleanRestr(RESTR(ineqs/.subst))

26 Пример 2 µ ineqs = [A.2::A.1, A.2::'C, A.3::'A] rs = RESTR ineqs s 1 = [A.1:->'A, A.2:->A.3] s 2 = [A.1:->'B, A.3:-> 'B] s 3 = [A.2:->A.1, A.3:->'A] Работа в классе: ineqs /. s 1 rs /. s 1 и т.д. ineqs /. s 1 = [A.3::'A, A.3::'C, A.3::'A] rs /. s 1 = RESTR [A.3::'A, A.3::'C] ineqs /. s 2 = [A.2::'B, A.2::'C, 'B::'A] rs /. s 2 = RESTR[A.2::'B, A.2::'C] ineqs /. s 3 = [A.1::A.1, A.1::'C, 'A::'A] rs /. s 3 = INCONSISTENT

27 2.8. Свойства подстановок µ подстановка сохраняет «a-» и «e-» тип с- выражения µ подстановка сохраняет вид c- конструкции (ca-выражение, ce- выражение, список c-выражений длины n, c-связь, c-среда, c-состояние, неравенство, противоречие, тавтология, список неравенств длины n, рестрикция, SR-выражение)

28 2.8. Свойства подстановок Жесткий n - местный конструктор C: (C x 1 … x n ) == (C y 1 … y n ) ۸ k=1..n (x k ==y k ) µ в силу жесткости конструкторов, при помощи которых из атомов и c- переменных конструируются SR-базы, выполнено:

29 2.8. Свойства подстановок µ Утверждение 5 Если cx SR-база; s 1, s 2 подстановки, то cx/.s 1 == cx/.s 2 тогда и только тогда, когда для любой c- переменной cv из cx выполнено cv/.s 1 ==cv/.s 2 : (cx/.s 1 ==cx/.s 2 ) ۸ (cv/.s 1 ==cv/.s 2 ) cv cvars cx

30 Доказательство Доказательство µ Структурная индукция: любая SR-база cx это либо атом, либо с-переменная, либо жесткий конструктор: cx = (C cx 1 … cx n ). Докажем: (cx/.s 1 ==cx/.s 2 ) ۸ (cv/.s 1 ==cv/.s 2 ) cv cvars cx µ Если cx атом, то... ч.т.д. µ Если cx с-переменная, то... ч.т.д. µ Пусть для cx 1 … cx n утверждение выполнено, докажем его для cx = (C cx 1 … cx n )

31 Доказательство Доказательство (cx/.s 1 ==cx/.s 2 ) (C cx 1 … cx n )/.s 1 == (C cx 1 … cx n )/.s 2 (C cx 1 /.s 1 … cx n /.s 1 ) == (C cx 1 /.s 2 … cx n /.s 2 ) ۸ k=1..n (cx k /.s 1 == cx k /.s 2 ) ۸ k=1..n (۸ cv cvars cx_k (cv/.s 1 ==cv/.s 2 )) ۸ cv (cvars cx_1)++…++(cvars cx_n) (cv/.s 1 ==cv/.s 2 ) ۸ cv nub((cvars cx_1)++…++(cvars cx_n)) (cv/.s 1 ==cv/.s 2 ) ۸ cv cvars (C cx_1 … cx_n) (cv/.s 1 ==cv/.s 2 ) ۸ cv cvars cx (cv/.s 1 ==cv/.s 2 ) чтд

32 2.9. Отождествление c-выражений µ Aлгоритм отождествления unify по двум спискам c-выражений ces1 и ces2 строит следующий результат: µ (False, []) если не существует подстановки s такой, что ces1/.s=ces2 µ (True, s) если существует такая подстановка. При этом, s подстановка, такая, что ces1/.s=ces2 и dom s = cvars ces1

33 Идея алгоритма µ Уравнение (clash) и решение уравнения: ces 1 `unify` ces 2 µ Доброволец! µ [A.1, (CONS A.2 'A), E.3, A.2] `unify` ['B, (CONS A.4 'A), (CONS 'A 'C)] µ [A.1, (CONS A.2 'A), E.3, A.2] `unify` ['B, (CONS A.4 'A), (CONS 'A 'C), A.4] µ [A.1, (CONS A.2 'A), E.3, A.2] `unify` ['B, A.4, (CONS 'A 'C), A.4] µ [A.1, (CONS A.2 'A), E.3, A.2] `unify` ['B, (CONS A.4 'A), (CONS 'A 'C), A.5]

34 2.9. Отождествление c-выражений µ type UnifRes = (Bool, Subst) µ fail = (False, []) :: UnifRes µ data Clashe = CExp :=: CExp уравнение type Clashes = [Clashe] µ unify :: CExps -> CExps -> UnifRes µ unify ces1 ces2 | (length ces1)/=(length ces2) = fail | otherwise = unify [] chs where chs = zipWith (:=:) ces1 ces2

35 2.9. Отождествление c-выражений µ unify :: Clashes -> Clashes -> UnifRes µ Первый и второй аргументы unify их смысл µ unify rchs [] = (True, subst) where subst = map (\(a:=:b)->(a:->b)) rchs µ Второе уравнение разбирает все случаи для первого неразрешенного уравнения µ Таблица вариантов

36 Таблица вариантов: заполним? :=: 'A 1 А.1Е.1CONS a 1 b 1 'A 2 'A 1 ='A 2 'A 1 'A 2 fail А.2 MoveCL fail Е.2 MoveCL CONS a 2 b 2 fail a 2 :=:a 1 b 2 :=:b 1

37 2.9. Отождествление c-выражений unify rchs = case ch of ATOM a :=: ATOM b | a==b-> unify rchs chs ATOM a :=: cex -> fail _):=: (ATOM _)-> moveCl rchs chs _):=: (CVA _) -> moveCl rchs chs _):=: cex-> fail _):=: cex-> moveCl rchs chs CONS a1 b1 :=: CONS a2 b2-> unify rchs (p++chs) where p=[a1:=:a2,b1:=:b2] CONS a1 b1 :=:cex-> fail

38 2.9. Отождествление c-выражений moveCl:: Clashes -> Clashes -> UnifRes moveCl rchs = case [ y | (x:=:y) unify (ch:rchs) chs [y] | y==cexp -> unify rchs chs [y] | otherwise -> fail

39 2.9. Отождествление c-выражений µ Теорема. Для любых списков c-выражений ces1, ces2 вычисление unify ces1 ces2 завершается за конечное число шагов с правильным результатом (False, []) если не существует подстановки s такой, что ces1/.s=ces2 (True, s) если существует такая подстановка. При этом, s подстановка, такая, что ces1/.s=ces2 и dom s = cvars ces1

40 2.10 Представляемое множество Определение 11 Подстановка s полная для c-конструкции cx, если: она связывает все с-переменные из cx: cvars cx dom s со значениями: cv cvars cx: (cv/.s) Eval Пусть cx=(cb, rs) SR-выражение; п одстановка s допустимая для c- конструкции cx, если ее применение к rs не приводит к противоречиям: rs/. s /= INCONSISTENT

41 2.10 Представляемое множество µ Пусть x и y c-конструкции и s полная для x. Тогда: если cvars y cvars x то s полная для y если x = …y… то s полная для y µ Полная подстановка приводит SR-базу (ca- выражение, ce-выражение, список c- выражений длины n, c-связь, c-среда, c- состояние) к значению соответствующего вида (a-значение, e-значение, список значений длины n, связь, среда, состояние)

42 2.10 Представляемое множество µ Утверждение 9 Пусть (cx, rs) SR- выражение, s полная подстановка для (cx, rs). Пусть (cx, rs)/.s = (cx/.s, rs/.s) = (x,rs'). Тогда x является синтаксической конструкцией языка TSG, соответствующей виду cx s недопустимая для (cx, rs) rs' = INCONSISTENT s допустимая для (cx, rs) rs' = RESTR [ ]

43 2.10 Представляемое множество µ Определение 12. Пусть se=(cx,rs) SR- выражение. Множество полных допустимых для se подстановок обозначим через FVS(se)=FVS(cx,rs). Будем использовать se для представления множества синтаксических объектов языка TSG. Это множество будем обозначать =. Oпределим это множество так: = = { cx/.s | s FVS(cx,rs) }

44 2.10 Представляемое множество Примеры: µ (E.1, RESTR[]) µ (A.1, RESTR[]) µ µ Пусть e EVal, sngl(e) = (e, RESTR []) µ Тогда, - одноэлементное множество: = {e}. µ Пусть ce любая SR-база. Тогда, =Ø.

45 2.11 Классы и L-классы µ Определение 13 Пусть cx SR-база. Будем называть cx линейной, если в cx нет ce -переменных, имеющих повторные вхождения в cx. Линейные c-выражения будем называть Lc-выражениями, линейные списки c-выражений будем называть L-списками c-выражений.

46 2.11 Классы и L-классы µ Определение 14 Пусть ces список c- выражений, rs рестрикция. Тогда C=(ces,rs) будем называть классом. Если ces L-список c-выражений, то класс C=(ces,rs) будем называть L- классом. µ Классы используются для изображения множеств входных данных TSG- программ.

47 2.11 Классы и L-классы µ Пример 4 Рассмотрим класс: C=([A.1, (CONS E.2 A.3)], RESTR [A.1: : A.3]) Тогда C представляет множество всех данных, имеющих вид [a 1, (CONS e 2 a 3 )], где e 2 произвольное e-значение, a 1 и a 3 два несовпадающих a-значения

48 2.12 Конфигурации µ Определение 16 Будем называть конфигурацией SR-выражение conf, имеющее вид conf=((t, cenv), rs), где (t, cenv) c-состояние rs рестрикция t программный терм cenv c-среда. µ Конфигурации представляют множества состояний вычислений µ Далее будет видно, что введенных средств достаточно для представления всех множеств, которые возникают при метавычислениях

49 2.13 Суперпозиция подстановок µ (.*.) :: Subst -> Subst -> Subst sa.*. sb = [ cvar:->((cvar/.sa)/.sb) | cvar

50 2.14 Сужения µ contr ::= S subst | R restr µ instance APPLY c Subst => APPLY (c,Restr) Contr where (cx,rs) /. (S s) = (cx/.s, rs/.s) (cx,rs) /. (R rs')= (cx, rs+.rs') µ Утверждение 17 Пусть (cx,rs) SR- выражение, c сужение, (cx,rs)=(cx,rs)/.c. Тогда,.

51 2.14 Сужения µ Определение 20 Пусть cx, cx SR- выражения. Будем использовать обозначения cx cx и cx cx, eсли существуют такие сужения c 1,... c n, n > 0, что cx=cx/.c 1 /.c 2.../.c n. µ Утверждение 18 cx cx, cx cx cx cx cx cx µ Утверждение 19 Пусть cx, cx SR- выражения и cx cx, тогда

52 2.14 Сужения µ Утверждение 20 Данное d D принадлежит множеству, представленному классом C тогда, и только тогда, когда sngl(d) C. µ Определение 21 idC= S [ ] :: Contr emptC= R INCONSISTENT:: Contr

53 2.14 Сужения µ Утверждение 21 Пусть (cx,rs) SR- выражение. Тогда, выполнено: (cx,rs)/.idC = (cx,rs) = (cx,rs)/.emptC = (cx, INCONSISTENT) = Ø

54 2.14 Сужения µ Утверждение 22 Если x и x SR- выражения, то x x, тогда и только тогда, когда существуют два сужения: c1 = (S s) и c2 = (R r), такие, что x=x/.c1/.c2

55 2.14 Сужения µ Идея доказательства: x x x = x/.c 1 /.c 2... /.c n = x/.(S [])/.c 1 /.c 2... /.c n /.(R (RESTR[])) µ Далее преобразуем: SS S: /. (S s1) /. (S s2)= /. (S s1.*.s2) RR R:/. (R r1) /. (R r2)= /. (R r1+.r2) RS SR:/. (R r) /. (S s)= /. (S s)/.(R (r/.s))

56 2.15 Каноническая форма класса µ Неоднозначность представления классом множества данных. µ Причины неоднозначности: 1. c-переменные, входящие в класс, являются свободными параметрами; согласованное переименование c- переменных по сути не изменяет класса

57 2.15 Каноническая форма класса µ Причины неоднозначности: 2. рестрикция класса система неравенств; каждое неравенство неупорядоченная пара левая часть :: правая часть перестановка левой и правой части неравенства и переупорядочивание неравенств в рестрикции по сути не изменяет класса 3. В рестрикции неравенства могут входить многократно, могут быть тавтологии и противоречия. Преобразования рестрикций, выполняемые функцией cleanRestr, по сути не изменяют класса

58 2.15 Каноническая форма класса µ Борьба с причиной «3»: будем рассматривать классы с упрощенными рестрикциями. = µ Определение Перестановка s является переименовкой мнение класса?: все правые части с-переменные типы правых частей совпадают с типами левых частей все правые части различны

59 2.15 Каноническая форма класса µ Утверждение 23 Пусть С 1, С 2 классы, С 2 получен из С 1 (1) переупорядочиванием левых и правых частей и неравенств в рестрикции и/или (2) переименовкой s с-переменных в С 1 : cvars С 1 = dom s. Тогда =.

60 2.15 Каноническая форма класса µ Наведем порядок в рестрикциях! 1. Определим отношение (

61 2.15 Каноническая форма класса Вид x Вид y Определение (

62 2.15 Каноническая форма класса Вид x Вид y Определение (

63 2.15 Каноническая форма класса µ Определение 6 Класс C* будем называть канонической формой класса C, если: 1. C* может быть получен из класса C путем переименования c-переменных и переупорядочивания (п.ч./л.ч. и неравенств) в рестрикции (в соответствии с порядком

64 2.15 Каноническая форма класса µ Определение 6 Класс C* будем называть канонической формой класса C, если: 2. cvars C* имеет вид: [vt 1 1, vt 2 2,..., vt n n], где t i {CVA, CVE} конструкторы c- переменных. Т.е., для c-переменных в C* используются в качестве индексов все числа от 1 до n, где n число различных c- переменных. И если первое вхождение c- переменной v встречается в C* раньше (левее) первого вхождения c-переменной v, то должно выполняться v

65 2.15 Каноническая форма класса µ Определение 6 Класс C* будем называть канонической формой класса C, если: 3. Для любого неравенства x :: y в C* выполнено x

66 2.15 Каноническая форма класса µ Утверждение 9 1. Если C* является канонической формой C, то = 2. Существует алгоритм canon, который для любого класса C за конечное число шагов строит класс (canon C), являющийся канонической формой C

67 2.16 Подклассы и надклассы µ Определение 23 Пусть C 1, C 2 классы. Тогда: класс C 2 будем называть подклассом класса C 1, а класс C 1 будем называть надклассом класса C 2, если C 2 C 1 класс C 2 будем называть собственным подклассом класса C 1, а класс C 1 будем называть собственным надклассом класса C 2, и будем обозначать C 2 < C 1, если C 2 C 1 и канонические формы для классов C 1 и C 2 не совпадают: canon C 2 canon C 1

68 2.16 Подклассы и надклассы µ Теорема 10 Если множество атомов AVal конечно, то множество канонических форм надклассов класса C { canon C* | C C* } конечно для любого класса C

69 Доказательство Доказательство Пусть C C*, тогда «длина» SR-базы у C* меньше, чем «длина» L SR-базы у C µ Здесь «длина» число переменных, атомов и CONS «длина» SR-базы у canon C* чем L, эта SR- база состоит из атомов, (CONS … … ) и ca-, ce- переменных, индексы которых от 1 до L. Таких различных SR-баз конечное число. Рестрикции: конечное множество (без повторов) из пар, слева/справа: атомы или ca- переменные, индексы которых от 1 до L. Таких различных рестрикций конечное число.

70 2.17 Разбиения µ Определение 24 Пусть (cx, rs) SR- выражение. Тогда пару сужений sp = (c 1, c 2 ) назовем разбиением для (cx, rs), а сами сужения c 1 и c 2 назовем элементарными сужениями для (cx, rs), если пара (c 1, c 2 ) или пара (c 2, c 1 ) имеет один из следующих видов:

71 2.17 Разбиения 1. (idC, emptC ) 2. (S [E.i:->(CONS E.m E.n)], S [E.i:->A.p]) 3. (S [A.j:->A.k], R RESTR[A.j:=:A.k]) 4. (S [A.j:->a], R RESTR[A.j:=: a]) где E.i, A.j, A.k переменные из cx, то есть они входят в cvars cx E.m, E.n, A.p новые c-переменные для cx, то есть индексы m, n, p не используются в качестве индексов c-переменных в cx a некоторый атом

72 2.17 Разбиения Свойство. Элементарные сужения сохраняют линейность; р езультат элементарного сужения L-класса есть L- класс Теорема 29 Пусть sp=(c 1, c 2 ) разбиение для SR-выражения x, x 1 =x/.c 1, x 2 =x/.c 2. Тогда и разбиение множества : = = Ø

73 2.17 Разбиения

74 Обзор главы µ Проблема подбора (выбора) способов представления множества Подход, традиционный для математики { 2n + 1 | n 0 } µ { (5 cos φ, 5 sin φ) | 0 φ π/2 } Для языка TSG µ ((CONS A.1 E.2), RESTR[A.1 :=/=: A]) µ ((CONS A.1 A.2), RESTR[A.1 :=/=: A.2])

75 Обзор главы µ Ввели средства конструктивного представления множеств для языка TSG, исследуются и обосновываются их свойства µ Конфигурационные переменные (c- переменные), двух типов (для языка TSG): A.index, E.index µ Рестрикции: системы неравенств, задающих дополнительные ограничения на допустимые значения ca-переменных

76 Обзор главы µ SR-выражение (cx,rs) представляет множество : = { cx/.s | s FVS(cx,rs) } где s подстановка, (/.) операция применения подстановки s к cx, FVS(cx,rs) множество полных допустимых для (cx,rs) подстановок

77 Обзор главы µ Частные случаи SR-выражений: классы и L-классы представляют множества данных языка TSG конфигурации представляют множества состояний вычисления TSG- программ над данными и т.п.

78 Обзор главы µ Подстановки для получения элементов представленного множества и для сужения множеств µ Сужения либо подстановка, либо рестрикция (дополнение к имеющимся ограничениям на значения c- переменных) µ Суперпозиция для подстановок (сужений)

79 Обзор главы Отношение () частичного порядка на множестве SR-выражений: sr 1 sr 2, если sr 1 является результатом выполнения некоторого числа сужений sr 2. Свойство: sr 1 sr 2 µ Каноническая форма (canon C) записи класса C и его свойства: = множество { canon C* | C C* } канонических форм надклассов класса C конечно для любого класса C

80 Обзор главы µ Разбиение пара (c 1, c 2 ) элементарных сужений:,, =, = Ø µ Операция unify отождествления двух списков c-выражений