Poset-valued sets or how to build models for linear logics (Q1826627): Difference between revisions
From MaRDI portal
Created claim: Wikidata QID (P12): Q56994546, #quickstatements; #temporary_batch_1707252663060 |
ReferenceBot (talk | contribs) Changed an Item |
||
(4 intermediate revisions by 3 users not shown) | |||
Property / author | |||
Property / author: V. C. V. de Paiva / rank | |||
Property / author | |||
Property / author: V. C. V. de Paiva / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.tcs.2003.11.014 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2073721500 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Games and full completeness for multiplicative linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3024825 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3367300 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Localisation and interaction in one dimension / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3994895 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4499228 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Glueing and orthogonality for models of linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4222770 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The Carcinogenic Example / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3829551 / rank | |||
Normal rank |
Latest revision as of 18:37, 6 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Poset-valued sets or how to build models for linear logics |
scientific article |
Statements
Poset-valued sets or how to build models for linear logics (English)
0 references
6 August 2004
0 references
The authors construct yet another model for linear logic that gives precise control over items like: classical vs intuitionistic (properties of negation can be specified); products and coproducts coincide on objects or not, id for their units; tensor and par coincide on objects or not, id for their units. After giving two examples, they define the category \(P_F\)-\textbf{Set} (of \(P_F\) sets), where \(P\) is a poset and \(F\) is an endofunctor on \textbf{Rel} as follows: an object is a map \(FA \rightarrow P\); an arrow \((\alpha: FA \rightarrow P) \rightarrow (\beta: FB \rightarrow P)\) is a relation \(R: A \mapsto B\) such that \(x(FR)y\) implies \(\alpha(x) \leq \beta(y).\) The set \(A\) ``takes values'' (via \(F\)) in \(P\), whence the name. Identities in \(P_F\)-\textbf{Sets} are identity relations and composition is that of relations. Define now a categorical model of intuitionistic linear logic to be a category which: is symmetric monoidal closed; has finite products; is equipped with a linear exponential comonad [\textit{G. M. Berman}, ``What is a categorical model of intuitionistic linear logic?'', Lect. Notes Comput. Sci. 902, 73--93 (1995; Zbl 0813.68040)]. A model for classical linear logic is a category which: is *-autonomous; has finite products and (so) coproducts; is equipped with a linear exponential comonad and (so) a linear exponential monad. Theorem: If \(P\) is *-autonomous and a complete lattice and \(F\) satisfies the conditions of Proposition 3.3, then \(P_F\)-\textbf{Set} is a model for classical linear logic. In addition it has arbitrary products and coproducts. If P is symmetric monoidal closed and a complete lattice and \(F\) satisfies the conditions of Proposition 3.3, then \(P_F\)-\textbf{Set} is a model for intuitionistic linear logic. In addition, it has arbitrary products and coproducts.
0 references
poset-valued sets
0 references
linear logic
0 references
categorical models
0 references