Réduire le terme de calcul lambda à la forme normale

Question

Ceci est pour les devoirs avant que quelqu'un demande, je suis à la recherche de conseils.

Voici le premier terme de la question:

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

Je voudrais vous assurer que je pense à cela correctement. Le terme à droite est la valeur placée dans le paramètre x, correct? Ensuite, chaque instance de x est remplacée par le terme sur la droite. J'ai renommé y donc il n'y avait pas de confusion avec le y et le y borné. Maintenant, la chose que je ne comprends pas est la deuxième ligne commençant par =. Est-ce que le z le plus à droite est passé comme paramètre pour la variable z? Ou est-il passé en x? De toute façon, je pense que la réponse est la même, mais j'aimerais savoir quelle est la bonne méthode.

Voici le second terme de question

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

En raison des parenthèses, désigne le terme (λx.x) se substituer au paramètre x? Ou est-ce que y est substitué à x?

J'espère que cela a du sens. Merci d'avance pour votre aide.

Answer 1

calcul lambda se compose d'une grammaire sans contexte

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

où v plages plus variables, ainsi que les règles de réduction des eta bêta- et

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

a est-libre dans λ b. b a , mais pas au λ a. λ b. b a. Une expression à laquelle aucune des deux règles de réduction ne s'applique est sous la forme normale.

Ordre normal priorise la réduction des redexes les plus à gauche. Applicative-order normalise les arguments avant la substitution.

correct bêta- normal ordre et eta-normalisation des deux expressions:

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