New Semantical Insights Into Call-by-Value λ-Calculus

• Autorzy: Manzonetto Giulio , Pagani Michele , Ronchi Della Rocca Simona

Identyfikatory

DOI

10.3233/FI-2019-1862

• Języki publikacji: EN

Abstrakty

EN

Despite the fact that call-by-value λ-calculus was defined by Plotkin in 1977, we believe that its theory of program approximation is still at the beginning. A problem that is often encountered when studying its operational semantics is that, during the reduction of a λ-term, some redexes remain stuck (waiting for a value). Recently, Carraro and Guerrieri proposed to endow this calculus with permutation rules, naturally arising in the context of linear logic proof-nets, that succeed in unblocking a certain number of such redexes. In the present paper we introduce a new class of models of call-by-value λ-calculus, arising from non-idempotent intersection type systems. Beside satisfying the usual properties as soundness and adequacy, these models validate the permutation rules mentioned above as well as some reductions obtained by contracting suitable λI-redexes. Thanks to these (perhaps unexpected) features, we are able to demonstrate that every model living in this class satisfies an Approximation Theorem with respect to a refined notion of syntactic approximant. While this kind of results often require impredicative techniques like reducibility candidates, the quantitative information carried by type derivations in our system allows us to provide a combinatorial proof.

Słowa kluczowe

EN

lambda calculus; call-by-value; relational semantics; approximation theorem; intersection types

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 241--256
• Opis fizyczny: Bibliogr. 35 poz., rys.

Twórcy

autor

Manzonetto Giulio

• CNRS, LIPN, Université Paris-Nord, Villetaneuse, France

autor

Pagani Michele

• IRIF, Université Paris-Diderot, Paris, France

autor

Ronchi Della Rocca Simona

• Dipartimento di Informatica, Università di Torino, Torino, Italy

Bibliografia

• [1] Church A. The Calculi of Lambda Conversion, volume 6 of Annals of Mathematical Studies. Princeton University Press, Princeton, 1941. Reprinted by University Microfilms Inc., Ann Arbor, MI in 1963 and by Klaus Reprint Corp., New York in 1965.
• [2] Plotkin GD. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1975. 1(2):125-159. URL https://doi.org/10.1016/0304-3975(75)90017-1.
• [3] Carraro A, Guerrieri G. A Semantical and Operational Account of Call-by-Value Solvability. In: Muscholl A (ed.), Foundations of Software Science and Computation Structures, volume 8412 of Lecture Notes in Computer Science. Springer-Verlag, 2014 pp. 103-118. ISBN:9783642548291.
• [4] Guerrieri G, Paolini L, Ronchi Della Rocca S. Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus. Logical Methods in Computer Science, 2017. 13(4):1-27. www.lmcs-online.org.
• [5] Wadsworth CP. The Relation Between Computational and Denotational Properties for Scott’s D∞-Models of the Lambda-Calculus. SIAM Journal of Computing, 1976. 5(3):488-521. doi:10.1137/0205036.
• [6] Hyland JME. A Syntactic Characterization of the Equality in Some Models of the Lambda Calculus. Journal of the London Mathematical Society, 1976. 2-12(3):361-370. doi:10.1112/jlms/s2-12.3.361.
• [7] Egidi L, Honsell F, Ronchi Della Rocca S. Operational, Denotational and Logical Descriptions: a case study. Fundamenta Informaticae, 1992. 16(2):149-170. URL http://www.iospress.nl, Fax:[phone].
• [8] Paolini L, Ronchi Della Rocca S. The Parametric Parameter Passing λ-calculus. Information and Computation, 2004. 189(1):87-106. doi:10.1016/j.ic.2003.08.003.
• [9] Paolini L, Piccolo M, Ronchi Della Rocca S. Logical Semantics for Stability. Electr. Notes Theor. Comput. Sci., 2009. 249:429-449. URL https://doi.org/10.1016/j.entcs.2009.07.101.
• [10] Ehrhard T. Collapsing non-idempotent intersection types. In: CSL’12, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs). 2012 pp. 259-273. doi:10.4230/LIPIcs.CSL.2012.259.
• [11] Ehrhard T, Guerrieri G. The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016 pp. 174-187. doi:10.1145/2967973.2968608.
• [12] Curien PL, Herbelin H. The duality of computation. In: Odersky M, Wadler P (eds.), Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00). ACM. 2000 pp. 233-243. ISBN:1-58113-202-6. doi:10.1145/357766.351262.
• [13] Dyckhoff R, Lengrand S. Call-by-Value lambda-calculus and LJQ. Journal of Logic and Computation, 2007. 17(6):1109-1134. URL https://hal.archives-ouvertes.fr/hal-00150284.
• [14] Herbelin H, Zimmermann S. An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in ”Natural Deduction” Form. In: Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, volume 5608 of Lecture Notes in Computer Science. Springer-Verlag, 2009 pp. 142-156. doi: 10.1007/978-3-642-02273-9_12.
• [15] Accattoli B, Paolini L. Call-by-Value Solvability, Revisited. In: Functional and Logic Programming, volume 7294 of Lecture Notes in Computer Science. Springer-Verlag 2012 pp. 4-16. ISBN:978-3-642-29821-9.
• [16] Accattoli B, Sacerdoti Coen C. On the Relative Usefulness of Fireballs. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015. IEEE Computer Society 2015 pp. 141-155. ISBN:978-1-4799-8875-4.
• [17] Moggi E. Computational lambda-calculus and monads. Technical report, Edinburgh University, 1988. Tech. Report ECS-LFCS-88-66.
• [18] Moggi E. Computational Lambda-Calculus and Monads. In: Proceedings of the 4th Symposium on Logic in Computer Science (LICS’89). IEEE Computer Society. 1989 pp. 14-23. ISBN:0-8186-1954-6.
• [19] Sabry A, Felleisen M. Reasoning About Programs in Continuation-passing Style. SIGPLAN Lisp Pointers, 1992. V(1):288-298. doi:10.1145/141478.141563.
• [20] Sabry A, Felleisen M. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 1993. 6(3-4):289-360. doi:10.1007/BF01019462.
• [21] Maraist J, Odersky M, Turner DN, Wadler P. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Electronic Notes in Theoretical Computer Science, 1995. 1:370-392. URL https://doi.org/10.1016/S1571-0661(04)00022-2.
• [22] Sabry A, Wadler P. A Reflection on Call-by-Value. ACM Transactions on Programming Languages and Systems, 1997. 19(6):916-941.
• [23] Maraist J. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theoretical Computer Science, 1999. 228(1-2):175-210. doi:10.1016/S0304-3975(98)00358-2.
• [24] Guerrieri G. Head reduction and normalization in a call-by-value lambda-calculus. In: 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015), volume 46 of OpenAccess Series in Informatics (OASIcs) 2015 pp. 3-17. ISBN:978-3-939897-94-1.
• [25] Accattoli B, Guerrieri G. Open Call-by-Value. In: Programming Languages and Systems - 14th Asian Symposium (APLAS 2016), volume 10017 of Lecture Notes in Computer Science. Springer-Verlag, 2016 pp. 206-226.
• [26] Ehrhard T, Guerrieri G. The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016). ACM. ISBN 978-1-4503-4148-6, 2016 pp. 174-187. URL https://arxiv.org/abs/1701.08186.
• [27] Barendregt H. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundation of mathematics. North-Holland, revised edition, 1984. ISBN:0444867481, 9780444867483.
• [28] Ronchi Della Rocca S, Paolini L. The Parametric λ-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS Series. Springer, 2004. doi:10.1007/978-3-662-10394-4.
• [29] Hindley JR, Longo G. Lambda calculus models and extensionality. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 1980. 26:289-310. URL https://doi.org/10.1002/malq.19800261902.
• [30] Regnier L. Une équivalence sur les lambda-termes. Theoretical Computer Science, 1994. 126(2):281-292. URL https://doi.org/10.1016/0304-3975(94)90012-4.
• [31] de Carvalho D. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 2018. 28(7):1169-1203. URL https://doi.org/10.1017/S0960129516000396.
• [32] Paolini L, Piccolo M, Ronchi Della Rocca S. Essential and relational models. Mathematical Structures in Computer Science, 2017. 27(5):626-650. URL https://doi.org/10.1017/S0960129515000316.
• [33] Breuvart F, Manzonetto G, Ruoppolo D. Relational Graph Models at Work. Logical Methods in Computer Science, 2018. 14(3):1-43 doi:10.23638/LMCS-14(3:2)2018.
• [34] Guerrieri G. Personal communication, 2017.
• [35] Kerinec E, Manzonetto G, Pagani M. Revisiting Call-by-value Böhm trees in light of their Taylor expansion. CoRR, 2018. abs/1809.02659.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).