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?

  • $\begingroup$ Where did you see that? The definition of value may vary. $\endgroup$ – jmad May 4 '12 at 14:59
  • 2
    $\begingroup$ $(\lambda x. x)\ y$ is not a lambda abstraction, it's an application, namely, the application of $(\lambda x. x)$ to $y$. $\endgroup$ – Dave Clarke May 4 '12 at 15:02
  • 1
    $\begingroup$ @DaveClarke: I think Jeroen meant that $y$ was a normal form (to disprove that a value is an abstraction) and not that $(λx.x)y$ was an abstraction (to disprove that an abstraction is a value). $\endgroup$ – jmad May 4 '12 at 15:12
  • 2
    $\begingroup$ Variables are always values, in every calculi. $\endgroup$ – Fabio F. May 4 '12 at 17:22
  • 2
    $\begingroup$ @DaveClarke: I just checked Pierce's book. The confusion arised because the lambda-calculus' operational semantics is first touched on informally. It is there said in a footnote that the only values of the calculus are lambda-abstractions. Later, when the semantics is formally defined, it becomes clear that only closed terms are being considered. $\endgroup$ – codd May 5 '12 at 15:55

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.

  • 1
    $\begingroup$ This makes sense. The main thing I get out of it is that only closed terms should be taken into consideration. I will check with the original source to see if that is part of the formal definition of the operational semantics. $\endgroup$ – codd May 5 '12 at 15:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.