Теория вычислительных процессов (стр. 9 )

Стандартная схема в базисе свободна тогда и только тогда, когда она свободна на множестве всех свободных интерпретаций этого базиса, т. е. когда каждая цепочка схемы подтверждается хотя бы одной свободной интерпретацией.

1.3.4 Логико-термальная эквивалентность

Отношение эквивалентности , заданное на парах стандартных схем, называют корректным, если для любой пары схем и из следует, что , т. е.  и функционально эквивалентны.

Построение таких (корректных и разрешимых) отношений связанно с введением понятия истории цепочки схем. В истории с той или иной степенью детальности фиксируются промежуточные результаты выполнения операторов рассматриваемой цепочки. Эквивалентными объявляются схемы, у которых совпадают множества историй всех конечных цепочек.

Одним из отношений эквивалентности является логико-термальная эквивалентность (ЛТЭ).

Определим термальное значение переменной для конечного пути схемы как терм , который строится следующим образом.

1)  Если путь содержит только один оператор , то: , если – оператор присваивания, , в остальных случаях.

2)  Если , где – оператор, – выходящая из него дуга, – непустой путь, ведущий к , а – все переменные , то .

Понятие термального значения распространим на произвольные термы t:

Например, пути

start(х); y:=x; p1(x); x:=f(x); p0(y); y:=x; p1(x); x:=f(x) в схеме на рисунке 1.5 а соответствует термальное значение f(f(x)) переменной х.

а	б

Рис. 1.5

Для пути в стандартной схеме определим ее логико-термальную историю (ЛТИ) как слово, которое строится следующим образом.

1)  Если путь не содержит распознавателей и заключительной вершины, то – пустое слово.

2)  Если , где – распознаватель с тестом , а – выходящая из него -дуга, , то

.

3)  Если , где – заключительная вершина с оператором stop(t1, ..., tn), то

Например, логико-термальной историей пути, упомянутого в приведенном выше примере, будет p1(x) p0(x) p1(f(x)).

Детерминантом () стандартной схемы называют множество ЛТИ всех ее цепочек, завершающихся заключительным оператором.

Схемы и называют ЛТЭ (лт - эквивалентными) , если их детерминанты совпадают.

Логико-терминальная эквивалентность корректна, т. е. из ЛТЭ следует функциональная эквивалентность (). Обратное утверждение как видно из рисунка 1.5 б не верно.

1.4 Моделирование стандартных схем программ

1.4.1 Одноленточные автоматы

Конечный одноленточный (детерминированный, односторонний) автомат обнаруживают ряд полезных качеств, используемых в теории схем программ для установления разрешимости свойств ССП.

Одноленточный конечный автомат (ОКА) над алфавитом задается набором

и правилом функционирования, общим для всех таких автоматов. В наборе

‑ алфавит;

‑ конечное непустое множество состояний ;

‑ множество выделенных заключительных состояний ;

‑ выделенное начальное состояние;

‑ программа автомата;

‑ «пустой» символ.

Программа автомата представляет собой множество команд вида , в которой , и для любой пары существует единственная команда, начинающаяся этими символами.

Неформально ОКА можно представить как абстрактную машину, похожую на машину Тьюринга, но имеющую следующие особенности:

1)  выделены заключительные состояния;

2)  машина считывает символы с ленты, ничего не записывая на нее;

3)  на каждом шаге головка автомата, считав символ с ленты и перейдя согласно программе в новое состояние, обязательно передвигается вправо на одну клетку;

4)  автомат останавливается в том и только в том случае, когда головка достигнет конца слова, т. е. символа #.

Автомат допускает слово в алфавите , если, начав работать с лентой, содержащей это слово, он останавливается в заключительном состоянии. Автомат задает характеристическую функцию множества допускаемых им слов в алфавите , т. е. он распознает, принадлежит ли заданное слово множеству если связать с остановкой в заключительном состоянии символ 1, а с остановкой в незаключительном состоянии – 0.