Hostname: page-component-586b7cd67f-gb8f7 Total loading time: 0 Render date: 2024-11-22T04:54:02.884Z Has data issue: false hasContentIssue false
  • English
  • Français

Call-by-name extensionality and confluence

Part of: JFP Research Articles

Published online by Cambridge University Press:  27 February 2017

PHILIP JOHNSON-FREYD ,
PAUL DOWNEN  and
ZENA M. ARIOLA
PHILIP JOHNSON-FREYD
Affiliation:
University of Oregon, Eugene, Oregon, USA (e-mails: [email protected], [email protected], [email protected])
PAUL DOWNEN
Affiliation:
University of Oregon, Eugene, Oregon, USA (e-mails: [email protected], [email protected], [email protected])
ZENA M. ARIOLA
Affiliation:
University of Oregon, Eugene, Oregon, USA (e-mails: [email protected], [email protected], [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Designing rewriting systems that respect functional extensionality for call-by-name languages with effects turns out to be surprisingly challenging. Simply interpreting extensional laws like η as reduction rules easily breaks confluence. We explore these issues in the setting of a sequent calculus. Building on an insight that appears in different aspects of the theory of call-by-name functional languages—confluent rewriting for two independent control calculi and sound continuation-passing style transformations—we give a confluent reduction system for lazy extensional functions. Finally, we consider limitations to this approach when used for strict evaluation and types beyond functions.

Type
Articles
Information
Journal of Functional Programming , Volume 27 , 2017 , e12
Copyright
Copyright © Cambridge University Press 2017 

References

Ariola, Z. M. & Blom, S. (2002) Skew confluence and the lambda calculus with letrec. Ann. Pure Appl. Log. 117 (3), 95–168.CrossRefGoogle Scholar
Barendregt, H. P. (1984) The Lambda Calculus: Its Syntax and Semantics. Amsterdam: North-Holland.Google Scholar
Carraro, A., Ehrhard, T. & Salibra, A. (2012) The stack calculus. In Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2012, Rio de Janeiro, Brazil, September 29–30, 2012, pp. 93–108.Google Scholar
Curien, P.-L. & Herbelin, H. (2000) The duality of computation. In Proceedings of the Fifth ACM Sigplan International Conference on Functional Programming. New York, NY, USA: ACM, pp. 233–243.CrossRefGoogle Scholar
Curien, P.-L. & Munch-Maccagnoni, G. (2010) The duality of computation under focus. In IFIP International Conference on Theoretical Computer Science. Springer Berlin Heidelberg, pp. 165–181.CrossRefGoogle Scholar
Danvy, O. & Nielsen, L. R. (2004) Refocusing in Reduction Semantics. Technical Report BRICS. Danish National Research Foundation.CrossRefGoogle Scholar
David, R. & Py, W. (2001) λμ-calculus and Bohm's theorem. J. Symbol. Log. 66 (1), 407–413.CrossRefGoogle Scholar
Downen, P. & Ariola, Z. M. (2014) The duality of construction. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014. Shao, Z. (ed), Lecture Notes in Computer Science, vol. 8410. Springer, Berlin, Heidelberg, pp. 249–269.CrossRefGoogle Scholar
Fujita, K.-etsu (2003) A sound and complete CPS-translation for λμ-calculus. In Typed Lambda Calculi and Applications. Hofmann, M. (ed), LNCS, vol. 2701. Berlin Heidelberg: Springer, pp. 120–134.CrossRefGoogle Scholar
Herbelin, H. (2005) C'est maintenant qu'on calcule : Au cœur de la dualité. Habilitation à diriger les reserches, Université Paris 11.Google Scholar
Herbelin, H. & Ghilezan, S. (2008) An approach to call-by-name delimited continuations. In Proceedings of the 35th Annual ACM Sigplan-Sigact Symposium on Principles of Programming Languages. POPL '08. New York, NY, USA: ACM, pp. 383–394.CrossRefGoogle Scholar
Hofmann, M. & Streicher, T. (2002) Completeness of continuation models for λμ-calculus. Inform. Comput. 179 (2), 332–355.CrossRefGoogle Scholar
Klop, J. W. & de Vrijer, R. C. (1989) Unique normal forms for lambda calculus with surjective pairing. Inform. Comput. 80 (2), 97–113.CrossRefGoogle Scholar
Krivine, J.-L. (2007) A call-by-name lambda-calculus machine. Higher-Order Symbol. Comput. 20 (3), 199–207.CrossRefGoogle Scholar
Munch-Maccagnoni, G. (2013) Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD Thesis, Université Paris Diderot.CrossRefGoogle Scholar
Munch-Maccagnoni, G. & Scherer, G. (2015) Polarised intermediate representation of lambda calculus with sums. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS '15. Washington, DC, USA: IEEE Computer Society, pp. 127–140.CrossRefGoogle Scholar
Nakazawa, K. & Nagai, T. (2014) Reduction system for extensional lambda-mu calculus. In Rewriting and Typed Lambda Calculi: Joint International Conference, Rta-Tlca 2014, held as part of the Vienna Summer of Logic, vsl 2014, Dowek, G. (ed), Vienna, Austria, July 14–17, 2014. Proceedings. LNCS. Cham: Springer International Publishing, pp. 349–363.CrossRefGoogle Scholar
Parigot, M. (1992) Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In Proceedings of the International Conference on Logic Programming and Automated Reasoning. ACM, London, UK, UK: Springer-Verlag, pp. 190–201.Google Scholar
Pfenning, F. (2002) Logical frameworks–-a brief introduction. In Proof and System-Reliability. NATO Science Series II, vol. 62. Kluwer Academic Publishers, pp. 137–166.CrossRefGoogle Scholar
Pitts, A. M. (2000) Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci. 10 (3), 321–359.CrossRefGoogle Scholar
Plotkin, G. D. (1975) Call-by-name, call-by-value and the λ-calculus. Theor. Comput. Sci. 1 (2), 125–159.CrossRefGoogle Scholar
Sabry, A. & Felleisen, M. (1993) Reasoning about programs in continuation-passing style. Lisp Symbol. Comput. 6 (3–4), 289–360.CrossRefGoogle Scholar
Sabry, A. & Wadler, P. (1997) A reflection on call-by-value. ACM Trans. Program. Lang. Syst. 19 (6), 916–941.CrossRefGoogle Scholar
Saurin, A. (2010) Typing streams in the λμ-calculus. ACM Trans. Comput. Log. 11 (4), 28:1–28:34.CrossRefGoogle Scholar
Zeilberger, N. (2009) The Logical Basis of Evaluation Order and Pattern-Matching. PhD Thesis, Carnegie Mellon University, Pittsburgh, PA, USA.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.