Separating stages in the continuation-passing style transformation

ABSTRACT

The continuation-passing style (CPS) transformation is powerful but complex. Our thesis is that this transformation is in fact compound, and we set out to stage it. We factor the CPS transformation into several steps, separating aspects in each step: (1) Intermediate values are named; (2) Continuations are introduced; (3) Sequencing order is decided and administrative reductions are performed. Step 1 determines the evaluation order (e.g., call-by-name or call-by-value). Step 2 isolates the introduction of continuations and is expressed with local, structure-preserving rewrite rules — a novel aspect standing in sharp contrast with the usual CPS transformations. Step 3 determines the ordering of continuations (e.g., left-to-right or right-to-left evaluation) and leads to the familiar-looking continuation-passing terms. Step 2 is completely reversible and Steps 1 and 3 form Galois connections. Together they lead to the direct style (DS) transformation of our earlier work (including first-class continuations): (1) Intermediate continuations are named and sequencing order is abstracted; (2) Second-class continuations are eliminated; (3) Administrative reductions are performed. A subset of these transformations can leverage program manipulation systems: CPS-based compilers can modify sequencing to improve e.g., register allocation; static program analyzers can yield more precise results; and overspecified CPS programs can be rescheduled. Separating aspects of the CPS transformation also enables a new programming style, with applications to nondeterministic programming. As a byproduct, our work also suggests a new continuation semantics for unspecified sequencing orders in programming languages (e.g., Scheme).

REFERENCES

• 1: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 2: Anders Bondorf, Improving binding times without explicit CPS-conversion, Proceedings of the 1992 ACM conference on LISP and functional programming, p.1-10, June 22-24, 1992, San Francisco, California, United States
• 3: Anders Bondorf , Olivier Danvy, Automatic autoprojection of recursive equations with global variable and abstract data types, Science of Computer Programming, v.16 n.2, p.151-195, Sept. 1991 [doi>10.1016/0167-6423(91)90002-F]
• 4: H. Abelson , R. K. Dybvig , C. T. Haynes , G. J. Rozas , N. I. Adams, IV , D. P. Friedman , E. Kohlbecker , G. L. Steele, Jr. , D. H. Bartley , R. Halstead , D. Oxley , G. J. Sussman , G. Brooks , C. Hanson , K. M. Pitman , M. Wand , William Clinger , Jonathan Rees, Revised report on the algorithmic language scheme, ACM SIGPLAN Lisp Pointers, v.IV n.3, p.1-55, July, 1991 [doi>10.1145/382130.382133]
• 5: Charles Consel. Report on Schism'92. Oregon Graduate Institute, Beaverton, Oregon, October 1992. Research Report.
• 6: Charles Consel , Olivier Danvy, For a better support of static data flow, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.496-519, June 1991, Cambridge, Massachusetts, United States
• 7: Olivier Danvy. Three steps for the CPS transformation. Technical Report CIS-92-2, Kansas State University, Manhattan, Kansas, December 1991.
• 8: Olivier Danvy, Back to direct style, Symposium proceedings on 4th European symposium on programming, p.130-150, January 1992, Rennes, France
• 9: Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4), 1992. To appear.
• 10: Olivier Danvy and John Hatcliff. Thunks (continued). In Proceedings of the Workshop on Static Anal. ysis WSA '92, volume 81-82 of Bigre Journal, pages 3- 11, Bordeaux, France, September 1992. IRISA, Rennes, France.
• 11: Olivier Danvy , Julia L. Lawall, Back to direct style II: first-class continuations, Proceedings of the 1992 ACM conference on LISP and functional programming, p.299-310, June 22-24, 1992, San Francisco, California, United States
• 12: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 13: Andrzej Filinski, Declarative Continuations: an Investigation of Duality in Programming Language Semantics, Category Theory and Computer Science, p.224-249, September 05-08, 1989
• 14: Michael J. Fischer, Lambda calculus schemata, Proceedings of ACM conference on Proving assertions about programs, p.104-109, January 06-07, 1972, Las Cruces, New Mexico, United States
• 15: Pascal Fradet, Syntactic detection of single-threading using continuations, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.241-258, June 1991, Cambridge, Massachusetts, United States
• 16: Daniel P. Friedman , Christopher T. Haynes , Mitchell Wand, Essentials of programming languages, MIT Press, Cambridge, MA, 1992
• 17: Timothy G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-58, December 1989, San Francisco, California, United States [doi>10.1145/96709.96714]
• 18: Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, June 1991
• 19: William L. Harrison III. The interprocedural analysis and automatic parallelization of Scheme programs. LISP and Symbolic Computation, 2(3/4):179-396, October 1989.
• 20: Neil D. Jones , Steven S. Muchnick, Binding time optimization in programming languages: Some thoughts toward the design of an ideal language, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.77-94, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811542]
• 21: Proceedings ol the 199f2 A CM Conference on Lisp and Functional Programming, San Francisco, California, June 1992.
• 22: Karoline Malmkjaer. On static properties of specialized programs. In Michel Billaud et al., editor, Analyse Statique en Programmation Equationnelle, Fonctionnelie et Logique, volume 74 of Bigre Journal, pages 234- 241, Bordeaux, France, October 1991. IRISA, Rennes, France.
• 23: Karoline Malmkjmr. Predicting properties of residual programs. In Charles Consel, editor, A CM SIGPLAN Workshop on Partial Evaluation and Semantics.Based Program Manipulation, Research Report 909, Department of Computer Science, Yale University, pages 8-13, San Francisco, California, June 1992.
• 24: A Melton , D A Schmidt , G E Strecker, Galois connections and computer science applications, Proceedings of a tutorial and workshop on Category theory and computer programming, p.299-312, November 1986, Guildford, United Kingdom
• 25: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 26: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• 27: Chetan R. Murthy. An evaluation semantics for classical proofs. In Proceedings of the Sixth Symposium on Logic in Computer Science, pages 96-107, Amsterdam, The Netherlands, July 1991. IEEE.
• 28: Flemming Nielson. A denotational framework for data flow analysis. Acta informatica, 18:265--287, 1982.
• 29: Gordon D. Plotkin. Call-by-name, call-by-value and the A-calculus. Theoretical Computer Science, 1:125-159, 1975.
• 30: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 31: Amr Sabry , Matthias Felleisen, Reasoning about programs in continuation-passing style., Proceedings of the 1992 ACM conference on LISP and functional programming, p.288-298, June 22-24, 1992, San Francisco, California, United States
• 32: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 33: Guy L. Steele, Jr., Rabbit: A Compiler for Scheme, Massachusetts Institute of Technology, Cambridge, MA, 1978
• 34: Allen Stoughton, Substitution revisited, Theoretical Computer Science, v.59 n.3, p.317-325, Aug. 1988 [doi>10.1016/0304-3975(88)90149-1]
• 35: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 36: Christopher Strachey and Christopher P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Technical Monograph PRG-11, Oxford University Computing L~boratory, Programming Research Group, Oxford, England, 1974.
• 37: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
• 38: Mitchell Wand, Correctness of Procedure Representations in Higher-Order Assembly Language, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.294-311, March 25-28, 1991

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.2 Language Classifications

          Nouns: SCHEME

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages