Об отношении совместимости в исчислении Ламбека и в его варианте с операциями замещения (1104173), страница 16
Текст из файла (страница 16)
Çäåñü p1 , p2 , p3 ïðèìèòèâíûå òèïû ñ s(p1 ) = s(p2 ) =s(p3 ) = 1:a : (qs \(p1 /p3 )) · q1 , (q1 \(p1 /p3 )) · qsb : (q1 \(J \ p2 )) · q1 , (q1 \(J \ p2 )) · q2b : (q1 \(J \(p1 ↓1 p2 ))) · q1 , (q1 \(J \(p1 ↓1 p2 ))) · q2c : (q2 \(p2 \ p3 )) · q2 .976.5Äîêàçàòåëüñòâî êîððåêòíîñòè êîíñòðóêöèè äàííîì ðàçäåëå ìû äîêàæåì, ÷òî ïðåäëîæåííûé íàìè àëãîðèòì äåéñòâèòåëüíî ñòðîèò ãðàììàòèêó äëÿ ÿçûêà L ∩ LR . Ìîæíî ñ÷èòàòü, ÷òîLR = L(M ), ãäå M = h{q1 , . . . , qn }, Σ, ∆, q1 , {qn }i.  äàëüíåéøåì ìûáóäåì îáîçíà÷àòü Q = {q1 , . . .
, qn }. Îáîçíà÷èì ÷åðåç T ìíîæåñòâî âñåõòèïîâ èñ÷èñëåíèÿ DL, íå ñîäåðæàùèõ ïðèìèòèâíûõ òèïîâ èç ìíîæåñòâàQ. Äëÿ êàæäîãî òèïà T ∈ T îáîçíà÷èì ÷åðåç Ti,j òèï (qi \ T ) · qj . Òàêæåáóäåì îáîçíà÷àòü Ti,0 = qi \ T, T0,0 = T . Ïî ïîñòðîåíèþ ìîæíî ïåðåîáîçíà÷èòü H 0 = H1,n , à òàêæå B0 = {ha, Ai,j i | a B A, (hqi , ai → qj ) ∈ ∆}.Îáîçíà÷èì T 0 = T ∪ {Ti,j | T ∈ T , 1 6 i 6 n, 0 6 j 6 n} ∪ {qi |1 6 i 6 n}.
Çàìåòèì, ÷òî ìíîæåñòâî T 0 çàìêíóòî îòíîñèòåëüíî ïîäòèïîâ. Îáîçíà÷èì ÷åðåç O(T 0 ) ìíîæåñòâî êîíôèãóðàöèé, â êîòîðûõ ðàçðåøåíû òîëüêî òèïû èç ìíîæåñòâà T 0 . T 0 -ñåêâåíöèÿìè áóäåì íàçûâàòüñåêâåíöèè èñ÷èñëåíèÿ DL, èìåþùèå âèä Γ → A, ãäå Γ ∈ O(T 0 ), A ∈ T 0 .Èç ñâîéñòâà ïîäôîðìóëüíîñòè âûòåêàåò ñëåäóþùàÿ ëåììà:Ëåììà 6.3. âûâîäå T 0 -ñåêâåíöèè ó÷àñòâóþò òîëüêî T 0 -ñåêâåíöèè.Ïîëîæèì Q = Q ∪ {qi | qi ∈ Q}, ãäå q i íîâûå ïðèìèòèâíûåòèïû, è îáîçíà÷èì Θi = qi , Θi = q i , 1 6 i 6 n, Θ0 = Θ0 = Λ.
Äëÿêàæäîé àòîìàðíîé êîíôèãóðàöèè Γ, ïðèíàäëåæàùåé ìíîæåñòâó O(T 0 ),îïðåäåëèì å¼ q -îáðàç (Γ)q :1. (Λ)q = ([])q = ε,2. (qi )q = qi , åñëè qi ∈ Q,3. (Ti,j )q = Θi Θj , åñëè s(Ti,j ) = 0,4. (Ti,j {Γ1 ; . . . ; Γr })q = Θi (Γ1 )q . . . (Γr )q Θj .q -îáðàç (Γ)q êîíôèãóðàöèè Γ ðàâåí êîíêàòåíàöèè q -îáðàçîâ âõîäÿùèõ â íå¼ àòîìàðíûõ êîíôèãóðàöèé. Ïðîäîëæèì îïðåäåëåíèå q -îáðàçàíà T 0 -ñåêâåíöèè, ïîëîæèâ (Γ → Ti,j )q = Θi (Γ)q Θj , (Γ → qi )q = (Γ)q Θi .Ïðèìåð 6.11.Ïóñòü Q = {q1 , q2 }, p1 , p2 ∈/ Q, s(p1 ) = 1, s(p2 ) = 0, òîãäà(((q2 \(p1 ↑1 p2 ))·q1 ){q1(q2 \ p1 )}q2 )q = q 2 q1 q 2 q1 q2 , (p1 {[]} p1 {p2 ·q2 } → q1 )q =98q2 q 1 .Íåôîðìàëüíî, q -îáðàç êîíôèãóðàöèè ñîäåðæèò âñå âõîæäåíèÿýëåìåíòîâ ìíîæåñòâà Q â äàííóþ êîíôèãóðàöèþ â íåêîòîðîì åñòåñòâåííîì ïîðÿäêå ñ óêàçàíèåì èõ ïîëÿðíîñòè.Îïðåäåëåíèå 6.9.Êîíôèãóðàöèÿ Π íàçûâàåòñÿ ìàêñèìàëüíîé ïîä-êîíôèãóðàöèåé êîíôèãóðàöèè Γ, åñëè Γ ïðåäñòàâèìà â âèäå Φ0 [A{∆1 ;.
. . ; ∆j−1 ; Π; ∆j+1 ; . . . ; ∆s(A) }] äëÿ íåêîòîðûõ êîíòåêñòà Φ0 , òèïà A è êîíôèãóðàöèé ∆1 , . . . , ∆s(A) .Ïðèìåð 6.12.Ïóñòü s(p0 ) = s(p1 ) = 1, s(p2 ) = s(p3 ) = 0, òîãäàâ êîíôèãóðàöèè p0 {p1 {p2 }(p2 /p3 )}p1 {[]} ìàêñèìàëüíûìè ÿâëÿþòñÿ ïîäêîíôèãóðàöèè p2 , p1 {p2 }(p2 /p3 ) è [].Ïîíÿòèå ïðàâèëüíîé ñêîáî÷íîé ïîñëåäîâàòåëüíîñòè ïðèíàäëåæèòìàòåìàòè÷åñêîìó ôîëüêëîðó.
Ïóñòü ôèêñèðîâàíû íåêîòîðîå íàòóðàëüíîå ÷èñëî n, n áóêâ b1 , . . . , bn , êîòîðûå áóäåì íàçûâàòü îòêðûâàþ-ùèìè ñêîáêàìè, à òàêæå n ñîîòâåòñòâóþùèõ èì çàêðûâàþùèõ ñêîáîêb1 , . . . , bn . Îáîçíà÷èì B = {b1 , b1 , . . . , bn , bn }.Îïðåäåëåíèå6.10.Ïðàâèëüíîé ñêîáî÷íîé ïîñëåäîâàòåëüíîñòüþ(ÏÑÏ ) ðàíãà n íàçûâàåòñÿ âñÿêîå ñëîâî w ∈ B ∗ , êîòîðîå ìîæåò áûòüñîêðàùåíî äî ïóñòîãî ïîñëåäîâàòåëüíûì âû÷¼ðêèâàíèåì ïîäñëîâ âèäàbi bi , ãäå i 6 n.Ïðèìåð 6.13.b1 b1 b1 b2 b2 b1 b3 b2 b2 b3 ÿâëÿåòñÿ ÏÑÏ.
Ðàçáèåíèå íà ïàðûñîîòâåòñòâóþùèõ ñêîáîê èçîáðàæåíî íà ðèñóíêå.b1 b1 b1 b2 b2 b1 b3 b2 b2 b3Ìíîæåñòâî ÏÑÏ ðàíãà n çàäà¼òñÿ êîíòåêñòíî-ñâîáîäíîé ãðàììàòèêîé ñî ñòàðòîâûì ñèìâîëîì S è ïðàâèëàìè S → ε, S → bi Sbi S, 1 6i 6 n.  îäíó ïàðó ïðè ýòîì ïîïàäàþò îòêðûâàþùàÿ è çàêðûâàþùàÿ99ñêîáêè, ââåä¼ííûå â îäíîì è òîì æå ïðàâèëå.
Ñëåäóþùàÿ ëåììà ñëåäóåòèç îïðåäåëåíèÿ ÏÑÏ.Ëåììà 6.4.Âî âñÿêîì ïðåôèêñå ÏÑÏ ÷èñëî îòêðûâàþùèõ ñêîáîê íåìåíüøå ÷èñëà çàêðûâàþùèõ.Ïðèâåä¼ííûå íèæå óòâåðæäåíèÿ î ñâîéñòâàõ ÏÑÏ ïðèíàäëåæàòìàòåìàòè÷åñêîìó ôîëüêëîðó. Èõ äîêàçàòåëüñòâî âûòåêàåò èç îïðåäåëåíèÿ ÏÑÏ, ëåììû 6.4 è ñâîéñòâ ãðàììàòèêè, çàäàþùåé ìíîæåñòâî ÏÑÏðàíãà n.Ëåììà 6.5.1. Åñëè u è v ÿâëÿþòñÿ ÏÑÏ, òî uv òàêæå ÿâëÿåòñÿ ÏÑÏ.2. Åñëè u è uv ÿâëÿþòñÿ ÏÑÏ, òî v òàêæå ÿâëÿåòñÿ ÏÑÏ.Ëåììà 6.6.1. Åñëè ñëîâî u0 u1 . .
. ur , à òàêæå ñëîâà v1 , . . . , vr ÿâëÿåòñÿ ÏÑÏ, òîñëîâî u0 v1 u1 v2 . . . vr ur òàêæå áóäåò ÏÑÏ.2. Åñëè ñëîâà u1 vu2 è v ÿâëÿþòñÿ ÏÑÏ, òî ñëîâî u1 u2 òàêæå áóäåòÏÑÏ.3. Åñëè ñëîâà u0 vu1 , v è v 0 ÿâëÿþòñÿ ÏÑÏ, òî ñëîâî u0 = u0 v 0 u1 òàêæå áóäåò ÏÑÏ.Îïðåäåëåíèå 6.11.T 0 -êîíôèãóðàöèþ Γ áóäåì íàçûâàòü q -ïðàâèëüíîé,åñëè å¼ q -îáðàç ÿâëÿåòñÿ ÏÑÏ.Ëåììà 6.7.1. Åñëè Γ è ∆ q -ïðàâèëüíûå êîíôèãóðàöèè, òî Γ∆ òàêæå q ïðàâèëüíàÿ êîíôèãóðàöèÿ.2. Åñëè Γ è ∆ q -ïðàâèëüíûå êîíôèãóðàöèè, òî äëÿ ëþáîãî j 6 s(Γ)âåðíî, ÷òî Γ|j ∆ òàêæå q -ïðàâèëüíàÿ êîíôèãóðàöèÿ.3.
Åñëè Γ; Φ1 , . . . , Φs q -ïðàâèëüíûå êîíôèãóðàöèè, ïðè÷¼ì s(Γ) = s,òî Γ ⊗ {Φ1 ; . . . ; Φs } òàêæå q -ïðàâèëüíàÿ êîíôèãóðàöèÿ.1004. Åñëè Φ[Π], Π è Π0 q -ïðàâèëüíûå êîíôèãóðàöèè, òî Φ[Π0 ] òàêæåq -ïðàâèëüíàÿ êîíôèãóðàöèÿ.5. Åñëè Π, Π0 q -ïðàâèëüíûå êîíôèãóðàöèè, Γ = Φ[Π], à (Γ → C)qÿâëÿåòñÿ ÏÑÏ, òî ñëîâî (Γ0 → C)q , ãäå Γ0 = Φ[Π0 ], òàêæå áóäåòÏÑÏ.6. Åñëè (Π)q = Λ, Π0 , Φ1 , . . . , Φs q -ïðàâèëüíûå êîíôèãóðàöèè, Γ =ΦhΠi = Φ0 [Π ⊗ {Φ1 , .
. . , Φs }], à (Γ → C)q ÿâëÿåòñÿ ÏÑÏ, òî ñëîâî(Γ0 → C)q , ãäå Γ0 = ΦhΠ0 i = Φ0 [Π0 ⊗ {Φ1 , . . . , Φs }], òàêæå áóäåòÏÑÏ.Äîêàçàòåëüñòâî. Ïåðâûé ïóíêò ñðàçó âûòåêàåò èç ëåììû 6.5 è îïðåäåëåíèÿ q -îáðàçà, âòîðîé è òðåòèé äîêàçûâàþòñÿ èíäóêöèåé ïî ïîñòðîåíèþ êîíôèãóðàöèè Γ ñ èñïîëüçîâàíèåì ëåììû 6.6. ×åòâ¼ðòûé è ïÿòûéïóíêòû ñëåäóþò èç ïóíêòà 3 ëåììû 6.6. Äîêàæåì øåñòîé ïóíêò.
Ïîïóíêòó 3 íàñòîÿùåé ëåììû Π ⊗ {Φ1 , . . . , Φs } è Π0 ⊗ {Φ1 , . . . , Φs } áóäóòq -ïðàâèëüíûìè êîíôèãóðàöèÿìè, ïîñëå ÷åãî íóæíî ïðèìåíÿòü ïóíêò 5äàííîé ëåììû.Îïðåäåëåíèå 6.12.Êîíôèãóðàöèþ Γ áóäåì íàçûâàòü âíóòðåííå q -ïðàâèëüíîé, åñëè âñÿêàÿ å¼ ìàêñèìàëüíàÿ ïîäêîíôèãóðàöèÿ ÿâëÿåòñÿq -ïðàâèëüíîé.Ëåììà 6.8.1. Åñëè Γ è ∆ âíóòðåííå q -ïðàâèëüíûå êîíôèãóðàöèè, òî Γ∆ òàêæå áóäåò âíóòðåííå q -ïðàâèëüíîé êîíôèãóðàöèåé.2. Åñëè Γ è ∆ q -ïðàâèëüíûå êîíôèãóðàöèè, òî äëÿ ëþáîãî j 6 s(Γ)âåðíî, ÷òî Γ|j ∆ òàêæå áóäåò âíóòðåííå q -ïðàâèëüíîé êîíôèãóðàöèåé.3. Åñëè Γ âíóòðåííå q -ïðàâèëüíàÿ êîíôèãóðàöèÿ, à Φ1 , .
. . , Φs q -ïðàâèëüíûå êîíôèãóðàöèè, ïðè÷¼ì s(Γ) = s, òî Γ ⊗ {Φ1 ; . . . ; Φs }òàêæå áóäåò âíóòðåííå q -ïðàâèëüíîé êîíôèãóðàöèåé.4. Åñëè Φ[Π] âíóòðåííå q -ïðàâèëüíàÿ êîíôèãóðàöèÿ, à Π è Π0 101q -ïðàâèëüíûå êîíôèãóðàöèè, òî Φ[Π0 ] òàêæå áóäåò âíóòðåííå q ïðàâèëüíîé êîíôèãóðàöèåé.5. Åñëè ΦhΠi = Φ0 [Π ⊗ {Φ1 ; . . . ; Φs }], âíóòðåííå q -ïðàâèëüíàÿ êîíôèãóðàöèÿ, Φ1 , . . . , Φs q -ïðàâèëüíûå êîíôèãóðàöèè, (Π)q = Λ,à Π0 ÿâëÿåòñÿ q -ïðàâèëüíîé êîíôèãóðàöèåé ñîðòà s, òî ΦhΠ0 i =Φ0 [Π0 ⊗ {Φ1 ; . .
. ; Φs }] òàêæå áóäåò âíóòðåííå q -ïðàâèëüíîé êîíôèãóðàöèåé.Äîêàçàòåëüñòâî.1. Âñÿêàÿ ìàêñèìàëüíàÿ ïîäêîíôèãóðàöèÿ â Γ∆ ÿâëÿåòñÿ ìàêñèìàëüíîé ïîäêîíôèãóðàöèåé â Γ ëèáî ∆.2. Âñÿêàÿ ìàêñèìàëüíàÿ ïîäêîíôèãóðàöèÿ â Γ|j ∆ ëèáî ÿâëÿåòñÿ ìàêñèìàëüíîé ïîäêîíôèãóðàöèåé â Γ èëè ∆, ëèáî ïîëó÷åíà èç íåêîòîðîé ìàêñèìàëüíîé ïîäêîíôèãóðàöèè â Γ çàìåíîé ðàçäåëèòåëÿ íà ∆. ïîñëåäíåì ñëó÷àå íóæíî ïðèìåíèòü ïóíêò 2 ëåììû 6.7.3. Äîêàçàòåëüñòâî àíàëîãè÷íî ïðåäûäóùåìó ïóíêòó.4. Âñÿêàÿ ìàêñèìàëüíàÿ ïîäêîíôèãóðàöèÿ â Φ[Π0 ] ëèáî áûëà òàêîâîéâ Φ[Π], ëèáî ïîëó÷åíà èç íå¼ çàìåíîé Π íà Π0 . Ïîñëå ýòîãî óòâåðæäåíèå ëåììû ñëåäóåò èç ïóíêòà 4 ëåììû 6.7.5.
Íåòðóäíî âèäåòü, ÷òî îáå êîíôèãóðàöèè Π ⊗ {Φ1 ; . . . ; Φs } è Π0 ⊗{Φ1 ; . . . ; Φs } áóäóò âíóòðåííå q -ïðàâèëüíûìè. Ïîñëå ýòîãî óòâåðæäåíèå âûòåêàåò èç ïðåäûäóùåãî ïóíêòà.Ëåììà 6.9.Âñÿêàÿ âûâîäèìàÿ â èñ÷èñëåíèè DL T 0 -ñåêâåíöèÿ Γ → Aóäîâëåòâîðÿåò ñëåäóþùèì óñëîâèÿì:1. (Γ → A)q ÿâëÿåòñÿ ÏÑÏ.2. Γ ÿâëÿåòñÿ âíóòðåííå q -ïðàâèëüíîé êîíôèãóðàöèåé.Äîêàçàòåëüñòâî. Èíäóêöèÿ ïî âûâîäó â èñ÷èñëåíèè DL.
Ñëó÷àé àêñèîìû, à òàêæå ïðàâèë (→ I) è (→ J) î÷åâèäåí. Áàçà èíäóêöèè äîêàçàíà,íà øàãå èíäóêöèè ïðîâåä¼ì ðàçáîð ñëó÷àåâ â çàâèñèìîñòè îò ïîñëåäíåãîïðèìåíÿâøåãîñÿ ïðàâèëà.102BΠ → A, òîãäàΠ → B \Aâîçìîæíû äâà ñëó÷àÿ: B ∈ T è B = qi . Ïî îïðåäåëåíèþ ìíîæåñòâà T 0Ïóñòü ïîñëåäíèì ïðàâèëîì áûëî (→ \) â âèäåèìååì A ∈ T , ïîýòîìó â ïåðâîì ñëó÷àå (Π → B \ A)q = (Π)q = (BΠ →A)q . Âî âòîðîì ñëó÷àå èìååì (Π → B \ A)q = qi (Π)q = (BΠ → A)q ,ïîñëå ÷åãî ìîæíî ïðèìåíèòü ïðåäïîëîæåíèå èíäóêöèè äëÿ äîêàçàòåëüñòâà ïåðâîãî óòâåðæäåíèÿ ëåììû. Âòîðîå óòâåðæäåíèå ëåììû íåïîñðåäñòâåííî ñëåäóåò èç ïðåäïîëîæåíèÿ èíäóêöèè è òîãî, ÷òî àíòåöåäåíò çàêëþ÷åíèÿ ÿâëÿåòñÿ ïîäêîíôèãóðàöèåé àíòåöåäåíòà ïîñûëêè.
Ïðàâèëî(→ /) ðàçáèðàåòñÿ àíàëîãè÷íî.Γ→A ∆→B,Γ∆ → A · Bòîãäà âîçìîæíû äâà ñëó÷àÿ: B ∈ T è B = qj .  ïåðâîì ñëó÷àå ïî îïðåäåÏóñòü ïîñëåäíèì ïðàâèëîì áûëî (→ ·) â âèäåëåíèþ ìíîæåñòâà T 0 ïîëó÷àåì, ÷òî òàêæå A ∈ T , ÷òî ïðèâîäèò ê ðàâåíñòâàì (Γ∆ → A · B)q = (Γ∆)q = (Γ)q (∆)q , âî âòîðîì ñëó÷àå ïî îïðåäåëåíèþ ìíîæåñòâà T 0 èìååì A = qi \ C äëÿ íåêîòîðîãî òèïà C ∈ T . Îòñþäàñëåäóåò (Γ∆ → A·B)q = qi (Γ∆)q q j = qi (Γ)q (∆)q q j = (Γ → A)q (∆ → qj )q . îáîèõ ñëó÷àÿõ q -îáðàç çàêëþ÷åíèÿ ÿâëÿåòñÿ êîíêàòåíàöèåé q -îáðàçîâïîñûëîê, ïîñëå ÷åãî ïåðâûé ïóíêò ëåììû ñëåäóåò èç ïðåäïîëîæåíèÿ èíäóêöèè è ïóíêòà 1 ëåììû 6.7. Âòîðîé ïóíêò ñëåäóåò èç ïóíêòà 1 ëåììû6.8.Ïóñòü ïîñëåäíèì ïðàâèëîì â âûâîäå áûëî (→ ) â ôîðìåΓ→A ∆→B.
Òîãäà A j B ∈ T , ïîýòîìó (Γ|j ∆ → A j B)q =Γ|j ∆ → A j B(Γ|j ∆)q , îòêóäà ïî ïóíêòó 2 ëåììû 6.7 è ïðåäïîëîæåíèþ èíäóêöèè ñëåäóåò, ÷òî ïåðâûé ïóíêò ëåììû âûïîëíÿåòñÿ. Âòîðîé ïóíêò ñëåäóåò èçïóíêòà 2 ëåììû 6.8.Ïóñòü ïîñëåäíèì ïðàâèëîì â âûâîäå áûëî (→ ↓) â ôîðìåA|j Π → B, òîãäà ïî îïðåäåëåíèþ ìíîæåñòâà T 0 èìååì, ÷òî A ↓j B ∈ T ,Π → A ↓j Bòî åñòü (Π → A ↓j B)q = (Π)q = (A|j Π → B)q è ïåðâîå óòâåðæäåíèåëåììû ñëåäóåò èç ïðåäïîëîæåíèÿ èíäóêöèè. Âòîðîå óòâåðæäåíèå òàêæå âûïîëíÿåòñÿ, òàê êàê âñÿêàÿ ìàêñèìàëüíàÿ ïîäêîíôèãóðàöèÿ â Πáûëà ìàêñèìàëüíîé ïîäêîíôèãóðàöèåé â A|j Π.103Î÷åâèäíî, ÷òî ïðèìåíåíèå ïðàâèë (I →) è (J →) íå âëèÿåòíà q -îáðàç ñåêâåíöèè è ìàêñèìàëüíûõ ïîäêîíôèãóðàöèé àíòåöåäåíòà.Íåòðóäíî ïðîâåðèòü, ÷òî àíàëîãè÷íîå óòâåðæäåíèå âåðíî è äëÿ ïðàâèë(· →), ( →).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
