el numeral Iglesia para la adición

Question

Estoy atascado hacia el siguiente paso. Será genial si alguien me puede ayudar:

2 = λfx.f(f x)
3 = λfx.f(f(f x))
ADD = λm n f x. m f (n f x)

Mis pasos son los siguientes:

   (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
-> ((λn f x. (λf x.f(f(f x))) f (n f x))) (λf x.f(f x))
-> ((λf x. (λf' x'.f'(f'(f' x'))) f ((λf" x".f"(f" x")) f x)

¿Es la multa paréntesis? Realmente confundirme en las sustituciones y paréntesis. ¿Hay una, más fácil técnica formal para abordar este tipo de problemas?

Answer 1

Trate cocodrilo huevos!

Aquí están mis pasos, que me deriva con la ayuda de cocodrilo Huevos:

ADD 2 3
-> (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
->   (λn f x. (λf x.f(f(f x))) f (n f x))   (λf x.f(f x))
->     (λf x. (λf x.f(f(f x))) f ((λf x.f(f x)) f x)) 
->     (λf x.   (λx.f(f(f x)))   ((λf x.f(f x)) f x)) 
->     (λf x.       f(f(f(λf x.f(f x)) f x)))))
->     (λf x.       f(f(f  (λx.f(f x)) x)))))
->     (λf x.       f(f(f     (f(f x))  )))))

Answer 2

Mi consejo, por mi propia experiencia limitada, pero reciente:

1. un cosa a la vez: realizar una conversión de alfa, beta o una reducción de una conversión eta. Nota en el margen de la página que se está trabajando en lo que he tomado un paso para llegar a la siguiente línea. Si esas palabras no son familiares para usted, lo que hacen será - sólo echar un vistazo en el Wikipedia .

Un breve resumen de estas etapas de reducción:

Alpha sólo significa cambiar los nombres de las variables en un contexto coherente:

λfx. f (f x) => λgx. g (g x)

medios sólo se aplica la Beta de lambda a un argumento

(λf x. f x) b => λx. b x

Eta es simplemente 'desenvolver' una función innecesariamente envuelto que el cambio doesen't su significado.

λx.f x => f

Entonces

2. Uso lotes de la alfa de conversión para cambiar los nombres de las variables para hacer las cosas más claras. Todas esas fs, siempre va a ser confuso. Usted ha hecho algo similar con el " en su segunda fila

3. simular que eres un ordenador! No saltar por delante o por saltarse un paso cuando se está evaluando una expresión. Sólo hacer la siguiente cosa (y sólo una cosa). Sólo se mueven más rápido una vez que se está moviendo lentamente confianza.

4. Considere nombrar algunas de las expresiones y sólo sustituyéndolas por sus expresiones lambda cuando se necesita para evaluarlas. Por lo general nota de la sustitución en el margen de la página como by def ya que no es realmente una etapa de reducción. Algo así como:

   add two three 
   (λm n f x. m f (n f x)) two three | by def
   

Así pues, siguiendo las reglas anteriores, aquí está mi ejemplo práctico:

two   = λfx. f (f x)
three = λfx. f (f (f x))
add   = λmnfx. m f (n f x)

0  | add two three 
1  | (λm n f x. m f (n f x)) two three           | by def
2  | (λn f x. two f (n f x)) three               | beta
3  | (λf x. two f (three f x))                   | beta
4  | (λf x. two f ((λfx. f (f (f x))) f x))      | by def
5  | (λf x. two f ((λgy. g (g (g y))) f x))      | alpha
6  | (λf x. two f ((λy. f (f (f y))) x))         | beta
7  | (λf x. two f (f (f (f x))))                 | beta
8  | (λf x. (λfx. f (f x)) f (f (f (f x))))      | by def
9  | (λf x. (λgy. g (g y)) f (f (f (f x))))      | alpha
10 | (λf x. (λy. f (f y)) (f (f (f x))))         | beta
11 | (λf x. (λy. f (f (f (f (f x))))))           | beta

Answer 3

  

¿Hay una, más fácil técnica formal para abordar este tipo de problemas?

Es más más fácil escribir un reductor y prettyprinter de términos lambda de lo que es hacer reducciones a mano. Pero PLT Redex le puede dar una ventaja sobre las reducciones; intentar definir reglas para la reducción de orden normal, y entonces todo lo que tiene que hacer es preocuparse por prettyPrinting los resultados sin paréntesis redundantes .

Es probable que aprender mucho más, también.