son todos términos lambda simplemente tipados de tipo $(A\to A) \to A \to A$ ¿números de la iglesia?

Question

Los números de iglesia en los cálculos lambda son términos de la forma $\lambda f x . f(f(\cdots f(x) \cdots ))$ . En el cálculo lambda de tipado simple, estos numerales deben tener tipos de la forma $(A\to A) \to A \to A$ . ¿Es cierto lo contrario? ¿Debe cualquier término del tipo $(A\to A) \to A \to A$ ¿es un número de la Iglesia? ¿Igual que los booleanos de la Iglesia?

No se me ocurren contraejemplos y no veo muy bien cómo plantear la inducción en caso de ser cierta.

Answer 1

Depende de lo que se entienda por "de la forma". Trivialmente, puedo escribir $\lambda fx.(\lambda y.y)f x$ decir. Por supuesto, esto se reduce a $\lambda fx.fx$ . Así que, como señala DanielV, hay que considerar sólo las formas normales o los términos lambda hasta $\beta\eta$ -equivalencia o algo similar.

La siguiente cuestión es si $A$ es arbitraria. Por ejemplo, si $A$ resulta ser $B\to B$ decir, entonces $\lambda fx.(\lambda y.y)$ es un término lambda bien tipificado, pero no tiene la forma de ningún numeral de la Iglesia. Sin embargo, si $A$ es un tipo arbitrario y desconocido, entonces no hay manera de producir un término de tipo $A$ (de hecho, puede que no haya ninguno), excepto si se utiliza $x$ y $f$ . En este caso, los únicos términos de forma normal del tipo son los números de la Iglesia. Esto se puede formalizar considerando el cálculo lambda polimórfico (también conocido como Sistema F), y preguntando por los términos de forma normal de $\forall A.(A\to A)\to A\to A$ . Es un hecho bien conocido, pero no trivial, que cualquier tipo de datos algebraicos estrictamente positivos puede ser codificado sistemáticamente en el Sistema F preservando las propiedades esperadas. Esta codificación se denomina Codificación Böhm-Berarducci . Este artículo de Oleg Kiselyov puede servir de introducción más accesible.