Document Open Access Logo

A Positive Perspective on Term Representation (Invited Talk)

Authors Dale Miller , Jui-Hsuan Wu

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.3.pdf
  • Filesize: 0.82 MB
  • 21 pages

Document Identifiers

Author Details

Dale Miller
  • Inria Saclay, Palaiseau, France
  • LIX, Institut Polytechnique de Paris, France
Jui-Hsuan Wu
  • LIX, Institut Polytechnique de Paris, France

Acknowledgements

We thank Beniamino Accattoli and Kaustuv Chaudhuri for their valuable discussions and suggestions. We also thank anonymous reviewers for their comments on an earlier draft of this paper.

Cite AsGet BibTex

Dale Miller and Jui-Hsuan Wu. A Positive Perspective on Term Representation (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.3

Abstract

We use the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative polarity, LJF proofs encode terms as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given the positive polarity, LJF proofs yield a structure in which explicit sharing of term structures is possible. Such a representation of terms provides an explicit method for sharing term structures. In this setting, cut elimination yields a different notion of substitution. We illustrate these two approaches to term representation by applying them to the encoding of untyped λ-terms. We also exploit concurrency theory techniques - namely traces and simulation - to compare untyped λ-terms using such different structuring disciplines.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • term representation
  • sharing
  • focused proof systems

Metrics

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

Related Versions

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. of Logic and Computation, 2(3):297-347, 1992. URL: https://doi.org/10.1093/logcom/2.3.297.
  2. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. Journal of Formalized Reasoning, 7(2):1-89, 2014. URL: https://doi.org/10.6092/issn.1972-5787/4650.
  3. Taus Brock-Nannestad, Nicolas Guenot, and Daniel Gustafsson. Computation in focused intuitionistic logic. In Moreno Falaschi and Elvira Albert, editors, Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14-16, 2015, pages 43-54. ACM, 2015. URL: https://doi.org/10.1145/2790449.2790528.
  4. Paola Bruscoli and Alessio Guglielmi. On structuring proof search for first order linear logic. Theoretical Computer Science, 360(1-3):42-76, 2006. URL: https://doi.org/10.1016/j.tcs.2005.11.047.
  5. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Journal of Logic and Computation, 13(5):639-688, 2003. URL: https://doi.org/10.1093/logcom/13.5.639.
  6. Kaustuv Chaudhuri. Focusing strategies in the sequent calculus of synthetic connectives. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, LPAR: International Conference on Logic, Programming, Artificial Intelligence and Reasoning, volume 5330 of LNCS, pages 467-481. Springer, November 2008. URL: https://doi.org/10.1007/978-3-540-89439-1_33.
  7. Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A multi-focused proof system isomorphic to expansion proofs. J. of Logic and Computation, 26(2):577-603, 2016. URL: https://doi.org/10.1093/logcom/exu030.
  8. Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In G. Ausiello, J. Karhumäki, G. Mauri, and L. Ong, editors, Fifth International Conference on Theoretical Computer Science, volume 273 of IFIP, pages 383-396. Springer, September 2008. URL: https://doi.org/10.1007/978-0-387-09680-3_26.
  9. Andrea Condoluci, Beniamino Accattoli, and Claudio Sacerdoti Coen. Sharing equality is linear. In Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, pages 1-14, 2019. URL: https://doi.org/10.1145/3354166.3354174.
  10. Olivier Delande, Dale Miller, and Alexis Saurin. Proof and refutation in MALL as a game. Annals of Pure and Applied Logic, 161(5):654-672, February 2010. URL: https://doi.org/10.1016/j.apal.2009.07.017.
  11. Roy Dyckhoff and Stephane Lengrand. Call-by-value λ-calculus and LJQ. J. of Logic and Computation, 17(6):1109-1134, 2007. URL: https://doi.org/10.1093/logcom/exm037.
  12. José Espírito Santo. Completing herbelin’s programme. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4583 of LNCS, pages 118-132. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_10.
  13. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. ACM SIGPLAN Notices, 28(6):237-247, 1993. URL: https://doi.org/10.1145/155090.155113.
  14. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011. URL: https://doi.org/10.1016/j.ic.2010.09.004.
  15. Gerhard Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68-131. North-Holland, Amsterdam, 1935. Translation of articles that appeared in 1934-35. Collected papers appeared in 1969. URL: https://doi.org/10.1007/BF01201353.
  16. Ulysse Gérard and Dale Miller. Separating functional computation from relations. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of LIPIcs, pages 23:1-23:17, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.23.
  17. Jean-Yves Girard. A new constructive logic: classical logic. Math. Structures in Comp. Science, 1:255-296, 1991. URL: https://doi.org/10.1017/S0960129500001328.
  18. Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301-506, June 2001. URL: https://doi.org/10.1017/S096012950100336X.
  19. Clemens Grabmayer. Modeling terms by graphs with structure constraints (two illustrations). In Maribel Fernández and Ian Mackie, editors, TERMGRAPH@FSCD, volume 288 of EPTCS, pages 1-13, 2018. URL: https://doi.org/10.48550/arXiv.1902.02010.
  20. Stéphane Graham-Lengrand. Polarities and focussing: a journey from realisability to automated reasoning, December 2014. Habilitation à diriger des recherches. URL: https://tel.archives-ouvertes.fr/tel-01094980.
  21. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993. URL: https://doi.org/10.1145/138027.138060.
  22. Hugo Herbelin. A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure. In Computer Science Logic, 8th International Workshop, CSL '94, volume 933 of Lecture Notes in Computer Science, pages 61-75. Springer, 1995. URL: https://doi.org/10.1007/BFb0022247.
  23. Hugo Herbelin. Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes. PhD thesis, Université Paris 7, 1995. URL: https://tel.archives-ouvertes.fr/tel-00382528.
  24. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, 2009. Abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi. URL: https://doi.org/10.1016/j.tcs.2009.07.041.
  25. Chuck Liang and Dale Miller. A focused approach to combining logics. Annals of Pure and Applied Logic, 162(9):679-697, 2011. URL: https://doi.org/10.1016/j.apal.2011.01.012.
  26. Chuck Liang and Dale Miller. Focusing Gentzen’s LK proof system. In Thomas Piecha and Kai Wehmeier, editors, Peter Schroeder-Heister on Proof-Theoretic Semantics, Outstanding Contributions to Logic. Springer, 2022. To appear. URL: https://hal.archives-ouvertes.fr/hal-03457379.
  27. Sonia Marin, Dale Miller, Elaine Pimentel, and Marco Volpe. From axioms to synthetic inference rules via focusing. Annals of Pure and Applied Logic, 173(5):1-32, 2022. URL: https://doi.org/10.1016/j.apal.2022.103091.
  28. Dale Miller. Mechanized metatheory revisited. Journal of Automated Reasoning, 63(3):625-665, October 2019. URL: https://doi.org/10.1007/s10817-018-9483-3.
  29. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, June 2012. URL: https://doi.org/10.1017/CBO9781139021326.
  30. Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51(1-2):125-157, 1991. URL: https://doi.org/10.1016/0168-0072(91)90068-W.
  31. Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. on Computational Logic, 6(4):749-783, October 2005. URL: https://doi.org/10.1145/1094622.1094628.
  32. Dale Miller and Jui-Hsuan Wu. A positive perspective on term representations: Extended paper. Technical report, Inria, 2022. URL: https://hal.inria.fr/hal-03843587.
  33. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Part II. Information and Computation, 100(1):41-77, 1992. URL: https://doi.org/10.1016/0890-5401(92)90009-5.
  34. Guillaume Munch-Maccagnoni and Gabriel Scherer. Polarised intermediate representation of lambda calculus with sums. In 30th Symp. on Logic in Computer Science, pages 127-140. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.22.
  35. Elaine Pimentel, Vivek Nigam, and João Neto. Multi-focused proofs with different polarity assignments. In Mario Benevides and Rene Thiemann, editors, Proc. of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015), volume 323 of ENTCS, pages 163-179, July 2016. URL: https://doi.org/10.1016/j.entcs.2016.06.011.
  36. 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.
  37. Robert J. Simmons. Structural focalization. ACM Trans. on Computational Logic, 15(3):21, 2014. URL: https://doi.org/10.1145/2629678.
  38. Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. on Computational Logic, 11(2):13:1-13:35, 2010. URL: https://doi.org/10.1145/1656242.1656248.
  39. Philip Wadler. Call-by-value is dual to call-by-name. In 8th Int. Conf. on Functional Programming, pages 189-201, New York, NY, 2003. ACM. URL: https://doi.org/10.1145/944705.944723.
  40. Keven Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: The propositional fragment. In Post-proceedings of TYPES 2003 Workshop, number 3085 in LNCS. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24849-1_23.
  41. Noam Zeilberger. Focusing and higher-order abstract syntax. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 359-369. ACM, 2008. URL: https://doi.org/10.1145/1328897.1328482.
  42. Noam Zeilberger. On the unity of duality. Annals of Pure and Applied Logic, 153(1), 2008. Special issue on classical logic and computation. URL: https://doi.org/10.1016/j.apal.2008.01.001.
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