1626435695-d1df5d2e6d953ce7ad4b4ccb5f4f4e30 (844296), страница 21
Текст из файла (страница 21)
И"д) и ид = (й[, Ърд) линдой, что ид — д-я конфигурация протокола выполнения проераммм (Я, 1ь), а и,' — $ я конфигурация протокола выполнения крограмлдм (8, 1), еиполнено й, = Ц и для всех х бБ Ха К (х) = 1 (ггд (х)). Очеввдво, что справедливо и обратное утверждение: для любой свободной интерпретации существует некоторав согласованная с ней интерпретация; таковой нвляетсн, в частности, сама свободнан интерпретация. Введем важное вспомогательное понятие подстановки термез,. которым будем многократно пользоваться в дальнейжем. Если хд,..., х„(п > 0) — попарно различные переменные, гд,... ..., ч„— чермы из Т, а и — функциональное вли логическое выражение, то через к [чд/х„..., т„/х„) будем обозначать выражение, получающееся нз выражения и одновременной заменой каждого из вхождений переменной хд на терм т, (д = 1,..., и).
Более формально, понятие подстановки тернов т, вместо переменных х< в выражении п определяется следующим обрааом. 1. Дли д = 1,..., п хд [тд/хд,..., те/х„) = т,. 2. Если и = 0 или выражение и ие содержит вхождений переменных хд,..., х„, то и [т,/хд,..., т„/х„1 = и.
3. Если и = у (дд,..., дд), где у — функциональный или преднкатный символ, Фд,..., д„Е= Т, а й ) О, то и [тд/хд,... ..., ч„/х„1 = у (г [тд/х„..., т„/х„),..., Сд [тд/х„..., т„/х„)). П р и м е р ы: а [у/х) = а, У (х, у) [у/х, х/у1 = У (у, х), у (х) [у (х)/х[ = у (у (х)), р (х) [а/х1 = р (а). Л е м м а 4.2.
Пусть 1 — произвольная интерпретация бамдса Я, $т' — сосйояниу памяти такое, что для всех х И' (х) ~ Т. Пусть, далее, я — произммьное заражение, х,..., х„— все еголеременнме, а ду' — соскюяние памяти такое, чкю для всех х ФУ' (х) = 1 (ФР (х)). Тогда пд (И~') = 1 (н [И' (хд)/хд,..., гу (х )/х„1). Д о к а з а т е л ь с т в о. Очевидно,'й = й; и дли всех х с= ~ Хз 1(% (х)) = И'з (х), поскольку )Рз (з:) = И'з (х), И~т (х) = = $чг (х) и 1 (Ю~ (х)) = Фчг (х). Пусть для некоторого $ (з > О) выполнено (з) й; = й;. и (2) для всех х (-= Хв 1 (И', (х)) = чр; (х).
Докажем, что ($) и (2) будут выполняться тогда н для следующего г. Рассмотрим длн атого все возможные случаи (пусть 0 оаначает оператор, помеченный меткой й;). ($) 0 — оператор присваивания х: = т, а х„..., х„— вое переменные терна т. Тогда йиз = й;;з и 1 (И~и, (х)) = = 1(т(%; (хз)й„..., ар; (х„)lх„)) = тг (К) = Ж+~ (х). Для перемнаных у, отличных от х, имеем 1 (И~,+з (у)) = 1 (И'; (у)) = = И'. (у) = (~".Ы- (2) Π— условный оператор я, а хз, ...,х„ — все переменные теста я. Тогда И'„, = В;.и Вй~ = И';, так что для всех х Е= Хз 1 (И~~ з (х)) = 1 (чр; (х)) = В~ (х) = Кы (х).
Далее, по лемме 4.2 яз, (И'<) = 1ь (я (И~, (хд/х„..., В; (х )/х„)) и из ($К) = 1 (я (И"; (х,)й„..., И', (х„)/х„)), а в силу согласованности интерпретаций 1 н 1„правые части этих равенств совпадают, поатому оба вхождения распознавателя выберут одну и ту же дугу, т. е. й;+з — — й~+д. (3) 0 — петля. Тогда йиз = й; = й~ — — й, и для всех х~ ,— Хз 1 (И~,+з (х)) = 1 (уу; (х)) = ФК (х) = %Кз (х).
Итак, в случае, когда Π— заключительный оператор, имеем 1 (И', (х)) = %К (х) для всех х я Хз и оба протокола обрываются на конфигурации ио ( ) Л е м м а 4.4. Если интерпрвпация 1 и свободная иктерпреоция 1ь ь, то программы (А, 1) и (8, 1ь) либо обе зяцикливаются, либо обе останввлиеаются и 1 (ча) (8, 14) = = ча) (8, 1). Д о к а з а т е л ь с т в о. Эта лемма — очевидное следствие леммы 4.3. ( ) Л е м м а 4.5.
Если инкюрпрюкяция 1 и свободная интерпретация 1ь согласованы, пю они порождают одну и ту же цепочку (цепочку операторов) стели. Д о к а з а т е л ь с т в о. Непосредственное следствие леммы 4.3. Ц 3.4. Основные теоремы о свободных ннтерпретацивл. Т е о р е м а 4.1 (Лакхэм — Парк — Патерсон). Стандартные схемы Ез и Юз в базисе М Яункционально эквиваленкииз пюгдя и люлько тогда, когда они Функционально эквивалеювим на множеспим всех свободных интерпретаций базиса З, т. е. когда для любой свободной интарпрниации 1 программы (Ем 1) и (Ем 1) либо обе зациклизаютпся, либо обе останввливаюкюя и ча1 (Яы 1) = = ча1 (Яз, 1), ао Д о к аз а тел ь с та о. Необходимость очевидна.
Достаточность. Пусть 8» и 8» эквивалентны на множестве всех свободных интерпретаций, а 1 — произвольная интерпретация базиса Ю. По лемме 4Л существует свободная интерпретация 1„, согласованная с 1. По лемме 4.4 программы (Я» 1) и (8п 1„) либо обе зацикливаются, либо обе останавливаются, и 1 (ча1 (Бн 1„)) = = ча1 (8п 1). Аналогично, программы (8», 1) и (8, 1ь) либо обе зациклизаются, либо обе останавливаются, и 1 (ча1 (8, 1„)) = = ча1 (8», 1). Так как 8» и Я» эквивалентны на множестве свободных интерпретаций, программы (Я» 1„) и (8», 1») либо обе зацикливаются, либо обе останавливаются, и ча1 (дм 1„) = ча1 (Я»а 1»). Следовательно, программы (Ю, 1) и (8», 1) либо обе зацикливаются, либо обе останавливаются, и ча1 (Юн 1) = 1 (ча1 (Я», 1»)) =1 (ча1 (8», 1„)) = ча1 (8», 1).
Так как интерпретация 1 выбрана произвольно, Я» функционально эквивалентна 8 . 1 ) .Т е о р е м а 4.2. Стандартная схема 8 в базисе % пуста (тотальна) тогда и только тогда, когда она пуста (тотальна) на множестве всех свободных интерпрепищий этыо базиса, т. е.
если для любой свободной интерпретации 1„программа (8, 1,) зацикливается (останавливается). Д о к а з а т е л ь с т в о. Необходимость очевидна. Достаточность немедленно следует из лемм 4Л и 4.4. ( ~ Т е о р е м а 4.3. Стандартная схема в базисе эз свободна тое да и только тогда, когда она свободна на множестве всех свободных и терпретаций жного базиса, т.
е. когда каждая цепочка сзпмы подтверждаппея хотя бы одной свободной интерпретацией. Д о к а э а т е л ь с т в о. Необходимость. Любая допустимап цепочка схемы подтверждается кекоторой свободной иптеркретацией, что непосредственно следует иэ леммы 4Л н 4.5. Достаточность. Очевидна. [ ) Леммы 4Л вЂ” 4.5 и теоремы 4Л вЂ” 4.3 позволяют нам рассматривать в дальнейшем только свободно интерпретированные схемы как при исследовании проблем функциональной эквивалентности, пустоты, тотальности и свободы, так и в других задачах, связанных ео стандартными схемами и схемами других классов. В последнем случае нан потребуется перенос этих утверждений на новые классы программ, что будет сделано беэ повторения всех деталей доказательств — лишь указанием на ход рассуждений. Отметим, что существуют анеэрбрановы» классы схем программ, для которых неверны утверждения, аналогичные только что доказанным леммам и теоремам.
Задавив 4.4. А. Пап»жпта, чта стакдартпна схемы э ба»пса,Ю патерпратацзаваа взамарфжз (см. »адамка 4.3, з) тогда и таз»по тогда, когда авв пптарпратацзаппа в»аморфны па мкажаатва свободных интерпретаций этого ба»паз. Б. Папажвта, чта ожпдартпыа охами э ба»все Я слабо зпэпээяавтзн тогда п только тогда, когда авп слабо эпввэазавтвы па мважества свободных пптарпрагацзй этага Йепаа. 9$ 3.5.
Определение логике-зеркальной эквивалеитнеета и ее корректность. Отношение эквввалентностн Е, заданное на парах стандартных схем, назовем коррекшшьв, если для любой пары схем 8г и Яз вз Яг — Яз следует,что 8г Яю т. е. Схемы 8г и 8з к функциокалъно эквивалентны. Поиск разрешимых корревткых откошенвй эквивалентности представляет значительный интерес с точки зрения практической оптимизации и првобрааовеввя программ, посколъку, как мы увидим в следующей главе, функциональная эквивалентность стандартных схем алгорвтмически пвразрешима.
Идея построения таких (корректных и разрешимых) отношений связана с введением понятия истории цепочки схемы. В истории с той или ивой степенью детальности фиксируются промежуточные результаты евыполневияз операторов рассматриваемой цепочки. Эквивалентными объявляются схемы, у которых совпадают множества историй всех конечных цепочек. Одним из таких отношений эквивалентности является введенная Иткиным [22] логика-термалъная эквивалентность, основанная на понятии логике-термальной астории. Определим терлииьъное юачение неременной х длл коненково кути ю схемы 8 как терм Ф (ю, х), который строится следующнм образом.
1. Если путь ю содержит только один оператор А, то ° ° т, если А — оператор присваивания х:= т, Ф(ю,х) = х, в осталъвых случаях. 2. Если ю = ю'Ае, где А — оператор, е — выходящая из него дуга, ю' — непустой путь, ведущий к А, а хп..., х„— все переменные терка г(Ае, х), то С(ю, х) = г (Ае, х) [г (и/, х,)/хп... Ф( х)/х]- Понятие термального значения распространим на произвольные термы тт если х,..., х„— все переменные герма т, то положим Ф (ю, т) = т [г (ю, х,)/х„..., Ф (ю, х„)/х„].
Например, пути 1( ). х, /(х); ре(у); у:= х; р'(х); х -=У (х). в схеме на рве. 4.4, а соответствует тврмальное значение / (/ (х)) переменной х. Для пути ю в некоторой стандартной схеме Я определим ев лосино-тереиъеъную историю 1С (о, иу) как слово, которое строится следующим образом. 1. Если путь ю не содержит распознавателей и заключительной вершины, то 1$ (8, ю) — пустое слово.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
