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

[Brian Berns]

I think his implementation produces the same results as the formal system, although I haven't verified this. It just does it in a way that is both different from what he explicitly describes, and significantly harder to reason about (IMHO).

-- Brian

-----Original Message-----
From: John Clements <clements at brinckerhoff.org> 
Sent: Sunday, March 31, 2019 12:32 PM
To: Brian Berns <brianberns at gmail.com>
Cc: <types-list at lists.seas.upenn.edu> <types-list at LISTS.SEAS.UPENN.EDU>
Subject: Re: [TYPES] Order of evaluation rules in untyped lambda-calculus

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
>