1626435695-d1df5d2e6d953ce7ad4b4ccb5f4f4e30 (844296), страница 43
Текст из файла (страница 43)
В первом случае результат трансляции — стандартная схема, а именно — главная схема без инструкций вызова. Во втором случае получается схема с процедурамн, в которой число процедур и вызовов может уменыпаться по сравнению с исходной схемой. Такую схему с процедурами будем называть приведенной Процесс частичной трансляции всегда завершается. Действительно, каждая подстановка или уменьшает число инструкций вызова, нли не уменьшает, но зато число злементов в списках новых подставленных инструкций вызова увеличивается, по крайней мере, на единицу. Так как общее число определяемых функциональных символов в схеме конечно, наступит момент, когда очередную подстановку нельзя сделать. В этот момент в списке любого вызова будут находиться символы всех тех определяемых функций, при выполнении которых может возникнуть данный вызов. Остается убедиться, что полученная схема, будь то стандартная схема или приведенная схема с процедурами, зквизалентна исходной схеме.
Чисто техническая работа по сравнению протоколов исходной и полученной схем прн произвольной свободной интерпретации показывает, что зто так. Приведенная схема для о«, включает главную схему, построенную выше, и ту же схему процедуры, что к в Ю«,»«. Если частичная трансляция завершилась построением приведенной схемы с процедурами, то зто еще не значит, что исходную (или построенную) схему нельзя транслировать в стандартную схему. Алгоритм частичной трансляции обнаруживает отсутствие или наличие «синтаксической» рекурсии.
Но для некоторой схемы о может случиться, что при любой интерпретации 1 во время выполнения программы (о, 1) ни одна из процедур не вызывается повторно, пока не завершится выполнение предыдущего выаова этой же процедуры. Это значит, что в схеме о" нет, по существу, рекурсии. Такие схемы транслируются в стандартные. Другой пример рекурсивных схем и схем с процедурами, которые могут быть пропущены алгоритмом частичной трансляции, — схемы без условных операторов (или логических выражений). Краткий обзор н комментаряя Теоретическое изучение рекурсивного программирования было начато Маккарти [121, 122] в связи с его работами над языком Лисп [43] и одновременно в связи с попытками создать основы семантической теории программирования. В дальнейшем рекурсивные схемы и программы играли важную роль в развитии формальных методов описания и исследования семантики программ и языков программирования, в теории правильности программ.
Схематологические аспекты рекурсивного программирования впервые были исследованы Де Баккером и Скоттом [97], Стронгом [138], Патерсоном и Хьюиттом [129]. Де Беккер и Скотт предложили унарные рекурсивные схемы как обобщение схем Янова и инициировали изучение главных проблем для рекурсивных схем.
Так как класс рекурсивных схем строго мощнее класса стандартных схем (см. теорему 8.3), неразрешимость всех главных проблем для рекурсивных схем можно установить из их неразрешимости для стандартных схем. С другой стороны, класс праволинейных унарных схем равномощен классу схем Янова (см.
теорему 8.5), поэтому на этот класс переносятся все «пояснительные» результаты из теоряи схем Янова. В настоящее время между этими двумя полюсами мало существенных результатов. Гарланд и Лакхэм [[02! показали разрешимость проблемы эквнвалентности в классе линейных унарных схем, и Сабельфельд [631 построил полную систему эквивалентных преобразований для этого класса в духе системы преобразований Ершова для схем Янова. Наиболее полное исследование класса унарных схем выполнено Ашкрофтом, Манна и Пнуели [831, которые установили разрешимость проблем пустоты, тотальности и свободы в этом классе, а также разрешвмость проблемы эквивалентности в классе свободных уиарных схем. В классической работе И021 Гарланд и Лакхэм высказали гипотезу о разрешимости функциональной эквивалентности в классе унарных линевных рекурсивных схем с засылками констант, т. е.
схем, в которых разрешается нснользовать нульместные базовые функциональные символы. Однако все попытки применеяия «техники следов» для построения распознающего алгоритма оказались неудачными. Лисовик разработал новый метод (назвав его методом жестких множеств), применением которого [361 доказал гипотезу Гарлэнда — Лакхэма. Впрочем, другой алгоритм решения атой проблемы оказалось возможным извлечь из результатов работ [407, 601. Понятие укорной мешалииейяой «лемм отличается от унарной линейной только тем, что снимаются все ограничения, которые накладывались на главный терм схемы. Например, Р (Р» (Рз(в))). Р» (л) = если р (л) то л иначе л (Р«Ц (л))), Р (л) = если д (л) то [(Р (у (з))) иначе Р» (Й (х)), Р»(х) = если г(х) то х иначе Р»(у (Й (л))) — металинейная схема.
Лисовик показал [371, что проблема эквивалентности унарных металинейных рекурсивных схем с засылками констант алгоритмически разрешима. Этот результат был получен с помощью довольно длинной цепочки сведений, в конечном счете проблема была сведена к решению системы линейных диофантовых уравнений. В гл. 4 была определена логико-термальпая эквивалентность, оказавшаяся корректным и разрешимым отношением эквивалентности. Характерная особенность лт-эквивалентности состоит з том, что ее определение не использует понятия интерпретации. Несмотря на тот факт, что лт-эквивалентность существенно сильнее функциональной эквивалентности, набор преобразований, сохраняющий лт-эквивалентность, оказался довольно широким 197 (см.
гл. 6). Естествшшо попытаться ввести формальную эквивалентность, не использующую понятия интерпретации, и для рекурсивных схем. Такая эквивалентность, основанная на понятии дерева развертки всех возможных выполнений схемы, была введена Розеном (1341 под названием древесной эквивалентности (»гее е)в(та1евсе). Среди определяемых функциональных символов выделим особый символ й, Н (И) =О, рекурсивное уравнение которого будет иметь вид Й = Й, так что вычисление выражения Й (как вызова без фактических параметров) должно быть бескояечным при любой иятерпретации. Будем предполагать, что область интерпретации Р всегда содержит по крайней мере два разлячных элемента 1 и О.
Условное выражение если и то а иначе р будем записывать также в форме ~~ (я, а, ()), используя трехместиый базовый функцнональнын символ»1, который может интерпретироваться только такой трехместной функцней сопб: 11» -» В, для которой сопб ($, а, р) = а и сопй (О, а, (1) = (1, но совб (я, а, р) не определено, если я чь 1 и я ~ О. Термы из множества Т всех термов могут рассматриваться как деревья. Скажем, дерево у Г соответствует терму ~ Я(р (х, у), у, г'(л)), 6(а, з)). На множестве Т введем отношение частичного порядка, полагая 8» «( ~», если терм 8 можно получить из терма 1~ заменой некоторых вхождений Я на элементы из Т.
Напркмер, Я ~ г для всех зе— : Т. В соответствни с доказанным в (31 множество Т можно пополнить пределами всевозможных цепей элементов из Т, т. е. бесконечными деревья.ми (или мащюдерезьави). Результат пополнеяия— множество К с отношением частичного порядка «~» — обладает следующим свойством полноты: наимеиыпая верхняя грань 1вЬ (С) всякой цепи С элементов из у принадлежит Я. По рекурсивной схеме 8 построим последовательность термов ()» (8), я Р О).
Терм А» (Я) — это главный терм схемы я, а терм Х„»» (8) для я,:» О получается из терма Ь Щ открытой подстановкой всех самых внешних вызовов в Х„(8). Например, для схем»» 8в.»»» г (я. Ь)е г' (л, у) =есви р (х) то л иначе г'(1 (х), у (у)) 198 получим Ь (8 „) = Г (а, Ь), Ьт (Язлэ) = Ц (р (а), а, »г (~ (а), у (Ь))), З (8. ) =Ю(р( ). ° ~У(р(У( )) У( ) Р(УУ( )). 6(6(Ь))))).
Отображение р: Т»- Т определим следующим образом: л, если т = л, где л ~ Я; у(р(т,),...,р(т„))„если т = 7(т„..., т„), где 1 — базовый функциональный символ, ~чь»~ и»те($ ~ » ~(л) р(т»)ФЙ; ц(р(а),рф),р(7)), если т»Дсс,(»,7), причем р(а)+ьг и либо р(ЯФО, либо р(7)чь 0; П в остальнь»х случаях. »)еФ (8) =- (вЬ (р (Ъ (8)): и э О) — детерминант схемы 8. Схемы Я» и Яэ назовем древесно эвеиеален»эмили, если бей (Я») = дей (8 ), Папрнмер, схема 8п», древесно эквивалентна следующей схеме 8э.м.
»' (о)ю г" (л) = если р (я) то х иначе Г Ц (х)), поскольку их общим детерминантом является макродерево Проблема древесной эквявалентности оказалась равносильной (93, 94, 10Я проблеме эквивачентности детермвнировапных магазинкых автоматов, известной открытой проблеме в теории»Ьормальных языков. Что касается проблемы древесной пустоты (беФ (Б) = М), то в (67) описан алгоритм ее решения. Разрешимой является также проблема древесной эквивалентности в подклассе линейных (полпадических) рекурсивных схем И37). Эквивалентные преобразования для рекурсивных схем программ рассматривались в работах ((9, 66).
Условия применения многих преобразований извлекаются при этом с помощью алгоритмов глобального анализа, обобщающих алгоритмы разметки из гл. 2. Стронг, Патерсон и Хьюитт исследовали задачу трансляции рекурсивных схем в стандартные. Их работы открыли новый раздел теории схем программ — сравнительную схематологию. Задача сравнительной схематологяи — изучение выразительных возможностей различных средств (и методов) программирования, изучение возможности транслировать один класс схем в другой (более подробно эти вопросы рассмотрены в гл. 9). Стронг (138) показал, что класс рекурсивных схем не транслируется в класс стандартных схем (и даже в более об>ций класс счетчиковых схем, см. теорему 9.2), и выделил некоторые подклассы транслируемых схем. Одвовременио Патерсон и Хьюитт предложили выразитель ный пример рекурсивной схемы (схема Бал), для которой не существует эквивалентной стандартной схемы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
