Об отношении совместимости в исчислении Ламбека и в его варианте с операциями замещения, страница 14

Ëþáîé òèï A ∈ Tp0D ÿâëÿåòñÿ àòîìàðíîé êîíôèãóðàöèåé.843. Äëÿ ëþáîãî i > 0, ëþáîãî òèïà A ∈ TpiD è ëþáîãî êîíå÷íîãî íàáîðà ñëîâ Γ1 , . . . , Γi , êàæäîå èç êîòîðûõ ÿâëÿåòñÿ êîíêàòåíàöèåé êîíå÷íîãî ÷èñëà àòîìàðíûõ êîíôèãóðàöèé, âûðàæåíèå A{Γ1 ; . . . ; Γi }ÿâëÿåòñÿ àòîìàðíîé êîíôèãóðàöèåé.Êîíôèãóðàöèÿìè áóäåì íàçûâàòü ñëîâà, ïîëó÷åííûå êîíêàòåíàöèåé êîíå÷íîãî ÷èñëà àòîìàðíûõ êîíôèãóðàöèé. Êîíôèãóðàöèè áóäåìîáîçíà÷àòü áîëüøèìè ãðå÷åñêèìè áóêâàìè Γ, ∆, .

. ., âîçìîæíî ñ íèæíèìè èíäåêñàìè, à âñ¼ ìíîæåñòâî êîíôèãóðàöèé ÷åðåç O. Ïóñòóþêîíôèãóðàöèþ áóäåì îáîçíà÷àòü ÷åðåç Λ. Çàìåòèì, ÷òî åñëè Γ è ∆ ÿâëÿþòñÿ êîíôèãóðàöèÿìè, òî Γ∆ òàêæå áóäåò êîíôèãóðàöèåé.Íà êîíôèãóðàöèè åñòåñòâåííûì îáðàçîì ïðîäîëæàåòñÿ ôóíêöèÿñîðòà s, îïðåäåëÿåìàÿ ñëåäóþùèì îáðàçîì:1. s(Λ) = 0,2.

s([]) = 1,3. s(A) = 0, åñëè A ∈ Tp0D ,4. s(A{Γ1 ; . . . ; Γi }) = s(Γ1 ) + . . . + s(Γi ),5. s(Γ1 . . . Γr ) = s(Γ1 ) + . . . + s(Γr ), ãäå Γ1 , . . . , Γr àòîìàðíûå êîíôèãóðàöèè.Ïðèìåð 6.1.Ïóñòü s(A) = s(B) = 0, s(C) = 1, s(D) = 2, òîãäà(C/A){[]}(D↑1B){A; B; []} ÿâëÿåòñÿ êîíôèãóðàöèåé, s((C/A){[]}(D↑1 B){A; B; []}) = s((C/A){[]}) + s((D ↑1 B){A; B; []}) = 1 + 0 + 0 + 1 = 2.Äëÿ êàæäîé êîíôèãóðàöèè Γ ∈ O îïðåäåëèì å¼ ïðåäñòàâëÿþùèéòèï τ (Γ):1. τ ([]) = J ,2. τ (A) = A, åñëè A ∈ Tp0D ,3. τ (A{Γ1 ; . .

. ; Γi }) = (. . . (A i τ (Γi )) . . . 2 τ (Γ2 )) 1 τ (Γ1 ).4. τ (Γ1 . . . Γi ) = τ (Γ1 ) · . . . · τ (Γi ), åñëè Γ1 , . . . , Γi àòîìàðíûå êîíôèãóðàöèè.85Ïðèìåð 6.2.Ïóñòü s(A) = s(B) = 0, s(C) = 1, s(D) = 2 è Γ =(C/A){[]}(D↑1B){A; B; []}, òîãäà τ (Γ) = ((C/A)1 J)·((((D↑1B)3 J)2B) 1 A).Ëåììà 6.1.Äëÿ âñÿêîé êîíôèãóðàöèè Γ âåðíî, ÷òî s(Γ) = s(τ (Γ)).Äîêàçàòåëüñòâî. Èíäóêöèÿ ïî ïîñòðîåíèþ êîíôèãóðàöèè Γ.~ , ðàâÄëÿ êàæäîãî òèïà A îïðåäåëèì åãî âåêòîð-êîíôèãóðàöèþ Aíóþ A, åñëè s(A) = 0, è A{[]; .

. . ; []} â ïðîòèâíîì ñëó÷àå. Ñëåäóþùåå| {z }s(A) ðàçóòâåðæäåíèå âûòåêàåò èç àêñèîìàòèêè èñ÷èñëåíèÿ HDL è ñëåäñòâèÿ 4.1.Ëåììà 6.2.~ ÿâëÿþòñÿÄëÿ âñÿêîãî òèïà A ∈ TpD òèïû A è τ (A)ðàâíîñèëüíûìè â èñ÷èñëåíèè HDL.Òàêèì îáðàçîì, ïðè ïîñòðîåíèè êîíôèãóðàöèé êîíêàòåíàöèÿ ñîâïàäàåò ïî ñìûñëó ñî ñâÿçêîé ·, à îáîçíà÷åíèå A{Γ1 , . . . , Γs } îçíà÷àåò îä-~ íà êîíôèíîâðåìåííóþ çàìåíó ðàçäåëèòåëåé â âåêòîð-êîíôèãóðàöèè Aãóðàöèè Γ1 , .

. . , Γs , òî åñòü àíàëîãè÷íà ïîñëåäîâàòåëüíîìó ïðèìåíåíèþíåñêîëüêèõ îïåðàöèé j .Ëåãêî äîêàçàòü ïî èíäóêöèè, ÷òî ñîðò êîíôèãóðàöèè ðàâåí ÷èñëó âõîäÿùèõ â íå¼ ìåòàëèíãâèñòè÷åñêèõ ðàçäåëèòåëåé. Ýòè ðàçäåëèòåëèìîæíî óïîðÿäî÷èòü ñëåâà íàïðàâî. Ïóñòü Γ è ∆ êîíôèãóðàöèè, òîãäà ÷åðåç Γ|j ∆ îáîçíà÷àåòñÿ êîíôèãóðàöèÿ, ïîëó÷àåìàÿ çàìåíîé j -ãîðàçäåëèòåëÿ â Γ íà ∆. Ïóñòü s(Γ) = s, ∆1 , . . . , ∆s íåêîòîðûå êîíôèãóðàöèè, òîãäà ÷åðåç Γ ⊗ (∆1 ; . . .

; ∆s ) îáîçíà÷àåòñÿ êîíôèãóðàöèÿ,ïîëó÷àåìàÿ îäíîâðåìåííîé çàìåíîé âñåõ ðàçäåëèòåëåé â Γ ñëåâà íàïðàâî íà ∆1 , . . . , ∆s . Çàìåòèì, ÷òî êîíôèãóðàöèÿ Γ⊗(∆1 ; . . . ; ∆s ) ñîâïàäàåòñ êîíôèãóðàöèåé (. . . ((Γ|s ∆s )|s−1 ∆s−1 ) . . .)|1 ∆1 .Ïðèìåð 6.3.Ïóñòü s(A) = s(B) = 0, s(C) = 1, s(D) = 2, òîãäàC{(C/B){[]}}D{A; []} ⊗ {A; BJ{[]}} = C{(C/B){A}}, D{A; BJ{[]}}.Äëÿ äàëüíåéøåãî íàì ïîíàäîáèòñÿ ââåñòè ïîíÿòèå ãèïåðêîíòåêñòà. Âíà÷àëå îïðåäåëèì ïîíÿòèå êîíòåêñòà. Ôîðìàëüíîå îïðåäåëåíèå86ïðèâåäåíî íèæå, íåôîðìàëüíî æå êîíòåêñò ïðåäñòàâëÿåò ñîáîé êîíôèãóðàöèþ, â êîòîðîé îäèí èç ïðèìèòèâíûõ òèïîâ çàìåí¼í íà ñïåöèàëüíûéìàðêåð #, îáîçíà÷àþùèé ìåñòî ïîäñòàíîâêè â êîíòåêñò.Îïðåäåëåíèå 6.2.Ìíîæåñòâî êîíòåêñòîâ åñòü íàèìåíüøåå ìíîæå-ñòâî ñëîâ â àëôàâèòå TpD ∪ {[], {, }, ; , #}½ óäîâëåòâîðÿþùåå ñëåäóþùèìóñëîâèÿì:1.

# åñòü êîíòåêñò.2. Åñëè A ∈ TpD , s = s(A) > 0, 1 6 j 6 s, Ψ ÿâëÿåòñÿ êîíòåêñòîì, à Γ1 , . . . , Γj−1 , Γj+1 , . . . , Γs ÿâëÿþòñÿ êîíôèãóðàöèÿìè, òîA{Γ1 ; . . . ; Γj−1 ; Ψ; Γj+1 ; . . . ; Γs } ÿâëÿåòñÿ êîíòåêñòîì.3. Åñëè Ψ ÿâëÿåòñÿ êîíòåêñòîì, à Γ1 , . . . , Γj−1 , Γj+1 , . . . , Γs ÿâëÿþòñÿ àòîìàðíûìè êîíôèãóðàöèÿìè, òî Γ1 . . . Γj−1 ΨΓj+1 . . . Γs ÿâëÿåòñÿêîíòåêñòîì.Äëÿ êàæäîãî êîíòåêñòà Ψ è êîíôèãóðàöèè Γ ÷åðåç Ψ[Γ] îáîçíà÷èìðåçóëüòàò ïîäñòàíîâêè Γ â Ψ, ðàâíûé êîíôèãóðàöèè, ïîëó÷àþùåéñÿ ïðèçàìåíå â Ψ âõîæäåíèÿ ìàðêåðà # íà Γ.Ãèïåðêîíòåêñòîì Φ ñîðòà s íàçûâàåòñÿ ñîâîêóïíîñòü, ñîñòîÿùàÿèç êîíòåêñòà Ψ è êîíôèãóðàöèé ∆1 , . . . , ∆s . Ðåçóëüòàò ïîäñòàíîâêè êîíôèãóðàöèè Γ ñîðòà s â Φ ðàâåí Ψ[Γ ⊗ (∆1 ; . .

. ; ∆s )] è îáîçíà÷àåòñÿ ÷åðåçΦhΓi.  ýòîì ñëó÷àå Ψ íàçûâàåòñÿ âíåøíèì êîíòåêñòîì, à ∆1 , . . . , ∆s âíóòðåííèìè êîíôèãóðàöèÿìè äëÿ Γ. Ãèïåðêîíòåêñòû áóäåì îáîçíà÷àòü áîëüøîé ãðå÷åñêîé áóêâîé Φ.Ïðèìåð6.4.Ïóñòü s(A) = 0, s(B) = s(C) = 1, òîãäà Ψ =C{[]}(B ↑1 A){[]; #} ÿâëÿåòñÿ êîíòåêñòîì. Åñëè ãèïåðêîíòåêñò Φ ñîñòîèò èç âíåøíåãî êîíòåêñòà Ψ è âíóòðåííèõ êîíôèãóðàöèé A è B{A}, òîΦhB{[]}C{[]}i = C{[]}(B ↑1 A){[]; B{A}C{B{A}}}.Ñåêâåíöèè èñ÷èñëåíèÿ Ëàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿ èìåþòâèä Γ → A, ãäå Γ ∈ O, A ∈ TpD , ïðè÷¼ì s(Γ) = s(A). Òîãäà èñ÷èñëåíèåDL çàäà¼òñÿ ñëåäóþùåé àêñèîìàòèêîé:87~→AA~ →BΦhAiΓ→A(ax)ΦhΓi → B(cut)~ →CAΓ(→ \)Γ → A\C~ →DΦhCiΓ→A(\ →)−−−→ΦhΓ(A \ C)i → D~→CΓA(→ /)Γ → C/A~ →DΦhCiΓ→A(/ →)−−→Φh(C/A)Γi → DΓ→A∆→B(→ ·)Γ∆ → A · B~ Bi~ →DΦhA(· →)−−−→ΦhA · Bi → DΛ→IΦhΛi → A(→ I)~ kΓ → CA|Γ → A ↓k C~→CΓ|k AΓ → C ↑k AΦhIi → A(→↓)~ →DΦhCiΓ→A(↓→)−−−−−→ΦhΓ|k (A ↓k C)i → D(→↑)~ →DΦhCiΓ→A(↑ →)−−−−−→Φh(C ↑k A)|k Γi → D~ →D~ k BiΦhA|( →)−−−−→ΦhA k Bi → DΓ→A ∆→B(→ )Γ|k ∆ → A k BΦh[]i → A[] → J(→ J)Ïðèìåð 6.5.(I →)~ →AΦhJi(J →)~ → (A1 B)↑1 B ,Ïóñòü s(A) = s(B) = 1, òîãäà ñåêâåíöèè A−−−−−−−−−→A{J ·(A \ B)} → A ↓1 (A1 B) è (A ↑1 B) ↓1 A → A/(B \ A) ÿâëÿþòñÿ âû-âîäèìûìè â èñ÷èñëåíèè DL.

Ñîîòâåòñòâóþùèå âûâîäû ïðèâåäåíû íèæå.A{[]} → A B{[]} → BA{B} → A 1 BA{[]} → (A 1 B) ↓1 B88(→ )(→ ↓)A{[]} → A B{[]} → BA{B{[]}} → A 1 B(→ )A{[]} → AA{A{[]}(A \ B)} → A 1 BA{[](A \ B)} → A ↓1 (A 1 B)→↓A{J{[]}(A \ B)} → A ↓1 (A 1 B)(J →)A{J{[]} · (A \ B)} → A ↓1 (A 1 B)(· →)A{[]} → A B{[]} → BB{[]}(B \ A) → AA{[]} → A[](B \ A) → (A ↑1 B)((A ↑1 B) ↓1 A){[]}(B \ A) → A((A ↑1 B) ↓1 A){[]} → A/(B \ A)Ïðèìåð 6.6.(\ →)(\ →)(→ ↑)(↓ →)(→ /)Ïóñòü s(A) = s(B) = 1, òîãäà ñåêâåíöèÿ A{(A ↓1 B){[]}(J \ A)} → A 1 B ÿâëÿåòñÿ âûâîäèìîé â èñ÷èñëåíèè DL. Äåéñòâèòåëüíî, âûâåäåì ñíà÷àëà ñåêâåíöèþ A{A{(A ↓1 B){[]}}} → A 1 B :B{[]} → BA{[]} → AA{(A ↓1 B){[]}} → B(↓ →)A{[]} → AA{A{(A ↓1 B){[]}}} → A 1 B(→ )Ïðè ïðèìåíåíèè ïðàâèëà (↓ →), èìåþùåãî âèä~ →D Γ→AΦhCi−−−−−→ΦhΓ|k (A ↓k C) → D,ãèïåðêîíòåêñò Φ ñîñòîèò èç âíåøíåãî êîíòåêñòà # è âíóòðåííåé êîíôèãóðàöèè [], â êà÷åñòâå òèïîâ C è D âûñòóïàåò òèï B , à êîíôèãóðàöèÿ Γðàâíà A{[]}.Òåïåðü ïðèìåíèì ïðàâèëî (\ →), èìåþùåå âèä~ →D Γ→AΦhCi−−−→ΦhΓ(A \ C)i → D ,89âçÿâ â êà÷åñòâå âòîðîé ïîñûëêè âûâîäèìóþ ñåêâåíöèþ [] → J , à â êà÷åñòâå ãèïåðêîíòåêñòà Φ âçÿâ ñîâîêóïíîñòü èç âíåøíåãî êîíòåêñòà A{#}è âíóòðåííåé êîíôèãóðàöèè (A ↓1 B){[]}.

Òîãäà èìååò ìåñòî ðàâåíñòâî([](J \ A)) ⊗ ((A ↓1 B){[]}) = (A ↓1 B){[]} (J \ A), ÷òî ïðè ïîäñòàíîâêå âïðàâèëî ïðèâîäèò ê âûâîäèìîñòè ñåêâåíöèè A{(A ↓1 B){[]}(J \ A)} →A 1 B . äàëüíåéøåì ìû áóäåì îïóñêàòü çíà÷îê âåêòîðà ïðè çàïèñèâåêòîð-êîíôèãóðàöèé. Íàïðèìåð, åñëè s(A) = 0, s(B) = 1, s(C) =2, s(D) = 3, òî çàïèñü BAC → D îçíà÷àåò B{[]}AC{[]; []} → D.Êàê äîêàçàíî â ðàáîòå [32], DL ` Γ → A òîãäà è òîëüêî òîãäà,êîãäà HDL ` τ (Γ) → A. Îòñþäà ïî ëåììå 6.2 ñëåäóåò, ÷òî äëÿ ñåêâåíöèé âèäà A → B óòâåðæäåíèÿ îá èõ âûâîäèìîñòè â èñ÷èñëåíèÿõ DL èHDL ÿâëÿþòñÿ ðàâíîñèëüíûìè, òàêèì îáðàçîì èñ÷èñëåíèÿ DL è HDL âíåêîòîðîì ñìûñëå ýêâèâàëåíòíû.

Êàê äîêàçàíî â [24], â èñ÷èñëåíèè DLóñòðàíèìî ñå÷åíèå, òî åñòü âñÿêàÿ ñåêâåíöèÿ, âûâîäèìàÿ â ýòîì èñ÷èñëåíèè, ìîæåò áûòü âûâåäåíà áåç ïðèìåíåíèÿ ïðàâèëà (cut).  äàëüíåéøåììû áóäåì ðàññìàòðèâàòü òîëüêî âûâîäû áåç ñå÷åíèÿ, åñëè ÿâíî íå áóäåò îãîâîðåíî ïðîòèâíîå. Çàìåòèì, ÷òî èç óñòðàíèìîñòè ñå÷åíèÿ ñëåäóåòñâîéñòâî ïîäôîðìóëüíîñòè, èç êîòîðîãî âûòåêàåò ðàçðåøèìîñòü èñ÷èñëåíèÿ DL.Òàêæå èç óñòðàíèìîñòè ñå÷åíèÿ ñëåäóåò, ÷òî åñëè çàìåíèòü íåêîòîðûé ïîäòèï îäíîãî èç òèïîâ ñåêâåíöèè íà ðàâíîñèëüíûé åìó òèï, òîýòî íå ïîâëèÿåò íà âûâîäèìîñòü ñåêâåíöèè.

Êðîìå òîãî, â èñ÷èñëåíèèDL äîïóñòèìî ïðàâèëî ïîäñòàíîâêè, ïîçâîëÿþùåå çàìåíÿòü âñå âõîæäåíèÿ íåêîòîðîãî ïðèìèòèâíîãî òèïà p íà îäèí è òîò æå ïðîèçâîëüíûéòèï A òîãî æå ñîðòà. äàëüíåéøåì ïîä èñ÷èñëåíèåì Ëàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿìû áóäåì ïîäðàçóìåâàòü èìåííî èñ÷èñëåíèå DL.Îáîçíà÷èì ÷åðåç Ok ìíîæåñòâî êîíôèãóðàöèé, ñîðò êîòîðûõ íåïðåâûøàåò k , è êîòîðûå íå ñîäåðæàò òèïîâ íå èç Tpk . Èñ÷èñëåíèå, ïî90ëó÷àþùååñÿ èç DL çàïðåòîì òèïîâ íå èç Tpk è êîíôèãóðàöèé íå èçOk , îáîçíà÷àåòñÿ ÷åðåç DLk . Ïðè ëþáîì íàòóðàëüíîì k èñ÷èñëåíèå DLkýêâèâàëåíòíî ââåä¼ííîìó â ðàçäåëå 4.3 íåñåêâåíöèàëüíîìó èñ÷èñëåíèþHDLk .

Êàê è äëÿ ïîëíîãî èñ÷èñëåíèÿ DL, äëÿ ôðàãìåíòà DLk âåðíûñâîéñòâà ïîäôîðìóëüíîñòè è óñòðàíèìîñòè ñå÷åíèÿ. Èç ýòîãî âûòåêàåò,â ÷àñòíîñòè, ÷òî âñå èñ÷èñëåíèÿ DLk ÿâëÿþòñÿ êîíñåðâàòèâíûìè ðàñøèðåíèÿìè èñ÷èñëåíèé L∗ è L1 .6.2Êàòåãîðèàëüíûå ãðàììàòèêè, îñíîâàííûå íà âàðèàíòàõ èñ÷èñëåíèÿ ËàìáåêàÏîíÿòèå êàòåãîðèàëüíîé ãðàììàòèêè áûëî ââåäåíî Ê.