zbMATH — the first resource for mathematics

Call-by-name extensionality and confluence. (English) Zbl 1418.68033
Summary: 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 \(\eta\) 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.
68N18 Functional programming and lambda calculus
68Q42 Grammars and rewriting systems
Full Text: DOI
[1] Ariola, Z. M.; Blom, S., Skew confluence and the lambda calculus with letrec, Ann. Pure Appl. Log., 117, 95-168, (2002) · Zbl 1019.03011
[2] Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics, (1984), Amsterdam: North-Holland, Amsterdam · Zbl 0551.03007
[3] 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.
[4] 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. · Zbl 1321.68146
[5] 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. · Zbl 1202.68091
[6] Danvy, O. & Nielsen, L. R. (2004) Refocusing in Reduction Semantics. Technical Report BRICS. Danish National Research Foundation.
[7] David, R.; Py, W., λμ-calculus and Bohm’s theorem, J. Symbol. Log., 66, 407-413, (2001) · Zbl 0981.03019
[8] 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. · Zbl 1405.68079
[9] 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. · Zbl 1040.03008
[10] Herbelin, H. (2005) C’est maintenant qu’on calcule : Au cœur de la dualité. Habilitation à diriger les reserches, Université Paris 11.
[11] 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. · Zbl 1295.68063
[12] Hofmann, M.; Streicher, T., Completeness of continuation models for λμ-calculus, Inform. Comput., 179, 332-355, (2002) · Zbl 1096.03011
[13] Klop, J. W.; De Vrijer, R. C., Unique normal forms for lambda calculus with surjective pairing, Inform. Comput., 80, 97-113, (1989) · Zbl 0667.03008
[14] Krivine, J.-L., A call-by-name lambda-calculus machine, Higher-Order Symbol. Comput., 20, 199-207, (2007) · Zbl 1130.68057
[15] Munch-Maccagnoni, G. (2013) Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD Thesis, Université Paris Diderot.
[16] 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. · Zbl 1394.68068
[17] 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. · Zbl 1417.03133
[18] 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. · Zbl 0925.03092
[19] 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. doi:10.1007/978-94-010-0413-8_5 · Zbl 1097.68541
[20] Pitts, A. M., Parametric polymorphism and operational equivalence, Math. Struct. Comput. Sci., 10, 321-359, (2000) · Zbl 0955.68024
[21] Plotkin, G. D., Call-by-name, call-by-value and the λ-calculus, Theor. Comput. Sci., 1, 125-159, (1975) · Zbl 0325.68006
[22] Sabry, A.; Felleisen, M., Reasoning about programs in continuation-passing style, Lisp Symbol. Comput., 6, 289-360, (1993)
[23] Sabry, A.; Wadler, P., A reflection on call-by-value, ACM Trans. Program. Lang. Syst., 19, 916-941, (1997)
[24] Saurin, A., Typing streams in the λμ-calculus, ACM Trans. Comput. Log., 11, 28:1-28:34, (2010) · Zbl 1351.68065
[25] Zeilberger, N. (2009) The Logical Basis of Evaluation Order and Pattern-Matching. PhD Thesis, Carnegie Mellon University, Pittsburgh, PA, USA.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.