1610906281-974acaa5ee9a7bc9236c4fe86efeeea8 (824379), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

Ïîñëåäîâàòåëüíî îïðåäåëèì êîäû ðàçëè÷íûõ îáúåêòîâ ñëåäóþùèì îáðàçîì:Êîäèðîâàíèå ðåãèñòðîâ: γ(Ri ) = 2i, γ(Si ) = 2i + 1.Êîäèðîâàíèå êîìàíä:γ(Q := m)γ(Q := H)γ(inc Q)γ(dec Q)γ(if F = 0 goto m)γ(goto m)======h0, γ(Q), mi,h1, γ(Q), γ(H)i,h2, γ(Q)i,h3, γ(Q)i,h4, γ(F ), mi,h5, mi.Óïðàæíåíèå. Äîêàçàòü, ÷òî ìíîæåñòâî êîäîâ êîìàíä ïðèìèòèâíîðåêóðñèâíî.8Ãëàâà 1.ÌèíèìàøèíûÊîäèðîâàíèå ìàøèí: åñëè 0:c0 , 1:c1 , . . . , k-1:ck−1 ñïèñîê êîìàíäíåêîòîðîé ÌÌ M , òî êîäîì ýòîé ìàøèíû áóäåì íàçûâàòü ÷èñëîγ(M ) = hγ(c0 ), .

. . , γ(ck−1 )i.Óïðàæíåíèå. Äîêàçàòü, ÷òî ìíîæåñòâî âñåâîçìîæíûõ êîäîâ ìèíèìàøèí ïðèìèòèâíî ðåêóðñèâíî.Êàê óæå îòìå÷àëîñü, åñëè êàêîé-ëèáî ðåãèñòð (çà èñêëþ÷åíèåì R0 )íå óïîìèíàåòñÿ â ïðîãðàììå, òî ðåçóëüòàò âû÷èñëåíèÿ ÷èñëî, ñîäåðæàùååñÿ â ðåãèñòðå R0 ïîñëå çàâåðøåíèÿ ýòîé ïðîãðàììû íå çàâèñèò îòñîäåðæèìîãî ýòîãî ðåãèñòðà â íà÷àëå ðàáîòû ïðîãðàììû. Ïîýòîìó ïðèðàññìîòðåíèè ðàáîòû ìèíèìàøèíû èìååò ñìûñë ñëåäèòü çà çíà÷åíèÿìèíå âñåõ å¼ ðåãèñòðîâ, à òîëüêî òåõ, êîòîðûå óïîìÿíóòû â å¼ ïðîãðàììå.Åñëè ðåãèñòð Ri èëè Si óïîìÿíóò â ïðîãðàììå, òî, ïî ñâîéñòâàì êîäèðîâàíèÿ êîíå÷íûõ ïîñëåäîâàòåëüíîñòåé, åãî êîä (ñîîòâåòñòâåííî 2i èëè2i + 1) íå ïðåâîñõîäèò êîäà êîìàíäû, â êîòîðîé îí óïîìÿíóò, à ýòîò êîä,â ñâîþ î÷åðåäü, íå ïðåâîñõîäèò êîä âñåé ïðîãðàììû.

Òàêèì îáðàçîì,ìàêñèìàëüíûé íîìåð ðåãèñòðà, ñîäåðæèìîå êîòîðîãî íàì âîîáùå èìååòñìûñë îòñëåæèâàòü, ìîæíî õîòü è ãðóáî, íî çàòî ïðîñòî îöåíèòü ñâåðõóêîäîì ïðîãðàììû.Ýòî íàáëþäåíèå îáúÿñíÿåò ñëåäóþùåå îïðåäåëåíèå:Îïðåäåëåíèå 1.0.6 Êîíôèãóðàöèåé ìàøèíû c êîäîì a â íåêîòîðûéìîìåíò âðåìåíè íàçîâ¼ì ïàðó, ñîñòîÿùóþ èç ñîäåðæèìîãî êîìàíäíîãîðåãèñòðà c è ïîñëåäîâàòåëüíîñòè çíà÷åíèé ðåãèñòðîâ R0 , S0 , . . .

, Ra , Sa ,êîòîðûå ìû îáîçíà÷èì ñîîòâåòñòâåííî ÷åðåç [R0 ], [S0 ], . . . , [Ra ], [Sa ]. Åñëè C òàêàÿ êîíôèãóðàöèÿ, òî å¼ êîäîì íàçîâ¼ì ÷èñëîγ(C) = hc, h[R0 ], [S0 ], . . . , [Ra ], [Sa ]ii .Åñëè â ïðîöåññå çàâåðøèâøåãîñÿ âû÷èñëåíèÿ ìèíèìàøèíà ïîñëåäîâàòåëüíî íàõîäèëàñü â êîíôèãóðàöèÿõ C0 , C1 , . . . , Ck−1 , òî òàêóþ ïîñëåäîâàòåëüíîñòü áóäåì íàçûâàòü âû÷èñëåíèåì íà ýòîé ÌÌ, à êîäîì ýòîãîâû÷èñëåíèÿ íàçîâ¼ì ÷èñëî hγ(C0 ), γ(C1 ), . .

. , γ(Ck−1 )i.Òåïåðü âñå íåîáõîäèìûå êîäû îïðåäåëåíû, è ìû ìîæåì îïðåäåëèòüîòíîøåíèå T (a, x, y), èãðàþùåå âàæíåéøóþ ðîëü â òåîðèè âû÷èñëèìîñòè.9Îïðåäåëåíèå 1.0.7 Îïðåäåëèì îòíîøåíèå T (a, x, y) êàêT (a, x, y) ⇔ (a íîìåð íåêîòîðîé ÌÌ) ∧ (seq (x)) ∧(y êîä âû÷èñëåíèÿ, íà÷àòîãî ïðè ñîäåðæèìûõðåãèñòðîâ Ri , 1 6 i 6 min(a, `h (x)) ðàâíûõñîîòâåòñòâåííî (x)0 , (x)1 , . . . è íóëåâûõ çíà÷åíèÿõâî âñåõ îñòàëüíûõ ðåãèñòðàõ)Ëåììà 1.0.8 Îòíîøåíèå T (a, x, y), ïðèìèòèâíî ðåêóðñèâíî. îïðåäåëåíèè ýòîãî îòíîøåíèÿ ó÷àñòâóþò òðè êîíúþíêòèâíûõ ÷ëåíà, ïðè÷¼ì ïðèìèòèâíàÿ ðåêóðñèâíîñòü ïåðâûõ äâóõ ñëåäóåò èç óæåäîêàçàííîãî. Îñòàâøèéñÿ êîíúþíêòèâíûé ÷ëåí ìîæíî â ñâîþ î÷åðåäüïðåäñòàâèòü, êàê êîíúþíêöèþ ñëåäóþùèõ óñëîâèé (ñíà÷àëà ïðèâîäèòñÿíåôîðìàëüíîå îïèñàíèå, ïîòîì âûïèñûâàåòñÿ óñëîâèå, ãàðàíòèðóþùåååãî ïðèìèòèâíóþ ðåêóðñèâíîñòü):• y êîä ïîñëåäîâàòåëüíîñòè: seq (y),• (y)0 íîìåð ïîñëåäîâàòåëüíîñòè äëèíû 2, âòîðîé ýëåìåíò êîòîðîéêîäèðóåò ïîñëåäîâàòåëüíîñòü äëèíû 2a + 2:seq ((y)0 ) ∧ `h ((y)0 ) = 2 ∧ seq (((y)0 )1 ) ∧ `h (((y)0 )1 ) = 2a + 2.•  íà÷àëüíîé êîíôèãóðàöèè âñå çíà÷åíèÿ ðåãèñòðîâ Ri , êîäèðóþùèåâõîäíûå äàííûå, ðàâíû ñîîòâåòñòâåííî (x)0 , (x)1 , .

. .:∀i 6 min(a, `h (x))(i 6= 0 → (((y)0 )1 )2i = (x)i−̇1 ).•  íà÷àëüíîé êîíôèãóðàöèè â îñòàëüíûõ Ri ñîäåðæàòñÿ íóëè:(((y)0 )1 )0 = 0 ∧ ∀i 6 a(i > min(a, `h (x)) → (((y)0 )1 )2i = 0).•  íà÷àëüíîé êîíôèãóðàöèè âñå âñïîìîãàòåëüíûå ðåãèñòðû ñîäåðæàò0:∀i 6 a((((y)0 )1 )2i+1 = 0).Ïðåæäå, ÷åì ïðîäîëæèòü ïåðå÷èñëåíèå óñëîâèé, ïðåäïîëîæèì, ÷òî ìûóæå äîêàçàëè ïðèìèòèâíóþ ðåêóðñèâíîñòü ôóíêöèè Next(u, a), âûäàþùåé êîä êîíôèãóðàöèè, ïîëó÷àþùåéñÿ èç êîíôèãóðàöèè ñ êîäîì u çàîäèí øàã âû÷èñëåíèÿ íà ìàøèíå ñ êîäîì a, åñëè a êîä ìàøèíû è u 10Ãëàâà 1.Ìèíèìàøèíûêîä êîíôèãóðàöèè, è êàêîåíèáóäü (íåâàæíî êàêîå) ÷èñëî, â ïðîòèâíîìñëó÷àå.

Ýòî ìû ñäåëàåì ÷óòü ïîçæå. Òîãäà ê íàøèì óñëîâèÿì îñòàíåòñÿäîáàâèòü åùå ñëåäóþùèå êîíúþíêòèâíûå ÷ëåíû:• Êàæäàÿ ñëåäóþùàÿ êîíôèãóðàöèÿ ïîëó÷àåòñÿ èç ïðåäûäóùåé â ðåçóëüòàòå èñïîëíåíèÿ øàãà âû÷èñëåíèÿ:∀i < `h (y)(i + 1 < `h (y) → (y)i+1 = Next((y)i , a).•  ñàìîé ïîñëåäíåé êîíôèãóðàöèè íîìåð êîìàíäû äëÿ èñïîëíåíèÿ íåñîâïàäàåò íè ñ îäíèì íîìåðîì êîìàíäû â ïðîãðàììå:((y)`h (y)−̇1 )0 > `h (a)Ïðèâåä¼ííàÿ âûøå çàïèñü îòíîøåíèÿ T (a, x, y) ïîëó÷àåòñÿ èç îòíîøåíèé è ôóíêöèé, ïðèìèòèâíàÿ ðåêóðñèâíîñòü êîòîðûõ óæå äîêàçàíà,ñ ïîìîùüþ ëîãè÷åñêèõ ñâÿçîê ∧, ∨, ¬, → è íàâåøèâàíèÿ îãðàíè÷åííûõêâàíòîðîâ.

Ýòî ãàðàíòèðóåò ïðèìèòèâíóþ ðåêóðñèâíîñòü ýòîãî îòíîøåíèÿ.Îñòàëîñü ïîêàçàòü ïðèìèòèâíóþ ðåêóðñèâíîñòü ôóíêöèè Next(u, a).Çàìåòèì, ÷òî êîä êîìàíäû, èñïîëíÿåìîé â êîíôèãóðàöèè ñ êîäîì u (ò.å.,ñîäåðæèìîå êîìàíäíîãî ðåãèñòðà), ðàâåí Êîì (a, u) = (a)(u)0 . Íàì ïîíàäîáÿòñÿ òàêæå îïèñàííûå íèæå ïðèìèòèâíî ðåêóðñèâíûå ôóíêöèè.ÇàìÐåã (k, m, u): åñëè k êîä ðåãèñòðà â êîíôèãóðàöèè ñ êîäîì u, òî ýòàôóíêöèÿ âûäà¼ò êîä êîíôèãóðàöèè, ïîëó÷åííîé èç êîíôèãóðàöèèñ êîäîì u çàìåíîé ñîäåðæèìîãî ðåãèñòðà ñ êîäîì k íà m.Òàêóþ ôóíêöèþ ìîæíî îïðåäåëèòü, íàïðèìåð, òàê: ïîñêîëüêó ((u)1 )k ñîäåðæèìîå ðåãèñòðà ñ êîäîì k , äëÿ ïîëó÷åíèÿ òðåáóåìîãî êîäà ñîñòîÿíèÿ ðåãèñòðîâ ìîæíî â ðàçëîæåíèè ÷èñëà (u)1 (ò.å., êîäà ñîñòîÿíèÿðåãèñòðîâ) íà ïðîñòûå ñîìíîæèòåëè óáðàòü âñþ ñòåïåíü ïðîñòîãî pk , ò.å.,((u) ) +1ñîìíîæèòåëü pk 1 k è çàìåíèòüåãî íà pm+1, ïîëó÷èâ íîâûé êîä ñîñòîk(u) ·pm+1ÿíèÿ ðåãèñòðîâ ((u)1 1 )kk +1 à çàòåì `ñîáðàòü' êîä ïîëó÷åííîé êîíôèãóðàpk(u)1 ·pm+1köèè â âèäå (u)0 , ((u)1 )k +1 .

Ïîñëåäíåå âûðàæåíèå êàê ðàç ãîäèòñÿ âpkêà÷åñòâå îïðåäåëåíèÿ äëÿ ôóíêöèè ÇàìÐåã (k, m, u), ãàðàíòèðóþùåå å¼ïðèìèòèâíóþ ðåêóðñèâíîñòü.Ìû îñòàâëÿåì ÷èòàòåëþ íåñëîæíûå äîêàçàòåëüñòâà ñóùåñòâîâàíèÿïðèìèòèâíî ðåêóðñèâíûõ ôóíêöèé ñî ñëåäóþùèìè ñâîéñòâàìè:11ÇàìÊÐ (m, u): åñëè u êîä êîíôèãóðàöèè, òî ýòà ôóíêöèÿ âûäà¼ò êîäêîíôèãóðàöèè, ïîëó÷åííîé èç êîíôèãóðàöèè ñ êîäîì u çàìåíîéñîäåðæèìîãî êîìàíäíîãî ðåãèñòðà íà m.Ðåã (u, i): åñëè u êîä êîíôèãóðàöèè, òî çíà÷åíèå ýòîé ôóíêöèè ðàâíîñîäåðæèìîìó ðåãèñòðà ñ êîäîì i â ýòîé êîíôèãóðàöèè.ÊÐ (u): åñëè u êîä êîíôèãóðàöèè, òî çíà÷åíèå ýòîé ôóíêöèè ðàâíîñîäåðæèìîìó êîìàíäíîãî ðåãèñòðà â ýòîé êîíôèãóðàöèè.Çàìåòèì, ÷òî åñëè u êîä íåêîòîðîé êîíôèãóðàöèè, òî ïî íåìó ìîæíî îïðåäåëèòü òèï êîìàíäû, èñïîëíÿåìîé â ýòîé êîíôèãóðàöèè. Îí ïîëíîñòüþ îïðåäåë¼í ÷èñëîì (Êîì (a, u))0 (åñëè ýòî 0, òî êîìàíäà èìååò âèäR:=m, åñëè 1, òî R:=H è ò.ä.).Ôóíêöèþ Next(u, a) ìîæíî îïðåäåëèòü ìåòîäîì ðàçáîðà ñëó÷àåâ ñëåäóþùèì îáðàçîì.Êîä èñïîëíÿåìîé êîìàíäû áóäåò ðàâåí Êîì (a, u).

Åñëè ýòà êîìàíäà ÿâëÿåòñÿ êîìàíäîé ïðèñâàèâàíèÿ âèäà G:=m, ò.å., (Êîì (a, u))0 = 0,òî â êîäå íîâîé êîíôèãóðàöèè íóæíî çàìåíèòü ñîäåðæèìîå ðåãèñòðà G,ò.å., ðåãèñòðà ñ êîäîì (Êîì (a, u))1 íà (Êîì (a, u))2 (â ðåçóëüòàòå ïîëó÷èìÇàìÐåã ((Êîì (a, u))1 , (Êîì (a, u))2 , u)); êðîìå òîãî, íóæíî áóäåò ïðèáàâèòüê ñîäåðæèìîìó ÊÐ åäèíèöó. Ó÷èòûâàÿ óñòðîéñòâî êîäèðîâêè êîíôèãóðàöèé, ìû âèäèì, ÷òî äëÿ ýòîãî äîñòàòî÷íî óìíîæèòü ïîëó÷åííîå âûðàæåíèå íà p0 .

Èòàê, â ñëó÷àå (Êîì (a, u))0 = 0 çíà÷åíèå ôóíêöèè Next(u, a)ìîæíî âû÷èñëèòü, êàêp0 · ÇàìÐåã ((Êîì (a, u))1 , (Êîì (a, u))2 , u).Àíàëîãè÷íî, åñëè ýòà êîìàíäà ÿâëÿåòñÿ êîìàíäîé ïðèñâàèâàíèÿ âèäà G:=H, ò.å., (Êîì (a, u))0 = 1, òî â êîäå íîâîé êîíôèãóðàöèè íóæíîçàìåíèòü ñîäåðæèìîå ðåãèñòðà G, ò.å., ðåãèñòðà ñ êîäîì (Êîì (a, u))1 íàñîäåðæèìîå ðåãèñòðà ñ êîäîì (Êîì (a, u))2 , ò.å. íà Ðåã (u, (Êîì (a, u))2 )((u)1 )(Êîì (a,u)2 ) (â ðåçóëüòàòå ïîëó÷èì ÇàìÐåã ((Êîì (a, u))1 , Ðåã (u, (Êîì (a, u))2 ), u));ïðèáàâëÿÿ, êàê è ðàíüøå, åäèíèöó ê ÊÐ, ïîëó÷èì, ÷òî êîä êîíôèãóðàöèèïîñëå âûïîëíåíèÿ ýòîãî øàãà áóäåò ðàâåíp0 · ÇàìÐåã ((Êîì (a, u))1 , Ðåã (u, (Êîì (a, u))2 ), u).Âûïèñàâ àíàëîãè÷íûì îáðàçîì âûðàæåíèÿ äëÿ îñòàëüíûõ (âçàèìîèñêëþ÷àþùèõ) ñëó÷àåâ, êîãäà êîìàíäà èìååò âèä12Ãëàâà 1.Ìèíèìàøèíû• inc Q (ò.å., (Êîì (a, u))0 = 2)• dec Q (ò.å., (Êîì (a, u))0 = 3)• if F=0 goto m è ïðè ýòîì ñîäåðæèìîå ðåãèñòðà F ðàâíî 0 (ò.å.,(Êîì (a, u))0 = 4 è Ðåã (u, (Êîì (a, u))1 ) = 0)• if F=0 goto m è ïðè ýòîì ñîäåðæèìîå ðåãèñòðà F íå ðàâíî 0 (ò.å.,• (Êîì (a, u))0 = 4 è Ðåã (u, (Êîì (a, u))1 ) 6= 0) goto m (ò.å., (Êîì (a, u))0 =5),ìû ïîëó÷èì ïðèìåðíî ñëåäóþùåå îïðåäåëåíèå äëÿ ôóíêöèè Next(u, a)ìåòîäîì ðàçáîðà ñëó÷àåâ (íå ñëåäóåò ïóãàòüñÿ êîíêðåòíîãî âèäà äàííîéôóíêöèè, ãîðàçäî âàæíåå òî, ÷òî å¼ â ïðèíöèïå ìîæíî çàïèñàòü â òàêîìâèäå):Next(u, a) =p0 · ÇàìÐåã ((Êîì (a, u))1 , (Êîì (a, u))2 , u), åñëè (Êîì (a, u))0 = 0p0 · ÇàìÐåã ((Êîì (a, u))1 , Ðåã (u, (Êîì (a, u))2 ), u),åñëè (Êîì (a, u))0 = 1p0 · ÇàìÐåã ((Êîì (a, u))1 , Ðåã (u, (Êîì (a, u))1 ) + 1, u),åñëè (Êîì (a, u))0 = 2 p0 · ÇàìÐåã ((Êîì (a, u))1 , Ðåã (u, (Êîì (a, u))1 )−̇1, u),åñëè (Êîì (a, u))0 = 3=ÇàìÊÐ ((Êîì (a, u))2 , u),åñëè (Êîì (a, u))0 = 4 ∧ Ðåã (u, (Êîì (a, u))1 ) = 0ÇàìÊÐ (ÊÐ (u) + 1, u),åñëè (Êîì (a, u))0 = 4 ∧ Ðåã (u, (Êîì (a, u))1 ) 6= 0 ÇàìÊÐ ((Êîì (a, u))1 , u), åñëè (Êîì (a, u))0 = 5 0, â îñòàëüíûõ ñëó÷àÿõ.Ïðèâåä¼ííàÿ çàïèñü ãàðàíòèðóåò ïðèìèòèâíóþ ðåêóðñèâíîñòü ôóíêöèè Next(u, a).

Ëåììà äîêàçàíà.Åñëè y êîä âû÷èñëåíèÿ, òî, ïðîñìàòðèâàÿ îïðåäåëåíèÿ, ìû âèäèì,÷òî ðåçóëüòàò âû÷èñëåíèÿ ñîäåðæèìîå ðåãèñòðà R0 îïðåäåëÿåòñÿ ñïîìîùüþ ïðèìèòèâíî ðåêóðñèâíîé ôóíêöèèU (y) = (((y)`h (y)−̇1 )1 )0 .13Òàêèì îáðàçîì, ìû ïîëó÷àåì, ÷òî åñëè f (x1 , . . . , xn ) âû÷èñëÿåòñÿ íàÌÌ, òî ó ýòîé ÌÌ åñòü íîìåð, ñêàæåì, m, è ïîýòîìóf (x1 , . . . , xn ) ' U (µyT (m, hx1 , .

Характеристики

Список файлов лекций