[TYPES] Order of evaluation rules in untyped lambda-calculus

[Ezra e. k. Cooper]

It's a good question! Something subtle is indeed going on. (Or more than one.)

In most such systems, the value grammar is carefully chosen so that it does not reduce, and that all "meaningful" terms which do not reduce are in this grammar. Type systems will often play a role in ensuring that well-typed terms either reduce or are values. If you know that the values do not reduce and that the meaningful values do, then you know that the terms t1 for which t1 -> t1' are exactly the non-values (presuming the whole term is meaningful). It would usually be a bug in a semantics to define the values so that any of them reduce, but it's a proof obligation to show that you don't have that bug.

Strictly speaking, you are right that a little shortcut has been taken in the implementation. Strictly, to determine if an application admits the reduction step of E-App1, we should somehow check that the LHS reduces. How can we do that within this implementation? Well it happens that all the cases produce a new term (representing a reduction) except that final case whose body reads "raise NoRuleApplies". So, if we were auto-generating this sort of evaluator from the inference rules, we might implement the case for E-App1 by *trying* to evaluate the LHS and catching that exception. If there is no exception then we get the new left-hand term, t1'. If there is an exception then the rule E-App1 does not apply and we should fall through to other cases. Implementing all that as a pattern guard in OCaml would be a bit fiddly, though.

If you imagine implementing this system in, say, Prolog, you would very naturally write it so that some reduction exists whenever some other reduction exists; the interpreter knows how to search for those reductions, and exactly what to do if it doesn't find one (i.e., try to meet its goal through other rules, which is the equivalent of "falling through" in this case). That would be a more "direct" implementation of the rewrite rules, perhaps.

The activity that the Pierce evaluator is doing here is called "redex selection," or focusing, and, in a sense the evaluator on p. 87 is already a little "virtual machine" that has smarts about redex selection. There is a significant literature on virtual machines and how they correspond to rewrite rules as such. Danvy and Nielsen's "Refocusing in reduction semantics" is one notable paper in that area.

Cheers,
Ezra


On Sun, Mar 31, 2019, at 7:13 AM, Brian Berns wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> I'm working through Pierce's _Types and Programming Languages_ and I've
> found a subtle issue that I'd could use some help on. The problem is with
> the untyped lambda-calculus. The E-App1 evaluation rule on p. 72 says that
> t1 t2 -> t1' t2 if t1 -> t1' with the following comment:
> 
> "Notice how the choice of metavariables in these rules helps control the
> order of evaluation. ... Similarly, rule E-App1 applies to any application
> whose left-hand side is not a value, since t1 can match any term whatsoever,
> but **the premise further requires that t1 can take a step**." (Emphasis
> added.)
> 
> This strongly implies that the order of the rules shouldn't matter. The
> corresponding implementation on p. 87 then says "The single-step evaluation
> function is a direct transcription of the evaluation rules", but the rules
> appear in a different order and there is no guard on the E-App1 rule that
> prevents it from firing when t1 can't be reduced. Instead, it looks like the
> rules are arranged in an order that ensures that E-App1 is executed only as
> a last resort.
> 
> It seems to me that the "correct" implementation of E-App1 (and, in fact, of
> every evaluation rule) is to ensure that its premises are met before
> applying it. Instead, the implementation seems to take a shortcut here. I'm
> not opposed to that, but I'd like to understand how it works. Am I correct
> in thinking that the behavior of this implementation is subtly dependent on
> the order of its evaluation rules in a way that the definition of those
> rules was intended to avoid? If that's the case, are there any general
> guidelines that an implementor can/should use to order the evaluation rules
> for a language in the correct way?
> 
> Thanks for your help.
> 
> -- Brian Berns
> 
>