1626435694-d107b4090667f8488e7fa1ea1b3d0faa (844295), страница 54
Текст из файла (страница 54)
Обобщенные входы указываются жирными стрелками, входы (любые) метятся римскими цифрами, выходы — арабскими цифрами. Условия и метящие булевы функции записываются в виде логических формул. Сделанные определения поясняет пример фрагмента на рис. 8.3. В нем указывается, что к верхнему распознавателю обяаательно $8.2. коргиктность исчисления подходит некоторая дуга. В оператор А извне могут входить любые дуги.
В нижний распознаватель помимо входной стрелри могут вести извне любые дуги, но среди них не может быть ни одна из выходных дуг фрагмента, помеченных цифрой 3. Пометка двух выходных дуг одной и той же цифрой означает, что обе эти дуги должны вести,.к одной и той же вершине схемы. Исчисление равносильных преобразований схем Янова изображено на рис. 8.4 и 8.5. В посылках правил П1 и П2 символ у означает каантар всеобщности, с помощью которого формулируются утверждения вида зг (Т)(Р), звучащие в данном случае следующим образом: «для любого объекта вида Т, который можно усмотреть в преобразуемой схеме Янова, удовлетворяется свойство Р».
$ 8.2. Корректность исчисления Справедливость логических и топологических аксиом после их содержательного обсуждения в предыдущем параграфе очевидна и не требует дополнительных рассуждений. Верхняя разметка. Рассмотрим правила верхней разметки. Из аксиом видно, что при верхней разметке дуг схемы единственным безусловным источником наборов значений предикатных переменных является входная стрелка.
Аксиома А9 переносит на выходные дуги распознавателя лишь те наборы, которые поступают на его вход. Аксиома А10 порождает лишь те наборы, которые могут получиться из наборов, поступающих иа вход оператора, применением операции взятия максимума (заметим, что шах (1) = 1 для любого Р).Таким образом, если в результате применения' аксиом А7 — А10 на дуге в, ведущей к некоторой вершине У схемы, появилось множество наборов у, то ато значит, что каждый из этих наборов мог появиться на дуге лишь в результате применения аксиом А7 — А10 к цепочке фрагментов схемы, образующих путь от входной стрелки до вершины У ггг . Рг Ь ~~-г р Д д ... 1/,' и Ряс.
8.6. Путь верхвей разметки. (рнс.. 8.6). Более точно это формулируется так: для любого Ь, такого, что ~р(Л) = 1, существует путь в схеме от входной стрелки до вершины )г, образованный вершинами Р„..., У, и дугами, помеченными функциями ~р„..., <р„где У„=)г, ~р,=1, ~р, ии <р, 266 ГЛ. 8. ИСЧИСЛЕНИЕ РАВНОСИЛЬЫЫХ ПРЕОБРАЗОВАНИЙ а также существует последовательность наборов А„ ..., А„= А, удовлетворяющие следующим требованиям: 1) г«(А;) =1, 2) если К«(1(~1~ (г — 1) — распознаватель с условием Р, то А;+ = Лп причем Г(А«) = 1, если У«соединен с У«вд плюс- стрелкой, и Г(А«) = 1 в противном случае; 3) если У«(1( «( г — 1) — преобразователь с оператором А(Р), то Ь«+«отличается от Ь«не более чем значениями переменных, принадлежащих Р.
Мы уже указывали, что набор А называется допустимым для вершины У схемы, если в процессе порождения конфигурации ($7.3) возможен переход к вершине К с набором А. Только что проведенное рассуждение доказывает допустимость для У любого набора, принадлежащего функции «о, метящей какой-либо вход вершины Г. Назовем множество ФР всех допустимых наборов для вершины У полным условием работы этой вершины.
Нами доказана Л е м и а 1. Если к вершине У подходит дуга с пометкой «р, то «Р~ фо, Непосредственно из вида аксиом А9 и А10 вытекают такие леммы Л е м м а 2. Если плюс- и минус-стрелки распознавателя с условиел«Р' помечены функциями ()+ и () соответственно, то 3+-~Р, Р+д 3 =1 и Рд,() =1. Л е и и а 3. Если к распознавателю в обозначениях леммы 2 подходят т дуг, помеченных функциями «р«,..., «р, то ()+Ч 1-~Ч~«Ч " Ч %и. Л е м и а 4. Если к оператору А(Р) подходят т дуг, помеченных функциями «о„..., «р, и выход оператора помечен функцией (), то 'р ~ шах («г« ~/ ... ~/ «р ).
Назовем состояние схемы Янова, при кдтором выполнена посылка правила вывода П1, стационарной верхней разметкой. Это название, уже употреблявшееся неформально в предыдущем параграфе, оправдано тем, что в условиях стационарной разметки никакое дальнейшее применение аксиом А9 и А10 не изменит верхней разметки дуг схемы. Очевидна Л е м м а 5. В условиях стационарной верхней разметки и ,в обозначениях лемм 3 и 4 для любого распознавателя р+Ч(1 =— р«Ч'"Чц % 8.2. кОРРектность исчисления 2ат и для любого оператора А(Р) ()=шах (ф, /',... '/~ ~р ). Смысл правила П1 устанавливает следующая 'Л е ы м а 6. В условиях стационарной верхней разметки для любого распознавателя В с пометками на его выходных дугах ()».
и р Доказательство.Импликация р+~/() АРФЕ вытекает из лемм 1 и 5. Докажем импликацию Фя-э()+ ~/ р . Пусть набор Л является допустимым для распознавателя В. Это значит, что существуют путь движения от входной стрелки к вершине К через вершины Гп..., У„=В итакая последовательность наборов Л„...
Л,=Л, что при движении по схеме к вершине У8 подходили с набором Л; (1=1,..., г). Пусть теперь в пути через вершины И„ ..., У, проходимые входная стрелка и дуги в условиях стационарной разметки помечены функциями ~Р„ ..., ср, Покажем по индукции, что ~р,(Л;)=1(1 = 1,..., г). Для 8=1 это очевидно, так как юг=1, Пусть чч- (Л»- )=1. (1) Пусть У; т — распознаватель с условием Г и с пометками ()+ и р на выходных дугах. В этом случае Л,=Л,, (2) В силу стационарности разметки ~р,,~()+'»/р, значит, в силу (1) 1+(Л -2) Ч1-(Л»-2) =1 ' (З) Если т(Л»,)=1, то ч =1+ (4) и в силу леммы 2 не может быть, чтобы р (Л;,)=1.
Значит, зоилу (3) р+(Л;,)=1 и в силу (4) и (2) ф,(Л;)=1. Если Р(Л,,)=1, то »р»м() и, рассуждая аналогично, по лемме 2 и (2) получим также, что ф;(Л;)=1. Пусть У,,— преобразователь с оператором А(Р) с пометкой на выходе. Пусть /ь — функция, для которой Л является ее множеством истинности. Поскольку Л;, и Л, отличаются не более чем значениями переменных из Р, то г шах /а»» (Л») = 1. (5) Но в силу (1) (6) шах /ь,, э шах <р» Р гзд ГЛ. 8.
ИСЧИСЛЕНИЕ РАВНОСИЛЬНЫХ ПРЕОБРАЗОВАНИЙ и в силу стационарности п1ах ~рр 1 -э <р„ откуда в силу (5) и (6) получим, что ~р8(А,)='1. Ваяв доказанное утверждение индукции для р=г, получим, что ц„(А)=1; отсюда по лемме 5 доказывается требуемая имплнкация, а с ней и лемма 6. Нижняя разметка. Рассмотрим теперь правила нин:ней разметки. Л е и и а 7. В условиях стационарной нижней раеметки для любой вершины У схемы 6 функция ЧР, метяирая входы вершины У, тождественна функции ПР, истинной на множестве продуктивных наборов для У. Д о к а з а т е л ь с т в о.
Утверждение леммы в части нмпликации П,~У, очевидно, так как любая последовательность вершин от У к Я и та последовательность наборов, с которыми зги вершины проходятся при построении любой остаточной конфигурации, продуцнруемой набором А и вершиной У, взятые вместе и прочитанные в обратном направлении, задают последовательность применения аксиом А11 — А14, создающих разметку на входе У, включающую набор А. В силу стационарности любая последовательность будет заведомо реализованной. Пусть теперь, наоборот, известно, чтоЧ"Р(А)=1. 1'огда существует последовательность Я вершин схемы У=У„У„..., У, =-Я и последовательность функций Ч'Р не Ч'„Ч',,..., Ч'„=1, метящих дуги между этими вершинами, обладающие следующим свойством: для любого отрезка Х последовательности, обрааованного одними только распознавателями и ограниченного либо операторамн, либо (слева) началом, либо (справа) остановом: существует реалйзующий набор А, принадлежащий всем мстящим множествам из отрезка Х, и который, будучи поданным на начало Х, пройдет в графе переходов по вершинам, образующим Е.
При етом: (1) если началом последовательности Я таян:е является отрезок распоанавателей Хо, то А мон8ет быть его реализующим г В.г. Когвектность исчисления 299 шаборогц (2) если отрезки Х и Х' разделяются оператором А(Р), "то наборы А и А', реализугощие эти отрезки, образуют пару (Ь, А'), допустимую для А(Р). Сделанное утверждение, которое яв.ляется перефраэировкой правил применения аксиом А11 — А14, сразу дает конструкцию остаточной конфигурации, продуцируемой набором Ь и вершиной Р.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
