We give an introduction to logic tailored for algebraists, explaining how proofs in linear logic can be viewed as algorithms for constructing morphisms in symmetric closed monoidal categories with additional structure. This is made explicit by showing how to represent proofs in linear logic as linear maps between vector spaces. The interesting part of this vector space semantics is based on the cofree cocommutative coalgebra of Sweedler.
arXiv comments
v2: the article has been substantially rewritten to improve the exposition, some false statements about cut-elimination were corrected, a new section about second-order linear logic was added, and the material on geometry of interaction has been removed (to be published elsewhere), v3: fixed typos, added references
Linked by 2 identifiable commenters in 2 comments across 2 threads, from Jan 2018 to Jun 2020. Found in 1 HN submission from Nov 2022 to Nov 2022. Open submission discussions.
The reasoning is sort of a technical analogy. Linear Logic was discovered by an analysis of the structure of Coherent Spaces, which are a model of Intuitionistic logic distilled from Scott domains. Jean-Yves Girard realized that function spaces A => B can be decomposed into two…
Author here. The theoretical background can be found in: https://arxiv.org/abs/1407.2650 https://arxiv.org/abs/1701.01285 http://therisingsea.org/notes/MScThesisJamesClift.pdf As neel_k notes, a good way to understand this picture is in terms of differential linear logic (a…
The reasoning is sort of a technical analogy. Linear Logic was discovered by an analysis of the structure of Coherent Spaces, which are a model of Intuitionistic logic distilled from Scott domains. Jean-Yves Girard realized that function spaces A => B can be decomposed into two…
bitdizzyView on HNParent context