Document Open Access Logo

Solvability for Generalized Applications

Authors Delia Kesner , Loïc Peyrot

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.18.pdf
  • Filesize: 0.95 MB
  • 22 pages

Document Identifiers

Author Details

Delia Kesner
  • Université de Paris, CNRS, IRIF, France
  • Institut Universitaire de France, France
Loïc Peyrot
  • Université de Paris, CNRS, IRIF, France

Cite AsGet BibTex

Delia Kesner and Loïc Peyrot. Solvability for Generalized Applications. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.18

Abstract

Solvability is a key notion in the theory of call-by-name lambda-calculus, used in particular to identify meaningful terms. However, adapting this notion to other call-by-name calculi, or extending it to different models of computation - such as call-by-value - , is not straightforward. In this paper, we study solvability for call-by-name and call-by-value lambda-calculi with generalized applications, both variants inspired from von Plato’s natural deduction with generalized elimination rules. We develop an operational as well as a logical theory of solvability for each of them. The operational characterization relies on a notion of solvable reduction for generalized applications, and the logical characterization is given in terms of typability in an appropriate non-idempotent intersection type system. Finally, we show that solvability in generalized applications and solvability in the lambda-calculus are equivalent notions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Rewrite systems
  • Theory of computation → Type theory
Keywords
  • Lambda-calculus
  • Generalized applications
  • Solvability
  • CBN/CBV
  • Quantitative types

Metrics

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

References

  1. Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. J. Funct. Program., 1(4):375-416, 1991. URL: https://doi.org/10.1017/S0956796800000186.
  2. Beniamino Accattoli. Proof nets and the call-by-value λ-calculus. Theoretical Computer Science, 606:2-24, November 2015. URL: https://doi.org/10.1016/j.tcs.2015.08.006.
  3. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds, fully developed. J. Funct. Program., 30:e14, 2020. URL: https://doi.org/10.1017/S095679682000012X.
  4. Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. In Programming Languages and Systems, volume abs/1609.00322, pages 206-226. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_12.
  5. Beniamino Accattoli and Giulio Guerrieri. Call-by-value solvability and multi types. CoRR, abs/2202.03079, 2022. URL: http://arxiv.org/abs/2202.03079.
  6. Beniamino Accattoli and Delia Kesner. The structural λ-calculus. In Computer Science Logic, pages 381-395. Springer Berlin Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_30.
  7. Beniamino Accattoli and Luca Paolini. Call-by-value solvability, revisited. In Functional and Logic Programming, pages 4-16. Springer Berlin Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-29822-6_4.
  8. Henk Pieter Barendregt. The Lambda Calculus - Its Syntax and Semantics. Elsevier, 1984. URL: https://doi.org/10.1016/c2009-0-14341-6.
  9. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, volume 4646 of Lecture Notes in Computer Science, pages 298-312. Springer Berlin Heidelberg, Lausanne, Switzerland, September 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_24.
  10. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. In Functional and Logic Programming, pages 13-32. Springer International Publishing, 2020. URL: https://doi.org/10.1007/978-3-030-59025-3_2.
  11. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431-464, July 2017. URL: https://doi.org/10.1093/jigpal/jzx018.
  12. Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Lecture Notes in Computer Science, volume 8412, pages 103-118. Springer Berlin Heidelberg, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_7.
  13. M. Coppo and M. Dezani-Ciancaglini. A new type assignment for λ-terms. Archiv für Mathematische Logik und Grundlagenforschung, 19(1):139-156, December 1978. URL: https://doi.org/10.1007/bf02011875.
  14. Daniel De Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169-1203, January 2017. URL: https://doi.org/10.1017/s0960129516000396.
  15. José Espírito Santo. Delayed substitutions. In Lecture Notes in Computer Science, pages 169-183. Springer Berlin Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-73449-9_14.
  16. José Espírito Santo. The call-by-value lambda-calculus with generalized applications. In 28th EASCL Annual Conference on Computer Science Logic (CSL 2020). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany, 2020. URL: https://doi.org/10.4230/LIPICS.CSL.2020.35.
  17. José Espírito Santo, Maria João Frade, and Luís Pinto. Permutability in proof terms for intuitionistic sequent calculus with cuts. In Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić, editors, 22nd International Conference on Types for Proofs and Programs (TYPES 2016), volume 97 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:27, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2016.10.
  18. José Espírito Santo, Delia Kesner, and Loïc Peyrot. A faithful and quantitative notion of distant reduction for generalized applications. In Proc. of the 24th Int. Conference on Foundations of Software Science and Computation Structures (FoSSaCS), LNCS, April 2022. URL: http://arxiv.org/abs/2201.04156.
  19. José Espírito Santo and Luís Pinto. A calculus of multiary sequent terms. ACM Transactions on Computational Logic, 12(3):1-41, May 2011. URL: https://doi.org/10.1145/1929954.1929959.
  20. Álvaro García-Pérez and Pablo Nogueira. No solvable lambda-value term left behind. Logical Methods in Computer Science, 12(2), June 2016. URL: https://doi.org/10.2168/lmcs-12(2:12)2016.
  21. Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, Lecture Notes in Computer Science, pages 555-574. Springer Berlin Heidelberg, Berlin, Heidelberg, 1994. URL: https://doi.org/10.1007/3-540-57887-0_115.
  22. Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization and conservativity of a refined call-by-value lambda-calculus. Logical Methods in Computer Science ; Volume 13, 2017. URL: https://doi.org/10.23638/LMCS-13(4:29)2017.
  23. Hugo Herbelin and Stéphane Zimmermann. An operational account of call-by-value minimal and classical λ-calculus in “natural deduction” form. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, pages 142-156, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-02273-9_12.
  24. Felix Joachimski and Ralph Matthes. Standardization and confluence for a lambda calculus with generalized applications. In Rewriting Techniques and Applications, pages 141-155. Springer Berlin Heidelberg, 2000. URL: https://doi.org/10.1007/10721975_10.
  25. Felix Joachimski and Ralph Matthes. Short proofs of normalization for the simply-typed λ-calculus, permutative conversions and Gödel’s T. Archive for Mathematical Logic, 42(1):59-87, 2003. URL: https://doi.org/10.1007/s00153-002-0156-9.
  26. Emma Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting Call-by-value Böhm trees in light of their Taylor expansion. Logical Methods in Computer Science, Volume 16, Issue 3, July 2020. URL: https://doi.org/10.23638/LMCS-16(3:6)2020.
  27. Delia Kesner. A theory of explicit substitutions with safe and full composition. Log. Methods Comput. Sci., 5(3), 2009. URL: http://arxiv.org/abs/0905.2539.
  28. Delia Kesner and Daniel Ventura. Quantitative types for the linear substitution calculus. In Josep Diaz, Ivan Lanese, and Davide Sangiorgi, editors, Lecture Notes in Computer Science, pages 296-310, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-44602-7_23.
  29. Delia Kesner and Andrés Viso. Encoding tight typing in a unified framework. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), 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.
  30. Ralph Matthes. Characterizing strongly normalizing terms for a lambda calculus with generalized applications via intersection types. In Proc. ICALP 2000 (Geneva), volume 8 of Proceedings in Informatics, pages 339-353, 2000. Google Scholar
  31. Luca Paolini. Call-by-Value Separability and Computability. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, Theoretical Computer Science, Lecture Notes in Computer Science, pages 74-89, Berlin, Heidelberg, 2001. Springer. URL: https://doi.org/10.1007/3-540-45446-2_5.
  32. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value solvability. RAIRO - Theoretical Informatics and Applications, 33(6):507-534, November 1999. URL: https://doi.org/10.1051/ita:1999130.
  33. Gordon Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1:125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  34. Neil Tennant. Ultimate normal forms for parallelized natural deductions. Logic Journal of IGPL, 10(3):299-337, 2002. URL: https://doi.org/10.1093/jigpal/10.3.299.
  35. Jan von Plato. Natural deduction with general elimination rules. Archive for Mathematical Logic, 40(7):541-567, 2001. URL: https://doi.org/10.1007/s001530100091.
  36. 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. 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