Diferencia entre revisiones de «Cálculo lambda»

No hay un algoritmo que tome dos expresiones lambda y produzca <tt>TRUE</tt> o <tt>FALSE</tt> dependiendo de si las dos expresiones son o no equivalentes. Éste fue históricamente el primer problema para el cual la irresolubilidad pudo ser probada. Por supuesto, de manera previa para hacer esto, la noción de [[algoritmo]] tuvo que ser definida de forma clara; Church la definió usando funciones recursivas, la cual se sabe que es equivalente a todas las otras rasonables definiciones razonables de esta noción.

La primera prueba de Church reduce el problema de determinar si una expresión lambda dada tiene una ''forma normal''. Una forma normal es una expresión equivalente irreductible. Entonces élse asume que éste predicado es computable y que puede ser expresado de aquí en adelante en notación de cálculo lambda. Building on earlier work by Kleene and constructing a [[Gödel numbering]] for lambda expressions, he constructs a lambda expression <tt>''e''</tt> which closely follows the proof of [[Gödel's incompleteness theorem|Gödel's first incompleteness theorem]]. If <tt>''e''</tt> is applied to its own [[Gödel number]], a contradiction results.