Для общей модели операторных схем функциональная эквивалентность оказалась неразрешимой, однако удалось найти форму протокола - ... - Большая Энциклопедия Нефти и Газа
Выдержка из книги
Виноградов И.М.
Математическая энциклопедия Том 4
Для общей модели операторных схем функциональная эквивалентность оказалась неразрешимой, однако удалось найти форму протокола - т.н. логико-термальную историю, к-рая приводит к разрешимому детерминанту. Этот протокол фиксирует последовательность выполнения и значения предикатов схемы, а для каждого аргумента предиката указывает функциональный терм, к-рый вычислял значение данного аргумента при выполнении программы. Автоматом, воспринимающим детерминант, оказывается двухленточный конечный автомат. Для логико-термальной формальной эквивалентности также найдена полная система преобразований.