Главная/

Программирование, базы данных. /

Рекурсивные схемы

символы. Однако все попытки применения

«техники следов» для построения распознающего алгоритма ока-

зались неудачными. Лисовик разработал новый метод (назвав его

методом жестких множеств), применением которого доказал

гипотезу Гарлэнда-Лакхэма.  Впрочем, другой алгоритм реше-

ния этой проблемы оказалось возможным извлечь из результатов

работ.

Понятие унарной металинейной схемы отличается от унарной

линейной только тем, что снимаются все ограничения, которые

накладывались на главный терм схемы. Например,

F₁ (F₂(F₃(а))),

F₁ (х) = если р(х) тo х иначе g(F₁(f (х))),

F₂ (х) = если q(х) то f(F₃(g (х))) иначе F₁(h (x)),

F₃ (х) = если r(х) то х иначе F₃(g (h (х)))

—  металинейная схема. Лисовик показал, что проблема эк-

вивалентности унарных металинейных рекурсивных схем с за-

сылками констант алгоритмически разрешима. Этот результат

был получен с помощью довольно длинной цепочки сведений,

в конечном счете проблема была сведена к решению системы ли-

нейных диофантовых уравнений.

Была определена логико-термальная эквивалентность,

казавшаяся корректным и разрешимым отношением эквивалент-

ности. Характерная особенность лт-эквивалентпости состоит

в том, что ее определение не использует понятия интерпретации.

Несмотря на тот факт, что лт-эквивалентность существенно силь-

нее функциональной эквивалентности, набор преобразований,

охраняющий лт-эквивалентность, оказался довольно широким.

Естественно попытаться ввести формальную эквивалентность,

не использующую понятия интерпретации, и для рекурсивных

схем. Такая эквивалентность, основанная на понятии дерева раз-

вертки всех возможных выполнений схемы была введена

Розеном под названием древесной эквивалентности (tree

equivalence).

Проблема древесной эквивалентности иказалась равносильной

проблеме эквивалентности детерминированных магазинных

автоматов, известной открытой проблемме в теории формаль-

ных языков. Что касается проблеммы древесной пустоты —

алгоритм решения ее существует и описан. Разрешимой является

также проблемма древесной эквивалентности в подклассе линей-

ных (полиадических) рекурсивных схем.

Эквивалентные преобразования для рекурсивных схем про-

грамм также рассматривались в некоторых работах. Условия

применения многих преобразований извлекаются при этом

с помощью алгоритмов глобального анализа, обобщающих

алгоритмы разметки.

Стронг, Патерсон и Хьюитт исследовали задачу трансляции

рекурсивных схем в стандартные. Их работы открыли новый

раздел теории схем программ — сравнительную схематологию.

Задача сравнительной схематологии — изучение выразительных

возможностей различных средств (и методов) программирования,

изучение возможности транслировать один класс схем в другой.

Стронг показал, что класс рекурсивных схем не транслируется в

класс стандартных схем (и даже в более общий класс счетчиковых

схем ,  и  выделил  некоторые  подклассы  транслируемых

схем. Одновременно Патерсон и Хьюитт предложили выразитель-

ный пример рекурсивной схемы , для которой не существует

эквивалентной стандартной схемы. Они же анонсировали