Article

Free access

Continuations may be unreasonable

Authors:

Jon G. RieckeAuthors Info & Claims

LFP '88: Proceedings of the 1988 ACM conference on LISP and functional programming

Pages 63 - 71

https://doi.org/10.1145/62678.62685

Published: 01 January 1988 Publication History

Abstract

We show that two lambda calculus terms can be observationally congruent (i.e., agree in all contexts) but their continuation-passing transforms may not be. We also show that two terms may be congruent in all untyped contexts but fail to be congruent in a calculus with call/cc operators. Hence, familiar reasoning about functional terms may be unsound if the terms use continuations explicitly or access them implicitly through new operators. We then examine one method of connecting terms with their continuized form, extending the work of Meyer and Wand [8].

References

[1]

H. P. Barendregt. The Lambda Calculus: Its Syntaz and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, 1981. l~evised Edition, 1984.

[2]

M. Felleisen. Private communication, April 22, 1988.

[3]

M. Felleisen. The theory and practice of first-class prompts. In 15th Syrup. Principles of Programming Languages, pages 180-190, ACM, 1988.

Digital Library

[4]

M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba. Reasoning with continuations. In Syrup. or~ Logic in Computer Science, pages 131-I41, IEEE, 1986.

[5]

M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba. A syntactic theory of sequential control. Theoretical Computer Science, 52:205-237, 1987.

Digital Library

[6]

M. J. Fischer. Lambda calculus schemata. In Pvoc. of An A CM Conference on Proving Assertions About Programs, pages 104-109, Las Cruces, NM, 1972.

Digital Library

[7]

A. R. Meyer. Semantical paradigms. In Syrup. on Logic and Computer Science, IEEE, 1988. Appendices by Stavros Cosmadakis. To appear.

[8]

A. R. Meyer and M. Wand. Continuation semantics in typed lambda-calculi (summary). In R. Parikh, editor, Logics of Programs, pages 219-224, Volume 193 of Lecture Notes in Computer Science, Springer-Verlag, 1985.

Digital Library

[9]

R. Milner. A theory of type polymorphism in programming. J. Computer and System Sci., 17:348-375, 1978.

[10]

G. D. Plotkin. Call-by-name, call-byvalue and the lambda calculus. Theoretical Computer Science, 1:125-159, 1975.

[11]

G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-256, 1977.

[12]

G. D. Plotkin. Types and partial functions. 1984. Unpublished lecture notes.

[13]

J. Rees and W. Clinger. The revised3 report on the algorithmic language Scheme. ACM $'IGPLAN Notices, 21:37-79, 1986.

Digital Library

[14]

J. Reynolds. Definitional interpreters for higher-order programming languages. In Proc. of the A CM National Meeting (Boston, 197~), pages 717-740, 1972.

Digital Library

[15]

J. Reynolds. On the relation between direct and continuation semantics. In Proc. of the Second Colloquium on A~- tomata, Languages, and Programming, Lecture Notes in Computer Science 15, pages 141-156, Springer-Verlag, 1974.

Digital Library

[16]

D. A. Schmidt. Denoiational Semantics, A Methodology for Language Development. Allyn and Bacon, 1986.

Digital Library

[17]

R. Sethi and A. Tang. Constructing callby-value continuation semantics. Journal of the A CM, 27:580-597, 1980.

Digital Library

[18]

R. Statman. A-definable functionals and /3r/-conversion. A rchiv Math. Logik Grundlagenforsch., 22:1-6, 1982.

[19]

G. L. Steele. Rabbit: A Compiler for Scheme. Technical Report AI-TR-474, MIT Artificial Intelligence Laboratory, 1978.

[20]

G. L. Steele. Common Lisp: The Language. Digital Press, Bedford, MA, 1984.

Digital Library

[21]

J. E. Stoy. Denotational Semantics: The $cott-Sirachey Approach to Programming Language Theory. MIT Press, 1977.

Digital Library

[22]

J. E. Stoy. The congruence of two programming language definitions. Theoretical Computer Science, 13:151-174, 1981.

[23]

C. Strachey and C. Wadsworth. Contin~ations: A Mathematical Semantics for Handling Full Jumps. Technical Report PRG-11, Oxford University Computing Laboratory, 1974.

Cited By

New MBowman WAhmed A(2016)Fully abstract compilation via universal embeddingACM SIGPLAN Notices10.1145/3022670.295194151:9(103-116)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951941
New MBowman WAhmed AGarrigue JKeller GSumii E(2016)Fully abstract compilation via universal embeddingProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951941(103-116)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951941
Ahmed ABlume MChakravarty MHu ZDanvy O(2011)An equivalence-preserving CPS translation via multi-language semanticsProceedings of the 16th ACM SIGPLAN international conference on Functional programming10.1145/2034773.2034830(431-444)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034773.2034830
Show More Cited By

Index Terms

Continuations may be unreasonable
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

An approach to call-by-name delimited continuations
POPL '08

We show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al'...
An approach to call-by-name delimited continuations
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al'...
Linear lambda calculus with non-linear first-class continuations
ICSCA '17: Proceedings of the 6th International Conference on Software and Computer Applications

The Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LFP '88: Proceedings of the 1988 ACM conference on LISP and functional programming

January 1988

351 pages

ISBN:089791273X

DOI:10.1145/62678

Chairman:
Jerome Chailloux
INRIA, Rocquencourt

Copyright © 1988 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1988

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

LISP88

Sponsor:

LISP88: Lisp & Functional Programming 88

July 25 - 27, 1988

Utah, Snowbird, USA

Acceptance Rates

Overall Acceptance Rate 30 of 109 submissions, 28%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
315
Total Downloads

Downloads (Last 12 months)32
Downloads (Last 6 weeks)5

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

New MBowman WAhmed A(2016)Fully abstract compilation via universal embeddingACM SIGPLAN Notices10.1145/3022670.295194151:9(103-116)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951941
New MBowman WAhmed AGarrigue JKeller GSumii E(2016)Fully abstract compilation via universal embeddingProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951941(103-116)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951941
Ahmed ABlume MChakravarty MHu ZDanvy O(2011)An equivalence-preserving CPS translation via multi-language semanticsProceedings of the 16th ACM SIGPLAN international conference on Functional programming10.1145/2034773.2034830(431-444)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034773.2034830
Ahmed ABlume M(2011)An equivalence-preserving CPS translation via multi-language semanticsACM SIGPLAN Notices10.1145/2034574.203483046:9(431-444)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034574.2034830
Wheeler KMurphy RThain D(2008)Qthreads: An API for programming with millions of lightweight threads2008 IEEE International Symposium on Parallel and Distributed Processing10.1109/IPDPS.2008.4536359(1-8)Online publication date: Apr-2008
https://doi.org/10.1109/IPDPS.2008.4536359
Felleisen M(2005)On the expressive power of programming languagesESOP '9010.1007/3-540-52592-0_60(134-151)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-52592-0_60
Thielecke H(1999)Using a Continuation Twice and Its Implications for the Expressive Power of call/ccHigher-Order and Symbolic Computation10.1023/A:101006880049912:1(47-73)Online publication date: 1-Apr-1999
https://dl.acm.org/doi/10.1023/A%3A1010068800499
Kučan J(1998)Retraction Approach to CPS TransformHigher-Order and Symbolic Computation10.1023/A:101001253246311:2(145-175)Online publication date: 1-Sep-1998
https://dl.acm.org/doi/10.1023/A%3A1010012532463
Riecke JWilliams J(1993)Delimiting the scope of effectsProceedings of the conference on Functional programming languages and computer architecture10.1145/165180.165200(146-155)Online publication date: 1-Jul-1993
https://dl.acm.org/doi/10.1145/165180.165200
Riecke JWise D(1991)Fully abstract translations between functional languagesProceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/99583.99617(245-254)Online publication date: 3-Jan-1991
https://dl.acm.org/doi/10.1145/99583.99617
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents