Aritmética con números de iglesia

Question

Estoy trabajando a través de SICP, y el problem 2.6 me ha puesto en un dilema. Al tratar con los numerales de la Iglesia, el concepto de codificar cero y 1 como funciones arbitrarias que satisfacen ciertos axiomas parece tener sentido. Además, derivar la formulación directa de números individuales usando la definición de cero, y una función add-1 tiene sentido. No entiendo cómo se puede formar un operador plus.

Hasta ahora tengo esto.

(define zero (lambda (f) (lambda (x) x))) 
(define (add-1 n) 
    (lambda (f) (lambda (x) (f ((n f) x))))) 

(define one (lambda (f) (lambda (x) (f x)))) 
(define two (lambda (f) (lambda (x) (f (f x))))) 

Mirando a través de la entrada de Wikipedia para lambda calculus, he encontrado que la definición de ventaja era PLUS: = λmnfx.m f (n f x). Usando esa definición, pude formular el siguiente procedimiento.

(define (plus n m) 
    (lambda (f) (lambda (x) ((m f) ((n f) x))))) 

Lo que no entiendo, es cómo se puede derivar ese procedimiento directamente utilizando solo la información proporcionada por los procedimientos derivados anteriormente. ¿Alguien puede responder esto en algún tipo de forma de prueba rigurosa? Intuitivamente, creo que entiendo lo que está pasando, pero como dijo una vez Richard Feynman, "si no puedo construirlo, no lo puedo entender ..."

Answer 1

En realidad es bastante simple. Esto probablemente se verá como flamebait, pero los parens hacen que sea más difícil de ver: una mejor manera de ver lo que sucede es imaginar que estás en un lenguaje al curry, o simplemente usar el hecho de que Scheme tiene funciones de múltiples argumentos y abrazar esa ... He aquí una explicación que utiliza lambdas y argumento múltiple cuando sea conveniente:

• Cada número N se codifica como

  (lambda (f x) ...apply (f (f (f ... (f x)))) N times...) 
  

• Esto significa que la codificación de N es en realidad

  (lambda (f x) (f^N x)) 
  

  donde f^N es la exponenciación funcional.

• Una forma más sencilla de decir esto (currificación asumiendo): el número N se codifica como

  (lambda (f) f^N) 
  

  modo N es en realidad un "elevar a la potencia de N" función

• ahora tome su expresión (mirando dentro de la lambda s aquí):

  ((m f) ((n f) x)) 
  

  ya n se es una codificación de un número, es que la exponenciación, por lo que este es en realidad:

  ((m f) (f^n x)) 
  

  y lo mismo para m:

  (f^m (f^n x)) 
  

  y el resto debería ser obvio ... Tienes m aplicaciones de f aplicadas en n aplicaciones de f aplicadas en x.

• Por último, dejar algunos diversión - aquí es otra manera de definir plus:

  (define plus (lambda (m) (lambda (n) ((m add1) n)))) 
  

  (Bueno, no demasiado bien, ya que éste es probablemente más evidente.)

Answer 2

La respuesta de Eli es técnicamente correcta, pero dado que en el momento en que se formula esta pregunta, no se ha introducido el procedimiento #apply, no creo que los autores hayan querido que el alumno tenga conocimiento de eso o de conceptos tales como currying para poder responder a esta pregunta.

Bastante guían uno a la respuesta sugiriendo que uno aplique el método de sustitución, y desde allí uno debe notar que el efecto de la suma es una composición de un número en el otro. La composición es un concepto introducido en el ejercicio 1.42; y eso es todo lo que se necesita para comprender cómo un procedimiento aditivo puede funcionar en este sistema.

; The effect of procedure #add-1 on `one`, and `two` was the composition of `f` 
; onto `one` and `f` onto `two`. 
; 
; one : (λ (f) (λ (x) (f x))) 
; two : (λ (f) (λ (x) (f (f x)))) 
; three : (λ (f) (λ (x) (f (f (f x))))) 
; 
; Thus one may surmise from this that an additive procedure in this system would 
; work by composing one number onto the other. 
; 
; From exercise 1.42 you should already have a procedure called #compose. 
; 
; With a little trial and error (or just plain be able to see it) you get the 
; following solution. 

(define (adder n m) 
    (λ (f) 
    (let ((nf (n f)) 
      (mf (m f))) 
     (compose nf mf)))) 

Answer 3

^{(Asegúrese de entender higher-order functions).} En Alonzo Churchuntyped lambda calculus, una función es el único tipo de datos primitivo. No hay números, booleanos, listas o cualquier otra cosa, solo funciones. Las funciones pueden tener solo 1 argumento, pero las funciones pueden aceptar y/o devolver funciones, no valores de estas funciones, sino funciones mismas. Por lo tanto, para representar números, booleanos, listas y otros tipos de datos, debe encontrar una forma inteligente para que funciones anónimas los representen. Church numerals es la forma de representar natural numbers. Tres construcciones más primitivas en el cálculo lambda sin tipo son:

1. λx.x, una identity function, acepta alguna función e inmediatamente devuelve.
2. λx.x x, autoaplicación.
3. λf.λx.f x, aplicación de función, toma una función y un argumento, y aplica una función a un argumento.

¿Cómo se codifica 0, 1, 2 como nada más que funciones? De alguna manera necesitamos construir la noción de cantidad en el sistema. Solo tenemos funciones, cada función se puede aplicar solo a 1 argumento. ¿Dónde podemos ver algo parecido a la cantidad? ¡Oye, podemos aplicar una función a un parámetro varias veces! Obviamente hay una sensación de cantidad en 3 invocaciones repetidas de una función: f (f (f x)). Así que vamos a codificar en el cálculo lambda:

• 0 = λf.λx.x
• 1 = λf.λx.f x
• 2 = λf.λx.f (f x)
• 3 = λf.λx.f (f (f x))

Y así sucesivamente. ¿Pero cómo se pasa de 0 a 1, o de 1 a 2? ¿Cómo escribirías una función que, dado un número, devolvería un número incrementado en 1?Vemos el patrón en Números de la Iglesia que el término siempre comienza con λf.λx. y después de que tiene una aplicación repetida finita de f, así que tenemos que entrar de alguna manera en el cuerpo de λf.λx. y envolverlo en otro f. ¿Cómo se cambia un cuerpo de una abstracción sin reducción? Bueno, puedes aplicar una función, envolver el cuerpo en una función y luego envolver el nuevo cuerpo en la antigua abstracción lambda. Pero no desea que los argumentos cambien, por lo tanto, aplica abstracciones a los valores del mismo nombre: ((λf.λx.f x) f) x → f x, pero ((λf.λx.f x) a) b) → a b, que no es lo que necesitamos.

Por eso es add1λn.λf.λx.f ((n f) x): aplicar n a f y luego x para reducir la expresión al cuerpo, a continuación, aplicar f a ese cuerpo, entonces abstracta de nuevo con λf.λx.. Ejercicio: demasiado ver que es verdad, aprender rápidamente y reducir β-reduction(λn.λf.λx.f ((n f) x)) (λf.λx.f (f x)) al incremento de 2 por 1.

Ahora la comprensión de la intuición detrás de envolver el cuerpo en otra función de invocación, ¿cómo ponemos en práctica la adición de 2 números? Necesitamos una función que, dado λf.λx.f (f x) (2) y λf.λx.f (f (f x)) (3), devolvería λf.λx.f (f (f (f (f x)))) (5). Mire 2. ¿Qué pasaría si pudiera reemplazar su x con el cuerpo de 3, es decir f (f (f x))? Para obtener el cuerpo de 3, es obvio, simplemente aplíquelo al f y luego al x. Ahora aplique 2 a f, pero luego aplíquelo al cuerpo de 3, no a x. Luego envuélvalo en λf.λx. nuevamente: λa.λb.λf.λx.a f (b f x).

Conclusión: Para añadir los números 2 y ab juntos, ambos de los cuales se representan como números de la Iglesia, que desea reemplazar x en a con el cuerpo de b, de manera que f (f x) + f (f (f x)) = f (f (f (f (f x)))). Para que esto suceda, aplique a al f, luego al b f x.