оки4 (1155747), страница 2
Текст из файла (страница 2)
Действительно,x1 ∨ x2 |⇒ x1 ∨ x2 7→ (x1 ) · (x2 ) 7→ x1 · x2tM¬1tM&tM¬В отличие от тождеств (2.1)–(2.2) главы 1 данные тождества подстановки констант ориентированы на базис Б0 , где роль константы 0(константы 1) играет формула вида xi · xi (соответственно xi ∨ xi ).§1. Эквивалентные преобразования формул9иx1 ∨ x2 7→ x1 ∨ x2 7→ x1 · x2 7→ x2 · x1 |⇒ x2 ∨ x1 .tM¬tM∨tK&MtM& , t¬Аналогичным образом доказывается, что A M OΠ M t& , τ|⇒ tA|⇒ tOΠ,∨ , t& , τ∨DΠKMt&,∨ , τ M |⇒ tD|⇒ tΠKσ,∨ ,∨,& и tσ,& , τгде σ ∈ {0, 1}. Завершая примеры выводимостей, докажем,что ΠK DK OΠt1,& , t&,∨ , tA|⇒ tΠ .∨ , t∨ , t∨Действительно,x1 ∨ x1 x2 7→ x1 (x2 ∨ x2 ) ∨ x1 x2 7→ x1 ((x2 ∨ x2 ) ∨ x2 )tΠK1,&tD&,∨|⇒ x1 ((x2 ∨ x2 ) ∨ x2 ) 7→ x1 (x2 ∨ x2 ) 7→ x1 .KtA∨ ,t∨tOΠ∨tΠK1,&ПоложимΠK ΠKM A K OΠ Dτ осн = tM& , t¬ , t& , t& , t& , t&,∨ , t1,& , t0,& ,Aτ A = tA& , t∨ ,Kτ K = tK& , t∨ ,OΠτ OΠ = tOΠ,& , t∨DDDτ = t&,∨ , t∨,& ,ΠK ΠK ΠKτ ΠK = tΠK0,& , t1,& , t0,∨ , t1,∨ ,τeосн = τ M , τ A , τ K , τ OΠ , τ D , τ ΠK , tΠ .Систему τ осн будем называть системой основных тождеств,а систему τeосн — расширенной системой основных тождеств.
Рассмотренные выше примеры выводимостей доказывают следующее утверждение.10Глава 4. Эквивалентные преобразования управляющих системЛемма 1.1. Система τeосн выводима из системы τ осн .Покажем теперь, что с помощью ЭП на основе системытождеств τ осн из любой формулы можно получить совершенную ДНФ или формулу x1 x1 . Введем для этого некоторые понятия, характеризующие формулы, появляющиесяна промежуточных этапах указанного ЭП. Произвольнуюконъюнкцию букв, содержащую, в общем случае, повторяющиеся или противоположные буквы, будем называть обобщенной ЭК (ОЭК), а дизъюнкцию таких конъюнкций, содержащую, в общем случае, повторяющиеся «слагаемые», —обобщенной ДНФ (ОДНФ).
Обычную ЭК (ДНФ) и формулуx1 · x1 будем считать канонической ОЭК (соответственно канонической ОДНФ), а совершенную ДНФ и формулу x1 · x1— совершенными ОДНФ. Напомним (см. ??), что формула,в которой все ФС ¬ применяются только к БП и нет двухпоследовательно применяемых ФС ¬, называется формулойс поднятыми отрицаниями.Пусть формула F (x1 , .
. . , xn ) реализует ФАЛ f (x1 , . . . , xn ).Докажем существование ЭП видаF |⇒ F0τMbF00 |⇒ F|⇒{KtD&,∨ ,t&}τ ΠΠeF,|⇒{ΠΠtD&,∨ ,τ(1.2)}где τ ΠΠ = τ A , τ K , τ ΠK , τ OΠ , tΠ , F0 — формула с поднятыbиFe — каноними отрицаниями, F00 — обобщенная ДНФ, а Fческая и совершенная ОДНФ ФАЛ f соответственно. Действительно, поднятие отрицаний, то есть переход от F к F0в (1.2) (см. ??) можно осуществить применением тождествMMtM¬ , t& и t∨ к подформулам вида (F1 ), (F1 · F2 ) и (F1 ∨ F2 )соответственно до тех пор, пока все такие подформулы небудут «устранены».
Переход от F0 к F00 в (1.2), который называется раскрытиемno скобок, осуществляется применениемDKтождеств t&,∨ , t& к подформулам вида F1 · (F2 ∨ F3 ) или§1. Эквивалентные преобразования формул11(F1 ∨ F2 ) · F3 до тех пор, пока они встречаются в преобразуемой формуле.b в (1.2), который называется привеПереход от F00 к Fдением подобных, выполняется в три этапа. На первом этапе каждая ОЭК K 00 из ОДНФ F00 преобразуетсяв канониnoOΠΠKK , аческую ОЭК K с помощью тождеств t& , t0,& , tA,t& &также тождестваxi · xi = x1 · x1 ,(1.3)которое выводится из них следующим образом:xi · xi 7→ (x1 · x1 ) · (xi · xi ) 7→ (xi · xi ) · (x1 · x1 ) 7→ x1 · x1 .tΠK0,&tK&tΠK0,&bНа втором этапе полученная формула F̌ преобразуется в Fпутем «устранения» повторных вхождений равных элементарных конъюнкций или подформул x1 · x1 с помощью тождеств τ A , τ K , tOΠи, в случае f 6≡ 0, последующего«устра∨K , tΠK .нения» ОЭК x1 · x1 с помощью тождеств tA,t∨ ∨0,∨Заметим, что первые два этапа приведения подобных,на которых происходит приведение повторений БП в ОЭК иb Однако, для уменьЭК, уже дают нам искомую формулу F.шения числа шагов в последующих ЭП можно выполнитьтретий этап приведения подобных — этап приведения поглощений ЭК.
На каждом шаге этогоэтапа в полученнойДНФ с помощью тождеств τ A , τ K выделяется подформула вида K 00 ∨ K 00 · K, где K 00 и K — некоторые ЭК, а затемЭК K 00 · K «устраняется» с помощью ЭПK 00 ∨ K 00 · K 7→ K 00 .tΠЗаметим также, что раскрытие скобок и различные этапыприведения подобных можно чередовать друг с другом приbЭП подформул формулы F0 или формул F00 , F.beПереход от F к F в (1.2) выполняется в два этапа. Сначаb которая имеет ранг r, где r = n − q <b из F,ла каждая ЭК K12Глава 4. Эквивалентные преобразования управляющих системn, и не содержит букв БП xi1 , .
. . , xiq , приводится к ее соe от БП X (n) в результате следующеговершенной ДНФ KЭП:b |⇒ Kb (xi ∨ xi ) · · · xiq ∨ xiq |⇒ K.eK11tΠK1,&tD&,∨Затем в полученной ОДНФ устраняются повторные вхождения слагаемых так, как это делалось ранее при переходеb и в результате мы приходим к совершенной ОДНФот F̌ к F,eF. Таким образом, доказано следующее утверждение.Лемма 1.2. Любую формулу F (x1 , .
. . , xn ), реализующуюФАЛ f , с помощью ЭП на основе системы тождеств τ оснможно преобразовать в совершенную ОДНФ ФАЛ f от БПX (n).Рассмотрим описанные выше ЭП на примере формулыF = (x1 ∨ x2 ) · (x1 · x3 ) · (x2 ∨ x3 ) ,для которойF 7→ (x1 ∨ x2 ) · (x1 ∨ x3 ) · (x2 ∨ x3 )tM&F0|⇒{bFx1 x2 x3 ∨ x1 x2 ∨ x1 x2 x3 ∨ x2 x3ΠΠ \tΠtD&,∨ ,τ|⇒= F0 ,b= F̌ = F,}x1 x2 ∨ x2 x3b 0,=Fx1 x2 x3 ∨ x1 x2 x3 ∨ x1 x2 x3 ∨ x1 x2 x3e= F.{τ A ,τ K ,tΠ }b0F|⇒{ΠΠtD&,∨ ,τ}Теорема 1.1. Система τ осн — полная система тождеств.Доказательство. Пусть F0 и F00 — эквивалентные формулы,реализующие равные ФАЛ f 0 и f 00 соответственно, а наборx (n) = x содержит все различные БП, встречающиеся в F0§2.
Преобразования на основе тождеств13e — совершени F00 . Пусть, далее, ФАЛ f (x) равна f 0 и f 00 , а Fная ОДНФ ФАЛ f от БП X (n). В силу леммы 1.2, имеетместо ЭПe |⇒ F00 ,F0 |⇒ Fτ оснτ оснкоторое доказывает теорему.§2Эквивалентные преобразования схем из функциональных элементов и моделирование с ихпомощью эквивалентных преобразований формул. Моделирование эквивалентных преобразований формул и схем в различных базисах, теорема переходаРаспространим введенные в §1 понятия и обозначения напроизвольный класс схем U. В соответствии с определениями из §1 эквивалентность схем Σ0 и Σ00 из U имеет местотогда и только тогда, когда Σ0 и Σ00 реализуют равные системы (матрицы) ФАЛ. При этом, обычно, предполагается,что соответствующие друг другу полюса (выходы, входы) вΣ0 и Σ00 имеют одинаковые пометки, а эквивалентность Σ0 иΣ00 записывается в виде тождестваt : Σ0 ∼ Σ00 .Для схем из U, как и для формул, определяется ряд«простейших» преобразований, сохраняющих эквивалентностьсхем, которые называются подстановками.
Тождествоb0 ∼ Σb 00 ,bt: Σкоторое получается в результате применения одной и тойже подстановки к обеим частям тождества t : Σ0 ∼ Σ00 , называется подстановкой тождества t. Схема Σ0 называетсяподсхемой схемы Σ, еслиV Σ0 ⊆ V (Σ) ,E Σ0 ⊆ E (Σ)14Глава 4. Эквивалентные преобразования управляющих системи любая вершина v, v ∈ V (Σ0 ), которая либо относится кмножеству входов (выходов) Σ, либо служит конечной (соответственно начальной) вершиной некоторого ребра из E(Σ)\E(Σ0 ), является входом (соответственно выходом) Σ0 .Будем считать, что для схем из U, как и для формул,имеет место принцип эквивалентной замены, то есть замеb 0 схемы Σ эквивалентной ей схемой Σb 00 мыняя подсхему Σeполучаем схему Σ, которая эквивалентна схеме Σ.
При этомвсе введенные в §1 для случая эквивалентных преобразований формул понятия (однократная и кратная выводимость,полнота системы тождеств и др.), а также связанные с ними обозначения переносятся на случай ЭП схем из U безизменений. Заметим, что вопрос о существовании конечнойполной системы тождеств (КПСТ) является одним из основных вопросов, связанных с изучением ЭП схем из заданногокласса U.Рассмотрим эти вопросы на примере ЭП СФЭ. Мы будемиспользовать все введенные выше общие понятия и определения, касающиеся ЭП схем, считая подстановкой СФЭ переименование (с возможным отождествлением) ее входныхБП и переименование (с возможным дублированием и снятием1 ) ее выходных БП.Напомним, что формулы представляют собой частныйслучай СФЭ, и для определенности будем считать, что любая формула F из UΦБ является формулой-словом (см.
§2), асоответствующую ей формулу-граф, т. е. квазидерево (см. ??),будем обозначать через F. При этом тождеству t : F0 = F00 ,где F0 и F00 —формулы из UΦБ , будет соответствовать тождество t : F0 ∼ F00 , где F0 и F00 — соответствующие F0 и F00схемы из UCБ , являющееся «схемным» аналогом тождества t.Множество СФЭ вида F, где F ∈ F ⊆ UΦБ , будем обозначать1Под дублированием (снятием) выхода zi СФЭ понимается нанесение на вершину с пометкой zi еще одной выходной БП (соответственноудаление с неё пометки zi )§2.