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

302 Views Asked by At

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.

1

There are 1 best solutions below

2
On BEST ANSWER

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?)