Document Open Access Logo

Meaningfulness and Genericity in a Subsuming Framework (Invited Talk)

Authors Delia Kesner , Victor Arrial , Giulio Guerrieri

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.1.pdf
  • Filesize: 0.92 MB
  • 24 pages

Document Identifiers

Author Details

Delia Kesner
  • Université Paris Cité - CNRS - IRIF, France
Victor Arrial
  • Université Paris Cité - CNRS - IRIF, France
Giulio Guerrieri
  • University of Sussex, Department of Informatics, Brighton, United Kingdom

Cite AsGet BibTex

Delia Kesner, Victor Arrial, and Giulio Guerrieri. Meaningfulness and Genericity in a Subsuming Framework (Invited Talk). In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.1

Abstract

This paper studies the notion of meaningfulness for a unifying framework called dBang-calculus, which subsumes both call-by-name (dCBN) and call-by-value (dCBV). We first define meaningfulness in dBang and then characterize it by means of typability and inhabitation in an associated non-idempotent intersection type system previously appearing in the literature. We validate the proposed notion of meaningfulness by showing two properties: (1) consistency of the smallest theory, called ℋ, equating all meaningless terms, and (2) genericity, stating that meaningless subterms have no bearing on the significance of meaningful terms. The theory ℋ is also shown to have a unique consistent and maximal extension ℋ*, which coincides with a well-known notion of observational equivalence. Last but not least, we show that the notions of meaningfulness and genericity in the literature for dCBN and dCBV are subsumed by the corresponding ones proposed here for the dBang-calculus.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
Keywords
  • Lambda calculus
  • Solvability
  • Meaningfulness
  • Inhabitation
  • Genericity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Beniamino Accattoli. An abstract factorization theorem for explicit substitutions. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, volume 15 of LIPIcs, pages 6-21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPICS.RTA.2012.6.
  2. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 659-670. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535886.
  3. Beniamino Accattoli, Claudia Faggian, and Adrienne Lancelot. Normal form bisimulations by value. CoRR, abs/2303.08161, 2023. URL: https://doi.org/10.48550/arXiv.2303.08161.
  4. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds, fully developed. Journal of Functional Programming, 30:e14, 2020. URL: https://doi.org/10.1017/S095679682000012X.
  5. Beniamino Accattoli and Giulio Guerrieri. Call-by-value solvability and multi types. CoRR, abs/2202.03079, 2022. URL: https://arxiv.org/abs/2202.03079.
  6. Beniamino Accattoli and Giulio Guerrieri. The theory of call-by-value solvability. Proceedings of the ACM on Programming Languages, 6(ICFP):855-885, 2022. URL: https://doi.org/10.1145/3547652.
  7. Beniamino Accattoli and Delia Kesner. The structural lambda-calculus. In Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 381-395. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_30.
  8. Beniamino Accattoli and Delia Kesner. The permutative λ-calculus. In Nikolaj S. Bjørner and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, volume 7180 of Lecture Notes in Computer Science, pages 23-36. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28717-6_5.
  9. Beniamino Accattoli and Delia Kesner. Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Log. Methods Comput. Sci., 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:28)2012.
  10. Beniamino Accattoli and Adrienne Lancelot. Light genericity. In Naoki Kobayashi and James Worrell, editors, Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II, volume 14575 of Lecture Notes in Computer Science, pages 24-46. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57231-9_2.
  11. Beniamino Accattoli and Luca Paolini. Call-by-value solvability, revisited. In Functional and Logic Programming - 11th International Symposium, FLOPS 2012. Proceedings, volume 7294 of Lecture Notes in Computer Science, pages 4-16. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29822-6_4.
  12. Sandra Alves, Delia Kesner, and Daniel Ventura. A quantitative understanding of pattern matching, 2019. URL: https://arxiv.org/abs/1912.01914.
  13. Victor Arrial, Giulio Guerrieri, and Delia Kesner. Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework. Proceedings of the ACM on Programming Languages, 7(POPL):51:1483-51:1513, January 2023. URL: https://doi.org/10.1145/3571244.
  14. Victor Arrial, Giulio Guerrieri, and Delia Kesner. The benefits of diligence. In Chris Benzmüller, Marijn Heule, and Renate Schmidt, editors, 12th International Joint Conference on Automated Reasoning (IJCAR), 2024, Proceedings, Lecture Notes in Artificial Intelligence. Springer, 2024. Google Scholar
  15. Victor Arrial, Giulio Guerrieri, and Delia Kesner. Genericity through stratification. CoRR, abs/2401.12212, 2024. URL: https://doi.org/10.48550/arXiv.2401.12212.
  16. Davide Barbarossa and Giulio Manzonetto. Taylor subsumes scott, berry, kahn and plotkin. Proc. ACM Program. Lang., 4(POPL):1:1-1:23, 2020. URL: https://doi.org/10.1145/3371069.
  17. Henk Barendregt. Some extensional term models for combinatory logics and λ-calculi. PhD thesis, Univ. Utrecht, January 1971. Google Scholar
  18. Henk Barendregt. A characterization of terms of the lambda i-calculus having a normal form. Journal Symbolic Logic, 38(3):441-445, 1973. URL: https://doi.org/10.2307/2273041.
  19. Henk Barendregt. Solvability in lambda-calculi. In M. Guillaume, editor, Colloque international de logique: Clermont-Ferrand, 18-25 juillet 1975, pages 209-219, Paris, 1977. Éditions du CNRS. Google Scholar
  20. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundation of mathematics. North-Holland, Amsterdam, revised edition, 1984. Google Scholar
  21. Jan Bessai, Tzu-Chun Chen, Andrej Dudenhefner, Boris Düdder, Ugo de'Liguoro, and Jakob Rehof. Mixin composition synthesis based on intersection types. CoRR, abs/1712.06906, 2017. URL: https://arxiv.org/abs/1712.06906.
  22. Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Proving soundness of extensional normal-form bisimilarities. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:31)2019.
  23. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. In Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Proceedings, volume 12073 of Lecture Notes in Computer Science, pages 13-32. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59025-3_2.
  24. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. Inf. Comput., 293:105047, 2023. URL: https://doi.org/10.1016/J.IC.2023.105047.
  25. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. The inhabitation problem for non-idempotent intersection types. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, volume 8705 of Lecture Notes in Computer Science, pages 341-354. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44602-7_26.
  26. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Solvability = Typability + Inhabitation. Logical Methods in Computer Science, Volume 17, Issue 1, January 2021. URL: https://doi.org/10.23638/LMCS-17(1:7)2021.
  27. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Solvability = typability + inhabitation. Logical Methods in Computer Science, 17(1), 2021. URL: https://lmcs.episciences.org/7141.
  28. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Inhabitation for non-idempotent intersection types. Logical Methods in Computer Science, 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:7)2018.
  29. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability for pair pattern calculi. In TLCA, volume 38 of LIPIcs, pages 123-137. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl Publishing, 2015. Google Scholar
  30. Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 103-118, Grenoble, France, 2014. Springer. URL: https://doi.org/10.1007/978-3-642-54830-7_7.
  31. Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type assignment for λ-terms. Archiv für mathematische Logik und Grundlagenforschung, 19(1):139-156, 1978. URL: https://doi.org/10.1007/BF02011875.
  32. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, 1980. URL: https://doi.org/10.1305/ndjfl/1093883253.
  33. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Mathematical Logic Quarterly, 27(2-6):45-58, 1981. URL: https://doi.org/10.1002/malq.19810270205.
  34. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), pages 233-243. ACM, 2000. URL: https://doi.org/10.1145/351240.351262.
  35. Pierre-Louis Curien and Guillaume Munch-Maccagnoni. The duality of computation under focus. In Cristian S. Calude and Vladimiro Sassone, editors, Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010. Proceedings, volume 323 of IFIP Advances in Information and Communication Technology, pages 165-181. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15240-5_13.
  36. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. PhD thesis, Université Aix-Marseille II, 2007. Google Scholar
  37. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  38. Thomas Ehrhard. Call-by-push-value from a linear logic point of view. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 202-228, Eindhoven, The Netherlands, 2016. Springer. URL: https://doi.org/10.1007/978-3-662-49498-1_9.
  39. Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In James Cheney and Germán Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pages 174-187, Edinburgh, United Kingdom, 2016. ACM. URL: https://doi.org/10.1145/2967973.2968608.
  40. José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Modal embeddings and calling paradigms. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, volume 131 of LIPIcs, pages 18:1-18:20. Schloss Dagstuhl, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.18.
  41. Claudia Faggian and Giulio Guerrieri. Factorization in call-by-name and call-by-value calculi via linear logic. In Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings, volume 12650 of Lecture Notes in Computer Science, pages 205-225. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_11.
  42. Álvaro García-Pérez and Pablo Nogueira. No solvable lambda-value term left behind. Logical Methods in Computer Science, 12(2):1-43, 2016. URL: https://doi.org/10.2168/LMCS-12(2:12)2016.
  43. Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, pages 555-574, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. Google Scholar
  44. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  45. Jean-Yves Girard. On the unity of logic. Ann. Pure Appl. Log., 59(3):201-217, 1993. URL: https://doi.org/10.1016/0168-0072(93)90093-S.
  46. Giulio Guerrieri and Giulio Manzonetto. The bang calculus and the two girard’s translations. In Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, volume 292 of EPTCS, pages 15-30, Oxford, UK, 2018. URL: https://doi.org/10.4204/EPTCS.292.2.
  47. Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization and conservativity of a refined call-by-value lambda-calculus. Logical Methods Computer Science, 13(4):1-27, 2017. URL: https://doi.org/10.23638/LMCS-13(4:29)2017.
  48. Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries. Meaningless terms in rewriting. J. Funct. Log. Program., 1999(1), 1999. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-01/A99-01.html.
  49. Axel Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting call-by-value böhm trees in light of their taylor expansion. Logical Methods in Computer Science, 16(3):6:1-6:26, 2020. URL: https://lmcs.episciences.org/6638.
  50. Delia Kesner, Victor Arrial, and Giulio Guerrieri. Meaningfulness and genericity in a subsuming framework. CoRR, abs/2404.06361, 2024. URL: https://arxiv.org/abs/2404.06361.
  51. Delia Kesner and Shane Ó Conchúir. Milner’s lambda-calculus with partial substitutions. CoRR, abs/2312.13270, 2023. URL: https://doi.org/10.48550/arXiv.2312.13270.
  52. Delia Kesner and Andrés Viso. Encoding tight typing in a unified framework. In 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, volume 216 of LIPIcs, pages 27:1-27:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CSL.2022.27.
  53. Søren B. Lassen. Eager normal form bisimulation. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 345-354. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/LICS.2005.15.
  54. Paul Blain Levy. Call-by-push-value: A subsuming paradigm. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, pages 228-243, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-48959-2_17.
  55. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004. Google Scholar
  56. Zohar Manna and Richard J. Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems, 2(1):90-121, 1980. URL: https://doi.org/10.1145/357084.357090.
  57. John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. In Stephen D. Brookes, Michael G. Main, Austin Melton, and Michael W. Mislove, editors, Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 1995, Tulane University, New Orleans, LA, USA, March 29 - April 1, 1995, volume 1 of Electronic Notes in Theoretical Computer Science, pages 370-392. Elsevier, 1995. URL: https://doi.org/10.1016/S1571-0661(04)00022-2.
  58. John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theor. Comput. Sci., 228(1-2):175-210, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00358-2.
  59. Robin Milner. Local bigraphs and confluence: two conjectures. In Roberto Amadio and Iain Phillips, editors, Proceedings of the 13th Int. Workshop on Expressiveness in Concurrency (EXPRESS), volume 175, pages 65-73. Electronic Notes in Theoretical Computer Science, 2006. URL: https://doi.org/10.1016/j.entcs.2006.07.035.
  60. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 14-23. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39155.
  61. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  62. Guillaume Munch-Maccagnoni. Focalisation and classical realisability. In Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL. Proceedings, volume 5771 of Lecture Notes in Computer Science, pages 409-423. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04027-6_30.
  63. Luca Paolini, Elaine Pimentel, and Simona Ronchi Della Rocca. An operational characterization of strong normalization. In Luca Aceto and Anna Ingólfsdóttir, editors, Foundations of Software Science and Computation Structures, 9th International Conference, FOSSACS 2006, Proceedings, volume 3921 of Lecture Notes in Computer Science, pages 367-381, Vienna, Austria, 2006. Springer. URL: https://doi.org/10.1007/11690634_25.
  64. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value solvability. RAIRO Theoretical Informatics and Applications, 33(6):507-534, 1999. URL: https://doi.org/10.1051/ita:1999130.
  65. Daniele Pautasso and Simona Ronchi Della Rocca. A quantitative version of simple types. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 29:1-29:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSCD.2023.29.
  66. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  67. Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. In To H.B.Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, pages 561-577. Academic Press, 1980. Google Scholar
  68. Dag Prawitz. Classical versus intuitionistic logic. Why is this a Proof?, volume 27. College Publications, 2017. Google Scholar
  69. Miguel Ramos. Embedding the distant bang calculus with pattern-matching primitives, 2024. Personal Communication. Google Scholar
  70. Laurent Regnier. Une équivalence sur les lambda-termes. Theoretical Computer Science, 126(2):281-292, 1994. URL: https://doi.org/10.1016/0304-3975(94)90012-4.
  71. Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus - A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-10394-4.
  72. Simona Ronchi Della Rocca and Luca Roversi. Lambda calculus and intuitionistic linear logic. Stud Logica, 59(3):417-448, 1997. URL: https://doi.org/10.1023/A:1005092630115.
  73. Nicolas Wu Steffen van Bakel, Emma Tye. A calculus of delayed reductions. In PPDP 2023: 25th International Symposium on Principles and Practice of Declarative Programming, Cascais, Lisbon, Portugal, October 22 - 23, 2022. ACM, 2023. Google Scholar
  74. Pawel Urzyczyn. The emptiness problem for intersection types. Journal of Symbolic Logic, 64(3):1195-1215, 1999. URL: https://doi.org/10.2307/2586625.
  75. Christopher P. Wadsworth. Semantics and pragmatics of the lambda-calculus. Ph.D., University of Oxford, 1971. Accepted: 1971. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.476186.
  76. Christopher P. Wadsworth. The Relation between Computational and Denotational Properties for Scott’s D_∞-Models of the Lambda-Calculus. SIAM Journal on Computing, 5(3):488-521, September 1976. Publisher: Society for Industrial and Applied Mathematics. URL: https://doi.org/10.1137/0205036.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact