Об отношении совместимости в исчислении Ламбека и в его варианте с операциями замещения (1104173), страница 17
Текст из файла (страница 17)
Ðàçáåð¼ì îñòàëüíûå ïðàâèëà, ââîäÿùèå íåêîòîðóþ ñâÿçêóâ àíòåöåäåíòå.Ïóñòü ïîñëåäíèì ïðàâèëîì â âûâîäå áûëî (\ →) â ôîðìåΦhBi → C Π → A. Áîëåå ïîäðîáíî àíòåöåäåíò ïîñûëêè çàïèñûâàåòñÿΦhΠ(A \ B)i → Cêàê Φ0 [B{Φ1 ; . . . ; Φs(B) }], à àíòåöåäåíò çàêëþ÷åíèÿ êàê Φ0 [(Π(A \ B)) ⊗{Φ1 ; . . . ; Φs(B) }]. Âîçìîæíû äâà ñëó÷àÿ: A ∈ T è A = qi äëÿ íåêîòîðîãîi, â îáîèõ ñëó÷àÿõ ïî ïîñòðîåíèþ B ∈ T , òî åñòü (B)q = Λ, âñëåäñòâèå÷åãî âåðíî ðàâåíñòâî (Π(A \ B))q = (Π → A)q , è ïîýòîìó (Π(A \ B))q ÿâëÿåòñÿ ÏÑÏ. Ïî ïðåäïîëîæåíèþ èíäóêöèè Φ1 , . . . , Φs(B) q -ïðàâèëüíûåêîíôèãóðàöèè, ïîñëå ÷åãî äëÿ äîêàçàòåëüñòâà ïåðâîãî óòâåðæäåíèÿ ëåììû íóæíî ïðèìåíèòü ïóíêò 6 ëåììû 6.7. Âòîðîå óòâåðæäåíèå ëåììûàíàëîãè÷íûì îáðàçîì ñëåäóåò èç ïóíêòà 5 ëåììû 6.8.
Ñëó÷àé ïðàâèëà(/ →) ðàçáèðàåòñÿ àíàëîãè÷íî.Ïóñòü ïîñëåäíèì ïðàâèëîì â âûâîäå áûëî (↑ →) â ôîðìåΦhBi → C Π → A. Áîëåå ïîäðîáíî àíòåöåäåíò ïåðâîé ïîñûëêè çàΦh(B ↑j A)|j Πi → Cïèñûâàåòñÿ êàê Φ0 [B{Φ1 ; . . . ; Φs(B) }], à àíòåöåäåíò çàêëþ÷åíèÿ êàêΦ0 [(B ↑j A) ⊗ {Φ1 ; . .
. ; Φj−1 ; Π ⊗ {Φj ; . . . ; Φj+s(A)−1 }; Φj+s(A) ; . . . ; Φs(B) }].Ïî îïðåäåëåíèþ ìíîæåñòâà T 0 èìååì (B ↑j A)q = Λ, òîãäà (Π → A)q =(Π)q è ïî ïðåäïîëîæåíèþ èíäóêöèè Π áóäåò q -ïðàâèëüíîé êîíôèãóðàöèåé. Ñëåäîâàòåëüíî, ïî ïóíêòó 3 ëåììû 6.7 (B ↑j A)|j Π òàêæå áóäåòq -ïðàâèëüíîé êîíôèãóðàöèåé. Òàêæå q -ïðàâèëüíûìè êîíôèãóðàöèÿìèÿâëÿþòñÿ Φ1 , .
. . , Φs(B) è B{Φ1 ; . . . ; Φs(B) }, îòêóäà ïî ïóíêòó 5 ëåììû6.7 ïîëó÷àåì ïåðâîå óòâåðæäåíèå ëåììû. Ïðèìåíÿÿ ïðåäïîëîæåíèå èíäóêöèè è ïóíêò 5 ëåììû 6.8, äîêàçûâàåì è âòîðîå óòâåðæäåíèå ëåììû.Àíàëîãè÷íûå ðàññóæäåíèÿ ìîæíî èñïîëüçîâàòü â ñëó÷àå ïðàâèëà (↓→). Äåéñòâèòåëüíî, ïóñòü åãî ïðèìåíåíèå èìåëî âèäΦhBi → C Π → A. Òîãäà àíòåöåäåíò ïåðâîé ïîñûëêè â ïîäðîáíîéΦhΠ|j (A ↓j B)i → C104çàïèñè èìååò âèä Φ0 [B{Φ1 ; . . . ; Φs(B) }], à àíòåöåäåíò çàêëþ÷åíèÿ çàïèñûâàåòñÿ êàê Φ0 [Π ⊗ {Φ1 ; . .
. ; Φj−1 ; (A ↓j B) ⊗ {Φj ; . . . ; Φj+s(B)−s(A) };Φj+s(B)−s(A)+1 ; . . . ; Φs(B) }]. Ïî îïðåäåëåíèþ ìíîæåñòâà T 0 èìååì (A)q =(B)q = (A ↓j B)q = Λ. Ïîñëå ýòîãî ðàññóæäåíèÿ ïîâòîðÿþò äîêàçàòåëüñòâî ïðåäûäóùåãî ñëó÷àÿ.Âñå ñëó÷àè ðàçîáðàíû è ëåììà äîêàçàíà.Ïðèìåð 6.14.1. Ïóñòü ìíîæåñòâî T ñîäåðæèò òèï B ↓1 (B 1 C), ïðè÷¼ì s(B) =1, s(C) = 0, òîãäà ñåêâåíöèÿ (q1 \ C) · q2 → (q1 \(B ↓1 (B 1 C)) · q2ÿâëÿåòñÿ âûâîäèìîé è å¼ q -îáðàç ðàâåí q1 q 1 q2 q 2 .2.
Ïóñòü ìíîæåñòâî T ñîäåðæèò òèï (B ↑1 I) 1 C , ïðè÷¼ì s(B) =s(C) = 0, òîãäà ñåêâåíöèÿ q1 q2 (q2 \ C)(q1 \ B) → (B ↑1 I) 1 C ÿâëÿåòñÿ âûâîäèìîé è å¼ q -îáðàç ðàâåí q1 q2 q 2 q 1 .Ñîîòâåòñòâóþùèå âûâîäû ïðèâåäåíû íèæå. Çàìåòèì, ÷òî â ïåðâîì ïðèìåðå âõîæäåíèÿ ïðèìèòèâíîãî òèïà q1 â òå÷åíèå âûâîäà íàõîäèëèñüâíóòðè îäíîé èç ìàêñèìàëüíîé ïîäêîíôèãóðàöèé, õîòÿ â ïîñëåäíåé ñåêâåíöèè íå âõîäÿò íè â îäíó òàêóþ ïîäêîíôèãóðàöèþ.
Ýòî îáúÿñíÿåòðàññìîòðåíèå ìàêñèìàëüíûõ ïîäêîíôèãóðàöèé â ëåììå 6.9.B→B C→C(→ )B{C} → B 1 Cq1 → q1B{q1 (q1 \ C)} → B 1 Cq1 (q1 \ C) → B ↓1 (B 1 C)(\ →)(→ ↓)(q1 \ C) → q1 \(B ↓1 (B 1 C))(→ \)q 2 → q2(q1 \ C)q2 → (q1 \(B ↓1 (B 1 C))) · q2(q1 \ C) · q2 → (q1 \(B ↓1 (B 1 C))) · q2105(→ ·)(· →)B→Bq 1 → q1q1 (q1 \ B) → Bq1 I(q1 \ B) → B(\ →)(I →)q1 [](q1 \ B) → B ↑1 I(→↑)C→Cq2 → q2q2 (q2 \ C) → Cq1 q2 (q2 \ C)(q1 \ B) → (B ↑1 I) 1 C(\ →)(→ )Äîêàæåì ïðîñòóþ òåõíè÷åñêóþ ëåììó:Ëåììà 6.10.Òèïû B è (I \ B) · I ÿâëÿþòñÿ ðàâíîñèëüíûìè â èñ÷èñ-ëåíèè DL.Äîêàçàòåëüñòâî.B→B(I →)IB → B(→ \)B → I \B→IB → (I \ B) · I(→ ·)B→B →I(→ \)(I \ B) → B(I →)(I \ B)I → B(· →)(I \ B) · I → BÍàïîìíèì, ÷òî â èñ÷èñëåíèè DL äîïóñòèìû ïðàâèëà ïîäñòàíîâêèè çàìåíû òèïà íà ýêâèâàëåíòíûé.Ëåììà 6.11.Ãðàììàòèêà G 0 ïîðîæäàåò â òî÷íîñòè ÿçûê L ∩ LR .Äîêàçàòåëüñòâî.
Äîñòàòî÷íî äîêàçàòü, ÷òî âûâîäèìîñòü ñåêâåíöèèA1i1 ,j1 . . . Arir ,jr → Hj0 ,i0 äëÿ íåîòðèöàòåëüíûõ i0 , j0 , . . . , ir , jr ðàâíîñèëüíà îäíîâðåìåííîìó âûïîëíåíèþ óñëîâèé DL ` A1 . . . Ar → H è j0 = i1 ,. . . , jr−1 = ir , jr = i0 . Ïóñòü âíà÷àëå ñåêâåíöèÿ A1 . . . Ar → H âûâîäèìàâ èñ÷èñëåíèè DL, òîãäà ïðèìåíÿÿ r − 1 ðàç ïðàâèëî (\ →), ïîëó÷àåì,÷òî DL ` qj0 (qj0 \ A1 )qj1 . . . Ar−1 qjr−1 (qjr−1 \ Ar ) → H , îòêóäà ïî ïðàâèëó106(→ \) ïîëó÷àåì DL ` (qj0 \ A1 )qj1 .
. . Ar−1 qjr−1 (qjr−1 \ Ar ) → qj0 \ H , ÷òîïî ïðàâèëó (→ ·) âëå÷¼ò DL ` (qj0 \ A1 )qj1 . . . Ar−1 qjr−1 (qjr−1 \ Ar )qi0 →(qj0 \ H) · qi0 , îòêóäà ïîñëå r − 1 ïðèìåíåíèé ïðàâèëà (· →) ïîëó÷àåìòðåáóåìîå.Ïóñòü òåïåðü ñåêâåíöèÿ A1i1 ,j1 . . . Arir ,jr → Hj0 ,i0 ÿâëÿåòñÿ âûâîäèìîé. ż q -îáðàç ðàâåí qj0 q i1 qj1 . . . q ir qjr q i0 . Ïîñêîëüêó âñå èíäåêñû îòëè÷íû îò 0, èç ëåììû 6.9 ïîëó÷àåì j0 = i1 , j1 = i2 , .
. . ,jr−1 = ir , jr = i0 . Ïîäñòàâèì â ðàññìàòðèâàåìóþ ñåêâåíöèþ òèï Iâìåñòî âñåõ ïðèìèòèâíûõ òèïîâ èç ìíîæåñòâà Q, ïîëó÷èì ñåêâåíöèþ(I \ A1 ) · I . . . (I \ Ar ) · I → (I \ H) · I .  ñèëó äîïóñòèìîñòè ïðàâèëàïîäñòàíîâêè äàííàÿ ñåêâåíöèÿ áóäåò âûâîäèìîé. Âîñïîëüçóåìñÿ äîïóñòèìîñòüþ çàìåíû òèïà íà ýêâèâàëåíòíûé, òîãäà ïî ëåììå 6.10 èìååì,÷òî ñåêâåíöèÿ A1 . . . Ar → H òàêæå áóäåò âûâîäèìîé, ÷òî è òðåáîâàëîñü.Ëåììà äîêàçàíà.Èç äîêàçàííîé ëåììû ñëåäóåò ñëåäóþùàÿ òåîðåìà.Òåîðåìà 15.Ìíîæåñòâî ÿçûêîâ, ðàñïîçíàâàåìûõ DL -ãðàììàòèêàìè,çàìêíóòî îòíîñèòåëüíî ïåðåñå÷åíèÿ ñ àâòîìàòíûìè ÿçûêàìè, íå ñîäåðæàùèìè ïóñòîãî ñëîâà.Ê ñîæàëåíèþ, êîíñòðóêöèþ, èñïîëüçîâàííóþ â äàííîé ðàáîòå, ïîêà íå óäà¼òñÿ îáîáùèòü íà ñëó÷àé, êîãäà êîíå÷íûé àâòîìàò ñîäåðæèòáîëåå îäíîãî çàâåðøàþùåãî ñîñòîÿíèÿ.
Îòìåòèì, ÷òî òî÷íàÿ õàðàêòåðèçàöèÿ êëàññà ÿçûêîâ, ïîðîæäàåìûõ DL -ãðàììàòèêàìè, òàêæå ÿâëÿåòñÿîòêðûòûì âîïðîñîì.107Ïðåäìåòíûé óêàçàòåëüAk , 53A0 , 29A1 , 29A2 , 29A3 , 30dAe, 46JAK, 43, 68JAK∗ , 70hAi, 26JAKp , 70[A]∼ , 81b, 42A~ , 86AA ∼ B , 24, 67At, 41Bl , 53Base, 60D(A), 52DL, 87DLk , 91E(A, B), 52F, 68G , 24Fm, 41108G 0 , 97H , 91HDLk , 63L, 14L(G), 9193L1 , 57L∗ , 18MCLL, 41Mj (l1 , l2 ), 25MjMCLL (l1 , l2 ), 45N, 20N , 47O(T 0 ), 98Occ, 17Occ+ , 17Occ− , 17O, 85Ok , 90P , 20P , 26Pr, 14PrD , 60Prk , 68Q, 97Q, 98Subocc+ (A), 17Subocc− (A), 17Tk , 53Ti,j , 98Tp, 14109Tp0∼ , 81TpD , 60TpiD , 84Tpk , 63T , 98T 0 , 98Ul , 53Vi , 53Var, 40Wi , 53d(A), 43h(JEK), 82l(A), 44s(A), 60s(w), 58s(Γ), 85ΩΓ , 45Σ, 18Σ∗ , 18Σ+ , 18Σ1 , 58α, ýëåìåíò ãðóïïû F, 68χ(w), 26δΓ (α), 46δΓ (α, β), 46ε, 18φ(w), 26τ (Γ), 85àêñèîìíàÿ ñâÿçü, 47àëôàâèò, 18110àíòåöåäåíò, 14áóêâà, 18âåêòîð-êîíôèãóðàöèÿ, 86âõîæäåíèåïîäòèïà, 17ïðèìèòèâíîãî òèïà, 17ãèïåðêîíòåêñò, 87ãðàììàòèêàËàìáåêà, 91ðàçðûâíàÿ, 93DL -ãðàììàòèêà, 93DLk -ãðàììàòèêà, 93HDL-ãðàììàòèêà, 92L-ãðàììàòèêà, 91äëèíàñëîâà, 18òèïàâ èñ÷èñëåíèè HDLk , 69â èñ÷èñëåíèè L, 16çàìåùåíèå, 59èíòåðïðåòàöèÿâ ñâîáîäíîé àáåëåâîé ãðóïïå, 68â ñâîáîäíîé ãðóïïåôîðìóë èñ÷èñëåíèÿ MCLL, 43òèïîâ èñ÷èñëåíèÿ L, 24èñ÷èñëåíèå Ëàìáåêàäîïóñêàþùåå ïóñòûå àíòåöåäåíòû, 18ñ åäèíèöåé, 57ñ îïåðàöèÿìè çàìåùåíèÿíåñåêâåíöèàëüíîå, 61111ñåêâåíöèàëüíîå, 87êîíå÷íûé àâòîìàò, 94êîíêàòåíàöèÿ, 19êîíñåðâàòèâíîñòü, 57êîíòåêñò, 87êîíôèãóðàöèÿèñ÷èñëåíèÿ DL, 85q -ïðàâèëüíàÿ, 100àòîìàðíàÿ, 84âíóòðåííå q -ïðàâèëüíàÿ, 101êîíå÷íîãî àâòîìàòà, 94ëåâîå äåëåíèå, 14îïåðàöèÿ íàä ÿçûêàìè, 19ìîäåëüíà ïîäìíîæåñòâàõ ñâîáîäíîãî ìîíîèäà, 21íà ïîäìíîæåñòâàõ ñâîáîäíîé ïîëóãðóïïû, 20ÿçûêîâàÿäëÿ èñ÷èñëåíèÿ HDL, 64äëÿ èñ÷èñëåíèÿ L, 20ìóëüòèïëèêàòèâíàÿ öèêëè÷åñêàÿ ëèíåéíàÿ ëîãèêà, 410-îáðàç, 80q -îáðàç, 98îòíîøåíèå ñîâìåñòèìîñòèâ èñ÷èñëåíèè HDLk , 67â èñ÷èñëåíèè L, 22â èñ÷èñëåíèè MCLL, 43ïàð, 41ïåðåâîä, ñòàíäàðòíûé ïåðåâîä, 42<Γ -ïëàíàðíûé ãðàô, 46ïîäôîðìóëüíîñòü, 57112ïîäòèï, 17ïðàâèëüíàÿ ñêîáî÷íàÿ ïîñëåäîâàòåëüíîñòü, 99ïðàâîå äåëåíèå, 14îïåðàöèÿ íàä ÿçûêàìè, 19ïðåäñòàâëÿþùèé òèï, 85ïðåôèêñ, 19ïóñòîå ñëîâî, 18ðàçäåëèòåëü, 58ðàñïîçíàþùàÿ ïîñëåäîâàòåëüíîñòü, 94ñâîáîäíàÿ ïîëóãðóïïà, 19ñâîáîäíûé ìîíîèä, 19ñåêâåíöèÿèñ÷èñëåíèÿ DL, 87èñ÷èñëåíèÿ HDL, 60èñ÷èñëåíèÿ L, 14èñ÷èñëåíèÿ MCLL, 41T 0 -ñåêâåíöèÿ, 98ñå÷åíèå, 15ñëîâàðü, 92, 93ñëîâî, 18ñîâìåñòèìûå òèïû, 22ñîâìåùàþùàÿ ôîðìóëà, 43ñîâìåùàþùèé òèï, 22â èñ÷èñëåíèè HDLk , 66ñîâìåñòèìûå ôîðìóëû, 43ñîâìåñòèìûå òèïûâ èñ÷èñëåíèè HDLk , 66ñîåäèíÿþùèé òèï, 22ñîðò, 85ñëîâà, 58113òèïà èñ÷èñëåíèÿ HDL, 60ñóêöåäåíò, 15ñóôôèêñ, 19òåíçîð, 41òèïáàçîâûé, 60áåç îòðèöàòåëüíûõ óìíîæåíèé, 27áåç ïîëîæèòåëüíûõ óìíîæåíèé, 27èñ÷èñëåíèÿ HDL, 60èñ÷èñëåíèÿ L, 14íåïðåðûâíûé, 77ïðèâåä¼ííûé, 78ïðèìèòèâíûéâ èñ÷èñëåíèè HDL, 60â èñ÷èñëåíèè L, 14òîíêàÿïàðà ôîðìóë, 52ôîðìóëà, 51óìíîæåíèå, 14óïðîù¼ííàÿ ñåòü äîêàçàòåëüñòâà, 47ôîðìóëà, 41öåëåâîé òèï, 91ÿçûêôîðìàëüíûé, 181, 58A⊥ , 41[], ðàçäåëèòåëü, 84#, 87v, 19w, 19114↓jîïåðàöèÿ íàä ÿçûêàìè, 59ñâÿçêà èñ÷èñëåíèÿ DL, 60/îïåðàöèÿ íàä ÿçûêàìè, 19ñâÿçêà èñ÷èñëåíèÿ Ëàìáåêà, 14·îïåðàöèÿ íàä ÿçûêàìè, 19ñâÿçêà èñ÷èñëåíèÿ Ëàìáåêà, 146Γ , 46<Γ , 46jîïåðàöèÿ íàä ÿçûêàìè, 59ñâÿçêà èñ÷èñëåíèÿ HDL, 60⊗, 41îïåðàöèÿ çàìåíû, 86O, 41B, 91, 46→M , 94↑jîïåðàöèÿ íàä ÿçûêàìè, 59ñâÿçêà èñ÷èñëåíèÿ HDL, 60`, 15\îïåðàöèÿ íàä ÿçûêàìè, 19ñâÿçêà èñ÷èñëåíèÿ Ëàìáåêà, 14115Ëèòåðàòóðà[1] V.
M. Abrusci. Phase semantics and sequent calculus for pure noncommutative classical linear logic // Journal of Symbolic Logic. 1991. Vol. 56, No. 1. P. 1403-1451.[2] A. V. Aho, R. Sethi, J. D. Ullman. Compilers: principles, techniquesand tools. Reading, Mass. Addison-Wesley. 1985.Ðóññêèé ïåðåâîä: À. Â. Àõî, Ð.
Ñåòè, Äæ. Ä. Óëüìàí. Êîìïèëÿòîðû:ïðèíöèïû, òåõíîëîãèè è èíñòðóìåíòû. Ì.: ¾Âèëüÿìñ¿, 2001. 768c.[3] K. Ajdukiewicz. Die syntaktische Konnexitat // Studia philosophica. 1935. Vol. 3, No. 1. - P. 127.[4] W. Buszkowski. Compatibility of a categorial grammar with anassociated category system. // Zeitschrift fur mathematische Logik undGrundlagen der Mathematik. 1982. Vol 28.
P. 229238.[5] Y. Bar-Hillel, C. Gaifman, E. Shamir. On the categorial and phrasestructure grammars // Bulletin of the Research Council of Israel,Section F. 1960. Vol. 9F. P. 116.[6] N. Chomsky. Three models for the description of language // IRETransactions on Information Theory. 1956. Vol. I T-2, No. 3. P. 113124.Ðóññêèé ïåðåâîä: Í. Õîìñêèé.
Òðè ìîäåëè îïèñàíèÿ ÿçûêà // Êè-áåðíåòè÷åñêèé ñáîðíèê, âûï. 2. Ì.: ÈË, 1961. Ñ. 237266.[7] N. Chomsky. A note on phrase structure grammars // Information andcontrol. 1959. Vol. 2, No. 4. P. 393395.Ðóññêèé ïåðåâîä: Í. Õîìñêèé. Çàìåòêà î ãðàììàòèêàõ íåïîñðåä116ñòâåííî ñîñòàâëÿþùèõ // Êèáåðíåòè÷åñêèé ñáîðíèê, âûï. 5. Ì.:ÈË, 1962. Ñ. 312316.[8] N. Chomsky, M. P.
Schutzenberger. The algebraic theory of contextfree languages // Computer programming and formal systems / EditorsP. Braort and D. Hirschberg. Amsterdam: North-Holland, 1963. P. 118.Ðóññêèé ïåðåâîä: Í. Õîìñêèé. Àëãåáðàè÷åñêàÿ òåîðèÿ êîíòåêñòíîñâîáîäíûõ ÿçûêîâ. Êèáåðíåòè÷åñêèé ñáîðíèê, âûï. 3. Ì.: ÈË,1966. Ñ. 195242.[9] M. Dekhtyar, A. Dikovsky. Generalized categorial dependency grammars // Trakhtenbrot/Festschrift, Proceedings / Editors A. Avron etal. Berlin etc.: Springer, 2008.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
