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

Ñëåäóþùàÿ ëåììà íåïîñðåäñòâåííî âûòåêàåò èçëåìì 3.9 è 3.10.Ëåììà 3.11.Äëÿ ëþáîé òîíêîé ïàðû ñîâìåñòèìûõ ôîðìóë A è B èëþáîé ôîðìóëû C , êîòîðàÿ ÿâëÿåòñÿ ñîâìåùàþùåé äëÿ A è B , âûïîëíÿåòñÿ íåðàâåíñòâî l(C) > D(A) + D(B) + E(A, B).3.5Äîêàçàòåëüñòâî íèæíåé îöåíêèÇàäà÷åé äàííîãî ðàçäåëà ÿâëÿåòñÿ äîêàçàòåëüñòâî îñíîâíîé òåîðåìûäàííîé ãëàâû:Òåîðåìà 7.Äëÿ ëþáûõ k è l îäèíàêîâîé ÷¼òíîñòè íàéäóòñÿ òàêèåñîâìåñòèìûå òèïû T è U èñ÷èñëåíèÿ L∗ (èñ÷èñëåíèÿ L) äëèíû k è lñîîòâåòñòâåííî, ÷òî äëÿ âñÿêîãî òèïà C , êîòîðûé ÿâëÿåòñÿ ñîâìåùàþùèì äëÿ T è U , âûïîëíÿåòñÿ íåðàâåíñòâî l(C) >k 2 +l28+k+l4− 9.Ñ ýòîé öåëüþ äëÿ âñåõ k, l > 1 ìû ïîñòðîèì ôîðìóëû Ak , Bl èñ÷èñëåíèÿ MCLL, ÿâëÿþùèåñÿ ïåðåâîäàìè íåêîòîðûõ òèïîâ Tk è Ul èñ÷èñëåíèÿ Ëàìáåêà, òàêèå ÷òî l(Ak ) = k, l(Bl ) = l è D(Ak ) + D(Bl ) +E(Ak , Bl ) >k 2 +l2k+l8 + 4 −9.Âñëåäñòâèå ëåììû 3.11 èç ñóùåñòâîâàíèÿ äàí-íûõ òèïîâ áóäåò ñëåäîâàòü òðåáóåìàÿ íèæíÿÿ îöåíêà íà äëèíó êðàò÷àé52øåé ñîâìåùàþùåé ôîðìóëû â èñ÷èñëåíèè MCLL, à çíà÷èò, è íà äëèíóñîâìåùàþùåãî òèïà â èñ÷èñëåíèè L∗ .

Îñòàâøàÿñÿ ÷àñòü äàííîãî ðàçäåëà ñîäåðæèò àëãîðèòì ïîñòðîåíèÿ èñêîìûõ òèïîâ è äîêàçàòåëüñòâîñîîòâåòñòâóþùèõ îöåíîê.Ïóñòü ìíîæåñòâî Pr ïðèìèòèâíûõ òèïîâ ñîâïàäàåò ñ ìíîæåñòâîìïåðåìåííûõ Var è ñîäåðæèò äëÿ âñÿêîãî i ýëåìåíòû pi , ri , si , ti , ïðè÷¼ìâñå òàêèå ïðèìèòèâíûå òèïû ðàçëè÷íû. Äëÿ êàæäîãî i > 0 èíäóêòèâíîîïðåäåëèì âñïîìîãàòåëüíûå òèïû Vi , Wi ñëåäóþùèì îáðàçîì: Vi = (pi ·.

. . ·p1 )/(q1 ·. . . ·qi ), W1 = p1 /q1 , Wi+1 = pi+1 /(qi+1 /Wi ). Òàêæå îïðåäåëèìäëÿ êàæäîãî íàòóðàëüíîãî k òèï Tk . Åñëè k = 4i, òî Tk = Vi \ Wi . T4i+2ïîëó÷àåòñÿ èç T4i çàìåíîé âõîæäåíèé ïðèìèòèâíîãî òèïà p1 íà òèï p1 ·p0 ,T2 ïîëàãàåì ðàâíûì p1 /q1 . Äëÿ íå÷¼òíûõ k îïðåäåëèì Tk = p0 · Tk−1 , ãäåp0 íîâûé ïðèìèòèâíûé òèï, T1 = p0 . Òèï Uk ïîëó÷àåòñÿ èç Tk çàìåíîéâñåõ âõîæäåíèé pj íà rj è qj íà tj .Ïðèìåð 3.11.T1 = U1 = p0 ,T2 = p1 /q1 , U2 = r1 /t1 ,T3 = p0 ·(p1 /q1 ),U3 = p0 ·(r1 /t1 ),T4 = (p1 /q1 ) \(p1 /q1 ),U4 = (r1 /t1 ) \(r1 /t1 )T5 = p0 ·((p1 /q1 ) \(p1 /q1 ),U5 = p0 ·((r1 /t1 ) \(r1 /t1 )),T6 = ((p1 ·p0 )/q1 ) \((p1 ·p0 )/q1 ),U6 = ((r1 ·r0 )/t1 ) \((r1 ·r0 )/t1 ),T7 = p0 ·(((p1 ·p0 )/q1 ) \((p1 ·p0 )/q1 )),U7 = p0 ·(((r1 ·r0 )/t1 ) \((r1 ·r0 )/t1 )),T8 = ((p2 ·p1 )/(q1 ·q2 )) \(p2 /(q2 /(p1 /q1 ))),U8 = ((r2 ·r1 )/(t1 ·t2 )) \(r2 /(t2 /(r1 /t1 ))).Îáîçíà÷èì ÷åðåç Ak è Bl ïåðåâîäû òèïîâ Tk è Ul â ëèíåéíóþ ëîãèêó.

Äîêàæåì íåêîòîðûå ñâîéñòâà ïîñòðîåííûõ òèïîâ è ôîðìóë. ÏóñòüA òîíêàÿ ôîðìóëà, à p ∈ Var, òîãäà â äîêàçûâàåìîé íèæå ëåììå áóäåì îáîçíà÷àòü ÷åðåç αA (p) è βA (p) âõîæäåíèÿ àòîìîâ p è p â ôîðìóëóA (â ñëó÷àå åñëè òàêîâûå èìåþòñÿ).Ëåììà 3.12.531. Äëÿ ëþáîãî m âûïîëíÿþòñÿ ðàâåíñòâà dVbm e = pm ⊗ . . .

⊗ p1 Ocm e = pm O . . . O p1 O q1 ⊗ . . . ⊗ qm .q1 O . . . O qm , d W2. JAk K = JTk K = ε, åñëè k ÷¼òíî, JAk K = JTk K = p0 , åñëè k íå÷¼òíî.3. d(Ak ) = 1, åñëè k ÷¼òíî, d(Ak ) = 0, åñëè k íå÷¼òíî.4. Ïóñòü ÷èñëà i, k, m òàêîâû, ÷òî m = b k4 c è 0 < i 6 m, òîãäàδAk (αAK (pi ))−δAk (βAK (pi )) = δAk (αAK (qi ))−δAk (βAK (qi )) = 1+2(m−i). Åñëè k > 4 è k − 4m ∈ {2, 3}, òî δAk (αAK (p0 )) − δAk (βAK (p0 )) =2m − 1.cm e âû÷èñëÿþòñÿ ïî îïðåäåëåíèþ ïåÄîêàçàòåëüñòâî. Ñëîâà dVbm e è dWðåâîäà òèïîâ èç èñ÷èñëåíèÿ Ëàìáåêà â ìóëüòèïëèêàòèâíóþ öèêëè÷åñêóþ ëèíåéíóþ ëîãèêó.

Èç ïóíêòà 1 ñðàçó ñëåäóåò, ÷òî äëÿ ëþáîãî mcm ) = 1, ïîñëå ýòîãî èç ðàâåíñòâàâûïîëíÿåòñÿ ðàâåíñòâî d(Vbm ) = d(Wcm è ëåììû 3.6 ïîëó÷àåì, ÷òî d(A4m ) = −d(Vbm ) + 1 +A4m = Vbm⊥ O Wcm ) = 1. Òàêæå íåïîñðåäñòâåííî ïðîâåðÿåòñÿ, ÷òî d(A4m+2 ) = 1. Äëÿd(Wíå÷¼òíûõ k óòâåðæäåíèå âûòåêàåò èç ðàâåíñòâà Ak = p0 ⊗ Ak−1 .Íåòðóäíî âèäåòü, ÷òî äëÿ âñÿêîãî m âåðíî ïðåäñòàâëåíèå JVm K =−1JWm K = pm .

. . p1 q1−1 . . . qm. Îòñþäà ñëåäóåò, ÷òî JT4m K = JVm K−1 JWm K =ε. Ñõîæèì îáðàçîì äîêàçûâàåòñÿ ðàâåíñòâî JT4m+2 K = ε. Äëÿ íå÷¼òíûõk èç ðàâåíñòâà Ak = p0 ⊗ Ak−1 âûòåêàåò òðåáóåìîå ðàâåíñòâî JTk K = p0 .Ðàâåíñòâî JAk K = JTk K ñëåäóåò èç ëåììû 3.3.Òàêèì îáðàçîì, ìû äîêàçàëè ïåðâûå 3 ïóíêòà ëåììû. Äîêàæåìcm . Ñîîòâåòñòâåííî,÷åòâ¼ðòûé ïóíêò. Ïóñòü k = 4m, òîãäà Ak = Vbm⊥ O Wb⊥δAk (αAk (pi )) = δAk (αWcm (pi )) = 2 + d(Vm ) + δWcm (αWcm (pi )) = 1 + (m − i).Àíàëîãè÷íî δAk (βAk (pi )) = δAk (βVb ⊥ (pi )) = δVb ⊥ (βVb ⊥ (pi )) = δVbm (αVbm (pi )) −mmmd(Vbm ) = 1 + (i − m) − 1 = i − m.

Òàêæå δAk (αAk (qi )) = δVb ⊥ (αVb ⊥ (qi )) =mmδVbm (βVbm (qi ) − 1 = m − i + 1 è δAk (βAk (qi )) = 1 + δWcm (βWcm (qi )) = m + 2 − i.Îòñþäà ïîëó÷àåì óòâåðæäåíèå ïóíêòà 4 äëÿ ñëó÷àåâ k = 4m è k =4m + 1.  ñëó÷àå k ∈ {4m + 2, 4m + 3} ðàññóæäåíèÿ àíàëîãè÷íû. Ëåììàäîêàçàíà.Ëåììà 3.13.54k9k28 + 2 − 2.2D(Ak ) > k8 +1. Äëÿ ëþáîãî ÷¼òíîãî k âûïîëíÿåòñÿ íåðàâåíñòâî D(Ak ) >2. Äëÿ ëþáîãî íå÷¼òíîãî k âûïîëíÿåòñÿ íåðàâåíñòâîk4− 5.Äîêàçàòåëüñòâî. Çàìåòèì, ÷òî åñëè m = b k4 c è m − 4k < 2, òî ìíîæåñòâî íåéòðàëüíûõ ïåðåìåííûõ äëÿ ôîðìóëû Ak ðàâíî â òî÷íîñòè {pi , qi |1 6 i 6 k}.

 ñëó÷àå åñëè k − 4m ∈ {2, 3} â ýòî ìíîæåñòâî äîáàâëÿåòñÿïåðåìåííàÿ p0 . Èñïîëüçóÿ ëåììó 3.12, ïîëó÷àåì, ÷òî ïðè k = 4m âûïîëíÿåòñÿ ðàâåíñòâî D(Tk ) = 2mP((2i − 1) + 1) = 2(m2 + m − 2) =i=2÷òî è áûëî íóæíî. Ïðè k = 4m+2 èìååì D(Tk ) = 22(m2 + 2m − 2) =(k−2)28+ (k − 2) − 4 =k28+k2−kPk28+ k2 − 4,((2i−1)+1)+2m =i=292 , ÷òîè òðåáîâàëîñü.Äëÿ ÷¼òíûõ k ëåììà äîêàçàíà.Ðàçáåð¼ì ñëó÷àé íå÷¼òíûõ k . Ïðè ýòîì D(Tk ) = D(Tk−1 ), ïîýòîìóïðè k = 4m + 1 ìîæíî çàïèñàòü D(Tk ) =k28k28(k−1)28+ k−12 −4 =+ k4 − 5. Ïðè k = 4m + 3 àíàëîãè÷íî èìååì D(Tk ) =+ k4 − 4 78 >k28(k−1)28k28+ k4 − 4 38 >9+ (k−1)2 −2 =+ k4 − 5, ÷òî è òðåáîâàëîñü. Ëåììà äîêàçàíà.Î÷åâèäíî, ÷òî äîêàçàííûå óòâåðæäåíèÿ ðàâíûì îáðàçîì ïðèìåíèìû è ê ôîðìóëàì Bl .

Ýòî ïîçâîëÿåò íàì äîêàçàòü èñêîìóþ íèæíþþîöåíêó íà ìèíèìàëüíóþ äëèíó ñîâìåùàþùåãî òèïà.Òåîðåìà 8.Äëÿ ëþáûõ k è l îäèíàêîâîé ÷¼òíîñòè íàéäóòñÿ òàêèåñîâìåñòèìûå ôîðìóëû A è B èñ÷èñëåíèÿ MCLL äëèíû k è l ñîîòâåòñòâåííî, ÷òî äëÿ âñÿêîé ôîðìóëû C , êîòîðàÿ ÿâëÿåòñÿ ñîâìåùàþùåéäëÿ A è B , âûïîëíÿåòñÿ íåðàâåíñòâî l(C) >k 2 +l28+k+l4− 9.Äîêàçàòåëüñòâî. Âîçüì¼ì â êà÷åñòâå A è B îïðåäåë¼ííûå â äàííîìðàçäåëå ôîðìóëû Ak è Bl . Îíè ñîâìåñòèìû â ñèëó ëåììû 3.12 è êðèòåðèÿ ñîâìåñòèìîñòè.

Ïóñòü C èõ ñîâìåùàþùàÿ ôîðìóëà, òîãäà ïîëåììå 3.11 èìååì l(C) > D(Ak )+D(Bl )+E(Ak , Bl ).  ñëó÷àå ÷¼òíûõ k, lïîëó÷èì D(Ak ) >k28+ k2 − 92 , D(Bl ) >ñóììèðîâàíèè äà¼ò l(C) >k 2 +l28l28+ 2l − 29 , E(Ak , Bl ) = 0, ÷òî ïðè+ k+l2 −9 >55k 2 +l28+ k+l4 − 9. Ïðè íå÷¼òíûõk, l èìååì D(Ak ) >k28+ k4 − 5, D(Bl ) >ñóììèðîâàíèè äà¼ò l(C) >k 2 +l28+k+l4l28+ 4l − 5, E(Ak , Bl ) = 1, ÷òî ïðè− 9, ÷òî è òðåáîâàëîñü. Òåîðåìàäîêàçàíà.Çàìåòèì, ÷òî èñïîëüçîâàííûå â äîêàçàòåëüñòâå ôîðìóëû Ak èBl ÿâëÿþòñÿ ïåðåâîäàìè òèïîâ èñ÷èñëåíèÿ Ëàìáåêà.

Òàêèì îáðàçîì,äëÿ ââåä¼ííîé â ðàçäåëå 3.2 âåëè÷èíû MjMCLL (l1 , l2 ) âåðíà îöåíêàMjMCLL (l1 , l2 ) >k 2 +l28+ k+l4 −9. Èç ëåììû 3.5 âûòåêàåò àíàëîãè÷íàÿ îöåí-êà íà ìèíèìàëüíóþ äëèíó ñîâìåùàþùåãî òèïà â èñ÷èñëåíèè Ëàìáåêà,òî åñòü íà âåëè÷èíó Mj (l1 , l2 ).Òåîðåìà 9.Äëÿ ëþáûõ k è l îäèíàêîâîé ÷¼òíîñòè íàéäóòñÿ òàêèåñîâìåñòèìûå òèïû T è U èñ÷èñëåíèÿ L∗ (èñ÷èñëåíèÿ L) äëèíû k è lñîîòâåòñòâåííî, ÷òî äëÿ âñÿêîãî òèïà C , êîòîðûé ÿâëÿåòñÿ ñîâìåùàþùèì äëÿ T è U , âûïîëíÿåòñÿ íåðàâåíñòâî l(C) >k 2 +l28+k+l4− 9.Èç äàííîé òåîðåìû ñëåäóåò ñëåäóþùàÿ îäíîïàðàìåòðè÷åñêàÿîöåíêà:Ñëåäñòâèå 3.1.Äëÿ ëþáîãî ÷¼òíîãî m íàéäóòñÿ ñîâìåñòèìûå òèïû T èU èñ÷èñëåíèÿ L∗ (èñ÷èñëåíèÿ L), òàêèå ÷òî l(T )+l(U ) = m è äëÿ âñÿêîãîòèïà C , êîòîðûé ÿâëÿåòñÿ ñîâìåùàþùèì äëÿ T è U , âåðíî íåðàâåíñòâîl(C) >m216+m4− 9.56Ãëàâà 4Èñ÷èñëåíèå Ëàìáåêà ñ îïåðàöèÿìèçàìåùåíèÿ4.1Èñ÷èñëåíèå Ëàìáåêà ñ åäèíèöåéÄàííàÿ ãëàâà ñîäåðæèò èçâåñòíûå òåîðåòè÷åñêèå ôàêòû, êàñàþùèåñÿòàê íàçûâàåìûõ ¾ðàçðûâíûõ¿ îïåðàöèé íàä ÿçûêàìè è èñ÷èñëåíèÿ Ëàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿ.

Âíà÷àëå îïðåäåëèì èñ÷èñëåíèå Ëàìáåêàñ åäèíèöåé L1 ([19]). Ïóñòü êîíñòàíòà I íå âõîäèò â ìíîæåñòâî ïðèìèòèâíûõ òèïîâ Pr, òîãäà òèïû èñ÷èñëåíèÿ L1 ñòðîÿòñÿ èç ýëåìåíòîâìíîæåñòâà Pr ∪ {I} ñ ïîìîùüþ ñâÿçîê \, / è ·. Àêñèîìàòèêà èñ÷èñëåíèÿL1 ïîëó÷àåòñÿ èç àêñèîìàòèêè èñ÷èñëåíèÿ L∗ äîáàâëåíèåì àêñèîìû → Iè ïðàâèëà âûâîäàΓ∆ → AΓI∆ → A.Êàê è â èñ÷èñëåíèè L∗ , â èñ÷èñëåíèè Ëàìáåêà ñ åäèíèöåé äîïóñòèìî ïðàâèëî ñå÷åíèÿ.

Êðîìå òîãî, èñ÷èñëåíèå L1 îáëàäàåò ñâîéñòâîìïîäôîðìóëüíîñòè , òî åñòü â âûâîäå ñåêâåíöèè ó÷àñòâóþò òîëüêî ïîäòèïû âõîäÿùèõ â íå¼ òèïîâ. Èç ñâîéñòâà ïîäôîðìóëüíîñòè ñëåäóåò, ÷òîâñÿêàÿ ñåêâåíöèÿ èñ÷èñëåíèÿ L∗ , âûâîäèìàÿ â èñ÷èñëåíèè L1 , ÿâëÿåòñÿ âûâîäèìîé è â èñõîäíîì èñ÷èñëåíèè L1 . Äàííîå ñâîéñòâî íàçûâàåòñÿêîíñåðâàòèâíîñòüþ èñ÷èñëåíèÿ L1 íàä L∗ . ãëàâå 5 íàì áóäåò óäîáíî ðàññìàòðèâàòü íåñåêâåíöèàëüíóþ âåð-57ñèþ èñ÷èñëåíèÿ L1 , êîòîðóþ ìû áóäåì îáîçíà÷àòü ÷åðåç HL1 . Äàííîåèñ÷èñëåíèå òàêæå áûëî ââåäåíî â [19]. Îíî çàäà¼òñÿ àêñèîìàìè âèäàA → A, ãäå A ïðîèçâîëüíûé òèï èñ÷èñëåíèÿ L1 , è ïðèâåä¼ííûìèíèæå ïðàâèëàìè âûâîäà:A → C/BA·B →CA → C/BA·B →CB → A\CA·B →CB → A \ C,A·B →Càêñèîìàìè äëÿ êîíñòàíòû I :A · I ↔ A ↔ I · A,ãäå çàïèñü B ↔ C îçíà÷àåò, ÷òî îáå ñåêâåíöèè B → C è C → B ÿâëÿþòñÿ àêñèîìàìè èñ÷èñëåíèÿ HL1 , à òàêæå ïðàâèëîì òðàíçèòèâíîñòè:A→BB→CA→CÈñ÷èñëåíèÿ L1 è HL1 ÿâëÿþòñÿ ýêâèâàëåíòíûìè (ñì.