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

[19]), à èìåííî, âûâîäèìîñòü ñåêâåíöèè A1 · . . . · Ar → B , ãäå r > 0, â èñ÷èñëåíèè HL1ðàâíîñèëüíà âûâîäèìîñòè ñåêâåíöèè A1 . . . Ar → B â èñ÷èñëåíèè L1 , àâûâîäèìîñòü ñåêâåíöèè → B â èñ÷èñëåíèè L1 ðàâíîñèëüíà âûâîäèìîñòèñåêâåíöèè I → B â èñ÷èñëåíèè HL1 .4.2Ðàçðûâíûå îïåðàöèè íàä ÿçûêàìè ëèíãâèñòè÷åñêèõ ïðèëîæåíèÿõ äîïîëíèòåëüíî ê îïåðàöèè êîíêàòåíàöèè óäîáíî ââåñòè òàê íàçûâàåìóþ îïåðàöèþ çàìåùåíèÿ, ïîçâîëÿþùóþîïåðèðîâàòü ðàçðûâíûìè ñèíòàêñè÷åñêèìè ñîñòàâëÿþùèìè. Ïóñòü 1 íåêîòîðûé âûäåëåííûé ýëåìåíò, íå ñîäåðæàùèéñÿ â ìíîæåñòâå Σ, êîòîðûé ìû áóäåì íàçûâàòü ðàçäåëèòåëåì . Îáîçíà÷èì Σ1 = Σ ∪ {1}.Äëÿ êàæäîãî ñëîâà w ∈ Σ∗1 îïðåäåëèì åãî ñîðò s(w), ðàâíûé |w|1 ,58òî åñòü ÷èñëó âõîæäåíèé ðàçäåëèòåëÿ â w.

Íà ìíîæåñòâå Σ1 äëÿ âñÿêîãî öåëîãî ïîëîæèòåëüíîãî j îïðåäåëèì ÷àñòè÷íóþ áèíàðíóþ îïåðàöèþ j -çàìåùåíèÿ j , ñîñòîÿùóþ â çàìåíå j -ãî ñëåâà ðàçäåëèòåëÿâ ïåðâîì àðãóìåíòå äàííîé îïåðàöèè íà å¼ âòîðîé àðãóìåíò.  ñëó÷àå åñëè ïåðâûé àðãóìåíò îïåðàöèè j ñîäåðæèò ìåíåå j ðàçäåëèòåëåé, ðåçóëüòàò å¼ ïðèìåíåíèÿ íå îïðåäåë¼í. Îïåðàöèÿ j -çàìåùåíèÿåñòåñòâåííûì îáðàçîì ïðîäîëæàåòñÿ íà ôîðìàëüíûå ÿçûêè ïî ïðàâèëóL1 j L2 = {w1 j w2 | w1 ∈ L1 , w2 ∈ L2 }.

Îïðåäåëèì òàêæå áèíàðíûåîïåðàöèè ↓j , ↑j , ïîëîæèâ L1 ↓j L2 = {w ∈ Σ∗1 | ∀w1 ∈ L1 (w1 j w ∈ L2 )},L1 ↑j L2 = {w ∈ Σ∗1 | ∀w2 ∈ L2 (w j w2 ∈ L1 )}.Ïðèìåð4.1.Ïóñòü L1 = {a1a, a1b}, L2 = {a}. Òîãäà L1 ↑1 L2 ={11a, 11b}, L1 ↑2 L2 = {a11}, L1 ↓1 L2 = ∅, L1 1 L2 = {aab, aaa}.Ñëåäóþùåå óòâåðæäåíèå âûòåêàåò èç îïðåäåëåíèÿ ñîîòâåòñòâóþùèõ îïåðàöèé.Ëåììà 4.1.Äëÿ âñÿêîãî j è ïðîèçâîëüíûõ ÿçûêîâ L1 , L2 , L ⊂ Σ∗1 ðàâ-íîñèëüíû óñëîâèÿ:1. L1 j L2 ⊆ L,2. L1 ⊆ L ↑j L2 ,3. L2 ⊆ L1 ↓j L.Òàêèì îáðàçîì, îïåðàöèè j , ↑j è ↓j äëÿ âñÿêîãî j ïðåäñòàâëÿþòñîáîé ðàçðûâíûé àíàëîã îïåðàöèé ·, /, \.4.3Èñ÷èñëåíèå Ëàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿÈñ÷èñëåíèå Ëàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿ ïîçâîëÿåò äîïîëíèòåëüíî ê ñòàíäàðòíûì îïåðàöèÿì ·, \, / ðàññìàòðèâàòü òàêæå è îïåðàöèèj , ↑j , ↓j äëÿ âñÿêîãî íàòóðàëüíîãî j .

 äàííîì ðàçäåëå ìû ðàññìîòðèì íåñåêâåíöèàëüíîå èñ÷èñëåíèå Ëàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿ,59ââåä¼ííîå Î. Âàëåíòèíîì â [32]. Îíî ýêâèâàëåíòíî ñåêâåíöèàëüíîìó èñ÷èñëåíèþ DL, âïåðâûå èçó÷àâøåìóñÿ â ðàáîòå [21], êîòîðîå áóäåò ðàññìàòðèâàòüñÿ â ãëàâå 6.Ïóñòü äàíî ñ÷¼òíîå ìíîæåñòâî ïðèìèòèâíûõ òèïîâ PrD , íà êîòîðîì çàäàíà ôóíêöèÿ ñîðòà s : PrD → N. Êðîìå òîãî, ïóñòü âûäåëåíûäâà ýëåìåíòà I, J ∈/ PrD .

Ìíîæåñòâî Base = PrD ∪ {I, J} áóäåì íàçûâàòü ìíîæåñòâîì áàçîâûõ òèïîâ, äîîïðåäåëèì ôóíêöèþ s : Base → N,ïîëîæèâ s(I) = 0 è s(J) = 1. Òèïû èñ÷èñëåíèÿ Ëàìáåêà ñ îïåðàöèÿìèçàìåùåíèÿ ñòðîÿòñÿ èç áàçîâûõ òèïîâ ñ ïîìîùüþ áèíàðíûõ ñâÿçîê \, /, ·,à òàêæå ñ÷¼òíîãî ñåìåéñòâà áèíàðíûõ ñâÿçîê ↑k , ↓k , k , ãäå k ∈ N, k > 1.Ïåðâûå òðè ñâÿçêè èìåþò òîò æå ñìûñë, ÷òî è â ñòàíäàðòíîì èñ÷èñëåíèè Ëàìáåêà, à êàæäàÿ èç òðîåê {k , ↑k , ↓k } ïðåäñòàâëÿåò ðàçðûâíûéàíàëîã òðîéêè {·, /, \}. Ìû áóäåì îáîçíà÷àòü òèïû áîëüøèìè ëàòèíñêèìè áóêâàìè A, B, . . ., âîçìîæíî ñ íèæíèìè èíäåêñàìè.

Ôîðìàëüíîìíîæåñòâî òèïîâ TpD çàäà¼òñÿ ñëåäóþùèì ðåêóðñèâíûì îïðåäåëåíèåì:1. Äëÿ âñåõ òèïîâ A, B ∈ TpD , òàêèõ ÷òî s(A) > s(B), òàêæå (A/B) ∈TpD , (B \ A) ∈ TpD , ïðè÷¼ì s(A/B) = s(B \ A) = s(A) − s(B).2. Äëÿ âñåõ òèïîâ A, B ∈ TpD òàêæå (A · B) ∈ TpD , ïðè÷¼ì s(A · B) =s(A) + s(B).3. Äëÿ âñåõ òèïîâ A, B ∈ TpD , òàêèõ ÷òî s(B) > 1 è s(A) > s(B) − 1,è âñåõ k 6 s(B) òàêæå B ↓k A ∈ TpD , ïðè÷¼ì s(B ↓k A) = s(A) −s(B) + 1.4. Äëÿ âñåõ òèïîâ A, B ∈ TpD , òàêèõ ÷òî s(A) > s(B), è âñåõk 6 s(A) − s(B) + 1 òàêæå (A ↑k B) ∈ TpD , ïðè÷¼ì s(A ↑k B) =s(A) − s(B) + 1.5.

Äëÿ âñåõ òèïîâ A, B ∈ TpD , òàêèõ ÷òî s(A) > 1, è âñåõ k 6 s(A)òàêæå (A k B) ∈ TpD , ïðè÷¼ì s(A k B) = s(A) + s(B) − 1.Ñåêâåíöèÿìè äàííîãî èñ÷èñëåíèÿ ÿâëÿþòñÿ âûðàæåíèÿ âèäàA → B , òàêèå ÷òî A, B ∈ T pD è s(A) = s(B), âûâîäèìîñòü ñåêâåíöèèA → B áóäåì îáîçíà÷àòü ÷åðåç HDL ` A → B . Àêñèîìû èñ÷èñëåíèÿ60HDL èìåþò âèä A → A, A ∈ TpD , íèæå ïðèâåäåíû ïðàâèëà âûâîäà äëÿñâÿçîê äàííîãî èñ÷èñëåíèÿ:A → C/BA·B →CA → C/BA·B →CB → A\CA·B →CB → A\CA·B →CA → C ↑j BA j B → CA j B → CA → C ↑j BB → A ↓j CA j B → CA j B → CB → A ↓j Cà òàêæå ñòðóêòóðíûå ïîñòóëàòû, âêëþ÷àþùèå â ñåáÿ àêñèîìû äëÿ êîíñòàíò (çàïèñü B ↔ C îçíà÷àåò, ÷òî îáå ñåêâåíöèè B → C è C → Bÿâëÿþòñÿ àêñèîìàìè èñ÷èñëåíèÿ HDL):A · I ↔ A ↔ I · A,J 1 A ↔ A ↔ A j J, åñëè j 6 s(A),àêñèîìû àññîöèàòèâíîñòè äëÿ ìóëüòèïëèêàòèâíûõ ñâÿçîê:(A · B) · C ↔ A · (B · C),(A i B) j C ↔ (A j C) i+s(B)−1 B, åñëè j < i,(A i B) j C ↔ A j (B j−i+1 C), åñëè i 6 j < i + s(B),(A i B) j C ↔ (A j+1−s(B) C) i B, åñëè i + s(B) 6 j,àêñèîìû âçàèìîäåéñòâèÿ ìåæäó ¾íåïðåðûâíûìè¿ è ¾ðàçðûâíûìè¿ñâÿçêàìè:A · B ↔ (A · J) s(A)+1 B ↔ (J · B) 1 Aè ïðàâèëî òðàíçèòèâíîñòè:A→BB→CA→CÄàëåå ìû áóäåì îïóñêàòü ñêîáêè â òèïàõ âèäà (A·B)·C , ïîëüçóÿñüàññîöèàòèâíîñòüþ ñâÿçêè ·, ïî òîé æå ïðè÷èíå áóäåì ïèñàòü A \ B/Câìåñòî (A \ B)/C è A \(B/C).61Ïðèìåð 4.2.Ïóñòü s(A) = s(B) = 1, òîãäà ñåêâåíöèÿ (A ↑1 B) ↓1 A →A/(B \ A) âûâîäèìà â èñ÷èñëåíèè HDL.

Ñîîòâåòñòâóþùèé âûâîä ïðèâåäåí íèæå.B \A → B \AB · (B \ A) → A(J · (B \ A)) 1 B → A (A ↑1 B) ↓1 A → (A ↑1 B) ↓1 AJ · (B \ A) → A ↑1 BA ↑1 B → A ↑1 ((A ↑1 B) ↓1 A)J · (B \ A) → A ↑1 ((A ↑1 B) ↓1 A)(J · (B \ A)) 1 ((A ↑1 B) ↓1 A) → A((A ↑1 B) ↓1 A) · (B \ A) → A(A ↑1 B) ↓1 A → A/(B \ A)Ñôîðìóëèðóåì íåñêîëüêî ïðàâèë, êîòîðûå ÿâëÿþòñÿ äîïóñòèìûìè â èñ÷èñëåíèè HDL è õàðàêòåðèçóþò ìîíîòîííîñòü ñâÿçîê äàííîãîèñ÷èñëåíèÿ. Äîïóñòèìîñòü äàííûõ ïðàâèë ëåãêî ïðîâåðèòü íåïîñðåäñòâåííî, îñíîâûâàÿñü íà àêñèîìå òðàíçèòèâíîñòè.Ëåììà 4.2.Ïóñòü ñîðòà òèïîâ A1 , B1 , A2 , B2 òàêîâû, ÷òî âñå òèïû,âõîäÿùèå â ïðàâèëà, êîððåêòíî îïðåäåëåíû.

Òîãäà ñëåäóþùèå ïðàâèëàÿâëÿþòñÿ äîïóñòèìûìè â èñ÷èñëåíèè HDL:A1 → A2 B1 → B2A1 · B1 → A2 · B2A1 → A2 B1 → B2A1 j B1 → A2 j B2A1 → A2 B1 → B2A1 /B2 → A2 /B1A1 → A2 B1 → B2B2 \ A1 → B1 \ A2A1 → A2 B1 → B2A1 ↑j B2 → A2 ↑j B1A1 → A2 B1 → B2B2 ↓j A1 → B1 ↓j A2 .Ñëåäñòâèå 4.1.Ïóñòü òèïû A è B ðàâíîñèëüíû â èñ÷èñëåíèè HDL,òîãäà çàìåíà íåêîòîðûõ âõîæäåíèé òèïà A íà òèï B íå âëèÿåò íà âûâîäèìîñòü ñåêâåíöèè.Çàìåòèì, ÷òî åñëè ðàññìàòðèâàòü òîëüêî ñåêâåíöèè ñ òèïàìè, ñîäåðæàùèìè ñâÿçêè \, /, · è êîíñòàíòó I , òî ìû ïîëó÷èì íåñåêâåíöèàëüíóþ àêñèîìàòèêó äëÿ èñ÷èñëåíèÿ L1 .

Òàêèì îáðàçîì, âñÿêàÿ ñåêâåíöèÿ,62âûâîäèìàÿ â L1 , áóäåò âûâîäèìà è â HDL. Áîëåå òîãî, åñëè ñåêâåíöèÿèñ÷èñëåíèÿ L1 îêàæåòñÿ âûâîäèìîé â èñ÷èñëåíèè HDL, òî îíà áóäåò âûâîäèìà è â ñàìîì èñ÷èñëåíèè L1 , òî åñòü èñ÷èñëåíèå HDL êîíñåðâàòèâíîíàä L1 . Äàííîå ñâîéñòâî âûòåêàåò èç ñâîéñòâà ïîäôîðìóëüíîñòè ýêâèâàëåíòíîãî ñåêâåíöèàëüíîãî èñ÷èñëåíèÿ DL, èçó÷àåìîãî â ãëàâå 6. Ïîýòîé æå ïðè÷èíå ìîæíî ñ÷èòàòü, ÷òî â âûâîäå ñåêâåíöèè âñòðå÷àþòñÿòîëüêî òå ïðèìèòèâíûå òèïû, êîòîðûå âõîäÿò â ñàìó ñåêâåíöèþ.Îáîçíà÷èì ÷åðåç Tpk ìíîæåñòâî òèïîâ, ïîëó÷àþùååñÿ ïðè îãðàíè÷åíèè ìàêñèìàëüíîãî ñîðòà òèïîâ ÷èñëîì k .

Åñëè çàïðåòèòü â âûâîäàõ ñåêâåíöèé òèïû íå èç Tpk , òî ïîëó÷èòñÿ èñ÷èñëåíèå HDLk . Êàêè èñ÷èñëåíèå HDL, âñå èñ÷èñëåíèÿ HDLk ÿâëÿþòñÿ êîíñåðâàòèâíûìèðàñøèðåíèÿìè èñ÷èñëåíèÿ L1 .Äîêàæåì âàæíóþ ñòðóêòóðíóþ ëåììó, ïîêàçûâàþùóþ âçàèìîñâÿçü ìåæäó îïåðàöèÿìè · è j .Ëåììà 4.3.Ïóñòü òèïû A, B, C ∈ Tpk òàêîâû, ÷òî A · B ∈ Tpk ès(A) + s(B) + s(C) 6 k + 1, òîãäà âåðíû ñëåäóþùèå óòâåðæäåíèÿ:1. Åñëè j 6 s(A), òî (A · B) j C ↔ (A j C) · B .2.

Åñëè s(A) < j 6 s(A) + s(B), òî (A · B) j C ↔ A · (B j−s(A) C).Äîêàçàòåëüñòâî. Äîêàæåì ïåðâîå óòâåðæäåíèå, âòîðîå äîêàçûâàåòñÿàíàëîãè÷íî. Èç óñëîâèé ëåììû ñëåäóåò, ÷òî òèïû (A·B)j C è (Aj C)·Bêîððåêòíû è ïðèíàäëåæàò Tpk . Òîãäà â ñèëó àêñèîì àññîöèàòèâíîñòè,àêñèîìû äëÿ êîíñòàíòû J , à òàêæå ñëåäñòâèÿ 4.1 èìååì (A · B) j C ↔((J ·B)1 A)j C ↔ (J ·B)1 (Aj C) ↔ (Aj C)·B , ÷òî è òðåáîâàëîñü.Çàìåòèì, ÷òî èç óñëîâèÿ j 6 s(A) âûòåêàåò, ÷òî s(J · B) 6 s(A · B) 6 kè ïîýòîìó J · B ∈ Tpk , à òàêæå ÷òî (J · B) 1 A ∈ Tpk . Òàêèì îáðàçîì,äàííûé âûâîä íà ñàìîì äåëå ÿâëÿåòñÿ âûâîäîì íå òîëüêî â èñ÷èñëåíèèHDL, íî è â èñ÷èñëåíèè HDLk , ÷åì ìû áóäåì ïîëüçîâàòüñÿ â äàëüíåéøåì.634.4Ìîäåëè èñ÷èñëåíèÿ Ëàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿÅñëè òèïû ñòàíäàðòíîãî èñ÷èñëåíèÿ Ëàìáåêà èíòåðïðåòèðóþòñÿ êàêìíîæåñòâà ñëîâ íàä íåêîòîðûì àëôàâèòîì Σ, à ñâÿçêè ·, \ è / êàê ñîîòâåòñòâóþùèå îïåðàöèè íàä ôîðìàëüíûìè ÿçûêàìè, òî òèïû èñ÷èñëåíèÿËàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿ ìîæíî èíòåðïðåòèðîâàòü êàê ìíîæåñòâà ñëîâ íàä ðàñøèðåííûì àëôàâèòîì Σ1 = Σ ∪ {1}, ãäå 1 âûäåëåííûé ðàçäåëèòåëü (ñì.

ðàçäåë 4.2). Ïîíÿòèå ÿçûêîâîé ìîäåëè äëÿ èñ÷èñëåíèÿ HDL ââîäèòñÿ àíàëîãè÷íî òîìó, êàê ýòî áûëî ñäåëàíî â ðàçäåëå1.4 äëÿ èñ÷èñëåíèé L è L∗ . À èìåííî, ÿçûêîâîé ìîäåëüþ áóäåì íàçûâàòüïàðó M = hΣ, Inti, ãäå Σ êîíå÷íûé àëôàâèò, à Int : TpD → P(Σ∗1 ) îòîáðàæåíèå, óäîâëåòâîðÿþùåå ñëåäóþùèì óñëîâèÿì:1. Int(p) ⊆ {w ∈ Σ∗1 | |w|1 = s(p)}, åñëè p ∈ PrD .2. Int(I) = {ε}.3. Int(J) = {1}.4.

Int(A ? B) = (Int(A) ? Int(B)) ∩ {w ∈ Σ∗1 | |w|1 = s(A ? B)} äëÿïðîèçâîëüíîé áèíàðíîé ñâÿçêè ? èñ÷èñëåíèÿ HDL. Ïðè ýòîì ïðåäïîëàãàåòñÿ, ÷òî òèï A ? B îïðåäåë¼í.Ïðèìåð 4.3.Ïóñòü s(A) = 1, s(B) = 0, Int(A) = {a1a, a1b}, Int(B) ={a}.  ýòîì ñëó÷àå Int(A · B) = {a1aa, a1ba}, Int(A/B) = {a1},Int(B \ A) = {1b, 1a}, Int(A↑1 B) = {11b, 11a}, Int(A↑2 B) = {a11},Int(A ↓1 B) = ∅, Int(A 1 B) = {aab, aaa}.Ïðèìåð 4.4.Ïóñòü Σ = {a, b}, s(A) = s(B) = 0, Int(A) = {b}, Int(B) ={a}.  ýòîì ñëó÷àå Int(A/B) = ∅, òîãäà s(A ↑1 (A/B)) = 1 è ïî îïðåäåëåíèþ Int(A ↑1 (A/B)) = {w ∈ Σ∗1 | s(w) = 1} = {u1v | u, v ∈ Σ∗ }.Èíäóêöèåé ïî ïîñòðîåíèþ òèïà ëåãêî äîêàçàòü, ÷òî ìíîæåñòâîInt(A) ñîäåðæèò òîëüêî ñëîâà ñîðòà s(A).

Óñëîâèå íà ñîðòà ñëîâ â ïîñëåäíåì ïóíêòå îïðåäåëåíèÿ ÿçûêîâîé ìîäåëè íåîáõîäèìî, ÷òîáû ðåçóëüòàò äåëåíèÿ íà ïóñòîå ìíîæåñòâî ñîäåðæàë ñëîâà ëèøü òðåáóåìîãî64ñîðòà. Ñåêâåíöèþ A → B áóäåì íàçûâàòü èñòèííîé â ìîäåëè M , åñëèâåðíî âêëþ÷åíèå Int(A) ⊆ Int(B).Èíäóêöèåé ïî äëèíå âûâîäà â èñ÷èñëåíèè HDL ëåãêî äîêàçàòü,÷òî âñÿêàÿ âûâîäèìàÿ â í¼ì ñåêâåíöèÿ áóäåò èñòèííà â ëþáîé ìîäåëè.Îòìåòèì, ÷òî îáðàòíîå óòâåðæäåíèå íåâåðíî, òî åñòü èñ÷èñëåíèå HDLíåïîëíî. Ýòî ñëåäóåò èç íåïîëíîòû èñ÷èñëåíèÿ L1 , â êîòîðîì íåâûâîäèìà ñåêâåíöèÿ (I/A)BA → B , èñòèííàÿ âî âñåõ ìîäåëÿõ, à òàêæå èçíåâûâîäèìîñòè ñåêâåíöèè I ↑1 I → J (ñì. [32]).  òî æå âðåìÿ â ðàáîòå[32] äîêàçàíî, ÷òî äëÿ ñåêâåíöèé, ñîäåðæàùèõ òîëüêî ñâÿçêè \, /, ↑j è↓j è íå ñîäåðæàùèõ êîíñòàíò, âûâîäèìîñòü ýêâèâàëåíòíà èñòèííîñòè âîâñåõ ÿçûêîâûõ ìîäåëÿõ.  ýòîé æå ðàáîòå äîêàçàíà ïîëíîòà äëÿ íåêîòîðîãî áîëåå øèðîêîãî ôðàãìåíòà áåç ñâÿçîê · è j è ñ îãðàíè÷åíèÿìè íàâõîæäåíèÿ êîíñòàíò.