Об отношении совместимости в исчислении Ламбека и в его варианте с операциями замещения (1104173), страница 5
Текст из файла (страница 5)
Âûâîäèìîñòü ñåêâåíöèè A → A0ïî ëåììå 1.2 ðàâíîñèëüíà âûâîäèìîñòè ñåêâåíöèè (B/C)C01 . . . C0n → B0 ,êîòîðàÿ ñëåäóåò ïî ïðàâèëó (/ →) èç âûâîäèìûõ ñåêâåíöèé B → B0 èC01 . . . C0n → C . Çàìåòèì, ÷òî l(A0 ) = l(B0 ) +nPl(C0i ) = l(B) + l(C) =i=1l(A), ÷òî è òðåáîâàëîñü. Êðîìå òîãî, hA0 i = h(. . . (B0 /C0n ) . . .)/C01 i =hB0 ihC0n i−1 . .
. hC01 i−1 = hB0 i(hC01 i . . . hC0n i)−1 = hBihCi−1 = hB/Ci =hAi. Ñëó÷àé A = C \ B ðàçáèðàåòñÿ àíàëîãè÷íî.2. Ðàçáåð¼ì òðè ñëó÷àÿ. Ïåðâûé ñëó÷àé A = B · C . Ïóñòü ìíîæåñòâà òèïîâ B01 , . . . , B0n1 è C01 , . . . , C0n2 âçÿòû èç ïóíêòà 2 ëåììû, ïðèìåí¼ííîé ê òèïàì B è C ñîîòâåòñòâåííî. Òîãäà ïîëîæèì n = n1 +n2 , Ai0 = B0i ïðè i 6 n1 è Ai0 = C0i−n1 ïðè i > n1 . Âûâîäèìîñòü ñåêâåí28öèè A10 . . . An0 → A ñëåäóåò ïî ïðàâèëó (→ ·) èç âûâîäèìîñòè ñåêâåíöèéA10 .
. . An0 1 → B è An0 1 +1 . . . An0 1 +n2 → C . Îñòàëüíûå óòâåðæäåíèÿ ëåììûòàêæå ëåãêî ïðîâåðÿþòñÿ.Ðàçáåð¼ì òåïåðü ñëó÷àé A = B/C . Ïóñòü òèïû B01 , . . . , B0n âçÿòûèç ïóíêòà 2 ëåììû, ïðèìåí¼ííîãî ê òèïó B , à òèï C0 èç ïóíêòà 1 ëåììû, ïðèìåí¼ííîãî ê òèïó C . Ïîëîæèì A10 = B01 , . . .
, An−1= B0n−1 , An0 =0B0n /C0 . Ïî ïðåäïîëîæåíèþ èíäóêöèè íè îäèí èç òèïîâ A10 , . . . , An−1íå0ñîäåðæèò ïîëîæèòåëüíûõ óìíîæåíèé, An0 = B0n /C0 òàêæå íå ñîäåðæèòïîëîæèòåëüíûõ âõîæäåíèé óìíîæåíèÿ, ò. ê. âñÿêîå òàêîå âõîæäåíèåäîëæíî ëèáî ïîëîæèòåëüíî âõîäèòü â B0n , ëèáî îòðèöàòåëüíî âõîäèòüâ C0 , ÷åãî íå ìîæåò áûòü ïî ïðåäïîëîæåíèþ èíäóêöèè. Âûâîäèìîñòüñåêâåíöèè A10 .
. . An0 → A0 äîêàçûâàåòñÿ ïðèâåä¼ííûì âûâîäîì:B01 . . . B0n−1 B0n → BC → C0B01 . . . B0n−1 (B0n /C0 )C → BB01 . . . B0n−1 (B0n /C0 ) → B/C(/ →)(→ /)Òàêæå âåðíî, ÷òî l(A10 ) + . . . + l(An0 )=l(B01 ) + . . . +l(B0n ) + l(C0 ) = l(B) + l(C) = l(A). Êðîìå òîãî, hA10 i . . . hAn0 i =hB01 i . . . hB0n−1 ihB0n ihC0 i−1 = hBihCi−1 = hAi, ÷òî è òðåáîâàëîñü.
Ñëó÷àéïðîòèâîïîëîæíîãî äåëåíèÿ ðàçáèðàåòñÿ àíàëîãè÷íî.Ðàññìîòðèì ïðîèçâîëüíóþ ïàðó ñîâìåñòèìûõ òèïîâ A è B è ïîñòðîèì äëÿ íèõ òèïû A0 , B0 áåç îòðèöàòåëüíûõ óìíîæåíèé, òàêèå ÷òîL ` A → A0 è L ` B → B0 , à òàêæå l(A0 ) = l(A) è l(B0 ) = l(B).Çàìåòèì, ÷òî âñÿêèé òèï C , ÿâëÿþùèéñÿ ñîâìåùàþùèì äëÿ òèïîâ A0 èB0 , òàêæå áóäåò ñîâìåùàþùèì äëÿ òèïîâ A è B . Ñëåäîâàòåëüíî, ÷òîáûîãðàíè÷èòü ñâåðõó âåëè÷èíó Mj (l1 , l2 ), äîñòàòî÷íî îöåíèòü ñâåðõó äëèíó ñîâìåùàþùåãî òèïà òîëüêî äëÿ ñîâìåñòèìûõ òèïîâ, íå ñîäåðæàùèõîòðèöàòåëüíûõ óìíîæåíèé.Íà ðèñóíêå 2.1 ïðèâåäåíà îáùàÿ ñõåìà ïîñòðîåíèÿ ñîâìåùàþùåãîòèïà C äëÿ çàäàííûõ ñîâìåñòèìûõ òèïîâ A è B . Òèïû A1 , A2 , B1 , B2 ñóùåñòâóþò íà îñíîâàíèè ëåììû 2.6 (ìû ïîëüçóåìñÿ òåì, ÷òî hAi = hA0 i29ABA0φ(hAi)A1{φ(JAK)##A3A2#{B2{èB0#B3B1{CuÐèñ. 2.1: Ñõåìà ïîñòðîåíèÿ ñîâìåùàþùåãî òèïàA{#)φ(hBi)Cäëÿ çàäàííûõ ñîâìåñòèìûõ òèïîâB.è hBi = hB0 i). Ïîñëå ýòîãî òèï A3 ïîëó÷àåòñÿ èç òèïîâ A1 , A2 è φ(hAi)ïîñëå ïðèìåíåíèÿ ëåììû 2.2, òèï B3 ñòðîèòñÿ àíàëîãè÷íûì îáðàçîì.
Òîãäà èñêîìûé òèï C ïîëó÷àåòñÿ èç òèïîâ A3 , B3 è òèïà φ(JAK) = φ(JBK)îïÿòü æå íà îñíîâàíèè ëåììû 2.2.  ñëåäóþùåì ðàçäåëå ìû ïðåäúÿâèì àëãîðèòì ïîñòðîåíèÿ òèïîâ A1 , B1 , A2 , B2 , ïîçâîëÿþùèé îöåíèòüèõ äëèíû, à çíà÷èò, è äëèíó òèïà C .Ïðèìåð 2.3.Ïóñòü A = p/(q \(r · (r \ q))), B = ((q · (q \ r))/p) \ r. ýòîì ñëó÷àå hAi = pq −1 rr−1 q, hBi = prq −1 qr, JAK = JBK = p,à çíà÷èò φ(hAi) = p · (q \ q/q) · r · (r \ r/r) · q, φ(hBi) = p · (r \ r/r) ·q · (q \ q/q) · r, φ(JAK) = φ(JBK) = p.
Ïîëîæèì A0 = (p/(r \ q))/(q \ r),B0 = (q \ r/p) \(q \ r), òîãäà ìîæíî âçÿòü A1 = A2 = A3 =(q/p) \((q/(r \ q))/(q \ r)), B1 = B3 = (q \ r/p) \(q \((r/(q \ r))/(r \ q))),B2 = (r/p) \((r/(q \ r))/(r \ q))). Ñëåäîâàòåëüíî, ñîâìåùàþùèé òèï ðàâåí C = (p/A3 ) \ p/(B3 \ p). Âûâîäèìîñòü òðåáóåìûõ ñåêâåíöèé ïðîâåðÿåòñÿ íåïîñðåäñòâåííî.2.3ÂÏîñòðîåíèå ñîâìåùàþùåãî òèïàäàííîìðàçäåëåìûïðåäúÿâèìàëãîðèòìïîñòðîåíèÿòèïîâA1 , A2 , A3 , B1 , B2 , B3 , C , îáîçíà÷åííûõ íà ðèñóíêå 2.1, à òàêæå îöåíèì èõäëèíû. Âíà÷àëå ïðèâåä¼ì ñîîòíîøåíèÿ íà äëèíû òèïîâ φ(hAi) è φ(JAK)30(÷åðåç |w| ìû îáîçíà÷àåì äëèíó ñëîâà w).Ëåììà 2.8.1.
Åñëè A ∈ Tp è JAK 6= ε, òî l(φ(hAi)) = l(φ(JAK)) + 2 (l(A) − |JAK|) 62 l(A) + |JAK| 6 3 l(A).2. Åñëè A ∈ Tp è JAK = ε, òî l(hAi) = 2 l(A).Äîêàçàòåëüñòâî.1. Ïóñòü w ∈ P ∗ , îáîçíà÷èì ÷åðåç |w|+ ÷èñëî áóêâ â ñëîâå w, ïðèíàäëåæàùèõ ìíîæåñòâó Pr, à ÷åðåç |w|− ÷èñëî áóêâ, ïðèíàäëåæàùèõ ìíîæåñòâó {p | p ∈ Pr}.
Íàïðèìåð, åñëè w = pqpqp, òî|w|+ = 3, |w|− = 2. Èç îïðåäåëåíèÿ îòîáðàæåíèÿ φ ñëåäóåò, ÷òîäëÿ âñÿêîãî w ∈ P ∗ âûïîëíÿåòñÿ ðàâåíñòâî l(φ(w)) = |w|+ + 3|w|− .Êðîìå òîãî, âåðíû ñîîòíîøåíèÿ |hAi|+ − |JAK|+ = |hAi|− − |JAK|− è|hAi| = l(A). Îáîçíà÷èì ÷åðåç δ ðàçíîñòü |hAi|+ − |JAK|+ , òîãäà δ =12 (|hAi|+− |JAK|) =l(A)−|JAK|.2+Îòñþäà ñëåäóåò ðàâåíñòâî l(φ(hAi)) =|hAi| + 3|hAi|− = |JAK| + 3|JAK|− + 4δ = l(φ(JAK)) + 2(l(A) − |JAK|).Î÷åâèäíî, l(φ(JAK)) 6 3|JAK| è |JAK| 6 l(A), îòêóäà ïîëó÷àåìl(φ(hAi)) = l(φ(JAK)) + 2(l(A) − |JAK|) 6 2l(A) + |JAK| 6 3l(A).2. Îáîçíà÷èì l+ (A) = |Occ+ (A)|, l− (A) = |Occ− (A)|, òîãäà ëåãêî ïîêàçàòü, ÷òî |hAi|+ = l+ (A) è |hAi|− = l− (A), îòêóäà ïîëó÷àåì ðàâåíñòâî l(φ(hAi)) = l+ (A) + 3l− (A).
Èç óñëîâèÿ JAK = 0 ñëåäóåò,÷òî |hAi|+ = |hAi|− , îòêóäà ëåãêî ïîëó÷àåòñÿ òðåáóåìîå ðàâåíñòâî.Ëåììà äîêàçàíà.Ñëåäóþùàÿ ëåììà ÿâëÿåòñÿ âñïîìîãàòåëüíîé â äàëüíåéøèõ ïîñòðîåíèÿõ.Ëåììà 2.9.Äëÿ ëþáîãî òèïà U ∈ Tp è ëþáîãî ñëîâà w ∈ P + , òàêîãî÷òî χ(w) = ε, ñóùåñòâóþò òàêèå òèïû U 0 , U 00 , ÷òî1. L ` U φ(w) → U 0 , L ` U → U 0 , ïðè ýòîì l(U 0 ) < l(U ) + 2 |w|.2. L ` φ(w)U → U 00 , L ` U → U 00 , ïðè ýòîì l(U 00 ) < l(U ) + 2 |w|.31Äîêàçàòåëüñòâî.
Äîñòàòî÷íî äîêàçàòü ïåðâîå óòâåðæäåíèå ëåììû, âòîðîå ïîëó÷àåòñÿ èç íåãî ïî ñèììåòðè÷íîñòè ëåâîãî è ïðàâîãî äåëåíèé.Äîêàçàòåëüñòâî ïðîâåä¼ì èíäóêöèåé ïî äëèíå ñëîâà w. Áàçîé ñëóæèòñëó÷àé |w| = 2, òîãäà ëèáî w = pp, ëèáî w = pp äëÿ íåêîòîðîãîïðèìèòèâíîãî òèïà p. Ñîîòâåòñòâåííî, ëèáî φ(w) = p · (p \ p/p), ëèáîφ(w) = (p \ p/p) · p.  ïåðâîì ñëó÷àå ïîëîæèì U 0 = (U · p)/p, âî âòîðîìñëó÷àå ïîëîæèì U 0 = (p/U ) \ p.  îáîèõ ñëó÷àÿõ íåòðóäíî ïðîâåðèòü,÷òî îáà òðåáîâàíèÿ, íàëîæåííûå íà òèï U 0 , âûïîëíÿþòñÿ.Ïðè äîêàçàòåëüñòâå øàãà èíäóêöèè ðàçáåð¼ì äâà ñëó÷àÿ: â ïåðâîì ñëó÷àå ñëîâî w ïðåäñòàâèìî â âèäå w = uv äëÿ íåêîòîðûõ íåïóñòûõñëîâ u, v , òàêèõ ÷òî χ(u) = χ(v) = ε; âî âòîðîì ñëó÷àå òàêîå ïðåäñòàâëåíèå íåâîçìîæíî.
 ïåðâîì ñëó÷àå ïðèìåíèì óòâåðæäåíèå ëåììûñíà÷àëà ê òèïàì U è φ(u), ïîëó÷èì, ÷òî íàéä¼òñÿ òèï Uu , òàêîé ÷òîL ` U φ(u) → Uu è U → Uu , ïðè÷¼ì l(Uu ) < l(U ) + 2 |u|. Ïîñëå ýòîãîïðèìåíèì óòâåðæäåíèå ëåììû ê òèïàì Uu è φ(v), ïîëó÷èì íåêîòîðûéòèï U 0 , òàêîé ÷òî L ` Uu φ(v) → U 0 , à òàêæå L ` Uu → U 0 .Äîêàæåì, ÷òî òèï U 0 ÿâëÿåòñÿ èñêîìûì. Ïðèìåíÿÿ ê âûâîäèìûìñåêâåíöèÿì U → Uu è Uu → U 0 ïðàâèëî ñå÷åíèÿ, ïîëó÷àåì, ÷òî L ` U →U 0 . Êðîìå òîãî, l(U 0 ) < l(U 0 )+2 |v| < l(U )+2 |u|+2 |v| = l(U )+2 |w|, ÷òîè áûëî íóæíî.
Ïî îïðåäåëåíèþ îòîáðàæåíèÿ φ èìååì φ(w) = φ(u)·φ(v).Âûâîäèìîñòü ñåêâåíöèè U · φ(w) → U 0 äîêàçàíà íèæå.U φ(u) → UuUu φ(v) → U 0U φ(u)φ(v) → U 0U (φ(u) · φ(v)) → U 0(cut)(· →)Òåïåðü ðàçáåð¼ì âòîðîé ñëó÷àé. Ñ òî÷íîñòüþ äî ïåðåèìåíîâàíèÿïåðåìåííûõ âîçìîæíû äâà ïîäñëó÷àÿ: w = pup è w = pup, ïðè÷¼ì ñëîâîu íåïóñòî è χ(u) = ε. Ýòî îçíà÷àåò, ÷òî ëèáî φ(w) = p · φ(u) · (p \ p/p),ëèáî φ(w) = (p \ p/p) · φ(u) · p.Ïðèìåíèì ëåììó ê òèïó p è ñëîâó u, ïîëó÷èì, ÷òî ñóùåñòâóþòòèïû P 0 è P 00 , òàêèå ÷òî ñåêâåíöèè pφ(u) → P 0 è p → P 0 , à òàêæå32φ(u)p → P 00 è p → P 00 ÿâëÿþòñÿ âûâîäèìûìè, ïðè÷¼ì l(P 0 ) < 2 |u| + 1è l(P 00 ) < 2 |u| + 1.
 ñëó÷àå åñëè φ(w) = p · φ(u) · (p \ p/p), ïîëîæèìU 0 = (p/(U · P 0 )) \ p/p, à âî âòîðîì ñëó÷àå U 0 = (p/U ) \ p/(P 00 \ p). Âîáîèõ ñëó÷àÿõ ïîëó÷àåì, ÷òî l(U 0 ) < l(U ) + 3 + 2 |u| + 1 = l(U ) + 2 |w|,÷òî è òðåáîâàëîñü.Äîêàæåì âûâîäèìîñòü ñåêâåíöèé U φ(w) → U 0 è U → U 0 . Íèæåïðèâåäåíû âûâîäû íåîáõîäèìûõ ñåêâåíöèé äëÿ ïåðâîãî ïîäñëó÷àÿ.pφ(u) → P 0U →UU pφ(u) → U · P 0(p/(U · P 0 ))U (p · φ(u))(p \ p/p)p → p(p/(U · P 0 ))U (p · φ(u) · (p \ p/p))p → p(→ /)U (p · φ(u) · (p \ p/p)) → (p/(U · P 0 )) \ p/pU →Up → P0Up → U · P 0(p/(U · P 0 ))U p → p(p/(U · P 0 ))U → p/p(/ →)(· →)(p/(U · P 0 ))U (p · φ(u) · (p \ p/p)) → p/pp→p(· →)U (p · φ(u)) → U · P 0p(p \ p/p))p → p(→ ·)(→ \)(→ ·)(/ →)(→ /)U → (p/(U · P 0 )) \ p/p(→ \)Äàëåå ïðèâåäåíû âûâîäû ñåêâåíöèé U · φ(w) → U 0 è U → U 0 äëÿâòîðîãî ïîäñëó÷àÿ.p → p φ(u)p → P 00p→pφ(u)p(P 00 \ p) → p(p/p)φ(u)p(P 00 \ p) → p(\ →)(/ →)p→p U →U(p/U )U → p(p/U )U (p \ p/p)φ(u)p(P 00 \ p) → p(p/U )U ((p \ p/p) · φ(u) · p)(P 00 \ p) → p(p/U )U ((p \ p/p) · φ(u) · p) → p/(P 00 \ p)(\ →)(· →)(→ /)U ((p \ p/p) · φ(u) · p) → (p/U ) \ p/(P 00 \ p)33(/ →)(→ \)p → P 00 U → Up→p(p/U )U → P 00(p/U )U (P 00 \ p) → p(p/U )U → p/(P 00 \ p)(/ →)(\ →)(→ /)U → (p/U ) \ p/(P 00 \ p)(→ \)Ëåììà äîêàçàíà.Ñëåäñòâèå 2.1.Äëÿ ëþáûõ òèïîâ U, E ∈ Tp, òàêèõ ÷òî JEK = ε, ñóùå-ñòâóþò òàêèå òèïû U 0 , U 00 , ÷òî1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
