Lambda the Ultimate

I have to speculate a bit about the intentions of the authors, but my guess is that the different sources are making different default assumptions about the strictness of normal-order reduction.

If you assume that unqualified normal-order reduction is strict (i.e. you have to continue evaluating the arguments, even if they are not used in the body of the beta-reduction), then call-by-name is different than normal-order reduction.

If you assume that arguments not used in the beta-reducation can be discarded without evaluation (i.e. non-strict), then they are the same.

If you are doing LC proofs you want to be aware of making this distinction, whereas a more introductory paper such as this probably chose to ignore that technical detail and speak more informally in a way people familiar with PLs would understand.

I did some digging (I don't have my copy of TaPL handy) and found another reference where Pierce made the distinction between normal-order reduction and call-by-name, so I can make a hopefully nicer response.

The distinction Pierce is making depends on whether sub-expressions WITHIN a lambda expression can/must be evaluated or not.

In this scheme,
λy.(λx.x) y
is a normal-form in call-by-name but not in the the normal-order reduction discipline, where a further reduction to
λy.y
is required/possible.

Again this is a pretty technical detail that you would only have to consider when you want to be very precise about which variant of the LC you are using, and how you are mapping it as a model for a PL.

The authors of the thread-starting paper are definining things based on the ordinary assumptions about the "default" lambda calculus.

Welcome to the world of formal systems! ;-)

λy.(λx.x) y is actually in weak head normal form, not normal form. I believe call-by-name evaluation reduces to WHNF, whereas normal-order reduction for the lambda calculus only stops at normal form, hence they are not the same. Reduction to WHNF is the default for non-strict languages like Haskell, though they are call-by-need and not call-by-name.

At the risk of being tedious about this, this particular question hasn't let me go yet, and I want to refine my previous answer.

I've come to the opinion that Pierce is just plain right: he's not being "technical", he is just using precise and correct language.

Felleisen and Flatt are just being sloppy, but, to be fair to them, sloppy in a way that is very common in the literature.

In the "default" LC, anything that can reduce MUST reduce to be in normal form, so if you want any other behaviour you really should specify it as part of your definition of the sub-flavour of LC that you are using.

I hope my successive answer refinement has generated more illumination than confusion. ;-)

I think you are right about the distinction, and it took me a few years to notice it too. Not reducing under lambdas is an important difference between real (by which I mean "extant" — not a moral judgement) programming languages and typical calculi.

However, I wonder if the conflation arises because of the term normal order.

You can interpret order as denoting the reduction relation, which is an order-theoretic entity.

But you can also interpret it in the nontechnical (well — jargon-free) sense that it says in what order to reduce subterms, regardless of whether you actually do so. This agrees with the sense I get from leftmost, outermost, which I think is used more or less synonymously with normal order.

If you regard normal order in this latter sense, then call-by-name (no reducing under lambdas) and "CBN + reducing under lambdas" are both normal order.

However, I wonder if the conflation arises because of the term normal order.

I think, as you say, it is partly because of the range of formal and informal meaning of the term that problems arise.

If you are only thinking by analogy with PL parameter passing, you can see how you would say "applicative order is CBV, normal order is CBN". It is only when we want precise and complete LC models of PL semantics that we have to deal with some of the gory details.

I think a similar problem is that we usually say "the" LC is a semantic model for a PL, when, like any productive formal system, there are actually variants that work slightly differently, and we really mean one of those.

I think this kind of "abuse of terminology" is a wide-spread phenomenon throughout technical literature, and is one of the barriers to understanding for all newcomers to such fields.

I guess that is partly why I found Koray's question so compelling. ;-)

If you are only thinking by analogy with PL parameter passing, you can see how you would say "applicative order is CBV, normal order is CBN". It is only when we want precise and complete LC models of PL semantics that we have to deal with some of the gory details.

For those who want to revel in those gory details, the best summary of LC reduction strategies that I've seen is in Peter Sestoft's Demonstrating Lambda Calculus Reduction [link corrected] — see section 7 (context for the paper is here). The paper describes seven reduction strategies, including three hybrid strategies. Section 6 also contains a nice table which shows how the various normal forms relate to the strict/non-strict choice and whether to reduce under abstractions. Here's a stripped-down summary version:

[Edit: I've added to the table, in parentheses, what the paper calls the "uniform" reduction strategy which leads to the normal form in question. In the case of the top left cell (Normal form), other strategies also produce that form, including normal order reduction, of course.]

For those who want to revel in those gory details, the best summary of LC reduction strategies that I've seen

As someone who does revel in the gory details ;-), my only quibble is with calling these different evaluation rules "strategies" as though they define formally equivalent systems.

To reuse an earlier example to see how you get different systems consider:

λy.(λx.x) y

and

λy.y

In the weak "strategies" these are non-equivalent normal forms, even though they provably represent the same computation, as demonstrated by their equivalence in the non-weak "strategies."

(I suppose you could posit a two-tier evaluation to handle this, but that would yet another different formal system. ;-) )

Similarly, a system where some particular evaluation order is required describes a somewhat different model from one that allows any evaluation order (such as the "original" LC).

Admittedly, this is a fairly theoretical point, but one which has more or less importance to you depending on whether you are, say, trying to prove a theorem about PLs in general or really only want a reasonably precise semantic model for a particular PL.

(I've switched the subject line from being related to Gore to being related to Bush.)

I believe that the quibble about calling them strategies goes beyond usual practice in the field, e.g. both the paper I linked to and TAPL calls them strategies, as do many other sources.

I assume that this is (at least in part) because in any lambda calculus in which full beta reduction is allowed, i.e. any term can be reduced at any time, all of the other strategies are valid ways to perform reduction. In that context — which is a "default" context for LC — the different evaluation rules are indeed just strategies. Also in that context, it doesn't make sense to say something like "In the weak 'strategies' these are non-equivalent normal forms," because the strategy doesn't define the system being used.

I agree that there are more restricted contexts in which one might wish to be more specific, but when discussing reduction strategies in general, it's common to do that in a general context such as LC with full beta reduction.

I believe that the quibble about calling them strategies goes beyond usual practice in the field

I'm quibbling with the field, Anton, not with you. ;-)

Felleisen and Flatt are no slouches, but I think it is confusing that they choose to say, as is common in the field, that normal order reduction = call-by-name. (Hence Koray's original question)

Likewise, though I think I understand the origin of the usage (as a practical issue of PL operational semantics), calling them evaluation "strategies" confuses some of the issues for those trying to come to grips with the formal systems involved.

I think this point is worth making because I think this kind of terminological fuzziness often causes people to have to wrestle with the material for longer and harder than necessary to grasp the core insights on offer, and may cause others to give up entirely.

...is that like tribbles, they multiply.

I'm happy to act as a proxy for the field on this point, although you get what you pay for. :)

The two cases seem quite different to me. Felleisen and Flatt give a formal description of normal order reduction, which does reduce under lambdas, and then state "Normal order reduction is also called call-by-name." That statement is not consistent with a definition of call-by-name that excludes reduction under lambdas. Frank's explanation is plausible in other contexts, where PL-style semantics are assumed in both cases, but it doesn't really work here. So there's some other explanation for this anomaly, which hasn't been given in this thread. The text could just be in error — note that it's a draft text.

However, the term "reduction strategy" is well-defined, e.g. Barendregt defines it as a map from lambda terms to lambda terms. There's no confusion about its applicability in the context of the Sestoft paper, which states at the beginning of section 3, "We use the pure untyped lambda calculus," and references Barendregt. You might be able to quibble about the term's use in some other context, but in that case we should probably look at a concrete example. A straw man example is easy to imagine, but for all I know it may never have existed in practice.

Barendregt defines it as a map from lambda terms to lambda terms.

Oh well, I'll give up now then: No point arguing with Barendregt about the LC. ;-)

Is the link above really to the right paper? I don't find any extensive discussion or table on reduction strategies in it.

The correct link is here, sorry about that.

Koray Can wrote:

On page 30, they state that

Normal-order reduction is also called call-by-name.

My copy of TaPL (or this wikipedia, entry, which has TaPL in its references) disagrees. It's no big deal, but why do these two recent texts differ?

I emailed Felleisen and Flatt about this. Felleisen's response was, in part:

This is definitely a nonsensical statement and it must have slipped in by accident.

Keep in mind, the text is a draft.

CBN is a programming language semantics for the syntax of LC. It is best specified as the left-most/outer-most reduction of redexes in BY-NAME evaluation contexts via BETA.

CBV is also a programming language semantics for the syntax of LC. It is best specified as the left-most/outer-most reduction of redexes in BY-VALUE evaluation contexts via BETA-VALUE.

Just in case: a semantics is a partial function from programs (closed terms) to answers or values. The latter is a subset of the LC terms.

Plotkin (1974) settled the argument about CBN vs CBV once and for all. His paper has been my inspiration for the entire time I have conducted research on this branch of semantics. So this statement in PLLC entirely contradicts Plotkin's and deserves a bit of explanation.

The monograph is an unpublished outgrowth (translation) of my dissertation (1987) into lecture format for my first few years at Rice University. I stopped teaching this graduate course in 1998 and have only taught something related to it at Northeastern once.

Thankfully, Matthew Flatt has taken on the task of evolving the monograph. He teaches from the monograph and it's only natural that we share such texts when they are useful. While I do look at it on occasion, I haven't been forced to evaluate every word in the monograph in a long time. For this reason, the language slipped a bit recently. We will correct this asap.

I fully accept responsibility, however, for not catching this kind of thing earlier than today.