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

[John Clements]

Is the system you’re thinking about one whose conditionals would attempt to verify premises before deciding which rule to use? If so, I would point out that the system as written makes different things easier to reason about: specifically, the given implementation clearly does not explore multiple different possibilities, and therefore defines evaluation to be a function (at most one output for a given input). Also, it gives a much clearer sense of what the computational cost of generating the answer is going to be.

Naturally, you’re welcome to disagree :).

John

> On Mar 31, 2019, at 09:43, Brian Berns <brianberns at gmail.com> wrote:
> 
> 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
>> 
> 
> 
> 
>