Research

Proof nets for additive linear logic with units


Reference:

Heijltjes, W., 2011. Proof nets for additive linear logic with units. In: 2011 26th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE, pp. 207-216.

Related documents:

[img]
Preview
PDF (Author's accepted version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (188kB) | Preview

    Official URL:

    http://dx.doi.org/10.1109/LICS.2011.9

    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.

    Details

    Item Type Book Sections
    CreatorsHeijltjes, W.
    DOI10.1109/LICS.2011.9
    DepartmentsFaculty of Science > Computer Science
    Publisher StatementSigma_Pi.pdf: © 2011 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
    RefereedNo
    StatusPublished
    ID Code32342
    Additional InformationISSN 1043-6871

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...