Normalization Without Syntax

Willem Heijltjes; Dominic Hughes; Lutz Strassburger

doi:10.4230/LIPIcs.FSCD.2022.19

Normalization Without Syntax

Willem Heijltjes
, Dominic Hughes
, Lutz Strassburger

INRIA Saclay

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

82 Downloads (Pure)

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.

Original language	English
Title of host publication	7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
Subtitle of host publication	FSCD 2022
Editors	Amy P. Felty
Place of Publication	Dagstuhl, Germany
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages	19:1-19:19
Number of pages	19
Volume	228
Edition	2022
ISBN (Electronic)	978-3-95977-233-4
DOIs	https://doi.org/10.4230/LIPIcs.FSCD.2022.19
Publication status	Published - 28 Jun 2022

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	228
ISSN (Print)	1868-8969

Bibliographical note

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

Publisher Copyright:
© Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger

Keywords

Curry–Howard
combinatorial proofs
intuitionistic logic
lambda-calculus
proof nets

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.FSCD.2022.19Licence: CC BY

Normalization Without SyntaxFinal published version, 812 KBLicence: CC BY

Cite this

Heijltjes, W., Hughes, D., & Strassburger, L. (2022). Normalization Without Syntax. In A. P. Felty (Ed.), 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022: FSCD 2022 (2022 ed., Vol. 228, pp. 19:1-19:19). Article 19 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 228). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2022.19

Normalization Without Syntax. / Heijltjes, Willem; Hughes, Dominic; Strassburger, Lutz.
7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022: FSCD 2022. ed. / Amy P. Felty. Vol. 228 2022. ed. Dagstuhl, Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2022. p. 19:1-19:19 19 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 228).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Heijltjes, W, Hughes, D & Strassburger, L 2022, Normalization Without Syntax. in AP Felty (ed.), 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022: FSCD 2022. 2022 edn, vol. 228, 19, Leibniz International Proceedings in Informatics, LIPIcs, vol. 228, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Dagstuhl, Germany, pp. 19:1-19:19. https://doi.org/10.4230/LIPIcs.FSCD.2022.19

Heijltjes W, Hughes D, Strassburger L. Normalization Without Syntax. In Felty AP, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022: FSCD 2022. 2022 ed. Vol. 228. Dagstuhl, Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2022. p. 19:1-19:19. 19. (Leibniz International Proceedings in Informatics, LIPIcs). doi: 10.4230/LIPIcs.FSCD.2022.19

Heijltjes, Willem ; Hughes, Dominic ; Strassburger, Lutz. / Normalization Without Syntax. 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022: FSCD 2022. editor / Amy P. Felty. Vol. 228 2022. ed. Dagstuhl, Germany : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2022. pp. 19:1-19:19 (Leibniz International Proceedings in Informatics, LIPIcs).

@inproceedings{ef4a14fc15d14c18b959616ec0d1bd12,

title = "Normalization Without Syntax",

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.",

keywords = "Curry–Howard, combinatorial proofs, intuitionistic logic, lambda-calculus, proof nets",

author = "Willem Heijltjes and Dominic Hughes and Lutz Strassburger",

note = "Funding Information: Funding Supported by EPSRC Grant EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing and Inria Associated Team Combinatorial Proof Normalization (COMPRONOM). Publisher Copyright: {\textcopyright} Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Stra{\ss}burger",

year = "2022",

month = jun,

day = "28",

doi = "10.4230/LIPIcs.FSCD.2022.19",

language = "English",

volume = "228",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

pages = "19:1--19:19",

editor = "Felty, \{Amy P.\}",

booktitle = "7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022",

address = "Germany",

edition = "2022",

}

TY - GEN

T1 - Normalization Without Syntax

AU - Heijltjes, Willem

AU - Hughes, Dominic

AU - Strassburger, Lutz

N1 - Funding Information: Funding Supported by EPSRC Grant EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing and Inria Associated Team Combinatorial Proof Normalization (COMPRONOM). Publisher Copyright: © Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger

PY - 2022/6/28

Y1 - 2022/6/28

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

UR - https://www.scopus.com/pages/publications/85133696430

U2 - 10.4230/LIPIcs.FSCD.2022.19

DO - 10.4230/LIPIcs.FSCD.2022.19

M3 - Chapter in a published conference proceeding

VL - 228

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 19:1-19:19

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

CY - Dagstuhl, Germany

ER -

Normalization Without Syntax

Abstract

Publication series

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Typed Lambda-Calculi with Sharing and Unsharing

Cite this

Normalization Without Syntax

Abstract

Publication series

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this