Диссертация (1104034), страница 4
Текст из файла (страница 4)
Äëÿ α < ε0 ìíîæåñòâî Uαn ⊂ U ÿâëÿåòñÿ ìíîæåñòâîì âñåõ ïîñëåäîâàòåëüíîñòåé îðäèíàëîâ(α0 , α1 , . . . , αn )21òàêèõ, ÷òî α0 < α è αi+1 ≤ `(αi ) äëÿ êàæäîãî i < n − 1. Äëÿ êàæäîãîk ≤ n áèíàðíîå îòíîøåíèå Rk çàäàåòñÿ ñëåäóþùèì îáðàçîì:def(α0 , α1 , . . . , αn ) Rk (β0 , β1 , . . . , βn ) ⇐⇒ βk < αk ∧ ∀i < k(αi = βi ).Îòìåòèì íåñêîëüêî ïîëó÷àåìûõ íåïîñðåäñòâåííîé ïðîâåðêîé ñâîéñòâìîäåëåé Uαn :Ëåììà 1.5.Ïóñòü n íàòóðàëüíîå ÷èñëî, à α îðäèíàë, 0 < α < ε0 .1.
åäèíñòâåííûì ýëåìåíòîì Uα−1 ÿâëÿåòñÿ ();2. äëÿ âñÿêîãî α0 ìîäåëü ({(β0 , β1 , . . . , βn ) ∈ Uαn | α0 = β0 }, R1 , . . . , Rn )n−1;èçîìîðôíà ìîäåëè U`(α0 )+13. äëÿ âñåõ k îò 1 äî n − 1 è (β0 , . . . , βn ), (γ0 , . . . , γn ) ∈ Uαn òàêèõ, ÷òî(β0 , . . . , βn ) Rk (γ0 , . . . , γn ),ìû èìååì β0 = γ0 .Ìîäåëü Uωnn+1 ÿâëÿåòñÿ óíèâåðñàëüíîé ìîäåëüþ äëÿ çàìêíóòîãîôðàãìåíòà ëîãèêè GLPn [22, 23, 9]; îòìåòèì, ÷òî ëîãèêà GLP−1 ýòîïðîñòî èñ÷èñëåíèå âûñêàçûâàíèé PC.
Óíèâåðñàëüíîñòü çäåñü îçíà÷àåò,÷òî äëÿ êàæäîé çàìêíóòîé GLPn -ôîðìóëû ϕ ìû èìååìGLP ` ϕ ⇐⇒ Uωnn+1 |= ϕ.Ìû áóäåì èñïîëüçîâàòü ìîäåëü âû÷èñëåíèéRAM (ìàøèíà ñ ïðî-èçâîëüíûì äîñòóïîì ê ïàìÿòè). Òî÷íåå ãîâîðÿ, ìû èñïîëüçóåì îïðåäåëåíèå RAM èç [16] ñî âðåìåíåì èñïîëíåíèÿ âñåõ èíñòðóêöèé ðàâíûì 1.
Âñåîãðàíè÷åíèÿ íà âðåìÿ èñïîëíåíèÿ äàíû äëÿ ýòîé ìîäåëè âû÷èñëåíèé.Îòìåòèì, ÷òî â [16] áûëî ïîêàçàíî, ÷òîRAM ìîæåò áûòü ñèìóëèðîâà-íà íà ìíîãîëåíòî÷íûõ ìàøèíàõ Òüþðèíãà ñ íå áîëåå ÷åì êóáè÷åñêèìðîñòîì âðåìåíè èñïîëíåíèÿ.Ìû äàåì ýôôåêòèâíîå êîäèðîâàíèå íåêîòîðûõ ïîäìíîæåñòâ Uαn .Äëÿ äîêàçàòåëüñòâà ýòîãî ìû èñïîëüçóåì êîäèðîâàíèå îðäèíàëîâ, ìåíüøèõ ε0 , èçâåñòíîå êàê êàíòîðîâñêàÿ ñèñòåìà îðäèíàëüíûõ îáîçíà÷åíèé.22Êàæäûé îðäèíàë β < ε0 êîäèðóåòñÿ, ëèáî ñèìâîëîì 0, åñëè îí ðàâåí 0,ëèáî ñâîåé ÊÍÔω β0 + · · · + ω βm−1 ,ãäå âñå βi äàíû â âèäå àíàëîãè÷íûõ êîäîâ.Áîëåå ôîðìàëüíî, ìû ïðåäñòàâëÿåì îðäèíàë 0 ñèìâîëîì 0, à âñÿêèé îðäèíàë β > 0 ñ ÊÍÔ ω β0 + · · · + ω βm−1 ñòðîêîéωˆ(s0 ) + ωˆ(s1 ) + · · · + ωˆ(sm−1 ),ãäå ïðè êàæäîì i îò 0 äî m − 1 ñòðîêà si ïðåäñòàâëÿåò îðäèíàë βi . Èçòåõíè÷åñêèõ ñîîáðàæåíèé îäíîâðåìåííî ñî ñòðîêîé s, ïðåäñòàâëÿþùåéîðäèíàë β , ìû õðàíèì ìàññèâ a íàòóðàëüíûõ ÷èñåë òàêîé, ÷òî1.
ðàçìåð a ðàâåí äëèíå s,2. åñëè èìååòñÿ îòêðûâàþùàÿñÿ (çàêðûâàþùàÿñÿ) ñêîáêà íà ïîçèöèèi â ñòðîêå s, òî ìû õðàíèì ïîçèöèþ ñîîòâåòñòâóþùåé åé çàêðûâàþùåéñÿ (îòêðûâàþùåéñÿ) ñêîáêè íà ïîçèöèè i ìàññèâà a,3. âî âñåõ îñòàëüíûõ ïîçèöèÿõ ìàññèâà ñòîèò 0.ßñíî, ÷òî äëÿ ñòðîêè s, ïðåäñòàâëÿþùåé íåêîòîðûé îðäèíàë, ìû ìîæåìñêîíñòðóèðîâàòü ñîîòâåòñòâóþùèé åé ìàññèâ a çà âðåìÿ O(|s|). Î÷åâèäíî, ýòî äàåò íàì êîä äëÿ êàæäîãî îðäèíàëà ìåíüøåãî ε0 .
 ñèëó òåîðåìûÊàíòîðà î íîðìàëüíîé ôîðìå îðäèíàëîâ ýòîò êîä åäèíñòâåíåí. Êîãäàìû ãîâîðèì î âû÷èñëèìûõ ôóíêöèÿõ îò îðäèíàëîâ α < ε0 , ìû ïåðåäàåì ýòè îðäèíàëû íà âõîä ôóíêöèè â âèäå ÷åòâåðîê (slink , alink , kfirst , klast ),ãäå slink ÿâëÿåòñÿ ññûëêîé íà ñòðîêó s, alink ÿâëÿåòñÿ ññûëêîé íà ìàññèâ a, à ïàðà s è a îáðàçóþò êîä îðäèíàëà, 0 ≤ kfirst < klast ≤ |s|,è ïîäñòðîêà s0 = s[kfirst ]s[kfirst + 1] . . . s[klast − 1] ÿâëÿåòñÿ ïðåäñòàâëåíèåì îðäèíàëà α.
Ýòî ñîãëàøåíèå ïîçâîëÿåò íàì ðàáîòàòü ñ îðäèíàëàìè β = ω β0 + · · · + ω βm−1 , êàê ñ íåèçìåíÿåìûìè ñïèñêàìè îðäèíàëîâ(β0 , . . . , βm−1 ), ò.å. ìû ìîæåì õðàíèòü ññûëêè íà βi â O(1) ïàìÿòè, ñòðîèòü ññûëêè íà βi+1 è βi−1 èç ññûëêè íà βi çà O(1) âðåìåíè è äåëàòüâûçîâû ôóíêöèè ñ àðãóìåíòîì βi çà O(1) (áåç ó÷åòà âðåìåíè ðàáîòûñàìîé ôóíêöèè), ïåðåäàâàÿ åé ññûëêó íà βi .23Äàëåå â ýòîì ðàçäåëå íàñ áóäóò èíòåðåñîâàòü òîëüêî îðäèíàëû,ìåíüøèå ε0 .  ýòîì ðàçäåëå ìû îòîæäåñòâëÿåì îðäèíàëû ìåíüøèå ε0 èè èõ êîäû.Ìû îïðåäåëÿåì ôóíêöèþ c : ε0 → ω . Äëÿ îðäèíàëà α = ω β0 +· · · + ω βn−1 â êàíòîðîâñêîé íîðìàëüíîé ôîðìå ìû ïîëàãàåìc(α) = 1 + c(β0 ) + · · · + c(βn−1 ).Êðîìå òîãî, c(0) = 1. Ýòî äàåò íàì îäíîçíà÷íîå îïðåäåëåíèå ôóíêöèèc. Îòìåòèì, ÷òî ïàìÿòü, òðåáóåìàÿ äëÿ õðàíåíèÿ îðäèíàëà α, ðàâíàO(c(α)).Ëåììà 1.6.Ìîæíî ïðîèçâåñòè ñðàâíåíèå îðäèíàëîâ α, β çà âðåìÿO(min(c(α), c(β))).Äîêàçàòåëüñòâî.
Îïèøåì ðåêóðñèâíûé àëãîðèòì. Ïóñòü α = ω α0 +· · ·+ω αn−1 è β = ω β0 + · · · + ω βm−1 îðäèíàëû â ÊÍÔ. Íà÷èíàÿ ñ i = 0, ìûóâåëè÷èâàåì i íà 1 äî òåõ ïîð ïîêà èëè ìû íå áóäåì èìåòü i ≥ min(n, m),èëè αi 6= βi ; ìû èñïîëüçóåì ðåêóðñèâíûå âûçîâû îïèñûâàåìîé ôóíêöèèäëÿ ñðàâíåíèÿ αi è βi . Åñëè ïîñëå ýòîé ïðîöåäóðû îêàçûâàåòñÿ, ÷òî i =n = m, òî ìû óñòàíîâèëè, ÷òî α = β . Åñëè i = n < m èëè i < min(n, m) èαi < βi , òî ìû óñòàíîâèëè, ÷òî α < β . Èíà÷å, ìû óñòàíîâèëè, ÷òî α > β .Èíäóêöèåé ïî c(α) + c(β) ìû ïðîâåðÿåì, ÷òî âûïîëíÿåòñÿ òðåáóåìàÿ âåðõíÿÿ îöåíêà íà âðåìÿ ðàáîòû.Ëåììà 1.7.Äëÿ îðäèíàëîâ α è β ìû ìîæåì ïîñòðîèòü îðäèíàë α +βçà âðåìÿ O(c(α) + c(β)). Ïðè ýòîì c(α + β) ≤ c(α) + c(β).Äîêàçàòåëüñòâî.
Ñëó÷àè β = 0 è α = 0 òðèâèàëüíû. Äàëåå ìû ïðåäïîëàãàåì, ÷òî α, β > 0. Ïóñòü α = ω α0 + · · · + ω αn−1 è β = ω β0 + · · · + ω βm−1 îðäèíàëû â ÊÍÔ. Ìû íàõîäèì íàèìåíüøåå k < n òàêîå, ÷òî αk < β0 .Î÷åâèäíî, ÷òî ÊÍÔ α + β èìååò âèäω α0 + · · · + ω αk−1 + ω β0 + · · · + ω βm−1 .Î÷åâèäíî, èìååò ìåñòî òðåáóåìàÿ ëèíåéíàÿ âåðõíÿÿ îöåíêà íàâðåìÿ ðàáîòû.24Äëÿ îðäèíàëîâ α è β , α < β ìû êîäèðóåì ïîëóèíòåðâàë [α, β) ={γ | α ≤ γ < β} ïàðîé hα, βi.
Äëÿ ïîëóèíòåðâàëà A = [α, β) ìû ïîëàãàåì`(A) = sup{`(γ) + 1 | γ ∈ A}.Íàïðèìåð,`([ω ω + 1, ω ω + ω + ω)) = `(ω ω + ω) + 1 = 2.Ëåììà 1.8.Äëÿ ïîëóèíòåðâàëà A = [α, β) òàêîãî, ÷òî `(α) = 0:1. ìû ìîæåì íàéòè `(A) çà âðåìÿ O(c(α) + c(β));2. c(`(A)) ≤ c(β);3.
[0, `(A)) = {`(γ) | γ ∈ A}.Äîêàçàòåëüñòâî. Ïóñòü îðäèíàëû α è β èìåþò ñëåäóþùóþ ÊÍÔ:α = ω α0 + · · · + ω αn−1 èβ = ω β0 + · · · + ω βm−1 .Ïóñòü k = min({n} ∪ {i | αi < βi }). Î÷åâèäíî, ÷òî k < m.Ïóñòü ζ = max(βk , 1), åñëè k = m − 1 è ïóñòü ζ = βk + 1 èíà÷å.Äîêàæåì, ÷òî {`(γ) | γ ∈ A)} = [0, ζ).Íà÷íåì ñ ðàññìîòðåíèÿ íåêîòîðîãî γ ∈ A è äîêàæåì, ÷òî `(γ) < ζ .ÊÍÔ îðäèíàëà γ ðàâíàγ = ω α0 + · · · + ω αk−1 + ω γ0 + · · · + ω γl−1 ,ãäå âñå γi ≤ βk è åñëè k = m − 1, òî âñå γi < βk . Åñëè l = 0, òî α = γ è`(γ) = `(α) = 0 < ζ .Ïóñòü l 6= 0. Òîãäà ìû èìååì `(γ) = γl−1 ≤ βk , åñëè k < m − 1 è`(γ) = γl−1 < βk , åñëè k = m − 1. Ñëåäîâàòåëüíî `(γ) < ζ .Òåïåðü ìû ðàññìàòðèâàåì ïðîèçâîëüíîå δ ∈ [0, ζ) è íàõîäèì γ ∈ Aòàêîå, ÷òî `(γ) = δ .
Åñëè δ = 0, òî ìû ìîæåì âûáðàòü α â êà÷åñòâå γ .Èíà÷å ìû âûáèðàåì γ = α+ω δ ; î÷åâèäíî, ÷òî îòñþäà γ ∈ A. Òåì ñàìûì,{`(γ) | γ ∈ A)} = [0, ζ).25Òàêèì îáðàçîì, `(A) = ζ . Èç ëåììû 1.6 ñëåäóåò, ÷òî ìû ìîæåìíàéòè k çà O(c(α)+c(β)) âðåìåíè. Òàêèì îáðàçîì, èç ëåììû 1.7 ñëåäóåò,÷òî ζ ìîæåò áûòü íàéäåí çà âðåìÿ O(c(α)+c(β)). Íåñëîæíî âèäåòü, ÷òîc(ζ) ≤ c(βk ) + 1 ≤ c(β).Äëÿ êàæäîãî îðäèíàëà α > 0 è öåëîãî ÷èñëà n ≥ −1 ìû îïðåäåëÿåì ìíîæåñòâî êîäîâ Cnα è ôóíêöèþ îöåíêè evnα : Cnα → P(Uαn ). Êàæ−1äîå ìíîæåñòâî C−1α ýòî ïðîñòî {0, 1}.
Ìû ïîëàãàåì evα (0) = ∅ ènev−1α (1) = {()}. Äëÿ n ≥ 0 ýëåìåíòû Cα ýòî òðîéêè, ñîñòîÿùèå èç:1. ÷èñëà m > 0;2. êîíå÷íîé ïîñëåäîâàòåëüíîñòè (A0 , . . . , Am−1 ), ãäå êàæäûé Ai ÿâëÿåòñÿ íåïóñòûì ïîëóèíòåðâàëîì [βi , γi ), ïðåäñòàâëåííûì â êà÷åñòâåïàðû hβi , γi i; äëÿ âñåõ i ìû èìååì βi 6∈ Lim,i < m − 1 ìû èìååì γi = βi+1 ;Si<mAi = [0, α) è äëÿ âñåõn−13. c0 ∈ Cn`(−1A0 ) , . . . , cm−1 ∈ C`(Am−1 ) .Ñ ôîðìàëüíîé òî÷êè çðåíèÿ, äëÿ n ≥ 0 ýëåìåíò d ∈ Cnα ÿâëÿåòñÿ òðîéêîéhm, A, ci. Çàäàäèì îòîáðàæåíèå evnα èç Cnα â P(Uαn ), êàê ïåðåâîäÿùååhm, A, ci â[{(β0 , β1 , . .
. , βn ) ∈ Uαn | β0 ∈ Ai , (β1 , . . . , βn ) ∈ evn`(−1Ai ) (ci )}.i<mÏóñòü A ÿâëÿåòñÿ ïîäìíîæåñòâîì Uαn è c ýòî ýëåìåíò Cnα òàêîé, ÷òîevnα (c) = A. Òîãäà ìû ãîâîðèì, ÷òî c ÿâëÿåòñÿ êîäîì äëÿ A.Äëÿ êàæäîãî öåëîãî ÷èñëà n ≥ −1 è îðäèíàëà α ∈ [1, ε0 ) ìû ââîäèì ôóíêöèþ wαn : Cnα → ω , ïåðåâîäÿùóþ êîä â åãî ¾øèðèíó¿ è ôóíêöèþ ocnα : Cnα → ω , ïåðåâîäÿùóþ êîä â åãî ¾îðäèíàëüíóþ ñëîæíîñòü¿,äëÿ èçìåðåíèÿ ñëîæíîñòè êîäîâ:1.
wα0 (c) = 1;2. wαn+1 (hm, A, ci) = max({m} ∪ {wαn (ci ) | i < m});3. oc0α (c) = 1;4. ocnα+1 (hm, A, ci) = max c(βi ) + max ocn`(Ai ) (ci ).i<mi<m26Ïóñòü äàëåå â ýòîì ðàçäåëå â ôîðìóëèðîâêàõ ëåìì n ýòî öåëîå÷èñëî áîëüøåå èëè ðàâíîå −1.Ëåììà 1.9.Ïóñòü c = hm, A, di ∈ Cnα è äëÿ âñåõ i < m, ïîëóèíòåðâàëAi = [βi , γi ). Òîãäà äëÿ âñåõ i < m ìû èìååì c(βi ) ≤ ocnα (c), c(γi ) ≤max(c(α), ocnα (c)), ocnα (di ) ≤ ocnα (c) è c(`(Ai )) ≤ max(c(α), ocnα (c)).Äîêàçàòåëüñòâî.
Ìû íåïîñðåäñòâåííîé ïðîâåðêîé ïîëó÷àåì, ÷òî âñåòðåáóåìûå íåðàâåíñòâà âûïîëíåíû. Ïîñëåäíåå âûâîäèòñÿ èç ëåììû1.8.Ëåììà 1.10.Îáúåì ïàìÿòè, òðåáóåìîé äëÿ õðàíåíèÿ êîäà c ∈ Cnα ,îöåíèâàåòñÿ ñâåðõó êàê O((ocnα (c) + c(α)) · (wαn (c))n ).Äîêàçàòåëüñòâî. Ïðîâåäåì ïðîâåðêó èíäóêöèåé ïî n ñ èñïîëüçîâàíèåìëåììû 1.9 è òîãî ôàêòà, ÷òî îðäèíàë β ìîæíî õðàíèòü â O(c(β)) ïàìÿòè.Ëåììà 1.11.Èìååòñÿ âû÷èñëèìàÿ ôóíêöèÿ IsEmpn (α, c) òàêàÿ, ÷òîíà àðãóìåíòàõ 0 < α < ε0 è c ∈ Cnα :1. IsEmpn âîçâðàùàåò 1, åñëè evnα (c) = ∅, è âîçâðàùàåò 0 èíà÷å;2. âðåìÿ ðàáîòû IsEmpn îöåíèâàåòñÿ êàêO(max(ocnα (c), c(α)) · (wαn (c))n ).Äîêàçàòåëüñòâî. Íåôîðìàëüíî, èäåÿ äîêàçàòåëüñòâ ñîñòîèò â òîì, ÷òîáû ïðîâåðèòü, ÷òî âñå C−1β -êîäû, èñïîëüçóåìûå â êîäå c ðàâíû 0.Ìû äîêàçûâàåì ëåììó èíäóêöèåé ïî n. Ïóñòü n = 0. Òîãäà äëÿäàííîãî α è c, ìû èìååì evnα (c) = ∅ â òîì è òîëüêî òîì ñëó÷àå, åñëèc = 0.
Ýòî äàåò íàì ôóíêöèþ IsEmp0 .Òåïåðü ìû ðàññìàòðèâàåì ñëó÷àé n > 0. Èç ëåììû 1.8 (ïóíêò3) ñëåäóåò, ÷òî äëÿ äàííîãî îðäèíàëà α è êîäà c = hk, A, di çíà÷åíèåevnα (c) = ∅ â òîì è òîëüêî òîì ñëó÷àå, åñëè äëÿ âñåõ i < k ìû èìååìn−1ev`(Ai ) (di ) = ∅. Ïðîâåðêà òîãî, ÷òî ïðàâàÿ ÷àñòü òðåáóåìîé ýêâèâàëåíò-íîñòè âûïîëíåíà, ìîæåò áûòü ïðîâåäåíà çà k âûçîâîâ ôóíêöèè IsEmpn−127ñ âåðõíåé îöåíêîé ïî âðåìåíè O(max(ocnα (c), c(α)) · (wαn (c))n−1 ). Ýòî äàåò íàì IsEmpn ñ âðåìåíåì ðàáîòû O(max(ocnα (c), c(α)) · (wαn (c))n ).Ëåììà 1.12.Èìååòñÿ âû÷èñëèìàÿ ôóíêöèÿ Cmpln (α, c) òàêàÿ, ÷òîíà àðãóìåíòàõ 0 < α < ε0 è c ∈ Cnα ìû èìååì:1.
Cmpln (α, c) ∈ Cnα ;2. evnα (Cmpln (α, c)) = Uαn \ evnα (c);3. ocnα (Cmpln (α, c)) = ocnα (c), wαn (Cmpln (α, c)) = wαn (c);4. âðåìÿðàáîòûCmplnìîæåòáûòüîöåíåíîñâåðõó,êàêO(max(ocnα (c), c(α)) · (wαn (c))n ).Äîêàçàòåëüñòâî. Íåôîðìàëüíî, èäåÿ ðàáîòû ýòîé ôóíêöèè ñîñòîèò âòîì, ÷òîáû çàìåíèòü íà îáðàòíûé êàæäîå âõîæäåíèå C−1β -êîäîâ, èìåþùååñÿ â êîäå c (ìû çàìåíÿåì êàæäûé 0 íà 1 è êàæäóþ 1 íà 0).Ìû äîêàçûâàåì ýòó ëåììó èíäóêöèåé ïî n.Ðàññìîòðèì ñëó÷àé n = −1. Ïóñòü ìû ïîëó÷èëè íà âõîä (α, c). Òîãäà ìû ïîëàãàåì Cmpl−1 (α, c) = 0, åñëè c = 1, è ïîëàãàåì Cmpl−1 (α, c) =1 èíà÷å.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
