TY - GEN
T1 - Normalization Without Syntax
AU - Heijltjes, Willem B.
AU - Hughes, Dominic J.D.
AU - Straßburger, Lutz
N1 - Publisher Copyright:
© Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger
PY - 2022/6/1
Y1 - 2022/6/1
N2 - 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.
AB - 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.
KW - Curry–Howard
KW - combinatorial proofs
KW - intuitionistic logic
KW - lambda-calculus
KW - proof nets
U2 - 10.4230/LIPIcs.FSCD.2022.19
DO - 10.4230/LIPIcs.FSCD.2022.19
M3 - Conference contribution
AN - SCOPUS:85133696430
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
A2 - Felty, Amy P.
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
Y2 - 2 August 2022 through 5 August 2022
ER -