Subject: Re: SURA: от нас с Робертом всем -- трократное, симметричное URA
From: Arkady Klimov (klark@bagirra.net)
Date: Tue May 08 2001 - 12:27:54 MSD
Привет всем!
Отличный подарок!
И что меня в этом подходе заинтриговало: не получится ли теперь "на УРА" композиция? Была, мне кажется, такая слабость у УРА: композиция функций, каждая из которых в отдельности решается легко, вместе могут составлять очень сложную проблему. А как с этим теперь обстоит? (Прошу прощения, что не могу столь же четко и ясно, как Сергей, выразить свою мысль).
Алик.
----- Original Message -----
From: Sergei M. Abramov (at home)
To: refal
Sent: Monday, May 07, 2001 5:27 PM
Subject: SURA: от нас с Робертом всем -- троекратное, симметричное URA!
День добрый, всем!
Мы с Робертом сегодня закончили очередную ревизию статьи--пригласили написать про УРА в журнал со смачным сокращением SCP ;-) http://www.elsevier.nl/locate/scico/ "Science of Computer Programming".
Статья зовется: ``The Universal Resolving Algorithm and its Correctness:Inverse Computation in a Functional Language''.
Это наш трудовой подарок В.Ф.Турчину к его замечательному юбилею.
Учитывая (пытаясь) противоречивые требования рецензентов (сократить объем на 5..10 страниц и добавить материала) нам пришлось "открыть закрома Родины"--пришлось предать гластности штучку, котоую мы давно дискутировали, но в тайне от народа.
Это потребовало сильно переписать (сильно сократить) Haskell пакет про URA и сильно переписать (сильно сократить) текст статьи.
Итак--симметричный УРА. На самом деле, штука не сложная, возможно она кому-то приходила в голову и/или бросалась в народ как идея на наших бурных семинарах.
Обычный УРА умеет решать такие задачи (замечание: здесь и ниже--угловые скобки--просто скобки):
ura match <[X1, "ABC"],[]> 'Success -- найти такие X1, что (match [X1, "ABC"] = 'Success); ura match <[X1, "ABC"],[]> 'Failure -- найти такие X1, что (match [X1, "ABC"] = 'Failure);
где match -- некая программа (например, проверка вхождения строки в подстроку), <[X1, "ABC"],[]> -- класс, описывающий множество входных данных, X1 -- с-переменная, [] -- рестрикция (набор неравенств, тут--пустой) на с-переменные. То есть, в задачах обычного УРА входные параметры неизвестны (или частично неизвестны), выходное значение программы--фиксировано.
Симметричный УРА исключает дискриминацию между входным и выходными значениями программы.
Ему кроме старых задач (1, 2) можно задавать и такие задачки (3-это обычное вычисление и делается в точности так же эффективно,4 и 5 -- "диаганальный случай", решение уравнений вида f(x)=x и др. более общих.):
1) ura match <( [X1, "ABC"], 'Success ), []> -- найти X1: match [X1, "ABC"] = 'Success; 2) ura match <( [X1, "ABC"], 'Failure ), []> -- найти X1: match [X1, "ABC"] = 'Failure;3) ura match <( ["AB", "ABC"], X1 ), []> -- найти X1: match ["AB", "ABC"] = X1; 4) ura match <( [X1, "ABC"], 'Error:X2), []> -- найти X1, Х2: match [X1, "ABC"] = 'Error:X2;
5) ura match <( [X1, "ABC"], X1 ), []> -- найти X1: match [X1, "ABC"] = X1;
^^^^^^^^^^^^io-class^^^^^^^^^^^^^
Как оказалось, добавление функциональности в УРА приводит к сокращению его кода и его описания. Кому интересно--смотрите ниже или спрашивайте PDF для proof-reader-ов ;-)
Удачи
Сергей.
------------------------------------------------------------------------------
Обычный УРА
Чтобы обсуждать симметричный УРА (SURA) надо договориться о том, что такое обычный УРА:
Это композиция трех функций:
a.. PPT получает программу и входной класс, и строит дерево процессов (не интересно, все знают);
b.. TAB -- обходит дерево в ширину, тащит через дерево входной класс, применяя к нему (к класу) по пути все сужения, что написаны на ребрах, дойдя до листа (пассивной конфигурации), она знает класс достижимости листа (какие данные придут к этому листу) и какой результат (выражение с c-переменными из этого класса) получится на выходе программы. Тем самым, строится пары (возможно бесконечный список пар):
входной подкласс==> с-выражение-для-результата
То есть исходная программа преобразуется в бесконечный список правил: "образец = результат", в терминах рефала. Все входные подклассы (левые части) в таблице tab -- непересекаются.
c.. INV -- проссматривает табличное представление программы, сравнивает (clash) желаемое значение с правой частью предложения из таблицы, если можно отождествить, то подуживает левую часть (контралируя, что это подужение не схлопывает правую часть в пусто).
Интересные места (ну, для нас PPT и TAB не интересны ведь!) в Haskell-реализации выглядили просто (правда буржуям приходится долго втолковывать тривиалные вещи, типа clash и subClassCntr -- CRA-теорему).
ura :: ProgTSG -> Class -> Dval -> [(CCsub,Restr)]ura p cls out = inv (tab (ppt p cls) cls) cls out
inv :: Tab -> Class -> Dval -> [(CCsub,Restr)]inv tab cls out = concat (map ans tab) where ans (cls_i, ce_i) = case (clash [ce_i] [out]) of (False, _) -> [] (True,sub') -> case cls_i' of (_, [CONTRA]) -> [] _ -> [(sub, r)] where cls_i' = cls_i/.sub' (sub, r) = subClassCntr cls cls_i'
Симметричный УРА
Переходим к симметричному УРА.
Шаг 1. Вводим понятие io-класс: конструкция с с-переменными, описывающая множество 2D-точек на плоскости "аргумент программы-результат"---просто вот такая конструкция (и рядом лежащие):
обычный класс:
<ds, r> -- описывает множество входных данных, ds--список с-выражений, r--рестрикция;
io-класс:
<(ds,d), r> -- описывает множество пар (входное данное, данное), ds--список с-выражений, d--с-выражение, r--рестрикция.
функции in_ и io -- ничего особенного, конструктор, селектор:
in_ (<(ds,d), r>) =def= <ds, r> /* проекция */
io (<ds, r>, d) =def= <(ds,d), r> /* декартово произведение, если угодно */
Шаг 2. Понимаем, что каждый буржуй (изучавший унификацию, но не изучавший clash) без объяснений и доказательств понимает, что пересечение классов есть класс, и делается пересечение при помощи унификации (the most general unifier):
Шаг 3. Понимаем, что вместо старой исходной задачи для УРА: по заданному языку, программе, входному классу и желаемому результату (константа), найти множетсво всех тех входных данных, которые:
можно брать симметричную постановку исходной задачи для УРА: по заданному языку, программе и io-классу, найти множетсво всех тех пар (входные данные-результат), корторые:
Шаг 4. Четкое осознаем, что старый добрый TAB -- не более чем представление в виде перечисления io-классов (непересекающихся!) графика функции программы на входном классе cls_in = in_(cls_io)
Шаг 5. Понимаем, что Inv(...) выписанное выше, не более, чем пересечение графика программы с исходным |cls_io|
Ну, в общем-то и все! Далее картинка:
И можно сравнить старый вариант УРА на Хаскеле, с новым вариантом (да, кодов PPT и TAB никто ни сколько не менял):
ura :: ProgTSG -> IOClass -> [ (CCsub,Restr) ]ura p cls_io = inv (tab (ppt p cls_in) cls_in) cls_io where cls_in = in_ cls_io
inv :: [IOClass] -> IOClass -> [ (CCsub,Restr) ]inv tab clsio = concat (map ((*.) clsio) tab)
This archive was generated by hypermail 2b25 : Mon Oct 25 2004 - 21:24:59 MSD