Why are lambda-abstractions the only terms that are values in the untyped lambda calculus?

Question

I am confused about the following claim: "The only values in the untyped lambda calculus are lambda-abstractions".

Why are the other terms not values? What does it mean for a lambda-abstraction to be a value? The first thing that came to my mind was that maybe lambda-abstractions are the only possible normal forms, but this is not true of course, e.g. $(\lambda x.\; x)\;y \to y$.

Can someone enlighten me?

Answer 1

There are a number of things going on here:

• The language you are talking about has no additional data types, otherwise there would be other kinds of values.
• The reduction strategy of the language does not reduce inside lambda abstractions. Both call-by-value and call-by-name conform to this. Otherwise, not every lambda abstraction would be a normal.
• One generally considers closed expressions as programs, so there are no free variables, hence the example you present is not considered.

Other terms are not values because they can be reduced or they do not appear in closed programs.

That a lambda abstraction is a value means that it cannot be reduced any further (depending on the reduction strategy).

For open terms, variables are also values.