Normalization Without Syntax
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.
combinatorial proofs
intuitionistic logic
lambda-calculus
Curry-Howard
proof nets
Theory of computation~Proof theory
Theory of computation~Lambda calculus
19:1-19:19
Regular Paper
Supported by EPSRC Grant EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing and Inria Associated Team Combinatorial Proof Normalization (COMPRONOM).
https://hal.inria.fr/hal-03654060
Dominic Hughes would like to thank Wes Holliday, his host at U.C. Berkeley. We thank the referees for their diligence.
Willem B.
Heijltjes
Willem B. Heijltjes
Department of Computer Science, University of Bath, UK
Dominic J. D.
Hughes
Dominic J. D. Hughes
Logic Group, University of California Berkeley, CA, USA
Lutz
Straßburger
Lutz Straßburger
Equipe Partout, Inria Saclay, Palaiseau, France
10.4230/LIPIcs.FSCD.2022.19
Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation, 163:409-470, 1996.
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.
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.
https://doi.org/10.1007/978-3-030-29026-9_13
Gianluigi Bellin and Jacques van de Wiele. Subnets of proof-nets in MLL^-. In Advances in Linear Logic, pages 249-270, 1995.
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.
Kim B. Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231-247, 1992.
Naim Cagman and J. Roger Hindley. Combinatory weak reduction in lambda calculus. Theoretical Computer Science, 198(1-2):239-249, 1998.
Roberto Di Cosmo. A short survey of isomorphisms of types. Mathematical structures in computer science, 15(5):825-838, 2005.
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.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987.
Jean-Yves Girard. Geometry of interaction 2: Deadlock-free algorithms. In International Conference on Computer Logic, pages 76-93, 1988.
Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. Logic and Algebra, pages 97-124, 1996.
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.
https://doi.org/10.1017/S096012950100336X
Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1989.
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.
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.
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.
https://hal.inria.fr/hal-03654060
Dominic Hughes. Proofs without syntax. Annals of Mathematics, 164(3):1065-1076, 2006.
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.
Dominic Hughes and Rob van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. Transactions on Computational Logic, 6(4):784-842, 2005.
Dominic J. D. Hughes. First-order proofs without syntax, 2019. arXiv preprint 1906.11236. URL: http://arxiv.org/abs/1906.11236.
http://arxiv.org/abs/1906.11236
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.
https://doi.org/10.1109/LICS52264.2021.9470579
Dominic J.D. Hughes. Simple free star-autonomous categories and full coherence. Journal of Pure and Applied Algebra, 216(11):2386-2410, 2012.
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.
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.
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.
Yves Lafont. Interaction nets. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 95-108, 1990.
Stéphane Lengrand. Normalisation and equivalence in proof theory and type theory. PhD thesis, University of St. Andrews, 2006.
Simon L. Peyton-Jones. The implementation of functional programming languages. Prentice Hall, 1987.
Andrea Aler Tubella and Lutz Straßburger. Introduction to deep inference. Lecture notes for ESSLLI'19, 2019. URL: https://hal.inria.fr/hal-02390267.
https://hal.inria.fr/hal-02390267
Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode