The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms:
- a variable, $x$, is itself a valid lambda term
- if $t$ is a lambda term, and $x$ is a variable, then $(\lambda x.t)$ is a lambda term (called a '''lambda abstraction''');
- if $t$ and $s$ are lambda terms, then $(ts)$ is a lambda term (called an '''application'''). Nothing else is a lambda term. Thus a lambda term is valid if and only if it can be obtained by repeated application of these three rules. However, some parentheses can be omitted according to certain rules. For example, the outermost parentheses are usually not written.
However, I cannot understand what variables are. Are they numbers? Or are they functions?
What is the result of an application? Is it a number or is it a function?
Reading many explanations regarding lambda calculus, I often see expressions like:
But, according to the definition above, those expressions are not valid lambda terms, because integers and operators are not valid lambda terms. So I guess I cannot express arithmetic expressions in lambda calculus. How can I describe functions?