Basic notions of Lambda calculus

$\alpha$-conversion changes names of bound variables to fresh ones before substitution. $\alpha$-equivalence equates formulas that differ only in the naming of bound variables. Note that we consider two normal forms to be equal if they are $\alpha$-equivalent.

$\beta$-reduction applies a $\lambda$-term to another term: $(\lambda x.\, e)\ e' \mapsto e\ [e'/x]$. Two expressions are $\beta$-equivalent, if they can be $\beta$-reduced into the same expression.

$\eta$-conversion converts between $λx.(f\ x)$ and $f$ whenever $x \not\in FV(f)$. It expresses the ideas that two functions are the same if and only if they give the same result for all arguments. Hence a function and its eta-conversion is $\eta$-equivalent. In FP, we usually use $\eta$-conversion to bound free variables inside an expression, e.g., to convert $e: A\rightarrow B \rightarrow C$ to $\lambda x.\lambda y.e$.

$\eta$-conversion (together with rule $M \equiv N \implies M\ x \equiv N\ x$) yields the Extensional Principle: $M\ x \equiv N\ x \implies M\equiv N$, given that $x\not\in FV(M)\cup FV(N)$. This principle expresses the lambda calculus form of the notion of extensional equality for functions. That is, two functions $f, g: A\rightarrow B$ are indistinguishable iff $f\ x \equiv g\ x$ for all $x:A$.

The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules. For example, $(λx.M)\ N$ is a beta-redex, and $λx.M\ x$ is an $eta$-redex if $x$ is not free in $M$. The expression to which a redex reduces is called its $reduct$. Using the previous example, the reducts of these expressions are respectively $M[N/x]$ and $M$.