оки4 (1155747), страница 3
Текст из файла (страница 3)
Преобразования на основе тождествx1x2•1x1••2&x2••¬ •∼1¬ z•115x1x2••• ¬• ¬&2•z1 ∨•yz1a)•{∨x1∼ z•1b)ΠKРис. 2.1: тождества tM& и t1,&через F, а систему тождеств вида t, где t ∈ τ , а τ — систематождеств для UΦБ , — через τ . Так, на рис. 2.1a и 2.1b привеΠKдены тождества tM& и t1,& , являющиеся схемными аналогамиПKвведенных выше формульных тождеств tM& и t1,& .На рис. 2.2a и 2.2b показаны тождество ветвления tBEiи тождество снятия tCEi для функционального элемента Ei , i ∈[1, b], соответственно, а на рис. 2.2c — тождество снятиявхода tCвх .
Заметим, что применение тождества снятия равносильно выполнению операции удаления висячей вершинысоответствующего типа (см. §3). Заметим также, что тожCCдества tBEi , tEi , tвх не являются аналогами формульных тождеств и положим bτБB = tBEi i=1 , bCτБC = tCEi i=1 ∪ tвх .Очевидно, что с помощью этих тождеств можно избавитьсяот всех висячих вершин и всех внутренних ветвлений, имеющихся в СФЭ. Следовательно, для любой СФЭ Σ, Σ ∈ UCБ,существует ЭП вида Σ |⇒ F, где F — формула (система{τ C ,τ B }формул) изUΦБ.16Глава 4.
Эквивалентные преобразования управляющих системx1 . . . xki••ki1ϕi •x1•∼...1ϕi • kiz1z1 , z2xki•ki1 • ϕiz2a)x1 . . . xki••∼x1 . . . xk i••x1•∼ ∅ϕi •b)c)Рис. 2.2: тождества ветвления, снятия ФЭ и снятия входаb — однократное ЭП для формул изПусть, далее, F 7→ FtUΦБ , где тождество t имеет видt : F0 (x1 , . . . , xn ) = F00 (x1 , .
. . , xn ) ,b получается из формулы F заменой подфора формула Fмулы F0 (F1 , . . . , Fn ) формулой F00 (F1 , . . . , Fn ). Сопоставимэтому ЭП «моделирующее» его однократное ЭП СФЭ виb (см. рис. 2.3). Заметим, что в том случае, когдада F 7→ Σtформулы F0 и F00 являются бесповторными формулами, аb совпадаБП x1 , . . . , xn — их существенными БП, СФЭ Σ00ет с СФЭ F . В остальных случаях из подформулы видаF0 (F1 , . .
. , Fn ) формулы F необходимо с помощью тождествτБB сформировать сначала подсхему F0 (F1 , . . . , Fn ), а затемb могут появитьсяприменить тождество t. При этом в СФЭ Σ§2. Преобразования на основе тождествF1FnF1...F017→−~Fn...tF00F~bΣРис. 2.3: моделирование ЭП формул с помощью ЭП СФЭвисячие вершины или внутренние «ветвления», и тогда дляb необходимо провести ЭП вида Σbb кFb |⇒ F.перехода от Σ{τ C ,τ B }b где F, Fb ∈ UΦ ,Следовательно, для любого ЭП вида F |⇒ F,Бτсуществует моделирующее его ЭП видаFbF.|⇒{B ,τ Cτ ,τББ}На рис. 2.4 показано ЭП СФЭ из UC , которое моделируетЭП (1.1) для формул из UΦ :x1 (x2 x3 ∨ x2 ∨ x3 ) 7→ x1 (x2 x3 ∨ x2 · x3 ) 7→ x1 .tM&tΠK1,&Из описанного выше способа «моделирования» ЭП формул с помощью ЭП СФЭ, а также способа перехода от формул к СФЭ и обратно на основе ЭП с помощью тождествτБB , τБC вытекает справедливость следующего утверждения.Теорема 2.1.
Если τ — конечная полная систематожCBΦдеств для ЭП формул из UБ , то τ , τ , τ— конечнаяполная система тождеств для ЭП СФЭ из UCБ. осн B C Следствие. Система тождеств τ , τ , τ— КПСТдля ЭП СФЭ из UC .18Глава 4. Эквивалентные преобразования управляющих системx1•x2x3•x1•¬ •#& •{••¬•#∨ −→x2&& •u•) &•→¬ −tB&•{∨&•∨•z1••tM&•{#x1x3•z1x2x3••&•{#• ¬ −−→−→tB&tΠK1,&•{&x1 x2••z1x3•&•}!⇒τCx1•z1∨•z1Рис. 2.4: пример моделирования ЭП формул с помощью ЭПСФЭ§2. Преобразования на основе тождеств19Рассмотрим далее вопросы структурного моделированияформул в различных базисах.
Пусть помимо базиса Б =конечный полныйбазис= {ϕi }bi=1 у нас имеется другой 0Б0 = {ϕ0i }bi=1 , и пусть формула Φ0i x1 , . . . , xki0из UΦ, гдеБ0ki0 > ki , реализует ФАЛ ϕi , i = 1, . . . , b. Заметим, что вслучае ki0 > ki БП xki +1 , . . . , xki0 являются фиктивными БПформулы Φ0i . ПоложимΦ0 = Φ01 , . . . , Φ0b ,Π0 = Π01 , . .
. , Π0b ,где Π0i — тождество вида ϕi = Φ0i , i = 1, . . . , b, и формулы изΦ0 (тождества из Π0 ) будем называть формулами (соответственно тождествами) перехода от базиса Б к базису Б0 .0Для формулы F, F ∈ UΦБ , обозначим через Π (F)0формулу над базисом Б , которая получается из F заменой каждой ее подформулывида ϕi (F1 , . . .
, Fki ) формулойΦ0i F1 , . . . , Fki , xki +1 , . . . , xki0 , то есть является результатомподстановки формулы Fj вместо БП xj в формулу Φ0i длявсех j, j = 1, . . . , ki . Переход от формулы F к формуле Π0 (F)будем называть структурным моделированием формулы Fв базисе Б0 на основе формул перехода Φ0 или, иначе, наоснове тождеств перехода Π0 . Заметим, что этот переходявляется специальным ЭП видаF |⇒ Π0 (F)Π0для формул над базисом Б ∪ Б0 . Отсюда следует, в частности, что в результате указанного структурного моделирования обеих частей тождества t, являющихся формулами из0ΦUΦБ , получается тождество t для формул из UБ0 , которое0мы будем обозначать через Π (t). Множество формул вида0Π0 (F), где F ∈ F ⊆ UΦБ , будем обозначать через Π (F), а0множество тождеств вида Π (t), где t ∈ τ — тождество над0UΦБ , — через Π (τ ).20Глава 4.
Эквивалентные преобразования управляющих системРассмотрим теперь вопросы моделирования ЭП формул в базисе Б с помощью ЭП формул базиса Б0 . ПустьΦ0 = (Φ01 , . . . , Φ0b ) — система формул перехода от базиса Б кбазису Б0 , а Π0 = (Π01 , . . . , Π0b ) — система тождеств перехода,связанная с Φ0 . Заметим, что любое ЭП для формул из UΦБ,имеющее видbF |⇒ F,(2.1)τможет быть «промоделировано» с помощью ЭП для формулвидаиз UΦБ0b 0,F0 |⇒ F(2.2)τ0b 0 = Π0 (F)b и τ 0 = Π0 (τ ). Действительно,где F0 = Π0 (F), Fпусть ЭП (2.1) является однократным ЭП на основе тождества t, t ∈ τ , которое имеет видt : A (x1 , . . .
, xq ) = B (x1 , . . . , xq ) ,b получается в результате замены подфори пусть формула Fмулы A (F1 , . . . , Fq ) формулы F формулой B (F1 , . . . , Fq ). Тогда тождество t0 = Π0 (t) имеет видt0 : A0 (x1 , . . . , x1 ) = B (x1 , . . . , xq ) ,b 0 может бытьгде A0 = Π0 (A) и B0 = Π0 (B), а формула Fполучена из формулыF0 в результате замены ее подформу000лы A F1 , . . . , Fq , где Fj0 = Π0 (Fj ) для всех j, j ∈ [1, q],формулой B0 F10 , . .
. , Fq0 . Моделирование кратного ЭП вида (2.1) с помощью кратного ЭП вида (2.2) осуществляетсяпутем последовательного моделирования однократных ЭП,составляющих ЭП (2.1).Описанное выше моделирование позволяет выполнятьЭП для тех эквивалентных формул из UΦ, которые приБ0,тоестьявляются«моделями»надлежат множеству Π0 UΦБ§2. Преобразования на основе тождеств210формул из UΦБ , на основе системы тождеств Π (τ ), являющихся «моделями» тождеств из τ . Для того чтобы проводить ЭП для произвольных формул из UΦс использованиБ0ем системы тождеств Π0 (τ ), выберем какую-либо системуформул перехода Φ = (Φ1 , . .
. , Φb0 ) от базиса Б0 к базисуБ и рассмотрим связанную с ней систему тождеств перехода Π = (Π1 , . . . , Πb0 ). Пусть Π̌ — система тождеств видаΠ̌ = Π0 (Π) для ЭП формул из UΦ, которая получается в реБ0зультате структурного моделирования правых частей тождеств из Π на основе системы тождеств Π0 . Для произволь, положимной формулы F0 , F0 ∈ UΦБ0Π̌ F0 = Π0 (Π (F))и заметим, чтоF0 |⇒ F̌0 = Π̌ F0 ,F̌0 ∈ Π0 UΦБ .Π̌В силу сказанного выше, отсюда вытекает справедливостьследующего утверждения.Теорема 2.2 (теорема перехода). Пусть τ — КПСТ для0ЭП формул из UΦБ , а Π и Π — системы тождеств дляперехода от базиса Б к базису Б0 и от базиса Б0 к базису Бсоответственно. Тогда система тождеств {Π0 (τ ) , Π0 (Π)}является КПСТ для ЭП формул из UΦБ.Следствие.
Из системы тождеств τ осн для ЭП формулиз UΦ (см. §3) указанным в теореме способом можно получить КПСТ для ЭП формул в любом базисе Б.Аналогичным образом на основе теоремы 2.1 решаютсявопросы построения КПСТ для ЭП СФЭ в произвольномбазисе.22Глава 4. Эквивалентные преобразования управляющих систем§3Эквивалентные преобразования контактныхсхем. Основные тождества, выводвспомогательных и обобщенных тождествРассмотрим вопросы ЭП для КС из UK с неразделенными (бесповторными) полюсами.
В соответствии с ?? эквивалентность КС Σ0 = Σ0 (x1 , . . . , xn ; a1 , . . . , am ) и Σ00 =Σ00 (x1 , . . . , xn ; a1 , . . . , am ), то есть справедливость тождестваt : Σ0 ∼ Σ00 означает, что для любых i и j из отрезка [1, m]ФАЛ проводимости от ai к aj в КС Σ0 равна ФАЛ проводимости от ai к aj в КС Σ00 . На рис. 3.1a–3.1e и 3.1f приведены пары эквивалентных КС, образующие тождества t1 –t5 и(m)t6 , m = 1, 2, .
. ., соответственно, которые мы будем называть основными тождествами для ЭП КС.Определим подстановку для КС как переименование (свозможным отождествлением и инвертированием) БП, атакже переименование (с возможным отождествлением иснятием) полюсов. Заметим, что применяя одну и ту же подстановку к двум эквивалентным КС, мы получим эквивалентные КС. Действительно, для переименования БП и переименования без отождествления полюсов это очевидно, ав случае отождествления полюсов эквивалентность получаемых КС вытекает из того, что матрица достижимости КС,являющейся результатом отждествления, однозначно определяется матрицей достижимости исходной КС.
На рис. 3.2a(3.2b) показана подстановка bt4 тождества t4 (соответственbно t5 тождества t5 ), связанная с переименованием БП x2 вx1 (соответственно полюсов 1 = 3 в 1).Понятие подсхемы для КС из рассматриваемого классаопределяется аналогично §5 с учетом неразделенности полюсов. Это означает, что для подсхемы Σ0 КС Σ имеет место включение V (Σ0 ) ⊂ V (Σ) и E(Σ0 ) ∈ E(Σ), а полюсамиΣ0 являются все принадлежащие ей полюса КС Σи все те еевершины, которые инцидентны в Σ ребрам из E(Σ) \ E(Σ0 ),§3. Эквивалентные преобразования контактных схемa) t1 :•x1b) t2 :x1c) t3 :x2•1x1•1∼2x2d) t4 :1∼2x1e) t5 :1∼2x1∼ ∅∼2x211f)(m)t6:122x2•x1x2•x1•12x1x2∼2x13•xmx1•13x1231•Рис. 3.1: основные тождества для КС24Глава 4.
Эквивалентные преобразования управляющих системa) bt4 :x112∼x1b) bt5 :1x12∼11x1•x1x1•x12x12x1Рис. 3.2: подстановки для основных тождестви, возможно, некоторые другие вершины. При таком определении подсхемы для рассматриваемого класса КС будетвыполняться принцип эквивалентной замены.Рассмотрим примеры ЭП контактных схем с помощьюсистемы основных тождеств. На рис. 3.3a–3.3e приведенытождества t7 –t11 , которые мы будем называть вспомогательными.