Términos lambda "activo" e "inactivo" e Iglesia.

Question

En el estudio histórico sobre el cálculo lambda y los combinadores Historia del lambda-cálculo y de la lógica combinatoria de Cardone y Hindley, leemos:

(El nombre de Church se asocia a menudo con el λI-cálculo, la versión del λ-cálculo en el que λx.M sólo se cuenta como término cuando x aparece pero no se limitó tan estrictamente a esta versión como se suele pensar. se suele pensar. En 1932 y '33 permitió que los términos no λI λx.M existir pero no ser "activos", es decir, no permitió que un término (λx.M)N se se contrajera cuando x no ocurriera libre en M, véase [Church, 1932, pp. 352, 355]. En su trabajo de 1940 sobre la teoría de tipos, donde la consistencia de los tipos, en el que la consistencia era menos dudosa, aunque probablemente no se haya demostrado estaba contento de que los términos no-λI estuvieran activos [Church, 1940, pp. 57, 60]. Sólo en su libro de 1941 prohibió su propia existencia [Church, 1941, p. 8].)

¿Puede alguien arrojar luz sobre por qué esos términos se permiten o no, o se consideran "activos" o no, es una cuestión importante?

Answer 1

Como mencioné en mi comentario, el $\lambda I$ El cálculo está íntimamente relacionado con lógica de la relevancia . Como se puede ver en esa página de Wikipedia, este era un tema que interesaba a Alonzo Church. Sin embargo, esta conexión es menos fuerte en un contexto no tipificado.

La segunda parte de mi comentario pretende sugerir las propiedades metateóricas $\lambda I$ tiene que el normal $\lambda$ el cálculo no lo hace. Dado que $\lambda I$ sigue siendo Turing-completo (como diríamos hoy en día), estas propiedades meta-lógicas más simples son convenientes. Esta respuesta discute brevemente algunas de esas propiedades metateóricas haciendo referencia a una breve discusión de $\lambda I$ en "The Lambda Calculus: Its Syntax and Semantics" de Barendregt.

Si eliminamos el requisito de que $x$ es gratis en $M$ en $\lambda x.\!M$ pero compensamos haciendo $(\lambda x.\!M)N$ no reducible (si $M$ y $N$ son irreducibles), entonces se convierte en una forma normal, y mantenemos al menos algunas de las propiedades metateóricas mientras aflojamos un poco la sintaxis. En particular, este cambio mantiene la propiedad, discutida en la respuesta mencionada, de que si un término $T$ tiene una forma normal, entonces también la tienen todos sus subterráneos. Obsérvese que esto no es cierto en el $\lambda$ cálculo. Por ejemplo, con el término $(\lambda x.\!\lambda y.\!y)((\lambda w.\!ww)(\lambda w.\!ww))$ que tiene la forma normal $\lambda y.\!y$ aunque $(\lambda w.\!ww)(\lambda w.\!ww)$ no tiene forma normal. Si desautorizamos el $\beta$ -reducción que implica $x$ , entonces el término no tiene forma normal.