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

[Brian Berns]

Yes, I'm verifying premises before deciding which rule to use. I do find that easier to think about, and potentially less buggy, although I totally agree that it could also be slower in practice. (I'm only building a toy implementation to crystalize my understanding of the material, so performance isn't critical in my case.) I believe that my evaluation routine should still be a valid function, because the formal system defines the rules so that no more than one applies to any given term.

FWIW, I'm implementing this system in F#, which has a feature called "active patterns" that supports a near-literal implementation of the spec. It looks something like this:

        /// Active pattern for a term that can take a step.
        let rec (|Step|_|) term =
            step term

        /// Reduces a term by one step, if it's not already in normal form.
        and step = function

                // try to reduce first term
            | Application (Step t1', t2) ->   // <== key line is here
                Application (t1', t2) |> Some

The key thing here is that the Application pattern first checks that t1 reduces to t1' before matching.

Thanks for your feedback. I appreciate it.

-- Brian

-----Original Message-----
From: John Clements <clements at brinckerhoff.org> 
Sent: Sunday, March 31, 2019 12:56 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

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
>> 
> 
> 
> 
>