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

Äëÿ èñ÷èñëåíèÿ ñî âñåìè ñâÿçêàìè è îãðàíè÷åíèÿìè íà âõîæäåíèÿ I è J ïîëíîòà ÿâëÿåòñÿ îòêðûòûì âîïðîñîì. Ìû íåáóäåì îñòàíàâëèâàòüñÿ íà ýòîì ïîäðîáíåå, ïîñêîëüêó â äàííîé ðàáîòå íåðàññìàòðèâàþòñÿ âîïðîñû ïîëíîòû èñ÷èñëåíèÿ Ëàìáåêà ñ îïåðàöèÿìèçàìåùåíèÿ.65Ãëàâà 5Îòíîøåíèå ñîâìåñòèìîñòè âèñ÷èñëåíèè Ëàìáåêà ñ îïåðàöèÿìèçàìåùåíèÿ5.1Îòíîøåíèåñîâìåñòèìîñòèèèíòåðïðåòàöèÿâñâîáîäíîé àáåëåâîé ãðóïïåÄàííàÿ ãëàâà ïîñâÿùåíà äîêàçàòåëüñòâó êðèòåðèÿ ñîâìåñòèìîñòè â èñ÷èñëåíèè HDLk ïðè ïðîèçâîëüíîì íàòóðàëüíîì k , à òàêæå èññëåäîâàíèþ îòíîøåíèÿ ñîâìåñòèìîñòè â ïîëíîì èñ÷èñëåíèè HDL.

Âíà÷àëå ââåä¼ì ïîíÿòèå ñîâìåñòèìîñòè äëÿ äàííûõ èñ÷èñëåíèé. Áóäåì ñ÷èòàòü, ÷òîçàôèêñèðîâàíî íåêîòîðîå íàòóðàëüíîå k > 1, êîòîðîå äî êîíöà ãëàâûáóäåì ïîëàãàòü íåèçìåííûì.Îïðåäåëåíèå 5.1.Òèï C ∈ Tpk íàçûâàåòñÿ ñîâìåùàþùèì äëÿ òèïîâA è B â èñ÷èñëåíèè HDLk , åñëè HDLk ` A → C, è HDLk ` B → C . Âýòîì ñëó÷àå òèïû A è B íàçûâàþòñÿ ñîâìåñòèìûìè.Ïðèìåð 5.1.Ïóñòü s(A) = s(B) = 1, òîãäà òèïû (A ↑1 B) ↓1 A è Bÿâëÿþòñÿ ñîâìåñòèìûìè â èñ÷èñëåíèè HDLk ïðè ëþáîì k > 1, ïðè÷¼ì(A/(B \ A)) ÿâëÿåòñÿ èõ ñîâìåùàþùèì òèïîì.

Âûâîäèìîñòü ñåêâåíöèè(A ↑1 B) ↓1 B → A/(B \ A) äîêàçàíà â ïðèìåðå 4.2, âûâîä âòîðîé ñåêâåí-66öèè ïðèâåä¼í íèæå.B \A → B \AB · (B \ A) → AB → A/(B \ A)Ìû áóäåì îáîçíà÷àòü îòíîøåíèå ñîâìåñòèìîñòè ñèìâîëîì ∼. Âñëó÷àå åñëè íåîáõîäèìî äîïîëíèòåëüíî óòî÷íèòü, ÷òî ðàññìàòðèâàåòñÿîòíîøåíèå ñîâìåñòèìîñòè èìåííî â èñ÷èñëåíèè HDLk , ìû áóäåì îáîçíà÷àòü îòíîøåíèå ñîâìåñòèìîñòè ÷åðåç ∼k .Ëåììà 5.1.∼ ÿâëÿåòñÿ îòíîøåíèåì ýêâèâàëåíòíîñòè.Äîêàçàòåëüñòâî. Ðåôëåêñèâíîñòü è ñèììåòðè÷íîñòü î÷åâèäíû, äîêàæåì òðàíçèòèâíîñòü.

Ïóñòü A1 ∼ B, B ∼ A2 , ïðè ýòîì C1 ÿâëÿåòñÿ ñîâìåùàþùèì òèïîì äëÿ òèïîâ A1 è B , à C2 äëÿ òèïîâ B èA2 . Ïðîâåðèì, ÷òî òèï (B/C1 ) \ B/(C2 \ B) áóäåò ñîâìåùàþùèì äëÿòèïîâ A1 è A2 . Äåéñòâèòåëüíî, âñëåäñòâèå ëåììû 4.2 è âûâîäèìîñòèñåêâåíöèè (B/C1 ) · C1 → B èç âûâîäèìîñòè ñåêâåíöèè A1 → C1 ñëåäóåò, ÷òî HDLk ` (B/C1 ) · A1 → B . Àíàëîãè÷íî äîêàçûâàåòñÿ, ÷òîHDLk ` B · (C2 \ B) → B , ÷òî ïî òðàíçèòèâíîñòè âëå÷¼ò âûâîäèìîñòü ñåêâåíöèè (B/C1 ) · A1 · (C2 \ B) → B , îòêóäà ëåãêî ñëåäóåò, ÷òîHDLk ` A1 → (B/C1 ) \ B/(C2 \ B). Àíàëîãè÷íûì îáðàçîì äîêàçûâàåòñÿâûâîäèìîñòü ñåêâåíöèè A2 → (B/C1 ) \ B/(C2 \ B).Íåòðóäíî âèäåòü, ÷òî òîëüêî òèïû îäèíàêîâîãî ñîðòà ìîãóò áûòüñîâìåñòèìûìè. Íàøà çàäà÷à ñîñòîèò â òîì, ÷òîáû ñôîðìóëèðîâàòü êðèòåðèé ñîâìåñòèìîñòè â èñ÷èñëåíèè HDLk â òåðìèíàõ àëãåáðàè÷åñêîéèíòåðïðåòàöèè. Äîêàæåì âíà÷àëå, ÷òî îòíîøåíèå ∼ ÿâëÿåòñÿ êîíãðóýíöèåé îòíîñèòåëüíî âñåõ ñâÿçîê èñ÷èñëåíèÿ HDLk .Ëåììà 5.2.∼ ÿâëÿåòñÿ êîíãðóýíöèåé îòíîñèòåëüíî ·, /, \, j , ↓j , ↑j .Äîêàçàòåëüñòâî.

Ïóñòü A1 ∼ B1 , A2 ∼ B2 , íàì íàäî äîêàçàòü ñîâìåñòèìîñòü òèïîâ A1 ∗ A2 è B1 ∗ B2 äëÿ ïðîèçâîëüíîé ñâÿçêè ∗ (â ñëó÷àå åñëè ñîîòâåòñòâóþùèå òèïû êîððåêòíî îïðåäåëåíû). Çàìåòèì, ÷òî67s(A1 ) = s(B1 ) è s(A2 ) = s(B2 ), ïîýòîìó òèïû A1 ∗ A2 è B1 ∗ B2 ëèáî îäíîâðåìåííî ñóùåñòâóþò, ëèáî îäíîâðåìåííî íå ñóùåñòâóþò. Ïóñòü C1 ñîâìåùàþùèé òèï äëÿ ïàðû òèïîâ A1 , B1 , à C2 ñîâìåùàþùèé òèï äëÿïàðû òèïîâ A2 , B2 . Äî êîíöà äîêàçàòåëüñòâà áóäåì ñ÷èòàòü, ÷òî ñîðòàòèïîâ A1 , A2 , B1 , B2 òàêîâû, ÷òî òèïû A1 ∗ A2 è B1 ∗ B2 îïðåäåëåíû.Îáîçíà÷èì D2 = (A2 /C2 ) · C2 · (C2 \ B2 ).

Cåêâåíöèè D2 → A2 èD2 → B2 áóäóò âûâîäèìûìè, âûâîä ñåêâåíöèè D2 → A2 ïðèâåä¼í íèæå,âòîðàÿ ñåêâåíöèÿ âûâîäèòñÿ àíàëîãè÷íûì îáðàçîì.C2 \ B2 → C2 \ B2C2 · (C2 \ B2 ) → B2 B2 → C2A2 /C2 → A2 /C2C2 · (C2 \ B2 ) → C2(A2 /C2 ) · C2 → A2(A2 /C2 ) · C2 · (C2 \ B2 ) → A2 êà÷åñòâå ñîâìåùàþùåãî òèïà äëÿ òèïîâ A1 ∗ A2 è B1 ∗ B2 , ∗ ∈{·} ∪ {j | j ∈ N}, ìîæíî âçÿòü òèï C1 ∗ C2 .  êà÷åñòâå ñîâìåùàþùåãîòèïà äëÿ òèïîâ A1 ∗ A2 è B1 ∗ B2 , ∗ ∈ {/} ∪ {↑j | j ∈ N}, ìîæíîâçÿòü òèï C1 ∗ D2 .

 êà÷åñòâå ñîâìåùàþùåãî òèïà äëÿ òèïîâ A2 ∗ A1 èB2 ∗ B1 , ∗ ∈ {\} ∪ {↓j | j ∈ N}, ìîæíî âçÿòü òèï D2 ∗ C1 . Âûâîäèìîñòüñîîòâåòñòâóþùèõ ñåêâåíöèé ñëåäóåò èç ëåììû 4.2.Îáîçíà÷èì ÷åðåç Prk ìíîæåñòâî ïðèìèòèâíûõ òèïîâ, èñïîëüçîâàííûõ ïðè ïîñòðîåíèè òèïîâ èç Tpk è ïóñòü α ∈/ Prk . Îáîçíà÷èì ÷åðåç F ñâîáîäíóþ àáåëåâó ãðóïïó, ïîðîæä¼ííóþ ìíîæåñòâîì Prk ∪ {α}.Óìíîæåíèå â äàííîé ãðóïïå áóäåì îáîçíà÷àòü ÷åðåç ◦ (ïðè ýòîì ìû ÷àñòî áóäåì îïóñêàòü ýòîò ñèìâîë), ýëåìåíò, îáðàòíûé ýëåìåíòó a, ÷åðåça−1 , à åäèíèöó ãðóïïû îáîçíà÷èì ÷åðåç ε.

Äëÿ êàæäîãî òèïà A ∈ Tpkîïðåäåëèì åãî èíòåðïðåòàöèþ JAK. Äàëåå ìû áóäåì èñïîëüçîâàòü îáî-çíà÷åíèå JAK èìåííî äëÿ èíòåðïðåòàöèè â ñâîáîäíîé àáåëåâîé ãðóïïå,à íå äëÿ èíòåðïðåòàöèè â íåêîììóòàòèâíîé ñâîáîäíîé ãðóïïå, êàê ýòîäåëàëîñü â ãëàâàõ 2 è 3.Îïðåäåëåíèå 5.2.Èíòåðïðåòàöèåé òèïà A â ãðóïïå F íàçûâàåòñÿýëåìåíò JAK ∈ F, îïðåäåëÿåìûé ñëåäóþùèìè ïðàâèëàìè:681. JpK = p, åñëè p ∈ Prk ,2. JIK = ε,3.

JJK = α,4. JA · BK = JAK ◦ JBK,5. JA/BK = JB \ AK = JAK ◦ JBK−1 ,6. JA j BK = JAK ◦ α−1 ◦ JBK äëÿ ëþáîãî j 6 k ,7. JB ↓j AK = JA ↑j BK = JAK ◦ α ◦ JBK−1 äëÿ ëþáîãî j 6 k .Äëÿ êàæäîãî òèïà A èñ÷èñëåíèÿ HDLk îïðåäåëèì íåñêîëüêî ñ÷¼ò-÷èêîâ: |A| åñòü äëèíà òèïà A, ðàâíàÿ ÷èñëó âõîæäåíèé áàçîâûõ òèïîâ âòèï A, |A|p , ãäå p ∈ Base, åñòü ÷èñëî âõîæäåíèé áàçîâîãî òèïà p â òèï−A. ×åðåç |A|+p è |A|p îáîçíà÷èì, ñîîòâåòñòâåííî, ÷èñëî ïîëîæèòåëüíûõè îòðèöàòåëüíûõ âõîæäåíèé áàçîâîãî òèïà p â òèï A. Äàííûå âåëè÷èíûîïðåäåëÿþòñÿ ñëåäóþùèì îáðàçîì:−1.

|p|+p = 1, |p|p = 0, åñëè p ∈ Base,−2. |q|+p = |q|p = 0, åñëè p, q ∈ Base, p 6= q ,−−−−+++3. |A · B|+p = |A j B|p = |A|p + |B|p , |A · B|p = |A j B|p = |A|p + |B|päëÿ ëþáîãî j 6 k ,+−−−−++4. |A/B|+p = |B \ A|p = |A|p + |B|p , |A/B|p = |B \ A|p = |A|p + |B|p ,+−++−−−5. |A ↑j B|+p = |B ↓j A|p = |A|p + |B|p , |A ↑j B|p = |B ↓j A|p = |A|p + |B|päëÿ ëþáîãî j 6 k .Ïðèìåð 5.2.Ïóñòü p, q, r ∈ Pr2 , s(p) = 0, s(q) = 1, s(r) = 2, A =r ↓2 (((p · r)/q) ↑1 (r/(q · p))), B = (r ↓1 (J · p)) 2 (p/(J \ q)).

Òîãäà |A|+p =+−−−2 −1 2+2, |A|+q = 1, |A|r = 1, |A|p = 0, |A|q = 1, |A|r = 2, JAK = p r α ; |B|p =+−−2 −1 −1 22, |B|−q = |B|r = 1, |B|J = 2, |B|J = 0, JBK = p q r α .Àíàëîãè÷íûì îáðàçîì äëÿ âñÿêîé ñâÿçêè ∗ ∈ {·, /, \, , ↑, ↓} è−âñÿêîãî òèïà A ∈ Tpk ìîæíî îïðåäåëèòü ñ÷¼ò÷èêè |A|∗ , |A|+∗ , |A|∗ , îáî-çíà÷àþùèå îáùåå ÷èñëî âõîæäåíèé ñâÿçêè ∗ â òèï A, à òàêæå ÷èñëî å¼ïîëîæèòåëüíûõ è îòðèöàòåëüíûõ âõîæäåíèé. Ôîðìàëüíîå îïðåäåëåíèåïðèâåäåíî íèæå.69−1. |p|+∗ = |p|∗ = 0, åñëè p ∈ Base, ∗ ∈ {·, /, \, j , ↑j , ↓j },+++++2. |A ∗ B|+∗ = |A|∗ + |B|∗ + 1, |A ∗ B|? = |A|? + |B|? ,åñëè ∗ ∈ {·, i }, ? ∈ {·, /, \, j , ↑j , ↓j }, ? 6= ∗,−−3.

|A ∗ B|−? = |A|? + |B|? , åñëè ∗ ∈ {·, i }, ? ∈ {·, /, \, j , ↑j , ↓j },−++−+4. |A ∗ B|+∗ = |A|∗ + |B|∗ + 1, |A ∗ B|? = |A|? + |B|? ,åñëè ∗ ∈ {/, ↑i }, ? ∈ {·, /, \, j , ↑j , ↓j }, ? 6= ∗,−+5. |A ∗ B|−? = |A|? + |B|? , åñëè ∗ ∈ {/, ↑i }, ? ∈ {·, /, \, j , ↑j , ↓j },−++−+6. |B ∗ A|+∗ = |A|∗ + |B|∗ + 1, |B ∗ A|? = |A|? + |B|? ,åñëè ∗ ∈ {\, ↓i }, ? ∈ {·, /, \, j , ↑j , ↓j }, ? 6= ∗,−+7. |B ∗ A|−? = |A|? + |B|? , åñëè ∗ ∈ {\, ↓i }, ? ∈ {·, /, \, j , ↑j , ↓j }.Ââåä¼ííûå ñ÷¼ò÷èêè ïîçâîëÿþò ïîëó÷èòü ïðîñòîå âûðàæåíèå äëÿèíòåðïðåòàöèè ïðîèçâîëüíîãî òèïà A â ñâîáîäíîé àáåëåâîé ãðóïïå. Äëÿ−êàæäîãî áàçîâîãî òèïà p îáîçíà÷èì ÷åðåç JAKp âåëè÷èíó |A|+p − |A|p .Àíàëîãè÷íûì îáðàçîì äëÿ âñÿêîãî ñèìâîëà áèíàðíîé ñâÿçêè ∗ îïðåäå−ëèì âåëè÷èíó JAK∗ = |A|+∗ − |A|∗ .Äëÿ âñÿêîãî òèïà A ∈ Tpk âåðíî ïðåäñòàâëåíèå JAK =Q JAKpα(JAKJ +JAK↑ +JAK↓ −JAK ) ◦p .Ëåììà 5.3.p∈PrkÄîêàçàòåëüñòâî.

Èíäóêöèÿ ïî ïîñòðîåíèþ òèïà A. Áàçà A ∈ Base ëåãêî ïðîâåðÿåòñÿ íåïîñðåäñòâåííî, ïðîâåä¼ì äîêàçàòåëüñòâî øàãà èíäóêöèè. Ïîñêîëüêó ñ÷¼ò÷èêè íå ó÷èòûâàþò íèæíåãî èíäåêñà ñâÿçîê, óñëîâèìñÿ â äîêàçàòåëüñòâå äàííîé ëåììû îïóñêàòü íèæíèå èíäåêñû â îáîçíà÷åíèÿõ j , ↓j , ↑j .Ïóñòü A = B · C , òîãäà JAK = JBKJCK = α(JBKJ +JBK↑ +JBK↓ −JBK )QpJBKp )α(JCKJ +JCK↑ +JCK↓ −JCK ) pJCKp = α(JBKJ +JCKJ +JBK↑ +JCK↑ +JBK↓ +JCK↓ )p∈Prkp∈PrkQ JBKp +JCKpQ−(JBK +JCK ))αp= α(JAKJ +JAK↑ +JAK↓ −JAK ) pJAKp , ÷òî è òðåáî(Qâàëîñü.p∈Prkp∈PrkÏóñòü A = B/C , òîãäà JAK = JBKJCK−1 = α(JBKJ +JBK↑ +JBK↓ −JBK )Q −JCKppJBKp ) α−(JCKJ +JCK↑ +JCK↓ −JCK )p= α(JBKJ −JCKJ )+(JBK↑ −JCK↑ )p∈PrkkQ JBKp −JCKp∈Pr(JBK↓ −JCK↓ )−(JBK −JCK )pαp=αJB/CKJ +JB/CK↑ +JB/CK↓ −JB/CK(Qp∈Prk70Q−+−+(p(|B|p +|C|p )−(|B|p +|C|p ) ) = αJB/CKJ +JB/CK↑ +JB/CK↓ −JB/CKp∈PrkQ+−p|B/C|p −|B/C|p ,p∈Prk÷òî è òðåáîâàëîñü.

Ñëó÷àé A = C \ B ðàçáèðàåòñÿ àíàëîãè÷íî.Ïóñòü òåïåðü A = B C ,òîãäà JAK = JBKJCKα−1 = αJBKJ +JBK↑αJBK↓ −JBK (QpJBKp )α(JCKJ +JCK↑ +JCK↓ −JCK ) ( pJCKp )α−1= α(JBKJ +JCKJ )p∈Prkp∈PrkQ JBK(JBK↑ +JCK↑ )+(JBK↓ +JCK↓ )−(JBK +JCK +1)αp p +JCKp = α(JAKJ +JAK↑ +JAK↓ −JAK )p∈PrkQ JAKpp , ÷òî è òðåáîâàëîñü.Qp∈PrkÏóñòü A = B ↑ C , òîãäà JAK = JBKJCK−1 α = α(JBKJ +JBK↑ +JBK↓ −JBK )Q −JCKppJBKp )α−(JCKJ +JCK↑ +JCK↓ −JCK ) (p)α = α(JBKJ −JCKJ )+(JBK↑ −JCK↑ +1)p∈Prkp∈PrkQ JBKp −JCK(JBK↓ −JCK↓ )−(JBK −JCK )pαp= αJB ↑ CKJ +JB ↑ CK↑ +JB ↑ CK↓ −JB ↑ CKkQ |B ↑ C|+Q (|B|+ +|C|− )+(|B|− +|C|p∈Pr+)ppppp= αJB ↑ CKJ +JB ↑ CK↑ +JB ↑ CK↓ −JB ↑ CKppp∈Prkp∈PrkQ −|B ↑ C|−p , ÷òî è òðåáîâàëîñü.

Ñëó÷àé A = C ↓ B ðàçáèðàåòñÿ àíàp(Qp∈Prkëîãè÷íî. Ëåììà ïîëíîñòüþ äîêàçàíà.Äëÿ âñÿêîãî òèïà A ∈ Tpk âåðíî ðàâåíñòâî s(A) = (JAKJ +PJAK↑ + JAK↓ − JAK ) +s(p) · JAKp .Ëåììà 5.4.p∈PrkÄîêàçàòåëüñòâî. Èíäóêöèÿ ïî ïîñòðîåíèþ òèïà A. Äîêàçàòåëüñòâîàíàëîãè÷íî ïðîâåä¼ííîìó â ëåììå 5.3.Ñëåäñòâèå 5.1.Åñëè JAK = JBK, ãäå A, B ∈ Tpk , òî s(A) = s(B).Äîêàçàòåëüñòâî. Ïóñòü JAK = JBK, òîãäà ïî ëåììå 5.3 ïîëó÷àåì, ÷òîäëÿ âñÿêîãî ïðèìèòèâíîãî òèïà p âåðíî ðàâåíñòâî JAKp = JBKp , à òàêæå÷òî JAKJ + JAK↑ + JAK↓ − JAK = JBKJ + JBK↑ + JBK↓ − JBK .