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

John Clements clements at brinckerhoff.org
Sun Mar 31 12:31:40 EDT 2019


Forgive me for answering your question with a question: Is there a difference between the two systems? That is, does the implementation relate two terms that the formal system does not, or fail to relate two terms that the formal system does?

John Clements

> On Mar 27, 2019, at 18:49, Brian Berns <brianberns at gmail.com> 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
> 





More information about the Types-list mailing list