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.
