eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-06-28
19:1
19:19
10.4230/LIPIcs.FSCD.2022.19
article
Normalization Without Syntax
Heijltjes, Willem B.
1
Hughes, Dominic J. D.
2
Straßburger, Lutz
3
Department of Computer Science, University of Bath, UK
Logic Group, University of California Berkeley, CA, USA
Equipe Partout, Inria Saclay, Palaiseau, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol228-fscd2022/LIPIcs.FSCD.2022.19/LIPIcs.FSCD.2022.19.pdf
combinatorial proofs
intuitionistic logic
lambda-calculus
Curry-Howard
proof nets