|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| Search | ||
| ||
2011 IEEE 26th Annual Symposium on Logic in Computer Science
Proof Nets for Additive Linear Logic with Units
Toronto, Ontario Canada
June 21-June 24
ISBN: 978-0-7695-4412-0
| ASCII Text | x | ||
| Willem Heijltjes, "Proof Nets for Additive Linear Logic with Units," Logic in Computer Science, Symposium on, pp. 207-216, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, 2011. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2011.9, author = {Willem Heijltjes}, title = {Proof Nets for Additive Linear Logic with Units}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2011}, issn = {1043-6871}, pages = {207-216}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2011.9}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - Proof Nets for Additive Linear Logic with Units SN - 1043-6871 SP207 EP216 A1 - Willem Heijltjes, PY - 2011 KW - proof nets KW - linear logic KW - graph rewriting VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2011.9
Additive linear logic, the fragment of linear logic concerning linear implication between strictly additive formulae, coincides with sum-product logic, the internal language of categories with free finite products and co products. Deciding equality of its proof terms, as imposed by the categorical laws, is complicated by the presence of the units (the initial and terminal objects of the category) and the fact that in a free setting products and co products do not distribute. The best known desicion algorithm, due to Cockett and Santocanale (CSL 2009), is highly involved, requiring an intricate case analysis on the syntax of terms. This paper provides canonical, graphical representations of the categorical morphisms, yielding a novel solution to this decision problem. Starting with (a modification of) existing proof nets, due to Hughes and Van Glabbeek, for additive linear logic without units, canonical forms are obtained by graph rewriting. The rewriting algorithm is remarkably simple. As a decision procedure for term equality it matches the known complexity of the problem. A main technical contribution of the paper is the substantial correctness proof of the algorithm.
Index Terms:
proof nets, linear logic, graph rewriting
Citation:
Willem Heijltjes, "Proof Nets for Additive Linear Logic with Units," lics, pp.207-216, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, 2011
Usage of this product signifies your acceptance of the Terms of Use.
