Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
From the evaluation strategy article on Wikipedia:
The notion of reduction strategy in lambda calculus is similar but distinct.
From the reduction strategy article on Wikipedia:
It is similar to but subtly different from the notion of evaluation strategy in computer science.
What is the subtle distinction between evaluation strategies and reduction strategies that these two articles hint at? Are they just two similar concepts from different domains?
A reduction strategy is a function on Lambda that picks one redex (reducible expression) from all possible redexes -- depending on what you define as a redex.
Informally, an evaluation strategy is the order in which a language evaluates its arguments. A parameter-passing strategy is what the language hands to the function.
To understand the connection among these, study Plotkin's paper on Call-by-name, call-by-value, and the lambda calculus. He clearly spells out that you want to choose distinct AXIOMS depending on which order of evaluation you want. For Cb-name you want the old beta axiom and for cb-value you want a beta-value axiom. If you do that, all meta-theorems work out the same for both flavors. I showed later on (with many collaborators) that this idea generalizes to everything the world of PL has studied.
It's all technical, not some poem that can be interpreted. Just read up on it.
-- Matthias Felleisen
p.s. I will say that I think people will have an easier time understanding Plotkin's paper from Part I in our Redex book. But yes, it's 3x as long.
The "Reduction strategy" wikipedia article is entirely extracted out of a particular edit made by an anonymous IP to the "Evaluation strategy" article.
The view that it represents is not consensual, in the sense that I suspect relatively few people of the field will spontaneously give this answer if you ask them "would you distinguish the names 'reduction strategy' and 'evaluation strategy'?". I have only heard it from Matthias Felleisen, which is adamant about the importance of this distinction -- and I assume this point of view is shared by others that had the chance of taking time to discuss these points in details with him.
My current understanding of this point (but I have not yet studied the technical details to their full justice) is about the following: this is about whether you use "big step" versus "small step" semantics -- this distinction is standard and understood by everyone in the field. Small-steps semantics define one atomic step of reduction, and the result is in general still reducible. Big-step semantics define one "big" step of reduction that goes all the way from the starting program to its value (or some richer "answer" type if your language has other observable effects than returning a value, eg. input/output or mutable state).
If you define both a big-step and small-step relation, you can check that the big-step semantics is included in the transitive closure of the small step relation, and that the small-step relation does not reduce to other stuck terms than those reached by the big-step relation, or diverge if the big-step reduction is defined. This is the expected coherence relation between both.
I think that the wording of the article can be more or less described, in modern terms, as "evaluation strategy is the big-step relation", "reduction strategy is the small-step relation". Do note that the discussion made in the "Reduction strategy" article is mostly about articles and research (and, more importantly, eloquent viewpoints formed during their reading and writing) between 1973 and 1991, at a time where those notions were just born, and probably not as well-understood as they are today. (big-step semantics was emphasized by Kahn in 1987, and one of the most important works on small-step semantics is Wright and Felleisen, 1992)
For the more opinionated side of why Felleisen insists on the importance of this difference (that is, why there may be more to it than just "small-step vs. big-step, meh"), my current understanding is the following: the point that is being made is that the small-step semantics should be viewed as an implementation detail. The semantics, according to this argument, is the abstract function that maps each program to its value/answer, and the rest are implementation devices designed to approximate it (or reason on the equivalence induced by this semantics). When we say big-step today, we think of a system of inference rules of syntactic nature, but the "reduction strategy" that is being discussed above is in fact its abstraction as a mapping. (I don't think this gives more expressivity or strength to the notion in practice, but it makes it more abstract.)
So I think that what this wikipedia page, and Matthias Felleisen, are saying is something like: "Define your evaluation in whichever way you like, but in the end of the day the thing that matters is how your programs are mapped to their values/answers/behaviors, and this is what should be called 'operational semantics' and reasoned about.".
Note that this position goes somewhat against the current distinction (which I think is rather consensual, but it may be a cultural bias on my part) between "operational semantics" and "denotational semantics", where the former is seen as more syntactic in nature (defined as a reduction relation), and the latter is typically characterized by the fact that computationally equivalent programs have the exact same denotation (so the denotation is oblivious to the actual computation mechanism). Under this latter view, what is proposed as an "evaluation strategy" or "operational semantics" in the articles and my explanation above would rather be seen as a denotational semantics -- but admittedly of a more concrete nature than most: values/answers/behaviors are closer to syntactic objects than many semantic domains.
References: to understand this point of view, it is probably useful to go back to its proclaimed source, which is the article by Gordon Plotkin in 1973. You may also have good luck trying one of the latter articles cited on wikipedia; I found for example that "Parameter-Passing and the Lambda Calculus", by Crank and Felleisen, 1991, gave a very clear overview of their position on the matter in the first few pages.
