scheme - Aritmética con números de iglesia

sicp lambda-calculus

Question

Estoy trabajando a través del 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 codificar cero y 1 para que sean funciones arbitrarias que satisfagan 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 aquí 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 el cálculo lambda , encontré que la definición de más era MÁS: = λmnfx.mf (nfx). 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 contestar esto en una forma de prueba 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. Probablemente, esto se verá como un ataque de fuego, pero los parens hacen que sea más difícil de ver; una mejor manera de ver qué sucede es imaginar que estás en un lenguaje con curry o simplemente usar el hecho de que Scheme tiene funciones de múltiples argumentos y acepta eso ... Aquí hay una explicación que usa lambdas y argumentos múltiples 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 (suponiendo que se hace currying): el número N se codifica como

  (lambda (f) f^N)

  por lo que N es en realidad una función "elevar a la potencia de N"

• Ahora toma tu expresión (mirando dentro de las lambda s aquí):

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

  ya que n es una codificación de un número, es esa exponenciación, por lo que esto es en realidad:

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

  y lo mismo para m :

  (f^m (f^n x))

  y el resto debe ser obvio ... Usted tiene m aplicaciones de f aplicadas en n aplicaciones de f aplicadas en x .

• Finalmente, para dejar un poco de diversión, aquí hay otra forma de definir plus :

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

  (Bueno, no es muy divertido, ya que este es probablemente más obvio).

Answer 2

La respuesta de Eli es técnicamente correcta, pero dado que en el momento en que se #apply esta pregunta no se ha introducido el procedimiento de #apply , no creo que los autores pretendan que el estudiante tenga conocimiento de eso o de conceptos como el curry para poder Responde esta pregunta.

Ellos prácticamente guían a uno a la respuesta sugiriendo que uno aplique el método de sustitución, y luego desde allí uno debe notar que el efecto de la suma es una composición de un número sobre el otro. La composición es un concepto que se introdujo 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 que entiende las funciones de orden superior ) .} En el cálculo lambda no tipificado de Alonzo Church , una función es el único tipo de datos primitivos. 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 los valores de estas funciones, sino las funciones mismas. Por lo tanto, para representar números, valores booleanos, listas y otros tipos de datos, debe encontrar una forma inteligente de que las funciones anónimas los representen. Los números de la iglesia es la forma de representar los números naturales . Las tres construcciones más primitivas en el cálculo lambda sin tipo son:

1. λx.x , una función de identidad , acepta alguna función y la devuelve inmediatamente.
2. λx.xx , auto-aplicación.
3. λf.λx.fx , aplicación de función, toma una función y un argumento, y aplica una función a un argumento.

¿Cómo codificas 0, 1, 2 como nada más que funciones? De alguna manera necesitamos incorporar 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? ¡Hey, 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 (fx)) . Así que vamos a codificarlo en cálculo lambda:

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

Y así. ¿Pero cómo vas 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 los números de la Iglesia que el término siempre comienza con λf.λx. y después de que tengas una aplicación repetida finita de f , debemos ingresar al cuerpo de λf.λx. y envolverlo en otro f . ¿Cómo cambias 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 abstracción lambda antigua. Pero no desea que los argumentos cambien, por lo tanto, aplica abstracciones a los valores del mismo nombre: ((λf.λx.fx) f) x → fx , pero ((λf.λx.fx) a) b) → ab , que no es lo que necesitamos.

Es por eso que add1 es λn.λf.λx.f ((nf) x) : aplica n a f y luego x para reducir la expresión al cuerpo, luego aplica f a ese cuerpo y luego lo abstrae nuevamente con λf.λx. . Ejercicio: también vea que es cierto, aprenda rápidamente β-reduction y reduzca (λn.λf.λx.f ((nf) x)) (λf.λx.f (fx)) para incrementar 2 en 1.

Ahora que entendemos la intuición detrás de envolver el cuerpo en otra invocación de función, ¿cómo implementamos la suma de 2 números? Necesitamos una función que, dada λf.λx.f (fx) (2) y λf.λx.f (f (fx)) (3), devuelva λf.λx.f (f (f (f (fx)))) (5). Mira a 2. ¿Qué pasaría si pudieras reemplazar su x con el cuerpo de 3, eso es f (f (fx)) ? Para obtener el cuerpo de 3, es obvio, solo aplícalo en f y luego en x . Ahora aplique 2 a f , pero luego aplíquelo al cuerpo de 3, no a x . Luego envuélvelo en λf.λx. de nuevo: λa.λb.λf.λx.af (bfx) .

Conclusión: para sumar 2 números a y b , ambos representados como números de iglesia, desea reemplazar x en a con el cuerpo de b , de modo que f (fx) + f (f (fx)) = f (f (f (f (fx)))) . Para hacer que esto suceda, aplique a a f , luego a bfx .