Эквивалентность программ: различия между версиями

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


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


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


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


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


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


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


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


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


==См. также ==
==См. также ==
''[[Неинтерпретированные схемы]], [[Стандартные схемы]], [[Схема программ]], [[Схема с косвенной  адресацией]], [[Схемы Лаврова]], [[Схемы Мартынюка]], [[Схемы Янова]].''
* ''[[Неинтерпретированные схемы]],''
* ''[[Стандартные схемы]],''
* ''[[Схема программ]],''
* ''[[Схема с косвенной  адресацией]],''
* ''[[Схемы Лаврова]],''
* ''[[Схемы Мартынюка]],''
* ''[[Схемы Янова]].''
==Литература==
==Литература==
[Ершов/77],
* Ершов А.П. Введение в теоретическое программирование. Беседы о методе. — М.: Наука, 1977.


[Ершов/94]
* Ершов А.П. Избранные труды.  — Новосибирск: Наука. Сиб. отд-ние, 1994.

Навигация