6.4. Различные подходы к инверсии программ 99
Данное str является представлением (см. замечание на стр. 4.3.3) строки (’A
’B ’C ). Инверсное вычисление ura’ prog x true i должно построить представле-
ние множества <x>
prog
−1
true
, то есть предствление множества всех данных d вида:
d = [ E.1, str ], где E.1—произвольное е-значение, на которых программа prog
определена и результатом вычисления prog d является true. Задача заключается в
нахождении представления для множества всех подстрок строки str, где определение
предиката “строка E.1 является подстрокой строки str” задано программой prog.
Вычисление ura’ prog x true i приводит к следующему:
<x>
prog
−1
true
= ura’ prog x true i =
<[ ([A.12,str], RESTR[]),
([CONS ’A A.18,str], RESTR[]),
([CONS ’A (CONS ’B A.24),str], RESTR[ ]) ,
([CONS ’B A.18,str], RESTR[]),
([CONS ’A (CONS ’B (CONS ’C A.30)),str], RESTR[]),
([CONS ’B (CONS ’C A.24),str], RESTR[ ]) ,
([CONS ’C A.18,str], RESTR[]) ]>
Альтернативное представление результатов инверсного в ычисления данного запроса
очень наглядно отражает найденные значения неизвестной E.1:
ura prog x true i =
[ ([E.1 :-> A.12],[]),
([E.1 :-> CONS ’A A.18],[]),
([E.1 :-> CONS ’A (CONS ’B A.24)],[]),
([E.1 :-> CONS ’B A.18],[]),
([E.1 :-> CONS ’A (CONS ’B (CONS ’C A.3 0) )] ,[ ]) ,
([E.1 :-> CONS ’B (CONS ’C A.24)],[]),
([E.1 :-> CONS ’C A.18],[]) ]
Итак, в результате данного вычисления получено конечное представление множе-
ства <x>
prog
−1
true
—в виде объединения семи подклассов класса x. Результаты описывают
семь множеств представлений (см. замечание о возможности использования произволь-
ного атома в качестве признака конца строки) всех семи подстрок строки str:
(), (’A), (’A ’B), (’B), (’A ’B ’C), (’B ’C), (’C)
В [FTP] приведены другие примеры инверсного вычисления в TSG.
6.4 Различные подходы
к инвер сии программ
Первые эксперименты по созданию и исследованию свойств УРА для языка Рефал
проведены В.Ф.Турчиным и С.А.Романенко в 1973 г.
В эти же годы вышла статья [1], которая, по сути, является первой работой, описыва-
ющей применение методов мета вычислений для инверсии программ. В ней используется
иной подход для инверсии программ, основанный на построении графа конфигураций