Lambda calculus

Definition

Fix a countably infinite set $V$ of variables. The lambda terms are the strings defined by these rules:

1. every variable $x \in V$ is a term;
2. if $M$ is a term and $x \in V$, then $(\lambda x.\, M)$ is a term, called an abstraction;
3. if $M$ and $N$ are terms, then $(M\, N)$ is a term, called an application.

In $\lambda x.\, M$ the variable $x$ is bound in $M$. Terms that differ only in the names of bound variables are identified ($\alpha$-equivalence). Let $M[x := N]$ be the term obtained from $M$ by replacing the free occurrences of $x$ by $N$. Before the replacement, bound variables of $M$ are renamed so that no free variable of $N$ gets bound. The untyped lambda calculus is the set of terms together with $\beta$-reduction. This is the relation generated by the rule $$(\lambda x.\, M)\, N \to_\beta M[x := N],$$ applied to any subterm of a term.