Kirche Zeichen für die Zugabe

Question

Ich bin im folgenden Schritt stecken. Es wird großartig sein, wenn jemand kann mir helfen:

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

Meine Schritte sind:

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

Ist die Klammer in Ordnung? Ich verwirren mich wirklich auf den Substitutionen und Klammern. Gibt es eine formale, einfachere Technik Adresse solche Probleme?

Answer 1

Versuchen Sie Alligator Eier!

Hier sind meine Schritte, die ich mit Hilfe von Alligator Eiern abgeleitet:

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

Mein Rat, aus meinen eigenen begrenzten, aber den jüngsten Erfahrungen:

1. Do ein , was zu einem Zeitpunkt: führen Sie eine Alpha-Umwandlung, eine Beta-Reduktion oder eine eta-Konvertierung. Anmerkung am Rande der Seite, die Sie gerade arbeiten, was Schritt haben Sie ergriffen, um die nächste Zeile zu erreichen. Wenn diese Worte Ihnen nicht vertraut sind, was sie werden tun - nur einen Blick auf Wikipedia .

Eine kurze Zusammenfassung dieser Reduktionsschritte:

Alpha nur Mittel ändern die Namen von Variablen in einem Kontext konsequent:

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

Beta nur Mittel anwenden, das Lambda ein Argument

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

Eta ist einfach ‚Abwickeln‘ eine unnötig eingewickelt Funktion dass doesen't ändern ihre Bedeutung.

λx.f x => f

Dann

2. Mit Partien von Alpha Umwandlung der Namen der Variablen zu ändern, die Dinge klarer zu machen. All diese fs, es wird immer verwirrend werden. Sie haben etwas ähnliches mit dem " auf Ihrer zweiten Reihe getan

3. Pretend Sie ein Computer sind! Sie springen vor nicht oder überspringen einen Schritt, wenn Sie einen Ausdruck sind zu bewerten. Tun Sie einfach das nächste, was (und nur eins). bewegen sich schneller Erst wenn Sie sind davon überzeugt, bewegt sich langsam.

4. Betrachten wir einige der Ausdrücke benennen und nur sie für ihre Lambda-Ausdrücke ersetzt, wenn man sie beurteilen müssen. Ich stelle fest, in der Regel die Substitution in den Rand der Seite als by def, da es nicht wirklich ein Reduktionsschritt ist. So etwas wie:

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

So die oben genannten Regeln folgen, hier ist mein bearbeitetes Beispiel:

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

  

Gibt es eine formale, einfachere Technik Adresse solche Probleme?

Es ist viel einfacher, einen Druckminderer und für Lambda-Ausdrücke Pretty zu schreiben, als es ist Reduzierungen von Hand zu tun. Aber PLT Redex können Sie ein Bein geben auf die Kürzungen auf; versuchen, Regeln für die normale Ordnung Reduktion zu definieren, und dann alles, was Sie tun müssen, ist Sorge über pretty die Ergebnisse ohne redundante Klammern .

Sie werden wahrscheinlich viel mehr lernen, auch.