[ 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
