Lambda Calculus Grammar

896 Views Asked by At

So in a lot of explanations of the Lambda Calculus the syntax is defined in the following way:

<expression> := <variable>
                | λ <variable>.<expression> //abstraction
                | <expression> <expression> //application

This implies that an application can be of the form:

<variable> <expression>

which to me doesn't make any sense and it should rather be:

<abstraction> <expression>

Am I correct, or am I getting this wrong?

EDIT: see this Wikipedia article for example

1

There are 1 best solutions below

3
On BEST ANSWER

$x(\lambda y.\!y)$ is a perfectly valid lambda term. It's not a closed lambda term, but that is a notion that is usually built on top of this basic notion of lambda terms. (Though, you can directly formalize "lambda-terms-in-context" which is probably a better basis for many purposes.)

Also, something like $\lambda f.\!\lambda x.\!((fx)(\lambda y.\!y))$ is a perfectly valid (closed) lambda term even though it consists of a subterm of the form <application> <expression>. The grammar means what it says.

My guess at what's leading to your uncertainty is that you are thinking about beta reduction which indeed applies only to terms of the form $(\lambda x.\!M)N$, but all this means is for applications not of that form we can't apply beta reduction at that particular application. So, for example, $x(\lambda y.\!y)$ is not reducible.