|Steele and Sussman||March 10, 1976||31||LAMBDA: The Ultimate Imperative|
We can see that continuation-passing removes the need for the left-to-right rule if we consider the form of SCHEME expressions in continuation-passing style. In the style of Church, we can describe a SCHEME expression recursively:
- A variable, which evaluates to its bound value in the current environment.
- A constant, which evaluates to itself. Primitive operators such as
- A lambda expression, which evaluates to a closure.
- A label expression, which evaluates its body in the new environment. The body may be any SCHEME expression. Only closures of lambda expressions may be bound to labelled variables.
- A conditional expression, which must evaluate its predicate recursively before choosing which consequent to evaluate. The predicate and the two consequents may be any SCHEME expressions.
- A combination, which must evaluate all its elements recursively before performing the application of function to arguments. The elements may be any SCHEME expressions.
We say that an expression evaluates trivially if it is in category (1), (2), or (3); or in category (4) if the label body evaluates trivially; or in category (5) if the predicate and both consequents of the conditional evaluate trivially.
Lemma: expressions which evaluate trivially have no side effects.
We say that an expression is in continuation-passing form if it is in category (1), (2), (3); or in category (4) if the label body is in continuation-passing form; or in category (5) if the predicate evaluates trivially and the consequents are in continuation-passing form; or in category (6) if all the elements of the combination evaluate trivially, including the function.
Theorem: expressions in continuation-passing form cannot depend on left-to-right argument evaluation.
Proof: all arguments to functions evaluate trivially, and so their evaluations have no side effects. Hence they may be evaluated in any order. QED
It is not too difficult to prove from this that an evaluator for expressions in continuation-passing form can be iterative; it need not be recursive or use a control stack. Another way to look at it is that continuation-passing style forces the programmer to represent recursive evaluations explicitly. What would be the control stack during evaluation of an ordinary expression is represented in environment structures in continuation-passing style.
What if a programming language does not have all these features? Function calls and conditionals are clearly desirable features. Functional values are also valuable. It may be argued that dynamic scoping is just as good as lexical; our view is that both are desirable, and we have shown how to get dynamic scoping given lexical scoping. As for correct handling of tail-recursions, it is not difficult to see that a lexically scoped language which does not handle tail-recursions correctly is holding onto more information than is strictly necessary to execute the program.