¿Es innecesariamente complicada la codificación de números naturales de la Iglesia?

Question

El Estructura e interpretación de programas informáticos. El libro que he estado leyendo presenta los números de la Iglesia definiendo cero y una función de incremento.

zero: λf. λx. x
increment: λf. λx. f ((n f) x)

Esto me pareció bastante complicado y me llevó mucho tiempo resolverlo y derivar uno (λf.λx. f x) y dos (λf.λx. f (f x)).

¿No sería mucho más sencillo codificar números de esta manera, siendo el cero la lambda vacía?

zero: λ
increment: λf. λ. f

Ahora es trivial derivar uno (λ. λ) y dos (λ. λ. λ), etcétera.

Esta parece una forma mucho más obvia e intuitiva de representar números con lambdas.¿Hay algún problema con este enfoque y, por lo tanto, una buena razón por la cual los números de la Iglesia funcionan como lo hacen?¿Está ya atestiguado este enfoque?

Answer 1

Su codificación (cero: λx.x, uno: λx.λx.x, dos: λx.λx.λx.x, etc.) facilita la definición de incrementos y decrementos, pero más allá de eso, resulta bastante complicado desarrollar combinadores para su codificación.Por ejemplo, ¿cómo definirías isZero?

Una forma intuitiva de pensar en la codificación de la Iglesia es que un número n está representado por la acción de iterar n veces.Esto facilita el desarrollo de combinadores como plus simplemente usando la iteración codificada en el número.No se necesitan combinadores sofisticados para la recursividad.

En la codificación de la Iglesia, cada número tiene la misma interfaz:se necesitan dos argumentos.Mientras que en su codificación, cada número se define por la cantidad de argumentos que toma, lo que hace que sea realmente complicado operar de manera uniforme.

Otra forma de codificar números sería pensar en los números como n = 0 | S N, y use una codificación de vainilla para sindicatos.

Answer 2

La sintaxis propuesta para los numerales no es válida en el cálculo lambda, mientras que los numerales de Church son construcciones válidas en el cálculo lambda.Esa es una posible razón por la que los números de la Iglesia son como son: la codificación del número debe cumplir con el cálculo lambda definición de una manera que también permite que las operaciones adicionales también definidas en el cálculo lambda (incremento, por ejemplo) operen sobre los números codificados.