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

L ` U φ(hEi) → U 0 , L ` U → U 0 , ïðè ýòîì l(U 0 ) < l(U ) + 2 |E|.2. L ` φ(hEi)U → U 00 , L ` U → U 00 , ïðè ýòîì l(U 00 ) < l(U ) + 2 |E|. ñëåäóþùåé ëåììå ìû äîêàçûâàåì âåðõíþþ îöåíêó íà äëèíóòèïîâ A2 è B2 ñ ðèñóíêà 2.1. Ïîìèìî ýòîãî, èç äîêàçàòåëüñòâà ëåììûìîæíî èçâëå÷ü àëãîðèòì ïîñòðîåíèÿ äàííûõ òèïîâ.Ëåììà 2.10.Äëÿ âñÿêîãî òèïà A ∈ Tp ñóùåñòâóåò òèï A2 , òàêîé÷òî L ` φ(hAi) → A2 , L ` φ(JAK) → A2 , ïðè÷¼ì l(A2 ) 6 l(φ(hAi)).Äîêàçàòåëüñòâî. Ðàññìîòðèì äâà ñëó÷àÿ: JAK = ε è JAK 6= ε.  ïåðâîìñëó÷àå φ(JAK) = q/q . Ïðèìåíèì ëåììó 2.1 ê òèïàì q è A, ïîëó÷èì,÷òî ñóùåñòâóåò òèï Q, òàêîé ÷òî L ` q → Q, φ(hAi)q → Q è l(Q) <2 l(A)+1.

Ïîëîæèì A2 = Q/q . Òîãäà íåòðóäíî ïðîâåðèòü, ÷òî ñåêâåíöèèq/q → A2 è φ(hAi)(q/q) → A2 áóäóò âûâîäèìû â èñ÷èñëåíèè L. Êðîìåòîãî, èç âûâîäèìîñòè ñåêâåíöèè φ(hAi)q → Q è ëåììû 2.8 âûòåêàåò,÷òî âåëè÷èíû l(Q) è l(φ(hAi)) + l(q) = 2 l(A) + 1 èìåþò îäèíàêîâóþ÷¼òíîñòü. Ïîñêîëüêó l(Q) < 2 l(A) + 1, òî l(Q) 6 2 l(A) − 1. Òàêèìîáðàçîì, l(A2 ) = l(Q) + 1 6 2 l(A) = l(φ(hAi)), ÷òî è òðåáîâàëîñü.Ïåðâûé ñëó÷àé ïîëíîñòüþ ðàçîáðàí.Òåïåðü ðàçáåð¼ì ñëó÷àé JAK 6= ε.  ýòîì ñëó÷àå íàéäóòñÿ òàêèåòèïû B1 , . .

. , Bl , C0 , . . . , Cl , ÷òî ñ òî÷íîñòüþ äî ïåðåãðóïïèðîâêè ñêîáîêφ(JAK) = B1 · . . . · Bl , φ(hAi) = φ(hC0 i) · B1 · φ(hC1 i) · B2 . . . · Bl · φ(hCl i),34ïðè÷¼ì äëÿ âñåõ j 6 l âûïîëíÿåòñÿ ðàâåíñòâî JCj K = ε (òèïû C0 èCl ìîãóò îòñóòñòâîâàòü). Åñëè òèï C0 ñóùåñòâóåò, ïðèìåíèì ñëåäñòâèå2.1 ê òèïàì B1 è C0 , ïîëó÷èì, ÷òî íàéä¼òñÿ òèï D1 , òàêîé ÷òî âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ: L ` B1 → D1 , L ` φ(hC0 i)B1 → D1 èl(D1 ) 6 l(B1 ) + 2 l(C0 ). Åñëè òèï C0 îòñóòñòâóåò, ïîëîæèì D1 = B1 ,òàêæå îïðåäåëèì òèïû D2 = B2 , . . .

, Dl = Bl .Òåïåðü äëÿ êàæäîãî j = 1, . . . , l − 1 ïðèìåíèì ñëåäñòâèå 2.1 êòèïàì Dj è Cj , ïîëó÷èì, ÷òî ñóùåñòâóþò òèïû D10 , . . . , Dl0 , òàêèå ÷òîäëÿ êàæäîãî j = 1, . . . , l − 1 âûïîëíÿþòñÿ ñëåäóþùèå óòâåðæäåíèÿ:L ` Dj → Dj0 , L ` Dj Cj → Dj0 è l(Dj0 ) < l(Dj ) + 2 l(Cj ). Åñëè òèï Clñóùåñòâóåò, àíàëîãè÷íûì îáðàçîì ïîñòóïèì è ñ òèïàìè Dl è Cl , èíà÷åïîëîæèì Dl0 = Cl .Ïîëîæèì A2 = D10 · . . . · Dl0 . Èñïîëüçóÿ ïðàâèëà (cut) è (· →)íåòðóäíî âûâåñòè, ÷òî L ` φ(hAi) → A2 è L ` φ(JAK) → A2 . Îñòàëîñüäîêàçàòü îöåíêó íà äëèíó òèïà A2 .  ñàìîì äåëå, l(A2 ) =lPl(Di0 ) 6i=1lP(l(Di ) + 2 l(Ci )) 6 (l(B1 ) + 2 l(C0 )) + 2 l(C1 ) +i=1lPi=1lP(l(Di ) + 2 l(Ci )) =i=2l(Bi ) + 2çàíà.lPi=0l(Ci ) =lPi=1l(Bi ) +lPl(φ(hCi i)) = l(φ(hAi)). Ëåììà äîêà-i=0Òàêèì îáðàçîì, ìû ìîæåì îöåíèòü äëèíû òèïîâ A2 , B2 íà ðèñóíêå2.1.

Ñëåäóþùàÿ ëåììà ïîçâîëÿåò îöåíèòü òàêæå è äëèíû òèïîâ A1 è B1 .Ëåììà 2.11.Äëÿ âñÿêîãî òèïà A ∈ Tp ñóùåñòâóåò òèï A1 , òàêîé÷òî L ` A → A1 , L ` φ(hAi) → A1 è l(A1 ) 6 21 l2 (A) + l(A).Äîêàçàòåëüñòâî.  ñèëó ëåììû 2.7 ìîæíî ñ÷èòàòü, ÷òî A íå ñîäåðæèòîòðèöàòåëüíûõ óìíîæåíèé. Äîêàæåì ëåììó èíäóêöèåé ïî ïîñòðîåíèþòèïà A. Áàçà èíäóêöèè: A = p ∈ Pr, òîãäà A1 = p è óòâåðæäåíèå ëåììûâûïîëíÿåòñÿ.Íà øàãå èíäóêöèè âîçìîæíû òðè ñëó÷àÿ: A = B · C, A = B/C èA = C \ B .

 ñèëó ñèììåòðè÷íîñòè ëåâîãî è ïðàâîãî äåëåíèé äîñòàòî÷íî35ðàçîáðàòü ïåðâûå äâà èç íèõ, ðàçáåð¼ì ïåðâûé. Ïðèìåíèì ïðåäïîëîæåíèå èíäóêöèè ê òèïàì B è C , ïîëó÷èì, ÷òî ñóùåñòâóþò òèïû B1 , C1 ,òàêèå ÷òî ñåêâåíöèè B → B1 , φ(hBi) → B1 è C → C1 , φ(hCi) → C1ÿâëÿþòñÿ âûâîäèìûìè è l(B1 ) 6 12 l2 (B) + l(B), l(C1 ) 6 21 l2 (C) + l(C).Ïîëîæèì A1 = B1 · C1 , òîãäà èç ïðàâèë (· →) è (→ ·) ñëåäóåò, ÷òîL ` A → A1 . Ïîñêîëüêó â ýòîì ñëó÷àå φ(hAi) = φ(hBi) · φ(hCi),òî àíàëîãè÷íûì îáðàçîì äîêàçûâàåòñÿ, ÷òî L ` φ(hAi) → A1 .

Êðîìå òîãî, l(A1 ) = l(B1 ) + l(C1 ) 61 22 (l (B)+ l2 (C)) + l(B) + l(C) 6+ l(C))2 + l(B) + l(C) = 12 l2 (A) + l(A). Òàêèì îáðàçîì, òèï A112 (l(B)ïîëíîñòüþ óäîâëåòâîðÿåò çàêëþ÷åíèþ ëåììû.Òåïåðü ðàçáåð¼ì âòîðîé ñëó÷àé A = B/C . Ïîñêîëüêó òèïA íå ñîäåðæèò îòðèöàòåëüíûõ óìíîæåíèé, òî C ïðåäñòàâèì â âèäåD(k) \(. . . (D(1) \(.

. . ((p/E (l) )/ . . .)/E (1) ) . . .), ãäå îäíî èëè îáà èç ÷èñåëk, l ìîãóò ðàâíÿòüñÿ 0. Îáîçíà÷èì D = D(1) · . . . · D(k) , E = E (1) · . . . · E (l) ,òîãäà òèï C ðàâíîñèëåí òèïó D \ p/E (åñëè k 6= 0, l 6= 0 è îáà òèïàD è E ïðèñóòñòâóþò). Áóäåì ñ÷èòàòü, ÷òî è ñàì òèï C ïðåäñòàâëåí âòàêîì âèäå. Âîçìîæíû ÷åòûðå ïîäñëó÷àÿ â çàâèñèìîñòè îò òîãî, êàêèåèç ÷èñåë k è l ðàâíû 0. Îáîçíà÷èì ÷åðåç B1 òèï, ïîëó÷åííûé â ðåçóëüòàòå ïðèìåíåíèÿ ïðåäïîëîæåíèÿ èíäóêöèè ê òèïó B , àíàëîãè÷íûé ñìûñëèìåþò îáîçíà÷åíèÿ D1 è E1 .Ïåðâûé ïîäñëó÷àé: k = l = 0, òîãäà A = B/p è φ(hAi) = φ(hBi) ·(p \ p/p). Ïîëîæèì A1 = ((p/B1 ) \ p/p). Âûâîäèìîñòü ñåêâåíöèè A → A1ïðîâåðÿåòñÿ íåïîñðåäñòâåííî. Ñåêâåíöèÿ φ(hAi) → A1 èìååò ñëåäóþùèéâûâîä:p → p φ(hBi) → B1(p/p)p → p(p/B1 )φ(hBi) → p(p/B1 )φ(hBi)(p \ p/p)p → p(p/B1 )(φ(hBi) · (p \ p/p))p → p(p/B1 )(φ(hBi) · (p \ p/p)) → p/pφ(hBi) · (p \ p/p) → (p/B1 ) \ p/p(/ →)(· →)(→ /)(→ /)(→ \)Êðîìå òîãî, l(A1 ) = l(B1 ) + 3 6 21 l2 (B) + l(B) + 3.

Åñëè l(B) > 2, òî36äàííàÿ âåëè÷èíà ìàæîðèðóåòñÿ âåëè÷èíîé 21 (l(B) + 1)2 + (l(B) + 1) =1 22 l (A) + l(A).Åñëè æå l(B) = 1, òî áåç îãðàíè÷åíèÿ îáùíîñòè A = p0 /pè A1 = (p/p0 ) \ p/p, òîãäà l(A1 ) = 4 = 12 (l(A)2 ) + l(A), è íåðàâåíñòâîñíîâà âûïîëíÿåòñÿ. Ïåðâûé ïîäñëó÷àé ðàçîáðàí.Ðàçáåð¼ì ïîäñëó÷àé k 6= 0, l 6= 0.  ýòîì ñëó÷àå A = B/(D \ p/E),òîãäà φ(hAi) = φ(hBi) · φ(hEi) · (p \ p/p) · φ(hDi).

Ïîëîæèì A1 = (p/(B1 ·E1 )) \ p/((D1 \ p/E)·E), òîãäà l(A1 ) = l(B1 )+l(D1 )+l(E1 )+2 l(E)+3 61 2222 (l (B)+l (D)+l (E))+(l(B)+l(D)+l(E))+2 l(E)+326 21 (l2 (B)+l2 (D)+l (E) + 2 (l(B) + l(D) + l(E) + l(E)(l(B) + l(D)))) + (l(B) + l(D) + l(E)) <12 (l(B)+ l(D) + l(E) + 1)2 + (l(B) + l(D) + l(E) + 1) = 12 l2 (A) + l(A).Íèæå ïðèâåäåíû âûâîäû ñåêâåíöèé A → A1 è φ(hAi) → A1 âûâîäèìû.p/E → p/ED → D1D(D1 \ p/E) → p/EB → B1E → E1D1 \ p/E → D \ p/E(B/(D \ p/E))(D1 \ p/E) → B1(B/(D \ p/E))(D1 \ p/E)E → B1 · E1p→p(B/(D \ p/E))((D1 \ p/E) · E) → B1 · E1(p/(B1 · E1 ))(B/(D \ p/E))((D1 \ p/E) · E) → p(p/(B1 · E1 ))(B/(D \ p/E)) → p/((D1 \ p/E) · E)B/(D \ p/E) → (p/(B1 · E1 )) \ p/((D1 \ p/E) · E)(\ →)(→ \)(→ /)(→ ·)(· →)(/ →)(→ /)(→ \)(p/E)E → p φ(hDi) → D1φ(hDi)(D1 \ p/E)E → pp(p \ p) → pφ(hDi)((D1 \ p/E) · E) → p φ(hBi) → B1 φ(hEi) → E1p(p \ p/p)φ(hDi)((D1 \ p/E) · E) → pφ(hBi)φ(hEi) → B1 · E1p((p \ p/p) · φ(hDi))((D1 \ p/E) · E) → pφ(hBi) · φ(hEi) → B1 · E1(p/(B1 · E1 ))(φ(hBi) · φ(hEi))((p \ p/p) · φ(hDi))((D1 \ p/E) · E) → p(p/(B1 · E1 ))(φ(hBi) · φ(hEi) · (p \ p/p) · φ(hDi))((D1 \ p/E) · E) → p(p/(B1 · E1 ))(φ(hBi) · φ(hEi) · (p \ p/p) · φ(hDi)) → p/((D1 \ p/E) · E)φ(hBi) · φ(hEi) · (p \ p/p) · φ(hDi) → (p/(B1 · E1 )) \ p/((D1 \ p/E) · E)37Ïóñòü òåïåðü k = 0, l 6= 0, òîãäà A = B/(p/E) è φ(hAi) =φ(hBi)·φ(hEi)·(p \ p/p).

Ïîëîæèì A1 = (p/(B1 ·E1 )) \ p/((p/E)·E), òîãäàl(A1 ) = l(B1 )+l(E1 )+2 l(E)+3 6 21 (l2 (B)+l2 (E))+(l(B)+3 l(E))+3. Âñëó÷àå l(B) > 2 ýòà âåëè÷èíà íå ïðåâîñõîäèò 21 (l2 (B) + l2 (E) + 2 (l(B) +l(E) + l(B)l(E)) + 1) + (l(B) + l(E) + 1) = 21 l2 (A) + l(A), ÷òî è òðåáóåòñÿ. Åñëè æå l(B) = 1, òî áåç îãðàíè÷åíèÿ îáùíîñòè B1 = B = p èl(A1 ) = l(E1 )+2 l(E)+4 6 21 l2 (E)+3 l(E)+4 = 21 (l(E)+2)2 +(l(E)+2) =1 22 l (A)+ l(A), ÷òî è òðåáîâàëîñü. Òðåòèé ïîäñëó÷àé ðàçîáðàí. Âûâîäè-ìîñòü ñåêâåíöèé A → A1 è φ(hAi) → A1 ïðîâåðÿåòñÿ àíàëîãè÷íî ïðåäûäóùåìó ïîäñëó÷àþ.Ïóñòü òåïåðü k 6= 0, l = 0, òîãäà A = B/(D \ p).  ýòîì ñëó÷àåφ(hAi) = φ(hBi) · (p \ p/p) · φ(hDi).

Ïîëîæèì A1 = (p/B1 ) \ p/(D1 \ p),òîãäà l(A1 ) = l(B1 ) + l(D1 ) + 3 61 22 (l (B)+ l2 (D)) + l(B) + l(D) +3 6 21 (l2 (B) + l2 (D) + 2 l(B)l(D) + 2 (l(B) + l(D)) + 1) + (l(B) + l(D) +1) = 21 l2 (A) + l(A). Âûâîäèìîñòü ñåêâåíöèé A → A1 è φ(hAi) → A1ïðîâåðÿåòñÿ àíàëîãè÷íî âòîðîìó ïîäñëó÷àþ.Òåïåðü èñõîäÿ èç äîêàçàííûõ îöåíîê íà äëèíû òèïîâ A1 , A2 , àòàêæå B1 , B2 , ìû ìîæåì îöåíèòü äëèíû òèïîâ A3 , B3 , à çíà÷èò, è òèïàC .

 äàëüíåéøåì äîêàçàòåëüñòâå îñíîâíóþ ðîëü èãðàåò ëåììà 2.1.Ëåììà 2.12.Äëÿ ëþáîãî òèïà A ∈ Tp ñóùåñòâóåò òèï A3 , òàêîé÷òî L ` A → A3 , L ` φ(JAK) → A3 è l(A3 ) 6 12 l2 (A) + 13 l(A).Äîêàçàòåëüñòâî.  ñîîòâåòñòâèè ñ ëåììîé 2.1 è ðèñóíêîì 2.1 â êà÷åñòâå A3 ìîæíî âçÿòü òèï (φ(hAi)/A1 ) \ φ(hAi)/(A2 \ φ(hAi)). Ïðèìåíÿÿëåììû 2.11 è 2.10, ïîëó÷àåì, ÷òî l(A3 ) = l(A1 ) + l(A2 ) + 3 l(φ(hAi)) 61 22 l (A)+ l(A) + 4 l(φ(hAi)).

Ïî ëåììå 2.8 ïîëó÷àåì èñêîìóþ îöåíêó.Òåîðåìà 3.Äëÿ ëþáûõ ñîâìåñòèìûõ â èñ÷èñëåíèè L òèïîâ A, B ∈ Tpíàéä¼òñÿ ñîâìåùàþùèé òèï C , òàêîé ÷òî l(C) 6 12 (l2 (A) + l2 (B)) +352(l(A) + l(B)).38Äîêàçàòåëüñòâî. Áåç îãðàíè÷åíèÿ îáùíîñòè ìîæíî ñ÷èòàòü, ÷òî l(A) 6l(B). Òîãäà â ñîîòâåòñòâèè ñ ëåììîé 2.1 è ðèñóíêîì 2.1 â êà÷åñòâå Cìîæíî âçÿòü òèï (φ(JAK)/A3 ) \ φ(JAK)/(B3 \ φ(JAK)). Òîãäà ïî ëåììå 2.12è ëåììå 2.8 èìååì l(C) = l(A3 ) + l(B3 ) + 3 l(φ(JAK)) 6 21 (l2 (A) + l2 (B)) +13 (l(A)+l(B))+3 l(φ(hAi)) 6 21 (l2 (A)+l2 (B))+13 (l(A)+l(B))+9 l(A) 61 222 (l (A) + l (B)) +352 (l(A) + l(B)).Ñëåäñòâèå2.2.13 (l(A) + l(B)) + 92 (l(A) + l(B)) 6 21 (l2 (A) + l2 (B)) +Äëÿ ëþáûõ ñîâìåñòèìûõ â èñ÷èñëåíèè L∗ òèïîâA, B ∈ Tp íàéä¼òñÿ ñîâìåùàþùèé òèï C , òàêîé ÷òî l(C) 6 12 (l2 (A) +l2 (B)) +352(l(A) + l(B)).Çàìåòèì, ÷òî èç äîêàçàòåëüñòâà ëåììû 2.1 ñëåäóåò, ÷òî ìèíèìàëüíàÿ äëèíà ñîâìåùàþùåãî òèïà è ìèíèìàëüíàÿ äëèíà ñîåäèíÿþùåãî òèïà ðàçëè÷àþòñÿ íå áîëåå ÷åì íà ëèíåéíîå ñëàãàåìîå îòíîñèòåëüíî äëèíèñõîäíûõ òèïîâ.

Òàêèì îáðàçîì, èç äîêàçàííîé òåîðåìû òàêæå ñëåäóåòâåðõíÿÿ îöåíêà íà äëèíó ñîåäèíÿþùåãî òèïà â èñ÷èñëåíèè L.39Ãëàâà 3Íèæíÿÿ îöåíêà äëèíûñîâìåùàþùåãî òèïà â èñ÷èñëåíèè3.1LÌóëüòèïëèêàòèâíàÿ öèêëè÷åñêàÿ ëèíåéíàÿ ëîãèêà äàííîé ãëàâå ìû äîêàæåì íèæíþþ îöåíêó íà ââåä¼ííóþ â ãëàâå 2.2âåëè÷èíó Mj (l1 , l2 ). Äîêàçûâàåìàÿ îöåíêà òàêæå áóäåò êâàäðàòè÷íîé.Äîêàçàòåëüñòâî íèæíåé îöåíêè ïðîâåä¼ì äëÿ èñ÷èñëåíèÿ Ëàìáåêà L∗ ,äîïóñêàþùåãî ïóñòûå àíòåöåäåíòû. Ïîëó÷åííàÿ âåëè÷èíà áóäåò ÿâëÿòüñÿ íèæíåé îöåíêîé è äëÿ èñ÷èñëåíèÿ L, ïîñêîëüêó âñÿêèé ñîâìåùàþùèéòèï â èñ÷èñëåíèè L òàêæå áóäåò ñîâìåùàþùèì è â L∗ .Ïðè äîêàçàòåëüñòâå ìû èñïîëüçóåì ãðàôè÷åñêèé ñïîñîá ïðåäñòàâëåíèÿ ñèíòàêñè÷åñêèõ âûâîäîâ òàê íàçûâàåìûå ñåòè äîêàçàòåëüñòâà.Ïðè ýòîì ìû áóäåì ðàññìàòðèâàòü ñåòè äîêàçàòåëüñòâà íå äëÿ ñàìîãîèñ÷èñëåíèÿ Ëàìáåêà L∗ , à äëÿ åãî êîíñåðâàòèâíîãî ðàñøèðåíèÿ MCLL.Èñ÷èñëåíèå MCLL, íàçûâàåìîå ìóëüòèïëèêàòèâíîé öèêëè÷åñêîéëèíåéíîé ëîãèêîé, áûëî ââåäåíî Ä.

Éåòòåðîì â [34]. Îíî ïðåäñòàâëÿåòñîáîé ôðàãìåíò ââåä¼ííîé â [12] ëèíåéíîé ëîãèêè Æ.-È. Æèðàðà. Åãîêîíñåðâàòèâíîñòü íàä èñ÷èñëåíèåì Ëàìáåêà L∗ , äîïóñêàþùèì ïóñòûåàíòåöåäåíòû, áûëà äîêàçàíà â ðàáîòå [27].Ðàññìîòðèì ñ÷¼òíîå ìíîæåñòâî ïåðåìåííûõ Var = {p1 , p2 , . . .}, âäàëüíåéøåì ìû áóäåì ñ÷èòàòü, ÷òî îíî ñîâïàäàåò ñ ìíîæåñòâîì Pr ïðè40ìèòèâíûõ òèïîâ èñ÷èñëåíèÿ Ëàìáåêà. Àòîìàìè áóäåì íàçûâàòü ýëåìåíòû ìíîæåñòâà At = Var ∪ {p | p ∈ Var}.