Abstract
In a simply-typed, call-by-value (CBV) language with first-class continuations, the usual CBV fixpoint operator can be defined in terms of a simple, infinitely-looping iteration primitive. We first consider a natural but flawed definition, based on exceptions and “iterative deepening” of finite unfoldings, and point out some of its shortcomings. Then we present the proper construction using full first-class continuations, with both an informal derivation and a proof that the behavior of the defined operator faithfully mimics a “built-in” recursion primitive. In fact, given an additional uniformity assumption, the construction is a two-sided inverse of the usual definition of iteration from recursion. Continuing, we show that the CBV looping primitive is in fact the direct-style equivalent of a continuation-passing-style fixpoint, and that this correspondence extends all the way to traditional definitions of these operators in terms of reflexive types.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Clinger, W. and Rees, J. Revised4 report on the algorithmic language Scheme.Lisp Pointers, 4, 3 (July 1991) 1–55.
Danvy, O. and Filinski, A. Representing control: A study of the CPS transformation.Mathematical Structures in Computer Science, 2, 4 (December 1992) 361–391.
Danvy, O. and Lawall, J. L. Back to direct style II: First-class continuations. InProceedings of the 1992 ACM Conference on Lisp and Functional Programming, San Francisco, California (June 1992) 299–310.
Duba, B. F., Harper, R., and MacQueen, D. Typing first-class continuations in ML. InProceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida (January 1991) 163–173.
Felleisen, M. and Hieb, R. The revised report on the syntactic theories of sequential control and state.Theoretical Computer Science, 103, 2 (1992) 235–271.
Felleisen, M., Friedman, D. P., Kohlbecker, E., and Duba, B. Reasoning with continuations. InProceedings of Symposium on Logic in Computer Science, IEEE, Cambridge, Massachusetts (June 1986) 131–141.
Filinski, A. Declarative continuations: An investigation of duality in programming language semantics. In Pitt, D. H.et al, editors,Category Theory and Computer Science, Manchester, UK (September 1989) 224–249.
Greibach, S.Theory of Program Structures: Schemes, Semantics, Verification. Lecture Notes in Computer Science 36 (1975).
Griffin, T. G. A formulae-as-types notion of control. InProceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California (January 1990) 47–58.
Gunter, C. A.Semantics of Programming Languages: Structures and Techniques. The MIT Press (1992).
Harper, R. and Lillibridge, M. Polymorphic type assignment and CPS conversion. InProceedings of the ACM SIGPLAN Workshop on Continuations, San Francisco, California (June 1992) 13–22. Revised version inLisp and Symbolic Computation (this issue).
Hindley, J. R. and Seldin, J. P.Introduction to Combinators and λ-Calculus. Volume 1 ofLondon Mathematical Society Student Texts, Cambridge University Press (1986).
Kfoury, A. J.The Translation of Functional Programs into Tail-Recursive Form (Part I). BUCS Tech Report 87-003, Computer Science Department, Boston University (January 1987).
Landin, P. J. A correspondence between ALGOL60 and Church's lambda notation.Communications of the ACM, 8 (1965) 89–101 and 158–165.
Milner, R., Tofte, M., and Harper, R.The Definition of Standard ML. The MIT Press (1990).
Moggi, E. Computational lambda-calculus and monads. InProceedings of the Fourth Annual Symposium on Logic in Computer Science, IEEE, Pacific Grove, California (June 1989) 14–23.
Plotkin, G. D. Call-by-name, call-by-value and the λ-calculus.Theoretical Computer Science, 1 (1975) 125–159.
Reynolds, J. C. Gedanken — a simple typeless language based on the principle of completeness and the reference concept.Communications of the ACM, 13, 5 (May 1970) 308–319.
Reynolds, J. C. Definitional interpreters for higher-order programming languages. InProceedings of 25th ACM National Conference, Boston (August 1972) 717–740.
Sabry, A. and Felleisen, M. Reasoning about programs in continuation-passing style. InProceedings of the 1992 ACM Conference on Lisp and Functional Programming, San Francisco, California (June 1992) 288–298. Revised and extended version inLisp and Symbolic Computation (this issue).
Scott, D. S. Continuous lattices. InProceedings of 1971 Dalhousie Conference, Springer-Verlag (1972) 97–136.
Talcott, C. A theory for program and data type specification.Theoretical Computer Science, 104, 1 (1992) 129–159.
Walker, S. A. and Strong, H. R. Characterizations of flowchartable recursions.Journal of Computer and System Sciences, 7 (1973) 404–447.
Author information
Authors and Affiliations
Additional information
An earlier version of this work appeared inProceedings of the 1992 ACM SIGPLAN Workshop on Continuations.
Supported in part by NSF Grant CCR-8922109 and in part by the Avionics Lab, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, OH 45433-6543 under Contract F33615-90-C-1465, ARPA Order No. 7597. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. Government.
Rights and permissions
About this article
Cite this article
Filinski, A. Recursion from iteration. LISP and Symbolic Computation 7, 11–37 (1994). https://doi.org/10.1007/BF01019943
Issue Date:
DOI: https://doi.org/10.1007/BF01019943