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

Материал из WikiGrapp
Перейти к:навигация, поиск

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

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

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

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

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

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

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

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

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

См. также

Литература

  • Ершов А.П. Введение в теоретическое программирование. Беседы о методе. — М.: Наука, 1977.
  • Ершов А.П. Избранные труды. — Новосибирск: Наука. Сиб. отд-ние, 1994.