¿Existe algún cálculo lambda tipificado completo de Turing? Si es así, ¿cuáles son algunos ejemplos?
computability
lambda-calculus
type-theory
Bola de nieve
fuente
fuente
Respuestas:
Si seguro. Muchos cálculos lambda mecanografiados aceptan solo términos fuertemente normalizados , por diseño, por lo que no pueden expresar cálculos arbitrarios. Pero un sistema de tipos puede ser lo que quieras; hazlo lo suficientemente amplio y podrás expresar todos los cálculos deterministas.
Un sistema de tipo trivial que abarca un fragmento completo de Turing del cálculo lambda es el que acepta todos los términos como bien tipados (con un tipo superior ).
Más prácticamente, los lenguajes de programación funcional tipados estáticamente tienen en su núcleo un cálculo lambda tipado que permite un combinador de punto fijo también tipado. Por ejemplo, comience con el cálculo lambda simplemente tipeado (o el sistema de tipo ML o el sistema F o cualquier otro sistema de tipo de su elección) y agregue una regla que haga algún combinador de punto fijo como bien escrito. Γ ⊢ f : T → TY=λf.(λx.f(xx))(λx.f(xx))
Las reglas presentadas anteriormente son bastante torpes, ya que hacen términos comoY
Siguiendo el cálculo lambda puro, un sistema de tipos interesante es el cálculo lambda con tipos de intersección.
Los tipos de intersección tienen propiedades interesantes con respecto a la normalización:
Consulte Caracterización de términos lambda que tienen tipos de unión para obtener una idea de por qué los tipos de intersección tienen un alcance tan notable.
Por lo tanto, tiene un sistema de tipos que define un lenguaje completo de Turing (ya que cada término está bien tipado) y una caracterización simple de los cálculos de terminación. Por supuesto, dado que este tipo de sistema caracteriza la normalización, no es decidible.
fuente