Terms in the lambda calculus

Question

The formal definition of the lambda calculus I am seeing here reads:

The class of $\lambda$-terms is defined inductively as follows:

1. Every variable is a $\lambda$-term.
2. If $M$ and $N$ are $\lambda$-terms, then so is $(M N)$.
3. If $M$ is a $\lambda$-term and $x$ is a variable, then $(\lambda x[M])$ is a $\lambda$-term.

Usually, the authors after similar definitions proceed to talk about expressions such as "$\lambda x. x + 2$", but I am not seeing any definition of the legal syntax for the terms $M, N, \dots$. From the inductive definition above, it seems I can only use "variables", but not even the symbol "$+$" in a term.

Is that because the $\lambda$-calculus is in fact not concerned with the actual expressions of $M, N \dots$?

Answer 1

In order that expressions such as $\lambda x. x+2$ make sense in the $\lambda$-calculus (i.e. they are $\lambda$-terms), the expression $x+2$ should be a $\lambda$-term, according to your rule 3.

Actually, $x+2$ is a $\lambda$-term if it is interpreted as the expression $((+ \, x) 2)$ (i.e. two nested applications) where:

• $x$ is a variable;
• $+$ is the $\lambda$-term representing the arithmetic addition, i.e. $λm.λn.λf.λx.((m f) ((n f) x))$;
• $2$ is the $\lambda$-term representing the natural number 2, i.e. $\lambda f. \lambda x. (f(fx))$.

The idea is that $+$ and $2$ are just ''macros'' or shorthands for the $\lambda$-terms I wrote above.

For more information, see here.

More in general, since the $\lambda$-calculus is Turing-complete, every computable function on natural numbers can be represented by a $\lambda$-term, so any expression of the form $\lambda x_1. \dots \lambda x_n. f(x_1, \dots, x_n)$ can be seen as a $\lambda$-term, provided that $f \colon \mathbb{N}^n \to \mathbb{N}$ is a computable function.