Об отношении совместимости в исчислении Ламбека и в его варианте с операциями замещения (1104173), страница 3
Текст из файла (страница 3)
Òîãäà ìíîæåñòâî òèïîâ ñòðîèòñÿ íà îñíîâå ìíîæåñòâà ïðèìèòèâíûõ òèïîâ ñ ïîìîùüþ ñâÿçîê \ (ëåâîå äåëåíèå), / (ïðàâîå äåëåíèå) è · (óìíîæåíèå). Ôîðìàëüíî, ìíîæåñòâî Tp òèïîâ èñ÷èñëåíèÿ Ëàìáåêà åñòü íàèìåíüøåå ìíîæåñòâî, óäîâëåòâîðÿþùåå ñëåäóþùèìóñëîâèÿì:1. Pr ⊂ Tp;2. åñëè A, B ∈ Tp, òî (A \ B), (B/A), (A · B) ∈ Tp.Ìû áóäåì îáîçíà÷àòü ïðèìèòèâíûå òèïû ìàëûìè ëàòèíñêèìèáóêâàìè p, q, r, âîçìîæíî ñ íèæíèìè èíäåêñàìè.
Äëÿ òèïîâ èñ÷èñëåíèÿËàìáåêà ìû áóäåì ïðèìåíÿòü áîëüøèå ëàòèíñêèå áóêâû A, B, C, . . .. Êîíå÷íûå ïîñëåäîâàòåëüíîñòè òèïîâ îáîçíà÷àþòñÿ áîëüøèìè ãðå÷åñêèìèáóêâàìè. Ïðè çàïèñè ïîñëåäîâàòåëüíîñòè å¼ ýëåìåíòû íå ðàçäåëÿþòñÿçàïÿòûìè.Âûâîäèìûìè îáúåêòàìè èñ÷èñëåíèÿ L ÿâëÿþòñÿ ñåêâåíöèè , èìåþùèå âèä Γ → A, ãäå Γ ÿâëÿåòñÿ íåïóñòîé ïîñëåäîâàòåëüíîñòüþ òèïîâ,à A ÿâëÿåòñÿ òèïîì. Ïîñëåäîâàòåëüíîñòü Γ èìåíóåòñÿ àíòåöåäåíòîì , à14òèï A ñóêöåäåíòîì ñåêâåíöèè. Îòìåòèì, ÷òî â èñ÷èñëåíèè L çàïðåùåíû ïóñòûå àíòåöåäåíòû.Èñ÷èñëåíèå Ëàìáåêà çàäà¼òñÿ åäèíñòâåííîé àêñèîìîé A → A, A ∈Tp, è ïðàâèëàìè âûâîäà, ïðèâåä¼ííûìè íèæå.ΠA → BΓB∆ → C Π → A(→ /)(/ →)Π → B/AΓ(B/A)Π∆ → CΓB∆ → C Π → AAΠ → B(→ \)(\ →)Π → A\BΓΠ(A \ B)∆ → CΓ→A ∆→BΓAB∆ → C(→ ·)(· →)Γ∆ → A · BΓ(A · B)∆ → CÏðèìåð 1.1.
Ñåêâåíöèÿ (p/q)r → p/(r \ q) ÿâëÿåòñÿ âûâîäèìîé â èñ÷èñëåíèè L. ż âûâîä ïðèâåä¼í íèæå.p→pq→q(p/q)q → p(/ →)(p/q)r(r \ q) → p(p/q)r → p/(r \ q)r→r(\ →)(→ /)Âûâîäèìîñòü ñåêâåíöèè Γ → A îáîçíà÷àåòñÿ L ` Γ → A. Îòìåòèì, ÷òî ïðîáëåìà âûâîäèìîñòè ñåêâåíöèè ÿâëÿåòñÿ ðàçðåøèìîé, ïîñêîëüêó ïðèìåíåíèå êàæäîãî èç ïðàâèë âûâîäà ¾ñíèçó ââåðõ¿ ïðèâîäèòê óìåíüøåíèþ ñóììû ÷èñëà âõîæäåíèé ïðèìèòèâíûõ òèïîâ è ñâÿçîê âñåêâåíöèè.Ïðàâèëî íàçûâàåòñÿ äîïóñòèìûì, åñëè åãî äîáàâëåíèå ê ïðàâèëàì âûâîäà èñ÷èñëåíèÿ Ëàìáåêà íå óâåëè÷èâàåò ìíîæåñòâî âûâîäèìûõñåêâåíöèé.
Êàê äîêàçàíî â [18], äîïóñòèìûì ÿâëÿåòñÿ ïðàâèëî ñå÷åíèÿΠ → B ΓB∆ → C, òî åñòü èñ÷èñëåíèå Ëàìáåêà îáëàäàåò ñâîéñòâîìΓΠ∆ → Cóñòðàíèìîñòè ñå÷åíèÿ, êîòîðîå õàðàêòåðíî äëÿ áîëüøèíñòâà ñåêâåíöèàëüíûõ èñ÷èñëåíèé.  äàëüíåéøåì ìû áóäåì ñ÷èòàòü, ÷òî ïðàâèëî ñå÷åíèÿ ÿâíî âêëþ÷åíî â àêñèîìàòèêó èñ÷èñëåíèÿ Ëàìáåêà.Äâà òèïà B, C ∈ Tp íàçûâàþòñÿ ðàâíîñèëüíûìè, åñëè îáå ñåêâåíöèè B → C è C → B ÿâëÿþòñÿ âûâîäèìûìè â èñ÷èñëåíèè L. Ëåãêîïîêàçàòü, ÷òî îòíîøåíèå ðàâíîñèëüíîñòè ÿâëÿåòñÿ êîíãðóýíöèåé îòíîñèòåëüíî ñâÿçîê /, \, ·, òî åñòü èç ðàâíîñèëüíîñòè òèïîâ A1 è A2 , à òàêæå15B1 è B2 ñëåäóåò ðàâíîñèëüíîñòü òèïîâ A1 ? B1 è A2 ? B2 äëÿ ïðîèçâîëüíîé ñâÿçêè ? ∈ {\, /, ·}. Äëÿ îáîçíà÷åíèÿ ðàâíîñèëüíîñòè èñïîëüçóåòñÿçíà÷îê ↔ ñ èíäåêñîì L, ñîîòâåòñòâóþùèì èñ÷èñëåíèþ.
Íèæå ïðèâåäåíû ïðèìåðû ðàâíîñèëüíûõ òèïîâ, ïîçâîëÿþùèå íàì íå èñïîëüçîâàòüñêîáêè â âûðàæåíèÿõ âèäà A · B · C è B \ A/C .Ëåììà 1.1.1. Äëÿ ëþáûõ òèïîâ A, B, C ∈ Tp âåðíî, ÷òî (A · B) · C ↔L A · (B · C).2. Äëÿ ëþáûõ òèïîâ A, B, C ∈ Tp âåðíî, ÷òî (B\ A)/C ↔L B \(A/C).Ïðèâåä¼ííàÿ íèæå ëåììà ïðèíàäëåæèò ìàòåìàòè÷åñêîìó ôîëüêëîðó è ëåãêî ñëåäóåò èç óñòðàíèìîñòè ñå÷åíèÿ â èñ÷èñëåíèè Ëàìáåêà:Ëåììà 1.2.Ïðàâèëà (· →), (→ /) è (→ \) îáðàòèìû, ò.å.:1.
Åñëè L ` Γ(A · B)∆ → C , òî L ` ΓAB∆ → C .2. Åñëè L ` Π → A/B , òî L ` ΠB → A.3. Åñëè L ` Π → B \ A, òî L ` BΠ → A.Íà îñíîâàíèè äàííîé ëåììû ìû áóäåì ñ÷èòàòü, ÷òî åñëè â àíòåöåäåíò ñåêâåíöèè âõîäèò òèï âèäà A · B , òî ïîñëåäíèì â âûâîäå ïðèìåíÿëîñü ïðàâèëî (· →), ââîäèâøåå ñâÿçêó · â ñàìîì ïðàâîìèç òèïîâ ïîäîáíîãî âèäà. Åñëè æå â àíòåöåäåíòå îòñóòñòâóåò òèï âèäà A · B , íî ñóêöåäåíò èìååò âèä A/B (èëè B \ A), òî ïîñëåäíèìïðèìåíÿëîñü ïðàâèëî (→ /) ((→ \), ñîîòâåòñòâåííî). Òàêæå èç ïðèâåä¼ííîé ëåììû âûòåêàåò, ÷òî ñåêâåíöèè A · B → C, A → C/B,B → A \ C ëèáî îäíîâðåìåííî âûâîäèìû, ëèáî îäíîâðåìåííî íåâûâîäèìû.Íàçîâ¼ì äëèíîé òèïà A ñóììàðíîå ÷èñëî âõîäÿùèõ â íåãî ïðèìèòèâíûõ òèïîâ; äëèíó òèïà A áóäåì îáîçíà÷àòü ÷åðåç l(A).
Îïðåäåëèìòàêæå âåëè÷èíó kAk, ðàâíóþ ñóììàðíîìó ÷èñëó âõîæäåíèé ïðèìèòèâíûõ òèïîâ è ñâÿçîê â òèï A, ëåãêî âèäåòü, ÷òî kAk = 2l(A) − 1. Ââåä¼ííûå âåëè÷èíû çàäàþòñÿ ñëåäóþùèì èíäóêòèâíûì îïðåäåëåíèåì:1. l(p) = kpk = 1, åñëè p ∈ Pr,162. l(A ∗ B) = l(A) + l(B), kA ∗ Bk = kAk + kBk + 1, åñëè ∗ ∈ {·, \, /}Îïðåäåëèì ôîðìàëüíî îòíîøåíèå ¾áûòü ïîäòèïîì¿ è ïîíÿòèåâõîæäåíèÿ ïîäòèïà B â òèï A.Ìíîæåñòâî SubTp(A) ïîäòèïîâ òèïà A çàäà¼òñÿÎïðåäåëåíèå 1.1.ñëåäóþùèì èíäóêòèâíûì îïðåäåëåíèåì:1. SubTp(p) = {p}, åñëè p ∈ Pr,2. SubTp(A ∗ B) = SubTp(A) ∪ SubTp(B) ∪ {A ∗ B}, åñëè ∗ ∈ {·, \, /}.Äëÿ âñÿêîãî ïîäòèïà B ∈ SubTp(A) âõîæäåíèå ïîäòèïà B âòèï A ïðåäñòàâëÿåò ñîáîé ïàðó hB, ii, ãäå i íåêîòîðîå íàòóðàëüíîå÷èñëî îò 0 äî kAk − 1. Âõîæäåíèÿ ïîäòèïîâ äåëÿòñÿ íà ïîëîæèòåëüíûåè îòðèöàòåëüíûå. Ìíîæåñòâî ïîëîæèòåëüíûõ âõîæäåíèé îáîçíà÷àåòñÿ÷åðåç Subocc+ (A), à ìíîæåñòâî îòðèöàòåëüíûõ ÷åðåç Subocc− (A).Îïðåäåëåíèå 1.2.Ìíîæåñòâà Subocc+ (A) è Subocc− (A) îïðåäåëÿþòñÿñëåäóþùèì îáðàçîì.1.
Subocc+ (p) = {hp, 0i}, Subocc− (p) = ∅, åñëè p ∈ Pr,2. Subocc+ (C·B) = Subocc+ (C)∪{hD, kCk+ii | hD, ii ∈ Subocc+ (B)}∪{hC · B, kCki},Subocc− (C ·B) = Subocc− (C)∪{hD, kCk+ii | hD, ii ∈ Subocc− (B)},3. Subocc+ (C/B) = Subocc+ (C)∪{hD, kCk+ii | hD, ii ∈ Subocc− (B)}∪{hC/B, kCki},Subocc− (C/B) = Subocc− (C)∪{hD, kCk+ii | hD, ii ∈ Subocc+ (B)},4.
Subocc+ (C \ B) = Subocc− (C)∪{hD, kCk + ii | hD, ii ∈ Subocc+ (B)}∪{hC \ B, kCki},Subocc− (C \ B) = Subocc+ (C)∪{hD, kCk+ii | hD, ii ∈ Subocc− (B)}.Ìíîæåñòâî âñåõ âõîæäåíèé áóäåì îáîçíà÷àòü ÷åðåç Subocc(A),Subocc(A) = Subocc+ (A) ∪ Subocc− (A). Ïî èíäóêöèè ëåãêî äîêàçûâàåòñÿ, ÷òî |Subocc(A)| = kAk. Ìíîæåñòâî Occ+ (A) âõîæäåíèé ïðèìèòèâ-íûõ òèïîâ â òèï A îïðåäåëÿåòñÿ êàê Occ(A) = {hp, ii ∈ Subocc(A) | p ∈Pr}. ×åðåç Occ+ (A) è Occ− (A) îáîçíà÷àþòñÿ, ñîîòâåòñòâåííî, ìíîæåñòâà ïîëîæèòåëüíûõ è îòðèöàòåëüíûõ âõîæäåíèé ïðèìèòèâíûõ òèïîâ.17Ïðèìåð 1.2.Ïóñòü A = ((p/(r \ q)) · q)/(r/p), òîãäà Occ+ (A) = {hp, 0i,hr, 2i, hq, 6i, hp, 10i}, Occ− (A) = {hq, 4i, hr, 8i}, Subocc+ (A) = Occ+ (A) ∪{h((p/(r \ q)) · q)/(r/p), 7i, h(p/(r \ q)) · q, 5i, hp/(r \ q), 1i}, Subocc− (A) =Occ− (A) ∪ {h(r \ q), 3i, hr/p, 9i}.1.2Èñ÷èñëåíèåL∗ ñëó÷àå åñëè â îïðåäåëåíèè ñåêâåíöèè èñ÷èñëåíèÿ L óáðàòü óñëîâèåíåïóñòîòû àíòåöåäåíòà, íå ìåíÿÿ ïðè ýòîì àêñèîìàòèêè, ìû ïîëó÷èì èñ÷èñëåíèå L∗ , íàçûâàåìîå èñ÷èñëåíèåì Ëàìáåêà, äîïóñêàþùèì ïóñòûåàíòåöåäåíòû .
 ýòîì èñ÷èñëåíèè âûâîäèìû íåêîòîðûå ñåêâåíöèè ñíåïóñòûìè àíòåöåäåíòàìè, íåâûâîäèìûå â èñ÷èñëåíèè L. Íàïðèìåð, íèæå ïðèâåä¼í âûâîä ñåêâåíöèè p/(q/q) → p â èñ÷èñëåíèè L∗ , â òî âðåìÿêàê â èñ÷èñëåíèè L äàííàÿ ñåêâåíöèÿ íåâûâîäèìà.q→qp→p→ q/qp/(q/q) → p(→ /)(/ →)Òàê æå, êàê è â èñ÷èñëåíèè L, â L∗ äîïóñòèìî ïðàâèëî ñå÷åíèÿ.Êðîìå òîãî, äëÿ íåãî âåðíû ëåììà 1.2 è äðóãèå óòâåðæäåíèÿ äîêàçàííûåâ ðàçäåëå 1.1 äëÿ èñ÷èñëåíèÿ L.1.3Ôîðìàëüíûå ÿçûêè è îïåðàöèè íàä íèìèÀëôàâèòîì áóäåì íàçûâàòü ïðîèçâîëüíîå íå áîëåå ÷åì ñ÷¼òíîå ìíîæåñòâî Σ; ÷àùå âñåãî îíî áóäåò êîíå÷íûì. Ýëåìåíòû àëôàâèòà áóäåìíàçûâàòü áóêâàìè , à êîíå÷íûå ïîñëåäîâàòåëüíîñòè áóêâ, â òîì ÷èñëå èïóñòóþ ïîñëåäîâàòåëüíîñòü, ñëîâàìè .
Ìíîæåñòâî âñåõ ñëîâ íàä àëôàâèòîì Σ îáîçíà÷àåòñÿ Σ∗ , ìíîæåñòâî âñåõ íåïóñòûõ ñëîâ Σ+ , ïóñòîåñëîâî áóäåì îáîçíà÷àòü ÷åðåç ε. Ïîäìíîæåñòâà ìíîæåñòâà Σ∗ áóäåì íàçûâàòü ôîðìàëüíûìè ÿçûêàìè . Åñëè w ∈ Σ∗ ñëîâî, òî åãî äëèíóáóäåì îáîçíà÷àòü ÷åðåç |w|, à êîëè÷åñòâî áóêâ a â ñëîâå w ÷åðåç |w|a .18Åñëè w ïðåäñòàâèìî â âèäå w = uv , òî u áóäåì íàçûâàòü ïðåôèêñîìñëîâà w, à v ñóôôèêñîì , èñïîëüçóÿ îáîçíà÷åíèÿ u v w è v w w.Íà ìíîæåñòâå ñëîâ îïðåäåëèì îïåðàöèþ êîíêàòåíàöèè w1 · w2 ,ñîñòîÿùóþ â ïðèïèñûâàíèè w2 ê w1 ñçàäè (íàïðèìåð, ab · acb = abacb).Ìíîæåñòâà Σ+ è Σ∗ ñ îïðåäåë¼ííîé íà íèõ îïåðàöèåé êîíêàòåíàöèè íàçûâàþòñÿ, ñîîòâåòñòâåííî, ñâîáîäíîé ïîëóãðóïïîé è ñâîáîäíûì ìîíî-èäîì, ïîðîæä¼ííûìè ìíîæåñòâîì Σ.
.  äàëüíåéøåì ìû áóäåì ÷àñòîîïóñêàòü ñèìâîë ·. Ââåä¼ííàÿ îïåðàöèÿ ëåãêî ïðîäîëæàåòñÿ ñî ñëîâ íàìíîæåñòâà ñëîâ (òî åñòü íà ôîðìàëüíûå ÿçûêè): L1 · L2 = {w1 w2 | w1 ∈L1 , w2 ∈ L2 }.Ââåä¼ì íà ïîäìíîæåñòâàõ ìíîæåñòâà Σ+ îïåðàöèè ëåâîãî è ïðà-âîãî äåëåíèÿ : L1 \ L2 = {w ∈ Σ+ | ∀w1 ∈ L1 (w1 w ∈ L2 )}, L1 /L2 = {w ∈Σ+ | ∀w2 ∈ L2 (ww2 ∈ L1 )}.Ïðèìåð1.3.L1 · L2=Ïóñòü L1 = {ab, bb, aab, abb, aaab}, L2 = {b, ab}, òîãäà{abb, bbb, aabb, abbb, aaabb, abab, bbab, aabab, abbab, aaabab},L1 /L2 = {a, aa}, L2 \ L1 = {b}.Ñëåäóþùàÿ ëåììà ñëåäóåò èç îïðåäåëåíèÿ îïåðàöèé ·, / è \:Ëåììà1.3.Äëÿ ëþáûõ ïîäìíîæåñòâ L, L1 , L2 ⊆ Σ+ ñëåäóþùèåóòâåðæäåíèÿ ðàâíîñèëüíû:1.
L1 · L2 ⊆ L,2. L1 ⊆ L/L2 ,3. L2 ⊆ L1 \ L.Îïåðàöèè ëåâîãî è ïðàâîãî äåëåíèÿ ìîæíî îïðåäåëèòü è íà ïîäìíîæåñòâàõ ìíîæåñòâà Σ∗ , ïîëîæèâ L1 \ L2 = {w ∈ Σ∗ | ∀w1 ∈L1 (w1 w ∈ L2 )}, L1 /L2 = {w ∈ Σ∗ | ∀w2 ∈ L2 (ww2 ∈ L1 )}. Îòìåòèì, ÷òî ðåçóëüòàò ïðèìåíåíèÿ ýòèõ îïåðàöèé ìîæåò áûòü ðàçëè÷íûìâ çàâèñèìîñòè îò òîãî, ðàññìàòðèâàþòñÿ ëè ÿçûêè L1 è L2 êàê ïîäìíîæåñòâà ñâîáîäíîé ïîëóãðóïïû Σ+ èëè æå êàê ïîäìíîæåñòâà ñâîáîäíîãîìîíîèäà Σ∗ .19Ïðèìåð 1.4.Ïóñòü L = {a, ba}, òîãäà L/L = ∅, åñëè ðàññìàòðèâàòü Lêàê ïîäìíîæåñòâî ìíîæåñòâà Σ+ , è L/L = {ε}, åñëè ðàññìàòðèâàòü Lêàê ïîäìíîæåñòâî ìíîæåñòâà Σ∗ .Ëåììà1.4.Äëÿ ëþáûõ ïîäìíîæåñòâ L, L1 , L2 ⊆ Σ∗ ñëåäóþùèåóòâåðæäåíèÿ ðàâíîñèëüíû:1.
L1 · L2 ⊆ L,2. L1 ⊆ L/L2 ,3. L2 ⊆ L1 \ L.1.4Ìîäåëè èñ÷èñëåíèÿ ËàìáåêàÅñòåñòâåííîé ñåìàíòèêîé äëÿ òèïîâ èñ÷èñëåíèÿ L âûñòóïàþò ïîäìíîæåñòâà ñâîáîäíîé ïîëóãðóïïû Σ+ , à äëÿ òèïîâ èñ÷èñëåíèÿ L∗ ïîäìíîæåñòâà ñâîáîäíîãî ìîíîèäà Σ∗ . Ïðè ýòîì ñâÿçêè \, /, · èíòåðïðåòèðóþòñÿêàê ñîîòâåòñòâóþùèå îïåðàöèè íàä ôîðìàëüíûìè ÿçûêàìè.  ñëåäóþùåì îïðåäåëåíèè è â äàëüíåéøåì ÷åðåç P(A) îáîçíà÷åíî ìíîæåñòâîâñåõ ïîäìíîæåñòâ ìíîæåñòâà A..Îïðåäåëåíèå 1.3.Ìîäåëüþ íà ïîäìíîæåñòâàõ ñâîáîäíîé ïîëóãðóï-ïû èëè ÿçûêîâîé ìîäåëüþ íàçûâàåòñÿ ïàðà M = hΣ, Inti, ãäå Σ àëôàâèò, à Int : Tp → P(Σ+ ) îòîáðàæåíèå, óäîâëåòâîðÿþùåå óñëîâèþInt(A ? B) = Int(A) ? Int(B) äëÿ ïðîèçâîëüíîé ñâÿçêè ? ∈ {\, /, ·} èïðîèçâîëüíûõ òèïîâ A è B èñ÷èñëåíèÿ L.Çàìåòèì, ÷òî îòîáðàæåíèå Int äîñòàòî÷íî îïðåäåëèòü íà ïðèìèòèâíûõ òèïàõ, äàëüøå îíî îäíîçíà÷íî äîñòðàèâàåòñÿ ïî èíäóêöèè.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
