Глава 3. Дерево процессов

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

Обзор главы 3. Дерево процессов µ Вводятся понятие дерева процессов и алгоритм построения дерева процессов базовое понятие и базовый алгоритм метавычислений.

Определение дерева конфигураций tree Дерево конфигураций tree: ориентированное (возможно бесконечное) дерево, каждому узлу n которого приписана некоторая конфигурация c; каждому ребру a, выходящему из некоторого узла n с конфигурацией c, приписано сужение cnt; причем, если из узла n с конфигурацией c выходит k 1 ребер a 1,... a k с сужениями cnt 1,... cnt k, то множества попарно не пересекаются, а их объединение совпадает с.

idC cnt 1 cnt 2 cnt … idC cnt 3 cnt 4 cnt … c2c2 c1c1 c0c0 c…c… c…c… c3c3 c4c4 Дерево конфигураций

Определение множества для пути w из tree Путь w в дереве конфигураций tree представляет множество последовательностей P переходов из одного состояния s i вычисления в языке TSG к другому: = { P | P отождествимо с w }, где «P отождествимо с w» (или, «w представляет P») означает, что: cnt 0 cnt 1 cnt 2 w = c 0 c 1 c 2...c n... P = s 0 s 1 s 2...s n... P и w имеют одинаковые длины для каждого s i выполнено: s i, и если s i не последнее в P, то s i.

idC cnt 2 idC cnt 3 s3s3 s4s4 s0s0 s2s2 s1s1 c2c2 c1c1 c0c0 cnt 1 cnt … cnt 4 cnt … c…c… c…c… c3c3 c4c4 P=s 0... s 4 отождествима с путем w

Определение множества Определение множества µ Дерево tree представляет множество последовательностей состояний вычислений: = [ | w путь из корня tree и w нельзя продлить ] объединение всех, где w путь в tree из корневой вершины, который нельзя продлить: либо w имеет бесконечную длину либо w завершается в листовой вершине дерева tree

Определение множества процессов вычисления µ Множество процессов вычисления p на данных из некоторого класса C (на обобщенном данном программы p): P(p, C) = { process(p, d) | d }

Определение дерева процессов µ Пусть p программа на TSG; C класс, обобщенное данное для p; tree некоторое дерево конфигураций. Тогда: tree дерево процессов вычисления p на данных из, если P(p, C). Если при этом для каждой вершины дерева существует d, такое, что эта вершина используется в представлении process(p,d), то tree перфектное дерево (совершенное, нет лишних вершин)

idC cnt 1 cnt 2 C d cnt … idC cnt 3 cnt 4 cnt … s0s0 s1s1 s2s2 s3s3 s4s4 c2c2 c1c1 c0c0 c…c… c…c… c3c3 c4c4 Дерево процессов process(p,d)=s0... s4 может быть бесконечны м

Далее в Главе 3. Дерево процессов Приводятся и обосновываются: µ алгоритм ptr построения дерева процессов вычисления p на данных из : tree = ptr p C µ алгоритм xptr построения перфектного дерева процессов вычисления p на данных из : ptree= xptr p C

3.1 Синтаксис представления дерева процессов µ tree::= (LEAF conf ) | (NODE conf [branch 1,... branch n ]) n 0 µ branch::= (contr, tree)

3.2 Вспомогательные функции в алгоритме ptr µ mkCAVar, mkCEVar :: FreeIndx -> (CVar, FreeIndx) mkCEVar i = ((CVE i), i+1 ) mkCAVar i = ((CVA i), i+1 ) µ splitA :: CVar -> CExp -> Split splitA _) caexp = (S [cv:->caexp], R (RESTR[cv:=/=:caexp]) )

3.2 Вспомогательные функции в алгоритме ptr µ splitE :: CVar -> FreeIndx -> (Split,FreeIndx) splitE _) i = ( (S[cv:-> (CONS cvh cvt)], S[cv:-> cva]), i) where(cvh, i1)=mkCEVar i (cvt, i2)=mkCEVar i1 (cva, i)=mkCAVar i2

3.2 Вспомогательные функции в алгоритме ptr µ freeindx :: FreeIndx -> Class -> FreeIndx freeindx i c = 1 + maximum(i:(map index (cvars c))) whereindex (CVA i) = i index (CVE i) = i

Идея алгоритма ptr µ Мы имеем программу p и класс C «обобщенные данные» для p. µ Нам надо «отследить» process(p, d) для всех d, понятие process(p, d) определено через int p d µ В некотором смысле требуется выполнить программу p на множестве : process(p, ) или int p µ Это и делается в ptr p C для обобщенных данных C для p мы пытаемся делать те же преобразования, что и для обычных данных для p делают в int

Идея алгоритма ptr µ В начале для p и C строится начальная конфигурация c 0 так же, как строится начальное состояние s 0 в int p d µ Начальная конфигурация c 0 записывается в корень дерева µ Далее для любой граничной и нетерминальной конфигурации делается попытка выполнить «следующий шаг вычисления программы p» так же, как это сделал бы int

Идея алгоритма ptr µ Для некоторых конфигураций c наличие c-переменных в с-состоянии не мешают однозначно выполнить шаг вычисления программы p (так же, как это сделал бы int), построить следующее с-состояние и следующую конфигурацию c. В этом случае мы делаем шаг вычисления c c и в дереве проводим ребро c idC c

Идея алгоритма ptr µ Для других конфигураций c наличие c- переменных в с-состоянии мешают однозначно выполнить шаг вычисления программы p (так же, как это сделал бы int): µ Некоторые состояния из «выбирает один вариант» продолжения вычислений, а другие другой вариант. µ В этом случае удается построить разбиение sp=(cnt, cnt) такое, что для и шаг уже можно сделать однозначно, перейдя к c и c, соответственно. µ В дереве проводим два ребра c cnt c и c cnt c.

Если наличие c- переменных в с- состоянии не мешают однозначно выполнить шаг программы p (как это сделал бы int) и построить следующее с-состояние и следующую конфигурацию c делаем шаг. cnt 1 cnt 2 c2c2 c…c… Для p и C строим начальную конфигурацию c 0 так же, как строится начальное состояние s 0 в int p d c 0 записывается в корень дерева, для граничных и нетерминальных c k выполняем шаг вычисления программы p как это сделал бы int C cnt … idC c1c1 c0c0 idC c3c3 cnt 3 cnt 4 c…c… c4c4 Идея алгоритма ptr Для других конфигураций c наличие c-переменных в с- состоянии мешают однозначно выполнить шаг программы p (как это сделал бы int): некоторые состояния из «выбирает один вариант» продолжения вычислений, а другие другой вариант. В этом случае удается построить разбиение sp=(cnt, cnt) такое, что для и шаг уже можно сделать однозначно, перейдя к c и c, соответственно.

cnt 1 cnt 2 c2c2 c…c… C cnt … idC c1c1 c0c0 idC c3c3 cnt 3 cnt 4 c…c… c4c4 Еще раз Идея алгоритма ptr

Интерпретатор языка TSG µ int :: ProgR -> [EVal] -> EVal int p ds = eval s p where(DEFINE f prms _) : p' = p e = mkEnv prms ds s = ((CALL f prms), e)

3.3 Алгоритм ptr µ ptr :: ProgR -> Class -> Tree ptr p r) = evalT c p i where (DEFINE f prms _) : p = p ce = mkEnv prms ces c = ((CALL f prms, ce), r) i = freeindx 0 cl

Интерпретатор языка TSG µ eval :: State -> ProgR -> EVal eval f args), e) p = eval s' p where DEFINE _ prms t' = getDef f p e' = mkEnv prms (args/.e) s' = (t',e')

3.4 Алгоритм ptr (функция evalT) µ evalT ::Conf->ProgR->FreeIndx -> Tree evalT CALL f args, ce), r) p i = NODE c [ (idC, evalT c p i) ] where DEFINE _ prms t = getDef f p ce = mkEnv prms (args/.ce) c = ((t,ce),r)

Интерпретатор языка TSG µ eval c t1 t2), e) p = case cond c e of TRUE ue -> eval (t1,e+.ue) p FALSE ue -> eval (t2,e+.ue) p

3.4 Алгоритм ptr (функция evalT) µ evalT ALT cnd t1 t2, ce), r) p i = NODE c [ (cnt1,evalT c1 p i), (cnt2,evalT c2 p i) ] where ((cnt1,cnt2), uce1, uce2, i) = ccond cnd ce i ((_,ce1),r1) = c/.cnt1 c1 = ((t1, ce1+.uce1), r1) ((_,ce2),r2) = c/.cnt2 c2 = ((t2, ce2+.uce2), r2)

Интерпретатор языка TSG µ eval p = exp/.e

3.4 Алгоритм ptr (функция evalT) µ evalT p i = LEAF c

Интерпретатор языка TSG (функция cond) µ cond :: Cond -> Env -> CondRes cond (EQA? x y) e = let x' = x/.e; y' = y/.e in case (x', y') of (ATOM a, ATOM b) | a==b -> TRUE [ ] (ATOM a, ATOM b) -> FALSE[ ]

3.5 Алгоритм ptr (функция ccond) µ ccond :: Cond->CEnv->FreeIndx ->(Split,CEnv,CEnv,FreeIndx) ccond (EQA x y) ce i = let x = x/.ce; y = y/.ce in case (x, y) of (a, b )|a==b ->((idC,emptC), [],[],i) (ATOM a, ATOM b)->((emptC, idC), [],[],i) (CVA _, a ) ->( splitA x a, [],[],i) (a, CVA _ ) ->( splitA y a, [],[],i)

Интерпретатор языка TSG (функция cond) µ cond (CONS? x vh vt va) e = let x' = x/.e in case x' of CONS h t->TRUE [vh:=h,vt:=t] ATOM a->FALSE[va:=x']

3.5 Алгоритм ptr (функция ccond) µ ccond (CONS x vh vt va) ce i = let x = x/.ce in case x of CONS h t ->((idC,emptC), [vh:=h,vt:=t], [], i ) ATOM a ->((emptC,idC), [], [va:=x], i ) CVA _ ->((emptC,idC), [], [va:=x], i ) CVE _ ->( split, [vh:=ch,vt:=ct], [va:=ca], i) where (split, i) = splitE x i (S[_:->(CONS ch ct)], S[_:->ca]) = split

Свойства ptr µ Теорема 30. Пусть p программа на языке TSG; C = (ces, r) класс, обобщенное данное для p. Тогда, определенное алгоритмом ptr дерево tree = ptr p C является деревом процессов программы p для класса C. µ Доказательство: разобрать самостоятельно (стр. 48 ̶ 52).

Наша цель совершенство µ Множество достижимости некоторой вершины в дереве: множество данных из C, которые «проходят» через данную вершину µ Перфектное дерево все множества достижимости непустые µ Можно ли построить множества достижимости?

Множества достижимост и cnt 2 idC cnt 1 C cnt … idC c2c2 c1c1 c0c0 c…c… cnt 3 cnt 4 cnt … c…c… c3c3 c4c4

3.6 Алгоритм xptr µ Сухие ветви, причины возникновения сухих веток. Обрезание сухих веток в дереве. µ Перфектное дерево процессов неперфектное, в котором удалены «сухие ветви».

3.6 Алгоритм xptr µ Как распознать, пустое ли множество ? Работает класс! µ При любом sr имеем = Ø µ Если cleanRestr r INCONSISTENT то Ø, для бесконечного Atoms (или «в Atoms достаточно много элементов») µ Для конечных Atoms конечным перебором можно понять пустоту FVS(sr,r)

3.6 Алгоритм xptr µ Рестрикции в конфигурации и в классе достижимости одни и те же! (по индукции) µ Перфектное дерево процессов. µ xptr :: ProgR -> Class -> Tree xptr p cl = NODE c (cutT brs) where tree = ptr p cl NODE c brs = tree

3.6 Алгоритм xptr µ cutT :: [Branch] -> [Branch] cutT [ ] = [ ] cutT tree) : bs) = case tree of LEAF (_, INCONSISTENT) -> cutT bs NODE (_, INCONSISTENT) _ -> cutT bs LEAF c -> (b :cutT bs) NODE c bs -> (b:cutT bs) where tree = NODE c (cutT bs) b = (cnt, tree)

3.6 Алгоритм xptr µ Теорема 32. Пусть p программа на языке TSG; C = (ces, r) класс, обобщенное данное для p. Тогда, определенное алгоритмом xptr дерево tree = xptr p C является перфектным деревом процессов программы p для класса C. µ Доказательство: разобрать самостоятельно (стр. 5253).

d d s0s0 s1s1 idC cnt 1 cnt 2 s2s2 C d d cnt … idC s3s3 cnt 3 cnt 4 s4s4 d cnt … c2c2 c1c1 c0c0 c…c… c…c… c3c3 c4c4

Обзор главы 3. Дерево процессов µ Дерево конфигураций µ Путь w в дереве конфигураций tree представляет множество последовательностей P переходов из одного состояния s i вычисления в языке TSG к другому µ Дерево tree представляет множество последовательностей состояний вычислений: = [ | w путь из корня tree и w нельзя продлить ]

Обзор главы 3. Дерево процессов µ Множество процессов вычисления p на данных из некоторого класса C (на обобщенном данном программы p): P(p, C) = { process(p, d) | d } µ Дерево процессов вычисления p на данных из : дерево конфигураций tree, такое что P(p, C)

Обзор главы 3. Дерево процессов µ Дерево tree процессов вычисления p на данных из перфектное, если для каждой вершины дерева существует d, такое, что эта вершина используется в представлении process(p,d)

Обзор главы 3. Дерево процессов Приводятся и обосновываются: µ алгоритм ptr построения дерева процессов вычисления p на данных из : tree = ptr p C µ алгоритм xptr построения перфектного дерева процессов вычисления p на данных из : ptree= xptr p C