Reduzieren Lambda-Kalkül Begriff auf Normalform

Question

Dies ist für Hausaufgaben, bevor jemand fragt, ich bin nur auf der Suche nach Anleitung.

Hier ist die erste Frage Begriff:

(λx.λy.x y)(λx.x y) 
=(λx.λz.x z)(λx.x y)   α-renaming 
=(λz.(λx.x y) z) 
=(λx.x y) 

Ich mag würde sicherstellen, dass ich dies richtig denke. Der rechte Ausdruck ist der Wert, der in den Parameter x eingegeben wird, richtig? Dann wird jede Instanz von x durch den Begriff auf der rechten Seite ersetzt. Ich habe y umbenannt, also gab es keine Verwechslungen mit dem freien y und dem begrenzten y. Was ich jetzt nicht verstehe, ist die zweite Zeile, die mit = beginnt. Wird der ganz rechte z als Parameter für die Variable z übergeben? Oder wird es in x weitergegeben? Wie auch immer ich denke, die Antwort ist die gleiche, aber ich würde gerne wissen, welche die richtige Methode ist. Hier

ist die zweite Frage Begriff

((λx.λy.x y)(λx.x)) y 
=((λx.λz.x z)(λx.x)) y 
=(λz.(λx.x)z) y 
=(λx.x)y 
=(λx.x) 

Wegen der Klammern, bedeutet der Begriff (λx.x) für den Parameter x ersetzt werden? Oder wird y für x substituiert?

Ich hoffe, das macht Sinn. Vielen Dank im Voraus für jede Hilfe.

Answer 1

Lambda-Kalkül besteht in einer kontextfreien Grammatik

E ::= v  Variable 
    | λ v. E Abstraction 
    | E E  Application 

wo v Bereiche über Variablen zusammen mit den Beta- und eta-Reduktionsregeln

(λ x. B) E => B where every occurrence of x in B in substituted by E 
    λ x. E x => E if x doesn't occur free in E 

akostenlos in λ b. b a ist , aber nicht in λ a. λ b. b a. Ein Ausdruck, für den keine der beiden Reduktionsregeln gilt, ist Normalform.

Normaler Ordnung priorisiert die Reduktion von Redexes ganz links. Applicative-order normalisiert Argumente vor der Ersetzung.

reguläre normale Ordnung beta- und eta-Normalisierung der beiden Ausdrücke:

(λ x. (λ y. x y)) (λ a. a b) 
= (λ x. x) (λ a. a b)   Eta-reduction 
= λ a. a b      Beta-reduction 

    ((λ x. (λ y. x y)) (λ a. a)) f 
= ((λ x. x) (λ a. a)) f 
= (λ a. a) f 
= f