def s(d): if r(d, d): q(b) else: p(a)
Ptejme se nyní, co udělá s(s)? Pokud s(s) řeší P, pak jej neřeší, protože se spustí q(b). Pokud jej však neřeší, pak jej řeší, protože se spustí p(a). V obou případech tedy dostáváme spor, což je další spor, a tedy program r nemůže existovat.
Pokud je formální systém tak složitý, že může zpracovávat kód jako datum (tzn. ani moc jednoduchý, ani moc složitý), pak není žádný problém rozhodnutelný. Na Halting Problému se to sice dobře ukazuje, ale nemyslím, že by obecný výše uvedený důkaz nějak komplikovaný. Tento důkaz není ani tak podobný Gödelovu/Rosserovu důkazu, protože tam je sebereference, která vede ke sporu s úplností, nikoli s její existencí. V tomto důkazu vede sebereference ke sporu s vlastní existencí. Z epistemického hlediska je tento důkaz podobný spíše diagonálnímu důkazu Cantorovu.
Přímým důsledkem této věty je fakt, že každý řešitelný problém lze řešit nekonečně mnoha navzájem velmi nepodobnými způsoby, jinými slovy, prostor pro kreativitu není omezen. Matematici tuto větu znají v podobě, která používá Gödelovo výrazivo: Množina kódů programu řešící nějaký problém je buď prázdná, nebo nerekursivní. Toto a mnohé jiné se můžete dočíst v připravované knize Michala Černého Výpočty: http://nb.vse.cz/~cernym/vypocty.pdf.
2 komentáře:
Děkuji za ujasnění a rozšíření obzorů :-)
No, není zač. Opomenul jsem zdůraznit, že jde jenom o nástin důkazu. Důkaz v celé své "kráse" tak krátký a přehledný pochopitelně není.
Okomentovat