numéro de l'Église pour l'addition

Question

Je suis coincé à l'étape suivante. Il sera grand si quelqu'un peut me aider:

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

Mes étapes sont:

   (λ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)

La belle parenthèse? Je me confonds vraiment sur les substitutions et entre parenthèses. Y at-il une technique formelle, plus facile à résoudre ces problèmes?

Answer 1

Essayez alligator oeufs!

Voici mes étapes que je Dérivée à l'aide d'alligator oeufs:

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

Mon conseil, de ma propre expérience limitée mais récente:

1. Do un chose à la fois: effectuer une conversion alpha, une réduction de bêta ou une conversion eta. Note dans la marge de la page que vous travaillez sur ce que vous avez l'étape nécessaire pour atteindre la ligne suivante. Si ces mots ne sont pas familiers, ce qu'ils font sera - il suffit de jeter un coup d'oeil sur Wikipedia .

Un résumé rapide de ces étapes de réduction:

Alpha seulement des moyens de modifier les noms des variables dans un contexte toujours:

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

Beta Il suffit d'appliquer le moyen lambda un argument

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

Eta est simplement « déballer » une fonction inutilement enveloppée que doesen't changer son sens.

λx.f x => f

Ensuite

2. Utilisez beaucoup de l'alpha conversion pour modifier les noms des variables pour rendre les choses plus claires. Tous ces fs, il va toujours être source de confusion. Vous avez fait quelque chose de similaire avec le " sur votre deuxième ligne

3. Imaginez que vous êtes un ordinateur! Ne pas sauter en avant ou sauter une étape lorsque vous évaluez une expression. Il suffit de faire la chose suivante (et une seule chose). Seulement aller plus vite une fois que vous êtes à l'aise se déplaçant lentement.

4. envisager de nommer quelques-unes des expressions et ne les substituer à leurs expressions lambda quand vous avez besoin de les évaluer. Je note habituellement la substitution dans la marge de la page by def que ce n'est pas vraiment une étape de réduction. Quelque chose comme:

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

suivant les règles ci-dessus, voici mon exemple détaillé:

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

  

Y at-il une technique formelle, plus facile à résoudre ces problèmes?

Il est beaucoup plus facile d'écrire un réducteur et prettyprinter pour les termes lambda que de faire des réductions à la main. Mais PLT Redex peut vous donner une longueur d'avance sur les réductions; définir des stratégies de réduction ordre normal, et tout ce que vous avez à faire est de vous soucier de prettyPrinting les résultats sans parenthèses redondantes .

Vous apprendrez probablement beaucoup plus, aussi.