Lambda kalkul: Porovnání verzí

 

Problém určit, zda dva výrazy v lambda kalkulu jsou ekvivalentní, nemůže žádný univerzální [[algoritmus]] vyřešit a tento problém byl první, u kterého se nerozhodnutelnost podařilo dokázat. V důkazu tohoto faktu Alan Church nejprve problém zredukoval na určení, zda daný lambda výraz má nějakou ''normální formu'', přičemž takovou formou se míní ekvivalentní výraz, který nelze dále zjednodušit. Poté v rámci [[důkaz sporem|důkazu sporem]] předpokládá, že takový predikát je vyčíslitelný a lze ho tedy vyjádřit pomocí lambda kalkulu. S využitím předchozích Kleeneho výsledků dokázal lambda výrazům přiřadit [[Gödelovo číslo]] a poté obdobnou technikou jako v důkazu [[první Gödelova věta o neúplnosti|první Gödelovy věty o neúplnosti]] vytvořil lambda výraz ''e''. Konečně, pokud je ''e'' aplikováno samo na sebe (na své Gödelovo číslo), výsledkem je spor.

 

== Související články ==