Constructing Fully Complete Models of Multiplicative Linear Logic
The multiplicative fragment of Linear Logic is the formal system in this family with the best understood proof theory, and the categorical models which best capture this theory are the fully complete ones. We demonstrate how the Hyland-Tan double glueing construction produces such categories, either...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2015-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1582/pdf |
| _version_ | 1811225329138663424 |
|---|---|
| author | Andrea Schalk Hugh Paul Steele |
| author_facet | Andrea Schalk Hugh Paul Steele |
| author_sort | Andrea Schalk |
| collection | DOAJ |
| description | The multiplicative fragment of Linear Logic is the formal system in this
family with the best understood proof theory, and the categorical models which
best capture this theory are the fully complete ones. We demonstrate how the
Hyland-Tan double glueing construction produces such categories, either with or
without units, when applied to any of a large family of degenerate models. This
process explains as special cases a number of such models from the literature.
In order to achieve this result, we develop a tensor calculus for compact
closed categories with finite biproducts. We show how the combinatorial
properties required for a fully complete model are obtained by this glueing
construction adding to the structure already available from the original
category. |
| first_indexed | 2024-04-12T09:05:14Z |
| format | Article |
| id | doaj.art-bb0b6eea87514d52986a0d0777cc2557 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-12T09:05:14Z |
| publishDate | 2015-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-bb0b6eea87514d52986a0d0777cc25572022-12-22T03:39:07ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742015-09-01Volume 11, Issue 310.2168/LMCS-11(3:6)20151582Constructing Fully Complete Models of Multiplicative Linear LogicAndrea SchalkHugh Paul SteeleThe multiplicative fragment of Linear Logic is the formal system in this family with the best understood proof theory, and the categorical models which best capture this theory are the fully complete ones. We demonstrate how the Hyland-Tan double glueing construction produces such categories, either with or without units, when applied to any of a large family of degenerate models. This process explains as special cases a number of such models from the literature. In order to achieve this result, we develop a tensor calculus for compact closed categories with finite biproducts. We show how the combinatorial properties required for a fully complete model are obtained by this glueing construction adding to the structure already available from the original category.https://lmcs.episciences.org/1582/pdfcomputer science - logic in computer science |
| spellingShingle | Andrea Schalk Hugh Paul Steele Constructing Fully Complete Models of Multiplicative Linear Logic Logical Methods in Computer Science computer science - logic in computer science |
| title | Constructing Fully Complete Models of Multiplicative Linear Logic |
| title_full | Constructing Fully Complete Models of Multiplicative Linear Logic |
| title_fullStr | Constructing Fully Complete Models of Multiplicative Linear Logic |
| title_full_unstemmed | Constructing Fully Complete Models of Multiplicative Linear Logic |
| title_short | Constructing Fully Complete Models of Multiplicative Linear Logic |
| title_sort | constructing fully complete models of multiplicative linear logic |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/1582/pdf |
| work_keys_str_mv | AT andreaschalk constructingfullycompletemodelsofmultiplicativelinearlogic AT hughpaulsteele constructingfullycompletemodelsofmultiplicativelinearlogic |