Meaning of variables and applications in lambda calculus

Question

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?

Answer 1

Pure $\lambda$-calculus is rather restrictive. Nevertheless, you can extend it to contain "$3$" and "$+$" (either by really extending the language, or perhaps by denoting by $3$ some special lambda term like $\lambda f.\ \lambda x.\ f(f(f x))$).

Variables are unique symbols (most often strings), which make it easier to construct lambda-terms and define the whole affair. Compare for example De Brujin index, which uses plain numbers for the same task.

When thinking about lambda-terms, think about ordinary functions, only defined on some weird domain, e.g. for your example it would be

$x \mapsto x+3,$

or using different notation

$$f$$

where

$$f(x) = x+3.$$

Also, note the difference, $f(x)$ is not $f$, that is, $f$ is a function, while $f(x)$ is a symbol $x$ applied to function $f$; in other words you can write $f = x \mapsto x+3$, but $f(x) = x \mapsto x+3$ would be nonsensical (or it could yield falsehood, depending on your interpretation of "$=$", but that's different story).

The type of result of an application depends on a function. For $f$ it would be a number, e.g. $f(4) = 7$, but for a diffrent function like $g$ it could be another function, for example

$$g = y \mapsto (x \mapsto x + y),$$

or in other notation $$g(y)(x) = x+y.$$

Now, the result of $g(3)$ is a function, and it happens that $g(3) = (x \mapsto x+3) = f$, or to put it different way $g(3)(x) = x+3 = f(x)$. This happens because $f : \mathbb{N} \to \mathbb{N}$, while $g : \mathbb{N} \to (\mathbb{N} \to \mathbb{N})$, or as set-theorists would sometimes write $g : \mathbb{N} \to \mathbb{N}^\mathbb{N}$, hence $g(3) : \mathbb{N} \to \mathbb{N}$. Of course, in $\lambda$-calculus I could write these applications withouth parentheses, e.g. $g\ 3\ 5 = 8$ (and the equality sign isn't actually good, there are many types of equality, and here it could mean reduction which is yet a different kind of beast than equality).

I hope this helps $\ddot\smile$

Answer 2

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.