1626435695-d1df5d2e6d953ce7ad4b4ccb5f4f4e30 (844296), страница 34
Текст из файла (страница 34)
Если все достижимые вершины окааались обработанными, то алгоритм ааканчивается успешно. Т е о р е и а 7.8. Алгоршнм э( заканчивается для любой парк приведенных свободных снвознкх схем, удовлео»ворами»ей условию раздеяе ности персменнкг. Д о к а в а т е л ь с т в о. Поскольку каждая достижимая вершина обрабатывается на шагах 1 — 3 ровно оден раэ, достаточно убедиться, что множество достижимых вершин конечно. Разобьем это множество на два непересекающихся подмножества О» и 6"г (7» = ([А, В, з)! е»((А, В, з)), О = ((А, В, з11 ~ е») (А, В, з)).
Пусть о, = 1А„В„з»1, » ) Π— последовательность различных .достижимых вершин иэ О (8», 8,), последовательно порождаемых алгоритмом э(. Для фиксированных распознавателей А, В схем Ю» н Яг соответственно и для сети з ~ К такой, что е»( (А, В, з), рассмотрим подпоследовательность о;,.= (А,, В», з,.), 1 ) О, вершин этой последовательности, для которых т» 1 (А;,. = А) 8» (В». — — В) 8» ((ЗАБЫТБ) з». = з). Тогда по построению графа О (з„з,) получим»зу (г». ь з» ) 8» »й (з»; чь з». ), т.
е. строго убывающую цепь полурешетки 2'. Поэтому конечность множества Ю» вытекает иэ условия обрыва цепей для Я', конечности множества К и множеств вершнн исходных схем. Что касается конечности множества Рг, то она вытекает иэ того, что благодаря проверке условия (Зв) расстояние каждой иэ вершин иэ Ю от вершин множества Ю нли от входа е не превосходит суммы количеств ключевых вершин исходных схем.
2.5. Корректность алгоритма э(. Граф О (В», Яг) устроен так, что всякий путь ю в нем имеет прообразы в схемах Я» и Вг. Мы будем называть их проекциями пути ш. Для» = 1, 2 положим пр» (ю) = пустой путь, если»с — пустой путь; пр, (ю) = ю„если ю = е, где ю» — путь по операторам луча, начинаю»цегося выходной дугой начального оператора схемы Я» н заканчивающегося дугой, которая ведет к некоторой ключевой вершине; пр, (»е) = пр» (и'), если и» = ю'ое, где е — дуга, которая ие является Я;»»угой в О (Ям Вг); ир» [и) = пр» (ю') А»и~о если ю = и'ое, где е — В»-дуга вершины о = (А„А„з), причем если е — Л-дуга, то и~» — путь по операторам луча в В», начинающегося й-дугой расповнавателя А» н заканчивающегося дугой, которая ведет к некоторой ключевой вершине.
Л е м ма 7.7. Пусть о = (А, В, з) — достижимая вершина грау»а О (Ю„Яз), а ю — произвольный путь от входа е, и о. Тогда !56 если (х = у) (=- аэвегС (г) длл х Е— : Хг и у (== Хг, то г (пр1 (ы), х) = == С (пр (ю), у); если (Л = и) Е= авгегС (г), то логическое выражение и Л-игбиэючно либо на пути прг (и), либо на пути прг (ю). Д о к а з а т е л ь с т в о.
Сформулируем задачу глобального анализа для графа О (8„8г). В качестве полурешвткн свойств возьмем (2', /~). Начальная разметка сопоставляет сеть 6 входу е и 1 всем остальным дугам. Семантическую функгвпо разметки определим следующим образом: урр.<,~ о урр,н,1, если е = е'= е '„ уррб ь если е — недуга вершины р, а дуга е' ведет к р; 1, в остальных случаях, где у — преобразователь сетей, использованный в доказательстве теоремы 7.5.Функцию ~ распространим, как в гл. 2, на пронавольные пути в в О (Ям 8г), начинающиеся входом ег и кончающиеся некоторой дугой е.
гь если ю = ее йю ~; о у„, если ю = иУре. Тогда для сформулированной задачи глобального анализа существует стационарная разметка (г, причем в силу теоремы 2.1 имеем р (е) ь, /~ 2„(6) для всех дуг е графа О (Я„Яг). Легко видеть; что граф О (8„8 ) построен вместе с его стационарной разметкой р. Более точно, для каждой вершины р = (А, В, г) и для всех ведущих к ней дуг е справедливо р (е) = г.
Поэтому если х Е= Хы у ~— : Хю и — произволыэый путь от ер к р = [А, В, г), то из (х = := у) ~ аээегС (г) следует (х = у) Е авэегС (у (6)). Функция 2 представляет собой в конечном счете суперповицию эффектов присваивания и аффектов тестов, которые коммугативны, если соответствуют операторам разных схем, т. е. 4'-/" = 1" ° 4'.
осли е1 и е2 — дуги схем 8 и Яг соответственно. Коммутативность преобразователей является следствием условия разделенности переменных этих схем. Более того, нетрудно видеть, что у юу =у еу где ю, (С = 1, 2) — произвольный путь в схеме 81. Поэтому ив (х = у) ~ аэгегС ф, (6)) получаем С (прг (ю), х) = С (прг (и) пр (и>), х) = С (пр (и) пр (в), у) = М (пр (в), у). Аналогично, если (Л = я) Е= аззегС (г), то (Л = м) Е= аэзегС (2„(6)) = = аэгегс (урра 1 о урра > [6)), откуда следует, что логическое выражение н является Л-избыточным либо на пути пр (и), либо на пути прг (ю). П Будем говорить, что путь ю в графе О (8м 8 ) согласован с интернрежацивй 1, если пути пр (ю) и прг (ю) явлшотся начальпы- Сэт ми отрезками цепочек схем 8 и 8, подтверждаемых интерпретацией 1. Количество 8;~~уг пути в навозом Бд-длиной этого пути (обозначение: [епд (в)).
Т е о р е м а 7.9. Если 8 ь Яг, лю алгоритм з( гаканчиеается бег успеха. Д о к а з а т е л ь с т в о будем вести от противного. Предположим, что Яд ~- 8, и алгоритм $( заканчивается успешно. Пусть 1 — интерпретация, для которой ча1(о„1) ~ ча1(8„1), а вд (д = 1, 2) — допустимая цепочка схемы Яо подтверждаемая интерпретацией 1. Покажем, что для любых лд, яг таких, дто яд не превосходит количества распознавателей цепочки в,(д = 1, 2), существует согласованный с 1 путь в в графе О (Яд, Яг), для которого ч д' = 1, 2 1епд (в) =г яд.
Путь в начнем входом ег и будем продолжать построение в добавлением вершин и дуг. Пусть иа некотором шаге уже построен согласованный с 1 пуп в', который кончается дугой, ведущей к вершине г = [Ад, Аг, г), и для некоторого й (1 ~ я ~( 2) 1еп„(в') ~ я„. Тогда хотя бы одна извершин А„А — распознаватель, н из вершины г выходит хотя бы одна дуга. Рассмотрим два возможных случая. Случай 1.
Из вершины и выходит хотя бы одна Яг-дуга. Выберем тогда Л ~= (О, 1) так, чтобы путь в„в 8„был продолжением пути прг (й) по Л-дуге распознавателя А„и Л ~= (О, 1), Л ~ Л. Если бы среди Яз-дуг вершины и не было Л-дуги, то по построению графа О (Яд, Яг) это обозначало бы (Л=ал„) ~ аззегс (г), а в силу леммы 7.7 и Л-избыточность теста а„„на одном из путей пр (в') или прг (в'), что противоречит допустимости цепочек в, и вг.
Таким образом, среди 8„-дуг вершиньд и имеется Л-дуга е. Воаьмем тогда согласованный с 1 путь и" = в'ие и будем продолжать построение пути в добавлением вершин и дуг к в'. Случай 2. Иа вершины и не выходит ни одной 8„-дуги. Будем считать для определенности й = 2 (симметричный случай й = 1 рассматривается совершенно аналогично). Тогда из и выходит. хотя бы одна 8-дуга, и мы можем действовать как в случае 1, получая согласованные с 1 пути добавлением новых вершин и Яддуг до тех пор, пока не будет доствтяута вершина, из которой выходит хотя бы одна Яг-дуга. Когда тацая вершина достигнута, выберем для продолжения Яд-дугу. Если бы все согласованные с 1 продолжения по Яд-дугам проходили только через такие вершины, у которых иет Я -дуг, то зто означало бы существование контура в графе О (Юд, Яд), проходшцего по вершинам из Ог, т.
е. противоречие с предположением об успешном окончании алгоритма и. Итак, если один из результатов ча[ (8„1) определен, а другой — нет, то построенный описанным способом путь в ведет к вершине, для которой истинно одно нз условий (Зб) нли (Зз), так что алгоритм з( не может заканчиваться успешно.
Если же ча[ (8„1) и ча[(ог,1) определены, то путь в ведет к вершине о = [Ад, А, г) такой, что Ад — заключительный оператор стоп 158 (х, ..., и,„), А — заключительный оператор стоп (у,..., у„). В силу предположения об успешном окончании алгоритма % имеем т = и и т с (1 «( с «( п) (х,'= у,) я аззегс (г), так что по лемме 7.7 чС (1 ~ С «( и) С(пут (ю), х,) — — С(прг (в), ус).
Это дает немедленное противоречие с та1(Я„1) чъ та1(8г, 1). [ 3 Для доказательства успешного окончания алгоритма з( в случае эквивалентности исходных схем введем несколько вспомогательных понятий. Понятие квагисвободной интерпрелшции обобщает понятие свободной интерпретации и отличается от него только тем, что квазисвободная интерпретация сопоставляет переменным произвольные термы иэ области интерпретации.
Областью квааисвободных интерпретаций служит, как н в случае свободных интерпретаций, множество всех функциональных термов. Будем говорить, что квазисвободная интерпретация Е согласована с сетью в (г Ф $), если для нее истинны все утверждения нэ аззегъ (г), т. е. (х — — т) ~ аззегФ (г) -> 1 (х) =- 1 (т), (Л = я) Е= аззегз (г) =+ 1 (я) = Л, Через С1 (г) обозначим множество всех кваэисвободных интерпретаций, согласованных с сетью г. Положим С1 (1) = Я по определению. Две вершины А, В (одной и той же или разных стандартных схем) назовем г-вявиваленлтььви (обозначение: А * В), если ЪЧ б= С1 (г) та1 ф(А), 1) та1 (8 (В), 1), где через 8 (А) обозначена схема, получающаяся нз схемы, содержащей вершину А, заменой ее началъного оператора на такой оператор старт, выходная дуга которого направляется к вершине А, а множество резулътатов определяется требованием правильности получающейся схемы.
Заметим, что из этих определений непосредственно вытекают два следующих полезных свойства: г ( г =Ф С1 (гг) с:. С1 (гг), еВбеАиВ На множестве переменных Ю введем какой-нибудь полный порядок ««и определим множество базовых переменных Ьаз (г) для произвольной сети гЕ Я', гчъ Я: Ьаз(г) = (х(Зги= У, (х е )пюи, (и)) й (Ьпомв (Р) С Ю) Й ( ту е йпотгв (о) х ««у)). Неформально это множество всех таких переменных х, для которых правая часть всякого утверждения вида х = т из аззегз (г) является переменной, которая не меньше, чем х. Две кваэисвободные интерпретации 1„1, называются соглаеованнзьви, если для любого логического выражения я справедливо 1, (я) = 1г (и).
В классе квазисвободных интерпретацнй С1 (г) выделим подкласс МС1 (г) минимальных интерпретаций 1, И59 для которых х, если х 6= Ьае (г), 1(х) = т, если (х =т) ~ аггее(г) н т — терм над переменными иэ Ьаэ(г). Минимальные интерпретации, согласованные с 8, играют такую же роль по отношению и кваэнсвободным, согласованным с сетью г, какую свободные интерпретации играют по отношению ко всем интерпретациям базиса, Л е и и а 7.8. Для всякой интериретации 1 ~ С1 (г) суще.
ствует согласованная с ней интерпретаиия Г ~ МСХ (г). Для всех минилшльных интерпретаций Г, согласованных с 1 ~= С1 (з), ~ ~Т 1()=1(Г()), тЮ та1(8„1) ~ 1 (та1 (8, Г)). Л е м м а 7.9. чЧ Е= СХ (г) та! (Юг 1) ~ та1 (Вг, 1) <=ь <=> УХ Е= МС! (г) та1 (В, 1') ж та1 (8, 1 ). Д о к а э а т ел ь с т в о лемм 7.8 и 7.9 проводится аналогич- но доказательству лемм 4.3, 4.4 и теоремы 4А. Таким образом, для докаэательства г-эквивалентности двух вершин А, В доста- точно убедиться, что ЪЧ е= МС1 (г) та1 (Я (А), 1) та1 (8 (В), Х)- П Л е м и а 7АО.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
