Lambda Reduction

lambda-calculus

Alpha Reduction

Definition

Alpha Reduction

The process of renaming bound variables is called alpha reduction.

Link to original

Beta Reduction

Definition

Beta Reduction

The beta reduction relation is defined as the least congruence relation on expressions $e$ such that:

$$(\lambda x.e_1)e_2\to [e_2/x]e_1$$

where $[t/x]$ means substituting the term $t$ for each free occurrence of $x$ in $e$. If there are free variables in $e_2$ then bound variables in $e_2$ must be renamed so that substitution does not result in the free variables in $e_2$ becoming bound. This process of renaming bound variables is called alpha reduction.

Link to original