# 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... Mar 10, 2014 at 21:04
• That may be the case. I've added more details to the question. Mar 11, 2014 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? Mar 11, 2014 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. Mar 12, 2014 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.