1626435694-d107b4090667f8488e7fa1ea1b3d0faa (844295), страница 55
Текст из файла (страница 55)
ху Л е м и а 8. В условияа стационарной нижней равягеткилюбое применение правила П2 корректно. Доказательное рассуждение уже проведено в предыдущем па,раграфе при введении понятия нигкней разметки. ~7 Отношение равносильности. Заметим, что поскольку схема ш целом является частныи случаем понятия фрагмента, правила ПЗ и П4 позволяют выводить соотношения равносильности для схем. Свойства равносильности как бинарного отношения выражает Л е и и а 9. Отношение равносильности рефлексивно, сиэьиетрично и транаитивно. Д о к а з а т е л ь с т в о. Рефлексивность следует нз прави.ла ПЗ при одинаковых сг и ().
Симметричность следует из правила П4, если в качестве посылки взять следующие соотношения: Уг Уг Уг ,Доказательство транзитивности требует Ь качестве посылки соот- :ношения Уг У Уг ~г э(о симметричности эту посылку можно переписать в видо Уг Уп Уг Уг, е откуда по правилу П4 вытекает, что У, Уг. г7 Формальную воэможность трактовать рассмотренную аксиовгатику как правила преобрааования схем предоставляет Л е м м а 10 (п р а в и л о п о д с т а н о в к и). Если 'Яг 9г, то У(У )-У (У,). Д о к а з а т о л ь с т в о.
Взяв в правиле П4 в качестве посылки У, У „У (У,)-У (У"г), получим, что 9 (9,) У'(9,), откуда в силу симметричности вытеевает утверждение леммы.~7 3 а м е ч а н и е. Свойство симметричности в соединении о правилогг подстановки гарантирует обратимость системы преобразований, задаваемой аксиоматикой. Справедливость правила П4 была установлена при неформальном обосновании аксиоматики в предыдущей главе. 270 ГЛ. З. ИСЧИСЛЕНИЕ РАВНОСИЛЬНЫХ ПРЕОБРАЗОВАНИЯ Проведенное вьппе содержательное иаучение исчисления равносильных преобразований резюмирует Т е о р е м а 3. Л'юбые две равносильные операторные схемы Янова эквивалентны.
й 8.3. Канонические схемы и технические теоремы Каноническиеехемы. Схема Янова 6(р„..., рь) с операторами А„..., А„называетсв матричной, если она содержит (н+1)э распознавателей В„(Р;;) (1=0,...,и; у=1,..., и+1), один распознаватель — заглушку 8, соединенных следующим образом: 1. Каждый распознаватель ВО имеет один вход.
2. В распознаватель Вм ведет входная стрелка, в распознаватель Вы (у=-1,..., и) ведет выходная дуга оператора А;. 3. Плюс-стрелка распоанавателя В;у(1=0,..., и;у=1, . ', Л) ведет к оператору Ау, а минус-стрелка — к распознавателю Вьу+Р 4. Плюс-стрелка распоанавателя Вь„э, (1=0,..., и) ведет к астапову, а минус-стрелка к заглушке ®. 5. Условия гы (1=0,..., н; у=1,..., и+1) удовлетворяют соотношениям Ге„если у, = у, гп,й рп, ш т е с т если у,ть ум 6. Каждое условие есть иля 1 илн имеет вид диэъюнктнвной совершенной нормальной формы. Оператор А схемы 6 называется выполнимым, если существует конфигурация схемы 6, содержащая А. Канонической схемой Янова нааывается матричная схема, все операторы которой выполнимы, и з которой всеусловия истинны только на своих допустимых я продуктивных наборах.
Пример канонической схемы Янова (эквивалентной примеру с рис. 7.9) указан на рис. 8.7. Две схемы Янова нааываются равными, если они сравнимы, их графы переходов изоморфны, имеют одинаковое распределение плюс- и минус-стрелок, а соответственным вершинам сопоставлены одни и те же операторы н условия. Специфические свойства канонических схем устанавливает Т е о р е м а 4. Если две канонические схемы Янова не равны', то они не эквивалентны. Д о к а з а т ел ь с т в о. Если неравные канонические схемы содержат неравное количество операторов или неодинаковые операторы, то множества'конфигураций'этих схем не будут совпадать в силу выполнимости каждого из операторов.
Таким образом, % а 2. канонические схемы и технические теОРемы 871 остается рассмотреть лишь сравнимые схемы 6, и 6„содержащие одинаковый набор операторов Аы ..., А„. Если такие схемы ие равны, то это значит, что существует такой набор Л и такой распознаватель Я(т, что Г()Р(Л) = Ф (1) и р(2) (Л) (й) где Рп иуп — условия,сопоставлеяиыеВ)7 в схемах 6, и 6 (!) (2) Рнч( 8.7. т(аноннчеснан схема Нноеа. соответственно. В силу (1) набор Л являетсядопустимымнпродуктивпым для распознавателя Л(т.
Это значит, что для 6, существует конфигурация, начало которой имеет вид .Л,...Л, Л (3) А;,... А, *). Если для схемы 62 ие существует конфигурации, начало которой имеет вид (3), то неэквивалентность 6, и 6, доказана. Пусть 6, также имеет конфигурация), начало которои равно (3). Тогда, очевидно, в силу (1) и в силу свойства 5 матричных схем в схеме 6, после символа А, в рассматриваемой конфигурации окажется символА) (или останов, если у=я+1), а в схеме 6 ') Здесь А( — операторный симеон оператора А( 272 ГЛ В.
ИСЧИСЛЕНИИ РАВНОСИЛЬНЫХ ПРВОБРАЗОВАНИЙ окажется наверняка не символ А1. Это утверждение завершает доказательство теоремы 4. т7с7 Техпическиетеоремы. Очевидно, что основным применением построенного исчислекия будет доказательство возможноств ТТТ аида 1(ли У) ТТЕ а с ТТ0 а ТТ7 а 1 ТТ10 Если алр=с ис ТТ0 1711 Если а А0 иЕ си 1 С - 1 У Рис. 8.8.
Технические теоремы. построить для любой схемы Янова равносильную ей каноническую схему. Для этой цели потребуется целая серия дополнительных 0 1 С 0 ТТ,7 а г~л а а Л а 1 1 1 1 ТТЕ 1 /1 1 0 ТТР а см а' х 1 У 1 01 теф ф ф~~ф Сф д 8.3. канонические схемы и технические теОРемы 375 77;Р" Гъ.Я ЛУ-А 77Ут 1 1'яс. 8.11. Докааатеаьства техвиаеских теорем (ТТ9 — ТТ11). ТУУУт ~ийфит7 ПУХ: фйфит",т гм чайф и гм ф а г У,т Х гГ А- 276 ГЛ 8.
ИСЧИСЛЕ1П1Е РАВНОСИЛЬНЫХ ПРЕОБРАЗОВАНИИ правил преобразования, которые будут ниже упоминаться под названием технических теорем (ТТ). Каждая техническая теорема имеет вид выводимого соотношения равносильности между некоторыми фрагментами 91 и У 8; формулировки одиннадцати технических теорем приведены на рис. 8.8. Доказательства этих теорем, приведенные на рнс. 8.9 — 8.11 имеют вид цепочек равноснльностей, начинающихся и кончающихся фрагментами у 1 и у"8 соответственно. Над каждым знаком равносильности указывается ссылка на аксиому, правило вывода, или ранее доказанную техническую теорему, в силу которой справедлива данная равносильность. Ссылка, помеченная звездочкой, означает применение аксиомы или теоремы в инверсной форме, т.
е. когда правая часть соотношения равносильности, образующего утверждение, заменяется на левую. Единственное доказательство, которое, быть может, требует дополнительных замечаний, — это теорема ТТ6-Б. Поскольку фрагмент, о котором идет речь в теореме, не имеет входов, разметка его, сделанная по аксиоме А7, будет инвариантна по отношению к любому вхождению этого фрагмента в какую бы то ни было схему. Поэтому применение правила П1 допустимо. Дадим наперед несколько топологических определений.
Последовательность распознавателей В„..., В, в схеме называется цепочкой, если В1 имеет В1».1 своим преемником (1=1, . ..., г — 1). Цепочка называется правильной, если каждый распознаватель из цепочки имеет только один вход. Замкнутая цепочка (В, соединен с В,) называется циклом. Распознаватель, у которого один из выходов является одновременно его входом, называется пол уциклом. 3 8.4. Полнота исчисления Основу данного параграфа составляет Теорема 5. Для любой схемы Янова б существует равносильная ей каноническая схема 6х.
Доказательство теоремы будет дано в виде алгоритма преобра- эованиЯ схемы б в схемУ 1"х ИУтем послеДовательного пРименения аксиом, правил вывода и рассмотренных выше технических теорем. Формирование цепочек. 1 - й ш а г. Стандартизация распознавателей. По правилу ПЗ условие в каждом из нетоя»дественно ложных распознавателей записывается в совершенной нормальной дизъюнктивной форме, а затем по аксиоме АЗ все распоанаватели расчленяются так, что условие в каждом распознавателе имеет вид элементарной конъюнкции (заметим, что любые элементарные конъюнкции 61 и 68 либо равны, либо ортогональны, т е. 61о162=1) $8А.ПОЛНОТА ИСЧИСЛЕНИЯ 277 2-й ш а г .
Перенос плюс-стрелок. Определим процесс переноса плюс-стрелок к)8ждого из распознавателей В схемы по следующему правилу: а) если  — заглушка, стрелка не переносится; 6) если Л вЂ” полуцикл, применяется теорема ТТ7; в) если плюс-стрелка от В ведет к преобразователю, останову или ааглушке, стрепка не переносится; г) если плюс-стрелка от Л(и) ведет к распознавателю В()1), то применяется аксиома Аб, если аж(1, и ТТ11, если ай()— = 1. Будем последовательно применять этн правила к каждому из,распознавателей схемы. Кроме того, если какой-либо из распознавателей в силу переноса стрелок окажется без входа, то он сразу же уничтонгается по теореме ТТ6. При переносе плюс-стрелки могут встретиться два случая: А.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
