Subject: SURA: от нас с Робертом всем -- троекратное, симметричное URA!
From: Sergei M. Abramov (at home) (abram@botik.ru)
Date: Mon May 07 2001 - 18:27:13 MSD
День добрый, всем!
Мы с Робертом сегодня закончили очередную ревизию статьи--пригласили написать
про УРА в журнал со смачным сокращением 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