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

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


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


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


''Информационный граф реализации программы''. [[Вершина|Вершинами]]
''[[Информационный граф реализации программы]]''. [[Вершина|Вершинами]]
[[граф|графа]] являются преобразователи. Вершина <math>S_1</math> соединяется с
[[граф|графа]] являются преобразователи. Вершина <math>S_1</math> соединяется с
вершиной <math>S_2</math>, если <math>S_2</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>S</math> графа
построить некоторое дерево, которое называется  
построить некоторое [[дерево]], которое называется  
''термальным значением аргумента'' <math>a</math> и включает в себя все
''термальным значением аргумента'' <math>a</math> и включает в себя все
вершины, достижимые из <math>a</math> при движении навстречу дугам
вершины, достижимые из <math>a</math> при движении навстречу [[дуга|дугам]]
информационнных связей. Продвигаясь "вниз" по
информационнных связей. Продвигаясь "вниз" по
информационному графу, мы получим в конце концов термальные
информационному графу, мы получим в конце концов термальные
значения результативных переменных.
значения результативных переменных.


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


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


[Ершов/94]
[Ершов/94]

Версия от 12:29, 1 июня 2010

Эквивалентность программ (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]