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

Ôîðìóëû ëèíåéíîé ëîãèêèñòðîÿòñÿ èç àòîìîâ ñ ïîìîùüþ áèíàðíûõ ñâÿçîê O (ïàð èëè ìóëüòèïëèêàòèâíàÿ äèçúþíêöèÿ) è ⊗ (òåíçîð èëè ìóëüòèïëèêàòèâíàÿ êîíúþíêöèÿ). Ôîðìàëüíî, ìíîæåñòâî ôîðìóë Fm åñòü íàèìåíüøåå ìíîæåñòâî,óäîâëåòâîðÿþùåå ñëåäóþùèì óñëîâèÿì:1. At ⊂ Fm,2. åñëè A, B ∈ Fm, òî (A O B), (A ⊗ B) ∈ Fm.Äëÿ êàæäîé ôîðìóëû A ∈ Fm îïðåäåëèì âíåøíèì îáðàçîì å¼îòðèöàíèå A⊥ : p⊥ = p, (p)⊥ = p, åñëè p ∈ Var, (B O C)⊥ = C ⊥ ⊗B ⊥ , (B ⊗C)⊥ = C ⊥ O B ⊥ . Ñåêâåíöèè èñ÷èñëåíèÿ MCLL èìåþò âèä → Γ,ãäå Γ åñòü íåïóñòàÿ ïîñëåäîâàòåëüíîñòü ôîðìóë. Èñ÷èñëåíèå çàäà¼òñÿàêñèîìàìè âèäà → pp, p ∈ Var è ïðèâåä¼ííûìè íèæå ïðàâèëàìè âûâîäà.→ ΓAB∆(→ O)→ Γ(A O B)∆→ ΓA → B∆(→ ⊗)→ Γ(A ⊗ B)∆→ ΓA → A⊥ ∆(cut)→ Γ∆→ Γ∆(rotate)→ ∆ΓÏðèìåð 3.1.Ñåêâåíöèÿ → ((p2 ⊗ p3 ) O p3 )((p2 ⊗ p1 ) O p1 ) âûâîäèìà âèñ÷èñëåíèè MCLL.→ p 2 p2 → p3 p 3→ p2 (p2 ⊗ p3 )p3(→ ⊗)→ p1 p 1(rotate)→ (p2 ⊗ p3 )p3 p2→ p1 p 1(→ ⊗)→ (p2 ⊗ p3 )p3 (p2 ⊗ p1 )p1(→ O)→ (p2 ⊗ p3 )p3 ((p2 ⊗ p1 ) O p1 )(→ O)→ ((p2 ⊗ p3 ) O p3 )((p2 ⊗ p1 ) O p1 )(rotate) èñ÷èñëåíèè MCLL óñòðàíèìî ñå÷åíèå, òî åñòü âñÿêàÿ âûâîäèìàÿ ñåêâåíöèÿ ìîæåò áûòü âûâåäåíà áåç ïðèìåíåíèÿ ïðàâèëà (cut).

Âûâîäèìîñòü ñåêâåíöèè → Γ îáîçíà÷àåòñÿ MCLL `→ Γ.Ïîíÿòèå âíåøíåãî îòðèöàíèÿ ïîçâîëÿåò ðàññìàòðèâàòü â MCLLè äâóñòîðîííèå ñåêâåíöèè, ïîíèìàÿ çàïèñü A1 . . . Am → B1 . . . Bn êàê41⊥äðóãîå îáîçíà÷åíèå ñåêâåíöèè → A⊥m . . . A1 B1 . . . Bn . Âûâîäèìîñòü ñå-êâåíöèè Γ → ∆ â èñ÷èñëåíèè MCLL îáîçíà÷àåòñÿ MCLL ` Γ → ∆.Ñòàíäàðòíûì ïåðåâîäîì (äàëåå, ïåðåâîäîì ) òèïàb , ïîëó÷àåìóþ ïî ñëåäóþùèì ïðàA ∈ Tp áóäåì íàçûâàòü ôîðìóëó AÎïðåäåëåíèå 3.1.âèëàì:1. pb = p, åñëè p ∈ Pr,b⊗Bb,[2. A·B =A[=AbO Bb⊥,3.

A/B\b⊥ O Ab,4. B\A = BÑòàíäàðòíûì ïåðåâîäîì ïîñëåäîâàòåëüíîñòè òèïîâ Γ = A1 . . . An ÿâ-b1 . . . Abn . Ñòàíäàðòíûì ïåðåâîäîìëÿåòñÿ ïîñëåäîâàòåëüíîñòü ôîðìóë Ab1 . . . Abn → Bb , òî åñòüñåêâåíöèè A1 . . . An → B ÿâëÿåòñÿ ñåêâåíöèÿ Ab⊥b⊥îäíîñòîðîííÿÿ ñåêâåíöèÿ → An . . . A1 B .Ïðèìåð 3.2.Ôîðìóëà p1 O((p3 O p2 ) ⊗ p4 ) ÿâëÿåòñÿ ïåðåâîäîì òèïàp1 /(p4 \(p2 · p3 )).Ñëåäóþùàÿ òåîðåìà áûëà äîêàçàíà â [27].Òåîðåìà 4(Ì. Ð. Ïåíòóñ, 1992). Èñ÷èñëåíèå MCLL ÿâëÿåòñÿ êîíñåðâà-òèâíûì ðàñøèðåíèåì èñ÷èñëåíèÿ L∗ â ñìûñëå ñòàíäàðòíîãî ïåðåâîäà,òî åñòü âåðíà ñëåäóþùàÿ ðàâíîñèëüíîñòü:b1 . . .

Abn → B.bL∗ ` A1 . . . An → B ⇔ MCLL ` AÏðèìåð 3.3.Âûâîäèìàÿ â MCLL ñåêâåíöèÿ → (p2 ⊗ p3 )p3 (p2 ⊗ p1 )p1ÿâëÿåòñÿ îáðàçîì âûâîäèìîé â L∗ ñåêâåíöèè (p1 /p2 )p3 (p3 \ p2 ) → p1 .3.2Îòíîøåíèå ñîâìåñòèìîñòè â èñ÷èñëåíèèMCLLÄîáàâëåíèå äâóñòîðîííèõ ñåêâåíöèé â èñ÷èñëåíèå MCLL ïîçâîëÿåòñôîðìóëèðîâàòü ïîíÿòèå ñîâìåñòèìîñòè è äëÿ ýòîãî èñ÷èñëåíèÿ.Îïðåäåëåíèå 3.2.421.

Ôîðìóëû A, B ∈ Fm íàçûâàþòñÿ ñîâìåñòèìûìè, åñëè ñóùåñòâóåòòàêàÿ ôîðìóëà C ∈ Fm, ÷òî îäíîâðåìåííî âûïîëíÿþòñÿ óñëîâèÿMCLL ` A → C è MCLL ` B → C .  ýòîì ñëó÷àå ôîðìóëà Cíàçûâàåòñÿ ñîâìåùàþùåé äëÿ A è B .2. Ôîðìóëû A, B ∈ Fm íàçûâàþòñÿ ñîåäèíèìûìè, åñëè ñóùåñòâóåòòàêàÿ ôîðìóëà D ∈ Fm, ÷òî îäíîâðåìåííî âûïîëíÿþòñÿ óñëîâèÿMCLL ` D → A è MCLL ` D → B .Ñëåäóþùàÿ ëåììà ÿâëÿåòñÿ àíàëîãîì ëåììû 2.2 äëÿ èñ÷èñëåíèÿMCLL è áûëà äîêàçàíà â [27].Ëåììà 3.1.Ñëåäóþùèå óñëîâèÿ ðàâíîñèëüíû:1. Ôîðìóëû A, B ∈ Fm ÿâëÿþòñÿ ñîâìåñòèìûìè â èñ÷èñëåíèè MCLL.2.

Ôîðìóëû A, B ∈ Fm ÿâëÿþòñÿ ñîåäèíèìûìè â èñ÷èñëåíèè MCLL.Èç ëåììû 3.1 ñëåäóåò, ÷òî îòíîøåíèå ñîâìåñòèìîñòè â èñ÷èñëåíèèMCLL òàêæå ÿâëÿåòñÿ ýêâèâàëåíòíîñòüþ. Îáîçíà÷èì ÷åðåç G ñâîáîäíóþ ãðóïïó, ïîðîæä¼ííóþ ìíîæåñòâîì Var; ãðóïïîâóþ îïåðàöèþ, îïåðàöèþ âçÿòèÿ îáðàòíîãî ýëåìåíòà è åäèíèöó ãðóïïû áóäåì îáîçíà÷àòüòàê æå, êàê è â ãëàâå 2.1 ïðè èçó÷åíèè èíòåðïðåòàöèè äëÿ òèïîâ èñ÷èñëåíèÿ Ëàìáåêà. Äëÿ êàæäîãî òèïà îïðåäåëèì ïîíÿòèÿ èíòåðïðåòàöèè â ñâîáîäíîé ãðóïïå è áàëàíñà. Îïðåäåëåíèå èíòåðïðåòàöèè ïðèâåäåíî íèæå, à áàëàíñîì d(A) ôîðìóëû A íàçûâàåòñÿ ðàçíîñòü ìåæäó ÷èñëîì âõîæäåíèé ñâÿçîê O è ⊗ â äàííóþ ôîðìóëó.

Íàïðèìåð,d((p1 O p2 ) ⊗ (p1 ⊗ p3 )) = −1.Îïðåäåëåíèå 3.3.Èíòåðïðåòàöèÿ JAK ôîðìóëû A â ñâîáîäíîé ãðóïïåG åñòü îòîáðàæåíèå, çàäàâàåìîå ñëåäóþùèìè ïðàâèëàìè:1. JpK = p, åñëè p ∈ Var,2. JpK = p−1 , åñëè p ∈ Var,3. JA ⊗ BK = JA O BK = JAKJBK.Ñëåäóþùàÿ òåîðåìà áûëà äîêàçàíà Ì. Ð. Ïåíòóñîì â ðàáîòå [27].43Òåîðåìà 5.Ôîðìóëû A, B ∈ Fm ÿâëÿþòñÿ ñîâìåñòèìûìè â èñ÷èñ-ëåíèè MCLL òîãäà è òîëüêî òîãäà, êîãäà îäíîâðåìåííî âûïîëíÿþòñÿóñëîâèÿ JAK = JBK è d(A) = d(B).Ðàññìîòðèì âçàèìîñâÿçü ìåæäó ñîâìåñòèìîñòüþ òèïîâ A è B âèñ÷èñëåíèè L∗ è ñîâìåñòèìîñòüþ èõ îáðàçîâ â èñ÷èñëåíèè MCLL.Ëåììà 3.2.Äëÿ ëþáîé ôîðìóëû A ∈ Fm âåðíî, ÷òî JA⊥ K = JAK−1 .Äîêàçàòåëüñòâî.

Èíäóêöèÿ ïî ïîñòðîåíèþ ôîðìóëû A.Ëåììà 3.3.b = JAK.Äëÿ ëþáîãî òèïà A ∈ Tp âåðíî ðàâåíñòâî JAKÄîêàçàòåëüñòâî. Èíäóêöèÿ ïî ïîñòðîåíèþ A, äëÿ ïðèìèòèâíûõ òèïîâ óòâåðæäåíèå î÷åâèäíî. Ïóñòü A = B · C , òîãäà JAK = JBKJCK =b ⊗ CKb = JAKb , ÷òî è áûëî íóæíî.

Ïóñòü A = B/C , òîãäà JAK =JBb CKb −1 = JBKJb Cb⊥ K = JBbOCb⊥ K = JAKb . Ñëó÷àé A = C \ BJBKJCK−1 = JBKJðàçáèðàåòñÿ àíàëîãè÷íî. Ëåììà äîêàçàíà.Òèïû A, B ∈ Tp ñîâìåñòèìû â èñ÷èñëåíèè L∗ òîãäà èbèBb ñîâìåñòèìû â èñ÷èñëåíèè MCLL.òîëüêî òîãäà, êîãäà èõ îáðàçû AËåììà 3.4.Äîêàçàòåëüñòâî.

Ïóñòü òèïû A è B ñîâìåñòèìû, òîãäà äëÿ íèõ íàéä¼òñÿ ñîâìåùàþùèé òèï C , òî åñòü L∗ ` A → C, L∗ ` B → C .  ñèëób→Cbêîíñåðâàòèâíîñòè èñ÷èñëåíèÿ MCLL íàä L∗ âåðíî, ÷òî MCLL ` Ab→Cb, òî åñòü ôîðìóëà Cb áóäåò ñîâìåùàþùåé äëÿ AbèBb.è MCLL ` BbèBb ñîâìåñòèìû â MCLL. Òîãäà ïî òåîÏóñòü òåïåðü ôîðìóëû Ab = JBKb , îòêóäà ïî ëåììå 3.3 ñëåäóåò, ÷òî JAK = JBK, ÷òî ïîðåìå 5 JAKòåîðåìå 1 âëå÷¼ò ñîâìåñòèìîñòü òèïîâ A è B . Ëåììà äîêàçàíà.Ïóñòü A ∈ Fm ôîðìóëà, òîãäà áóäåì îáîçíà÷àòü ÷åðåç l(A)äëèíó A, ðàâíóþ ÷èñëó âõîæäåíèé ïåðåìåííûõ â A. Çàìåòèì, ÷òî äëÿb ñîâïàäàþò.âñÿêîãî òèïà A èñ÷èñëåíèÿ Ëàìáåêà âåëè÷èíû l(A) è l(A)Åñëè Γ ∈ Fm∗ íåïóñòàÿ ïîñëåäîâàòåëüíîñòü ôîðìóë è Γ = A1 .

. . An ,òî ïîëîæèì l(Γ) =nPl(Ai ). Îòìåòèì, ÷òî ñóììàðíîå ÷èñëî âõîæäåíèéi=1ïåðåìåííûõ è ñâÿçîê â ôîðìóëó A âñåãäà ðàâíî 2l(A) − 1.44Ïðèìåð 3.4.Ïóñòü A = (p1 O p2 ) ⊗ (p3 O p1 ), òîãäà l(A) = 4.Ïóñòü A, B ∈ Tp ñîâìåñòèìûå òèïû èñ÷èñëåíèÿ L∗ , îáîçíà÷èì÷åðåç mMCLL(A, B) äëèíó ñàìîé êîðîòêîé ñîâìåùàþùåé ôîðìóëû äëÿjbèBb . Åñëè îáîçíà÷èòü ÷åðåç M MCLL (l1 , l2 ) ìàêñèìóì äàíèõ ïåðåâîäîâ Ajíîé âåëè÷èíû ïî âñåì âîçìîæíûì òèïàì äëèíû l1 è l2 ñîîòâåòñòâåííî,òî ñëåäóþùàÿ ëåììà ïðÿìî âûòåêàåò èç äîêàçàòåëüñòâà ëåììû 3.4.Ëåììà3.5.Ôóíêöèÿ MjMCLL (l1 , l2 ) ÿâëÿåòñÿ íèæíåé îöåíêîé äëÿôóíêöèè Mj (l1 , l2 ).Òàêèì îáðàçîì, äëÿ äîêàçàòåëüñòâà íèæíåé îöåíêè äëÿ âåëè÷èíûMj (l1 , l2 ) äîñòàòî÷íî îãðàíè÷èòü ñíèçó âåëè÷èíó MjMCLL (l1 , l2 ).

Ýòîìó èáóäåò ïîñâÿùåíà îñòàâøàÿñÿ ÷àñòü äàííîé ãëàâû.3.3Óïðîù¼ííûå ñåòè äîêàçàòåëüñòâàÄëÿ äîêàçàòåëüñòâà íèæíåé îöåíêè íà äëèíó ñîâìåùàþùåé ôîðìóëûäëÿ äàííûõ ñîâìåñòèìûõ ôîðìóë A è B íàì ïîíàäîáèòñÿ ñôîðìóëèðîâàòü íåîáõîäèìîå óñëîâèå òîãî, ÷òî ôîðìóëà C ÿâëÿåòñÿ ñîâìåùàþùåéäëÿ A è B . Óñëîâèå áóäåò îñíîâàíî íà ñåòÿõ äîêàçàòåëüñòâà ãðàôè÷åñêîì êðèòåðèè âûâîäèìîñòè â èñ÷èñëåíèè MCLL.Ïîíÿòèå ñåòè äîêàçàòåëüñòâà áûëî âïåðâûå ââåäåíî â [12] äëÿ ëèíåéíîé ëîãèêè.

Ðàçëè÷íûå âàðèàíòû ñåòåé äîêàçàòåëüñòâà äëÿ ðîäñòâåííûõ èñ÷èñëåíèé (â îñíîâíîì ìóëüòèïëèêàòèâíîé öèêëè÷åñêîé ëèíåéíîéëîãèêè è èñ÷èñëåíèÿ Ëàìáåêà) ïðåäëàãàëèñü â ðàáîòàõ [1], [30] è [28].Ìû áóäåì èñïîëüçîâàòü êðèòåðèé âûâîäèìîñòè, äîêàçàííûé â [28]. Ïîñêîëüêó íàñ èíòåðåñóåò òîëüêî íåîáõîäèìîå óñëîâèå âûâîäèìîñòè, ìû íåáóäåì ââîäèòü ïîíÿòèå ñåòè äîêàçàòåëüñòâà â ïîëíîì îáú¼ìå, à èñïîëüçóåì òîëüêî ÷àñòü óñëîâèé ñîîòâåòñòâóþùåãî êðèòåðèÿ, ÷òî ïîçâîëèòóïðîñòèòü ôîðìóëèðîâêó.Êàæäîé ñåêâåíöèè → Γ ïîñòàâèì â ñîîòâåòñòâèå ñòðóêòóðó ΩΓ =hΩΓ , 6Γ i. Äëÿ êàæäîé ôîðìóëû A ∈ Fm ââåä¼ì å¼ ïðåäñòàâëÿþùåå45ñëîâî dAe, ïîëó÷åííîå óäàëåíèåì èç çàïèñè A âñåõ ñêîáîê.

Åñëè Γ =A1 . . . An , òî dΓe = dA1 e . . . dAn e, ãäå íîâûé ñèìâîë, íàçûâàåìûé ðîìáîì . Òîãäà ýëåìåíòàìè ìíîæåñòâà ΩΓ áóäóò ïàðû hsk , ki, ãäå÷åðåç sk îáîçíà÷åí k -é ñëåâà ñèìâîë â çàïèñè dΓe (íóìåðàöèÿ íà÷èíàåòñÿ ñ 0). Îòíîøåíèå ïîðÿäêà 6Γ îñóùåñòâëÿåò ñðàâíåíèå òàêèõ ïàð ïîâòîðîìó ýëåìåíòó, ñîîòâåòñòâóþùåå îòíîøåíèå ñòðîãîãî ïîðÿäêà áóäåìîáîçíà÷àòü ÷åðåç <Γ .Ïðèìåð 3.5.Äëÿ ñåêâåíöèè → Γ, ãäå Γ = (p1 O(p2 ⊗ p3 ))(p3 O p1 ),ïðåäñòàâëÿþùåå ñëîâî ðàâíî dΓe = p1 O p2 ⊗ p3 p3 O p1 , à ΩΓ ={h, 0i, hp1 , 1i, hO, 2i, hp2 , 3i, h⊗, 4i, hp3 , 5i, h, 6i, hp3 , 7i, hO, 8i, hp1 , 9i}.Ýëåìåíòû ìíîæåñòâà ΩΓ áóäåì îáîçíà÷àòü ãðå÷åñêèìè áóêâàìè⊗α, β, . .