Programming Language Theory Concept

Alpha conversion renaming variable capture capture avoiding

Journey Statuslearning

Example:

(λ x . λ y . x) y \to [x \to y] λ y . x

Without alpha-conversion, performing a naive substitution would result in:

[x \to y] λ y . x = λ y . y

So, a function that was always returning a constant $x$ becomes an identity function.

With alpha-conversion, we can correctly perform a substitution:

[x \to y] λ y . x = [x \to y] λ z . x = λ z . y