Document Open Access Logo

Normalization Without Syntax

Authors Willem B. Heijltjes, Dominic J. D. Hughes, Lutz Straßburger

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.19.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Author Details

Willem B. Heijltjes
  • Department of Computer Science, University of Bath, UK
Dominic J. D. Hughes
  • Logic Group, University of California Berkeley, CA, USA
Lutz Straßburger
  • Equipe Partout, Inria Saclay, Palaiseau, France

Funding

Supported by EPSRC Grant EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing and Inria Associated Team Combinatorial Proof Normalization (COMPRONOM).

Acknowledgements

Dominic Hughes would like to thank Wes Holliday, his host at U.C. Berkeley. We thank the referees for their diligence.

Cite AsGet BibTex

Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Normalization Without Syntax. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.19

Abstract

We present normalization for intuitionistic combinatorial proofs (ICPs) and relate it to the simply-typed lambda-calculus. We prove confluence and strong normalization. Combinatorial proofs, or "proofs without syntax", form a graphical semantics of proof in various logics that is canonical yet complexity-aware: they are a polynomial-sized representation of sequent proofs that factors out exactly the non-duplicating permutations. Our approach to normalization aligns with these characteristics: it is canonical (free of permutations) and generic (readily applied to other logics). Our reduction mechanism is a canonical representation of reduction in sequent calculus with closed cuts (no abstraction is allowed below a cut), and relates to closed reduction in lambda-calculus and supercombinators. While we will use ICPs concretely, the notion of reduction is completely abstract, and can be specialized to give a reduction mechanism for any representation of typed normal forms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Lambda calculus
Keywords
  • combinatorial proofs
  • intuitionistic logic
  • lambda-calculus
  • Curry-Howard
  • proof nets

Metrics

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

Related Versions

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation, 163:409-470, 1996. Google Scholar
  2. Matteo Acclavio and Lutz Straßburger. On combinatorial proofs for logics of relevance and entailment. In Rosalie Iemhoff and Michael Moortgat, editors, 26th Workshop on Logic, Language, Information and Computation (WoLLIC 2019). Springer, 2019. Google Scholar
  3. Matteo Acclavio and Lutz Straßburger. On combinatorial proofs for modal logic. In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings, volume 11714 of Lecture Notes in Computer Science, pages 223-240. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29026-9_13.
  4. Gianluigi Bellin and Jacques van de Wiele. Subnets of proof-nets in MLL^-. In Advances in Linear Logic, pages 249-270, 1995. Google Scholar
  5. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In 6th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 203-212, 1991. Google Scholar
  6. Kim B. Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231-247, 1992. Google Scholar
  7. Naim Cagman and J. Roger Hindley. Combinatory weak reduction in lambda calculus. Theoretical Computer Science, 198(1-2):239-249, 1998. Google Scholar
  8. Roberto Di Cosmo. A short survey of isomorphisms of types. Mathematical structures in computer science, 15(5):825-838, 2005. Google Scholar
  9. Gerhard Gentzen. Untersuchungen über das logische Schließen I, II. Mathematische Zeitschrift, 39:176-210, 405-431, 1934-1935. English translation in: The Collected Papers of Gerhard Gentzen, M.E. Szabo (ed.), North-Holland 1969. Google Scholar
  10. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987. Google Scholar
  11. Jean-Yves Girard. Geometry of interaction 2: Deadlock-free algorithms. In International Conference on Computer Logic, pages 76-93, 1988. Google Scholar
  12. Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. Logic and Algebra, pages 97-124, 1996. Google Scholar
  13. Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301-506, 2001. URL: https://doi.org/10.1017/S096012950100336X.
  14. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1989. Google Scholar
  15. Willem Heijltjes. Proof nets for additive linear logic with units. In IEEE 26th Annual Symposium on Logic in Computer Science (LICS), pages 207-216, 2011. Google Scholar
  16. Willem Heijltjes, Dominic Hughes, and Lutz Straßburger. Intuitionistic proofs without syntax. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2019. Google Scholar
  17. Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Normalization without syntax. Technical Report HAL-03654060, Inria, 2022. URL: https://hal.inria.fr/hal-03654060.
  18. Dominic Hughes. Proofs without syntax. Annals of Mathematics, 164(3):1065-1076, 2006. Google Scholar
  19. Dominic Hughes and Willem Heijltjes. Conflict nets: efficient locally canonical mall proof nets. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016. Google Scholar
  20. Dominic Hughes and Rob van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. Transactions on Computational Logic, 6(4):784-842, 2005. Google Scholar
  21. Dominic J. D. Hughes. First-order proofs without syntax, 2019. arXiv preprint 1906.11236. URL: http://arxiv.org/abs/1906.11236.
  22. Dominic J. D. Hughes, Lutz Straßburger, and Jui-Hsuan Wu. Combinatorial proofs and decomposition theorems for first-order logic. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470579.
  23. Dominic J.D. Hughes. Simple free star-autonomous categories and full coherence. Journal of Pure and Applied Algebra, 216(11):2386-2410, 2012. Google Scholar
  24. R.J.M. Hughes. Super-combinators: a new implementation method for applicative languages. In ACM Symposium on Lisp and Functional Programming, pages 1-10, 1982. Google Scholar
  25. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000. Google Scholar
  26. Thomas Johnsson. Lambda lifting: Transforming programs to recursive equations. In Conference on Functional Programming Languages and Computer Architecture, volume 201 of LNCS, pages 190-203, 1985. Google Scholar
  27. Yves Lafont. Interaction nets. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 95-108, 1990. Google Scholar
  28. Stéphane Lengrand. Normalisation and equivalence in proof theory and type theory. PhD thesis, University of St. Andrews, 2006. Google Scholar
  29. Simon L. Peyton-Jones. The implementation of functional programming languages. Prentice Hall, 1987. Google Scholar
  30. Andrea Aler Tubella and Lutz Straßburger. Introduction to deep inference. Lecture notes for ESSLLI'19, 2019. URL: https://hal.inria.fr/hal-02390267.
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