=Vety o rekurzi a jejich aplikace, Riceova veta (6×🎓)=
{{Zkazky|
* '''Věta o rekurzi a její aplikace (2013)''' - Zkoušejícího zajímalo znění, důkaz (preferoval ten přes s-m-n větu, ale spokojil se i s diagonalizačním), aplikace (Riceova věta a její znění, existence množin jako <math>W_x=\{x\}</math> s důkazem).
* '''Věty o rekurzi, Riceova věta (2009)''' - Napsal jsem základní větu, generování pevných bod a větu o rekurzi v závislosti na parametrech (vše samozřejmě s těmi jednoduchými důkazy). Napsal jsem Riceovu větu a její důkaz plynoucí ze základní věty o rekurzi. Ptal se mě odkud plynou důkazy, odpovědel jsem, že z Kleeneho věty a s.m.n. Pak se ještě ptal na trochu jinou verzi "Věty o programu co vypíše sám sebe", tam jsem trochu tápal, ale intuitivně jsem věděl (tu větu jsem znal, bohužel jsem ji neuvedl).
* '''vety o rekurzi (2009, Mlcek)''' - Ze zacatku jsme se bavili o tom, co jsem si pripravil, pak se to stocilo nekam, kde uz jsem se moc nechytal, ale prislo mi, ze mi spis chtel ukazat, jak se ty vety taky daj taky hezky a elegantne pouzit pro dukaz ruznejch kuriozit, takze to pak byla spis takova prednaska. Bohuzel jsem byl v takovym rozpolozeni, ze jsem si z ni moc neodnes :-) Kazdopadne docela pohoda.
* '''Vety o rekurzii a ich aplikacie (2009, Mlcek)''' - Napisal som 2 z 3 zakladnych viet. Ukazal som ako sa to pouzije pri dokaze Rice. Samozrejme nasledovala otazka na 3. z viet o rekurzii (resp. pevnom bode), co vlastne viedlo na program, ktory na kazdom vstupe vypise vlasny program. Aj ked som nebol 100%-tny vo vsetkom, tiez prijemne skusanie
* '''Vety o rekurzi a jejich dusledky (+ Riceova veta) (2009, Mlcek)''' Formuloval jsem a dokazal Vo pevnem bode, Vo generovani PB a Riceovu vetu (+ jeji dusledek). Dale to uz byl jen dialog jak se daji ty vety aplikovat (program co vypise svuj kod). Dalsi otazky jako co je to ze predikat Psi e x konverguje - rek. spoc. (halting problem), co je to mna K, Ko, jejich ekvivalence (jiz bez dukazu jen ustne).
* '''Vety o rekurzii (2008,Mlček)''' - pre mňa najťažšia otázka, našťastie som si fotograficky zapamätal dôkaz Riceovej vety a niektoré vety o rekurzii, takže ma nevyhodil
}}
{{theorem
| ∀ ORF ''f'' ∃ ''n'': ''φₙ ≃ φ<sub>f(n)</sub>''
| VoR
}}
: 💡 ∀ ORF transformacni funkci algoritmu f ∃ n tak že oba TS počítají stejnou fci (mají stejný algoritmus)
: 💡 n se říká pevný bod f
; Dk (přes s-m-n větu)
: Nechť ''e''₁ je číslem funkce, pro kterou platí ''φₑ₁''(''e, x'')'' ≃ φ<sub>f</sub>''<sub>(''φₑ''(''e''))</sub>(''x'')'','' (tuto funkci bychom snadno odvodili pomocí univerzální ČRF).
: Nechť ''b'' je Gödelovým číslem funkce ''s¹₁''(''e₁, e''), podle s-m-n věty tedy platí, že :
: ''φ<sub>φ<sub>b</sub></sub>''<sub>(''e'')</sub>(''x'')'' <math>\stackrel{\text{dosadím s¹₁}}{≃}</math> φ<sub>s₁¹</sub>''<sub>(''e₁, e'')</sub>(''x'')'' <math>\stackrel{\text{obrácená sᵐₙ}}{≃}</math> φₑ₁''(''e, x'')'' <math>\stackrel{\text{dosadím e₁ = f(φₑ(e))}}{≃}</math> φ<sub>f</sub>''<sub>(''φₑ''(''e''))</sub>(''x'')
: Protože ''φ<sub>b</sub>'' je PRF (podle s-m-n), je ''φ<sub>b</sub>''(''b'')''↓'' a platí, že ''φ<sub>φ<sub>b</sub></sub>''<sub>(''b'')</sub>'' ≃ φ<sub>f</sub>''<sub>(''φ<sub>b</sub>''(''b''))</sub>'','' ''φ<sub>b</sub>''(''b'') je tedy hledaným pevným bodem ''f''.
{{TODO|doplnit poznámky}}
===Důsledky VoR===
{{theorem
| ∃ prostá PRF <math>g</math>, která ke GČ funkce <math>f</math> určí její pevný bod
| 💡
}}
{{theorem
| ∀ ORF <math>f</math> má ∞ pevných bodů
| 💡
}}
{{theorem
| ∃ <math>n ∈ N</math>, pro nějž:
# <math>W_n = \{n\}</math>
# <math>φ_n ≃ λx[n]</math>
| 💡
}}
; Dk:
# Nechť <math>e</math> je Gödelovo číslo funkce definované jako <math>φ_e^{(2)}(x, y) ≃ μz[x = y]</math> (💡 tedy <math>φ_e^{(2)}(x, y)↓</math> ⇔ <math>x = y</math>). Použijeme s-m-n větu a definujeme-li <math>f(x) ≃ s_1^1(e, x)</math>, dostaneme, že <math>φ_{f(x)} ≃ φ_{s-1-1(e,x)} ≃ φ_e(x, y)</math> a tedy <math>W_{f(x)} = \{x\}</math>. Funkce <math>f</math> je ORF (podle s-m-n), a tak podle VoR: <math>∃ n: φ_n ≃ φ_{f(n)}</math>, a tak <math>W_n = W_{f(n)} = \{n\}</math>.
# Podobně, nechť <math>e</math> je GČ funkce definované jako <math>φ_e^{(2)}(x, y) ≃ x</math>. Pomocí s-m-n věty definujeme-li <math>f(x) = s_1^1(e, x)</math>, dostaneme <math>φ_{f(x)}(y) ≃ x</math> a s použitím VoR nalezneme <math>n</math>, pro něž je <math>φ_n(y) ≃ φ_{f(n)}(y) ≃ n</math>.
{{theorem
| <math>f(x,y)</math> je ORF <math>⇒ ∃</math> prostá ORF <math>n(y)</math> taková, že <math>φ_{n(y)} ≃ φ_{f(n(y),y)} ∀y ∈ N</math>
| VoR s parametry
}}
==Riceova v. - dk s VoR==
{{theorem
| <math>\cal C</math> třída ČRF, <math>A_\cal C = \{e | \varphi_e ∈ C\}</math> je RM ⇔ <math>\cal C = \emptyset</math> nebo <math>\cal C</math> obsahuje všechny ČRF
| Rice
}}
💡 <math>A_\cal C</math> je mnozina indexů (Gödel.č.) funkci z třídy <math>\cal C</math>
;Dk (sporem)
: předpokládejme že <math>\cal C</math> NEní ∅ a <math>\cal C</math> NEobsahuje všechny ČRF
: předpokládejme sporem že <math>A_\cal C</math> je rekurzivní
: definujme si fci <math>f</math>:
:: <math>f(x) = a ~~ x∉ A_\cal C</math>
:: <math>f(x) = b ~~ x∈ A_\cal C</math>
::: <math>f</math> je ORF
::: <math>a∈A_\cal C</math>
::: <math>b∉ A_\cal C</math>
: <math>n</math> je pevný bod <math>f</math> a <math>φ_n≃ φ_{f(n)}</math>
: <math>φ_n∈\cal C ⇒ n ∈ A_\cal C ⇒ f(n)=b ⇒ f(n)∉ A_\cal C ⇒ φ_{f(n)} ∉ \cal C</math>
: <math>φ_n∉\cal C ⇒ n ∈ A_\cal C ⇒ f(n)=a ⇒ f(n)∈ A_\cal C ⇒ φ_{f(n)}∈ \cal C</math>
: ⇒ '''spor'''
{{collapse|1=Dk (pomocí převoditelnosti)|2=
: předpokládejme že <math>\cal C</math> NEní ∅ a <math>\cal C</math> NEobsahuje všechny ČRF
: ukážeme sporem že <math>K ≤_1 A_\cal C</math>
: <math>e_0</math> je GČ fce nedefinové pro žádný vstup a <math>φ_{e0} ∈ \overline{\cal C}</math>
: <math>e_1</math> je GČ fce <math>φ_{e1}∈C</math> a <math>φ_{e0}≄ φ_{e1}</math>
: <math>\varphi_{e_2}(x, y)\simeq\cases{ \varphi_{e_1}(y)&je-li $x\in K$\cr \uparrow }</math>
:: <math>φ_{e2}(x , y) ≃ φ_{s^1_1}(e, x) (y) ≃ φ_{f(x)}(y)</math>
: <math>x∈K ⇒ φ_{f(x)}≃φ_{e1} ⇒ φ_{f(x)}(y) ∈ C ⇒ f(x) ∈ A_\cal C</math>
: <math>x∉K ⇒ φ_{f(x)}≃φ_{e0} ⇒ φ_{f(x)}(y) ∉ C ⇒ f(x)∉ A_\cal C</math>
:: tedy <math>x ∈ K ⇔ f(x) ∈ Ac</math>
}}
{{Statnice I2}}
