Об отношении совместимости в исчислении Ламбека и в его варианте с операциями замещения (1104173), страница 4
Текст из файла (страница 4)
Âïðèìåðå íèæå è â äàëüíåéøåì ÷åðåç N îáîçíà÷åíî ìíîæåñòâî íàòóðàëüíûõ ÷èñåë, ìû ñ÷èòàåì, ÷òî íàòóðàëüíûå ÷èñëà íà÷èíàþòñÿ ñ 0.Ïðèìåð 1.5.Ïóñòü Int(A) = {bk a | k ∈ N}, Int(B) = {ba, a}, òîãäàInt(A·B) = {bk abl a | k ∈ N, l ∈ {0, 1}}, Int(A/B) = {b}+ , Int(B \ A) = ∅.20Ñåêâåíöèþ A1 . . . An → B áóäåì íàçûâàòü èñòèííîé â ìîäåëèM = hΣ, Inti, åñëè Int(A1 ) · . . . · Int(An ) ⊆ Int(B). Èíäóêöèåé ïî âûâîäó ëåãêî äîêàçûâàåòñÿ, ÷òî âñÿêàÿ ñåêâåíöèÿ, âûâîäèìàÿ â èñ÷èñëåíèèL, áóäåò èñòèííà âî âñåõ ìîäåëÿõ íà ïîäìíîæåñòâàõ ñâîáîäíîé ïîëóãðóïïû, òî åñòü èñ÷èñëåíèå Ëàìáåêà êîððåêòíî îòíîñèòåëüíî ÿçûêîâûõìîäåëåé.
Îáðàòíûé ðåçóëüòàò (òî åñòü ïîëíîòà èñ÷èñëåíèÿ Ëàìáåêà îòíîñèòåëüíî ÿçûêîâûõ ìîäåëåé) áûë ïîëó÷åí Â. Áóøêîâñêèì äëÿ ñëó÷àÿèñ÷èñëåíèÿ Ëàìáåêà áåç óìíîæåíèÿ ([4]) è Ì. Ð. Ïåíòóñîì äëÿ ñëó÷àÿïîëíîãî èñ÷èñëåíèÿ Ëàìáåêà L ([36]).Àíàëîãè÷íûì îáðàçîì îïðåäåëÿþòñÿ ìîäåëè èñ÷èñëåíèÿ L∗ íàïîäìíîæåñòâàõ ñâîáîäíîãî ìîíîèäà.
Êàê è â ñëó÷àå èñ÷èñëåíèÿ L, èìååòìåñòî òåîðåìà êîððåêòíîñòè. Òåîðåìà ïîëíîòû äëÿ èñ÷èñëåíèÿ L∗ îòíîñèòåëüíî ìîäåëåé íà ïîäìíîæåñòâàõ ñâîáîäíîãî ìîíîèäà áûëà òàêæåäîêàçàíà Â. Áóøêîâñêèì äëÿ ñëó÷àÿ èñ÷èñëåíèÿ áåç óìíîæåíèÿ ([4]) èÌ. Ð. Ïåíòóñîì äëÿ ñëó÷àÿ ïîëíîãî èñ÷èñëåíèÿ L∗ ([28]).21Ãëàâà 2Âåðõíÿÿ îöåíêà äëèíûñîâìåùàþùåãî òèïà â èñ÷èñëåíèè2.1LÊðèòåðèé ñîâìåñòèìîñòè â èñ÷èñëåíèè Ëàìáåêà äàííîé ãëàâå ìû ðàññìîòðèì îòíîøåíèå ñîâìåñòèìîñòè äëÿ èñ÷èñëåíèÿ L, âïåðâûå îïðåäåë¼ííîå â [18].  [27] äîêàçàí êðèòåðèé ñîâìåñòèìîñòè â èñ÷èñëåíèè Ëàìáåêà â òåðìèíàõ èíòåðïðåòàöèè â ñâîáîäíîéïîëóãðóïïå.Îïðåäåëåíèå 2.1.Òèï C ∈ Tp íàçûâàåòñÿ ñîâìåùàþùèì äëÿ òèïîâA è B , åñëè L ` A → C è L ` B → C .
 ýòîì ñëó÷àå òèïû A è Bíàçûâàþòñÿ ñîâìåñòèìûìè .Îïðåäåëåíèå 2.2.Òèï D ∈ Tp íàçûâàåòñÿ ñîåäèíÿþùèì äëÿ òèïîâA è B , åñëè L ` D → A è L ` D → B .  ýòîì ñëó÷àå òèïû A è Bíàçûâàþòñÿ ñîåäèíèìûìè.Ïðèìåð 2.1.1. Òèï (p/(q \ p))/q ÿâëÿåòñÿ ñîâìåùàþùèì äëÿ òèïîâ (p/p) · (q/q) èq/q .2. Òèï p ÿâëÿåòñÿ ñîåäèíÿþùèì äëÿ òèïîâ (q/(p \ q)) è (r/p) \ r.Ñîîòâåòñòâóþùèå âûâîäû ïðèâåäåíû íèæå:221.p→p p→p(p/p)p → p(/ →)q →q q →q(q/q)q → q(p/p)(q/q)q(q \ p) → p(p/p)(q/q)q → p/(q \ p)(p/p)·(q/q) → (p/(q \ p))/qp→p(q/q)q → q(q/q)q(q \ p) → p(q/q)q → p/(q \ p)q/q → (p/(q \ p))/q2.q →q p→pp(p \ q) → qp → q/(p \ q)(→ \)(→ /)(p/p)(q/q) → (p/(q \ p))/qq →q q →q(/ →)(→ /)(· →)(/ →)(\ →)(→ /)(→ /)r→r p→p(\ →)(r/p)p → r(→ /)p → (r/p) \ r(/ →)(→ \)Ëåììà 2.1.1. Ïóñòü L ` A → C è L ` B → C .
Òîãäà L ` (A/C)A(A \ B) → A,L ` (A/C)A(A \ B) → B .2. Ïóñòü L ` D → A è L ` D → B . Òîãäà L ` A → (D/A) \ A/(B \ A),L ` B → (D/A) \ A/(B \ A).Äîêàçàòåëüñòâî.1.B→C A→AA→A A→C(\ →)(\ →)A → A A(A \ B) → CB→B(A/C)A → A(/ →)(\ →)(A/C)A(A \ B) → A(A/C)A(A \ B) → B2.D→B A→AA→A B→B(/ →)(/ →)A→A(D/A)A → BD → A B(B \ A) → A(\ →)(/ →)(D/A)A(B \ A) → A(D/A)B(B \ A) → A(→ \)(→ \)A(B \ A) → (D/A) \ AB(B \ A) → (D/A) \ A(→ /)(→ /)A → (D/A) \ A/(B \ A)B → (D/A) \ A/(B \ A)23Ëåììà 2.2.Òèïû A, B ∈ Tp ÿâëÿþòñÿ ñîâìåñòèìûìè òîãäà è òîëüêîòîãäà, êîãäà îíè ÿâëÿþòñÿ ñîåäèíèìûìè.Äîêàçàòåëüñòâî.
Ïóñòü A è B ñîâìåñòèìû, è C èõ ñîâìåùàþùèé òèï. êà÷åñòâå ñîåäèíÿþùåãî òèïà ìîæíî âçÿòü D = (A/C) · A · (A \ B).Ïóñòü òåïåðü A è B ñîåäèíèìû, è D èõ ñîåäèíÿþùèé òèï. Òîãäàñîâìåùàþùèì áóäåò òèï C = (D/A) \ A/(B \ A). Âûâîäèìîñòü ñîîòâåòñòâóþùèõ ñåêâåíöèé äîêàçàíà â ëåììå 2.1.Èç äàííîé ëåììû, âïåðâûå äîêàçàííîé â [18], ñëåäóåò, ÷òî îïðåäåëåíèÿ 2.1 è 2.2 çàäàþò îäíî è òî æå îòíîøåíèå, êîòîðîå ïðèíÿòîíàçûâàòü îòíîøåíèåì ñîâìåñòèìîñòè. Íåòðóäíî âèäåòü, ÷òî îòíîøåíèåñîâìåñòèìîñòè ÿâëÿåòñÿ ýêâèâàëåíòíîñòüþ. Ìû áóäåì ïèñàòü A ∼ B âñëó÷àå åñëè òèïû A è B ÿâëÿþòñÿ ñîâìåñòèìûìè.Ëåììà 2.3.∼ ÿâëÿåòñÿ êîíãðóýíöèåé îòíîñèòåëüíî ·, /, \.Äîêàçàòåëüñòâî.
Ïóñòü A1 ∼ B1 , A2 ∼ B2 , à C1 , C2 ñîâìåùàþùèåòèïû äëÿ äàííûõ ïàð òèïîâ, à D1 , D2 ñîåäèíÿþùèå òèïû äëÿ òåõæå ïàð. Äîêàæåì, ÷òî A1 · A2 ∼ B1 · B2 . Äåéñòâèòåëüíî, â êà÷åñòâåñîâìåùàþùåãî òèïà ìîæíî âçÿòü C1 · C2 . Àíàëîãè÷íûì îáðàçîì òèïC1 /D2 áóäåò ñîâìåùàþùèì äëÿ òèïîâ A1 /A2 è B1 /B2 , à òèï D2 \ C1 äëÿ òèïîâ B2 \ B1 è A2 \ A1 .Ïóñòü Pr = {p1 , p2 , .
. .} ìíîæåñòâî ïðèìèòèâíûõ òèïîâ, èñïîëüçîâàííûõ ïðè ïîñòðîåíèè òèïîâ èç Tp. Îáîçíà÷èì ÷åðåç G ñâîáîäíóþãðóïïó, ïîðîæä¼ííóþ ìíîæåñòâîì Pr, ãðóïïîâóþ îïåðàöèþ áóäåì îáîçíà÷àòü ÷åðåç ◦ (â äàëüíåéøåì ìû çà÷àñòóþ áóäåì îïóñêàòü ñèìâîë îïåðàöèè), åäèíèöó ãðóïïû G áóäåì îáîçíà÷àòü ÷åðåç ε, à ýëåìåíò, îáðàòíûéê ýëåìåíòó a, ÷åðåç a−1 .Îïðåäåëåíèå 2.3.Èíòåðïðåòàöèåé òèïà A â ãðóïïå G íàçûâàåòñÿýëåìåíò JAK ∈ G , îïðåäåëÿåìûé ñëåäóþùèìè ïðàâèëàìè:241.
JpK = p, åñëè p ∈ Pr,2. JA · BK = JAK ◦ JBK,3. JA/BK = JAK ◦ JBK−1 ,4. JB \ AK = JBK−1 ◦ JAK.Ïîíÿòèå èíòåðïðåòàöèè ìîæåò áûòü ïðîäîëæåíî íà ïîñëåäîâàòåëüíîñòè òèïîâ: JA1 . . . An K = JA1 K . . . JAn K. Ñëåäóþùåå óòâåðæäåíèåëåãêî äîêàçûâàåòñÿ èíäóêöèåé ïî âûâîäó â èñ÷èñëåíèè L.Åñëè L ` Γ → A, òî JΓK = JAK.Ëåììà 2.4.Ñëåäóþùàÿ òåîðåìà, äîêàçàííàÿ â [27], õàðàêòåðèçóåò îòíîøåíèåñîâìåñòèìîñòè â èñ÷èñëåíèÿõ L è L∗ â òåðìèíàõ èíòåðïðåòàöèè â ñâîáîäíîé ãðóïïå.Òåîðåìà 1(Ì. Ð.
Ïåíòóñ, 1992). Ñëåäóþùèå óòâåðæäåíèÿ ðàâíîñèëü-íû:1. A ∼L B .2. A ∼L∗ B .3. JAK = JBK.2.2Ñõåìà ïîñòðîåíèÿ ñîâìåùàþùåãî òèïàÕîòÿ òåîðåìà 1 è çàäà¼ò óñëîâèÿ ñóùåñòâîâàíèÿ ñîâìåùàþùåãî òèïà,îíà íå ïîçâîëÿåò ÿâíî îöåíèòü åãî äëèíó. Ïóñòü A è B ñîâìåñòèìûåòèïû, îáîçíà÷èì ÷åðåç mj (A, B) äëèíó èõ ñàìîãî êîðîòêîãî ñîâìåùàþùåãî òèïà. Îáîçíà÷èì ÷åðåç Mj (l1 , l2 ) ìàêñèìàëüíîå çíà÷åíèå äàííîéâåëè÷èíû äëÿ ñîâìåñòèìûõ òèïîâ A è B , òàêèõ ÷òî l(A) = l1 è l(B) = l2 .Íàøà çàäà÷à ñîñòîèò â îöåíêå ñâåðõó âåëè÷èíû Mj (l1 , l2 ), â ÷àñòíîñòè,ìû äîêàæåì ñëåäóþùóþ òåîðåìó:Òåîðåìà 2.Äëÿ ëþáûõ ñîâìåñòèìûõ â èñ÷èñëåíèè L òèïîâ A, B ∈ Tpíàéä¼òñÿ ñîâìåùàþùèé òèï C , òàêîé ÷òî l(C) 6 12 (l2 (A) + l2 (B)) +352(l(A) + l(B)).25Äîêàçàòåëüñòâî áóäåò ïðîâåäåíî êîíñòðóêòèâíî ïóò¼ì ïðåäúÿâëåíèÿ ñîîòâåòñòâóþùåãî òèïà C .
 äàííîì ðàçäåëå ìû îïèøåì îáùóþñõåìó åãî ïîñòðîåíèÿ, à â ñëåäóþùåé äîêàæåì, ÷òî ïîñòðîåííûé òèï èâïðàâäó óäîâëåòâîðÿåò óñëîâèÿì òåîðåìû.Ââåä¼ì âñïîìîãàòåëüíûé àëôàâèò P = Pr ∪ {p | p ∈ Pr}. Äëÿêàæäîãî ñëîâà w ∈ P + îïðåäåëèì îáðàòíîå ñëîâî w−1 : p−1 = p,p−1 = p, (a1 . . . an )−1 = (an )−1 . . . (a1 )−1 , ãäå a1 , . . . , an ∈ P . Ïîñëå ýòîãî äëÿ êàæäîãî òèïà A ∈ Tp îïðåäåëèì åãî ïðåäñòàâëåíèå hAi, ïîëîæèâ hpi = p, p ∈ Pr, hA · Bi = hAihBi, hA/Bi = hAihBi−1 , hB \ Ai =hBi−1 hAi. Çàìåòèì, ÷òî ôàêòè÷åñêè îòîáðàæåíèå h·i : Tp → P ∗ ïðåäñòàâëÿåò ñîáîé èíòåðïðåòàöèþ â ñâîáîäíîì ìîíîèäå, ïîðîæä¼ííîì ïðèìèòèâíûìè òèïàìè è èõ îáðàòíûìè ýëåìåíòàìè.
Ïóñòü îòîáðàæåíèåχ : P → G äåéñòâóåò ïî ïðàâèëó χ(p) = p, χ(p) = p−1 , òîãäà χ åñòåñòâåííûì îáðàçîì ïðîäîëæàåòñÿ äî ãîìîìîðôèçìà èç ñâîáîäíîãî ìîíîèäà P ∗â ñâîáîäíóþ ãðóïïó G . Çàìåòèì, ÷òî ïðè ýòîì JAK = χ(hAi), òî åñòü JAKôàêòè÷åñêè ÿâëÿåòñÿ íîðìàëüíîé ôîðìîé ñëîâà hAi ïîñëå åñòåñòâåííîãî îòîæäåñòâëåíèÿ ýëåìåíòîâ p è p−1 è ñîêðàùåíèÿ äî ïóñòîãî ñëîâà ïàðp−1 p è pp−1 . Òàêèì îáðàçîì, åñëè hAi = hBi, òî òåì áîëåå JAK = JBK è,ñëåäîâàòåëüíî, òèïû A è B â ýòîì ñëó÷àå ÿâëÿþòñÿ ñîâìåñòèìûìè.Áåç îãðàíè÷åíèÿ îáùíîñòè ìîæíî ñ÷èòàòü, ÷òî ìíîæåñòâî Pr ñîäåðæèò âûäåëåííûé ýëåìåíò q , íå âõîäÿùèé â òèïû A è B .
Îïðåäåëèì îòîáðàæåíèå φ : P ∗ → Tp, ïîëîæèâ φ(ε) = q/q, φ(p) = p,φ(p) = (p \ p/p), p ∈ Pr, φ(aw1 ) = φ(a) · φ(w1 ), a ∈ P, w1 6= ε. Îòîæäåñòâèâ ýëåìåíòû p è p−1 , ìîæíî ñ÷èòàòü, ÷òî φ òàêæå îïðåäåëåíî íàíåñîêðàòèìûõ ñëîâàõ íàä àëôàâèòîì Pr ∪ {p−1 | p ∈ Pr}, òî åñòü íàäñâîáîäíîé ãðóïïîé G .Ïðèìåð2.2.Ïóñòü A = ((p · r)/p) \((p/(q/r)) · r), òîãäà hAi =prpprqr, χ(hAi) = pr−1 p−1 prq −1 r, JAK = pq −1 r, φ(hAi) = p · (r \ r/r) ·(p \ p/p) · p · r · (q \ q/q) · r, φ(JAK) = p · (q \ q/q) · r.Ëåììà 2.5.Äëÿ ëþáîãî ñëîâà w ∈ P ∗ âåðíî, ÷òî Jφ(w)K = χ(w).26Äîêàçàòåëüñòâî.
Èíäóêöèÿ ïî äëèíå ñëîâà w. Äëÿ äîêàçàòåëüñòâà áàçûèíäóêöèè ðàññìîòðèì ñëó÷àè |w| = 0 è |w| = 1. Åñëè |w| = 0, òî w = ε èJφ(w)K = Jq/qK = ε = w. Åñëè |w| = 1 è w = p ∈ Pr, òî Jφ(w)K = p = w,åñëè æå |w| = 1 è w = p, òî Jφ(w)K = Jp \ p/pK = p−1 = χ(p), òàêèìîáðàçîì, áàçà èíäóêöèè ïîëíîñòüþ äîêàçàíà.Ïóñòü òåïåðü w > 1, òîãäà w = aw1 , a ∈ P .  ýòîì ñëó÷àåJφ(aw1 )K = Jφ(a)φ(w1 )K = Jφ(a)KJφ(w1 )K = χ(a)χ(w1 ) = χ(aw1 ), ÷òîè òðåáîâàëîñü.Ëåììà 2.6.Òèïû A, φ(hAi) è φ(JAK) ÿâëÿþòñÿ ñîâìåñòèìûìè â èñ-÷èñëåíèè L äëÿ ëþáîãî A ∈ Tp.Äîêàçàòåëüñòâî. Äëÿ äîêàçàòåëüñòâà ïðèìåíèì êðèòåðèé ñîâìåñòèìîñòè (òåîðåìó 1).
 ñèëó ëåììû 2.5 âåðíî, ÷òî Jφ(hAi)K = χ(hAi) = JAKè Jφ(JAK)K = χ(JAK) = JAK. Ëåììà äîêàçàíà.Çàìåòèì, ÷òî óòâåðæäåíèÿ ëåììû 2.6 ìîãóò áûòü äîêàçàíû èíåïîñðåäñòâåííî ïóò¼ì ïðåäúÿâëåíèÿ ñîîòâåòñòâóþùèõ ñîâìåùàþùèõ òèïîâ. Ìû îñóùåñòâèì ýòî â ñëåäóþùåì ðàçäåëå. Äîêàæåì âñïîìîãàòåëüíóþ òåõíè÷åñêóþ ëåììó.Îïðåäåëåíèå 2.4.1. Òèï A íàçûâàåòñÿ òèïîì áåç ïîëîæèòåëüíûõ óìíîæåíèé , åñëèìíîæåñòâî Subocc+ (A) íå ñîäåðæèò ýëåìåíòîâ âèäà hC · D, ii íèäëÿ êàêèõ C, D ∈ Tp è i ∈ N.2. Òèï A íàçûâàåòñÿ òèïîì áåç îòðèöàòåëüíûõ óìíîæåíèé , åñëè ìíîæåñòâî Subocc− (A) íå ñîäåðæèò ýëåìåíòîâ âèäà hC · D, ii íè äëÿêàêèõ C, D ∈ Tp è i ∈ N.Ëåììà 2.7.1. Äëÿ ëþáîãî A ∈ Tp ñóùåñòâóåò A0 ∈ Tp áåç îòðèöàòåëüíûõóìíîæåíèé, òàêîé ÷òî L ` A → A0 , l(A0 ) = l(A) è hA0 i = hAi.272.
Äëÿ ëþáîãî A ∈ Tp ñóùåñòâóþò òèïû A10 , . . . , An0 ∈ Tp áåç ïîëînPl(Ai0 ) =æèòåëüíûõ óìíîæåíèé, òàêèå ÷òî L ` A10 . . . An0 → A,l(A) èhA10 i . . . hAn0 ii=1= hAi.Äîêàçàòåëüñòâî. Áóäåì ïàðàëëåëüíî äîêàçûâàòü îáà ïóíêòà èíäóêöèåéïî ïîñòðîåíèþ òèïà A.  ñëó÷àå A = p â îáîèõ ïóíêòàõ äîñòàòî÷íîïîëîæèòü A0 = p.1. Íà øàãå èíäóêöèè ðàçáåð¼ì òðè ñëó÷àÿ. Ïåðâûé ñëó÷àé: A = B·C , â ýòîì ñëó÷àå äîñòàòî÷íî ïîëîæèòü A0 = B0 · C0 , ãäå B0 è C0 áåðóòñÿèç ïðèìåíåíèÿ ïåðâîãî ïóíêòà ëåììû ê òèïàì B è C . Äåéñòâèòåëüíî,ïî ïðàâèëàì (· →) è (→ ·) ñåêâåíöèÿ B · C → B0 · C0 áóäåò âûâîäèìà.
Ïîîïðåäåëåíèþ èìååì l(A0 ) = l(B0 ) + l(C0 ) = l(B) + l(C) = l(A), à òàêæåhA0 i = hB0 ihC0 i = hBihCi = hB · Ci, ÷òî è òðåáîâàëîñü.Ðàçáåð¼ì âòîðîé ñëó÷àé A = B/C . Âîçüì¼ì òèï B0 , ïîëó÷àþùèéñÿ ïðè ïðèìåíåíèè ïóíêòà 1 ëåììû ê òèïó B , è òèïû C01 , . . . , C0n ,ïîëó÷àþùèåñÿ ïðè ïðèìåíåíèè ïóíêòà 2 ëåììû ê òèïó C , è ðàññìîòðèìòèï A0 = (. . . (B0 /C0n ) . . .)/C01 . Äîêàæåì, ÷òî A0 óäîâëåòâîðÿåò óòâåðæäåíèþ ëåììû. Äåéñòâèòåëüíî, îòðèöàòåëüíûå âõîæäåíèÿ óìíîæåíèÿâ A0 áûëè ëèáî îòðèöàòåëüíûìè âõîæäåíèÿìè óìíîæåíèÿ â B0 , ëèáîjïîëîæèòåëüíûìè âõîæäåíèÿìè â îäíîì èç C0 , íî è òå, è äðóãèå îòñóòñòâóþò ïî ïðåäïîëîæåíèþ èíäóêöèè.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
