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

[Brian Berns]

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