Эквивалентность программ

Эквивалентность программ (Program equivalence) - существенная часть формализма понятия программы. В том случае, когда программа реализует некоторую функцию (а это, как правило, так), имеет место естественное и наиболее общее (слабое) определение эквивалентности, требующей лишь равенства функций, вычисляемых программами, --- так называемая функциональная эквивалентность.

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

Среди основных типов историй рассматриваются следующие:

Операционная история программы. Под этим подразумевается запись последовательности преобразователей, выполняемых при работе программы.

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

Информационный граф реализации программы. Вершинами графа являются преобразователи. Вершина [math]\displaystyle{ S_1 }[/math] соединяется с вершиной [math]\displaystyle{ S_2 }[/math], если [math]\displaystyle{ S_2 }[/math] использует результат [math]\displaystyle{ S_1 }[/math] в качестве аргумента.

Информационно-логический граф реализации программы. К информационному графу добавляются вершины проходимых распознавателей. Их аргументы соединяются с соответствующими результатами информационными связями. Кроме того, каждый распознаватель соединяется связью особого рода с каждой вершиной информационно-логического графа, прохождение или непрохождение которой непосредственно зависит от выполнения данного распознавателя.

Термальное значение результирующих переменных. Очевидно, что информационный граф является ациклическим. Это позволяет для каждого аргумента [math]\displaystyle{ a }[/math] любой вершины [math]\displaystyle{ S }[/math] графа построить некоторое дерево, которое называется термальным значением аргумента [math]\displaystyle{ a }[/math] и включает в себя все вершины, достижимые из [math]\displaystyle{ a }[/math] при движении навстречу дугам информационнных связей. Продвигаясь "вниз" по информационному графу, мы получим в конце концов термальные значения результативных переменных.

Логико-термальная история реализации получается добавлением к термальному значению результативных переменных цепочки пройденных распознавателей вместе с термальными значениями их аргументов. Логико-термальная история строится по информационно-логическому графу.

См. также

Неинтерпретированные схемы, Стандартные схемы, Схема программ, Схема с косвенной адресацией, Схемы Лаврова, Схемы Мартынюка, Схемы Янова.

Литература

[Ершов/77],

[Ершов/94]