- •Функции и графы
- •Вычислимость и разрешимость
- •Программы и схемы программ
- •Базис класса стандартных схем программ
- •Графовая форма стандартной схемы
- •Линейная форма стандартной схемы
- •Интерпретация стандартных схем программ
- •Эквивалентность, тотальность, пустота, свобода
- •Свободные интерпретации
- •Согласованные свободные интерпретации
- •Логико-термальная эквивалентность
- •Одноленточные автоматы
- •Многоленточные автоматы
- •Двухголовочные автоматы
- •1.4.3.1. Проблемы пустоты и эквивалентности.
- •1.4.3.2. Двоичный двухголовочный автомат
- •1.4.3.3. Построение схемы, моделирующей автомат
- •Рекурсивное программирование
- •Определение рекурсивной схемы
- •Трансляция обогащенных схем
- •О сравнении классов схем
- •Схемы с процедурами
- •Классы обогащенных схем
- •Трансляция обогащенных схем
- •Структурированные схемы
- •Описание смысла программ
- •Операционная семантика
- •Аксиоматическая семантика
- •2.1.2.1. Краткое введение в исчисление высказываний
- •2.1.2.2. Преобразователь предикатов
- •2.1.2.3. Аксиоматическое определение операторов языка программирования в терминах wp.
- •Денотационная семантика
- •Декларативная семантика
- •Методы доказательства правильности программ
- •Использование высказываний в программах
- •Правила верификации к. Хоара
- •Определения
- •Реализация процессов
- •Протоколы
- •Операции над протоколами
- •Протоколы процесса
- •Спецификации
- •Взаимодействие
- •Параллелизм
- •Задача об обедающих философах
- •I.Встаёт праваЯi).
- •Помеченные процессы
- •Множественная пометка
- •Ввод и вывод
- •Взаимодействия
- •Подчинение
- •Поочередное использование
- •Общая память
- •Кратные ресурсы
- •Планирование ресурсов
- •Основные понятия
- •Многопоточная обработка
- •Условные критические участки
- •Мониторы
- •Instanсе ракетa: счет; р.
- •Обмен сообщениями
- •Параллелизм данных
- •Модель общей памяти
- •Теоретико-множественное определение сетей Петри
- •Графы сетей Петри
- •Маркировка сетей Петри
- •Правила выполнения сетей Петри
- •События и условия
- •Одновременность и конфликт
- •Моделирование параллельных систем взаимодействующих процессов
- •Свойства сетей Петри
- •Методы анализа
Согласованные свободные интерпретации
Полагают, что интерпретация Iи СИIh(того же базисаВ) согласованы, если для любого логического выражениясправедливоIh() =I().
Пусть, например, = `g(h(h(x)), g(h(x), g(x,a)))`, а интерпретацияI3совпадает с интерпретациейI1 из п. 1.2.4 за исключением лишь того, чтоI(x) = 3. Так какI3(a) = 1;I3(g) - функция умножения; I3(h) - функция вычитания 1; получаемI3() = ((3-1)-1)*((3-1)*(3*1)) = 6.
В этом случае Ihпримера из п. 1.3.2. согласована с только что рассмотренной интерпретациейI3, а так же с I2(рисок 1.3, в), но не согласована сI1(рисунок 1.3, б).
Справедливы прямое и обратное утверждения, что для каждой интерпретации IбазисаВсуществует согласованная с ней СИ этого базиса.
Так, например, выше было сказано, что Ihрассмотренного примера не согласована сI1. Что бы сделатьIhсогласованной, необходимо условиеР() видоизменить:P() = 1, если число функциональных символов вбольше трех,P() = 0, в противном случае.
Можно поступить и по другому. Оставить Ihбез изменения и согласовать с нейI1. Для этого необходимо будет заменитьI1(x) = 4, наI1(x) = 3.
Введем важное вспомогательное понятие подстановки термов, используемое в дальнейшем. Еслиx1, …,xn(n≥ 0) – попарно различные переменные,1, ...,n– термы изТ, а- функциональное или логическое выражение, то через[1/x1, ...,n /xn] будем обозначать выражение, получающееся из выраженияодновременной заменой каждого из вхождений переменнойxiна термI(i= 1, …,n). Например:
a[y/x] = a, f(x, y)[y/x, x/y] = f(y, x), g(x)[g(x)/x] = g(g(x)), p(x)[a/x] = p(a).
Приведем без доказательства несколько важных утверждений:
Если интерпретация Iи свободная интерпретацияIhсогласованы, то программы (S, I) и (S, Ih) либо зацикливаются, либо обе останавливаются иI(val(S,Ih)) =val(S,I), т.е. каждой конкретной программе можно поставить во взаимно-однозначное соответствие свободно интерпретированную (стандартную) согласованную программу.
Если интерпретация и свободная интерпретация согласованы, они порождают одну и ту же цепочку операторов схемы.
Теорема Лакхэма – Парка – Паттерсона.Стандартные схемыS1иS2в базисеВфункционально эквивалентны тогда и только тогда, когда они функционально эквивалентны на множестве всех свободных интерпретаций базисаВ, т.е. когда для любой свободной интерпретацииIh программы (S1,Ih) и (S2,Ih) либо обе зацикливаются, либо обе останавливаются и
val(S1,I) = {I(val(S1 Ih)) = I(val(S2 Ih))} = val(S2,I).
Стандартная схема Sв базисеВ пуста (тотальна, свободна) тогда и только тогда, когда она пуста (тотальна, свободна) на множестве всех свободных интерпретаций этого базиса, т.е. если для любой свободной интерпретацииIh программа (S, Ih) зацикливается (останавливается).
Стандартная схема Sв базисеВсвободна тогда и только тогда, когда она свободна на множестве всех свободных интерпретаций базисаВ, т. е. когда каждая цепочка схемы подтверждается хотя бы одной свободной интерпретацией.
Логико-термальная эквивалентность
Отношение эквивалентности Е,заданное на парах стандартных схем, называюткорректным,если для любой пары схемS1иS2изS1 Е S2следует, чтоS1 S2, т. е.S1 иS2функционально эквивалентны.
Поиск разрешимых корректных отношений эквивалентности представляет значительный интерес с точки зрения практической оптимизации преобразования программ, поскольку в общем виде функциональная эквивалентность стандартных схем алгоритмически неразрешима.
Идея построения таких (корректных и разрешимых) отношений связанна с введением понятия истории цепочки схем. В истории с той или иной степенью детальности фиксируются промежуточные результаты выполнения операторов рассматриваемой цепочки. Эквивалентными объявляются схемы, у которых совпадают множества историй всех конечных цепочек.
Одним из отношений эквивалентности является логико-термальная эквивалентность(ЛТЭ).
Определим термальное значение переменной хдля конечного путиwсхемыSкак термt(w, x), который строится следующим образом.
1.Если путь wсодержит только один операторА, то:t(w, x) =, еслиА– оператор присваивания,t(w, x) =х, в остальных случаях.
2.Если w = w’Ае, гдеА– оператор,е– выходящая из него дуга,w’ – непустой путь, ведущий кА, аx1, …, xn– все переменные термаt(Ае,x), тоt(w, x) =t(Ае, x)[t(w’, x1)/x1, …, t(w’, xn)/xn].
Понятие термального значения распространим на произвольные термы :
t(w, x) = [t(w, x1)/x1, …, t(w, xn)/xn].
Например, пути start(х);y:=x;p1(x);x:=f(x);p0(y);y:=x;p1(x);x:=f(x) в схеме на рисунке 1.5, а соответствует термальное значениеf(f(x)) переменнойх.
Для пути wв стандартной схемеSопределим еелогико-термальную историю (ЛТИ)lt(S, w) как слово, которое строится следующим образом.
1.Если путь wне содержит распознавателей и заключительной вершины, тоlt(S, w) – пустое слово.
2.Если w = w’vе, гдеv– распознаватель с тестомp(1, ...,k), ае– выходящая из него Δ-дуга, Δ0,1, то
lt(S, w) = lt(S, w’) pΔ(t(w’, 1), …, t(w’, k)).
3.Еслиw = w’v, гдеv– заключительная вершина с операторомstop(1, ...,k), тоlt(S, w) = lt(S, w’) t(w’, 1) … t(w’, k).
Например, логико-термальной историей пути, упомянутого в приведенном выше примере, будет p1(x)p0(x)p1(f(x)).
Детерминантом(обозначение:det(S)) стандартной схемыSназывают множество ЛТИ всех ее цепочек, завершающихся заключительным оператором.
Схемы S1 иS2 называют ЛТЭ (лт - эквивалентными)S1 ЛТS2, если их детерминанты совпадают.
Приведем без доказательства следующие утверждение:
Логико-терминальная эквивалентность корректна, т. е. из ЛТЭ следует функциональная эквивалентность (S1ЛТS2 S1 S2). Обратное утверждение как видно из рисунка 1.5 не верно.
ЛТ – эквивалентность допускает меньше сохраняющих ее преобразований, чем функциональная эквивалентность.
Моделирование стандартных схем программ