{{TOC float}}

{{Sources| Tohle je poněkud obšírnější výcuc ke z pro obory a , 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 -- 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 ORF{{ref|1}} 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í následující -- první výraz je ČRF, má tedy své číslo <math> e\,\!</math>, druhá rovnost 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ým 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 ORF{{ref|1}} <math>f</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 (O rekurzi pro více proměnných)

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

Důkaz

<math>f(y,x_1,\ldots,x_n)\simeq \Psi_{n+1}(e,y,x_1,\ldots,x_n)\simeq \varphi_{s_1(e,y)}(x_1,\ldots,x_n)</math>

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

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

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

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

Důkaz

Pro <math> n=0\,\!</math> je to totéž jako verze bez parametrů. <math> g\,\!</math> nachází pevné body v závislosti na parametrech. Podobně jako v předchozích větách platí: <math> \varphi_{f(s_{n+1}(z,z,y_1,\ldots,y_n),y_1,\ldots,y_n)}(x) \simeq \Psi_{n+2}(e,z,y_1,\ldots,y_n,x) \simeq \varphi_{s_{n+1}(e,z,y_1,\ldots,y_n)}(x)\,\!</math>. Zvolme <math> g(y_1,\ldots,y_n)=s_{n+1}(e,e,y_1,\ldots,y_n)\,\!</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> (indexy programů, které vyčíslují funkce z <math>\mathcal{A}</math>) je nerekurzivní.

Důkaz

Sporem. Nechť <math> A_{\mathcal{A}}\,\!</math> je rekurzivní. Potom lze vytvořit ORF <math> f\,\!</math> takovou, že všechny prvky z <math> A_{\mathcal{A}}\,\!</math> zobrazí na nějaký prvek <math> b \notin A_{\mathcal{A}}\,\!</math> a všechny prvky mimo <math> A_{\mathcal{A}}\,\!</math> zobrazí na nějaký prvek <math> a \in A_{\mathcal{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_{\mathcal{A}} \Rightarrow f(u_0)=b \notin A_{\mathcal{A}}</math> :<math>u_0 \notin A_{\mathcal{A}} \Rightarrow f(u_0)=a \in A_{\mathcal{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_{\mathcal{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 nelze efektivně).

Proto platí:

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

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


{{note|1|Věta platí i pro ČRF, s využitím toho, že ani jedna ze stran <math>\simeq</math> nemusí dávat smysl, aby výraz platil.}}

{{Statnice I3}}