LLWiki - User contributions [en]

Main Page

2012-04-22T02:49:44Z

Pierre-Marie Pédrot: added system L

== Contents ==

* An [[introduction]] to linear logic
* Syntax
** [[Sequent calculus]]
** [[Intuitionistic linear logic]]
** [[Polarized linear logic]]
** [[Fragment|Fragments]]
** [[Proof-nets]]
** [[System L]]
** Translations of [[Translations of classical logic|classical]] and [[Translations of intuitionistic logic|intuitionistic]] logics
* [[Semantics]]
** [[Coherent semantics]]
** [[Phase semantics]]
** [[Categorical semantics]]
** [[Relational semantics]]
** [[Finiteness semantics]]
** [[Geometry of interaction]]
** [[Game semantics]]
* [[Light linear logics]]

== Getting started ==

* Please read the [[recommendations]] before edition in this wiki.
* If you are familiar with these [[recommendations]] (are you?) and only want a reference of available LaTeX macros, see [[LLWiki LaTeX Style]].
* Consult the [http://meta.wikimedia.org/wiki/Help:Contents User's Guide] for information on using the wiki software.
* You can use the [[sandbox]] for tests.
* [[Special:Wantedpages|Wanted pages]].

System L

2012-04-22T02:48:02Z

Pierre-Marie Pédrot: propaganda for system L

'''System L''' is a family of syntax for a variety of variants of linear logic, inspired from classical calculi such as <math>\bar\lambda\mu\tilde\mu</math>-calculus. These, in turn, stem from the study of abstract machines for <math>\lambda</math>-calculus. In this realm, [[Polarized linear logic|polarization]] and [[focalization]] are features that appear naturally. Positives are typically values, and negatives pattern-matches. Contraction and weakening are implicit.

We present here a system for explicitely polarized and focalized linear logic. Polarization classifies terms and types between positive and negative; focalization separates values from non-values.

== Definitions ==

Positive types: <math>P ::= 1 \mid P_1 \otimes P_2 \mid 0 \mid P_1 \oplus P_2 \mid \shpos N \mid \oc N</math>

Negative types: <math>N ::= \bot \mid N_1 \parr N_2 \mid \top \mid N_1 \with N_2 \mid \shneg P \mid \wn P</math>

Positive values: <math>v^+ ::= x^+ \mid () \mid (v_1^+, v_2^+) \mid inl(v^+) \mid inr(v^+) \mid \shpos t^- \mid \mu(\wn x^+).c</math>

Positive terms: <math>t^+ ::= v^+ \mid \mu x^-.c</math>

Negative terms: <math>t^- ::= x^- \mid \mu x^+.c \mid \mu().c \mid \mu(x^+, y^+).c \mid \mu [\cdot] \mid \mu[inl(x^+).c_1 \mid inr(y^+).c_2] \mid \mu(\shpos x^-).c \mid \wn v^+</math>

Commands: <math>c ::= \langle t^+ \mid t^- \rangle</math>

== Typing ==

There are as many typing sequents classes as there are terms classes. Typing of positive values corresponds to focalized sequents, and commands are cuts.

Positive values: sequents are of the form <math>\vdash \Gamma :: v^+ : P</math>.

<math>
\LabelRule{\rulename{ax}^+}
\NulRule{\vdash x^+:P\orth :: x^+: P}
\DisplayProof
</math>

<math>
\LabelRule{1}
\NulRule{\vdash \ :: () : 1}
\DisplayProof
</math>

<math>
\AxRule{\vdash \Gamma_1 :: v_1^+ : P_1}
\AxRule{\vdash \Gamma_2 :: v_2^+ : P_2}
\LabelRule{\rulename{\otimes}}
\BinRule{\vdash\Gamma_1, \Gamma_2 :: (v_1^+, v_2^+) : P_1\otimes P_2}
\DisplayProof
</math>

<math>
\AxRule{\vdash \Gamma :: v^+ : P_1}
\LabelRule{\rulename{\oplus_1}}
\UnaRule{\vdash\Gamma :: inl(v^+) : P_1\oplus P_2}
\DisplayProof
\qquad
\AxRule{\vdash \Gamma :: v^+ : P_2}
\LabelRule{\rulename{\oplus_2}}
\UnaRule{\vdash\Gamma :: inr(v^+) : P_1\oplus P_2}
\DisplayProof
</math>

<math>
\AxRule{\vdash \Gamma \mid t^- : N}
\LabelRule{\shpos}
\UnaRule{\vdash\Gamma :: \shpos t^- : \shpos N}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \wn\Gamma, x^+ : N}
\LabelRule{\oc}
\UnaRule{\vdash\wn\Gamma :: \mu(\wn x^+).c : \oc N}
\DisplayProof
</math>

Positive terms: sequents are of the form <math>\vdash\Gamma\mid t^+:P</math>.

<math>
\AxRule{\vdash \Gamma :: v^+ : P}
\LabelRule{\rulename{foc}}
\UnaRule{\vdash\Gamma \mid v^+ : P}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \Gamma, x^- : P}
\LabelRule{\rulename{\mu^-}}
\UnaRule{\vdash\Gamma \mid\mu x^-.c : P}
\DisplayProof
</math>

Negative terms: sequents are of the form <math>\vdash\Gamma\mid t^-:N</math>.

<math>
\LabelRule{\rulename{ax}^-}
\NulRule{\vdash x^-:N\orth \mid x^-: N}
\DisplayProof
</math>

<math>
\AxRule{c\vdash \Gamma, x^+: N}
\LabelRule{\mu^+}
\UnaRule{\vdash\Gamma \mid \mu x^+.c : N}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \Gamma}
\LabelRule{\bot}
\UnaRule{\vdash \Gamma \mid \mu().c : \bot}
\DisplayProof
</math>

<math>
\AxRule{c\vdash \Gamma, x^+: N_1, y^+: N_2}
\LabelRule{\rulename{\parr}}
\UnaRule{\vdash\Gamma \mid \mu(x^+, y^+).c : N_1 \parr N_2}
\DisplayProof
</math>

<math>
\LabelRule{\rulename{\top}}
\NulRule{\vdash \Gamma \mid \mu[\cdot] : \top}
\DisplayProof
</math>

<math>
\AxRule{c_1\vdash \Gamma, x^+:N_1}
\AxRule{c_2\vdash \Gamma, y^+:N_2}
\LabelRule{\rulename{\with}}
\BinRule{\vdash\Gamma \mid \mu[inl(x^+).c_1 \mid inr(y^+).c_2] : N_1 \with N_2}
\DisplayProof
</math>

<math>
\AxRule{c\vdash \Gamma, x^-: P}
\LabelRule{\shneg}
\UnaRule{\vdash\Gamma \mid \mu(\shpos x^-).c : \shneg P}
\DisplayProof
</math>

<math>
\AxRule{\vdash \Gamma :: v^+ : P}
\LabelRule{\wn}
\UnaRule{\vdash\Gamma \mid \wn v^+ : \wn P}
\DisplayProof
</math>

Commands:

<math>
\AxRule{\vdash \Gamma \mid t^+ : P}
\AxRule{\vdash \Delta \mid t^- : P\orth}
\LabelRule{\rulename{cut}}
\BinRule{\langle t^+ \mid t^-\rangle\vdash\Gamma, \Delta}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \Gamma}
\LabelRule{\rulename{wkn}}
\UnaRule{c \vdash\Gamma, x^+: \wn P}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \Gamma, x_1^+:\wn P, x_2^+:\wn P}
\LabelRule{\rulename{ctr}}
\UnaRule{c[x_1^+ := x^+, x_2^+ := x^+] \vdash\Gamma, x^+: \wn P}
\DisplayProof
</math>

== Reduction rules ==

<math>\langle v^+ \mid \mu x^+.c \rangle \rightarrow c[ x^+ := v^+] </math>

<math>\langle \mu x^-.c \mid t^- \rangle \rightarrow c[x^- := t^-] </math>

<math>\langle () \mid \mu().c \rangle \rightarrow c </math>

<math>\langle (v_1^+, v_2^+) \mid \mu(x^+, y^+).c \rangle \rightarrow c[x^+ := v_1^+, y^+ := v_2^+] </math>

<math>\langle inl(v^+) \mid \mu[inl(x^+).c_1 \mid inr(y^+).c_2] \rangle \rightarrow c_1[x^+ := v^+] </math>

<math>\langle inr(v^+) \mid \mu[inl(x^+).c_1 \mid inr(y^+).c_2] \rangle \rightarrow c_2[y^+ := v^+] </math>

<math>\langle \shpos t^- \mid \mu(\shpos x^-).c \rangle \rightarrow c[x^- := t^-] </math>

<math>\langle \mu(\wn x^+).c \mid \wn v^+ \rangle \rightarrow c[x^+ := v^+] </math>

== References ==

* {{BibEntry|bibtype=proceedings|author=Pierre-Louis Curien and Guillaume Munch-Maccagnoni|title=The duality of computation under focus|booktitle=IFIP TCS|year=2010}}

Phase semantics

2011-10-22T14:05:45Z

Pierre-Marie Pédrot: /* Completeness */ typo

==Introduction==

The semantics given by phase spaces is a kind of "formula and provability semantics", and is thus quite different in spirit from the more usual denotational semantics of linear logic. (Those are rather some "formulas and ''proofs'' semantics".)

--- probably a whole lot more of blabla to put here... ---

==Preliminaries: relation and closure operators==

Part of the structure obtained from phase semantics works in a very general framework and relies solely on the notion of relation between two sets.

===Relations and operators on subsets===

The starting point of phase semantics is the notion of ''duality''. The structure needed to talk about duality is very simple: one just needs a relation <math>R</math> between two sets <math>X</math> and <math>Y</math>. Using standard mathematical practice, we can write either <math>(a,b) \in R</math> or <math>a\mathrel{R} b</math> to say that <math>a\in X</math> and <math>b\in Y</math> are related.

{{Definition|
If <math>R\subseteq X\times Y</math> is a relation, we write <math>R^\sim\subseteq Y\times X</math> for the converse relation: <math>(b,a)\in R^\sim</math> iff <math>(a,b)\in R</math>.
}}

Such a relation yields three interesting operators sending subsets of <math>X</math> to subsets of <math>Y</math>:

{{Definition|
Let <math>R\subseteq X\times Y</math> be a relation, define the operators <math>\langle R\rangle</math>, <math>[R]</math> and <math>\_^R</math> taking subsets of <math>X</math> to subsets of <math>Y</math> as follows:
# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in x,\ (a,b)\in R</math>
# <math>b\in[R](x)</math> iff <math>\forall a\in X,\ (a,b)\in R \implies a\in x</math>
# <math>b\in x^R</math> iff <math>\forall a\in x, (a,b)\in R</math>
}}

The operator <math>\langle R\rangle</math> is usually called the ''direct image'' of the relation, <math>[R]</math> is sometimes called the ''universal image'' of the relation.

It is trivial to check that <math>\langle R\rangle</math> and <math>[R]</math> are covariant (increasing for the <math>\subseteq</math> relation) while <math>\_^R</math> is contravariant (decreasing for the <math>\subseteq</math> relation). More interesting:

{{Lemma|title=Galois Connections|
# <math>\langle R\rangle</math> is right-adjoint to <math>[R^\sim]</math>: for any <math>x\subseteq X</math> and <math>y\subseteq Y</math>, we have <math>[R^\sim]y \subseteq x</math> iff <math>y\subseteq \langle R\rangle(x)</math>
# we have <math>y\subseteq x^R</math> iff <math>x\subseteq y^{R^\sim}</math>
}}

This implies directly that <math>\langle R\rangle</math> commutes with arbitrary unions and <math>[R]</math> commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form <math>\langle R\rangle</math> (resp. <math>[R]</math>).

{{Remark|the operator <math>\_^R</math> sends unions to intersections because <math>\_^R : \mathcal{P}(X) \to \mathcal{P}(Y)^\mathrm{op}</math> is right adjoint to <math>\_^{R^\sim} : \mathcal{P}(Y)^{\mathrm{op}} \to \mathcal{P}(X)</math>...}}

===Closure operators===

{{Definition|
A closure operator on <math>\mathcal{P}(X)</math> is a monotonic operator <math>P</math> on the subsets of <math>X</math> which satisfies:
# for all <math>x\subseteq X</math>, we have <math>x\subseteq P(x)</math>
# for all <math>x\subseteq X</math>, we have <math>P(P(x))\subseteq P(x)</math>
}}

Closure operators are quite common in mathematics and computer science. They correspond exactly to the notion of ''monad'' on a preorder...

It follows directly from the definition that for any closure operator <math>P</math>, the image <math>P(x)</math> is a fixed point of <math>P</math>. Moreover:

{{Lemma|
<math>P(x)</math> is the smallest fixed point of <math>P</math> containing <math>x</math>.
}}

One other important property is the following:

{{Lemma|
Write <math>\mathcal{F}(P) = \{x\ |\ P(x)\subseteq x\}</math> for the collection of fixed points of a closure operator <math>P</math>. We have that <math>\left(\mathcal{F}(P),\bigcap\right)</math> is a complete inf-lattice.
}}

{{Remark|
A closure operator is in fact determined by its set of fixed points: we have <math>P(x) = \bigcup \{ y\ |\ y\in\mathcal{F}(P),\,y\subseteq x\}</math>}}

Since any complete inf-lattice is automatically a complete sup-lattice, <math>\mathcal{F}(P)</math> is also a complete sup-lattice. However, the sup operation isn't given by plain union:

{{Lemma|
If <math>P</math> is a closure operator on <math>\mathcal{P}(X)</math>, and if <math>(x_i)_{i\in I}</math> is a (possibly infinite) family of subsets of <math>X</math>, we write <math>\bigvee_{i\in I} x_i = P\left(\bigcup_{i\in I} x_i\right)</math>.

We have <math>\left(\mathcal{F}(P),\bigcap,\bigvee\right)</math> is a complete lattice.
}}

{{Proof|
easy.
}}

A rather direct consequence of the Galois connections of the previous section is:

{{Lemma|
The operator and <math>\langle R\rangle \circ [R^\sim]</math> and the operator <math>x\mapsto {x^R}^{R^\sim}</math> are closures.
}}

A last trivial lemma:

{{Lemma|
We have <math>x^R = {{x^R}^{R^\sim}}^{R}</math>.

As a consequence, a subset <math>x\subseteq X</math> is in <math>\mathcal{F}({\_^R}^{R^\sim})</math> iff it is of the form <math>y^{R^\sim}</math>.
}}

{{Remark|everything gets a little simpler when <math>R</math> is a symmetric relation on <math>X</math>.}}

==Phase Semantics==

===Phase spaces===

{{Definition|title=monoid|
A monoid is simply a set <math>X</math> equipped with a binary operation <math>\_\cdot\_</math> s.t.:
# the operation is associative
# there is a neutral element <math>1\in X</math>
The monoid is ''commutative'' when the binary operation is commutative.
}}

{{Definition|title=Phase space|
A phase space is given by:
# a commutative monoid <math>(X,1,\cdot)</math>,
# together with a subset <math>\Bot\subseteq X</math>.
The elements of <math>X</math> are called ''phases''.

We write <math>\bot</math> for the relation <math>\{(a,b)\ |\ a\cdot b \in \Bot\}</math>. This relation is symmetric.

A ''fact'' in a phase space is simply a fixed point for the closure operator <math>x\mapsto x\biorth</math>.
}}

Thanks to the preliminary work, we have:

{{Corollary|
The set of facts of a phase space is a complete lattice where:
# <math>\bigwedge_{i\in I} x_i</math> is simply <math>\bigcap_{i\in I} x_i</math>,
# <math>\bigvee_{i\in I} x_i</math> is <math>\left(\bigcup_{i\in I} x_i\right)\biorth</math>.
}}

===Additive connectives===

The previous corollary makes the following definition correct:

{{Definition|title=additive connectives|
If <math>(X,1,\cdot,\Bot)</math> is a phase space, we define the following facts and operations on facts:
# <math>\top = X = \emptyset\orth</math>
# <math>\zero = \emptyset\biorth = X\orth</math>
# <math>x\with y = x\cap y</math>
# <math>x\plus y = (x\cup y)\biorth</math>
}}

Once again, the next lemma follows from previous observations:

{{Lemma|title=additive de Morgan laws|
We have
# <math>\zero\orth = \top</math>
# <math>\top\orth = \zero</math>
# <math>(x\with y)\orth = x\orth \plus y\orth</math>
# <math>(x\plus y)\orth = x\orth \with y\orth</math>
}}

===Multiplicative connectives===

In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space. One interpretation that is reminiscent in phase semantics is that our spaces are collections of ''tests'' / programs / proofs / ''strategies'' that can interact with each other. The result of the interaction between <math>a</math> and <math>b</math> is simply <math>a\cdot b</math>.

The set <math>\Bot</math> can be thought of as the set of "good" things, and we thus have <math>a\in x\orth</math> iff "<math>a</math> interacts correctly with all the elements of <math>x</math>".

{{Definition|
If <math>x</math> and <math>y</math> are two subsets of a phase space, we write <math>x\cdot y</math> for the set <math>\{a\cdot b\ |\ a\in x, b\in y\}</math>.
}}
Thus <math>x\cdot y</math> contains all the possible interactions between one element of <math>x</math> and one element of <math>y</math>.

The tensor connective of linear logic is now defined as:

{{Definition| title=multiplicative connectives|
If <math>x</math> and <math>y</math> are facts in a phase space, we define
* <math>\one = \{1\}\biorth</math>;
* <math>\bot = \one\orth</math>;
* the tensor <math>x\tens y</math> to be the fact <math>(x\cdot y)\biorth</math>;
* the par connective is the de Morgan dual of the tensor: <math>x\parr y = (x\orth \tens y\orth)\orth</math>;
* the linear arrow is just <math>x\limp y = x\orth\parr y = (x\tens y\orth)\orth</math>.
}}

Note that by unfolding the definition of <math>\limp</math>, we have the following, "intuitive" definition of <math>x\limp y</math>:

{{Lemma|
If <math>x</math> and <math>y</math> are facts, we have <math>a\in x\limp y</math> iff <math>\forall b\in x,\,a\cdot b\in y</math>
}}

{{Proof|
easy exercise. }}

Readers familiar with realisability will appreciate...

{{Remark|
Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}}

===Properties===

All the expected properties hold:

{{Lemma|
* The operations <math>\tens</math>, <math>\parr</math>, <math>\plus</math> and <math>\with</math> are commutative and associative,
* They have respectively <math>\one</math>, <math>\bot</math>, <math>\zero</math> and <math>\top</math> for neutral element,
* <math>\zero</math> is absorbant for <math>\tens</math>,
* <math>\top</math> is absorbant for <math>\parr</math>,
* <math>\tens</math> distributes over <math>\plus</math>,
* <math>\parr</math> distributes over <math>\with</math>.
}}

===Exponentials===

{{Definition|title=Exponentials|
Write <math>I</math> for the set of idempotents of a phase space: <math>I=\{a\ |\ a\cdot a=a\}</math>. We put:
# <math>\oc x = (x\cap I\cap \one)\biorth</math>,
# <math>\wn x = (x\orth\cap I\cap\one)\orth</math>.
}}

This definition captures precisely the intuition behind the exponentials:
* we need to have contraction, hence we restrict to indempotents in <math>x</math>,
* and weakening, hence we restrict to <math>\one</math>.
Since <math>I</math> isn't necessarily a fact, we then take the biorthogonal to get a fact...

== Soundness ==

{{Definition|Let <math>(X, 1, \cdot)</math> be a commutative monoid.

Given a formula <math>A</math> of linear logic and an assignation <math>\rho</math> that associate a fact to any variable, we can inductively define the interpretation <math>\sem{A}_\rho</math> of <math>A</math> in <math>X</math> as one would expect. Interpretation is lifted to sequents as <math>\sem{A_1, \dots, A_n}_\rho = \sem{A_1}_\rho \parr \cdots \parr \sem{A_n}_\rho</math>.}}

{{Theorem|Let <math>\Gamma</math> be a provable sequent in linear logic. Then <math>1_X \in \sem{\Gamma}</math>.}}

{{Proof|By induction on <math>\vdash\Gamma</math>.}}

== Completeness ==

Phase semantics is complete w.r.t. linear logic. In order to prove this, we need to build a particular commutative monoid.

{{Definition|We define the '''syntactic monoid''' as follows:

* Its elements are sequents <math>\Gamma</math> quotiented by the equivalence relation <math>\cong</math> generated by the rules:
*# <math>\Gamma \cong \Delta</math> if <math>\Gamma</math> is a permutation of <math>\Delta</math>
*# <math>\wn{A}, \wn{A}, \Gamma \cong \wn{A}, \Gamma</math>

* Product is concatenation: <math>\Gamma \cdot \Delta := \Gamma, \Delta</math>

* Neutral element is the empty sequent: <math>1 := \emptyset</math>.}}

The equivalence relation intuitively means that we do not care about the multiplicity of <math>\wn</math>-formulae.

{{Lemma|The syntactic monoid is indeed a commutative monoid.}}

{{Definition|The '''syntactic assignation''' is the assignation that sends any variable <math>\alpha</math> to the fact <math>\{\alpha\}\orth</math>.}}

We instantiate the pole as <math>\Bot := \{\Gamma \mid \vdash\Gamma\}</math>.

{{Theorem|If <math>\Gamma\in\sem{\Gamma}\orth</math>, then <math>\vdash\Gamma</math>.}}

{{Proof|By induction on <math>\Gamma</math>.}}

== Cut elimination ==

Actually, the completeness result is stronger, as the proof does not use the cut-rule in the reconstruction of <math>\vdash\Gamma</math>. By refining the pole as the set of ''cut-free'' provable formulae, we get:

{{Theorem|If <math>\Gamma\in\sem{\Gamma}\orth</math>, then <math>\Gamma</math> is cut-free provable.}}

From soundness, one can retrieve the cut-elimination theorem.

{{Corollary|Linear logic enjoys the cut-elimination property.}}

==The Rest==

Phase semantics

2011-10-21T15:06:19Z

Pierre-Marie Pédrot:

==Introduction==

The semantics given by phase spaces is a kind of "formula and provability semantics", and is thus quite different in spirit from the more usual denotational semantics of linear logic. (Those are rather some "formulas and ''proofs'' semantics".)

--- probably a whole lot more of blabla to put here... ---

==Preliminaries: relation and closure operators==

Part of the structure obtained from phase semantics works in a very general framework and relies solely on the notion of relation between two sets.

===Relations and operators on subsets===

The starting point of phase semantics is the notion of ''duality''. The structure needed to talk about duality is very simple: one just needs a relation <math>R</math> between two sets <math>X</math> and <math>Y</math>. Using standard mathematical practice, we can write either <math>(a,b) \in R</math> or <math>a\mathrel{R} b</math> to say that <math>a\in X</math> and <math>b\in Y</math> are related.

{{Definition|
If <math>R\subseteq X\times Y</math> is a relation, we write <math>R^\sim\subseteq Y\times X</math> for the converse relation: <math>(b,a)\in R^\sim</math> iff <math>(a,b)\in R</math>.
}}

Such a relation yields three interesting operators sending subsets of <math>X</math> to subsets of <math>Y</math>:

{{Definition|
Let <math>R\subseteq X\times Y</math> be a relation, define the operators <math>\langle R\rangle</math>, <math>[R]</math> and <math>\_^R</math> taking subsets of <math>X</math> to subsets of <math>Y</math> as follows:
# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in x,\ (a,b)\in R</math>
# <math>b\in[R](x)</math> iff <math>\forall a\in X,\ (a,b)\in R \implies a\in x</math>
# <math>b\in x^R</math> iff <math>\forall a\in x, (a,b)\in R</math>
}}

The operator <math>\langle R\rangle</math> is usually called the ''direct image'' of the relation, <math>[R]</math> is sometimes called the ''universal image'' of the relation.

It is trivial to check that <math>\langle R\rangle</math> and <math>[R]</math> are covariant (increasing for the <math>\subseteq</math> relation) while <math>\_^R</math> is contravariant (decreasing for the <math>\subseteq</math> relation). More interesting:

{{Lemma|title=Galois Connections|
# <math>\langle R\rangle</math> is right-adjoint to <math>[R^\sim]</math>: for any <math>x\subseteq X</math> and <math>y\subseteq Y</math>, we have <math>[R^\sim]y \subseteq x</math> iff <math>y\subseteq \langle R\rangle(x)</math>
# we have <math>y\subseteq x^R</math> iff <math>x\subseteq y^{R^\sim}</math>
}}

This implies directly that <math>\langle R\rangle</math> commutes with arbitrary unions and <math>[R]</math> commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form <math>\langle R\rangle</math> (resp. <math>[R]</math>).

{{Remark|the operator <math>\_^R</math> sends unions to intersections because <math>\_^R : \mathcal{P}(X) \to \mathcal{P}(Y)^\mathrm{op}</math> is right adjoint to <math>\_^{R^\sim} : \mathcal{P}(Y)^{\mathrm{op}} \to \mathcal{P}(X)</math>...}}

===Closure operators===

{{Definition|
A closure operator on <math>\mathcal{P}(X)</math> is a monotonic operator <math>P</math> on the subsets of <math>X</math> which satisfies:
# for all <math>x\subseteq X</math>, we have <math>x\subseteq P(x)</math>
# for all <math>x\subseteq X</math>, we have <math>P(P(x))\subseteq P(x)</math>
}}

Closure operators are quite common in mathematics and computer science. They correspond exactly to the notion of ''monad'' on a preorder...

It follows directly from the definition that for any closure operator <math>P</math>, the image <math>P(x)</math> is a fixed point of <math>P</math>. Moreover:

{{Lemma|
<math>P(x)</math> is the smallest fixed point of <math>P</math> containing <math>x</math>.
}}

One other important property is the following:

{{Lemma|
Write <math>\mathcal{F}(P) = \{x\ |\ P(x)\subseteq x\}</math> for the collection of fixed points of a closure operator <math>P</math>. We have that <math>\left(\mathcal{F}(P),\bigcap\right)</math> is a complete inf-lattice.
}}

{{Remark|
A closure operator is in fact determined by its set of fixed points: we have <math>P(x) = \bigcup \{ y\ |\ y\in\mathcal{F}(P),\,y\subseteq x\}</math>}}

Since any complete inf-lattice is automatically a complete sup-lattice, <math>\mathcal{F}(P)</math> is also a complete sup-lattice. However, the sup operation isn't given by plain union:

{{Lemma|
If <math>P</math> is a closure operator on <math>\mathcal{P}(X)</math>, and if <math>(x_i)_{i\in I}</math> is a (possibly infinite) family of subsets of <math>X</math>, we write <math>\bigvee_{i\in I} x_i = P\left(\bigcup_{i\in I} x_i\right)</math>.

We have <math>\left(\mathcal{F}(P),\bigcap,\bigvee\right)</math> is a complete lattice.
}}

{{Proof|
easy.
}}

A rather direct consequence of the Galois connections of the previous section is:

{{Lemma|
The operator and <math>\langle R\rangle \circ [R^\sim]</math> and the operator <math>x\mapsto {x^R}^{R^\sim}</math> are closures.
}}

A last trivial lemma:

{{Lemma|
We have <math>x^R = {{x^R}^{R^\sim}}^{R}</math>.

As a consequence, a subset <math>x\subseteq X</math> is in <math>\mathcal{F}({\_^R}^{R^\sim})</math> iff it is of the form <math>y^{R^\sim}</math>.
}}

{{Remark|everything gets a little simpler when <math>R</math> is a symmetric relation on <math>X</math>.}}

==Phase Semantics==

===Phase spaces===

{{Definition|title=monoid|
A monoid is simply a set <math>X</math> equipped with a binary operation <math>\_\cdot\_</math> s.t.:
# the operation is associative
# there is a neutral element <math>1\in X</math>
The monoid is ''commutative'' when the binary operation is commutative.
}}

{{Definition|title=Phase space|
A phase space is given by:
# a commutative monoid <math>(X,1,\cdot)</math>,
# together with a subset <math>\Bot\subseteq X</math>.
The elements of <math>X</math> are called ''phases''.

We write <math>\bot</math> for the relation <math>\{(a,b)\ |\ a\cdot b \in \Bot\}</math>. This relation is symmetric.

A ''fact'' in a phase space is simply a fixed point for the closure operator <math>x\mapsto x\biorth</math>.
}}

Thanks to the preliminary work, we have:

{{Corollary|
The set of facts of a phase space is a complete lattice where:
# <math>\bigwedge_{i\in I} x_i</math> is simply <math>\bigcap_{i\in I} x_i</math>,
# <math>\bigvee_{i\in I} x_i</math> is <math>\left(\bigcup_{i\in I} x_i\right)\biorth</math>.
}}

===Additive connectives===

The previous corollary makes the following definition correct:

{{Definition|title=additive connectives|
If <math>(X,1,\cdot,\Bot)</math> is a phase space, we define the following facts and operations on facts:
# <math>\top = X = \emptyset\orth</math>
# <math>\zero = \emptyset\biorth = X\orth</math>
# <math>x\with y = x\cap y</math>
# <math>x\plus y = (x\cup y)\biorth</math>
}}

Once again, the next lemma follows from previous observations:

{{Lemma|title=additive de Morgan laws|
We have
# <math>\zero\orth = \top</math>
# <math>\top\orth = \zero</math>
# <math>(x\with y)\orth = x\orth \plus y\orth</math>
# <math>(x\plus y)\orth = x\orth \with y\orth</math>
}}

===Multiplicative connectives===

In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space. One interpretation that is reminiscent in phase semantics is that our spaces are collections of ''tests'' / programs / proofs / ''strategies'' that can interact with each other. The result of the interaction between <math>a</math> and <math>b</math> is simply <math>a\cdot b</math>.

The set <math>\Bot</math> can be thought of as the set of "good" things, and we thus have <math>a\in x\orth</math> iff "<math>a</math> interacts correctly with all the elements of <math>x</math>".

{{Definition|
If <math>x</math> and <math>y</math> are two subsets of a phase space, we write <math>x\cdot y</math> for the set <math>\{a\cdot b\ |\ a\in x, b\in y\}</math>.
}}
Thus <math>x\cdot y</math> contains all the possible interactions between one element of <math>x</math> and one element of <math>y</math>.

The tensor connective of linear logic is now defined as:

{{Definition| title=multiplicative connectives|
If <math>x</math> and <math>y</math> are facts in a phase space, we define
* <math>\one = \{1\}\biorth</math>;
* <math>\bot = \one\orth</math>;
* the tensor <math>x\tens y</math> to be the fact <math>(x\cdot y)\biorth</math>;
* the par connective is the de Morgan dual of the tensor: <math>x\parr y = (x\orth \tens y\orth)\orth</math>;
* the linear arrow is just <math>x\limp y = x\orth\parr y = (x\tens y\orth)\orth</math>.
}}

Note that by unfolding the definition of <math>\limp</math>, we have the following, "intuitive" definition of <math>x\limp y</math>:

{{Lemma|
If <math>x</math> and <math>y</math> are facts, we have <math>a\in x\limp y</math> iff <math>\forall b\in x,\,a\cdot b\in y</math>
}}

{{Proof|
easy exercise. }}

Readers familiar with realisability will appreciate...

{{Remark|
Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}}

===Properties===

All the expected properties hold:

{{Lemma|
* The operations <math>\tens</math>, <math>\parr</math>, <math>\plus</math> and <math>\with</math> are commutative and associative,
* They have respectively <math>\one</math>, <math>\bot</math>, <math>\zero</math> and <math>\top</math> for neutral element,
* <math>\zero</math> is absorbant for <math>\tens</math>,
* <math>\top</math> is absorbant for <math>\parr</math>,
* <math>\tens</math> distributes over <math>\plus</math>,
* <math>\parr</math> distributes over <math>\with</math>.
}}

===Exponentials===

{{Definition|title=Exponentials|
Write <math>I</math> for the set of idempotents of a phase space: <math>I=\{a\ |\ a\cdot a=a\}</math>. We put:
# <math>\oc x = (x\cap I\cap \one)\biorth</math>,
# <math>\wn x = (x\orth\cap I\cap\one)\orth</math>.
}}

This definition captures precisely the intuition behind the exponentials:
* we need to have contraction, hence we restrict to indempotents in <math>x</math>,
* and weakening, hence we restrict to <math>\one</math>.
Since <math>I</math> isn't necessarily a fact, we then take the biorthogonal to get a fact...

== Soundness ==

{{Definition|Let <math>(X, 1, \cdot)</math> be a commutative monoid.

Given a formula <math>A</math> of linear logic and an assignation <math>\rho</math> that associate a fact to any variable, we can inductively define the interpretation <math>\sem{A}_\rho</math> of <math>A</math> in <math>X</math> as one would expect. Interpretation is lifted to sequents as <math>\sem{A_1, \hdots, A_n}_\rho = \sem{A_1}_\rho \parr \hdots \parr \sem{A_n}_\rho</math>.}}

{{Theorem|Let <math>\Gamma</math> be a provable sequent in linear logic. Then <math>1_X \in \sem{\Gamma}.}}

{{Proof|By induction on <math>\vdash\Gamma</math>.}}

== Completeness ==

Phase semantics is complete w.r.t. linear logic. In order to prove this, we need to build a particular commutative monoid.

{{Definition|We define the '''syntactic monoid''' as follows:

* Its elements are sequents <math>\Gamma</math> quotiented by the equivalence relation <math>\cong</math> generated by the rules:
*# <math>\Gamma \cong \Delta</math> if <math>\Gamma</math> is a permutation of <math>\Delta</math>
*# <math>\wn{A}, \wn{A}, \Gamma \cong \wn{A}, \Gamma</math>

* Product is concatenation: <math>\Gamma \cdot \Delta := \Gamma, \Delta</math>

* Neutral element is the empty sequent: <math>1 := \emptyset</math>.}}

The equivalence relation intuitively means that we do not care about the multiplicity of <math>\wn</math>-formulae.

{{Lemma|The syntactic monoid is indeed a commutative monoid.}}

{{Definition|The '''syntactic assignation''' is the assignation that sends any variable <math>\alpha</math> to the fact <math>\{\alpha\}\orth</math>.}}

We instantiate the pole as <math>\Bot</math><math> := \{\Gamma \mid \vdash\Gamma\}</math>.

{{Theorem|If <math>\Gamma\in\sem{\Gamma}\orth</math>, then <math>\vdash\Gamma</math>.}}

{{Proof|By induction on <math>\Gamma</math>.}}

== Cut elimination ==

Actually, the completeness result is stronger, as the proof does not use the cut-rule in the reconstruction of <math>\vdash\Gamma</math>. By refining the pole as the set of ''cut-free'' provable formulae, we get:

{{Theorem|If <math>\Gamma\in\sem{\Gamma}\orth</math>, then <math>\Gamma</math> is cut-free provable.}}

From soundness, one can retrieve the cut-elimination theorem.

{{Corollary|Linear logic enjoys the cut-elimination property.}}

==The Rest==

Talk:Phase semantics

2011-10-21T15:02:41Z

Pierre-Marie Pédrot: /* LaTeX parsing */ new section

== Preliminaries: relations and closures ==

===References===

I think everything I write in the preliminaries can be found in Birkhoff, "Lattice theory". Can anyone check? (I don't think I have easy access to a copy.

In particular, I think <math>x^R</math> was written <math>x^{\leftarrow}</math>, with the relation <math>R</math> being implicit.

If so, we should add a reference to that.

-- [[User:Pierre Hyvernat|Pierre Hyvernat]] 11:22, 8 February 2009 (UTC)

===Notation===

The refinement calculus people use the relation in the reverse order: what I write <math>\langle R\rangle</math>, they write <math>\langle R^\sim\rangle</math>. (The same is true of <math>[R]</math>.) I find it confusing, and since this is hardly "standard" notation one way or the other, I don't think this is important...

-- [[User:Pierre Hyvernat|Pierre Hyvernat]] 11:27, 8 February 2009 (UTC)

== Phase semantics ==

===Realisability===

I put the remark

:{{Remark|
:Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}}

at the end of the subsection "multiplicative connectives".

Has anybody heard the same about Tait proof and biorthogonal?

-- [[User:Pierre Hyvernat|Pierre Hyvernat]] 21:13, 8 February 2009 (UTC)

== LaTeX parsing ==

LaTeX is doing strange things and refuses to parse correct sentences. Any clues, someone? [[User:Pierre-Marie Pédrot|Pierre-Marie Pédrot]] 15:02, 21 October 2011 (UTC)

Phase semantics

2011-10-21T14:52:12Z

Pierre-Marie Pédrot: + soundness & completeness

==Introduction==

The semantics given by phase spaces is a kind of "formula and provability semantics", and is thus quite different in spirit from the more usual denotational semantics of linear logic. (Those are rather some "formulas and ''proofs'' semantics".)

--- probably a whole lot more of blabla to put here... ---

==Preliminaries: relation and closure operators==

Part of the structure obtained from phase semantics works in a very general framework and relies solely on the notion of relation between two sets.

===Relations and operators on subsets===

The starting point of phase semantics is the notion of ''duality''. The structure needed to talk about duality is very simple: one just needs a relation <math>R</math> between two sets <math>X</math> and <math>Y</math>. Using standard mathematical practice, we can write either <math>(a,b) \in R</math> or <math>a\mathrel{R} b</math> to say that <math>a\in X</math> and <math>b\in Y</math> are related.

{{Definition|
If <math>R\subseteq X\times Y</math> is a relation, we write <math>R^\sim\subseteq Y\times X</math> for the converse relation: <math>(b,a)\in R^\sim</math> iff <math>(a,b)\in R</math>.
}}

Such a relation yields three interesting operators sending subsets of <math>X</math> to subsets of <math>Y</math>:

{{Definition|
Let <math>R\subseteq X\times Y</math> be a relation, define the operators <math>\langle R\rangle</math>, <math>[R]</math> and <math>\_^R</math> taking subsets of <math>X</math> to subsets of <math>Y</math> as follows:
# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in x,\ (a,b)\in R</math>
# <math>b\in[R](x)</math> iff <math>\forall a\in X,\ (a,b)\in R \implies a\in x</math>
# <math>b\in x^R</math> iff <math>\forall a\in x, (a,b)\in R</math>
}}

The operator <math>\langle R\rangle</math> is usually called the ''direct image'' of the relation, <math>[R]</math> is sometimes called the ''universal image'' of the relation.

It is trivial to check that <math>\langle R\rangle</math> and <math>[R]</math> are covariant (increasing for the <math>\subseteq</math> relation) while <math>\_^R</math> is contravariant (decreasing for the <math>\subseteq</math> relation). More interesting:

{{Lemma|title=Galois Connections|
# <math>\langle R\rangle</math> is right-adjoint to <math>[R^\sim]</math>: for any <math>x\subseteq X</math> and <math>y\subseteq Y</math>, we have <math>[R^\sim]y \subseteq x</math> iff <math>y\subseteq \langle R\rangle(x)</math>
# we have <math>y\subseteq x^R</math> iff <math>x\subseteq y^{R^\sim}</math>
}}

This implies directly that <math>\langle R\rangle</math> commutes with arbitrary unions and <math>[R]</math> commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form <math>\langle R\rangle</math> (resp. <math>[R]</math>).

{{Remark|the operator <math>\_^R</math> sends unions to intersections because <math>\_^R : \mathcal{P}(X) \to \mathcal{P}(Y)^\mathrm{op}</math> is right adjoint to <math>\_^{R^\sim} : \mathcal{P}(Y)^{\mathrm{op}} \to \mathcal{P}(X)</math>...}}

===Closure operators===

{{Definition|
A closure operator on <math>\mathcal{P}(X)</math> is a monotonic operator <math>P</math> on the subsets of <math>X</math> which satisfies:
# for all <math>x\subseteq X</math>, we have <math>x\subseteq P(x)</math>
# for all <math>x\subseteq X</math>, we have <math>P(P(x))\subseteq P(x)</math>
}}

Closure operators are quite common in mathematics and computer science. They correspond exactly to the notion of ''monad'' on a preorder...

It follows directly from the definition that for any closure operator <math>P</math>, the image <math>P(x)</math> is a fixed point of <math>P</math>. Moreover:

{{Lemma|
<math>P(x)</math> is the smallest fixed point of <math>P</math> containing <math>x</math>.
}}

One other important property is the following:

{{Lemma|
Write <math>\mathcal{F}(P) = \{x\ |\ P(x)\subseteq x\}</math> for the collection of fixed points of a closure operator <math>P</math>. We have that <math>\left(\mathcal{F}(P),\bigcap\right)</math> is a complete inf-lattice.
}}

{{Remark|
A closure operator is in fact determined by its set of fixed points: we have <math>P(x) = \bigcup \{ y\ |\ y\in\mathcal{F}(P),\,y\subseteq x\}</math>}}

Since any complete inf-lattice is automatically a complete sup-lattice, <math>\mathcal{F}(P)</math> is also a complete sup-lattice. However, the sup operation isn't given by plain union:

{{Lemma|
If <math>P</math> is a closure operator on <math>\mathcal{P}(X)</math>, and if <math>(x_i)_{i\in I}</math> is a (possibly infinite) family of subsets of <math>X</math>, we write <math>\bigvee_{i\in I} x_i = P\left(\bigcup_{i\in I} x_i\right)</math>.

We have <math>\left(\mathcal{F}(P),\bigcap,\bigvee\right)</math> is a complete lattice.
}}

{{Proof|
easy.
}}

A rather direct consequence of the Galois connections of the previous section is:

{{Lemma|
The operator and <math>\langle R\rangle \circ [R^\sim]</math> and the operator <math>x\mapsto {x^R}^{R^\sim}</math> are closures.
}}

A last trivial lemma:

{{Lemma|
We have <math>x^R = {{x^R}^{R^\sim}}^{R}</math>.

As a consequence, a subset <math>x\subseteq X</math> is in <math>\mathcal{F}({\_^R}^{R^\sim})</math> iff it is of the form <math>y^{R^\sim}</math>.
}}

{{Remark|everything gets a little simpler when <math>R</math> is a symmetric relation on <math>X</math>.}}

==Phase Semantics==

===Phase spaces===

{{Definition|title=monoid|
A monoid is simply a set <math>X</math> equipped with a binary operation <math>\_\cdot\_</math> s.t.:
# the operation is associative
# there is a neutral element <math>1\in X</math>
The monoid is ''commutative'' when the binary operation is commutative.
}}

{{Definition|title=Phase space|
A phase space is given by:
# a commutative monoid <math>(X,1,\cdot)</math>,
# together with a subset <math>\Bot\subseteq X</math>.
The elements of <math>X</math> are called ''phases''.

We write <math>\bot</math> for the relation <math>\{(a,b)\ |\ a\cdot b \in \Bot\}</math>. This relation is symmetric.

A ''fact'' in a phase space is simply a fixed point for the closure operator <math>x\mapsto x\biorth</math>.
}}

Thanks to the preliminary work, we have:

{{Corollary|
The set of facts of a phase space is a complete lattice where:
# <math>\bigwedge_{i\in I} x_i</math> is simply <math>\bigcap_{i\in I} x_i</math>,
# <math>\bigvee_{i\in I} x_i</math> is <math>\left(\bigcup_{i\in I} x_i\right)\biorth</math>.
}}

===Additive connectives===

The previous corollary makes the following definition correct:

{{Definition|title=additive connectives|
If <math>(X,1,\cdot,\Bot)</math> is a phase space, we define the following facts and operations on facts:
# <math>\top = X = \emptyset\orth</math>
# <math>\zero = \emptyset\biorth = X\orth</math>
# <math>x\with y = x\cap y</math>
# <math>x\plus y = (x\cup y)\biorth</math>
}}

Once again, the next lemma follows from previous observations:

{{Lemma|title=additive de Morgan laws|
We have
# <math>\zero\orth = \top</math>
# <math>\top\orth = \zero</math>
# <math>(x\with y)\orth = x\orth \plus y\orth</math>
# <math>(x\plus y)\orth = x\orth \with y\orth</math>
}}

===Multiplicative connectives===

In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space. One interpretation that is reminiscent in phase semantics is that our spaces are collections of ''tests'' / programs / proofs / ''strategies'' that can interact with each other. The result of the interaction between <math>a</math> and <math>b</math> is simply <math>a\cdot b</math>.

The set <math>\Bot</math> can be thought of as the set of "good" things, and we thus have <math>a\in x\orth</math> iff "<math>a</math> interacts correctly with all the elements of <math>x</math>".

{{Definition|
If <math>x</math> and <math>y</math> are two subsets of a phase space, we write <math>x\cdot y</math> for the set <math>\{a\cdot b\ |\ a\in x, b\in y\}</math>.
}}
Thus <math>x\cdot y</math> contains all the possible interactions between one element of <math>x</math> and one element of <math>y</math>.

The tensor connective of linear logic is now defined as:

{{Definition| title=multiplicative connectives|
If <math>x</math> and <math>y</math> are facts in a phase space, we define
* <math>\one = \{1\}\biorth</math>;
* <math>\bot = \one\orth</math>;
* the tensor <math>x\tens y</math> to be the fact <math>(x\cdot y)\biorth</math>;
* the par connective is the de Morgan dual of the tensor: <math>x\parr y = (x\orth \tens y\orth)\orth</math>;
* the linear arrow is just <math>x\limp y = x\orth\parr y = (x\tens y\orth)\orth</math>.
}}

Note that by unfolding the definition of <math>\limp</math>, we have the following, "intuitive" definition of <math>x\limp y</math>:

{{Lemma|
If <math>x</math> and <math>y</math> are facts, we have <math>a\in x\limp y</math> iff <math>\forall b\in x,\,a\cdot b\in y</math>
}}

{{Proof|
easy exercise. }}

Readers familiar with realisability will appreciate...

{{Remark|
Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}}

===Properties===

All the expected properties hold:

{{Lemma|
* The operations <math>\tens</math>, <math>\parr</math>, <math>\plus</math> and <math>\with</math> are commutative and associative,
* They have respectively <math>\one</math>, <math>\bot</math>, <math>\zero</math> and <math>\top</math> for neutral element,
* <math>\zero</math> is absorbant for <math>\tens</math>,
* <math>\top</math> is absorbant for <math>\parr</math>,
* <math>\tens</math> distributes over <math>\plus</math>,
* <math>\parr</math> distributes over <math>\with</math>.
}}

===Exponentials===

{{Definition|title=Exponentials|
Write <math>I</math> for the set of idempotents of a phase space: <math>I=\{a\ |\ a\cdot a=a\}</math>. We put:
# <math>\oc x = (x\cap I\cap \one)\biorth</math>,
# <math>\wn x = (x\orth\cap I\cap\one)\orth</math>.
}}

This definition captures precisely the intuition behind the exponentials:
* we need to have contraction, hence we restrict to indempotents in <math>x</math>,
* and weakening, hence we restrict to <math>\one</math>.
Since <math>I</math> isn't necessarily a fact, we then take the biorthogonal to get a fact...

== Soundness ==

{{Definition|Let <math>(X, 1, \cdot)</math> be a commutative monoid.

Given a formula <math>A</math> of linear logic and an assignation <math>\rho</math> that associate a fact to any variable, we can inductively define the interpretation <math>\sem{A}_\rho</math> of <math>A</math> in <math>X</math> as one would expect. Interpretation is lifted to sequents as <math>\sem{A_1, \hdots, A_n}_\rho = \sem{A_1}_\rho \parr \hdots \parr \sem{A_n}_\rho</math>.}}

{{Theorem|Let <math>\Gamma</math> be a provable sequent in linear logic. Then <math>1_X \in \sem{\Gamma}.}}

{{Proof|By induction on <math>\vdash\Gamma</math>.}}

== Completeness ==

Phase semantics is complete w.r.t. linear logic. In order to prove this, we need to build a particular commutative monoid.

{{Definition|We define the '''syntactic monoid''' as follows:

* Its elements are sequents <math>\Gamma</math> quotiented by the equivalence relation <math>\cong</math> generated by the rules:
*# <math>\Gamma \cong \Delta</math> if <math>\Gamma</math> is a permutation of <math>\Delta</math>
*# <math>\wn{A}, \wn{A}, \Gamma \cong \wn{A}, \Gamma</math>

* Product is concatenation: <math>\Gamma \cdot \Delta := \Gamma, \Delta</math>

* Neutral element is the empty sequent: <math>1 := \emptyset</math>.}}

The equivalence relation intuitively means that we do not care about the multiplicity of <math>\wn</math>-formulae.

{{Lemma|The syntactic monoid is indeed a commutative monoid.}}

{{Definition|The '''syntactic assignation''' is the assignation that sends any variable <math>\alpha</math> to the fact <math>\{\alpha\}\orth</math>.}}

{{Theorem|If <math>\Gamma\in\sem{\Gamma}\orth</math>, then <math>\vdash\Gamma</math>.}}

{{Proof|By induction on <math>\Gamma</math>.}}

Actually, this result is stronger, as the proof does not use the cut-rule in the reconstruction of <math>\vdash\Gamma</math>.

{{Theorem|If <math>\Gamma\in\sem{\Gamma}\orth</math>, then <math>\Gamma</math> is cut-free provable.}}

From soundness, one can retrieve the cut-elimination theorem.

{{Corollary|Linear logic enjoys the cut-elimination property.}}

==The Rest==

Coherent semantics

2011-10-04T22:48:27Z

Pierre-Marie Pédrot:

''Coherent semantics'' was invented by Girard in the paper ''The system F, 15 years later''<ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=The System F of Variable Types, Fifteen Years Later|journal=Theoretical Computer Science|volume=45|issue=2|pages=159-192|doi=10.1016/0304-3975(86)90044-7|year=1986}}</ref>with the objective of building a denotationnal interpretation of second order intuitionnistic logic (aka polymorphic lambda-calculus).

Coherent semantics is based on the notion of ''stable functions'' that was initially proposed by Gérard Berry. Stability is a condition on Scott continuous functions that expresses the determinism of the relation between the output and the input: the typical Scott continuous but non stable function is the ''parallel or'' because when the two inputs are both set to '''true''', only one of them is the reason why the result is '''true''' but there is no way to determine which one.

A further achievement of coherent semantics was that it allowed to endow the set of stable functions from <math>X</math> to <math>Y</math> with a structure of domain, thus closing the category of coherent spaces and stable functions. However the most interesting point was the discovery of a special class of stable functions, ''linear functions'', which was the first step leading to Linear Logic.

== The cartesian closed structure of coherent semantics ==

There are three equivalent definitions of coherent spaces: the first one, ''coherent spaces as domains'', is interesting from a historical point of view as it emphazises the fact that coherent spaces are particular cases of Scott domains. The second one, ''coherent spaces as graphs'', is the most commonly used and will be our "official" definition in the sequel. The last one, ''cliqued spaces'' is a particular example of a more general scheme that one could call "symmetric reducibility"; this scheme is underlying lots of constructions in linear logic such as [[phase semantics]] or the proof of strong normalisation for proof-nets.

=== Coherent spaces ===

A coherent space <math>X</math> is a collection of subsets of a set <math>\web X</math> satisfying some conditions that will be detailed shortly. The elements of <math>X</math> are called the ''cliques'' of <math>X</math> (for reasons that will be made clear in a few lines). The set <math>\web X</math> is called the ''web'' of <math>X</math> and its elements are called the ''points'' of <math>X</math>; thus a clique is a set of points. Note that the terminology is a bit ambiguous as the points of <math>X</math> are the elements of the web of <math>X</math>, not the elements of <math>X</math>.

The definitions below give three equivalent conditions that have to be satisfied by the cliques of a coherent space.

==== As domains ====

The cliques of <math>X</math> have to satisfy:
* subset closure: if <math>x\subset y\in X</math> then <math>x\in X</math>,
* singletons: <math>\{a\}\in X</math> for <math>a\in\web X</math>.
* binary compatibility: if <math>A</math> is a family of pairwise compatible cliques of <math>X</math>, that is if <math>x\cup y\in X</math> for any <math>x,y\in A</math>, then <math>\bigcup A\in X</math>.

A coherent space is thus ordered by inclusion; one easily checks that it is a domain. In particular finite cliques of <math>X</math> correspond to compact elements.

==== As graphs ====

There is a reflexive and symetric relation <math>\coh_X</math> on <math>\web X</math> (the ''coherence relation'') such that any subset <math>x</math> of <math>\web X</math> is a clique of <math>X</math> iff <math>\forall a,b\in x,\, a\coh_X b</math>. In other terms <math>X</math> is the set of complete subgraphs of the simple unoriented graph of the <math>\coh_X</math> relation; this is the reason why elements of <math>X</math> are called ''cliques''.

The ''strict coherence relation'' <math>\scoh_X</math> on <math>X</math> is defined by: <math>a\scoh_X b</math> iff <math>a\neq b</math> and <math>a\coh_X b</math>.

A coherent space in the domain sense is seen to be a coherent space in the graph sense by setting <math>a\coh_X b</math> iff <math>\{a,b\}\in X</math>; conversely one can check that cliques in the graph sense are subset closed and satisfy the binary compatibility condition.

A coherent space is completely determined by its web and its coherence relation, or equivalently by its web and its strict coherence.

==== As cliqued spaces ====

{{Definition|title=Duality|
Let <math>x, y\subseteq \web{X}</math> be two sets. We will say that they are dual, written <math>x\perp y</math> if their intersection contains at most one element: <math>\mathrm{Card}(x\cap y)\leq 1</math>. As usual, it defines an [[orthogonality relation]] over <math>\powerset{\web{X}}</math>.}}

The last way to express the conditions on the cliques of a coherent space <math>X</math> is simply to say that we must have <math>X\biorth = X</math>.

==== Equivalence of definitions ====

Let <math>X</math> be a cliqued space and define a relation on <math>\web X</math> by setting <math>a\coh_X b</math> iff there is <math>x\in X</math> such that <math>a, b\in x</math>. This relation is obviously symetric; it is also reflexive because all singletons belong to <math>X</math>: if <math>a\in \web X</math> then <math>\{a\}</math> is dual to any element of <math>X\orth</math> (actually <math>\{a\}</math> is dual to any subset of <math>\web X</math>), thus <math>\{a\}</math> is in <math>X\biorth</math>, thus in <math>X</math>.

Let <math>a\coh_X b</math>. Then <math>\{a,b\}\in X</math>; indeed there is an <math>x\in X</math> such that <math>a, b\in x</math>. This <math>x</math> is dual to any <math>y\in X\orth</math>, that is meets any <math>y\in X\orth</math> in a most one point. Since <math>\{a,b\}\subset x</math> this is also true of <math>\{a,b\}</math>, so that <math>\{a,b\}</math> is in <math>X\biorth</math> thus in <math>X</math>.

Now let <math>x</math> be a clique for <math>\coh_X</math> and <math>y</math> be an element of <math>X\orth</math>. Suppose <math>a, b\in x\cap y</math>, then since <math>a</math> and <math>b</math> are coherent (by hypothesis on <math>x</math>) we have <math>\{a,b\}\in X</math> and since <math>y\in X\orth</math> we must have that <math>\{a,b\}</math> and <math>y</math> meet in at most one point. Thus <math>a = b</math> and we have shown that <math>x</math> and <math>y</math> are dual. Since <math>y</math> was arbitrary this means that <math>x</math> is in <math>X\biorth</math>, thus in <math>X</math>. Finally we get that any set of pairwise coherent points of <math>X</math> is in <math>X</math>. Conversely given <math>x\in X</math> its points are obviously pairwise coherent so eventually we get that <math>X</math> is a coherent space in the graph sense.

Conversely given a coherent space <math>X</math> in the graph sense, one can check that it is a cliqued space. Call ''anticlique'' a set <math>y\subset \web X</math> of pairwise incoherent points: for all <math>a, b</math> in <math>y</math>, if <math>a\coh_X b</math> then <math>a=b</math>. Any anticlique intersects any clique in at most one point: let <math>x</math> be a clique and <math>y</math> be an anticlique, then if <math>a,b\in x\cap y</math>, since <math>a, b\in x</math> we have <math>a\coh_X b</math> and since <math>y</math> is an anticlique we have <math>a = b</math>. Thus <math>y\in X\orth</math>. Conversely given any <math>y\in X\orth</math> and <math>a, b\in y</math>, suppose <math>a\coh_X b</math>. Then <math>\{a,b\}\in X</math>, thus <math>\{a,b\}\perp y</math> which entails that <math>\{a, b\}</math> has at most one point so that <math>a = b</math>: we have shown that any two elements of <math>y</math> are incoherent.

Thus the collection of anticliques of <math>X</math> is the dual <math>X\orth</math> of <math>X</math>. Note that the incoherence relation defined above is reflexive and symetric, so that <math>X\orth</math> is a coherent space in the graph sense. Thus we can do for <math>X\orth</math> exactly what we've just done for <math>X</math> and consider the anti-anticliques, that is the anticliques for the incoherent relation which are the cliques for the in-incoherent relation. It is not difficult to see that this in-incoherence relation is just the coherence relation we started with; we thus obtain that <math>X\biorth = X</math>, so that <math>X</math> is a cliqued space.

=== Stable functions ===

{{Definition|title=Stable function|
Let <math>X</math> and <math>Y</math> be two coherent spaces. A function <math>F:X\longrightarrow Y</math> is ''stable'' if it satisfies:
* it is non decreasing: for any <math>x,y\in X</math> if <math>x\subset y</math> then <math>F(x)\subset F(y)</math>;
* it is continuous (in the Scott sense): if <math>A</math> is a directed family of cliques of <math>X</math>, that is if for any <math>x,y\in A</math> there is a <math>z\in A</math> such that <math>x\cup y\subset z</math>, then <math>\bigcup_{x\in A}F(x) = F(\bigcup A)</math>;
* it satisfies the stability condition: if <math>x,y\in X</math> are compatible, that is if <math>x\cup y\in X</math>, then <math>F(x\cap y) = F(x)\cap F(y)</math>.
}}

This definition is admitedly not very tractable. An equivalent and most useful caracterisation of stable functions is given by the following theorem.

{{Theorem|
Let <math>F:X\longrightarrow Y</math> be a non-decreasing function from the coherent space <math>X</math> to the coherent space <math>Y</math>. The function <math>F</math> is stable iff it satisfies: for any <math>x\in X</math>, <math>b\in\web Y</math>, if <math>b\in F(x)</math> then there is a finite clique <math>x_0\subset x</math> such that:
* <math>b\in F(x_0)</math>,
* for any <math>y\subset x</math> if <math>b\in F(y)</math> then <math>x_0\subset y</math> (<math>x_0</math> is ''the'' minimum sub-clique of <math>x</math> such that <math>b\in F(x_0)</math>).
}}

Note that the stability condition doesn't depend on the coherent space structure and can be expressed more generally for continuous functions on domains. However, as mentionned in the introduction, the restriction to coherent spaces allows to endow the set of stable functions from <math>X</math> to <math>Y</math> with a structure of coherent space.

{{Definition|title=The space of stable functions|
Let <math>X</math> and <math>Y</math> be coherent spaces. We denote by <math>X_{\mathrm{fin}}</math> the set of ''finite'' cliques of <math>X</math>. The function space <math>X\imp Y</math> is defined by:
* <math>\web{X\imp Y} = X_{\mathrm{fin}}\times \web Y</math>,
* <math>(x_0, a)\coh_{X\imp Y}(y_0, b)</math> iff <math>\begin{cases}\text{if } x_0\cup y_0\in X\text{ then } a\coh_Y b,\\
\text{if } x_0\cup y_0\in X\text{ and } a = b\text{ then } x_0 = y_0\end{cases}</math>.
}}

One could equivalently define the strict coherence relation on <math>X\imp Y</math> by: <math>(x_0,a)\scoh_{X\imp Y}(y_0, b)</math> iff when <math>x_0\cup y_0\in X</math> then <math>a\scoh_Y b</math> (equivalently <math>x_0\cup y_0\not\in X</math> or <math>a\scoh_Y b</math>).

{{Definition|title=Trace of a stable function|
Let <math>F:X\longrightarrow Y</math> be a function. The ''trace'' of <math>F</math> is the set:

<math>\mathrm{Tr}(F) = \{(x_0, b), x_0\text{ minimal such that } b\in F(x_0)\}</math>.
}}

{{theorem|
<math>F</math> is stable iff <math>\mathrm{Tr}(F)</math> is a clique of the function space <math>X\imp Y</math>
}}

In particular the continuity of <math>F</math> entails that if <math>x_0</math> is minimal such that <math>b\in F(x_0)</math>, then <math>x_0</math> is finite.

{{Definition|title=The evaluation function|
Let <math>f</math> be a clique in <math>X\imp Y</math>. We define a function <math>\mathrm{Fun}\,f:X\longrightarrow Y</math> by: <math>\mathrm{Fun}\,f(x) = \{b\in Y,\text{ there is }x_0\subset x\text{ such that }(x_0, b)\in f\}</math>.
}}

{{Theorem|title=Closure|
If <math>f</math> is a clique of the function space <math>X\imp Y</math> then we have <math>\mathrm{Tr}(\mathrm{Fun}\,f) = f</math>. Conversely if <math>F:X\longrightarrow Y</math> is a stable function then we have <math>F = \mathrm{Fun}\,\mathrm{Tr}(F)</math>.
}}

=== Cartesian product ===

{{Definition|title=Cartesian product|
Let <math>X_1</math> and <math>X_2</math> be two coherent spaces. We define the coherent space <math>X_1\with X_2</math> (read <math>X_1</math> ''with'' <math>X_2</math>):
* the web is the disjoint union of the webs: <math>\web{X_1\with X_2} = \{1\}\times\web{X_1}\cup \{2\}\times\web{X_2}</math>;
* the coherence relation is the serie composition of the relations on <math>X_1</math> and <math>X_2</math>: <math>(i, a)\coh_{X_1\with X_2}(j, b)</math> iff either <math>i\neq j</math> or <math>i=j</math> and <math>a\coh_{X_i} b</math>.
}}

This definition is just the way to put a coherent space structure on the cartesian product. Indeed one easily shows the

{{Theorem|
Given cliques <math>x_1</math> and <math>x_2</math> in <math>X_1</math> and <math>X_2</math>, we define the subset <math>\langle x_1, x_2\rangle</math> of <math>\web{X_1\with X_2}</math> by: <math>\langle x_1, x_2\rangle = \{1\}\times x_1\cup \{2\}\times x_2</math>. Then <math>\langle x_1, x_2\rangle</math> is a clique in <math>X_1\with X_2</math>.

Conversely, given a clique <math>x\in X_1\with X_2</math>, for <math>i=1,2</math> we define <math>\pi_i(x) = \{a\in X_i, (i, a)\in x\}</math>. Then <math>\pi_i(x)</math> is a clique in <math>X_i</math> and the function <math>\pi_i:X_1\with X_2\longrightarrow X_i</math> is stable.

Furthemore these two operations are inverse of each other: <math>\pi_i(\langle x_1, x_2\rangle) = x_i</math> and <math>\langle\pi_1(x), \pi_2(x)\rangle = x</math>. In particular any clique in <math>X_1\with X_2</math> is of the form <math>\langle x_1, x_2\rangle</math>.
}}

Altogether the results above (and a few other more that we shall leave to the reader) allow to get:

{{Theorem|
The category of coherent spaces and stable functions is cartesian closed.
}}

In particular this means that if we define <math>\mathrm{Eval}:(X\imp Y)\with X\longrightarrow Y</math> by: <math>\mathrm{Eval}(\langle f, x\rangle) = \mathrm{Fun}\,f(x)</math> then <math>\mathrm{Eval}</math> is stable.

== The monoidal structure of coherent semantics ==

=== Linear functions ===

{{Definition|title=Linear function|
A function <math>F:X\longrightarrow Y</math> is ''linear'' if it is stable and furthemore satisfies: for any family <math>A</math> of pairwise compatible cliques of <math>X</math>, that is such that for any <math>x, y\in A</math>, <math>x\cup y\in X</math>, we have <math>\bigcup_{x\in A}F(x) = F(\bigcup A)</math>.
}}

In particular if we take <math>A</math> to be the empty family, then we have <math>F(\emptyset) = \emptyset</math>.

The condition for linearity is quite similar to the condition for Scott continuity, except that we dropped the constraint that <math>A</math> is ''directed''. Linearity is therefore much stronger than stability: most stable functions are not linear.

However most of the functions seen so far are linear. Typically the function <math>\pi_i:X_1\with X_2\longrightarrow X_i</math> is linear from wich one may deduce that the ''with'' construction is also a cartesian product in the category of coherent spaces and linear functions.

As with stable function we have an equivalent and much more tractable caracterisation of linear function:

{{Theorem|
Let <math>F:X\longrightarrow Y</math> be a continuous function. Then <math>F</math> is linear iff it satisfies: for any clique <math>x\in X</math> and any <math>b\in F(x)</math> there is a unique <math>a\in x</math> such that <math>b\in F(\{a\})</math>.
}}

Just as the caracterisation theorem for stable functions allowed us to build the coherent space of stable functions, this theorem will help us to endow the set of linear maps with a structure of coherent space.

{{Definition|title=The linear functions space|
Let <math>X</math> and <math>Y</math> be coherent spaces. The ''linear function space'' <math>X\limp Y</math> is defined by:
* <math>\web{X\limp Y} = \web X\times \web Y</math>,
* <math>(a,b)\coh_{X\limp Y}(a', b')</math> iff <math>\begin{cases}\text{if }a\coh_X a'\text{ then } b\coh_Y b'\\
\text{if }a\coh_X a' \text{ and }b=b'\text{ then }a=a'\end{cases}</math>
}}

Equivalently one could define the strict coherence to be: <math>(a,b)\scoh_{X\limp Y}(a',b')</math> iff <math>a\scoh_X a'</math> entails <math>b\scoh_Y b'</math>.

{{Definition|title=Linear trace|
Let <math>F:X\longrightarrow Y</math> be a function. The ''linear trace'' of <math>F</math> denoted as <math>\mathrm{LinTr}(F)</math> is the set:
<math>\mathrm{LinTr}(F) = \{(a, b)\in\web X\times\web Y</math> such that <math>b\in F(\{a\})\}</math>.
}}

{{Theorem|
If <math>F</math> is linear then <math>\mathrm{LinTr}(F)</math> is a clique of <math>X\limp Y</math>.
}}

{{Definition|title=Evaluation of linear function|
Let <math>f</math> be a clique of <math>X\limp Y</math>. We define the function <math>\mathrm{LinFun}\,f:X\longrightarrow Y</math> by: <math>\mathrm{LinFun}\,f(x) = \{b\in\web Y</math> such that there is an <math>a\in x</math> satisfying <math>(a,b)\in f\}</math>.
}}

{{Theorem|title=Linear closure|
Let <math>f</math> be a clique in <math>X\limp Y</math>. Then we have <math>\mathrm{LinTr}(\mathrm{LinFun}\, f) = f</math>. Conversely if <math>F:X\longrightarrow Y</math> is linear then we have <math>F = \mathrm{LinFun}\,\mathrm{LinTr}(F)</math>.
}}

It remains to define a tensor product and we will get that the category of coherent spaces with linear functions is monoidal symetric (it is actually *-autonomous).

=== Tensor product ===

{{Definition|title=Tensor product|
Let <math>X</math> and <math>Y</math> be coherent spaces. Their tensor product <math>X\tens Y</math> is defined by: <math>\web{X\tens Y} = \web X\times\web Y</math> and <math>(a,b)\coh_{X\tens Y}(a',b')</math> iff <math>a\coh_X a'</math> and <math>b\coh_Y b'</math>.
}}

{{Theorem|
The category of coherent spaces with linear maps and tensor product is [[Categorical semantics#Modeling IMLL|monoidal symetric closed]].
}}

The closedness is a consequence of the existence of the linear isomorphism:
<math>\varphi:X\tens Y\limp Z\ \stackrel{\sim}{\longrightarrow}\ X\limp(Y\limp Z)</math>

that is defined by its linear trace: <math>\mathrm{LinTr}(\varphi) = \{(((a, b), c), (a, (b, c))),\, a\in\web X,\, b\in \web Y,\, c\in\web Z\}</math>.

=== Linear negation ===

{{Definition|title=Linear negation|
Let <math>X</math> be a coherent space. We define the ''incoherence relation'' on <math>\web X</math> by: <math>a\incoh_X b</math> iff <math>a\coh_X b</math> entails <math>a=b</math>. The incoherence relation is reflexive and symetric; we call ''dual'' or ''linear negation'' of <math>X</math> the associated coherent space denoted <math>X\orth</math>, thus defined by: <math>\web{X\orth} = \web X</math> and <math>a\coh_{X\orth} b</math> iff <math>a\incoh_X b</math>.
}}

The cliques of <math>X\orth</math> are called the ''anticliques'' of <math>X</math>. As seen in the section on cliqued spaces we have <math>X\biorth=X</math>.

{{Theorem|
The category of coherent spaces with linear maps, tensor product and linear negation is *-autonomous.
}}

This is in particular consequence of the existence of the isomorphism:
<math>\varphi:X\limp Y\ \stackrel{\sim}{\longrightarrow}\ Y\orth\limp X\orth</math>

defined by its linear trace: <math>\mathrm{LinTr}(\varphi) = \{((a, b), (b, a)),\, a\in\web X,\, b\in\web Y\}</math>.

== Exponentials ==

In linear algebra, bilinear maps may be factorized through the tensor product. Similarly there is a coherent space <math>\oc X</math> that allows to factorize stable functions through linear functions.

{{Definition|title=Of course|
Let <math>X</math> be a coherent space; recall that <math>X_{\mathrm{fin}}</math> denotes the set of finite cliques of <math>X</math>. We define the space <math>\oc X</math> (read ''of course <math>X</math>'') by: <math>\web{\oc X} = X_{\mathrm{fin}}</math> and <math>x_0\coh_{\oc X}y_0</math> iff <math>x_0\cup y_0</math> is a clique of <math>X</math>.
}}

Thus a clique of <math>\oc X</math> is a set of finite cliques of <math>X</math> the union of wich is a clique of <math>X</math>.

{{Theorem|
Let <math>X</math> be a coherent space. Denote by <math>\beta:X\longrightarrow \oc X</math> the stable function whose trace is: <math>\mathrm{Tr}(\beta) = \{(x_0, x_0),\, x_0\in X_{\mathrm{fin}}\}</math>. Then for any coherent space <math>Y</math> and any stable function <math>F: X\longrightarrow Y</math> there is a unique ''linear'' function <math>\bar F:\oc X\longrightarrow Y</math> such that <math>F = \bar F\circ \beta</math>.

Furthermore we have <math>X\imp Y = \oc X\limp Y</math>.
}}

{{Theorem|title=The exponential isomorphism|
Let <math>X</math> and <math>Y</math> be two coherent spaces. Then there is a linear isomorphism:
<math>\varphi:\oc(X\with Y)\quad\stackrel{\sim}{\longrightarrow}\quad \oc X\tens\oc Y</math>.
}}

The iso <math>\varphi</math> is defined by its trace: <math>\mathrm{Tr}(\varphi) = \{(x_0, (\pi_1(x_0), \pi_2(x_0)), x_0\text{ finite clique of } X\with Y\}</math>.

This isomorphism, that sends an additive structure (the web of a with is obtained by disjoint union) onto a multiplicative one (the web of a tensor is obtained by cartesian product) is the reason why the of course is called an ''exponential''.

== Dual connectives and neutrals ==

By linear negation all the constructions defined so far (<math>\with, \tens, \oc</math>) have a dual.

=== The direct sum ===

The dual of <math>\with</math> is <math>\plus</math> defined by: <math>X\plus Y = (X\orth\with Y\orth)\orth</math>. An equivalent definition is given by: <math>\web{X\plus Y} = \web{X\with Y} = \{1\}\times \web X \cup \{2\}\times\web Y</math> and <math>(i, a)\coh_{X\plus Y} (j, b)\text{ iff } i = j = 1 \text{ and } a\coh_X b,\text{ or }i = j = 2\text{ and } a\coh_Y b</math>.

{{Theorem|
Let <math>x'</math> be a clique of <math>X\plus Y</math>; then <math>x'</math> is of the form <math>\{i\}\times x</math> where <math>i = 1\text{ and }x\in X</math>, or <math>i = 2\text{ and }x\in Y</math>.

Denote <math>\mathrm{inl}:X\longrightarrow X\plus Y</math> the function defined by <math>\mathrm{inl}(x) = \{1\}\times x</math> and by <math>\mathrm{inr}:Y\longrightarrow X\plus Y</math> the function defined by <math>\mathrm{inr}(x) = \{2\}\times x</math>. Then <math>\mathrm{inl}</math> and <math>\mathrm{inr}</math> are linear.

If <math>F:X\longrightarrow Z</math> and <math>G:Y\longrightarrow Z</math> are ''linear'' functions then the function <math>H:X\plus Y \longrightarrow Z</math> defined by <math>H(\mathrm{inl}(x)) = F(x)</math> and <math>H(\mathrm{inr}(y)) = G(y)</math> is linear.
}}

In other terms <math>X\plus Y</math> is the direct sum of <math>X</math> and <math>Y</math>. Note that in the theorem all functions are ''linear''. Things doesn't work so smoothly for stable functions. Historically it was after noting this defect of coherent semantics w.r.t. the intuitionnistic implication that Girard was leaded to discover linear functions.

=== The par and the why not ===

We now come to the most mysterious constructions of coherent semantics: the duals of the tensor and the of course.

The ''par'' is the dual of the tensor, thus defined by: <math>X\parr Y = (X\orth\tens Y\orth)\orth</math>. From this one can deduce the definition in graph terms: <math>\web{X\parr Y} = \web{X\tens Y} = \web X\times \web Y</math> and <math>(a,b)\scoh_{X\parr Y} (a',b')</math> iff <math>a\scoh_X a'</math> or <math>b\scoh_Y b'</math>. With this definition one sees that we have:

<math>X\limp Y = X\orth\parr Y</math>

for any coherent spaces <math>X</math> and <math>Y</math>. This equation can be seen as an alternative definition of the par: <math>X\parr Y = X\orth\limp Y</math>.

Similarly the dual of the of course is called ''why not'' defined by: <math>\wn X = (\oc X\orth)\orth</math>. From this we deduce the definition in the graph sense which is a bit tricky: <math>\web{\wn X}</math> is the set of finite anticliques of <math>X</math>, and given two finite anticliques <math>x</math> and <math>y</math> of <math>X</math> we have <math>x\scoh_{\wn X} y</math> iff there is <math>a\in x</math> and <math>b\in y</math> such that <math>a\scoh_X b</math>.

Note that both for the par and the why not it is much more convenient to define the strict coherence than the coherence.

With these two last constructions, the equation between the stable function space, the of course and the linear function space may be written:

<math>X\imp Y = \wn X\orth\parr Y</math>.

=== One and bottom ===

Depending on the context we denote by <math>\one</math> or <math>\bot</math> the coherent space whose web is a singleton and whose coherence relation is the trivial reflexive relation.

{{Theorem|
<math>\one</math> is neutral for tensor, that is, there is a linear isomorphism <math>\varphi:X\tens\one\ \stackrel{\sim}{\longrightarrow}\ X</math>.

Similarly <math>\bot</math> is neutral for par.
}}

=== Zero and top ===

Depending on the context we denote by <math>\zero</math> or <math>\top</math> the coherent space with empty web.

{{Theorem|
<math>\zero</math> is neutral for the direct sum <math>\plus</math>, <math>\top</math> is neutral for the cartesian product <math>\with</math>.
}}

{{Remark|
It is one of the main defect of coherent semantics w.r.t. linear logic that it identifies the neutrals: in coherent semantics <math>\zero = \top</math> and <math>\one = \bot</math>. However there is no known semantics of LL that solves this problem in a satisfactory way.}}

== The failure of coherent semantics ==

Coherent semantics was an important milestone in the modern theory of logic of programs. However it suffers from a number of defects the correction of which have motivated lots of work.

=== Sequentiality ===

Sequentiality is a property that we will not define here (it would diserve its own article). We rely on the intuition that a function of <math>n</math> arguments is sequential if one can determine which of these argument is examined first during the computation. Obviously any function implemented in a functionnal language is sequential; for example the function ''or'' defined à la CAML by:

<code>or = fun (x, y) -> if x then true else y</code>

examines its argument x first. Note that this may be expressed more abstractly by the property: <math>\mathrm{or}(\bot, x) = \bot</math> for any boolean <math>x</math>: the function ''or'' needs its first argument in order to compute anything. On the other hand we have <math>\mathrm{or}(\mathrm{true}, \bot) = \mathrm{true}</math>: in some case (when the first argument is true), the function doesn't need its second argument at all.

The typical non sequential function is the ''parallel or'' (that one cannot define in a CAML like language).

For a while one may have believed that the stability condition on which coherent semantics is built was enough to capture the notion of ''sequentiality'' of programs. A hint was the already mentionned fact that the ''parallel or'' is not stable. This diserves a bit of explanation.

==== The parallel or is not stable ====

Let <math>B</math> be the coherent space of booleans, also know as the flat domain of booleans: <math>\web B = \{tt, ff\}</math> where <math>tt</math> and <math>ff</math> are two arbitrary distinct objects (for example one may take <math>tt = 0</math> and <math>ff = 1</math>) and for any <math>b_1, b_2\in \web B</math>, define <math>b_1\coh_B b_2</math> iff <math>b_1 = b_2</math>. Then <math>B</math> has exactly three cliques: the empty clique that we shall denote <math>\bot</math>, the singleton <math>\{tt\}</math> that we shall denote <math>T</math> and the singleton <math>\{ff\}</math> that we shall denote <math>F</math>. These three cliques are ordered by inclusion: <math>\bot \leq T, F</math> (we use <math>\leq</math> for <math>\subset</math> to enforce the idea that coherent spaces are domains).

Recall the [[#Cartesian product|definition of the with]], and in particular that any clique of <math>B\with B</math> has the form <math>\langle x, y\rangle</math> where <math>x</math> and <math>y</math> are cliques of <math>B</math>. Thus <math>B\with B</math> has 9 cliques: <math>\langle\bot,\bot\rangle,\ \langle\bot, T\rangle,\ \langle\bot, F\rangle,\ \langle T,\bot\rangle,\ \dots</math> that are ordered by the product order: <math>\langle x,y\rangle\leq \langle x,y\rangle</math> iff <math>x\leq x'</math> and <math>y\leq y'</math>.

With these notations in mind one may define the parallel or by:

<math>
\begin{array}{rcl}
\mathrm{Por} : B\with B &\longrightarrow& B\\
\langle T,\bot\rangle &\longrightarrow& T\\
\langle \bot,T\rangle &\longrightarrow& T\\
\langle F, F\rangle &\longrightarrow& F
\end{array}
</math>

The function is completely determined if we add the assumption that it is non decreasing; for example one must have <math>\mathrm{Por}\langle\bot,\bot\rangle = \bot</math> because the lhs has to be less than both <math>T</math> and <math>F</math> (because <math>\langle\bot,\bot\rangle \leq \langle T,\bot\rangle</math> and <math>\langle\bot,\bot\rangle \leq \langle F,F\rangle</math>).

The function is not stable because <math>\langle T,\bot\rangle \cap \langle \bot, T\rangle = \langle\bot, \bot\rangle</math>, thus <math>\mathrm{Por}(\langle T,\bot\rangle \cap \langle \bot, T\rangle) = \bot</math> whereas <math>\mathrm{Por}\langle T,\bot\rangle \cap \mathrm{Por}\langle \bot, T\rangle = T\cap T = T</math>.

Another way to see this is: suppose <math>x</math> and <math>y</math> are two cliques of <math>B</math> such that <math>tt\in \mathrm{Por}\langle x, y\rangle</math>, which means that <math>\mathrm{Por}\langle x, y\rangle = T</math>; according to the [[#Stable functions|caracterisation theorem of stable functions]], if <math>\mathrm{Por}</math> were stable then there would be a unique minimum <math>x_0</math> included in <math>x</math>, and a unique minimum <math>y_0</math> included in <math>y</math> such that <math>\mathrm{Por}\langle x_0, y_0\rangle = T</math>. This is not the case because both <math>\langle T,\bot\rangle</math> and <math>\langle T,\bot\rangle</math> are minimal such that their value is <math>T</math>.

In other terms, knowing that <math>\mathrm{Por}\langle x, y\rangle = T</math> doesn't tell which of <math>x</math> of <math>y</math> is responsible for that, although we know by the definition of <math>\mathrm{Por}</math> that only one of them is. Indeed the <math>\mathrm{Por}</math> function is not representable in sequential programming languages such as (typed) lambda-calculus.

So the first genuine idea would be that stability caracterises sequentiality; but...

==== The Gustave function is stable ====

The Gustave function, so-called after an old joke, was found by Gérard Berry as an example of a function that is stable but non sequential. It is defined by:

<math>
\begin{array}{rcl}
B\with B\with B &\longrightarrow& B\\
\langle T, F, \bot\rangle &\longrightarrow& T\\
\langle \bot, T, F\rangle &\longrightarrow& T\\
\langle F, \bot, T\rangle &\longrightarrow& T\\
\langle x, y, z\rangle &\longrightarrow& F
\end{array}
</math>

The last clause is for all cliques <math>x</math>, <math>y</math> and <math>z</math> such that <math>\langle x, y ,z\rangle</math> is incompatible with the three cliques <math>\langle T, F, \bot\rangle</math>, <math>\langle \bot, T, F\rangle</math> and <math>\langle F, \bot, T\rangle</math>, that is such that the union with any of these three cliques is not a clique in <math>B\with B\with B</math>. We shall denote <math>x_1</math>, <math>x_2</math> and <math>x_3</math> these three cliques.

We furthemore assume that the Gustave function is non decreasing, so that we get <math>G\langle\bot,\bot,\bot\rangle = \bot</math>.

We note that <math>x_1</math>, <math>x_2</math> and <math>x_3</math> are pairwise incompatible. From this we can deduce that the Gustave function is stable: typically if <math>G\langle x,y,z\rangle = T</math> then exactly one of the <math>x_i</math>s is contained in <math>\langle x, y, z\rangle</math>.

However it is not sequential because there is no way to determine which of its three arguments is examined first: it is not the first one otherwise we would have <math>G\langle\bot, T, F\rangle = \bot</math> and similarly it is not the second one nor the third one.

In other terms there is no way to implement the Gustave function by a lambda-term (or in any sequential programming language). Thus coherent semantics is not complete w.r.t. lambda-calculus.

The research for a right model for sequentiality was the motivation for lot of
work, ''e.g.'', ''sequential algorithms'' by Gérard Bérry and Pierre-Louis
Currien in the early eighties, that were more recently reformulated as a kind
of [[Game semantics|game model]], and the theory of ''hypercoherent spaces'' by
Antonio Bucciarelli and Thomas Ehrhard.

=== Multiplicative neutrals and the mix rule ===

Coherent semantics is slightly degenerated w.r.t. linear logic because it identifies multiplicative neutrals (it also identifies additive neutrals but that's yet another problem): the coherent spaces <math>\one</math> and <math>\bot</math> are equal.

The first consequence of the identity <math>\one = \bot</math> is that the formula <math>\one\limp\bot</math> becomes provable, and so does the formula <math>\bot</math>. Note that this doesn't entail (as in classical logic or intuitionnistic logic) that linear logic is incoherent because the principle <math>\bot\limp A</math> for any formula <math>A</math> is still not provable.

The equality <math>\one = \bot</math> has also as consequence the fact that <math>\bot\limp\one</math> (or equivalently the formula <math>\one\parr\one</math>) is provable. This principle is also known as the [[Mix|mix rule]]

<math>
\AxRule{\vdash \Gamma}
\AxRule{\vdash \Delta}
\LabelRule{\rulename{mix}}
\BinRule{\vdash \Gamma,\Delta}
\DisplayProof
</math>

as it can be used to show that this rule is admissible:

<math>
\AxRule{\vdash\Gamma}
\LabelRule{\bot_R}
\UnaRule{\vdash\Gamma, \bot}
\AxRule{\vdash\Delta}
\LabelRule{\bot_R}
\UnaRule{\vdash\Delta, \bot}
\BinRule{\vdash \Gamma, \Delta, \bot\tens\bot}
\NulRule{\vdash \one\parr\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\Gamma,\Delta}
\DisplayProof
</math>

None of the two principles <math>1\limp\bot</math> and <math>\bot\limp\one</math> are valid in linear logic. To correct this one could extend the syntax of linear logic by adding the mix-rule. This is not very satisfactory as the mix rule violates some principles of [[Polarized linear logic]], typically the fact that as sequent of the form <math>\vdash P_1, P_2</math> where <math>P_1</math> and <math>P_2</math> are positive, is never provable.

On the other hand the mix-rule is valid in coherent semantics so one could try to find some other model that invalidates the mix-rule. For example Girard's Coherent Banach spaces were an attempt to address this issue.

== References ==
<references />

Polarized linear logic

2011-10-04T22:47:47Z

Pierre-Marie Pédrot: cr

'''Polarized linear logic''' (LLP) is a logic close to plain linear logic in which structural rules, usually restricted to <math>\wn</math>-formulas, have been extended to the whole class of so called ''negative'' formulae.

== Polarization ==

LLP relies on the notion of ''polarization'', that is, it discriminates between two types of formulae, ''negative'' (noted <math>M, N...</math>) vs. ''positive'' (<math>P, Q...</math>). They are mutually defined as follows:

<math>M, N ::= X \mid M \parr N \mid \bot \mid M \with N \mid \top \mid \wn{P}</math>

<math>P, Q ::= X\orth \mid P \otimes Q \mid 1 \mid P \oplus Q \mid 0 \mid \oc{N}</math>

The dual operation <math>(-)\orth</math> extended to propositions exchanges the roles of connectors and reverses the polarity of formulae.

== Deduction rules ==

They are several design choices for the structure of sequents. In particular, LLP proofs are ''focalized'', i.e. they contain at most one positive formula. We choose to represent this explicitly using sequents of the form <math>\vdash\Gamma\mid\Delta</math>, where <math>\Gamma</math> is a multiset of negative formulae, and <math>\Delta</math> is a ''stoup'' that contains at most one positive formula (though it may be empty).

<math>
\LabelRule{\rulename{ax}}
\NulRule{\vdash P\orth \mid P}
\DisplayProof
\qquad
\AxRule{\vdash \Gamma_1, N \mid \Delta}
\AxRule{\vdash \Gamma_2 \mid N\orth}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\Gamma_1, \Gamma_2 \mid \Delta}
\DisplayProof
</math>

<br/>

<math>
\AxRule{\vdash\Gamma, N\mid\cdot}
\LabelRule{p}
\UnaRule{\vdash\Gamma\mid \oc{N}}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid P}
\LabelRule{d}
\UnaRule{\vdash\Gamma,\wn{P}\mid \cdot}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma,N,N\mid \Delta}
\LabelRule{c}
\UnaRule{\vdash\Gamma, N\mid\Delta}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid \Delta}
\LabelRule{w}
\UnaRule{\vdash\Gamma,N\mid\Delta}
\DisplayProof
</math>

<br/>

<math>
\AxRule{\vdash\Gamma_1\mid P}
\AxRule{\vdash\Gamma_2\mid Q}
\LabelRule{\tens}
\BinRule{\vdash\Gamma_1,\Gamma_2\mid P\otimes Q}
\DisplayProof
\qquad
\LabelRule{\one}
\NulRule{\vdash\cdot\mid\one}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma, M, N\mid \Delta}
\LabelRule{\parr}
\UnaRule{\vdash\Gamma, M\parr N\mid \Delta}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid \Delta}
\LabelRule{\bot}
\UnaRule{\vdash\Gamma, \bot\mid\Delta}
\DisplayProof
</math>

<br/>

<math>
\AxRule{\vdash\Gamma\mid P}
\LabelRule{\plus_1}
\UnaRule{\vdash\Gamma\mid P\plus Q}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid Q}
\LabelRule{\plus_2}
\UnaRule{\vdash\Gamma\mid P\plus Q}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma,M\mid \Delta}
\AxRule{\vdash\Gamma,N\mid \Delta}
\LabelRule{\with}
\BinRule{\vdash\Gamma,M\with N\mid \Delta}
\DisplayProof
\qquad
\LabelRule{\top}
\NulRule{\vdash\Gamma,\top\mid \Delta}
\DisplayProof
</math>

Main Page

2011-10-04T22:02:48Z

Pierre-Marie Pédrot: + polarized linear logic link

== Contents ==

* An [[introduction]] to linear logic
* Syntax
** [[Sequent calculus]]
** [[Intuitionistic linear logic]]
** [[Polarized linear logic]]
** [[Fragment|Fragments]]
** [[Proof-nets]]
** Translations of [[Translations of classical logic|classical]] and [[Translations of intuitionistic logic|intuitionistic]] logics
* [[Semantics]]
** [[Coherent semantics]]
** [[Phase semantics]]
** [[Categorical semantics]]
** [[Relational semantics]]
** [[Finiteness semantics]]
** [[Geometry of interaction]]
** [[Game semantics]]
* [[Light linear logics]]

== Getting started ==

* Please read the [[recommendations]] before edition in this wiki.
* If you are familiar with these [[recommendations]] (are you?) and only want a reference of available LaTeX macros, see [[LLWiki LaTeX Style]].
* Consult the [http://meta.wikimedia.org/wiki/Help:Contents User's Guide] for information on using the wiki software.
* You can use the [[sandbox]] for tests.
* [[Special:Wantedpages|Wanted pages]].

Coherent semantics

2011-10-04T22:02:17Z

Pierre-Marie Pédrot: ortho

''Coherent semantics'' was invented by Girard in the paper ''The system F, 15 years later''<ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=The System F of Variable Types, Fifteen Years Later|journal=Theoretical Computer Science|volume=45|issue=2|pages=159-192|doi=10.1016/0304-3975(86)90044-7|year=1986}}</ref>with the objective of building a denotationnal interpretation of second order intuitionnistic logic (aka polymorphic lambda-calculus).

Coherent semantics is based on the notion of ''stable functions'' that was initially proposed by Gérard Berry. Stability is a condition on Scott continuous functions that expresses the determinism of the relation between the output and the input: the typical Scott continuous but non stable function is the ''parallel or'' because when the two inputs are both set to '''true''', only one of them is the reason why the result is '''true''' but there is no way to determine which one.

A further achievement of coherent semantics was that it allowed to endow the set of stable functions from <math>X</math> to <math>Y</math> with a structure of domain, thus closing the category of coherent spaces and stable functions. However the most interesting point was the discovery of a special class of stable functions, ''linear functions'', which was the first step leading to Linear Logic.

== The cartesian closed structure of coherent semantics ==

There are three equivalent definitions of coherent spaces: the first one, ''coherent spaces as domains'', is interesting from a historical point of view as it emphazises the fact that coherent spaces are particular cases of Scott domains. The second one, ''coherent spaces as graphs'', is the most commonly used and will be our "official" definition in the sequel. The last one, ''cliqued spaces'' is a particular example of a more general scheme that one could call "symmetric reducibility"; this scheme is underlying lots of constructions in linear logic such as [[phase semantics]] or the proof of strong normalisation for proof-nets.

=== Coherent spaces ===

A coherent space <math>X</math> is a collection of subsets of a set <math>\web X</math> satisfying some conditions that will be detailed shortly. The elements of <math>X</math> are called the ''cliques'' of <math>X</math> (for reasons that will be made clear in a few lines). The set <math>\web X</math> is called the ''web'' of <math>X</math> and its elements are called the ''points'' of <math>X</math>; thus a clique is a set of points. Note that the terminology is a bit ambiguous as the points of <math>X</math> are the elements of the web of <math>X</math>, not the elements of <math>X</math>.

The definitions below give three equivalent conditions that have to be satisfied by the cliques of a coherent space.

==== As domains ====

The cliques of <math>X</math> have to satisfy:
* subset closure: if <math>x\subset y\in X</math> then <math>x\in X</math>,
* singletons: <math>\{a\}\in X</math> for <math>a\in\web X</math>.
* binary compatibility: if <math>A</math> is a family of pairwise compatible cliques of <math>X</math>, that is if <math>x\cup y\in X</math> for any <math>x,y\in A</math>, then <math>\bigcup A\in X</math>.

A coherent space is thus ordered by inclusion; one easily checks that it is a domain. In particular finite cliques of <math>X</math> correspond to compact elements.

==== As graphs ====

There is a reflexive and symetric relation <math>\coh_X</math> on <math>\web X</math> (the ''coherence relation'') such that any subset <math>x</math> of <math>\web X</math> is a clique of <math>X</math> iff <math>\forall a,b\in x,\, a\coh_X b</math>. In other terms <math>X</math> is the set of complete subgraphs of the simple unoriented graph of the <math>\coh_X</math> relation; this is the reason why elements of <math>X</math> are called ''cliques''.

The ''strict coherence relation'' <math>\scoh_X</math> on <math>X</math> is defined by: <math>a\scoh_X b</math> iff <math>a\neq b</math> and <math>a\coh_X b</math>.

A coherent space in the domain sense is seen to be a coherent space in the graph sense by setting <math>a\coh_X b</math> iff <math>\{a,b\}\in X</math>; conversely one can check that cliques in the graph sense are subset closed and satisfy the binary compatibility condition.

A coherent space is completely determined by its web and its coherence relation, or equivalently by its web and its strict coherence.

==== As cliqued spaces ====

{{Definition|title=Duality|
Let <math>x, y\subseteq \web{X}</math> be two sets. We will say that they are dual, written <math>x\perp y</math> if their intersection contains at most one element: <math>\mathrm{Card}(x\cap y)\leq 1</math>. As usual, it defines an [[orthogonality relation]] over <math>\powerset{\web{X}}</math>.}}

The last way to express the conditions on the cliques of a coherent space <math>X</math> is simply to say that we must have <math>X\biorth = X</math>.

==== Equivalence of definitions ====

Let <math>X</math> be a cliqued space and define a relation on <math>\web X</math> by setting <math>a\coh_X b</math> iff there is <math>x\in X</math> such that <math>a, b\in x</math>. This relation is obviously symetric; it is also reflexive because all singletons belong to <math>X</math>: if <math>a\in \web X</math> then <math>\{a\}</math> is dual to any element of <math>X\orth</math> (actually <math>\{a\}</math> is dual to any subset of <math>\web X</math>), thus <math>\{a\}</math> is in <math>X\biorth</math>, thus in <math>X</math>.

Let <math>a\coh_X b</math>. Then <math>\{a,b\}\in X</math>; indeed there is an <math>x\in X</math> such that <math>a, b\in x</math>. This <math>x</math> is dual to any <math>y\in X\orth</math>, that is meets any <math>y\in X\orth</math> in a most one point. Since <math>\{a,b\}\subset x</math> this is also true of <math>\{a,b\}</math>, so that <math>\{a,b\}</math> is in <math>X\biorth</math> thus in <math>X</math>.

Now let <math>x</math> be a clique for <math>\coh_X</math> and <math>y</math> be an element of <math>X\orth</math>. Suppose <math>a, b\in x\cap y</math>, then since <math>a</math> and <math>b</math> are coherent (by hypothesis on <math>x</math>) we have <math>\{a,b\}\in X</math> and since <math>y\in X\orth</math> we must have that <math>\{a,b\}</math> and <math>y</math> meet in at most one point. Thus <math>a = b</math> and we have shown that <math>x</math> and <math>y</math> are dual. Since <math>y</math> was arbitrary this means that <math>x</math> is in <math>X\biorth</math>, thus in <math>X</math>. Finally we get that any set of pairwise coherent points of <math>X</math> is in <math>X</math>. Conversely given <math>x\in X</math> its points are obviously pairwise coherent so eventually we get that <math>X</math> is a coherent space in the graph sense.

Conversely given a coherent space <math>X</math> in the graph sense, one can check that it is a cliqued space. Call ''anticlique'' a set <math>y\subset \web X</math> of pairwise incoherent points: for all <math>a, b</math> in <math>y</math>, if <math>a\coh_X b</math> then <math>a=b</math>. Any anticlique intersects any clique in at most one point: let <math>x</math> be a clique and <math>y</math> be an anticlique, then if <math>a,b\in x\cap y</math>, since <math>a, b\in x</math> we have <math>a\coh_X b</math> and since <math>y</math> is an anticlique we have <math>a = b</math>. Thus <math>y\in X\orth</math>. Conversely given any <math>y\in X\orth</math> and <math>a, b\in y</math>, suppose <math>a\coh_X b</math>. Then <math>\{a,b\}\in X</math>, thus <math>\{a,b\}\perp y</math> which entails that <math>\{a, b\}</math> has at most one point so that <math>a = b</math>: we have shown that any two elements of <math>y</math> are incoherent.

Thus the collection of anticliques of <math>X</math> is the dual <math>X\orth</math> of <math>X</math>. Note that the incoherence relation defined above is reflexive and symetric, so that <math>X\orth</math> is a coherent space in the graph sense. Thus we can do for <math>X\orth</math> exactly what we've just done for <math>X</math> and consider the anti-anticliques, that is the anticliques for the incoherent relation which are the cliques for the in-incoherent relation. It is not difficult to see that this in-incoherence relation is just the coherence relation we started with; we thus obtain that <math>X\biorth = X</math>, so that <math>X</math> is a cliqued space.

=== Stable functions ===

{{Definition|title=Stable function|
Let <math>X</math> and <math>Y</math> be two coherent spaces. A function <math>F:X\longrightarrow Y</math> is ''stable'' if it satisfies:
* it is non decreasing: for any <math>x,y\in X</math> if <math>x\subset y</math> then <math>F(x)\subset F(y)</math>;
* it is continuous (in the Scott sense): if <math>A</math> is a directed family of cliques of <math>X</math>, that is if for any <math>x,y\in A</math> there is a <math>z\in A</math> such that <math>x\cup y\subset z</math>, then <math>\bigcup_{x\in A}F(x) = F(\bigcup A)</math>;
* it satisfies the stability condition: if <math>x,y\in X</math> are compatible, that is if <math>x\cup y\in X</math>, then <math>F(x\cap y) = F(x)\cap F(y)</math>.
}}

This definition is admitedly not very tractable. An equivalent and most useful caracterisation of stable functions is given by the following theorem.

{{Theorem|
Let <math>F:X\longrightarrow Y</math> be a non-decreasing function from the coherent space <math>X</math> to the coherent space <math>Y</math>. The function <math>F</math> is stable iff it satisfies: for any <math>x\in X</math>, <math>b\in\web Y</math>, if <math>b\in F(x)</math> then there is a finite clique <math>x_0\subset x</math> such that:
* <math>b\in F(x_0)</math>,
* for any <math>y\subset x</math> if <math>b\in F(y)</math> then <math>x_0\subset y</math> (<math>x_0</math> is ''the'' minimum sub-clique of <math>x</math> such that <math>b\in F(x_0)</math>).
}}

Note that the stability condition doesn't depend on the coherent space structure and can be expressed more generally for continuous functions on domains. However, as mentionned in the introduction, the restriction to coherent spaces allows to endow the set of stable functions from <math>X</math> to <math>Y</math> with a structure of coherent space.

{{Definition|title=The space of stable functions|
Let <math>X</math> and <math>Y</math> be coherent spaces. We denote by <math>X_{\mathrm{fin}}</math> the set of ''finite'' cliques of <math>X</math>. The function space <math>X\imp Y</math> is defined by:
* <math>\web{X\imp Y} = X_{\mathrm{fin}}\times \web Y</math>,
* <math>(x_0, a)\coh_{X\imp Y}(y_0, b)</math> iff <math>\begin{cases}\text{if } x_0\cup y_0\in X\text{ then } a\coh_Y b,\\
\text{if } x_0\cup y_0\in X\text{ and } a = b\text{ then } x_0 = y_0\end{cases}</math>.
}}

One could equivalently define the strict coherence relation on <math>X\imp Y</math> by: <math>(x_0,a)\scoh_{X\imp Y}(y_0, b)</math> iff when <math>x_0\cup y_0\in X</math> then <math>a\scoh_Y b</math> (equivalently <math>x_0\cup y_0\not\in X</math> or <math>a\scoh_Y b</math>).

{{Definition|title=Trace of a stable function|
Let <math>F:X\longrightarrow Y</math> be a function. The ''trace'' of <math>F</math> is the set:

<math>\mathrm{Tr}(F) = \{(x_0, b), x_0\text{ minimal such that } b\in F(x_0)\}</math>.
}}

{{theorem|
<math>F</math> is stable iff <math>\mathrm{Tr}(F)</math> is a clique of the function space <math>X\imp Y</math>
}}

In particular the continuity of <math>F</math> entails that if <math>x_0</math> is minimal such that <math>b\in F(x_0)</math>, then <math>x_0</math> is finite.

{{Definition|title=The evaluation function|
Let <math>f</math> be a clique in <math>X\imp Y</math>. We define a function <math>\mathrm{Fun}\,f:X\longrightarrow Y</math> by: <math>\mathrm{Fun}\,f(x) = \{b\in Y,\text{ there is }x_0\subset x\text{ such that }(x_0, b)\in f\}</math>.
}}

{{Theorem|title=Closure|
If <math>f</math> is a clique of the function space <math>X\imp Y</math> then we have <math>\mathrm{Tr}(\mathrm{Fun}\,f) = f</math>. Conversely if <math>F:X\longrightarrow Y</math> is a stable function then we have <math>F = \mathrm{Fun}\,\mathrm{Tr}(F)</math>.
}}

=== Cartesian product ===

{{Definition|title=Cartesian product|
Let <math>X_1</math> and <math>X_2</math> be two coherent spaces. We define the coherent space <math>X_1\with X_2</math> (read <math>X_1</math> ''with'' <math>X_2</math>):
* the web is the disjoint union of the webs: <math>\web{X_1\with X_2} = \{1\}\times\web{X_1}\cup \{2\}\times\web{X_2}</math>;
* the coherence relation is the serie composition of the relations on <math>X_1</math> and <math>X_2</math>: <math>(i, a)\coh_{X_1\with X_2}(j, b)</math> iff either <math>i\neq j</math> or <math>i=j</math> and <math>a\coh_{X_i} b</math>.
}}

This definition is just the way to put a coherent space structure on the cartesian product. Indeed one easily shows the

{{Theorem|
Given cliques <math>x_1</math> and <math>x_2</math> in <math>X_1</math> and <math>X_2</math>, we define the subset <math>\langle x_1, x_2\rangle</math> of <math>\web{X_1\with X_2}</math> by: <math>\langle x_1, x_2\rangle = \{1\}\times x_1\cup \{2\}\times x_2</math>. Then <math>\langle x_1, x_2\rangle</math> is a clique in <math>X_1\with X_2</math>.

Conversely, given a clique <math>x\in X_1\with X_2</math>, for <math>i=1,2</math> we define <math>\pi_i(x) = \{a\in X_i, (i, a)\in x\}</math>. Then <math>\pi_i(x)</math> is a clique in <math>X_i</math> and the function <math>\pi_i:X_1\with X_2\longrightarrow X_i</math> is stable.

Furthemore these two operations are inverse of each other: <math>\pi_i(\langle x_1, x_2\rangle) = x_i</math> and <math>\langle\pi_1(x), \pi_2(x)\rangle = x</math>. In particular any clique in <math>X_1\with X_2</math> is of the form <math>\langle x_1, x_2\rangle</math>.
}}

Altogether the results above (and a few other more that we shall leave to the reader) allow to get:

{{Theorem|
The category of coherent spaces and stable functions is cartesian closed.
}}

In particular this means that if we define <math>\mathrm{Eval}:(X\imp Y)\with X\longrightarrow Y</math> by: <math>\mathrm{Eval}(\langle f, x\rangle) = \mathrm{Fun}\,f(x)</math> then <math>\mathrm{Eval}</math> is stable.

== The monoidal structure of coherent semantics ==

=== Linear functions ===

{{Definition|title=Linear function|
A function <math>F:X\longrightarrow Y</math> is ''linear'' if it is stable and furthemore satisfies: for any family <math>A</math> of pairwise compatible cliques of <math>X</math>, that is such that for any <math>x, y\in A</math>, <math>x\cup y\in X</math>, we have <math>\bigcup_{x\in A}F(x) = F(\bigcup A)</math>.
}}

In particular if we take <math>A</math> to be the empty family, then we have <math>F(\emptyset) = \emptyset</math>.

The condition for linearity is quite similar to the condition for Scott continuity, except that we dropped the constraint that <math>A</math> is ''directed''. Linearity is therefore much stronger than stability: most stable functions are not linear.

However most of the functions seen so far are linear. Typically the function <math>\pi_i:X_1\with X_2\longrightarrow X_i</math> is linear from wich one may deduce that the ''with'' construction is also a cartesian product in the category of coherent spaces and linear functions.

As with stable function we have an equivalent and much more tractable caracterisation of linear function:

{{Theorem|
Let <math>F:X\longrightarrow Y</math> be a continuous function. Then <math>F</math> is linear iff it satisfies: for any clique <math>x\in X</math> and any <math>b\in F(x)</math> there is a unique <math>a\in x</math> such that <math>b\in F(\{a\})</math>.
}}

Just as the caracterisation theorem for stable functions allowed us to build the coherent space of stable functions, this theorem will help us to endow the set of linear maps with a structure of coherent space.

{{Definition|title=The linear functions space|
Let <math>X</math> and <math>Y</math> be coherent spaces. The ''linear function space'' <math>X\limp Y</math> is defined by:
* <math>\web{X\limp Y} = \web X\times \web Y</math>,
* <math>(a,b)\coh_{X\limp Y}(a', b')</math> iff <math>\begin{cases}\text{if }a\coh_X a'\text{ then } b\coh_Y b'\\
\text{if }a\coh_X a' \text{ and }b=b'\text{ then }a=a'\end{cases}</math>
}}

Equivalently one could define the strict coherence to be: <math>(a,b)\scoh_{X\limp Y}(a',b')</math> iff <math>a\scoh_X a'</math> entails <math>b\scoh_Y b'</math>.

{{Definition|title=Linear trace|
Let <math>F:X\longrightarrow Y</math> be a function. The ''linear trace'' of <math>F</math> denoted as <math>\mathrm{LinTr}(F)</math> is the set:
<math>\mathrm{LinTr}(F) = \{(a, b)\in\web X\times\web Y</math> such that <math>b\in F(\{a\})\}</math>.
}}

{{Theorem|
If <math>F</math> is linear then <math>\mathrm{LinTr}(F)</math> is a clique of <math>X\limp Y</math>.
}}

{{Definition|title=Evaluation of linear function|
Let <math>f</math> be a clique of <math>X\limp Y</math>. We define the function <math>\mathrm{LinFun}\,f:X\longrightarrow Y</math> by: <math>\mathrm{LinFun}\,f(x) = \{b\in\web Y</math> such that there is an <math>a\in x</math> satisfying <math>(a,b)\in f\}</math>.
}}

{{Theorem|title=Linear closure|
Let <math>f</math> be a clique in <math>X\limp Y</math>. Then we have <math>\mathrm{LinTr}(\mathrm{LinFun}\, f) = f</math>. Conversely if <math>F:X\longrightarrow Y</math> is linear then we have <math>F = \mathrm{LinFun}\,\mathrm{LinTr}(F)</math>.
}}

It remains to define a tensor product and we will get that the category of coherent spaces with linear functions is monoidal symetric (it is actually *-autonomous).

=== Tensor product ===

{{Definition|title=Tensor product|
Let <math>X</math> and <math>Y</math> be coherent spaces. Their tensor product <math>X\tens Y</math> is defined by: <math>\web{X\tens Y} = \web X\times\web Y</math> and <math>(a,b)\coh_{X\tens Y}(a',b')</math> iff <math>a\coh_X a'</math> and <math>b\coh_Y b'</math>.
}}

{{Theorem|
The category of coherent spaces with linear maps and tensor product is [[Categorical semantics#Modeling IMLL|monoidal symetric closed]].
}}

The closedness is a consequence of the existence of the linear isomorphism:
<math>\varphi:X\tens Y\limp Z\ \stackrel{\sim}{\longrightarrow}\ X\limp(Y\limp Z)</math>

that is defined by its linear trace: <math>\mathrm{LinTr}(\varphi) = \{(((a, b), c), (a, (b, c))),\, a\in\web X,\, b\in \web Y,\, c\in\web Z\}</math>.

=== Linear negation ===

{{Definition|title=Linear negation|
Let <math>X</math> be a coherent space. We define the ''incoherence relation'' on <math>\web X</math> by: <math>a\incoh_X b</math> iff <math>a\coh_X b</math> entails <math>a=b</math>. The incoherence relation is reflexive and symetric; we call ''dual'' or ''linear negation'' of <math>X</math> the associated coherent space denoted <math>X\orth</math>, thus defined by: <math>\web{X\orth} = \web X</math> and <math>a\coh_{X\orth} b</math> iff <math>a\incoh_X b</math>.
}}

The cliques of <math>X\orth</math> are called the ''anticliques'' of <math>X</math>. As seen in the section on cliqued spaces we have <math>X\biorth=X</math>.

{{Theorem|
The category of coherent spaces with linear maps, tensor product and linear negation is *-autonomous.
}}

This is in particular consequence of the existence of the isomorphism:
<math>\varphi:X\limp Y\ \stackrel{\sim}{\longrightarrow}\ Y\orth\limp X\orth</math>

defined by its linear trace: <math>\mathrm{LinTr}(\varphi) = \{((a, b), (b, a)),\, a\in\web X,\, b\in\web Y\}</math>.

== Exponentials ==

In linear algebra, bilinear maps may be factorized through the tensor product. Similarly there is a coherent space <math>\oc X</math> that allows to factorize stable functions through linear functions.

{{Definition|title=Of course|
Let <math>X</math> be a coherent space; recall that <math>X_{\mathrm{fin}}</math> denotes the set of finite cliques of <math>X</math>. We define the space <math>\oc X</math> (read ''of course <math>X</math>'') by: <math>\web{\oc X} = X_{\mathrm{fin}}</math> and <math>x_0\coh_{\oc X}y_0</math> iff <math>x_0\cup y_0</math> is a clique of <math>X</math>.
}}

Thus a clique of <math>\oc X</math> is a set of finite cliques of <math>X</math> the union of wich is a clique of <math>X</math>.

{{Theorem|
Let <math>X</math> be a coherent space. Denote by <math>\beta:X\longrightarrow \oc X</math> the stable function whose trace is: <math>\mathrm{Tr}(\beta) = \{(x_0, x_0),\, x_0\in X_{\mathrm{fin}}\}</math>. Then for any coherent space <math>Y</math> and any stable function <math>F: X\longrightarrow Y</math> there is a unique ''linear'' function <math>\bar F:\oc X\longrightarrow Y</math> such that <math>F = \bar F\circ \beta</math>.

Furthermore we have <math>X\imp Y = \oc X\limp Y</math>.
}}

{{Theorem|title=The exponential isomorphism|
Let <math>X</math> and <math>Y</math> be two coherent spaces. Then there is a linear isomorphism:
<math>\varphi:\oc(X\with Y)\quad\stackrel{\sim}{\longrightarrow}\quad \oc X\tens\oc Y</math>.
}}

The iso <math>\varphi</math> is defined by its trace: <math>\mathrm{Tr}(\varphi) = \{(x_0, (\pi_1(x_0), \pi_2(x_0)), x_0\text{ finite clique of } X\with Y\}</math>.

This isomorphism, that sends an additive structure (the web of a with is obtained by disjoint union) onto a multiplicative one (the web of a tensor is obtained by cartesian product) is the reason why the of course is called an ''exponential''.

== Dual connectives and neutrals ==

By linear negation all the constructions defined so far (<math>\with, \tens, \oc</math>) have a dual.

=== The direct sum ===

The dual of <math>\with</math> is <math>\plus</math> defined by: <math>X\plus Y = (X\orth\with Y\orth)\orth</math>. An equivalent definition is given by: <math>\web{X\plus Y} = \web{X\with Y} = \{1\}\times \web X \cup \{2\}\times\web Y</math> and <math>(i, a)\coh_{X\plus Y} (j, b)\text{ iff } i = j = 1 \text{ and } a\coh_X b,\text{ or }i = j = 2\text{ and } a\coh_Y b</math>.

{{Theorem|
Let <math>x'</math> be a clique of <math>X\plus Y</math>; then <math>x'</math> is of the form <math>\{i\}\times x</math> where <math>i = 1\text{ and }x\in X</math>, or <math>i = 2\text{ and }x\in Y</math>.

Denote <math>\mathrm{inl}:X\longrightarrow X\plus Y</math> the function defined by <math>\mathrm{inl}(x) = \{1\}\times x</math> and by <math>\mathrm{inr}:Y\longrightarrow X\plus Y</math> the function defined by <math>\mathrm{inr}(x) = \{2\}\times x</math>. Then <math>\mathrm{inl}</math> and <math>\mathrm{inr}</math> are linear.

If <math>F:X\longrightarrow Z</math> and <math>G:Y\longrightarrow Z</math> are ''linear'' functions then the function <math>H:X\plus Y \longrightarrow Z</math> defined by <math>H(\mathrm{inl}(x)) = F(x)</math> and <math>H(\mathrm{inr}(y)) = G(y)</math> is linear.
}}

In other terms <math>X\plus Y</math> is the direct sum of <math>X</math> and <math>Y</math>. Note that in the theorem all functions are ''linear''. Things doesn't work so smoothly for stable functions. Historically it was after noting this defect of coherent semantics w.r.t. the intuitionnistic implication that Girard was leaded to discover linear functions.

=== The par and the why not ===

We now come to the most mysterious constructions of coherent semantics: the duals of the tensor and the of course.

The ''par'' is the dual of the tensor, thus defined by: <math>X\parr Y = (X\orth\tens Y\orth)\orth</math>. From this one can deduce the definition in graph terms: <math>\web{X\parr Y} = \web{X\tens Y} = \web X\times \web Y</math> and <math>(a,b)\scoh_{X\parr Y} (a',b')</math> iff <math>a\scoh_X a'</math> or <math>b\scoh_Y b'</math>. With this definition one sees that we have:

<math>X\limp Y = X\orth\parr Y</math>

for any coherent spaces <math>X</math> and <math>Y</math>. This equation can be seen as an alternative definition of the par: <math>X\parr Y = X\orth\limp Y</math>.

Similarly the dual of the of course is called ''why not'' defined by: <math>\wn X = (\oc X\orth)\orth</math>. From this we deduce the definition in the graph sense which is a bit tricky: <math>\web{\wn X}</math> is the set of finite anticliques of <math>X</math>, and given two finite anticliques <math>x</math> and <math>y</math> of <math>X</math> we have <math>x\scoh_{\wn X} y</math> iff there is <math>a\in x</math> and <math>b\in y</math> such that <math>a\scoh_X b</math>.

Note that both for the par and the why not it is much more convenient to define the strict coherence than the coherence.

With these two last constructions, the equation between the stable function space, the of course and the linear function space may be written:

<math>X\imp Y = \wn X\orth\parr Y</math>.

=== One and bottom ===

Depending on the context we denote by <math>\one</math> or <math>\bot</math> the coherent space whose web is a singleton and whose coherence relation is the trivial reflexive relation.

{{Theorem|
<math>\one</math> is neutral for tensor, that is, there is a linear isomorphism <math>\varphi:X\tens\one\ \stackrel{\sim}{\longrightarrow}\ X</math>.

Similarly <math>\bot</math> is neutral for par.
}}

=== Zero and top ===

Depending on the context we denote by <math>\zero</math> or <math>\top</math> the coherent space with empty web.

{{Theorem|
<math>\zero</math> is neutral for the direct sum <math>\plus</math>, <math>\top</math> is neutral for the cartesian product <math>\with</math>.
}}

{{Remark|
It is one of the main defect of coherent semantics w.r.t. linear logic that it identifies the neutrals: in coherent semantics <math>\zero = \top</math> and <math>\one = \bot</math>. However there is no known semantics of LL that solves this problem in a satisfactory way.}}

== The failure of coherent semantics ==

Coherent semantics was an important milestone in the modern theory of logic of programs. However it suffers from a number of defects the correction of which have motivated lots of work.

=== Sequentiality ===

Sequentiality is a property that we will not define here (it would diserve its own article). We rely on the intuition that a function of <math>n</math> arguments is sequential if one can determine which of these argument is examined first during the computation. Obviously any function implemented in a functionnal language is sequential; for example the function ''or'' defined à la CAML by:

<code>or = fun (x, y) -> if x then true else y</code>

examines its argument x first. Note that this may be expressed more abstractly by the property: <math>\mathrm{or}(\bot, x) = \bot</math> for any boolean <math>x</math>: the function ''or'' needs its first argument in order to compute anything. On the other hand we have <math>\mathrm{or}(\mathrm{true}, \bot) = \mathrm{true}</math>: in some case (when the first argument is true), the function doesn't need its second argument at all.

The typical non sequential function is the ''parallel or'' (that one cannot define in a CAML like language).

For a while one may have believed that the stability condition on which coherent semantics is built was enough to capture the notion of ''sequentiality'' of programs. A hint was the already mentionned fact that the ''parallel or'' is not stable. This diserves a bit of explanation.

==== The parallel or is not stable ====

Let <math>B</math> be the coherent space of booleans, also know as the flat domain of booleans: <math>\web B = \{tt, ff\}</math> where <math>tt</math> and <math>ff</math> are two arbitrary distinct objects (for example one may take <math>tt = 0</math> and <math>ff = 1</math>) and for any <math>b_1, b_2\in \web B</math>, define <math>b_1\coh_B b_2</math> iff <math>b_1 = b_2</math>. Then <math>B</math> has exactly three cliques: the empty clique that we shall denote <math>\bot</math>, the singleton <math>\{tt\}</math> that we shall denote <math>T</math> and the singleton <math>\{ff\}</math> that we shall denote <math>F</math>. These three cliques are ordered by inclusion: <math>\bot \leq T, F</math> (we use <math>\leq</math> for <math>\subset</math> to enforce the idea that coherent spaces are domains).

Recall the [[#Cartesian product|definition of the with]], and in particular that any clique of <math>B\with B</math> has the form <math>\langle x, y\rangle</math> where <math>x</math> and <math>y</math> are cliques of <math>B</math>. Thus <math>B\with B</math> has 9 cliques: <math>\langle\bot,\bot\rangle,\ \langle\bot, T\rangle,\ \langle\bot, F\rangle,\ \langle T,\bot\rangle,\ \dots</math> that are ordered by the product order: <math>\langle x,y\rangle\leq \langle x,y\rangle</math> iff <math>x\leq x'</math> and <math>y\leq y'</math>.

With these notations in mind one may define the parallel or by:

<math>
\begin{array}{rcl}
\mathrm{Por} : B\with B &\longrightarrow& B\\
\langle T,\bot\rangle &\longrightarrow& T\\
\langle \bot,T\rangle &\longrightarrow& T\\
\langle F, F\rangle &\longrightarrow& F
\end{array}
</math>

The function is completely determined if we add the assumption that it is non decreasing; for example one must have <math>\mathrm{Por}\langle\bot,\bot\rangle = \bot</math> because the lhs has to be less than both <math>T</math> and <math>F</math> (because <math>\langle\bot,\bot\rangle \leq \langle T,\bot\rangle</math> and <math>\langle\bot,\bot\rangle \leq \langle F,F\rangle</math>).

The function is not stable because <math>\langle T,\bot\rangle \cap \langle \bot, T\rangle = \langle\bot, \bot\rangle</math>, thus <math>\mathrm{Por}(\langle T,\bot\rangle \cap \langle \bot, T\rangle) = \bot</math> whereas <math>\mathrm{Por}\langle T,\bot\rangle \cap \mathrm{Por}\langle \bot, T\rangle = T\cap T = T</math>.

Another way to see this is: suppose <math>x</math> and <math>y</math> are two cliques of <math>B</math> such that <math>tt\in \mathrm{Por}\langle x, y\rangle</math>, which means that <math>\mathrm{Por}\langle x, y\rangle = T</math>; according to the [[#Stable functions|caracterisation theorem of stable functions]], if <math>\mathrm{Por}</math> were stable then there would be a unique minimum <math>x_0</math> included in <math>x</math>, and a unique minimum <math>y_0</math> included in <math>y</math> such that <math>\mathrm{Por}\langle x_0, y_0\rangle = T</math>. This is not the case because both <math>\langle T,\bot\rangle</math> and <math>\langle T,\bot\rangle</math> are minimal such that their value is <math>T</math>.

In other terms, knowing that <math>\mathrm{Por}\langle x, y\rangle = T</math> doesn't tell which of <math>x</math> of <math>y</math> is responsible for that, although we know by the definition of <math>\mathrm{Por}</math> that only one of them is. Indeed the <math>\mathrm{Por}</math> function is not representable in sequential programming languages such as (typed) lambda-calculus.

So the first genuine idea would be that stability caracterises sequentiality; but...

==== The Gustave function is stable ====

The Gustave function, so-called after an old joke, was found by Gérard Berry as an example of a function that is stable but non sequential. It is defined by:

<math>
\begin{array}{rcl}
B\with B\with B &\longrightarrow& B\\
\langle T, F, \bot\rangle &\longrightarrow& T\\
\langle \bot, T, F\rangle &\longrightarrow& T\\
\langle F, \bot, T\rangle &\longrightarrow& T\\
\langle x, y, z\rangle &\longrightarrow& F
\end{array}
</math>

The last clause is for all cliques <math>x</math>, <math>y</math> and <math>z</math> such that <math>\langle x, y ,z\rangle</math> is incompatible with the three cliques <math>\langle T, F, \bot\rangle</math>, <math>\langle \bot, T, F\rangle</math> and <math>\langle F, \bot, T\rangle</math>, that is such that the union with any of these three cliques is not a clique in <math>B\with B\with B</math>. We shall denote <math>x_1</math>, <math>x_2</math> and <math>x_3</math> these three cliques.

We furthemore assume that the Gustave function is non decreasing, so that we get <math>G\langle\bot,\bot,\bot\rangle = \bot</math>.

We note that <math>x_1</math>, <math>x_2</math> and <math>x_3</math> are pairwise incompatible. From this we can deduce that the Gustave function is stable: typically if <math>G\langle x,y,z\rangle = T</math> then exactly one of the <math>x_i</math>s is contained in <math>\langle x, y, z\rangle</math>.

However it is not sequential because there is no way to determine which of its three arguments is examined first: it is not the first one otherwise we would have <math>G\langle\bot, T, F\rangle = \bot</math> and similarly it is not the second one nor the third one.

In other terms there is no way to implement the Gustave function by a lambda-term (or in any sequential programming language). Thus coherent semantics is not complete w.r.t. lambda-calculus.

The research for a right model for sequentiality was the motivation for lot of
work, ''e.g.'', ''sequential algorithms'' by Gérard Bérry and Pierre-Louis
Currien in the early eighties, that were more recently reformulated as a kind
of [[Game semantics|game model]], and the theory of ''hypercoherent spaces'' by
Antonio Bucciarelli and Thomas Ehrhard.

=== Multiplicative neutrals and the mix rule ===

Coherent semantics is slightly degenerated w.r.t. linear logic because it identifies multiplicative neutrals (it also identifies additive neutrals but that's yet another problem): the coherent spaces <math>\one</math> and <math>\bot</math> are equal.

The first consequence of the identity <math>\one = \bot</math> is that the formula <math>\one\limp\bot</math> becomes provable, and so does the formula <math>\bot</math>. Note that this doesn't entail (as in classical logic or intuitionnistic logic) that linear logic is incoherent because the principle <math>\bot\limp A</math> for any formula <math>A</math> is still not provable.

The equality <math>\one = \bot</math> has also as consequence the fact that <math>\bot\limp\one</math> (or equivalently the formula <math>\one\parr\one</math>) is provable. This principle is also known as the [[Mix|mix rule]]

<math>
\AxRule{\vdash \Gamma}
\AxRule{\vdash \Delta}
\LabelRule{\rulename{mix}}
\BinRule{\vdash \Gamma,\Delta}
\DisplayProof
</math>

as it can be used to show that this rule is admissible:

<math>
\AxRule{\vdash\Gamma}
\LabelRule{\bot_R}
\UnaRule{\vdash\Gamma, \bot}
\AxRule{\vdash\Delta}
\LabelRule{\bot_R}
\UnaRule{\vdash\Delta, \bot}
\BinRule{\vdash \Gamma, \Delta, \bot\tens\bot}
\NulRule{\vdash \one\parr\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\Gamma,\Delta}
\DisplayProof
</math>

None of the two principles <math>1\limp\bot</math> and <math>\bot\limp\one</math> are valid in linear logic. To correct this one could extend the syntax of linear logic by adding the mix-rule. This is not very satisfactory as the mix rule violates some principles of [[Polarized Linear Logic]], typically the fact that as sequent of the form <math>\vdash P_1, P_2</math> where <math>P_1</math> and <math>P_2</math> are positive, is never provable.

On the other hand the mix-rule is valid in coherent semantics so one could try to find some other model that invalidates the mix-rule. For example Girard's Coherent Banach spaces were an attempt to address this issue.

== References ==
<references />

Categorical semantics

2011-10-03T23:29:22Z

Pierre-Marie Pédrot: /* Compact closed categories */

Constructing denotational models of linear can be a tedious work. Categorical semantics are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models.

TODO: why categories? how to extract categorical models? etc.

See <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Overview ==

In order to interpret the various [[fragment]]s of linear logic, we define incrementally what structure we need in a categorical setting.

* The most basic underlying structure are '''symmetric monoidal categories''' which model the symmetric tensor <math>\otimes</math> and its unit <math>1</math>.
* The <math>\otimes, \multimap</math> fragment ([[IMLL]]) is captured by so-called '''symmetric monoidal closed categories'''.
* Upgrading to [[ILL]], that is, adding the exponential <math>\oc</math> modality to IMLL requires modelling it categorically. There are various ways to do so: using rich enough '''adjunctions''', or with an ad-hoc definition of a well-behaved comonad which leads to '''linear categories''' and close relatives.
* Dealing with the additives <math>\with, \oplus</math> is quite easy, as they are plain '''cartesian product''' and '''coproduct''', usually defined through universal properties in category theory.
* Retrieving <math>\parr</math>, <math>\bot</math> and <math>\wn</math> is just a matter of dualizing <math>\otimes</math>, <math>1</math> and <math>\oc</math>, thus requiring the model to be a '''*-autonomous category''' for that purpose.

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> admits a right adjoint. The notion of ''right closed structure'' can be defined similarly.
}}

In a symmetric monoidal category, a left closed structure induces a right closed structure and conversely, allowing us to simply speak of a ''closed symmetric monoidal category''.

== Modeling the additives ==
{{Definition|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar@/^/[rr]^{(L,l)}&\bot&\ar@/^/[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
Suppose that we are given a symmetric monoidal closed category <math>(\mathcal{C},\tens,I)</math> and an object <math>R</math> of <math>\mathcal{C}</math>. For every object <math>A</math>, we define a morphism
:<math>\partial_{A}:A\to(A\limp R)\limp R</math>
as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism <math>\mathrm{id}_{A\limp R}:A\limp R \to A\limp R</math>, we get a morphism <math>A\tens (A\limp R)\to R</math>, and thus a morphism <math>(A\limp R)\tens A\to R</math> by precomposing with the symmetry <math>\gamma_{A\limp R,A}</math>. The morphism <math>\partial_A</math> is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. The object <math>R</math> is called ''dualizing'' when the morphism <math>\partial_A</math> is a bijection for every object <math>A</math> of <math>\mathcal{C}</math>. A symmetric monoidal closed category is ''*-autonomous'' when it admits such a dualizing object.
}}

=== Compact closed categories ===

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
and
:<math>
\xymatrix{
&(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\
I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\
B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\
}
</math>
commute. The object <math>A</math> is called a left dual of <math>B</math> (and conversely <math>B</math> is a right dual of <math>A</math>).
}}

{{Lemma|
Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic.
}}

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a right dual <math>A^*</math>. We write
:<math>\eta_A:I\to A^*\tens A</math> and <math>\varepsilon_A:A\tens A^*\to I</math>
for the corresponding duality morphisms.
}}

{{Lemma|
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.
}}

{{Property|
A compact closed category <math>\mathcal{C}</math> is monoidal closed, with closure defined by
:<math>\mathcal{C}(A\tens B,C)\cong\mathcal{C}(B,A^*\tens C)</math>
}}
{{Proof|
To every morphism <math>f:A\tens B\to C</math>, we associate a morphism <math>\ulcorner f\urcorner:B\to A^*\tens C</math> defined as
:<math>
\xymatrix{
B\ar[r]^-{\lambda_B^{-1}}&I\tens B\ar[r]^-{\eta_A\tens B}&(A^*\tens A)\tens B\ar[r]^-{\alpha_{A^*,A,B}}&A^*\tens(A\tens B)\ar[r]^-{A^*\tens f}&A\tens C\\
}
</math>
and to every morphism <math>g:B\to A^*\tens C</math>, we associate a morphism <math>\llcorner g\lrcorner:A\tens B\to C</math> defined as
:<math>
\xymatrix{
A\tens B\ar[r]^-{A\tens g}&A\tens(A^*\tens C)\ar[r]^-{\alpha_{A,A^*,C}^{-1}}&(A\tens A^*)\tens C\ar[r]^-{\varepsilon_A\tens C}&I\tens C\ar[r]^-{\lambda_C}&C
}
</math>
It is easy to show that <math>\llcorner \ulcorner f\urcorner\lrcorner=f</math> and <math>\ulcorner\llcorner g\lrcorner\urcorner=g</math> from which we deduce the required bijection.
}}

{{Property|
A compact closed category is a (degenerated) *-autonomous category, with the obvious duality structure. In particular, <math>(A \otimes B)^* \cong A^*\otimes B^*</math>.
}}

{{Remark|The above isomorphism does not hold in *-autonomous categories in general. This means that models which are compact closed categories identify <math>\otimes</math> and <math>\parr</math> as well as <math>1</math> and <math>\bot</math>.}}

{{Proof|
The dualizing object <math>R</math> is simply <math>I^*</math>.

For any <math>A</math>, the reverse isomorphism <math>\delta_A : (A \multimap R)\multimap R \rightarrow A</math> is constructed as follows:

<math>\mathcal{C}((A \multimap R)\multimap R, A) := \mathcal{C}((A \otimes I^{**})\otimes I^{**}, A) \cong \mathcal{C}((A \otimes I)\otimes I, A) \cong \mathcal{C}(A, A)</math>

Identity on <math>A</math> is taken as the canonical morphism required.

}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2011-10-03T23:26:17Z

Pierre-Marie Pédrot: /* Compact closed categories */

Constructing denotational models of linear can be a tedious work. Categorical semantics are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models.

TODO: why categories? how to extract categorical models? etc.

See <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Overview ==

In order to interpret the various [[fragment]]s of linear logic, we define incrementally what structure we need in a categorical setting.

* The most basic underlying structure are '''symmetric monoidal categories''' which model the symmetric tensor <math>\otimes</math> and its unit <math>1</math>.
* The <math>\otimes, \multimap</math> fragment ([[IMLL]]) is captured by so-called '''symmetric monoidal closed categories'''.
* Upgrading to [[ILL]], that is, adding the exponential <math>\oc</math> modality to IMLL requires modelling it categorically. There are various ways to do so: using rich enough '''adjunctions''', or with an ad-hoc definition of a well-behaved comonad which leads to '''linear categories''' and close relatives.
* Dealing with the additives <math>\with, \oplus</math> is quite easy, as they are plain '''cartesian product''' and '''coproduct''', usually defined through universal properties in category theory.
* Retrieving <math>\parr</math>, <math>\bot</math> and <math>\wn</math> is just a matter of dualizing <math>\otimes</math>, <math>1</math> and <math>\oc</math>, thus requiring the model to be a '''*-autonomous category''' for that purpose.

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> admits a right adjoint. The notion of ''right closed structure'' can be defined similarly.
}}

In a symmetric monoidal category, a left closed structure induces a right closed structure and conversely, allowing us to simply speak of a ''closed symmetric monoidal category''.

== Modeling the additives ==
{{Definition|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar@/^/[rr]^{(L,l)}&\bot&\ar@/^/[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
Suppose that we are given a symmetric monoidal closed category <math>(\mathcal{C},\tens,I)</math> and an object <math>R</math> of <math>\mathcal{C}</math>. For every object <math>A</math>, we define a morphism
:<math>\partial_{A}:A\to(A\limp R)\limp R</math>
as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism <math>\mathrm{id}_{A\limp R}:A\limp R \to A\limp R</math>, we get a morphism <math>A\tens (A\limp R)\to R</math>, and thus a morphism <math>(A\limp R)\tens A\to R</math> by precomposing with the symmetry <math>\gamma_{A\limp R,A}</math>. The morphism <math>\partial_A</math> is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. The object <math>R</math> is called ''dualizing'' when the morphism <math>\partial_A</math> is a bijection for every object <math>A</math> of <math>\mathcal{C}</math>. A symmetric monoidal closed category is ''*-autonomous'' when it admits such a dualizing object.
}}

=== Compact closed categories ===

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
and
:<math>
\xymatrix{
&(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\
I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\
B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\
}
</math>
commute. The object <math>A</math> is called a left dual of <math>B</math> (and conversely <math>B</math> is a right dual of <math>A</math>).
}}

{{Lemma|
Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic.
}}

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a right dual <math>A^*</math>. We write
:<math>\eta_A:I\to A^*\tens A</math> and <math>\varepsilon_A:A\tens A^*\to I</math>
for the corresponding duality morphisms.
}}

{{Lemma|
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.
}}

{{Property|
A compact closed category <math>\mathcal{C}</math> is monoidal closed, with closure defined by
:<math>\mathcal{C}(A\tens B,C)\cong\mathcal{C}(B,A^*\tens C)</math>
}}
{{Proof|
To every morphism <math>f:A\tens B\to C</math>, we associate a morphism <math>\ulcorner f\urcorner:B\to A^*\tens C</math> defined as
:<math>
\xymatrix{
B\ar[r]^-{\lambda_B^{-1}}&I\tens B\ar[r]^-{\eta_A\tens B}&(A^*\tens A)\tens B\ar[r]^-{\alpha_{A^*,A,B}}&A^*\tens(A\tens B)\ar[r]^-{A^*\tens f}&A\tens C\\
}
</math>
and to every morphism <math>g:B\to A^*\tens C</math>, we associate a morphism <math>\llcorner g\lrcorner:A\tens B\to C</math> defined as
:<math>
\xymatrix{
A\tens B\ar[r]^-{A\tens g}&A\tens(A^*\tens C)\ar[r]^-{\alpha_{A,A^*,C}^{-1}}&(A\tens A^*)\tens C\ar[r]^-{\varepsilon_A\tens C}&I\tens C\ar[r]^-{\lambda_C}&C
}
</math>
It is easy to show that <math>\llcorner \ulcorner f\urcorner\lrcorner=f</math> and <math>\ulcorner\llcorner g\lrcorner\urcorner=g</math> from which we deduce the required bijection.
}}

{{Property|
A compact closed category is a (degenerated) *-autonomous category, with the obvious duality structure. In particular, <math>(A \otimes B)^* \cong A^*\otimes B^*</math>.
}}

{{Remark|The above isomorphism does not hold in *-autonomous categories in general.}}

{{Proof|
The dualizing object <math>R</math> is simply <math>I^*</math>.

For any <math>A</math>, the reverse isomorphism <math>\delta_A : (A \multimap R)\multimap R \rightarrow A</math> is constructed as follows:

<math>\mathcal{C}((A \multimap R)\multimap R, A) := \mathcal{C}((A \otimes I^{**})\otimes I^{**}, A) \cong \mathcal{C}((A \otimes I)\otimes I, A) \cong \mathcal{C}(A, A)</math>

Identity on <math>A</math> is taken as the canonical morphism required.

}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2011-10-03T23:06:01Z

Pierre-Marie Pédrot: introductory paragraph

Constructing denotational models of linear can be a tedious work. Categorical semantics are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models.

TODO: why categories? how to extract categorical models? etc.

See <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Overview ==

In order to interpret the various [[fragment]]s of linear logic, we define incrementally what structure we need in a categorical setting.

* The most basic underlying structure are '''symmetric monoidal categories''' which model the symmetric tensor <math>\otimes</math> and its unit <math>1</math>.
* The <math>\otimes, \multimap</math> fragment ([[IMLL]]) is captured by so-called '''symmetric monoidal closed categories'''.
* Upgrading to [[ILL]], that is, adding the exponential <math>\oc</math> modality to IMLL requires modelling it categorically. There are various ways to do so: using rich enough '''adjunctions''', or with an ad-hoc definition of a well-behaved comonad which leads to '''linear categories''' and close relatives.
* Dealing with the additives <math>\with, \oplus</math> is quite easy, as they are plain '''cartesian product''' and '''coproduct''', usually defined through universal properties in category theory.
* Retrieving <math>\parr</math>, <math>\bot</math> and <math>\wn</math> is just a matter of dualizing <math>\otimes</math>, <math>1</math> and <math>\oc</math>, thus requiring the model to be a '''*-autonomous category''' for that purpose.

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> admits a right adjoint. The notion of ''right closed structure'' can be defined similarly.
}}

In a symmetric monoidal category, a left closed structure induces a right closed structure and conversely, allowing us to simply speak of a ''closed symmetric monoidal category''.

== Modeling the additives ==
{{Definition|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar@/^/[rr]^{(L,l)}&\bot&\ar@/^/[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
Suppose that we are given a symmetric monoidal closed category <math>(\mathcal{C},\tens,I)</math> and an object <math>R</math> of <math>\mathcal{C}</math>. For every object <math>A</math>, we define a morphism
:<math>\partial_{A}:A\to(A\limp R)\limp R</math>
as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism <math>\mathrm{id}_{A\limp R}:A\limp R \to A\limp R</math>, we get a morphism <math>A\tens (A\limp R)\to R</math>, and thus a morphism <math>(A\limp R)\tens A\to R</math> by precomposing with the symmetry <math>\gamma_{A\limp R,A}</math>. The morphism <math>\partial_A</math> is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. The object <math>R</math> is called ''dualizing'' when the morphism <math>\partial_A</math> is a bijection for every object <math>A</math> of <math>\mathcal{C}</math>. A symmetric monoidal closed category is ''*-autonomous'' when it admits such a dualizing object.
}}

=== Compact closed categories ===

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
and
:<math>
\xymatrix{
&(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\
I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\
B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\
}
</math>
commute. The object <math>A</math> is called a left dual of <math>B</math> (and conversely <math>B</math> is a right dual of <math>A</math>).
}}

{{Lemma|
Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic.
}}

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a right dual <math>A^*</math>. We write
:<math>\eta_A:I\to A^*\tens A</math> and <math>\varepsilon_A:A\tens A^*\to I</math>
for the corresponding duality morphisms.
}}

{{Lemma|
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.
}}

{{Property|
A compact closed category <math>\mathcal{C}</math> is monoidal closed, with closure defined by
:<math>\mathcal{C}(A\tens B,C)\cong\mathcal{C}(B,A^*\tens C)</math>
}}
{{Proof|
To every morphism <math>f:A\tens B\to C</math>, we associate a morphism <math>\ulcorner f\urcorner:B\to A^*\tens C</math> defined as
:<math>
\xymatrix{
B\ar[r]^-{\lambda_B^{-1}}&I\tens B\ar[r]^-{\eta_A\tens B}&(A^*\tens A)\tens B\ar[r]^-{\alpha_{A^*,A,B}}&A^*\tens(A\tens B)\ar[r]^-{A^*\tens f}&A\tens C\\
}
</math>
and to every morphism <math>g:B\to A^*\tens C</math>, we associate a morphism <math>\llcorner g\lrcorner:A\tens B\to C</math> defined as
:<math>
\xymatrix{
A\tens B\ar[r]^-{A\tens g}&A\tens(A^*\tens C)\ar[r]^-{\alpha_{A,A^*,C}^{-1}}&(A\tens A^*)\tens C\ar[r]^-{\varepsilon_A\tens C}&I\tens C\ar[r]^-{\lambda_C}&C
}
</math>
It is easy to show that <math>\llcorner \ulcorner f\urcorner\lrcorner=f</math> and <math>\ulcorner\llcorner g\lrcorner\urcorner=g</math> from which we deduce the required bijection.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Coherent semantics

2011-09-30T14:51:35Z

Pierre-Marie Pédrot: replaced paragraph with a link

''Coherent semantics'' was invented by Girard in the paper ''The system F, 15 years later''<ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=The System F of Variable Types, Fifteen Years Later|journal=Theoretical Computer Science|volume=45|issue=2|pages=159-192|doi=10.1016/0304-3975(86)90044-7|year=1986}}</ref>with the objective of building a denotationnal interpretation of second order intuitionnistic logic (aka polymorphic lambda-calculus).

Coherent semantics is based on the notion of ''stable functions'' that was initially proposed by Gérard Berry. Stability is a condition on Scott continuous functions that expresses the determinism of the relation between the output and the input: the typical Scott continuous but non stable function is the ''parallel or'' because when the two inputs are both set to '''true''', only one of them is the reason why the result is '''true''' but there is no way to determine which one.

A further achievement of coherent semantics was that it allowed to endow the set of stable functions from <math>X</math> to <math>Y</math> with a structure of domain, thus closing the category of coherent spaces and stable functions. However the most interesting point was the discovery of a special class of stable functions, ''linear functions'', which was the first step leading to Linear Logic.

== The cartesian closed structure of coherent semantics ==

There are three equivalent definitions of coherent spaces: the first one, ''coherent spaces as domains'', is interesting from a historical point of view as it emphazises the fact that coherent spaces are particular cases of Scott domains. The second one, ''coherent spaces as graphs'', is the most commonly used and will be our "official" definition in the sequel. The last one, ''cliqued spaces'' is a particular example of a more general scheme that one could call "symmetric reducibility"; this scheme is underlying lots of constructions in linear logic such as [[phase semantics]] or the proof of strong normalisation for proof-nets.

=== Coherent spaces ===

A coherent space <math>X</math> is a collection of subsets of a set <math>\web X</math> satisfying some conditions that will be detailed shortly. The elements of <math>X</math> are called the ''cliques'' of <math>X</math> (for reasons that will be made clear in a few lines). The set <math>\web X</math> is called the ''web'' of <math>X</math> and its elements are called the ''points'' of <math>X</math>; thus a clique is a set of points. Note that the terminology is a bit ambiguous as the points of <math>X</math> are the elements of the web of <math>X</math>, not the elements of <math>X</math>.

The definitions below give three equivalent conditions that have to be satisfied by the cliques of a coherent space.

==== As domains ====

The cliques of <math>X</math> have to satisfy:
* subset closure: if <math>x\subset y\in X</math> then <math>x\in X</math>,
* singletons: <math>\{a\}\in X</math> for <math>a\in\web X</math>.
* binary compatibility: if <math>A</math> is a family of pairwise compatible cliques of <math>X</math>, that is if <math>x\cup y\in X</math> for any <math>x,y\in A</math>, then <math>\bigcup A\in X</math>.

A coherent space is thus ordered by inclusion; one easily checks that it is a domain. In particular finite cliques of <math>X</math> correspond to compact elements.

==== As graphs ====

There is a reflexive and symetric relation <math>\coh_X</math> on <math>\web X</math> (the ''coherence relation'') such that any subset <math>x</math> of <math>\web X</math> is a clique of <math>X</math> iff <math>\forall a,b\in x,\, a\coh_X b</math>. In other terms <math>X</math> is the set of complete subgraphs of the simple unoriented graph of the <math>\coh_X</math> relation; this is the reason why elements of <math>X</math> are called ''cliques''.

The ''strict coherence relation'' <math>\scoh_X</math> on <math>X</math> is defined by: <math>a\scoh_X b</math> iff <math>a\neq b</math> and <math>a\coh_X b</math>.

A coherent space in the domain sense is seen to be a coherent space in the graph sense by setting <math>a\coh_X b</math> iff <math>\{a,b\}\in X</math>; conversely one can check that cliques in the graph sense are subset closed and satisfy the binary compatibility condition.

A coherent space is completely determined by its web and its coherence relation, or equivalently by its web and its strict coherence.

==== As cliqued spaces ====

{{Definition|title=Duality|
Let <math>x, y\subseteq \web{X}</math> be two sets. We will say that they are dual, written <math>x\perp y</math> if their intersection contains at most one element: <math>\mathrm{Card}(x\cap y)\leq 1</math>. As usual, it defines an [[orthogonality relation]] over <math>\powerset{\web{X}}</math>.}}

The last way to express the conditions on the cliques of a coherent space <math>X</math> is simply to say that we must have <math>X\biorth = X</math>.

==== Equivalence of definitions ====

Let <math>X</math> be a cliqued space and define a relation on <math>\web X</math> by setting <math>a\coh_X b</math> iff there is <math>x\in X</math> such that <math>a, b\in x</math>. This relation is obviously symetric; it is also reflexive because all singletons belong to <math>X</math>: if <math>a\in \web X</math> then <math>\{a\}</math> is dual to any element of <math>X\orth</math> (actually <math>\{a\}</math> is dual to any subset of <math>\web X</math>), thus <math>\{a\}</math> is in <math>X\biorth</math>, thus in <math>X</math>.

Let <math>a\coh_X b</math>. Then <math>\{a,b\}\in X</math>; indeed there is an <math>x\in X</math> such that <math>a, b\in x</math>. This <math>x</math> is dual to any <math>y\in X\orth</math>, that is meets any <math>y\in X\orth</math> in a most one point. Since <math>\{a,b\}\subset x</math> this is also true of <math>\{a,b\}</math>, so that <math>\{a,b\}</math> is in <math>X\biorth</math> thus in <math>X</math>.

Now let <math>x</math> be a clique for <math>\coh_X</math> and <math>y</math> be an element of <math>X\orth</math>. Suppose <math>a, b\in x\cap y</math>, then since <math>a</math> and <math>b</math> are coherent (by hypothesis on <math>x</math>) we have <math>\{a,b\}\in X</math> and since <math>y\in X\orth</math> we must have that <math>\{a,b\}</math> and <math>y</math> meet in at most one point. Thus <math>a = b</math> and we have shown that <math>x</math> and <math>y</math> are dual. Since <math>y</math> was arbitrary this means that <math>x</math> is in <math>X\biorth</math>, thus in <math>X</math>. Finally we get that any set of pairwise coherent points of <math>X</math> is in <math>X</math>. Conversely given <math>x\in X</math> its points are obviously pairwise coherent so eventually we get that <math>X</math> is a coherent space in the graph sense.

Conversely given a coherent space <math>X</math> in the graph sense, one can check that it is a cliqued space. Call ''anticlique'' a set <math>y\subset \web X</math> of pairwise incoherent points: for all <math>a, b</math> in <math>y</math>, if <math>a\coh_X b</math> then <math>a=b</math>. Any anticlique intersects any clique in at most one point: let <math>x</math> be a clique and <math>y</math> be an anticlique, then if <math>a,b\in x\cap y</math>, since <math>a, b\in x</math> we have <math>a\coh_X b</math> and since <math>y</math> is an anticlique we have <math>a = b</math>. Thus <math>y\in X\orth</math>. Conversely given any <math>y\in X\orth</math> and <math>a, b\in y</math>, suppose <math>a\coh_X b</math>. Then <math>\{a,b\}\in X</math>, thus <math>\{a,b\}\perp y</math> which entails that <math>\{a, b\}</math> has at most one point so that <math>a = b</math>: we have shown that any two elements of <math>y</math> are incoherent.

Thus the collection of anticliques of <math>X</math> is the dual <math>X\orth</math> of <math>X</math>. Note that the incoherence relation defined above is reflexive and symetric, so that <math>X\orth</math> is a coherent space in the graph sense. Thus we can do for <math>X\orth</math> exactly what we've just done for <math>X</math> and consider the anti-anticliques, that is the anticliques for the incoherent relation which are the cliques for the in-incoherent relation. It is not difficult to see that this in-incoherence relation is just the coherence relation we started with; we thus obtain that <math>X\biorth = X</math>, so that <math>X</math> is a cliqued space.

=== Stable functions ===

{{Definition|title=Stable function|
Let <math>X</math> and <math>Y</math> be two coherent spaces. A function <math>F:X\longrightarrow Y</math> is ''stable'' if it satisfies:
* it is non decreasing: for any <math>x,y\in X</math> if <math>x\subset y</math> then <math>F(x)\subset F(y)</math>;
* it is continuous (in the Scott sense): if <math>A</math> is a directed family of cliques of <math>X</math>, that is if for any <math>x,y\in A</math> there is a <math>z\in A</math> such that <math>x\cup y\subset z</math>, then <math>\bigcup_{x\in A}F(x) = F(\bigcup A)</math>;
* it satisfies the stability condition: if <math>x,y\in X</math> are compatible, that is if <math>x\cup y\in X</math>, then <math>F(x\cap y) = F(x)\cap F(y)</math>.
}}

This definition is admitedly not very tractable. An equivalent and most useful caracterisation of stable functions is given by the following theorem.

{{Theorem|
Let <math>F:X\longrightarrow Y</math> be a non-decreasing function from the coherent space <math>X</math> to the coherent space <math>Y</math>. The function <math>F</math> is stable iff it satisfies: for any <math>x\in X</math>, <math>b\in\web Y</math>, if <math>b\in F(x)</math> then there is a finite clique <math>x_0\subset x</math> such that:
* <math>b\in F(x_0)</math>,
* for any <math>y\subset x</math> if <math>b\in F(y)</math> then <math>x_0\subset y</math> (<math>x_0</math> is ''the'' minimum sub-clique of <math>x</math> such that <math>b\in F(x_0)</math>).
}}

Note that the stability condition doesn't depend on the coherent space structure and can be expressed more generally for continuous functions on domains. However, as mentionned in the introduction, the restriction to coherent spaces allows to endow the set of stable functions from <math>X</math> to <math>Y</math> with a structure of coherent space.

{{Definition|title=The space of stable functions|
Let <math>X</math> and <math>Y</math> be coherent spaces. We denote by <math>X_{\mathrm{fin}}</math> the set of ''finite'' cliques of <math>X</math>. The function space <math>X\imp Y</math> is defined by:
* <math>\web{X\imp Y} = X_{\mathrm{fin}}\times \web Y</math>,
* <math>(x_0, a)\coh_{X\imp Y}(y_0, b)</math> iff <math>\begin{cases}\text{if } x_0\cup y_0\in X\text{ then } a\coh_Y b,\\
\text{if } x_0\cup y_0\in X\text{ and } a = b\text{ then } x_0 = y_0\end{cases}</math>.
}}

One could equivalently define the strict coherence relation on <math>X\imp Y</math> by: <math>(x_0,a)\scoh_{X\imp Y}(y_0, b)</math> iff when <math>x_0\cup y_0\in X</math> then <math>a\scoh_Y b</math> (equivalently <math>x_0\cup y_0\not\in X</math> or <math>a\scoh_Y b</math>).

{{Definition|title=Trace of a stable function|
Let <math>F:X\longrightarrow Y</math> be a function. The ''trace'' of <math>F</math> is the set:

<math>\mathrm{Tr}(F) = \{(x_0, b), x_0\text{ minimal such that } b\in F(x_0)\}</math>.
}}

{{theorem|
<math>F</math> is stable iff <math>\mathrm{Tr}(F)</math> is a clique of the function space <math>X\imp Y</math>
}}

In particular the continuity of <math>F</math> entails that if <math>x_0</math> is minimal such that <math>b\in F(x_0)</math>, then <math>x_0</math> is finite.

{{Definition|title=The evaluation function|
Let <math>f</math> be a clique in <math>X\imp Y</math>. We define a function <math>\mathrm{Fun}\,f:X\longrightarrow Y</math> by: <math>\mathrm{Fun}\,f(x) = \{b\in Y,\text{ there is }x_0\subset x\text{ such that }(x_0, b)\in f\}</math>.
}}

{{Theorem|title=Closure|
If <math>f</math> is a clique of the function space <math>X\imp Y</math> then we have <math>\mathrm{Tr}(\mathrm{Fun}\,f) = f</math>. Conversely if <math>F:X\longrightarrow Y</math> is a stable function then we have <math>F = \mathrm{Fun}\,\mathrm{Tr}(F)</math>.
}}

=== Cartesian product ===

{{Definition|title=Cartesian product|
Let <math>X_1</math> and <math>X_2</math> be two coherent spaces. We define the coherent space <math>X_1\with X_2</math> (read <math>X_1</math> ''with'' <math>X_2</math>):
* the web is the disjoint union of the webs: <math>\web{X_1\with X_2} = \{1\}\times\web{X_1}\cup \{2\}\times\web{X_2}</math>;
* the coherence relation is the serie composition of the relations on <math>X_1</math> and <math>X_2</math>: <math>(i, a)\coh_{X_1\with X_2}(j, b)</math> iff either <math>i\neq j</math> or <math>i=j</math> and <math>a\coh_{X_i} b</math>.
}}

This definition is just the way to put a coherent space structure on the cartesian product. Indeed one easily shows the

{{Theorem|
Given cliques <math>x_1</math> and <math>x_2</math> in <math>X_1</math> and <math>X_2</math>, we define the subset <math>\langle x_1, x_2\rangle</math> of <math>\web{X_1\with X_2}</math> by: <math>\langle x_1, x_2\rangle = \{1\}\times x_1\cup \{2\}\times x_2</math>. Then <math>\langle x_1, x_2\rangle</math> is a clique in <math>X_1\with X_2</math>.

Conversely, given a clique <math>x\in X_1\with X_2</math>, for <math>i=1,2</math> we define <math>\pi_i(x) = \{a\in X_i, (i, a)\in x\}</math>. Then <math>\pi_i(x)</math> is a clique in <math>X_i</math> and the function <math>\pi_i:X_1\with X_2\longrightarrow X_i</math> is stable.

Furthemore these two operations are inverse of each other: <math>\pi_i(\langle x_1, x_2\rangle) = x_i</math> and <math>\langle\pi_1(x), \pi_2(x)\rangle = x</math>. In particular any clique in <math>X_1\with X_2</math> is of the form <math>\langle x_1, x_2\rangle</math>.
}}

Altogether the results above (and a few other more that we shall leave to the reader) allow to get:

{{Theorem|
The category of coherent spaces and stable functions is cartesian closed.
}}

In particular this means that if we define <math>\mathrm{Eval}:(X\imp Y)\with X\longrightarrow Y</math> by: <math>\mathrm{Eval}(\langle f, x\rangle) = \mathrm{Fun}\,f(x)</math> then <math>\mathrm{Eval}</math> is stable.

== The monoidal structure of coherent semantics ==

=== Linear functions ===

{{Definition|title=Linear function|
A function <math>F:X\longrightarrow Y</math> is ''linear'' if it is stable and furthemore satisfies: for any family <math>A</math> of pairwise compatible cliques of <math>X</math>, that is such that for any <math>x, y\in A</math>, <math>x\cup y\in X</math>, we have <math>\bigcup_{x\in A}F(x) = F(\bigcup A)</math>.
}}

In particular if we take <math>A</math> to be the empty family, then we have <math>F(\emptyset) = \emptyset</math>.

The condition for linearity is quite similar to the condition for Scott continuity, except that we dropped the constraint that <math>A</math> is ''directed''. Linearity is therefore much stronger than stability: most stable functions are not linear.

However most of the functions seen so far are linear. Typically the function <math>\pi_i:X_1\with X_2\longrightarrow X_i</math> is linear from wich one may deduce that the ''with'' construction is also a cartesian product in the category of coherent spaces and linear functions.

As with stable function we have an equivalent and much more tractable caracterisation of linear function:

{{Theorem|
Let <math>F:X\longrightarrow Y</math> be a continuous function. Then <math>F</math> is linear iff it satisfies: for any clique <math>x\in X</math> and any <math>b\in F(x)</math> there is a unique <math>a\in x</math> such that <math>b\in F(\{a\})</math>.
}}

Just as the caracterisation theorem for stable functions allowed us to build the coherent space of stable functions, this theorem will help us to endow the set of linear maps with a structure of coherent space.

{{Definition|title=The linear functions space|
Let <math>X</math> and <math>Y</math> be coherent spaces. The ''linear function space'' <math>X\limp Y</math> is defined by:
* <math>\web{X\limp Y} = \web X\times \web Y</math>,
* <math>(a,b)\coh_{X\limp Y}(a', b')</math> iff <math>\begin{cases}\text{if }a\coh_X a'\text{ then } b\coh_Y b'\\
\text{if }a\coh_X a' \text{ and }b=b'\text{ then }a=a'\end{cases}</math>
}}

Equivalently one could define the strict coherence to be: <math>(a,b)\scoh_{X\limp Y}(a',b')</math> iff <math>a\scoh_X a'</math> entails <math>b\scoh_Y b'</math>.

{{Definition|title=Linear trace|
Let <math>F:X\longrightarrow Y</math> be a function. The ''linear trace'' of <math>F</math> denoted as <math>\mathrm{LinTr}(F)</math> is the set:
<math>\mathrm{LinTr}(F) = \{(a, b)\in\web X\times\web Y</math> such that <math>b\in F(\{a\})\}</math>.
}}

{{Theorem|
If <math>F</math> is linear then <math>\mathrm{LinTr}(F)</math> is a clique of <math>X\limp Y</math>.
}}

{{Definition|title=Evaluation of linear function|
Let <math>f</math> be a clique of <math>X\limp Y</math>. We define the function <math>\mathrm{LinFun}\,f:X\longrightarrow Y</math> by: <math>\mathrm{LinFun}\,f(x) = \{b\in\web Y</math> such that there is an <math>a\in x</math> satisfying <math>(a,b)\in f\}</math>.
}}

{{Theorem|title=Linear closure|
Let <math>f</math> be a clique in <math>X\limp Y</math>. Then we have <math>\mathrm{LinTr}(\mathrm{LinFun}\, f) = f</math>. Conversely if <math>F:X\longrightarrow Y</math> is linear then we have <math>F = \mathrm{LinFun}\,\mathrm{LinTr}(F)</math>.
}}

It remains to define a tensor product and we will get that the category of coherent spaces with linear functions is monoidal symetric (it is actually *-autonomous).

=== Tensor product ===

{{Definition|title=Tensor product|
Let <math>X</math> and <math>Y</math> be coherent spaces. Their tensor product <math>X\tens Y</math> is defined by: <math>\web{X\tens Y} = \web X\times\web Y</math> and <math>(a,b)\coh_{X\tens Y}(a',b')</math> iff <math>a\coh_X a'</math> and <math>b\coh_Y b'</math>.
}}

{{Theorem|
The category of coherent spaces with linear maps and tensor product is [[Categorical semantics#Modeling IMLL|monoidal symetric closed]].
}}

The closedness is a consequence of the existence of the linear isomorphism:
<math>\varphi:X\tens Y\limp Z\ \stackrel{\sim}{\longrightarrow}\ X\limp(Y\limp Z)</math>

that is defined by its linear trace: <math>\mathrm{LinTr}(\varphi) = \{(((a, b), c), (a, (b, c))),\, a\in\web X,\, b\in \web Y,\, c\in\web Z\}</math>.

=== Linear negation ===

{{Definition|title=Linear negation|
Let <math>X</math> be a coherent space. We define the ''incoherence relation'' on <math>\web X</math> by: <math>a\incoh_X b</math> iff <math>a\coh_X b</math> entails <math>a=b</math>. The incoherence relation is reflexive and symetric; we call ''dual'' or ''linear negation'' of <math>X</math> the associated coherent space denoted <math>X\orth</math>, thus defined by: <math>\web{X\orth} = \web X</math> and <math>a\coh_{X\orth} b</math> iff <math>a\incoh_X b</math>.
}}

The cliques of <math>X\orth</math> are called the ''anticliques'' of <math>X</math>. As seen in the section on cliqued spaces we have <math>X\biorth=X</math>.

{{Theorem|
The category of coherent spaces with linear maps, tensor product and linear negation is *-autonomous.
}}

This is in particular consequence of the existence of the isomorphism:
<math>\varphi:X\limp Y\ \stackrel{\sim}{\longrightarrow}\ Y\orth\limp X\orth</math>

defined by its linear trace: <math>\mathrm{LinTr}(\varphi) = \{((a, b), (b, a)),\, a\in\web X,\, b\in\web Y\}</math>.

== Exponentials ==

In linear algebra, bilinear maps may be factorized through the tensor product. Similarly there is a coherent space <math>\oc X</math> that allows to factorize stable functions through linear functions.

{{Definition|title=Of course|
Let <math>X</math> be a coherent space; recall that <math>X_{\mathrm{fin}}</math> denotes the set of finite cliques of <math>X</math>. We define the space <math>\oc X</math> (read ''of course <math>X</math>'') by: <math>\web{\oc X} = X_{\mathrm{fin}}</math> and <math>x_0\coh_{\oc X}y_0</math> iff <math>x_0\cup y_0</math> is a clique of <math>X</math>.
}}

Thus a clique of <math>\oc X</math> is a set of finite cliques of <math>X</math> the union of wich is a clique of <math>X</math>.

{{Theorem|
Let <math>X</math> be a coherent space. Denote by <math>\beta:X\longrightarrow \oc X</math> the stable function whose trace is: <math>\mathrm{Tr}(\beta) = \{(x_0, x_0),\, x_0\in X_{\mathrm{fin}}\}</math>. Then for any coherent space <math>Y</math> and any stable function <math>F: X\longrightarrow Y</math> there is a unique ''linear'' function <math>\bar F:\oc X\longrightarrow Y</math> such that <math>F = \bar F\circ \beta</math>.

Furthermore we have <math>X\imp Y = \oc X\limp Y</math>.
}}

{{Theorem|title=The exponential isomorphism|
Let <math>X</math> and <math>Y</math> be two coherent spaces. Then there is a linear isomorphism:
<math>\varphi:\oc(X\with Y)\quad\stackrel{\sim}{\longrightarrow}\quad \oc X\tens\oc Y</math>.
}}

The iso <math>\varphi</math> is defined by its trace: <math>\mathrm{Tr}(\varphi) = \{(x_0, (\pi_1(x_0), \pi_2(x_0)), x_0\text{ finite clique of } X\with Y\}</math>.

This isomorphism, that sends an additive structure (the web of a with is obtained by disjoint union) onto a multiplicative one (the web of a tensor is obtained by cartesian product) is the reason why the of course is called an ''exponential''.

== Dual connectives and neutrals ==

By linear negation all the constructions defined so far (<math>\with, \tens, \oc</math>) have a dual.

=== The direct sum ===

The dual of <math>\with</math> is <math>\plus</math> defined by: <math>X\plus Y = (X\orth\with Y\orth)\orth</math>. An equivalent definition is given by: <math>\web{X\plus Y} = \web{X\with Y} = \{1\}\times \web X \cup \{2\}\times\web Y</math> and <math>(i, a)\coh_{X\plus Y} (j, b)\text{ iff } i = j = 1 \text{ and } a\coh_X b,\text{ or }i = j = 2\text{ and } a\coh_Y b</math>.

{{Theorem|
Let <math>x'</math> be a clique of <math>X\plus Y</math>; then <math>x'</math> is of the form <math>\{i\}\times x</math> where <math>i = 1\text{ and }x\in X</math>, or <math>i = 2\text{ and }x\in Y</math>.

Denote <math>\mathrm{inl}:X\longrightarrow X\plus Y</math> the function defined by <math>\mathrm{inl}(x) = \{1\}\times x</math> and by <math>\mathrm{inr}:Y\longrightarrow X\plus Y</math> the function defined by <math>\mathrm{inr}(x) = \{2\}\times x</math>. Then <math>\mathrm{inl}</math> and <math>\mathrm{inr}</math> are linear.

If <math>F:X\longrightarrow Z</math> and <math>G:Y\longrightarrow Z</math> are ''linear'' functions then the function <math>H:X\plus Y \longrightarrow Z</math> defined by <math>H(\mathrm{inl}(x)) = F(x)</math> and <math>H(\mathrm{inr}(y)) = G(y)</math> is linear.
}}

In other terms <math>X\plus Y</math> is the direct sum of <math>X</math> and <math>Y</math>. Note that in the theorem all functions are ''linear''. Things doesn't work so smoothly for stable functions. Historically it was after noting this defect of coherent semantics w.r.t. the intuitionnistic implication that Girard was leaded to discover linear functions.

=== The par and the why not ===

We now come to the most mysterious constructions of coherent semantics: the duals of the tensor and the of course.

The ''par'' is the dual of the tensor, thus defined by: <math>X\parr Y = (X\orth\tens Y\orth)\orth</math>. From this one can deduce the definition in graph terms: <math>\web{X\parr Y} = \web{X\tens Y} = \web X\times \web Y</math> and <math>(a,b)\scoh_{X\parr Y} (a',b')</math> iff <math>a\scoh_X a'</math> or <math>b\scoh_Y b'</math>. With this definition one sees that we have:

<math>X\limp Y = X\orth\parr Y</math>

for any coherent spaces <math>X</math> and <math>Y</math>. This equation can be seen as an alternative definition of the par: <math>X\parr Y = X\orth\limp Y</math>.

Similarly the dual of the of course is called ''why not'' defined by: <math>\wn X = (\oc X\orth)\orth</math>. From this we deduce the definition in the graph sense which is a bit tricky: <math>\web{\wn X}</math> is the set of finite anticliques of <math>X</math>, and given two finite anticliques <math>x</math> and <math>y</math> of <math>X</math> we have <math>x\scoh_{\wn X} y</math> iff there is <math>a\in x</math> and <math>b\in y</math> such that <math>a\scoh_X b</math>.

Note that both for the par and the why not it is much more convenient to define the strict coherence than the coherence.

With these two last constructions, the equation between the stable function space, the of course and the linear function space may be written:

<math>X\imp Y = \wn X\orth\parr Y</math>.

=== One and bottom ===

Depending on the context we denote by <math>\one</math> or <math>\bot</math> the coherent space whose web is a singleton and whose coherence relation is the trivial reflexive relation.

{{Theorem|
<math>\one</math> is neutral for tensor, that is, there is a linear isomorphism <math>\varphi:X\tens\one\ \stackrel{\sim}{\longrightarrow}\ X</math>.

Similarly <math>\bot</math> is neutral for par.
}}

=== Zero and top ===

Depending on the context we denote by <math>\zero</math> or <math>\top</math> the coherent space with empty web.

{{Theorem|
<math>\zero</math> is neutral for the direct sum <math>\plus</math>, <math>\top</math> is neutral for the cartesian product <math>\with</math>.
}}

{{Remark|
It is one of the main defect of coherent semantics w.r.t. linear logic that it identifies the neutrals: in coherent semantics <math>\zero = \top</math> and <math>\one = \bot</math>. However there is no known semantics of LL that solves this problem in a satisfactory way.}}

== The failure of coherent semantics ==

Coherent semantics was an important milestone in the modern theory of logic of programs. However it suffers from a number of defects the correction of which have motivated lots of work.

=== Sequentiality ===

Sequentiality is a property that we will not define here (it would diserve its own article). We rely on the intuition that a function of <math>n</math> arguments is sequential if one can determine which of these argument is examined first during the computation. Obviously any function implemented in a functionnal language is sequential; for example the function ''or'' defined à la CAML by:

<code>or = fun (x, y) -> if x then true else y</code>

examines its argument x first. Note that this may be expressed more abstractly by the property: <math>\mathrm{or}(\bot, x) = \bot</math> for any boolean <math>x</math>: the function ''or'' needs its first argument in order to compute anything. On the other hand we have <math>\mathrm{or}(\mathrm{true}, \bot) = \mathrm{true}</math>: in some case (when the first argument is true), the function doesn't need its second argument at all.

The typical non sequential function is the ''parallel or'' (that one cannot define in a CAML like language).

For a while one may have believed that the stability condition on which coherent semantics is built was enough to capture the notion of ''sequentiality'' of programs. A hint was the already mentionned fact that the ''parallel or'' is not stable. This diserves a bit of explanation.

==== The parallel or is not stable ====

Let <math>B</math> be the coherent space of booleans, also know as the flat domain of booleans: <math>\web B = \{tt, ff\}</math> where <math>tt</math> and <math>ff</math> are two arbitrary distinct objects (for example one may take <math>tt = 0</math> and <math>ff = 1</math>) and for any <math>b_1, b_2\in \web B</math>, define <math>b_1\coh_B b_2</math> iff <math>b_1 = b_2</math>. Then <math>B</math> has exactly three cliques: the empty clique that we shall denote <math>\bot</math>, the singleton <math>\{tt\}</math> that we shall denote <math>T</math> and the singleton <math>\{ff\}</math> that we shall denote <math>F</math>. These three cliques are ordered by inclusion: <math>\bot \leq T, F</math> (we use <math>\leq</math> for <math>\subset</math> to enforce the idea that coherent spaces are domains).

Recall the [[#Cartesian product|definition of the with]], and in particular that any clique of <math>B\with B</math> has the form <math>\langle x, y\rangle</math> where <math>x</math> and <math>y</math> are cliques of <math>B</math>. Thus <math>B\with B</math> has 9 cliques: <math>\langle\bot,\bot\rangle,\ \langle\bot, T\rangle,\ \langle\bot, F\rangle,\ \langle T,\bot\rangle,\ \dots</math> that are ordered by the product order: <math>\langle x,y\rangle\leq \langle x,y\rangle</math> iff <math>x\leq x'</math> and <math>y\leq y'</math>.

With these notations in mind one may define the parallel or by:

<math>
\begin{array}{rcl}
\mathrm{Por} : B\with B &\longrightarrow& B\\
\langle T,\bot\rangle &\longrightarrow& T\\
\langle \bot,T\rangle &\longrightarrow& T\\
\langle F, F\rangle &\longrightarrow& F
\end{array}
</math>

The function is completely determined if we add the assumption that it is non decreasing; for example one must have <math>\mathrm{Por}\langle\bot,\bot\rangle = \bot</math> because the lhs has to be less than both <math>T</math> and <math>F</math> (because <math>\langle\bot,\bot\rangle \leq \langle T,\bot\rangle</math> and <math>\langle\bot,\bot\rangle \leq \langle F,F\rangle</math>).

The function is not stable because <math>\langle T,\bot\rangle \cap \langle \bot, T\rangle = \langle\bot, \bot\rangle</math>, thus <math>\mathrm{Por}(\langle T,\bot\rangle \cap \langle \bot, T\rangle) = \bot</math> whereas <math>\mathrm{Por}\langle T,\bot\rangle \cap \mathrm{Por}\langle \bot, T\rangle = T\cap T = T</math>.

Another way to see this is: suppose <math>x</math> and <math>y</math> are two cliques of <math>B</math> such that <math>tt\in \mathrm{Por}\langle x, y\rangle</math>, which means that <math>\mathrm{Por}\langle x, y\rangle = T</math>; according to the [[#Stable functions|caracterisation theorem of stable functions]], if <math>\mathrm{Por}</math> were stable then there would be a unique minimum <math>x_0</math> included in <math>x</math>, and a unique minimum <math>y_0</math> included in <math>y</math> such that <math>\mathrm{Por}\langle x_0, y_0\rangle = T</math>. This is not the case because both <math>\langle T,\bot\rangle</math> and <math>\langle T,\bot\rangle</math> are minimal such that their value is <math>T</math>.

In other terms, knowing that <math>\mathrm{Por}\langle x, y\rangle = T</math> doesn't tell which of <math>x</math> of <math>y</math> is responsible for that, although we know by the definition of <math>\mathrm{Por}</math> that only one of them is. Indeed the <math>\mathrm{Por}</math> function is not representable in sequential programming languages such as (typed) lambda-calculus.

So the first genuine idea would be that stability caracterises sequentiality; but...

==== The Gustave function is stable ====

The Gustave function, so-called after an old joke, was found by Gérard Berry as an example of a function that is stable but non sequential. It is defined by:

<math>
\begin{array}{rcl}
B\with B\with B &\longrightarrow& B\\
\langle T, F, \bot\rangle &\longrightarrow& T\\
\langle \bot, T, F\rangle &\longrightarrow& T\\
\langle F, \bot, T\rangle &\longrightarrow& T\\
\langle x, y, z\rangle &\longrightarrow& F
\end{array}
</math>

The last clause is for all cliques <math>x</math>, <math>y</math> and <math>z</math> such that <math>\langle x, y ,z\rangle</math> is incompatible with the three cliques <math>\langle T, F, \bot\rangle</math>, <math>\langle \bot, T, F\rangle</math> and <math>\langle F, \bot, T\rangle</math>, that is such that the union with any of these three cliques is not a clique in <math>B\with B\with B</math>. We shall denote <math>x_1</math>, <math>x_2</math> and <math>x_3</math> these three cliques.

We furthemore assume that the Gustave function is non decreasing, so that we get <math>G\langle\bot,\bot,\bot\rangle = \bot</math>.

We note that <math>x_1</math>, <math>x_2</math> and <math>x_3</math> are pairwise incompatible. From this we can deduce that the Gustave function is stable: typically if <math>G\langle x,y,z\rangle = T</math> then exactly one of the <math>x_i</math>s is contained in <math>\langle x, y, z\rangle</math>.

However it is not sequential because there is no way to determine which of its three arguments is examined first: it is not the first one otherwise we would have <math>G\langle\bot, T, F\rangle = \bot</math> and similarly it is not the second one nor the third one.

In other terms there is no way to implement the Gustave function by a lambda-term (or in any sequential programming language). Thus coherent semantics is not complete w.r.t. lambda-calculus.

The research for a right model for sequentiality was the motivation for lot of
work, ''e.g.'', ''sequential algorithms'' by Gérard Bérry and Pierre-Louis
Currien in the early eighties, that were more recently reformulated as a kind
of [[Game semantics|game model]], and the theory of ''hypercoherent spaces'' by
Antonio Bucciarelli and Thomas Ehrhard.

=== Multiplicative neutrals and the mix rule ===

Coherent semantics is slightly degenerated w.r.t. linear logic because it identifies multiplicative neutrals (it also identifies additive neutrals but that's yet another problem): the coherent spaces <math>\one</math> and <math>\bot</math> are equal.

The first consequence of the identity <math>\one = \bot</math> is that the formula <math>\one\limp\bot</math> becomes provable, and so does the formula <math>\bot</math>. Note that this doesn't entail (as in classical logic or intuitionnistic logic) that linear logic is incoherent because the principle <math>\bot\limp A</math> for any formula <math>A</math> is still not provable.

The equality <math>\one = \bot</math> has also as consequence the fact that <math>\bot\limp\one</math> (or equivalently the formula <math>\one\parr\one</math>) is provable. This principle is also known as the [[Mix|mix rule]]

<math>
\AxRule{\vdash \Gamma}
\AxRule{\vdash \Delta}
\LabelRule{\rulename{mix}}
\BinRule{\vdash \Gamma,\Delta}
\DisplayProof
</math>

as it can be used to show that this rule is admissible:

<math>
\AxRule{\vdash\Gamma}
\LabelRule{\bot_R}
\UnaRule{\vdash\Gamma, \bot}
\AxRule{\vdash\Delta}
\LabelRule{\bot_R}
\UnaRule{\vdash\Delta, \bot}
\BinRule{\vdash \Gamma, \Delta, \bot\tens\bot}
\NulRule{\vdash \one\parr\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\Gamma,\Delta}
\DisplayProof
</math>

None of the two principles <math>1\limp\bot</math> and <math>\bot\limp\one</math> are valid in linear logic. To correct this one could extend the syntax of linear logic by adding the mix-rule. This is not very satisfactory as the mix rule violates some principles of [[Polarised Linear Logic]], typically the fact that as sequent of the form <math>\vdash P_1, P_2</math> where <math>P_1</math> and <math>P_2</math> are positive, is never provable.

On the other hand the mix-rule is valid in coherent semantics so one could try to find some other model that invalidates the mix-rule. For example Girard's Coherent Banach spaces were an attempt to address this issue.

== References ==
<references />

Geometry of interaction

2011-09-30T14:39:39Z

Pierre-Marie Pédrot: ortho

The ''geometry of interaction'', GoI in short, was defined in the early nineties by Girard as an interpretation of linear logic into operators algebra: formulae were interpreted by Hilbert spaces and proofs by partial isometries.

This was a striking novelty as it was the first time that a mathematical model of logic (lambda-calculus) didn't interpret a proof of <math>A\limp B</math> as a morphism ''from'' <math>A</math> ''to'' <math>B</math> and proof composition (cut rule) as the composition of morphisms. Rather the proof was interpreted as an operator acting ''on'' <math>A\limp B</math>, that is a morphism from <math>A\limp B</math> to <math>A\limp B</math>. For proof composition the problem was then, given an operator on <math>A\limp B</math> and another one on <math>B\limp C</math> to construct a new operator on <math>A\limp C</math>. This problem was solved by the ''execution formula'' that bares some formal analogies with Kleene's formula for recursive functions. For this reason GoI was claimed to be an ''operational semantics'', as opposed to traditionnal [[Semantics|denotational semantics]].

The first instance of the GoI was restricted to the <math>MELL</math> fragment of linear logic (Multiplicative and Exponential fragment) which is enough to encode lambda-calculus. Since then Girard proposed several improvements: firstly the extension to the additive connectives known as ''Geometry of Interaction 3'' and more recently a complete reformulation using Von Neumann algebras that allows to deal with some aspects of [[Light linear logics|implicit complexity]]

The GoI has been a source of inspiration for various authors. Danos and Regnier have reformulated the original model exhibiting its combinatorial nature using a theory of reduction of paths in proof-nets and showing the link with abstract machines; the execution formula appears as the composition of two automata interacting through a common interface. Also the execution formula has rapidly been understood as expressing the composition of strategies in game semantics. It has been used in the theory of sharing reduction for lambda-calculus in the Abadi-Gonthier-Lévy reformulation and simplification of Lamping's representation of sharing. Finally the original GoI for the <math>MELL</math> fragment has been reformulated in the framework of traced monoidal categories following an idea originally proposed by Joyal.

= The Geometry of Interaction as operators =

The original construction of GoI by Girard follows a general pattern already mentionned in the section on [[coherent semantics]] under the name ''symmetric reducibility'' and that was first put to use in [[phase semantics]]. First set a general space <math>P</math> called the ''proof space'' because this is where the interpretations of proofs will live. Make sure that <math>P</math> is a (not necessarily commutative) monoid. In the case of GoI, the proof space is a subset of the space of bounded operators on <math>\ell^2</math>.

Second define a particular subset of <math>P</math> that will be denoted by <math>\bot</math>; then derive a duality on <math>P</math>: for <math>u,v\in P</math>, <math>u</math> and <math>v</math> are dual<ref>In modern terms one says that <math>u</math> and <math>v</math> are ''polar''.</ref>iff <math>uv\in\bot</math>.

Such a duality defines an [[orthogonality relation]], with the usual derived definitions and properties.

For the GoI, two dualities have proved to work; we will consider the first one: nilpotency, ''ie'', <math>\bot</math> is the set of nilpotent operators in <math>P</math>. Let us explicit this: two operators <math>u</math> and <math>v</math> are dual if there is a nonnegative integer <math>n</math> such that <math>(uv)^n = 0</math>. This duality is symmetric: if <math>uv</math> is nilpotent then <math>vu</math> is nilpotent also.

Last define a ''type'' as a subset <math>T</math> of the proof space that is equal to its bidual: <math>T = T\biorth</math>. This means that <math>u\in T</math> iff for all operator <math>v\in T\orth</math>, that is such that <math>u'v\in\bot</math> for all <math>u'\in T</math>, we have <math>uv\in\bot</math>.

The real work<ref>The difficulty is to find the right duality that will make logical operations interpretable. General conditions that allows to achieve this have been formulated by Hyland and Schalk thanks to their theory of ''[[double glueing]]''.</ref>is now to interpret logical operations, that is to associate a type to each formula, an object to each proof and show the ''adequacy lemma'': if <math>u</math> is the interpretation of a proof of the formula <math>A</math> then <math>u</math> belongs to the type associated to <math>A</math>.

== [[GoI for MELL: partial isometries|Partial isometries]] ==

The first step is to build the proof space. This is constructed as a special set of partial isometries on a separable Hilbert space <math>H</math> which turns out to be generated by partial permutations on the canonical basis of <math>H</math>.

These so-called ''<math>p</math>-isometries'' enjoy some nice properties, the most important one being that a <math>p</math>-isometry is a sum of <math>p</math>-isometries iff all the terms of the sum have disjoint domains and disjoint codomains. As a consequence we get that a sum of <math>p</math>-isometries is null iff each term of the sum is null.

A second important property is that operators on <math>H</math> can be ''externalized'' using <math>p</math>-isometries into operators acting on <math>H\oplus H</math>, and conversely operators on <math>H\oplus H</math> may be ''internalized'' into operators on <math>H</math>. This is widely used in the sequel.

== [[GoI for MELL: the *-autonomous structure|The *-autonomous structure]] ==

The second step is to interpret the linear logic multiplicative operations, most importantly the cut rule.

Internalization/externalization is the key for this: typically the type <math>A\tens B</math> is interpreted by a set of <math>p</math>-isometries which are internalizations of operators acting on <math>H\oplus H</math>.

The (interpretation of) the cut-rule is defined in two steps: firstly we use nilpotency to define an operation corresponding to lambda-calculus application which given two <math>p</math>-isometries in respectively <math>A\limp B</math> and <math>A</math> produces an operator in <math>B</math>. From this we deduce the composition and finally obtain a structure of *-autonomous category, that is a model of multiplicative linear logic.

== [[GoI for MELL: exponentials|The exponentials]] ==

Finally we turn to define exponentials, that is connectives managing duplication. To do this we introduce an isomorphism (induced by a <math>p</math>-isometry) between <math>H</math> and <math>H\tens H</math>: the first component of the tensor is intended to hold the address of the the copy whereas the second component contains the content of the copy.

We eventually get a quasi-model of full MELL; quasi in the sense that if we can construct <math>p</math>-isometries for usual structural operations in MELL (contraction, dereliction, digging), the interpretation of linear logic proofs is not invariant w.r.t. cut elimination in general. It is however invariant in some good cases, which are enough to get a correction theorem for the interpretation.

= The Geometry of Interaction as an abstract machine =

= Notes and references =

<references/>

Geometry of interaction

2011-09-30T14:38:14Z

Pierre-Marie Pédrot: replaced paragraph with a link

The ''geometry of interaction'', GoI in short, was defined in the early nineties by Girard as an interpretation of linear logic into operators algebra: formulae were interpreted by Hilbert spaces and proofs by partial isometries.

This was a striking novelty as it was the first time that a mathematical model of logic (lambda-calculus) didn't interpret a proof of <math>A\limp B</math> as a morphism ''from'' <math>A</math> ''to'' <math>B</math> and proof composition (cut rule) as the composition of morphisms. Rather the proof was interpreted as an operator acting ''on'' <math>A\limp B</math>, that is a morphism from <math>A\limp B</math> to <math>A\limp B</math>. For proof composition the problem was then, given an operator on <math>A\limp B</math> and another one on <math>B\limp C</math> to construct a new operator on <math>A\limp C</math>. This problem was solved by the ''execution formula'' that bares some formal analogies with Kleene's formula for recursive functions. For this reason GoI was claimed to be an ''operational semantics'', as opposed to traditionnal [[Semantics|denotational semantics]].

The first instance of the GoI was restricted to the <math>MELL</math> fragment of linear logic (Multiplicative and Exponential fragment) which is enough to encode lambda-calculus. Since then Girard proposed several improvements: firstly the extension to the additive connectives known as ''Geometry of Interaction 3'' and more recently a complete reformulation using Von Neumann algebras that allows to deal with some aspects of [[Light linear logics|implicit complexity]]

The GoI has been a source of inspiration for various authors. Danos and Regnier have reformulated the original model exhibiting its combinatorial nature using a theory of reduction of paths in proof-nets and showing the link with abstract machines; the execution formula appears as the composition of two automata interacting through a common interface. Also the execution formula has rapidly been understood as expressing the composition of strategies in game semantics. It has been used in the theory of sharing reduction for lambda-calculus in the Abadi-Gonthier-Lévy reformulation and simplification of Lamping's representation of sharing. Finally the original GoI for the <math>MELL</math> fragment has been reformulated in the framework of traced monoidal categories following an idea originally proposed by Joyal.

= The Geometry of Interaction as operators =

The original construction of GoI by Girard follows a general pattern already mentionned in the section on [[coherent semantics]] under the name ''symmetric reducibility'' and that was first put to use in [[phase semantics]]. First set a general space <math>P</math> called the ''proof space'' because this is where the interpretations of proofs will live. Make sure that <math>P</math> is a (not necessarily commutative) monoid. In the case of GoI, the proof space is a subset of the space of bounded operators on <math>\ell^2</math>.

Second define a particular subset of <math>P</math> that will be denoted by <math>\bot</math>; then derive a duality on <math>P</math>: for <math>u,v\in P</math>, <math>u</math> and <math>v</math> are dual<ref>In modern terms one says that <math>u</math> and <math>v</math> are ''polar''.</ref>iff <math>uv\in\bot</math>.

Such a duality defines an [[orthogonality relation]], with the usual derived definitions and properties.

For the GoI, two dualities have proved to work; we will consider the first one: nilpotency, ''ie'', <math>\bot</math> is the set of nilpotent operators in <math>P</math>. Let us explicit this: two operators <math>u</math> and <math>v</math> are dual if there is a nonnegative integer <math>n</math> such that <math>(uv)^n = 0</math>. This duality is symmetric: if <math>uv</math> is nilpotent then <math>vu</math> is nilpotent also.

Last define a ''type'' as a subset <math>T</math> of the proof space that is equal to its bidual: <math>T = T\biorth</math>. This means that <math>u\in T</math> iff for all operator <math>v\in T\orth</math>, that is such that <math>u'v\in\bot</math> for all <math>u'\in T</math>, we have <math>uv\in\bot</math>.

The real work<ref>The difficulty is to find the right duality that will make logical operations interpretable. General conditions that allows to achieve this have been formulated by Hyland and Schalk thanks to their theory of ''[[double gluing]]''.</ref>is now to interpret logical operations, that is to associate a type to each formula, an object to each proof and show the ''adequacy lemma'': if <math>u</math> is the interpretation of a proof of the formula <math>A</math> then <math>u</math> belongs to the type associated to <math>A</math>.

== [[GoI for MELL: partial isometries|Partial isometries]] ==

The first step is to build the proof space. This is constructed as a special set of partial isometries on a separable Hilbert space <math>H</math> which turns out to be generated by partial permutations on the canonical basis of <math>H</math>.

These so-called ''<math>p</math>-isometries'' enjoy some nice properties, the most important one being that a <math>p</math>-isometry is a sum of <math>p</math>-isometries iff all the terms of the sum have disjoint domains and disjoint codomains. As a consequence we get that a sum of <math>p</math>-isometries is null iff each term of the sum is null.

A second important property is that operators on <math>H</math> can be ''externalized'' using <math>p</math>-isometries into operators acting on <math>H\oplus H</math>, and conversely operators on <math>H\oplus H</math> may be ''internalized'' into operators on <math>H</math>. This is widely used in the sequel.

== [[GoI for MELL: the *-autonomous structure|The *-autonomous structure]] ==

The second step is to interpret the linear logic multiplicative operations, most importantly the cut rule.

Internalization/externalization is the key for this: typically the type <math>A\tens B</math> is interpreted by a set of <math>p</math>-isometries which are internalizations of operators acting on <math>H\oplus H</math>.

The (interpretation of) the cut-rule is defined in two steps: firstly we use nilpotency to define an operation corresponding to lambda-calculus application which given two <math>p</math>-isometries in respectively <math>A\limp B</math> and <math>A</math> produces an operator in <math>B</math>. From this we deduce the composition and finally obtain a structure of *-autonomous category, that is a model of multiplicative linear logic.

== [[GoI for MELL: exponentials|The exponentials]] ==

Finally we turn to define exponentials, that is connectives managing duplication. To do this we introduce an isomorphism (induced by a <math>p</math>-isometry) between <math>H</math> and <math>H\tens H</math>: the first component of the tensor is intended to hold the address of the the copy whereas the second component contains the content of the copy.

We eventually get a quasi-model of full MELL; quasi in the sense that if we can construct <math>p</math>-isometries for usual structural operations in MELL (contraction, dereliction, digging), the interpretation of linear logic proofs is not invariant w.r.t. cut elimination in general. It is however invariant in some good cases, which are enough to get a correction theorem for the interpretation.

= The Geometry of Interaction as an abstract machine =

= Notes and references =

<references/>

Finiteness semantics

2011-09-30T14:32:46Z

Pierre-Marie Pédrot: link to orthogonalities

The category <math>\mathbf{Fin}</math> of finiteness spaces and finitary relations was introduced by Ehrhard, refining the [[relational semantics|purely relational model of linear logic]]. A finiteness space is a set equipped with a finiteness structure, i.e. a particular set of subsets which are said to be finitary; and the model is such that the usual relational denotation of a proof in linear logic is always a finitary subset of its conclusion. By the usual co-Kleisli construction, this also provides a model of the simply typed lambda-calculus: the cartesian closed category <math>\mathbf{Fin}_\oc</math>.

The main property of finiteness spaces is that the intersection of two finitary subsets of dual types is always finite. This feature allows to reformulate Girard's quantitative semantics in a standard algebraic setting, where morphisms interpreting typed <math>\lambda</math>-terms are analytic functions between the topological vector spaces generated by vectors with finitary supports. This provided the semantical foundations of Ehrhard-Regnier's differential <math>\lambda</math>-calculus and motivated the general study of a differential extension of linear logic.

It is worth noticing that finiteness spaces can accomodate typed <math>\lambda</math>-calculi only: for instance, the relational semantics of fixpoint combinators is never finitary. The whole point of the finiteness construction is actually to reject infinite computations. Indeed, from a logical point of view, computation is cut elimination: the finiteness structure ensures the intermediate sets involved in the relational interpretation of a cut are all finite. In that sense, the finitary semantics is intrinsically typed.

== Finiteness spaces ==

The construction of finiteness spaces follows a well known pattern. It is given by the following notion of orthogonality: <math>a\mathrel \bot a'</math> iff <math>a\cap a'</math> is finite. Then one unrolls [[Orthogonality relation|familiar definitions]], as we do in the following paragraphs.

Let <math>A</math> be a set. Denote by <math>\powerset A</math> the powerset of <math>A</math> and by <math>\finpowerset A</math> the set of all finite subsets of <math>A</math>. Let <math>{\mathfrak F} \subseteq \powerset A</math> any set of subsets of <math>A</math>. We define the pre-dual of <math>{\mathfrak F}</math> in <math>A</math> as <math>{\mathfrak F}^{\bot_{A}}=\left\{a'\subseteq A;\ \forall a\in{\mathfrak F},\ a\cap a'\in\finpowerset A\right\}</math>. In general we will omit the subscript in the pre-dual notation and just write <math>{\mathfrak F}\orth</math>. For all <math>{\mathfrak F}\subseteq\powerset A</math>, we have the following immediate properties: <math>\finpowerset A\subseteq {\mathfrak F}\orth</math>; <math>{\mathfrak F}\subseteq {\mathfrak F}\biorth</math>; if <math>{\mathfrak G}\subseteq{\mathfrak F}</math>, <math>{\mathfrak F}\orth\subseteq {\mathfrak G}\orth</math>. By the last two, we get <math>{\mathfrak F}\orth = {\mathfrak F}\triorth</math>. A finiteness structure on <math>A</math> is then a set <math>{\mathfrak F}</math> of subsets of <math>A</math> such that <math>{\mathfrak F}\biorth = {\mathfrak F}</math>.

A finiteness space is a dependant pair <math>{\mathcal A}=\left(\web{\mathcal A},\mathfrak F\left(\mathcal A\right)\right)</math> where <math>\web {\mathcal A}</math> is the underlying set (the web of <math>{\mathcal A}</math>) and <math>\mathfrak F\left(\mathcal A\right)</math> is a finiteness structure on <math>\web {\mathcal A}</math>. We then write <math>{\mathcal A}\orth</math> for the dual finiteness space: <math>\web {{\mathcal A}\orth} = \web {\mathcal A}</math> and <math>\mathfrak F\left({\mathcal A}\orth\right)=\mathfrak F\left({\mathcal A}\right)^{\bot}</math>. The elements of <math>\mathfrak F\left(\mathcal A\right)</math> are called the finitary subsets of <math>{\mathcal A}</math>.

===== Example. =====
For all set <math>A</math>, <math>(A,\finpowerset A)</math> is a finiteness space and <math>(A,\finpowerset A)\orth = (A,\powerset A)</math>. In particular, each finite set <math>A</math> is the web of exactly one finiteness space: <math>(A,\finpowerset A)=(A,\powerset A)</math>. We introduce the following two: <math>\zero = \zero\orth = \left(\emptyset, \{\emptyset\}\right)</math> and <math>\one = \one\orth = \left(\{\emptyset\}, \{\emptyset, \{\emptyset\}\}\right)</math>. We also introduce the finiteness space of natural numbers <math>{\mathcal N}</math> by: <math>|{\mathcal N}|={\mathbf N}</math> and <math>a\in\mathfrak F\left(\mathcal N\right)</math> iff <math>a</math> is finite. We write <math>\mathcal O=\{0\}\in\mathfrak F\left({\mathcal N}\right)</math>.

Notice that <math>{\mathfrak F}</math> is a finiteness structure iff it is of the form <math>{\mathfrak G}\orth</math>. It follows that any finiteness structure <math>{\mathfrak F}</math> is downwards closed for inclusion, and closed under finite unions and arbitrary intersections. Notice however that <math>{\mathfrak F}</math> is not closed under directed unions in general: for all <math>k\in{\mathbf N}</math>, write <math>k{\downarrow}=\left\{j;\ j\le k\right\}\in\mathfrak F\left({\mathcal N}\right)</math>; then <math>k{\downarrow}\subseteq k'{\downarrow}</math> as soon as <math>k\le k'</math>, but <math>\bigcup_{k\ge0} k{\downarrow}={\mathbf N}\not\in\mathfrak F\left({\mathcal N}\right)</math>.

=== Multiplicatives ===
For all finiteness spaces <math>{\mathcal A}</math> and <math>{\mathcal B}</math>, we define <math>{\mathcal A} \tens {\mathcal B}</math> by <math>\web {{\mathcal A} \tens {\mathcal B}} = \web{\mathcal A} \times \web{\mathcal B}</math> and <math>\mathfrak F\left({\mathcal A} \tens {\mathcal B}\right) = \left\{a\times b;\ a\in \mathfrak F\left(\mathcal A\right),\ b\in\mathfrak F\left(\mathcal B\right)\right\}\biorth</math>. It can be shown that <math>\mathfrak F\left({\mathcal A} \tens {\mathcal B}\right) = \left\{ c \subseteq \web{\mathcal A}\times\web{\mathcal B};\ \left.c\right|_l\in \mathfrak F\left(\mathcal A\right),\ \left.c\right|_r\in\mathfrak F\left(\mathcal B\right)\right\}</math>, where <math>\left.c\right|_l</math> and <math>\left.c\right|_r</math> are the obvious projections.

Let <math>f\subseteq A \times B</math> be a relation from <math>A</math> to <math>B</math>, we write <math>f\orth=\left\{(\beta,\alpha);\ (\alpha,\beta)\in f\right\}</math>. For all <math>a\subseteq A</math>, we set <math>f\cdot a = \left\{\beta\in B;\ \exists \alpha\in a,\ (\alpha,\beta)\in f\right\}</math>. If moreover <math>g\subseteq B \times C</math>, we define <math>g \bullet f = \left\{(\alpha,\gamma)\in A\times C;\ \exists \beta\in B,\ (\alpha,\beta)\in f\wedge(\beta,\gamma)\in g\right\}</math>. Then, setting <math>{\mathcal A}\limp{\mathcal B} = \left({\mathcal A}\otimes {\mathcal B}\orth\right)\orth</math>, <math>\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)\subseteq {\web{\mathcal A}\times\web{\mathcal B}}</math> is characterized as follows:

<math>
\begin{align}
f\in \mathfrak F\left({\mathcal A}\limp{\mathcal B}\right) &\iff \forall a\in \mathfrak F\left({\mathcal A}\right), f\cdot a \in\mathfrak F\left({\mathcal B}\right) \text{ and } \forall b\in \mathfrak F\left({\mathcal B}\orth\right), f\orth\cdot b \in\mathfrak F\left({\mathcal A}\orth\right)
\\
&\iff \forall a\in \mathfrak F\left({\mathcal A}\right), f\cdot a \in\mathfrak F\left({\mathcal B}\right) \text{ and } \forall \beta\in \web{{\mathcal B}}, f\orth\cdot \left\{\beta\right\} \in\mathfrak F\left({\mathcal A}\orth\right)
\\
&\iff \forall \alpha\in \web{{\mathcal A}}, f\cdot \left\{\alpha\right\} \in\mathfrak F\left({\mathcal B}\right) \text{ and } \forall b\in \mathfrak F\left({\mathcal B}\orth\right), f\orth\cdot b \in\mathfrak F\left({\mathcal A}\orth\right)
\end{align}
</math>

The elements of <math>\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)</math> are called finitary relations from <math>{\mathcal A}</math> to <math>{\mathcal B}</math>. By the previous characterization, the identity relation <math>\mathsf{id}_{{\mathcal A}} = \left\{(\alpha,\alpha);\ \alpha\in\web{{\mathcal A}}\right\}</math> is finitary, and the composition of two finitary relations is also finitary. One can thus define the category <math>\mathbf{Fin}</math> of finiteness spaces and finitary relations: the objects of <math>\mathbf{Fin}</math> are all finiteness spaces, and <math>\mathbf{Fin}({\mathcal A},{\mathcal B})=\mathfrak F\left({\mathcal A}\limp{\mathcal B}\right)</math>. Equipped with the tensor product <math>\tens</math>, <math>\mathbf{Fin}</math> is symmetric monoidal, with unit <math>\one</math>; it is monoidal closed by the definition of <math>\limp</math>; it is <math>*</math>-autonomous by the obvious isomorphism between <math>{\mathcal A}\orth</math> and <math>{\mathcal A}\limp\one</math>.




===== Example. =====
Setting <math>\mathcal{S}=\left\{(k,k+1);\ k\in{\mathbf N}\right\}</math> and <math>\mathcal{P}=\left\{(k+1,k);\ k\in{\mathbf N}\right\}</math>, we have <math>\mathcal{S},\mathcal{P}\in\mathbf{Fin}({\mathcal N},{\mathcal N})</math> and <math>\mathcal{P}\bullet\mathcal{S}=\mathsf{id}_{{\mathcal N}}</math>.

=== Additives ===
We now introduce the cartesian structure of <math>\mathbf{Fin}</math>. We define <math>{\mathcal A} \oplus {\mathcal B}</math> by <math>\web {{\mathcal A} \oplus {\mathcal B}} = \web{\mathcal A} \uplus \web{\mathcal B}</math> and <math>\mathfrak F\left({\mathcal A} \oplus {\mathcal B}\right) = \left\{ a\uplus b;\ a\in \mathfrak F\left(\mathcal A\right),\ b\in\mathfrak F\left(\mathcal B\right)\right\}</math> where <math>\uplus</math> denotes the disjoint union of sets: <math>x\uplus y=(\{1\}\times x)\cup(\{2\}\times y)</math>. We have <math>\left({\mathcal A}\oplus {\mathcal B}\right)\orth = {\mathcal A}\orth\oplus{\mathcal B}\orth</math>.<ref>The fact that the additive connectors are identified, i.e. that we obtain a biproduct, is to be related with the enrichment of <math>\mathbf{Fin}</math> over the monoid structure of set union: see {{BibEntry|bibtype=journal|author=Marcello P. Fiore|title=Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic|journal=TLCA 2007}} This identification can also be shown to be a [[isomorphism]] of LL with sums of proofs.</ref>
The category <math>\mathbf{Fin}</math> is both cartesian and co-cartesian, with <math>\oplus</math> being the product and co-product, and <math>\zero</math> the initial and terminal object. Projections are given by:

<math>
\begin{align}
\lambda_{{\mathcal A},{\mathcal B}}&=\left\{\left((1,\alpha),\alpha\right);\ \alpha\in\web{\mathcal A}\right\}
\in\mathbf{Fin}({\mathcal A}\oplus{\mathcal B},{\mathcal A}) \\
\rho_{{\mathcal A},{\mathcal B}}&=\left\{\left((2,\beta),\beta\right);\ \beta\in\web{\mathcal B}\right\}
\in\mathbf{Fin}({\mathcal A}\oplus{\mathcal B},{\mathcal B})
\end{align}
</math>

and if <math>f\in\mathbf{Fin}({\mathcal C},{\mathcal A})</math> and <math>g\in\mathbf{Fin}({\mathcal C},{\mathcal B})</math>, pairing is given by:

<math>\left\langle f,g\right\rangle = \left\{\left(\gamma,(1,\alpha)\right);\ (\gamma,\alpha)\in f\right\} \cup \left\{\left(\gamma,(2,\beta)\right);\ (\gamma,\beta)\in g\right\} \in\mathbf{Fin}({\mathcal C},{\mathcal A}\oplus{\mathcal B}).</math>

The unique morphism from <math>{\mathcal A}</math> to <math>\zero</math> is the empty relation. The co-cartesian structure is obtained symmetrically.

===== Example. =====
Write <math>{\mathcal O}\orth=\left\{(0,\emptyset)\right\}\in\mathbf{Fin}({\mathcal N},\one)</math>. Then <math>\left\langle{{\mathcal O}\orth},{\mathcal{P}}\right\rangle =\{ (0,(1,\emptyset)) \}\cup \{ (k+1,(2,k)) ;\ k\in{\mathbf N} \} \in\mathbf{Fin}\left({\mathcal N},\one\oplus{\mathcal N}\right)</math>
is an isomorphism.



=== Exponentials ===
If <math>A</math> is a set, we denote by <math>\finmulset A</math> the set of all finite multisets of
elements of <math>A</math>, and if <math>a\subseteq A</math>, we write <math>a^{\oc}=\finmulset a\subseteq\finmulset A</math>.
If <math>\overline\alpha\in\finmulset A</math>, we denote its support by
<math>\mathrm{Support}\left(\overline \alpha\right)\in\finpowerset A</math>. For all finiteness space <math>{\mathcal A}</math>, we define
<math>\oc {\mathcal A}</math> by: <math>\web{\oc {\mathcal A}}= \finmulset{\web{{\mathcal A}}}</math> and <math>\mathfrak F\left(\oc{\mathcal A}\right)=\left\{a^{\oc};\ a\in\mathfrak F\left({\mathcal A}\right)\right\}\biorth</math>.
It can be shown that <math>\mathfrak F\left(\oc{\mathcal A}\right) = \left\{\overline a\subseteq\finmulset{\web{{\mathcal A}}};\ \bigcup_{\overline\alpha\in \overline a}\mathrm{Support}\left(\overline \alpha\right)\in\mathfrak F\left(\mathcal A\right)\right\}</math>.
Then, for all <math>f\in\mathbf{Fin}({\mathcal A},{\mathcal B})</math>, we set

<math>\oc f =\left\{\left(\left[\alpha_1,\ldots,\alpha_n\right],\left[\beta_1,\ldots,\beta_n\right]\right);\ \forall i,\ (\alpha_i,\beta_i)\in f\right\} \in \mathbf{Fin}(\oc {\mathcal A}, \oc {\mathcal B}),</math>

which defines a functor.
Natural transformations
<math>\mathsf{der}_{{\mathcal A}}=\left\{([\alpha],\alpha);\ \alpha\in \web{{\mathcal A}}\right\}\in\mathbf{Fin}(\oc{\mathcal A},{\mathcal A})</math> and
<math>\mathsf{digg}_{{\mathcal A}}=\left\{\left(\sum_{i=1}^n\overline\alpha_i,\left[\overline\alpha_1,\ldots,\overline\alpha_n\right]\right);\ \forall i,\ \overline\alpha_i\in\web{\oc {\mathcal A}}\right\}</math> make this functor a comonad.

===== Example. =====
We have isomorphisms

<math>\left\{([],\emptyset)\right\}\in\mathbf{Fin}(\oc\zero,\one)</math>
and

<math>\left\{ \left(\overline\alpha_l+\overline\beta_r,\left(\overline\alpha,\overline\beta\right)\right);\ (\overline\alpha_l,\overline\alpha)\in\oc\lambda_{{\mathcal A},{\mathcal B}}\wedge(\overline\beta_r,\overline\beta)\in\oc\rho_{{\mathcal A},{\mathcal B}}\right\} \in\mathbf{Fin}(\oc({\mathcal A}\oplus{\mathcal B}),\oc{\mathcal A}\tens\oc{\mathcal B}).</math>

More generally, we have
<math>\oc\left({\mathcal A}_1\oplus\cdots\oplus{\mathcal A}_n\right)\cong\oc{\mathcal A}_1\tens\cdots\tens\oc{\mathcal A}_n</math>.

==References==
<references />

Orthogonality relation

2011-09-30T14:10:04Z

Pierre-Marie Pédrot: cr

'''Orthogonality relations''' are used pervasively throughout linear logic models, being often used to define somehow the duality operator <math>(-)\orth</math>.

{{Definition|title=Orthogonality relation|Let <math>A</math> and <math>B</math> be two sets. An '''orthogonality relation''' on <math>A</math> and <math>B</math> is a binary relation <math>\mathcal{R}\subseteq A\times B</math>. We say that <math>a\in A</math> and <math>b\in B</math> are '''orthogonal''', and we note <math>a\perp b</math>, whenever <math>(a, b)\in\mathcal{R}</math>.}}

Let us now assume an orthogonality relation over <math>A</math> and <math>B</math>.

{{Definition|title=Orthogonal sets|Let <math>\alpha\subseteq A</math>. We define its orthogonal set <math>\alpha\orth</math> as <math>\alpha\orth:=\{b\in B \mid \forall a\in \alpha, a\perp b\}</math>.

Symmetrically, for any <math>\beta\subseteq B</math>, we define <math>\beta\orth:=\{a\in A \mid \forall b\in \beta, a\perp b\}</math>.
}}

Orthogonal sets define Galois connections and share many common properties.

{{Proposition|For any sets <math>\alpha, \alpha'\subseteq A</math>:

* <math>\alpha\subseteq \alpha\biorth</math>
* If <math>\alpha\subseteq\alpha'</math>, then <math>{\alpha'}\orth\subseteq\alpha\orth</math>
* <math>\alpha\triorth = \alpha\orth</math>
}}