Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-25T16:48:09.582Z Has data issue: false hasContentIssue false
  • English
  • Français

Representing Control: a Study of the CPS Transformation

Published online by Cambridge University Press:  04 March 2009

Oliver Danvy  and
Andrzex Filinski
Oliver Danvy
Affiliation:
Department of Computing and Information Sciences, Kansas State University, Manhattan Kansas 66506, USA. (danvy@cis.ksu.edu)
Andrzex Filinski
Affiliation:
School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213, USA. (Andrzej.Filinski@cs.cmu.edu)
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper investigates the transformation of λν-terms into continuation-passing style (CPS). We show that by appropriate η-expansion of Fisher and Plotkin's two-pass equational specification of the CPS transform, we can obtain a static and context-free separation of the result terms into “essential” and “administrative” constructs. Interpreting the former as syntax builders and the latter as directly executable code, We obtain a simple and efficient one-pass transformation algorithm, easily extended to conditional expressions, recursive definitions, and similar constructs. This new transformation algorithm leads to a simpler proof of Plotkin's simulation and indifference results.

We go on to show how CPS-based control operators similar to, more general then, Scheme's call/cc can be naturally accommodated by the new transformation algorithm. To demonstrate the expressive power of these operators, we use them to present an equivalent but even more concise formulation of the efficient CPS transformation algorithm. Finally, we relate the fundamental ideas underlying this derivation to similar concepts from other work on program manipulation; we derive a one-pass CPS transformation of λn-terms; and we outline some promising areas for future research.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 2 , Issue 4 , December 1992 , pp. 361 - 391
Copyright
Copyright © Cambridge University Press 1992

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Appel, A.W. (1992) Compiling with Continuations. Cambridge University Press.Google Scholar
Bondorf, A. (1991) Automatic autoprojection of higher-order recursive equations. Science of Computer Programming 17 3–34.CrossRefGoogle Scholar
Bondorf, A. and Danvy, O. (1991) Automatic autoprojection of recursive equations with global variables and abstract data types. Science of Computer Programming 16 151–195.CrossRefGoogle Scholar
Clinger, W. (1984) The Scheme 311 compiler, an excercise in Denotational Semantics. In: Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming, Austin, Texas356–364.CrossRefGoogle Scholar
Clinger, W. and Rees, J., editors (1991) Revised4 report on the algorithmic language Scheme. LISP Pointers IV(3) 1–55.Google Scholar
Consel, C. and Danvy, O. (1991 a) Static and dynamic semantics processing. In: Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida. ACM Press, 14–24.Google Scholar
Consel, C. and Danvy, O. (1991b) For a better support of static data flow. In: Proceedings of the Fifth ACM Conference on Functional Programming and Computer Architecture, number 523 in Lecture Notes in Computer Science, Cambridge, Massachusetts, 496–519.Google Scholar
Danvy, O. (1989) Programming with tighter control. Special issue of the BIGRE journal: Putting Scheme to Work, (65) 10–29.Google Scholar
Danvy, O. (1992) Back to direct style. In: Krieg-Brückner, B., editor, Proceedings of the Fourth European Symposium on Programming, number 582 in Lecture Notes in Computer Science, Rennes, France, 130–150.Google Scholar
Danvy, O. and Filinski, A. (1990) Abstracting control. In: Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, Nice, France, 151–160.Google Scholar
Danvy, O. and Lawall, J. L. (1992) Back to direct style II: First-class continuations. In: Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, San Fransisco, California.Google Scholar
Duba, B. F., Harper, R., and MacQuuen, D. (1991) Typing first-class continuations in ML. In: Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlanda, Florida. ACM Press, 163–173.Google Scholar
Felleisen, M. (1988) The theory and practice of first-class prompts. In: Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, 180–190.Google Scholar
Felleisen, M., Friedman, D.P., Duba, B., and Merrill, J. (1987a) Beyond continuations. Technical Report 216, Computer Science Department, Indiana University, Bloomington, Indiana.Google Scholar
Felleisen, M., Friedman, D.P., Kohlbecker, E., and Duba, B. (1986) Reasoning with continuations. In: Proceedings of the First Symposium on Logic in Computer Science, Cambridge, Massachusetts. IEEE, 131–141.Google Scholar
Felleisen, M., Friedman, D.P., Kohlbecker, E., and Duba, B. (1987b) A syntactic theory of sequential control. Theoretical Computer Science 52(3) 205–237.Google Scholar
Felleisen, M.Wand, M., Friedman, D.P. and Duba, B. F. (1988) Abstract continuations: A mathematical semantics for handling full functional jumps. In: Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, Snowbird, Utah, 52–62.Google Scholar
Fillnski, A. (1992) Linear continuations. In: Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, ACM Pree, 27–38.Google Scholar
Fisher, M. J. (1972) Lambda calculas schemata. In: Proceedings of the ACM Conference on Proving Assertions about Programs. SIGPLAN Notices 71 104–109 and SIGACT News 14.Google Scholar
Fradet, P. and Le Métayer, D. (1991) Compilation of functional languages by transformation. ACM Transactions on Programming Languages and Systems 13 21–51.Google Scholar
Griffin, T. G. (1990) A formulae-as-types notion of control. In: Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Franscisco, California. ACM Press, 47–58.Google Scholar
Griffin, R. E. and Grisworld, M. T. (1983) The Icon Programming Language. Prentice-Hall.Google Scholar
Harber, B. and Lillibridge, M. (1992) Polymorphic type assignment and CPS conversion. In: Danvy, O. and Talcott, C. L., editors, Proceedings of the ACM SIGPLAN Workshop on Continuations, San Franscisco, California. Technical report STAN-CS-92-1426, Standford University.Google Scholar
Jones, N. D., Sestoft, P., and Søndergaard, H. (1989) MIX: A self-applicable partial evaluator for experiments in compiler generation. LISP and Symbolic Computation 2(1) 9–50.Google Scholar
Mellish, C. and Hardy, S. (1984) Integrating Prolog in the POPLOG environment. In: Cambell, J. A., editor, Implements of PROLOG, Ellis Horwood, 147–162.Google Scholar
Milner, R., Tofte, M., and Harper, R. (1990) The definition of standard ML. The MIT Press.Google Scholar
Moggi, E. (1989) Computational lambda-calculas and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science, Pacific Grove, California, IEEE, 14–23.CrossRefGoogle Scholar
Murthy, C. R. (1990) Ectracting Constructive Content from Classical Proofs. PhD thesis, Department of Computer Science, Cornell University.Google Scholar
Murthy, C. R. (1992) Control operators, hierarchies, and pseudo-classical type systems: A-translation at work. In: Danvy, O. and Talcott, C. L., editors, Proceedings of the ACM SIGPLAN Work-shop on Continuations, San Fransisco, California. Technical report STAN-CS-92-1426, Standford University.Google Scholar
Nielson, F. (1989) Two-level semantics and abstract interpretaion. Theoretical Computer Science 69(2) 117–242.Google Scholar
Nielson, F. and Nielson, H. R. (1988) Two-level semantics and code generation. Theoretical Computer Science 56(1) 59–133.CrossRefGoogle Scholar
Plotkin, G. D. (1975) Call-by-name, call-by-value and the λ-calculas. Theoretical Computer Science 1 125–159.Google Scholar
Reynolds, J. C. (1972) Definitional interpreters for higher-order programming languages. In: Proceedings of 25th ACM National Conference, Boston, 717–740.Google Scholar
Riecke, J. G. (1989) Should a funcion continue? Master's thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts.Google Scholar
Sabry, A. and Felleisen, M. (1922) Reasoning about programs in continuation-passing style. In: Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, San Fransisco, Calfornia.Google Scholar
Shivers, O. (1991) The semantics of Scheme control-flow analysis. In: Hudak, P. and Jones, N. D.., editors, Symposium on Partial Evaluation and Semantics-Based Program Manipulation. SIGPLAN Notices 26 (9), ACM Press, New Haven, Connecticut. 190–198.Google Scholar
Sitaram, D. and Felleisen, M. (1990) Reasoning with continuations II: Full abstraction for models of control. In: Proceedings of the 1900 ACM on Lisp and Functional Programming, Nice, France, 161–175.Google Scholar
Steele, G. L. Jr (1978) Rabbit: A Compiler for Scheme. Technical Report A I-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts.Google Scholar
Wadler, P. (1992) The essence of functional programming. In: Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico. ACM Press, 1–14.Google Scholar
Wand, M. (1991) Correctness of procedure representations in higher-order assembly language. In: Brrokes, S., Main, M., Melton, A., and Schmidt, D., editors, Mathematical Foundations of Programming Semantics, volume 598 of Lecture Notes in Computer Science, Pittsburgh, Pennsylvania. 7th International Conference, 294–311.CrossRefGoogle Scholar