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

Ïîñêîëüêó âñå êîððåêòíûå òèïû âèäàA ↑j B ñîâìåñòèìû äðóã ñ äðóãîì, äîñòàòî÷íî äîêàçàòü óòâåðæäåíèåäëÿ êàêîãî-òî îäíîãî çíà÷åíèÿ j , âîçüì¼ì j = s(A) = s(A/J) + 1. Ïîïóíêòàì 1 è 6 ëåììû 5.6 âûïîëíÿþòñÿ ñîîòíîøåíèÿ (A (s(A/J)+1)B) ∼ ((A/J) · J) (s(A/J)+1) B ∼ (A/J) · B , ÷òî è òðåáîâàëîñü.Ñëåäñòâèå 5.3.Äëÿ âñÿêîãî òèïà A ∈ Tpk ñóùåñòâóåò íåïðåðûâíûéòèï A0 ∈ Tpk , òàêîé ÷òî òèïû A è A0 ñîâìåñòèìû.Äîêàçàòåëüñòâî. Èíäóêöèÿ ïî ÷èñëó ¾ðàçðûâíûõ¿ ñâÿçîê â òèïå A. Íàøàãå èíäóêöèè ïðèìåíÿåì ëåììó 5.10, ïîëó÷àÿ ñîâìåñòèìûé ñ äàííûìòèï, ñîäåðæàùèé ìåíüøåå ÷èñëî ðàçðûâíûõ ñâÿçîê.Ïðèìåð 5.3.Ïóñòü s(p1 ) = s(p2 ) = 0, s(q1 ) = s(q2 ) = 1.

Âîçüì¼ì òèï(((q2 ↑2 p2 )/q1 ) ↓1 q2 )p1 , ïðèíàäëåæàùèé ìíîæåñòâó Tp2 . Îí ñîâìåñòèìñ íåïðåðûâíûì òèïîì ((q2 /((((q2 /p2 ) · J)/q1 )/J))/J) · p1 .Îïðåäåëåíèå 5.4.Òèï A ∈ Tpk íàçûâàåòñÿ ïðèâåä¼ííûì, åñëè îí íåñîäåðæèò âõîæäåíèé áàçîâîãî òèïà I , à ïðèìèòèâíûå òèïû qj íåíóëåâîãîñîðòà è áàçîâûé òèï J âñòðå÷àþòñÿ òîëüêî â ïîäòèïàõ âèäà qj /J s(qj ) .78Èç îïðåäåëåíèÿ ñëåäóåò, ÷òî âñÿêèé íåïðåðûâíûé ïðèâåä¼ííûéòèï èìååò ñîðò 0.Ëåììà 5.11.Ïóñòü A, B, C ∈ Tpk , à i, j íåíóëåâûå íàòóðàëüíûå÷èñëà, òàêèå ÷òî âñå ðàññìàòðèâàåìûå òèïû êîððåêòíû, à òèïû âëåâûõ ÷àñòÿõ ñîîòíîøåíèé ïðèíàäëåæàò Tpk .

Òîãäà âåðíû ñëåäóþùèåñîîòíîøåíèÿ:1. (A · C i ) · (B · C j ) ∼ (A · B) · C i+j ,2. (A · C i )/(B · C j ) ∼ (A/B) · C i−j , åñëè i > j ,3. (B · C j ) \(A · C i ) ∼ (B \ A) · C i−j , åñëè i > j .Äîêàçàòåëüñòâî. Ïåðâûé ïóíêò ñðàçó âûòåêàåò èç ïóíêòà 2 ëåììû 5.8è àññîöèàòèâíîñòè óìíîæåíèÿ.

Âòîðîé ïóíêò ñëåäóåò èç öåïî÷êè ñîîòíîøåíèé (A · C i )/(B · C j ) ∼ (C i · A)/(C j · B) ∼ ((C i · A)/B)/C j ∼(C i · (A/B))/C j ∼ ((A/B) · C i )/C j ∼ (A/B) · (C i /C j ) ∼ (A/B) · C i−j ·(C j /C j ) ∼ (A/B) · C i−j , ñëåäóþùèõ èç ëåìì 5.8, 5.6 è 5.7. Òðåòèé ïóíêòäîêàçûâàåòñÿ àíàëîãè÷íî. Ëåãêî ïðîâåðèòü, ÷òî èç óñëîâèÿ ëåììû ñëåäóåò, ÷òî âñå ðàññìàòðèâàåìûå òèïû áóäóò ïðèíàäëåæàòü Tpk .Äëÿ âñÿêîãî òèïà A ∈ Tpk íàéä¼òñÿ íåïðåðûâíûé ïðèâåb, òàêîé ÷òî òèïû A è A·Jb s(A) ÿâëÿþòñÿ ñîâìåñòèìûìè.ä¼ííûé òèï AËåììà 5.12.Äîêàçàòåëüñòâî.

Áóäåì äîêàçûâàòü óòâåðæäåíèå èíäóêöèåé ïî ïîñòðîåíèþ òèïà A. Äëÿ ïðèìèòèâíîãî òèïà p ñîðòà 0 ïîëîæèì pb = p, äëÿïðèìèòèâíîãî òèïà q ñîðòà s > 0 ïîëîæèì qb = q/J s , òàêæå ïîëîæèìIb = Jb = p0 /p0 , ãäå p0 íåêîòîðûé íîâûé ïðèìèòèâíûé òèï ñîðòà 0.Òîãäà áàçà èíäóêöèè ñëåäóåò èç ïóíêòà 1 ëåììû 5.6 è ëåììû 5.7.Äîñòàòî÷íî äîêàçàòü óòâåðæäåíèå ëåììû äëÿ íåïðåðûâíûõ òèïîâ. Íà øàãå èíäóêöèè íóæíî ðàññìîòðåòü äâà ñëó÷àÿ A = B · C èA = B/C (ñëó÷àé A = C \ B ìîæíî íå ðàññìàòðèâàòü â ñèëó òîãî, ÷òîb = Bb·Cb, ïîñëåB/C ∼ C \ B ). Ïóñòü A = B · C , òîãäà ïîëîæèì A÷åãî óòâåðæäåíèå ëåììû âûòåêàåò èç ïóíêòà 1 ëåììû 5.11. Åñëè æåb = B/b Cb, â ýòîì ñëó÷àå óòâåðæäåíèå ëåììûA = B/C , òî ïîëîæèì Añëåäóåò èç ïóíêòà 2 ëåììû 5.11. Ëåììà äîêàçàíà.79Ïðèìåð 5.4.Ïóñòü s(p1 ) = s(p2 ) = 0, s(q1 ) = s(q2 ) = 1, s(r) = 2. Ðàñ-ñìîòðèì íåïðåðûâíûé òèï (q2 /((q1 /(p1 ·J))·p2 )) \ r ñîðòà 1, îí ñîâìåñòèìñ òèïîì (((q2 /J)/(((q1 /J)/(p1 · (p0 /p0 ))) · p2 )) \ r) · J , ïðåäñòàâëÿþùèì ñîáîé êîíêàòåíàöèþ íåïðåðûâíîãî ïðèâåä¼ííîãî òèïà è òèïà J .Ïåðåîáîçíà÷èì âñå ïðèìèòèâíûå òèïû ñîðòà i > 0 ÷åðåç qi,j , j ∈0N.

Äëÿ êàæäîãî òàêîãî òèïà ââåä¼ì íîâûé ïðèìèòèâíûé òèï qi,jñîðòà0. Äëÿ êàæäîãî ïðèâåä¼ííîãî òèïà A ∈ Tpk íàçîâ¼ì åãî 0 -îáðàçîì òèïA0 , ïîëó÷åííûé çàìåíîé âñåõ ïîäòèïîâ âèäà qi,j /J i íà ïðèìèòèâíûé òèï0qi,j(äëÿ êàæäîé ïàðû èíäåêñîâ i è j áåð¼òñÿ ñâîé ïðèìèòèâíûé òèï).Ïðèìåð 5.5.Ïóñòü A = (((p1 /(q2,1 /J 2 ))/(q1,1 /J))/(q1,2 /J)) \ p2 , òîãäà000) \ p2 .)/q1,2)/q1,1åãî 0 -îáðàç A0 ðàâåí (((p1 /q2,1Ëåììà 5.13.Ïóñòü A, B íåïðåðûâíûå ïðèâåä¼ííûå òèïû, à A0 , B 0 èõ 0-îáðàçû. Òîãäà èç ðàâåíñòâà JAK = JBK ñëåäóåò, ÷òî è JA0 K = JB 0 K.Äîêàçàòåëüñòâî. Êàê ñëåäóåò èç ëåììû 5.3, â ñëó÷àå íåïðåðûâíûõ ïðèâåä¼ííûõ A è B äëÿ âûïîëíåíèÿ ðàâåíñòâà JAK = JBK íåîáõîäèìî è äî-ñòàòî÷íî, ÷òîáû äëÿ âñÿêîãî áàçîâîãî òèïà p áûëî âåðíî óñëîâèå JAKp =JBKp . Ïðè ïîñòðîåíèè 0-îáðàçîâ äëÿ ïðèìèòèâíûõ òèïîâ ñîðòà 0 çíà÷å-íèÿ ñ÷¼ò÷èêîâ íå èçìåíÿòñÿ, åñëè æå qi,j ÿâëÿëñÿ ïðèìèòèâíûì òèïîì00 .ñîðòà i > 0, òî èìååò ìåñòî ðàâåíñòâî JA0 Kqi,j= JAKqi,j = JBKqi,j = JB 0 Kqi,jÊðîìå òîãî JA0 KJ = JB 0 KJ = 0, îòêóäà ïî ëåììå 5.3 ìîæíî çàêëþ÷èòü,÷òî JA0 K = JB 0 K.

Ëåììà äîêàçàíà.Ëåììà 5.14.Ïóñòü A, B ïðèâåä¼ííûå òèïû, à A0 , B 0 èõ 0-îáðàçû.Òîãäà èç óñëîâèÿ A0 ∼ B 0 ñëåäóåò, ÷òî è A ∼ B .Äîêàçàòåëüñòâî. Ïóñòü òèïû A0 è B 0 ñîâìåñòèìû, è C 0 èõ ñîâìåùàþùèé òèï. Îáîçíà÷èì ÷åðåç C òèï, ïîëó÷àþùèéñÿ çàìåíîé â C 0 âñåõ0ïðèìèòèâíûõ òèïîâ âèäà qi,jíà òèïû qi,j /J i . Çàìåòèì, ÷òî ïðîâåäÿ àíà-ëîãè÷íóþ çàìåíó â âûâîäå ñåêâåíöèè A0 → C 0 , ìû ïîëó÷èì âûâîä ñåêâåíöèè A → C â èñ÷èñëåíèè HDLk .

Àíàëîãè÷íûì îáðàçîì ïîëó÷àåòñÿ80âûâîä ñåêâåíöèè B → C , òàêèì îáðàçîì, òèï C áóäåò ñîâìåùàþùèìäëÿ òèïîâ A è B .Òåïåðü äîêàæåì îñíîâíóþ òåîðåìó äàííîé ãëàâû. Îñíîâíàÿ èäåÿäîêàçàòåëüñòâà âçÿòà èç äîêàçàòåëüñòâà òåîðåìû 1 â ðàáîòå [27]. Îáîçíà÷èì ÷åðåç Tp0∼ ìíîæåñòâî êëàññîâ ýêâèâàëåíòíîñòè 0 -îáðàçîâ íåïðåðûâíûõ òèïîâ ïî îòíîøåíèþ ∼. Ââåä¼ì íà ìíîæåñòâå Tp0∼ ñòðóêòóðóãðóïïû, ïîëîæèâ [A]∼ ◦ [B]∼ = [A · B]∼ , [A]−1∼ = [A \ A/A]∼ , 1 = [p/p]∼ .Çäåñü p íåêîòîðûé ïðîèçâîëüíî âûáðàííûé ïðèìèòèâíûé òèï, à ÷åðåç [A]∼ îáîçíà÷àåòñÿ êëàññ ýêâèâàëåíòíîñòè òèïà A ïî îòíîøåíèþ ∼,òî åñòü ìíîæåñòâî òèïîâ, ñîâìåñòèìûõ ñ A. Çàìåòèì, ÷òî äàííîå îïðåäåëåíèå êîððåêòíî, ò. ê.

âñå òèïû âèäà A/A ñîâìåñòèìû äðóã ñ äðóãîì,à êîððåêòíîñòü ïåðâûõ äâóõ ïóíêòîâ âûòåêàåò èç òîãî, ÷òî îòíîøåíèåñîâìåñòèìîñòè ÿâëÿåòñÿ êîíãðóýíöèåé.Ëåììà 5.15.Ñòðóêòóðà hTp0∼ , ◦, −1 , 1i ÿâëÿåòñÿ àáåëåâîé ãðóïïîé.Äîêàçàòåëüñòâî. Àññîöèàòèâíîñòü îïåðàöèè ◦ âûòåêàåò èç àññîöèàòèâíîñòè ñâÿçêè ·. Ñîîòíîøåíèå [A]∼ ◦ [B]∼ = [B]∼ ◦ [A]∼ ñëåäóåò èçñîâìåñòèìîñòè òèïîâ A · B è B · A â èñ÷èñëåíèè HDLk .

Êðîìå òîãî,[A]∼ ◦ [A]−1∼ = [A · (A \ A/A)]∼ = [A/A]∼ = 1, ãäå ïîñëåäíåå ðàâåíñòâîñëåäóåò èç ñîâìåñòèìîñòè òèïîâ A/A è p/p. Òàêæå äëÿ ëþáîãî òèïà Aâåðíî ñîîòíîøåíèå A ∼ A · (p/p), òî åñòü [A]∼ = [A]∼ ◦ 1. Ëåììà ïîëíîñòüþ äîêàçàíà.Òåîðåìà 11.Òèïû A, B ∈ Tpk ñîâìåñòèìû â èñ÷èñëåíèè HDLk òîãäàè òîëüêî òîãäà, êîãäà JAK = JBK.Äîêàçàòåëüñòâî. Íåîáõîäèìîñòü äîêàçàíà â ëåììå 5.2, äîêàæåì äîñòàòî÷íîñòü. Ïóñòü JAK = JBK.  ñèëó òðàíçèòèâíîñòè îòíîøåíèÿ ñîâìåñòèìîñòè è ñëåäñòâèÿ 5.3 òåîðåìó äîñòàòî÷íî äîêàçàòü äëÿ íåïðåðûâíûõòèïîâ, ïîýòîìó áóäåì ñ÷èòàòü, ÷òî A è B íåïðåðûâíû. Òîãäà ïî ëåììåbèBb , òàêèå ÷òî â ñëó5.12 íàéäóòñÿ íåïðåðûâíûå ïðèâåä¼ííûå òèïû AbèB ∼Bb , à â ñëó÷àå÷àå s(A) = s(B) = 0 âåðíû ñîîòíîøåíèÿ A ∼ A81b · Jl è B ∼ Bb · J l . Òîãäàs(A) = s(B) = l > 0 âåðíû ñîîòíîøåíèÿ A ∼ Ab = JA/J l K = JAKα−l = JBKα−l = JBKb .

Êðîìå òîãî, âïîëó÷àåì, ÷òî JAKñèëó òîãî, ÷òî îòíîøåíèå ñîâìåñòèìîñòè ÿâëÿåòñÿ êîíãðóýíöèåé, èç ñîâ-bèBb ñðàçó áóäåò ñëåäîâàòü ñîâìåñòèìîñòü èñõîäíûõìåñòèìîñòè òèïîâ Aòèïîâ A è B . Òàêèì îáðàçîì, òåîðåìó äîñòàòî÷íî äîêàçàòü äëÿ ñëó÷àÿíåïðåðûâíûõ ïðèâåä¼ííûõ òèïîâ A è B .Ïóñòü A0 è B 0 0-îáðàçû òèïîâ A è B , òîãäà â ñèëó ëåììû 5.14 äîñòàòî÷íî äîêàçàòü ñîâìåñòèìîñòü òèïîâ A0 è B 0 â èñ÷èñëåíèè HDLk , ïðèýòîì ïî ëåììå 5.13 âåðíî ðàâåíñòâî JA0 K = JB 0 K. Çàìåòèì, ÷òî ìíîæå-ñòâî 0 -îáðàçîâ íåïðåðûâíûõ ïðèâåä¼ííûõ òèïîâ çàìêíóòî îòíîñèòåëüíîïîäòèïîâ.

Îáîçíà÷èì ÷åðåç F0 ñâîáîäíóþ àáåëåâó ãðóïïó, ïîðîæä¼ííóþïðèìèòèâíûìè òèïàìè, âõîäÿùèìè â äàííîå ìíîæåñòâî. Äàëüíåéøèåðàññóæäåíèÿ ïîâòîðÿþò äîêàçàòåëüñòâî òåîðåìû 1 èç ðàáîòû [27].Ðàññìîòðèì îòîáðàæåíèå h : F0 → Tp0∼ , çàäàâàåìîå ñîîòíîøåíèÿìè h(p) = [p]∼ è h(p−1 ) = [p \ p/p]∼ , è ïðîäîëæèì åãî äî ãîìîìîðôèçìàèç F0 â Tp0∼ .

Äîêàæåì ïî èíäóêöèè, ÷òî äëÿ êàæäîãî 0 -îáðàçà E âåðíû ðàâåíñòâà h(JEK) = [E]∼ è h(JEK−1 ) = [E \ E/E]∼ . Áàçà èíäóêöèèñëåäóåò èç îïðåäåëåíèÿ îòîáðàæåíèÿ h.Äîêàæåì øàã èíäóêöèè. Âûïîëíÿþòñÿ ñîîòíîøåíèÿ h(JC · DK) =h(JCKJDK) = [C]∼ ◦ [D]∼ = [C · D]∼ , à òàêæå h(JC · DK−1 ) =h([C]−1 [D]−1 ) = [C \ C/C]∼ ◦ [D \ D/D]∼ ∼ [(C \ C/C) · (D \ D/D)]∼ .Íî ïî ïóíêòó 2 ëåììû 5.6 è ëåììå 5.7 èìååì (C \ C/C) · (D \ D/D) ∼C \((C/C) · (D \ D/D)) ∼ C \(D \ D/D) ∼ C \((D \ D) · (C/C))/D ∼C \(D \(D · C)/C)/D ∼ (D · C) \(D · C)/(D · C). Òàêèì îáðàçîì,h(JC · DK−1 ) = [(D · C) \(D · C)/(D · C)]∼ = [(C · D) \(C · D)/(C · D)]∼ ,÷òî è òðåáîâàëîñü.Ðàçáåð¼ì ñëó÷àé E = C/D, òîãäà h(JC/DK) = h(JCKJDK−1 ) =[C]∼ ◦[D \ D/D]∼ = [C·(D \ D/D)]∼ = [(C·(D \ D))/D]∼ = [C/D]∼ .

Êðîìå òîãî, h(JC/DK−1 ) = h(JDKJCK−1 ) = [D/C]∼ . Íî â ñèëó ïóíêòà 1 ëåììû 5.6 è ëåììû 5.7 âåðíà öåïî÷êà ñîîòíîøåíèé D/C ∼ D/((C/D)·D) ∼82(D/D)/(C/D) ∼ (C/D) \(C/D)/(C/D), ÷òî è òðåáîâàëîñü.Òàêèì îáðàçîì, äëÿ ëþáîãî 0 -îáðàçà E âûïîëíÿåòñÿ ñîîòíîøåíèåh(JEK) = [E]∼ . Íî òîãäà èç ðàâåíñòâà JA0 K = JB 0 K ñëåäóåò ðàâåíñòâî[A0 ]∼ = [B 0 ]∼ , òî åñòü ñîâìåñòèìîñòü òèïîâ A0 è B 0 . Òåîðåìà äîêàçàíà.Òàêèì îáðàçîì, ìû äîêàçàëè, ÷òî óñëîâèå JAK = JBK ÿâëÿåòñÿêðèòåðèåì ñîâìåñòèìîñòè â èñ÷èñëåíèè HDLk . Äîêàæåì, ÷òî îíî òàêæåÿâëÿåòñÿ êðèòåðèåì ñîâìåñòèìîñòè â ïîëíîì èñ÷èñëåíèè HDL. Ïî ëåììå 5.5 ðàâåíñòâî èíòåðïðåòàöèé áóäåò íåîáõîäèìûì óñëîâèåì. Ñ äðóãîéñòîðîíû, åñëè òèïû A è B ñîâìåñòèìû âî ôðàãìåíòå HDLk , òî îíè çàâåäîìî áóäóò ñîâìåñòèìûìè è â èñ÷èñëåíèè HDL.

Òàêèì îáðàçîì, èìååòìåñòî ñëåäóþùàÿ òåîðåìà.Òåîðåìà 12.Òèïû A, B ∈ Tpk ñîâìåñòèìû â èñ÷èñëåíèè HDL òîãäàè òîëüêî òîãäà, êîãäà JAK = JBK.Ñëåäñòâèå 5.4.Òèïû A, B ∈ Tpk ñîâìåñòèìû â èñ÷èñëåíèè HDLk òî-ãäà è òîëüêî òîãäà, êîãäà îíè ñîâìåñòèìû â ïîëíîì èñ÷èñëåíèè HDL.83Ãëàâà 6Î ïåðåñå÷åíèè ÿçûêîâ, ïîðîæäàåìûõðàçðûâíûìè ãðàììàòèêàìè Ëàìáåêà,ñ àâòîìàòíûìè ÿçûêàìè6.1Ñåêâåíöèàëüíîå èñ÷èñëåíèåDLÑóùåñòâåííûì íåäîñòàòêîì èñ÷èñëåíèÿ HDL, õàðàêòåðíûì äëÿ áîëüøèíñòâà íåñåêâåíöèàëüíûõ èñ÷èñëåíèé, ÿâëÿåòñÿ íàëè÷èå ïðàâèëàòðàíçèòèâíîñòè, êîòîðîå ìîæåò ïðèâîäèòü ê íàðóøåíèþ ñâîéñòâà ïîäôîðìóëüíîñòè.

 ñâÿçè ñ ýòèì â äàííîé ãëàâå ìû ðàññìîòðèì ìû ðàññìîòðèì ñåêâåíöèàëüíóþ ôîðìó èñ÷èñëåíèÿ Ëàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿ, îáîçíà÷àåìóþ ÷åðåç DL. èñ÷èñëåíèè Ëàìáåêà ñ îïåðàöèÿìè çàìåùåíèÿ ïîíÿòèå ñåêâåíöèè óñëîæíÿåòñÿ ïî ñðàâíåíèþ ñ èñ÷èñëåíèåì L∗ . Îñíîâíûì ïðè ýòîìÿâëÿåòñÿ îïðåäåëÿåìîå íèæå ïîíÿòèå êîíôèãóðàöèè. Îáîçíà÷èì ÷åðåçTpiD ìíîæåñòâî òèïîâ èç TpD èìåþùèõ ñîðò i, è ïóñòü íîâûé ñèìâîë []èãðàåò ðîëü ðàçäåëèòåëÿ.Îïðåäåëåíèå 6.1.Ìíîæåñòâî àòîìàðíûõ êîíôèãóðàöèé åñòü íàèìåíü-øåå ìíîæåñòâî ñëîâ â àëôàâèòå TpD ∪ {[], {, }, ; }, óäîâëåòâîðÿþùåå ñëåäóþùåìó èíäóêòèâíîìó îïðåäåëåíèþ:1. [] ÿâëÿåòñÿ àòîìàðíîé êîíôèãóðàöèåé.2.