Comment réduire le lambda-calcul

Question

J'essaie de comprendre le lambda-calcul et de lire le merveilleux article.

Sur la page 8, il y a une expression:

(λy.(x(λx.xy))) 

Si je vais remplacer l'extérieur le plus (λy) avec t gauche,

(λy.(x(λx.xy))) t 

alors le résultat serait?

x(λx.xy) 

Answer 1

Je pris la liberté de le réécrire à la syntaxe Haskell

(\y -> x (\x-> x y)) 
(\y -> x (\x-> x y)) t 

x (\x -> x t) 

depuis l'y est déjà lié à l'entrée \ y tous y seront remplacés par t. Editer: Comme indiqué dans le commentaire ci-dessous, si t où contenir un x libre, il serait important de renommer le x lié dans cette portée à un nom «frais». C'est un nom qui n'a actuellement aucun sens. Si nous disons

let t = \t -> x t 

Ensuite, la substitution appropriée ressemblerait

x (\z -> z (\t -> x t)) 

Si comme indiqué par pigworker certains z est choisi pour la fraîcheur comme identifiant frais pour remplacer notre borne x pour éviter de cacher la x libre en t.