{{TOC float}}

{{Sources| Tohle je poněkud obšírnější výcuc ke státnicovým okruhům z vyčíslitelnosti pro obory Matematická lingvistika a Softwarové systémy, pocházející ze Strojilových skript, papírových zápisků A. Kazdy a zápisků z předmětu Vyčíslitelnost I ze Studnice -- Tuetschek 14:01, 17 Aug 2010 (CEST)

}}

Věty o rekurzi

Věta (O rekurzi, o pevném bodě, self-reference)

Jestliže <math> f\,\!</math> je ČRF jedné proměnné, potom existuje <math> a\,\!</math> takové, že <math> \varphi_{f(a)}(x)\simeq \varphi_a(x)\,\!</math> pro všechna <math> x\,\!</math> (kde <math> \varphi_a(x)\,\!</math> značí <math> a\,\!</math>-tou funkci, tedy odpovídá <math> \Psi_1(a,x)\,\!</math>).

Důkaz

Zjevně platí (první výraz je ČRF, má tedy své číslo <math> e\,\!</math>, druhé plyne ze S-m-n věty):

:<math> \lambda z,\!x (\varphi_{f(s_1(z,z))}(x)) \simeq \Psi_2(e,z,x) \simeq \varphi_{s_1(e,z)}(x) </math> Dosadíme <math> z=e\,\!</math> a dostáváme hledané <math> a=s_1(e,e)\,\!</math>. Platí totiž <math> \varphi_{f(s_1(e,e))}(x) \simeq \Psi_2(e,e,x) \simeq \varphi_{s_1(e,e)}(x). </math>

Vlastnosti programů <math>a</math> a <math>f(a)</math>

Funkce <math> f\,\!</math> zobrazuje program na program. Bod <math> a\,\!</math> je pevný bodem zobrazení <math> f\,\!</math>. Jak vypadají programy <math> a\,\!</math> a <math> f(a)\,\!</math>? Který z nich počítá déle? Uvidíme, že program <math> a\,\!</math> počítá déle, než <math> f(a)\,\!</math>.

Co dělá program <math> e\,\!</math> na datech <math> (z,x)\,\!</math>? Počítá <math> \varphi_{f(s_1(z,z))}\,\!</math>, tj. vezme <math> z\,\!</math> a spočítá neprve <math> s_1(z,z)\,\!</math>, potom <math> f(s_1(z,z))\,\!</math>, který ale nemusí konvergovat. Jestliže <math> f(s_1(z,z))\!\!\downarrow\,\!</math>, spustí se na vstup <math> x\,\!</math>.

Co dělá program <math> a\,\!</math>? Program <math> a\,\!</math> vznikne jako <math> s_1(e,e)\,\!</math>. Mějme na vstupu <math> x\,\!</math>. Program <math> a\,\!</math> vezme <math> e\,\!</math> a přidá ho k <math> x\,\!</math> a spustí program <math> e\,\!</math> na <math> (e,x)\,\!</math>. Co udělá program <math> e\,\!</math> na těchto datech? Spočítá <math> s_1(e,e)\,\!</math> (tedy spočítá <math> a\,\!</math>), potom <math> f(s_1(e,e))=f(a)\,\!</math> a spustí program <math> f(a)\,\!</math> na <math> x\,\!</math>.

Program <math> a\,\!</math> tedy neprve spočítá <math> a\,\!</math>, potom spočítá <math> f(a)\,\!</math> (pokud konverguje) a ten simuluje na vstupu <math> x\,\!</math>. Program <math> a\,\!</math> je tedy složitější než <math> f(a)\,\!</math> a počítá déle.

Poznámka z <math>\lambda</math>kalkulu

V <math>\lambda</math>kalkule sa ekvivalentné tvrdenie ukazuje trošku jednoduchšie. Pre každý <math>\lambda</math>term <math>F</math> (program <math>F</math>) existuje <math>\lambda</math>term <math>X</math> taký, že <math>X = FX</math> (program <math>F</math> aplikovaný na <math>X</math> sa rovná <math>X</math>).

Dôkaz je nasledovný *Majme <math>F</math>, pre ktoré chceme nájsť jeho pevný bod X.

*Nech <math>W = \lambda x.F(xx)</math> (to je funkcia, ktorá <math>x</math> priradí <math>F(xx)</math>). *<math>X = WW</math> (to môžeme chápať ako program/funkciu <math>W</math> aplikovaný na <math>W</math>)

*<math>X = WW = (\lambda x.F(xx)) W = F(WW) = F(X)</math> (tretia rovnosť je <math>\beta</math>pravidlo <math>\lambda</math>kalkulu. Ak si ale <math>(\lambda x.F(xx)) W</math> predstavíme ako funkciu, ktorá <math>x</math> priradí <math>F(xx)</math> aplikovanú na <math>W</math>, rovnosť je (snáď) jasnejšia).

Věta (O generování pevných bodů)

Pro každou <math> f \in \mbox{ČRF}\,\!</math> existuje prostá rostoucí PRF <math> g\,\!</math> taková, že platí:

:<math>\varphi_{f(g(j))}(x)\simeq\varphi_{g(j)}(x)\,\!</math>

Tedy <math> g\,\!</math> rostoucím způsobem generuje nekonečně mnoho pevných bodů funkce <math> f\,\!</math>.

Důkaz

Postupujeme stejně jako v důkazu předchozí věty, jen máme o proměnnou (parametr <math> j\,\!</math> funkce <math> g\,\!</math>) navíc, tj. platí <math> \varphi_{f(s_2(z,z,j))}(x)\simeq\Psi_3(e,z,j,x)\simeq\varphi_{s_2(e,z,j)}(x)\,\!</math>. Zvolme <math> g(j)=s_2(e,e,j)\,\!</math>.

Věta (Jiná forma věty o rekurzi)

Nechť <math> h\,\!</math> je ČRF <math> n+1\,\!</math> proměnných. Potom existuje číslo <math> a\,\!</math> takové, že <math> a\,\!</math> je indexem funkce <math> \lambda{x_1,\ldots,x_n} h(a,x_1,\ldots,x_n)\,\!</math>, tedy platí <math> \varphi_a(x_1,\ldots,x_n)\simeq h(a,x_1,\ldots,x_n)\,\!</math>.

Důkaz

<math>h(v,x_1,\ldots,x_n)\simeq \Psi_{n+1}(b,v,x_1,\ldots,x_n)\simeq \varphi_{s_1(b,v)}(x_1,\ldots,x_n)</math>

Následně aplikujeme větu o rekurzi na <math> s_1(b,v)\,\!</math> v proměnné <math> v\,\!</math> a dostáváme hledané <math> a\,\!</math> (podle VR platí: <math> \exists v: \varphi_{s_1(b,v)}\simeq \varphi_{v}\,\!</math>).

Věta (O rekurzi v závislosti ma parametrech)

Jestliže <math> f\,\!</math> je ČRF <math> m+1\,\!</math> proměnných, potom existuje PRF <math> h\,\!</math> o <math> m\,\!</math> proměnných taková, že platí:

:<math>\varphi_{f(h(y_1,\ldots,y_m),y_1,\ldots,y_m)}(x)\simeq \varphi_{h(y_1,\ldots,y_m)}(x)\,\!</math>

Důkaz

Pro <math> m=0\,\!</math> je to totéž jako verze bez parametrů. <math> h\,\!</math> nachází pevné body v závislosti na parametrech. Podobně jako v předchozích větách platí: <math> \varphi_{f(s_{m+1}(z,z,y_1,\ldots,y_m),y_1,\ldots,y_m)}(x) \simeq \Psi_{m+2}(e,z,y_1,\ldots,y_m,x) \simeq \varphi_{s_{m+1}(e,z,y_1,\ldots,y_m)}(x)\,\!</math>. Zvolme <math> h(y_1,\ldots,y_m)=s_{m+1}(e,e,y_1,\ldots,y_m)\,\!</math>.

Riceova věta

Věta (Rice)

Jestliže <math> \mathcal{A}\,\!</math> je třída ČRF (jedné proměnné), která je netriviální (nejsou to všechny funkce a není prázdná), potom indexová množina <math> A_{\mathcal{A}} = \{ x : \varphi_x \in \mathcal{A}\}\,\!</math> je nerekurzivní.

Důkaz

Sporem. Nechť <math> A\,\!</math> je rekurzivní. Potom lze vytvořit ORF <math> f\,\!</math> takovou, že všechny prvky z <math> A\,\!</math> zobrazí na nějaký prvek <math> b \notin A\,\!</math> a všechny prvky mimo <math> A\,\!</math> zobrazí na nějaký prvek <math> a \in A\,\!</math>. Podle věty o rekurzi existuje pevný bod <math> f\,\!</math> <math> u_0\,\!</math>, tedy platí:

:<math> \varphi_{u_0}=\varphi_{f(u_0)} \,\!</math>

Takže:

:<math> u_0 \in A \Rightarrow f(u_0)=b \notin A</math> :<math>u_0 \notin A \Rightarrow f(u_0)=a \in A </math>

To je ovšem spor, protože <math> u_0\,\!</math> a <math> f(u_0)\,\!</math> jsou indexy stejné funkce, a tedy buď obě čísla v <math> A\,\!</math> leží nebo obě neleží.

Důsledky

Pozor, nejedná se o třídu programů, ale třídu funkcí. Tedy i pro jednoprvkovou <math> \mathcal{A}\,\!</math> bude <math> A_{\mathcal A}\,\!</math> nekonečná a nerekurzivní (každá funkce je vyčíslovaná nekonečně mnoha programy a rozhodnout o jejich ekvivalenci je nelze efektivně).

Proto platí:

  • Nechť <math> \mathcal{A}=\{\varphi_e\}\,\!</math>, potom <math> A=\{x:\varphi_x=\varphi_e\}\,\!</math> je nerekurzivní.

  • Rozhodnout o rovnosti funkcí vyčíslovaných dvěma programy nelze algoritmicky.

{{Statnice I3}}