The wikipedia definition of lambda terms is:
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:
$$\lambda x.x+3$$
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?
Best Answer
The point is that $\lambda$-calculus is pure syntax. The symbols are just symbols and don't stand for anything in particular. However, it is possible to do arithmetic in $\lambda$-calculus using Church numerals.
This is not to be confused with the simple notion of $\lambda$-abstraction, which finds use outside $\lambda$-calculus as a convenient way of defining function terms.