0
$\begingroup$

In pure lambda calculus, under the call-by-value reduction strategy, a term of the form $(\lambda x. x)y \rightarrow y$ implies that the free variable $y$ is a value. However, only abstractions are values in pure lambda calculus, and variables are defined as terms (Pierce, TAPL 53).

Reduction of the above term implies that all variables are abstractions. Can someone please explain? Am I missing something? Note that $y$ is a free variable, not a metavariable.

Edit: I wanted to prove to myself that an evaluation context exists for all forms of applications ($e_1e_2$ and $ve$). In the case analysis, I came across an instance where I had to determine whether an evaluation context exists for an expression of the form $(\lambda x. x) y$, and I regarded this case as irreducible, but in some of Pierce's examples (when talking about Church Booleans), he reduces expressions such as $test \, b \, v \, w$, where $test = \lambda l. \lambda m. \lambda n. l \, m \, n$. As Makholm pointed out, these types of reductions are only unambiguous under CBV for closed terms. Pierce says that $test$ is a combinator, and he defines combinators as closed terms.

So another question comes up for me: If $test$ is closed, then why is $test \, b \, v \, w$ closed? He makes a distinction regarding metavariables vs. variables, and says that a metavariable $s$ ranges over terms, and arbitrary variable $x$ is a metavariable that ranges over variables. I don't think this makes much difference, but I am not sure.

$\endgroup$
4
  • $\begingroup$ Do you have a reference for these definitions? It's hard to tell if you are possibly misreading a definition... $\endgroup$ Mar 10, 2014 at 21:04
  • $\begingroup$ That may be the case. I've added more details to the question. $\endgroup$
    – baffld
    Mar 11, 2014 at 17:23
  • $\begingroup$ No, $\mathit{test}\,b\,v\,w$ is definitely not closed if $b$, $v$, $w$ are variables. Perhaps, however, they might be metavariables ranging over value terms? $\endgroup$ Mar 11, 2014 at 17:55
  • $\begingroup$ I think that is what's implied. $b$ is a value, but $v$ $w$ are ambiguous. I think he assumes they are values and does not mention it for the sake of brevity. My primary point of confusion was whether $(\lambda x. x)y$ is "stuck" under CBV if $y$ is a free variable. The rest I can deduce from context. $\endgroup$
    – baffld
    Mar 12, 2014 at 13:31

1 Answer 1

2
$\begingroup$

Usually talking about "call-by-value" reduction is only unambiguously well-defined for closed terms. I've seen different authors do different things in this context for non-closed terms, including considering free variables to be "values", or refusing outright to deal with the case that a free variable ends up in an evaluation context.

If you see $(\lambda x.x)y\rightsquigarrow y$ being billed as a call-by-value reduction, then evidently you're in a context where free variables count as values. That's well and good, until you end up with $y\,M$ in an evaluation context. Presumably you will then either declare evaluation to have completed or proceed to reduce $M$ further.

In any case, the precise choices made here are not of the utmost importance here, as long as we agree on what happens to closed terms.

(I'm not entirely sure what your Pierce reference is. TAPL?)

$\endgroup$
2
  • $\begingroup$ Yes, it's TAPL. I ask precisely because I am working out the details of evaluation contexts using concrete sets (terms are defined as the limit of some sequence of sets). $\endgroup$
    – baffld
    Mar 11, 2014 at 16:44
  • $\begingroup$ Sorry, I sent that too early. I am adding some context to my question above. $\endgroup$
    – baffld
    Mar 11, 2014 at 16:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .