Pure Lambda Calculus: Call-by-value Free Variable Argument Application Reduction

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.

• Do you have a reference for these definitions? It's hard to tell if you are possibly misreading a definition... – Thomas Andrews Mar 10 '14 at 21:04
• That may be the case. I've added more details to the question. – baffld Mar 11 '14 at 17:23
• 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? – Henning Makholm Mar 11 '14 at 17:55
• 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. – baffld Mar 12 '14 at 13:31

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.