Aritmética con números Iglesia

Question

Estoy trabajando a través SICP, y el problema 2.6 me ha puesto en una especie de dilema. Al tratar con los números de la Iglesia, el concepto de codificación de cero y 1 para ser funciones arbitrarias que satisfagan ciertos axiomas parece tener sentido. Además, derivando la formulación directa de números individuales utilizando la definición de cero, y una función de complemento 1 tiene sentido. No entiendo cómo se puede formar un operador de suma.

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 cálculo lambda , he encontrado que la definición de ventaja era PLUS: = ?mnfx.mf (nfx). Usando esta definición yo era capaz de formular el siguiente procedimiento.

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

Lo que no entiendo, es la forma en que el procedimiento se puede derivar directamente utilizando sólo la información dada por los procedimientos previamente derivados. ¿Alguien puede responder a esto en algún tipo de prueba-como forma rigurosa? Intuitivamente, creo que entiendo lo que está pasando, pero como Richard Feynman dijo una vez: "Si no puedo construirlo, no puedo entenderlo ..."

Answer 1

En realidad es bastante simple. Esto probablemente será visto como flamebait, pero los parens hacen que sea más difícil de ver - una mejor manera de ver lo que sucede o bien se imagina que estás en un lenguaje al curry, o simplemente utiliza el hecho de que el esquema tiene funciones múltiples argumentos y abrazo que ... 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 exponenciación funcional.

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

  (lambda (f) f^N)
  

  N por lo que es en realidad un "subida al poder de la N" , función

• Ahora tome su expresión (mirando dentro de los lambdas aquí):

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

  ya es n 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 ... Usted tiene aplicaciones m de f aplican en las aplicaciones de n f aplicado 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

^{(asegúrese de que entiende funciones de orden superior ) .} En Alonzo Church 's sin tipo cálculo lambda es una función del tipo de datos sólo primitivo. No hay números, booleanos, listas o cualquier otra cosa, sólo funciona. Las funciones pueden tener sólo un 1 argumento, pero las funciones se pueden aceptar y / o devolver los valores de las funciones no de estas funciones, pero las funciones mismos. Por lo tanto, para representar números, booleanos, listas y otros tipos de datos, se debe llegar a una forma inteligente de funciones anónimas a presentarse a ellos. números Iglesia es la manera de representar números naturales . Tres mayoría de las construcciones primitivas en el cálculo lambda sin tipo son:

1. λx.x, un identidad función , acepta alguna función e inmediatamente vuelve a él.
2. λx.x x, la auto-aplicación.
3. λf.λx.f x, aplicación de función, toma una función y un argumento, y se aplica una función a un argumento.

¿Cómo se codifica 0, 1, 2 como nada más que funciones? De alguna manera necesitamos para construir la noción de cantidad en el sistema. Tenemos únicas funciones, cada función se puede aplicar sólo a 1 argumento. ¿Dónde podemos ver la cantidad algo parecido? Hey, podemos aplicar una función de un parámetro varias veces! Obviamente, hay un sentido de la 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 ir de 0 a 1, o de 1 a 2? ¿Cómo se escribe una función que, dado un número, se devolverá un número incrementado en 1? Vemos el patrón de números de la Iglesia que el término comienza siempre con λf.λx. y después de tener un finita aplicación repetida de f , por lo que tenemos que conseguir de alguna manera en el cuerpo de λf.λx. y se envuelve en otra f. ¿Cómo se cambia un cuerpo de una abstracción sin reducción? Bueno, se puede aplicar una función, envolver el cuerpo en una función, y luego envuelva el nuevo cuerpo en el viejo abstracción lambda. Pero no desea que los argumentos para el cambio, por lo tanto, aplicar las 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

Es por eso que 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: también ver que es verdad, aprender rápidamente ß-reducción y reducir (λ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 poner en práctica la adición de 2 números? Necesitamos una función que, dada λf.λx.f (f x) (2) y λf.λx.f (f (f x)) (3), volvería λf.λx.f (f (f (f (f x)))) (5). Vistazo a 2. ¿Y si pudiera reemplace su x con el cuerpo de 3, que es f (f (f x))? Para que el cuerpo de 3, es obvio, solo se aplica a f y luego x. Ahora aplique 2 a f, pero luego aplicarlo al cuerpo de 3, que no x. entonces wrAP en λf.λx. nuevo:. λa.λb.λf.λx.a f (b f x)

Conclusión: Para añadir 2 números a y b juntos, ambos de los cuales se representan como números de la Iglesia, que desea reemplace x en a con el cuerpo de b, de modo que f (f x) + f (f (f x)) = f (f (f (f (f x)))). Para que esto suceda, se aplica a a f, a continuación, a b f x.

Answer 3

La respuesta de Eli es técnicamente correcto, pero ya en el punto que se hizo esta pregunta el procedimiento #apply no se ha introducido, no creo que los autores pretenden que el estudiante tenga conocimiento de éste o de conceptos tales como currying estar capaz de responder a esta pregunta.

Ellos prácticamente guía uno a la respuesta al sugerir que uno se aplica el método de sustitución, y luego desde allí se debe notar que el efecto de la adición es una composición de una serie sobre el otro. Composición es un concepto fue introducido en el ejercicio 1,42; y eso es todo lo que se requiere para entender cómo un procedimiento aditivo puede trabajar 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))))