Proof nets for additive linear logic with units

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)
167 Downloads (Pure)

Abstract

Additive linear logic, the fragment of linear logic concerning linear implication between strictly additive formu- lae, coincides with sum-product logic, the internal language of categories with free finite products and coproducts. 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 coproducts 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.
Original languageEnglish
Title of host publication2011 26th Annual IEEE Symposium on Logic in Computer Science (LICS)
PublisherIEEE
Pages207-216
ISBN (Electronic)9780769544120
ISBN (Print)9781457704512
DOIs
Publication statusPublished - Jun 2011
Event26th Annual IEEE Symposium on Logic in Computer Science - Toronto, ON, Canada
Duration: 21 Jun 201124 Jun 2011

Conference

Conference26th Annual IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2011
CountryCanada
CityToronto, ON
Period21/06/1124/06/11

Fingerprint Dive into the research topics of 'Proof nets for additive linear logic with units'. Together they form a unique fingerprint.

Cite this