[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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 <[email protected]> > Sent: Sunday, March 31, 2019 12:32 PM > To: Brian Berns <[email protected]> > Cc: <[email protected]> <[email protected]> > 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 <[email protected]> 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 >> > > > >
