¿Por qué son abstracciones lambda los únicos términos que son valores en el cálculo lambda sin tipo?

Question

Me gustaría saber la siguiente afirmación: "Los únicos valores en el cálculo lambda sin tipo son abstracciones lambda"

¿Por qué son los otros términos no valores? ¿Qué significa para un lambda-abstracción que es un valor? Lo primero que vino a mi mente fue que tal vez lambda-abstracciones son los únicos posibles formas normales, pero esto no es cierto, por supuesto, por ejemplo, $ (\ Lambda x \;. X) \;. Y \ a y $

Puede alguien me ilumine?

Answer 1

Hay una serie de cosas que suceden aquí:

• El idioma que se habla de no tiene ningún tipo de datos adicionales, de lo contrario no habría otros tipos de valores.
• La estrategia de reducción de la lengua no reduce el interior abstracciones lambda. Tanto llamada por valor y llamada por nombre cumpla con la presente. De lo contrario, no todos los abstracción lambda sería una normal.
• Un considera generalmente expresiones cerradas como los programas, por lo que no hay variables libres, de ahí el ejemplo presente no se considera.

Otros términos no son valores, ya que pueden ser reducidos o que no aparecen en los programas cerrados.

Que una abstracción lambda es un medio de valor que no se puede reducir más lejos (en función de la estrategia de reducción).

En términos abiertos, las variables son también valores.