7
$\begingroup$

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?

Improve this question
$\endgroup$
7
  • $\begingroup$ Where did you see that? The definition of value may vary. $\endgroup$
    – jmad
    May 4, 2012 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, 2012 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, 2012 at 15:12
  • 2
    $\begingroup$ Variables are always values, in every calculi. $\endgroup$
    – Fabio Filippi
    May 4, 2012 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, 2012 at 15:55

1 Answer 1

Reset to default
10
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 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, 2012 at 15:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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