LLWiki - New pages [en]

Regular formula

2013-10-28T21:01:35Z

Olivier Laurent: Basic properties of regular formulas

A ''regular formula'' is a formula <math>R</math> such that <math>R\linequiv\wn\oc R</math>.

A formula <math>L</math> is ''co-regular'' if its dual <math>L\orth</math> is regular, that is if <math>L\linequiv\oc\wn L</math>.

== Alternative characterization ==

<math>R</math> is regular if and only if it is [[Sequent calculus#Equivalences|equivalent]] to a formula of the shape <math>\wn P</math> for some [[positive formula]] <math>P</math>.

{{Proof|
If <math>R</math> is regular then <math>R\linequiv\wn\oc R</math> with <math>\oc R</math> positive. If <math>R\linequiv\wn P</math> with <math>P</math> positive then <math>R</math> is regular since <math>P\linequiv\oc P</math>.
}}

== Regular connectives ==

A connective <math>c</math> of arity <math>n</math> is ''regular'' if for any regular formulas <math>R_1</math>,...,<math>R_n</math>, <math>c(R_1,\dots,R_n)</math> is regular.

{{Proposition|title=Regular connectives|
<math>\parr</math>, <math>\bot</math> and <math>\wn\oc</math> define regular connectives.
}}

{{Proof|
If <math>R</math> and <math>S</math> are regular, <math>R\parr S \linequiv \wn\oc R \parr \wn\oc S \linequiv \wn{(\oc R\plus\oc S)}</math> thus it is regular since <math>\oc R\plus\oc S</math> is positive.

<math>\bot\linequiv\wn\zero</math> thus it is regular since <math>\zero</math> is positive.

If <math>R</math> is regular then <math>\wn\oc R</math> is regular, since <math>\wn\oc\wn\oc R\linequiv \wn\oc R</math>.
}}

More generally, <math>\wn\oc A</math> is regular for any formula <math>A</math>.

Additive cut rule

2013-10-28T20:24:46Z

Olivier Laurent: Non admissibility

The additive cut rule is:
<math>
\AxRule{\Gamma\vdash A,\Delta}
\AxRule{\Gamma,A\vdash\Delta}
\LabelRule{\rulename{cut\;add}}
\BinRule{\Gamma\vdash\Delta}
\DisplayProof
</math>

In contrary to what happens in classical logic, this rule is '''not''' admissible in linear logic.

The formula <math>\alpha\plus\alpha\orth</math> is not provable in linear logic, while it is derivable with the additive cut rule:

<math>
\NulRule{\alpha\vdash\alpha}
\UnaRule{\vdash\alpha,\alpha\orth}
\LabelRule{\plus_{R2}}
\UnaRule{\vdash\alpha,\alpha\plus\alpha\orth}
\NulRule{\alpha\vdash\alpha}
\LabelRule{\plus_{R1}}
\UnaRule{\alpha\vdash\alpha\plus\alpha\orth}
\LabelRule{\rulename{cut\;add}}
\BinRule{\vdash\alpha\plus\alpha\orth}
\DisplayProof
</math>

Negative formula

2013-10-28T17:50:07Z

Olivier Laurent: Dual version of positive formula

A ''negative formula'' is a formula <math>N</math> such that <math>\wn N\limp N</math> (thus a [[Wikipedia:F-algebra|algebra]] for the [[Wikipedia:Monad (category theory)|monad]] <math>\wn</math>). As a consequence <math>N</math> and <math>\wn N</math> are [[Sequent calculus#Equivalences|equivalent]].

A formula <math>N</math> is negative if and only if <math>N\orth</math> is [[Positive formula|positive]].

== Negative connectives ==

A connective <math>c</math> of arity <math>n</math> is ''negative'' if for any negative formulas <math>N_1</math>,...,<math>N_n</math>, <math>c(N_1,\dots,N_n)</math> is negative.

{{Proposition|title=Negative connectives|
<math>\parr</math>, <math>\bot</math>, <math>\with</math>, <math>\top</math>, <math>\wn</math> and <math>\forall</math> are negative connectives.
}}

{{Proof|
This is equivalent to the fact that <math>\tens</math>, <math>\one</math>, <math>\plus</math>, <math>\zero</math>, <math>\oc</math> and <math>\exists</math> are [[Positive formula#Positive connectives|positive connectives]].
}}

More generally, <math>\wn A</math> is negative for any formula <math>A</math>.

The notion of negative connective is related with but different from the notion of [[synchronous connective]].

== Generalized structural rules ==

Negative formulas admit generalized right structural rules corresponding to a structure of [[Wikipedia:Monoid (category theory)|<math>\parr</math>-monoid]]: <math>N\parr N\limp N</math> and <math>\bot\limp N</math>. The following rule is derivable:

<math>
\AxRule{\Gamma\vdash N,N,\Delta}
\LabelRule{- c R}
\UnaRule{\Gamma\vdash N,\Delta}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash\Delta}
\LabelRule{- w R}
\UnaRule{\Gamma\vdash N,\Delta}
\DisplayProof
</math>

{{Proof|
This is equivalent to the [[Positive formula#Generalized structural rules|generalized left structural rules]] for positive formulas.
}}

Negative formulas are also acceptable in the context of the promotion rule. The following rule is derivable:

<math>
\AxRule{\vdash A,N_1,\dots,N_n}
\LabelRule{- \oc R}
\UnaRule{\vdash \oc{A},N_1,\dots,N_n}
\DisplayProof
</math>

{{Proof|
This is equivalent to the possibility of having positive formulas in the [[Positive formula#Generalized structural rules|left-hand side context of the promotion rule]].
}}

List of equivalences

2013-10-28T14:43:03Z

Olivier Laurent: Correction of useless corrections

Each [[List of isomorphisms|isomorphism]] gives an equivalence of formulas.
The following equivalences are ''not'' isomorphisms.

== Multiplicatives ==

<math>
\begin{array}{rcccl}
A &\linequiv& A \tens (A\orth\parr A) &\linequiv& (A\tens A\orth)\parr A \\
& & A\parr A\orth &\linequiv& (A\parr A\orth)\tens(A\parr A\orth)
\end{array}
</math>

== Additives ==

<math>
\begin{array}{rclcrcl}
A \with A &\linequiv& A \\
A \plus A &\linequiv& A \\
\\
A \with (A \plus B) &\linequiv& A &\quad& A \plus \top &\linequiv& \top \\
A \plus (A \with B) &\linequiv& A &\quad& A \with \zero &\linequiv& \zero
\end{array}
</math>

== Quantifiers ==

<math>
\begin{array}{rcll}
\forall X.A &\linequiv& A &\quad (X\notin A) \\
\exists X.A &\linequiv& A &\quad (X\notin A)
\end{array}
</math>

== Exponentials ==

<math>
\begin{array}{rclcrcl}
\oc A &\linequiv& \oc A\tens\oc A &\quad&
\wn A &\linequiv& \wn A\parr\wn A\\
\oc A &\linequiv& \oc\oc A &\quad& \wn A &\linequiv& \wn\wn A\\
\oc\wn A &\linequiv& \oc\wn\oc\wn A &\quad& \wn\oc A &\linequiv& \wn\oc\wn\oc A\\
\end{array}
</math>

Some of these equivalences are related with the [[lattice of exponential modalities]].

== Polarities ==

{|
| <math> \wn N \linequiv N </math>
|   (N [[Negative formula|negative]])
|-
| <math> \oc P \linequiv P </math>
|   (P [[Positive formula|positive]])
|-
| <math> \wn\oc R \linequiv R </math>
|   (R [[Regular formula|regular]])
|-
| <math> \oc\wn L \linequiv L </math>
|   (L [[Co-regular formula|co-regular]])
|}

== Second order encodings ==

<math>
\begin{array}{rclcrcl}
A &\linequiv &\forall X . (A \tens X\orth) \parr X \\
A &\linequiv &\exists X . (A \parr X\orth) \tens X \\
\\
A \with B &\linequiv& \exists X . \oc{(A \parr X\orth)} \tens \oc{(B \parr X\orth)} \tens X &\quad& \top &\linequiv& \exists X . X \\
A \plus B &\linequiv& \forall X . \wn{(A \tens X\orth)} \parr \wn{(B \tens X\orth)} \parr X &\quad& \zero &\linequiv& \forall X . X \\
\\
\bot &\linequiv& \exists X . X\tens X\orth \\
\one &\linequiv& \forall X . X\orth\parr X \\
\\
\forall \xi . A &\linequiv& \exists X . (\forall \xi . (A \parr X\orth)) \tens X \\
\exists \xi . A &\linequiv& \forall X . (\exists \xi . (A \tens X\orth)) \parr X
\end{array}
</math>

== Miscellaneous ==

<math>
\begin{array}{rcl}
\one &\linequiv& \oc{(A\orth\parr A)} \\
\bot &\linequiv& \wn{(A\orth\tens A)} \\
\\
\oc{\wn{(\oc{A}\with\oc{B})}} &\linequiv& \oc{(\wn{\oc{A}}\with\wn{\oc{B}})} \\
\wn{\oc{(\wn{A}\plus\wn{B})}} &\linequiv& \wn{(\oc{\wn{A}}\plus\oc{\wn{B}})}
\end{array}
</math>

Mix

2013-10-27T13:59:24Z

Olivier Laurent: Definition and main properties of the mix rules

The usual notion of <math>\rulename{Mix}</math> is the binary version of the rule but a nullary version also exists.

== Binary <math>\rulename{Mix}</math> rule ==

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

The <math>\rulename{Mix_2}</math> rule is equivalent to <math>\bot\vdash\one</math>:

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

They are also equivalent to the principle <math>A\tens B \vdash A\parr B</math>:

<math>
\LabelRule{\one}
\NulRule{\vdash\one}
\LabelRule{\one}
\NulRule{\vdash\one}
\LabelRule{\tens}
\BinRule{\vdash\one\tens\one}
\AxRule{\vdash\bot\parr\bot,\one\parr\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\one\parr\one}
\LabelRule{\rulename{ax}}
\NulRule{\vdash\bot,\one}
\LabelRule{\rulename{ax}}
\NulRule{\vdash\bot,\one}
\LabelRule{\tens}
\BinRule{\vdash\bot\tens\bot,\one,\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\one,\one}
\DisplayProof
\qquad
\LabelRule{\rulename{ax}}
\NulRule{\vdash A\orth,A}
\LabelRule{\rulename{ax}}
\NulRule{\vdash B\orth,B}
\LabelRule{Mix_2}
\BinRule{\vdash A\orth,A,B\orth,B}
\LabelRule{\parr}
\UnaRule{\vdash A\orth,B\orth,A\parr B}
\LabelRule{\parr}
\UnaRule{\vdash A\orth\parr B\orth,A\parr B}
\DisplayProof
</math>

== Nullary <math>\rulename{Mix}</math> rule ==

<math>
\LabelRule{Mix_0}
\NulRule{\vdash}
\DisplayProof
</math>

The <math>\rulename{Mix_0}</math> rule is equivalent to <math>\one\vdash\bot</math>:

<math>
\LabelRule{Mix_0}
\NulRule{\vdash}
\LabelRule{\bot}
\UnaRule{\vdash\bot}
\LabelRule{\bot}
\UnaRule{\vdash\bot,\bot}
\DisplayProof
\qquad
\LabelRule{\one}
\NulRule{\vdash\one}
\AxRule{\vdash\bot,\bot}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\bot}
\LabelRule{\one}
\NulRule{\vdash\one}
\LabelRule{\rulename{cut}}
\BinRule{\vdash}
\DisplayProof
</math>

The nullary <math>\rulename{Mix}</math> acts as a unit for the binary one:

<math>
\AxRule{\vdash\Gamma}
\LabelRule{Mix_0}
\NulRule{\vdash}
\LabelRule{Mix_2}
\BinRule{\vdash\Gamma}
\DisplayProof
</math>

If <math>\pi</math> is a proof which uses no <math>\bot</math> rule and no weakening rule, then (up to the simplification of the pattern <math>\rulename{Mix_0}/\rulename{Mix_2}</math> above into nothing) <math>\pi</math> is either reduced to a <math>\rulename{Mix_0}</math> rule or does not contain any <math>\rulename{Mix_0}</math> rule.

List of isomorphisms

2013-04-25T19:48:16Z

Olivier Laurent: Quantifiers added

== Linear negation ==

<math>
\begin{array}{rclcrcl}
A\biorth &\cong& A\\
(A\tens B)\orth &\cong& A\orth\parr B\orth &\quad& \one\orth &\cong& \bot\\
(A\parr B)\orth &\cong& A\orth\tens B\orth &\quad& \bot\orth &\cong& \one\\
(A\with B)\orth &\cong& A\orth\plus B\orth &\quad& \top\orth &\cong& \zero\\
(A\plus B)\orth &\cong& A\orth\with B\orth &\quad& \zero\orth &\cong& \top\\
(\oc A)\orth &\cong& \wn A\orth\\
(\wn A)\orth &\cong& \oc A\orth\\
\end{array}
</math>

== Neutrals ==

<math>
\begin{array}{rcl}
A\tens\one &\cong& \one\tens A\cong A\\
A\parr\bot &\cong& \bot\parr A\cong A\\
A\with\top &\cong& \top\with A\cong A\\
A\plus\zero &\cong&\zero\plus A\cong A\\
\end{array}
</math>

== Commutativity ==

<math>
\begin{array}{rcl}
A\tens B &\cong& B\tens A\\
A\parr B &\cong& B\parr A\\
A\with B &\cong& B\with A\\
A\plus B &\cong& B\plus A\\
\end{array}
</math>

== Associativity ==

<math>
\begin{array}{rcl}
(A\tens B)\tens C &\cong& A\tens(B\tens C)\\
(A\parr B)\parr C &\cong& A\parr(B\parr C)\\
(A\with B)\with C &\cong& A\with(B\with C)\\
(A\plus B)\plus C &\cong& A\plus(B\plus C)\\
\end{array}
</math>

== Multiplicative-additive distributivity ==

<math>
\begin{array}{rclcrcl}
A\tens(B\plus C) &\cong& (A\tens B)\plus(A\tens C) &\quad&
A\tens\zero &\cong& \zero\\
A\parr(B\with C) &\cong& (A\parr B)\with(A\parr C) &\quad&
A\parr\top &\cong& \top\\
\end{array}
</math>

== Linear implication ==

<math>
\begin{array}{rclcrcl}
A\limp B &\cong& A\orth\parr B\\
A\limp B &\cong& B\orth\limp A\orth\\
A\tens B \limp C &\cong& A\limp B \limp C\\
\end{array}
</math>

== The exponential isomorphisms ==

<math>
\begin{array}{rclcrcl}
\oc(A\with B) &\cong& \oc A\tens\oc B &\quad& \oc\top &\cong& \one\\
\wn(A\plus B) &\cong& \wn A\parr\wn B &\quad& \wn\zero &\cong& \bot\\
\end{array}
</math>

== Quantifiers ==

<math>
\begin{array}{rclcrcl}
\forall \xi_1. \forall\xi_2. A &\cong& \forall\xi_2. \forall\xi_1. A\\
\exists \xi_1. \exists\xi_2.A &\cong& \exists\xi_2.\exists\xi_1.A\\
\\
\forall \xi . (A \parr B) &\cong& A \parr \forall \xi.B \quad (\xi\notin A) \\
\exists \xi . (A \tens B) &\cong& A \tens \exists \xi.B \quad (\xi\notin A) \\
\\
\forall \xi . (A \with B) &\cong& (\forall \xi . A) \with (\forall \xi . B) & & \forall \xi . \top &\cong& \top \\
\exists \xi . (A \plus B) &\cong& (\exists \xi . A) \plus (\exists \xi . B) & & \exists \xi . \zero &\cong& \zero
\end{array}
</math>

Reversibility and focalization

2012-08-31T21:10:58Z

Emmanuel Beffara: /* Focalization */ improved terminology

== Reversibility ==

{{Theorem|
Negative connectives are reversible:

* A sequent <math>\vdash\Gamma,A\parr B</math> is provable if and only if <math>\vdash\Gamma,A,B</math> is provable.
* A sequent <math>\vdash\Gamma,A\with B</math> is provable if and only if <math>\vdash\Gamma,A</math> and <math>\vdash\Gamma,B</math> are provable.
* A sequent <math>\vdash\Gamma,\bot</math> is provable if and only if <math>\vdash\Gamma</math> is provable.
* A sequent <math>\vdash\Gamma,\forall\xi A</math> is provable if and only if <math>\vdash\Gamma,A</math> is provable, for some fresh variable <math>\xi</math>.
}}

{{Proof|
We start with the case of the <math>\parr</math> connective.
If <math>\vdash\Gamma,A,B</math> is provable, then by the introduction rule for <math>\parr</math>
we know that <math>\vdash\Gamma,A\parr B</math> is provable.
For the reverse implication we proceed by induction on a proof <math>\pi</math> of
<math>\vdash\Gamma,A\parr B</math>.

* If the last rule of <math>\pi</math> is the introduction of the <math>\parr</math> in <math>A\parr B</math>, then the premiss is exacty <math>\vdash\Gamma,A,B</math> so we can conclude.
* The other case where the last rule introduces <math>A\parr B</math> is when <math>\pi</math> is an axiom rule, hence <math>\Gamma=A\orth\tens B\orth</math>. Then we can conclude with the proof
* Otherwise <math>A\parr B</math> is in the context of the last rule. If the last rule is a tensor, then <math>\pi</math> has the shape
* or the same with <math>A\parr B</math> in the conclusion of <math>\pi_2</math> instead. By induction hypothesis on <math>\pi_1</math> we get a proof <math>\pi'_1</math> of <math>\vdash\Gamma_1,A,B,C</math>, then we can conclude with the proof
* The case of the cut rule has the same structure as the tensor rule.
* In the case of the <math>\with</math> rule, we have <math>A\with B</math> in both premisses and we conclude similarly, using the induction hypothesis on both <math>\pi_1</math> and <math>\pi_2</math>.
* If <math>A\parr B</math> is in the context of a rules for <math>\parr</math>, <math>\plus</math>, <math>\bot</math> or quantifiers, or in the context of a dereliction, weakening or contraction, the situation is similar as for <math>\tens</math> except that we have only one premiss.
* If <math>A\parr B</math> is in the context of <math>\top</math> rules, we can freely change the context of the rule to get the expected one.
* The two remaining cases are if the last rule is the rule for <math>1</math> or a promotion. By the constraints these rules impose on the contexts, these cases cannot happen.
The <math>\with</math> connective is treated in the same way.
In this cases where <math>A\with B</math> is in the context of a rule with two
premisses, the premiss where this formula is not present will be duplicated,
with one copy in the premiss for <math>A</math> and one in the premiss for <math>B</math>.

The <math>\forall</math> connective is also treated similarly.
Its peculiarity is that introducing <math>\forall\xi</math> requires that <math>\xi</math> does
not appear free in the context.
For all rules with one premiss except the quantifier rules, the set of fresh
variables in the same in the premiss and the conclusion, so everything works
well.
Other rules might change the set of free variables, but problems are avoided
by choosing for <math>\xi</math> a variable that is fresh for the whole proof we are
considering.
}}

Remark that this result is proved using only commutation rules, except when the
formula is introduced by an axiom rule.
Furthermore, if axioms are applied only on atoms, this particular case
disappears.

A consequence of this fact is that, when searching for a proof of some
sequent <math>\vdash\Gamma</math>, one can always start by decomposing negative
connectives in <math>\Gamma</math> without losing provability.
Applying this result to successive connectives, we can get generalized
formulations for more complex formulas. For instance:

* <math>\vdash\Gamma,(A\parr B)\parr(B\with C)</math> is provable
* iff <math>\vdash\Gamma,A\parr B,B\with C</math> is provable
* iff <math>\vdash\Gamma,A\parr B,B</math> and <math>\vdash\Gamma,A\parr B,C</math> are provable
* iff <math>\vdash\Gamma,A,B,B</math> and <math>\vdash\Gamma,A,B,C</math> are provable
So without loss of generality, we can assume that any proof of
<math>\vdash\Gamma,(A\parr B)\parr(B\with C)</math> ends like

<math>
\AxRule{ \vdash \Gamma, A, B, B }
\UnaRule{ \vdash \Gamma, A\parr B, B }
\AxRule{ \vdash \Gamma, A, B, C }
\UnaRule{ \vdash \Gamma, A\parr B, C }
\BinRule{ \vdash \Gamma, A\parr B, B\with C }
\UnaRule{ \vdash \Gamma, (A\parr B)\parr(B\with C) }
\DisplayProof
</math>

In order to define a general statement for compound formulas, as well as an
analogous result for positive connectives, we need to give a proper status to
clusters of connectives of the same polarity.

== Generalized connectives and rules ==

{{Definition|
A ''positive generalized connective'' is a parametrized formula
<math>P[X_1,\ldots,X_n]</math> made from the variables <math>X_i</math> using the connectives
<math>\tens</math>, <math>\plus</math>, <math>\one</math>, <math>\zero</math>.

A ''negative generalized connective'' is a parametrized formula
<math>N[X_1,\ldots,X_n]</math> made from the variables <math>X_i</math> using the connectives
<math>\parr</math>, <math>\with</math>, <math>\bot</math>, <math>\top</math>.

If <math>C[X_1,\ldots,X_n]</math> is a generalized connectives (of any polarity), the
''dual'' of <math>C</math> is the connective <math>C^*</math> such that
<math>C^*[X_1\orth,\ldots,X_n\orth]=C[X_1,\ldots,X_n]\orth</math>.
}}

It is clear that dualization of generalized connectives is involutive and
exchanges polarities.
We do not include quantifiers in this definition, mainly for simplicity.
Extending the notion to quantifiers would only require taking proper care of
the scope of variables.

Sequent calculus provides introduction rules for each connective. Negative
connectives have one rule, positive ones may have any number of rules, namely
2 for <math>\plus</math> and 0 for <math>\zero</math>. We can derive introduction rules for the
generalized connectives by combining the different possible introduction rules
for each of their components.

Considering the previous example
<math>N[X_1,X_2,X_3]=(X_1\parr X_2)\parr(X_2\with X_3)</math>, we can derive an
introduction rule for <math>N</math> as

<math>
\AxRule{ \vdash \Gamma, X_1, X_2, X_2 }
\UnaRule{ \vdash \Gamma, X_1\parr X_2, X_2 }
\AxRule{ \vdash \Gamma, X_1, X_2, X_3 }
\UnaRule{ \vdash \Gamma, X_1\parr X_2, X_3 }
\BinRule{ \vdash \Gamma, X_1\parr X_2, X_2\with X_3 }
\UnaRule{ \vdash \Gamma, (X_1\parr X_2)\parr(X_2\with X_3) }
\DisplayProof
\quad\text{or}\quad
\AxRule{ \vdash \Gamma, X_1, X_2, X_2 }
\AxRule{ \vdash \Gamma, X_1, X_2, X_3 }
\BinRule{ \vdash \Gamma, X_1, X_2, X_2\with X_3 }
\UnaRule{ \vdash \Gamma, X_1\parr X_2, X_2\with X_3 }
\UnaRule{ \vdash \Gamma, (X_1\parr X_2)\parr(X_2\with X_3) }
\DisplayProof
</math>

but these rules only differ by the commutation of independent rules.
In particular, their premisses are the same.
The dual of <math>N</math> is <math>P[X_1,X_2,X_3]=(X_1\tens X_2)\tens(X_2\plus X_3)</math>, for
which we have two possible derivations:

<math>
\AxRule{ \vdash \Gamma_1, X_1 }
\AxRule{ \vdash \Gamma_2, X_2 }
\BinRule{ \vdash \Gamma_1, \Gamma_2, X_1\tens X_2 }
\AxRule{ \vdash \Gamma_3, X_2 }
\UnaRule{ \vdash \Gamma_3, X_2\plus X_3 }
\BinRule{ \vdash \Gamma_1, \Gamma_2, \Gamma_3, (X_1\tens X_2)\tens(X_2\plus X_3) }
\DisplayProof
\qquad
\AxRule{ \vdash \Gamma_1, X_1 }
\AxRule{ \vdash \Gamma_2, X_2 }
\BinRule{ \vdash \Gamma_1, \Gamma_2, X_1\tens X_2 }
\AxRule{ \vdash \Gamma_3, X_3 }
\UnaRule{ \vdash \Gamma_3, X_2\plus X_3 }
\BinRule{ \vdash \Gamma_1, \Gamma_2, \Gamma_3, (X_1\tens X_2)\tens(X_2\plus X_3) }
\DisplayProof
</math>

These are actually different, in particular their premisses differ.
Each possible derivation corresponds to the choice of one side of the <math>\plus</math>
connective.

We can remark that the branches of the negative inference precisely correspond
to the possible positive inferences:

* the first branch of the negative inference has a premiss <math>X_1,X_2,X_2</math> and the first positive inference has three premisses, holding <math>X_1</math>, <math>X_2</math> and <math>X_2</math> respectively.
* the second branch of the negative inference has a premiss <math>X_1,X_2,X_3</math> and the second positive inference has three premisses, holding <math>X_1</math>, <math>X_2</math> and <math>X_3</math> respectively.
This phenomenon extends to all generalized connectives.

{{Definition|
The ''branching'' of a generalized connective <math>P[X_1,\ldots,X_n]</math> is the
multiset <math>\mathcal{I}_P</math> of multisets over <math>\{1,\ldots,n\}</math> defined
inductively as

<math> \mathcal{I}_{P\tens Q} := [ I+J \mid I\in\mathcal{I}_P, J\in\mathcal{I}_Q ] </math>,
<math> \mathcal{I}_{P\plus Q} := \mathcal{I}_P + \mathcal{I}_Q </math>,
<math> \mathcal{I}_\one := [[]] </math>,
<math> \mathcal{I}_\zero := [] </math>,
<math> \mathcal{I}_{X_i} := [[i]] </math>.

The branching of a negative generalized connective is the branching of its
dual. Elements of a branching are called branches.
}}

In the example above, the branching will be <math>[[1,2,2],[1,2,3]]</math>, which
corresponds to the granches of the negative inference and to the cases of
positive inference.

{{Definition|
Let <math>\mathcal{I}</math> be a branching.
Write <math>\mathcal{I}</math> as <math>[I_1,\ldots,I_k]</math> and write each <math>I_j</math> as
<math>[i_{j,1},\ldots,i_{j,\ell_j}]</math>.
The derived rule for a negative generalized connective <math>N</math> with
branching <math>\mathcal{I}</math> is

<math>
\AxRule{ \vdash \Gamma, A_{i_{1,1}}, \ldots, A_{i_{1,\ell_1}} }
\AxRule{ \cdots }
\AxRule{ \vdash \Gamma, A_{i_{k,1}}, \ldots, A_{i_{k,\ell_k}} }
\LabelRule{N}
\TriRule{ \vdash \Gamma, N[A_1,\ldots,A_n] }
\DisplayProof
</math>

For each branch <math>I=[i_1,\ldots,i_\ell]</math> of a positive generalized connective
<math>P</math>, the derived rule for branch <math>I</math> of <math>P</math> is

<math>
\AxRule{ \vdash \Gamma_1, A_{i_1} }
\AxRule{ \cdots }
\AxRule{ \vdash \Gamma_\ell, A_{i_\ell} }
\LabelRule{P_I}
\TriRule{ \vdash \Gamma_1, \ldots, \Gamma_\ell, P[A_1,\ldots,A_n] }
\DisplayProof
</math>
}}

The reversibility property of negative connectives can be rephrased in a
generalized way as

{{Theorem|
Let <math>N</math> be a negative generalized connective. A sequent
<math>\vdash\Gamma,N[A_1,\ldots,A_n]</math> is provable if and only if, for each
<math>[i_1,\ldots,i_k]\in\mathcal{I}_N</math>, the sequent
<math>\vdash\Gamma,A_{i_1},\ldots,A_{i_k}</math> is provable.
}}

The corresponding property for positive connectives is the focalization
property, defined in the next section.

== Focalization ==

{{Definition|
A formula is ''positive'' if it has a main connective among
<math>\tens</math>, <math>\plus</math>, <math>\one</math>, <math>\zero</math>.
It is called ''negative'' if it has a main connective among
<math>\parr</math>, <math>\with</math>, <math>\bot</math>, <math>\top</math>.
It is called ''neutral'' if it is neither positive nor negative.
}}

If we extended the theory to include quantifiers in generalized connectives,
then the definition of positive and negative formulas would be extended to
include them too.

{{Definition|
A proof <math>\pi\vdash\Gamma,A</math> is said to be ''positively focused on <math>A</math>'' if it has the shape

<math>
\AxRule{ \pi_1 \vdash \Gamma_1, A_{i_1} }
\AxRule{ \cdots }
\AxRule{ \pi_\ell \vdash \Gamma_\ell, A_{i_\ell} }
\LabelRule{P_{[i_1,\ldots,i_\ell]}}
\TriRule{ \vdash \Gamma_1, \ldots, \Gamma_\ell, P[A_1,\ldots,A_n] }
\DisplayProof
</math>

where <math>P</math> is a positive generalized connective, the <math>A_i</math> ar non-positive
and <math>A=P[A_1,\ldots,A_n]</math>. The formula <math>A</math> is called the ''focus'' of the
proof <math>\pi</math>.
}}

In other words, a proof is positively focused on a conclusion <math>A</math> if its last rules
build <math>A</math> from some of its non-positive subformulas in one cluster of
inferences. Note that this notion only makes sense for a sequent made only
of positive formulas, since by this definition a proof is obviously positively focused on
any of its non-positive conclusions, using the degenerate generalized
connective <math>P[X]=X</math>.

{{Theorem|
A sequent <math>\vdash\Gamma</math> is cut-free provable if and only if it is provable
by a cut-free proof that is positively focused.
}}

{{Proof|
We reason by induction on a proof <math>\pi</math> of <math>\Gamma</math>.
As noted above, the result trivially holds if <math>\Gamma</math> has a non-positive
formula.
We can thus assume that <math>\Gamma</math> contains only positive formulas and reason
on the nature of the last rule, which is necessarily the introduction of a
positive connective (it cannot be an axiom rule because an axiom always has
at least on non-positive conclusion).

Suppose that the last rule of <math>\pi</math> introduces a tensor, so that <math>\pi</math> is

<math>
\AxRule{ \rho \vdash \Gamma, A }
\AxRule{ \theta \vdash \Delta, B }
\BinRule{ \vdash \Gamma, \Delta, A\tens B }
\DisplayProof
</math>

By induction hypothesis, there are positively focused proofs <math>\rho'\vdash\Gamma,A</math>
and <math>\theta'\vdash\Delta,B</math>.
If <math>A</math> is the focus of <math>\rho'</math> and <math>B</math> is the focus of <math>\theta'</math>, then the
proof

<math>
\AxRule{ \rho' \vdash \Gamma, A }
\AxRule{ \theta' \vdash \Delta, B }
\BinRule{ \vdash \Gamma, \Delta, A\tens B }
\DisplayProof
</math>

is positively focused on <math>A\tens B</math>, so we can conclude.
Otherwise, one of the two proofs is positively focused on another conclusion.
Without loss of generality, suppose that <math>\rho'</math> is not positively focused on <math>A</math>.
Then it decomposes as

<math>
\AxRule{ \rho_1 \vdash \Gamma_1, C_{i_1} }
\AxRule{ \cdots }
\AxRule{ \rho_\ell \vdash \Gamma_\ell, C_{i_\ell} }
\TriRule{ \vdash \Gamma_1, \ldots, \Gamma_\ell, P[C_1,\ldots,C_n] }
\DisplayProof
</math>

where the <math>C_i</math> are not positive and <math>A</math> belongs to some context <math>\Gamma_j</math>
that we will write <math>\Gamma'_j,A</math>.
Then we can conclude with the proof

<math>
\AxRule{ \rho_1 \vdash \Gamma_1, C_{i_1} \quad\cdots }
\AxRule{ \rho_j \vdash \Gamma_j, A, C_{i_j} }
\AxRule{ \theta \vdash \Delta, B }
\BinRule{ \vdash \Gamma_j, \Delta, A\tens B, C_{i_j} }
\AxRule{ \cdots\quad \rho_\ell \vdash \Gamma_\ell, C_{i_\ell} }
\TriRule{ \vdash \Gamma_1, \ldots, \Gamma_\ell, \Delta, A\tens B, P[C_1,\ldots,C_n] }
\DisplayProof
</math>

which is positively focused on <math>P[C_1,\ldots,C_n]</math>.

If the last rule of <math>\pi</math> introduces a <math>\plus</math>, we proceed the same way
except that there is only one premiss.
If the last rule of <math>\pi</math> introduces a <math>\one</math>, then it is the only rule of
<math>\pi</math>, which is thus positively focused on this <math>\one</math>.
}}

As in the reversibility theorem, this proof only makes use of commutation of
independent rules.

These results say nothing about exponential modalities, because they respect
neither reversibility nor focalization. However, if we consider the fragment
of LL which consists only of multiplicative and additive connectives, we can
restrict the proof rules to enforce focalization without loss of
expressiveness.

Proof-nets

2012-08-30T23:43:00Z

Lionel Vaux: fix wording

We provide [[a formal account of nets]], but it is probably not the best way to learn about proof-nets if you have never seen them before.

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}}

Non provable formulas

2012-04-19T18:49:35Z

Olivier Laurent: Added some exponential cases (in relation with the Lattice of exponential modalities)

{{stub}}

<math>A \with (B\plus C) \not\limp (A\with B)\plus (A\with C)</math>

<math>(A\plus B)\with (A\plus C) \not\limp A\plus (B\with C)</math>

<math>(A\tens B)\parr C \not\limp A\tens (B\parr C)</math>

<math>A \not\limp \oc{A}</math>

<math>\oc{\wn{\oc{A}}} \not\limp A</math>

<math>\oc{\wn{\oc{A}}} \not\limp \oc{A}</math>

<math>\oc{\wn{A}} \not\limp \wn{\oc{A}}</math>

<math>\wn{\oc{A}} \not\limp \oc{\wn{A}}</math>

Provable formulas

2012-04-19T17:42:23Z

Olivier Laurent: Identites added

Important provable formulas are given by [[List of isomorphisms|isomorphisms]] and by [[List of equivalences|equivalences]].

In many of the cases below the [[Non provable formulas|converse implication does not hold]].

== Distributivities ==

=== Standard distributivities ===

<math>A\plus (B\with C) \limp (A\plus B)\with (A\plus C)</math>

<math>A\tens (B\with C) \limp (A\tens B)\with (A\tens C)</math>

<math>\exists \xi . (A \with B) \limp (\exists \xi . A) \with (\exists \xi . B)</math>

=== Linear distributivities ===

<math>A\tens (B\parr C) \limp (A\tens B)\parr C</math>

<math>\exists \xi. (A \parr B) \limp A \parr \exists \xi.B \quad (\xi\notin A)</math>

<math>A \tens \forall \xi.B \limp \forall \xi. (A \tens B) \quad (\xi\notin A)</math>

== Factorizations ==

<math>(A\with B)\plus (A\with C) \limp A\with (B\plus C)</math>

<math>(A\parr B)\plus (A\parr C) \limp A\parr (B\plus C)</math>

<math>(\forall \xi . A) \plus (\forall \xi . B) \limp \forall \xi . (A \plus B)</math>

== Identities ==

<math>\one \limp A\orth\parr A</math>

<math>A\tens A\orth \limp\bot</math>

== Additive structure ==

<math>
\begin{array}{rclcrclcrcl}
A\with B &\limp& A &\quad& A\with B &\limp& B &\quad& A &\limp& \top\\
A &\limp& A\plus B &\quad& B &\limp& A\plus B &\quad& \zero &\limp& A
\end{array}
</math>

== Quantifiers ==

<math>
\begin{array}{rcll}
A &\limp& \forall \xi.A &\quad (\xi\notin A) \\
\exists \xi.A &\limp& A &\quad (\xi\notin A)
\end{array}
</math>

<br />

<math>
\begin{array}{rcl}
\forall \xi_1.\forall \xi_2. A &\limp& \forall \xi. A[^\xi/_{\xi_1},^\xi/_{\xi_2}] \\
\exists \xi.A[^\xi/_{\xi_1},^\xi/_{\xi_2}] &\limp& \exists \xi_1. \exists \xi_2.A
\end{array}
</math>

== Exponential structure ==

Provable formulas involving exponential connectives only provide us with the [[lattice of exponential modalities]].

<math>
\begin{array}{rclcrcl}
\oc A &\limp& A &\quad& A&\limp&\wn A\\
\oc A &\limp& 1 &\quad& \bot &\limp& \wn A
\end{array}
</math>

== Monoidality of exponentials ==

<math>
\begin{array}{rcl}
\wn(A\parr B) &\limp& \wn A\parr\wn B \\
\oc A\tens\oc B &\limp& \oc(A\tens B) \\
\\
\oc{(A \with B)} &\limp& \oc{A} \with \oc{B} \\
\wn{A} \plus \wn{B} &\limp& \wn{(A \plus B)} \\
\\
\wn{(A \with B)} &\limp& \wn{A} \with \wn{B} \\
\oc{A} \plus \oc{B} &\limp& \oc{(A \plus B)}
\end{array}
</math>

== Promotion principles ==

<math>
\begin{array}{rcl}
\oc{A} \tens \wn{B} &\limp& \wn{(A \tens B)} \\
\oc{(A \parr B)} &\limp& \wn{A} \parr \oc{B}
\end{array}
</math>

== Commutations ==

<math>\exists \xi . \wn A \limp \wn{\exists \xi . A}</math>

<math>\oc{\forall \xi . A} \limp \forall \xi . \oc A</math>

<math>\wn{\forall \xi . A} \limp \forall \xi . \wn A</math>

<math>\exists \xi . \oc A \limp \oc{\exists \xi . A}</math>

A formal account of nets

2012-02-15T16:16:29Z

Lionel Vaux: /* The short story */

The aim of this page is to provide a common framework for describing linear
logic proof nets, interaction nets, multiport interaction nets, and the likes,
while factoring out most of the tedious, uninteresting details (clearly not the
fanciest page of LLWiki).

== Preliminaries ==

=== The short story ===

* the general flavor is that of multiport interaction nets;
* the top/down or passive/active orientation of cells is related with the distinction between premisses and conclusions of rules, (and in that sense, a cut is not a logical rule, but the focus of interaction between two rules);
* cuts are thus wires rather than cells/links: this fits with the intuition of GoI, but not with the most common presentations of proof nets;
* because the notion of subnet is not trivial in multiport interaction nets, and to avoid the use of geometric conditions (boxes must not overlap but can be nested), we introduce boxes as particular cells;
* when representing proof nets, we introduce axioms explicitly as cells, so that axiom-cuts do not vanish.

== Nets ==

=== Wires ===

A ''wiring'' is the data of a finite set <math>P</math> of ports
and of a partition <math>{W}</math> of <math>P</math> by pairs (the ''wires''):
if <math>\{p,q\}\in{W}</math>, we write <math>{W}(p)=q</math> and <math>{W}(q)=p</math>.
Hence a wiring is equivalently given by
an involutive permutation <math>{W}</math> of finite domain <math>P</math>,
without fixpoints (forall <math>p</math>, <math>{W}(p)\not=p</math>): the wires are then
the orbits.
Another equivalent presentation is to consider <math>{W}</math> as
a (simple, loopless, undirected) graph, with vertices in P,
all of degree 1.

We say two wirings are disjoint when their sets of ports are.
A ''connection'' between two disjoint wirings <math>W</math> and <math>W'</math> is
a partial injection <math>(I,I',f):P\pinj P'</math>: <math>I\subseteq P</math>,
<math>I'\subseteq P'</math> and <math>f</math> is a bijection <math>I\cong I'</math>.
We then write <math>W\bowtie_f{{W}'}</math> for the wiring obtained
by identifying the ports pairwise mapped by <math>f</math>, and then
``straightening`` the paths thus obtained to recover wires:
notice this might also introduce loops and we write <math>\Inner{W}{W'}_f</math>
for the number of loops thus appeared.

We describe these operations a bit more formally.
Write <math>P = P_0\uplus I</math> and <math>P' = P_0'\uplus I'</math>.
Then consider the graph <math>W\dblcolon_f{{W}'}</math> with vertices in
<math>P\cup P'</math>, and such that
there is an edge between <math>p</math> and <math>q</math> iff
<math>q={W}(p)</math> or
<math>q={W'}(p)</math> or
<math>q=f(p)</math> or
<math>p=f(q)</math>:
in other words, <math>W\dblcolon_f{{W}'}=W\cup W'\cup f\cup f^{-1}</math>.
Vertices in <math>P_0\cup P'_0</math>
are of degree 1, and the others are of degree 2.
Hence maximal paths in <math>W\dblcolon_f{{W}'}</math> are of two kinds:

* straight paths, with both ends in <math>P_0\cup P_0'</math>;
* cycles, with vertices all in <math>I\cup I'</math>.
Then the wires in <math>W\bowtie_f{{W}'}</math> are the pairs <math>\{p,p'\}</math> such that
<math>p</math> and <math>p'</math> are the ends of a path in <math>W\dblcolon_f{{W}'}</math>.
And <math>\Inner{W}{W'}_{f}</math> is the number of
cycles in <math>W\dblcolon_f{{W}'}</math>, or more precisely
the number of support sets of cycles (i.e. we forget about the starting
vertice of cycles).

{{Lemma|
Consider three wirings <math>(P,W)</math>, <math>(P',W')</math> and <math>(P'',W'')</math>,
and two connections <math>(I,I',f):P\pinj P'</math> and
<math>(J',J'',g):P'\pinj P''</math> such that <math>I'\cap J'=\emptyset</math>.
Then

<math> (W\bowtie_f W')\bowtie_g W''=
W\bowtie_f(W'\bowtie_g W'')</math>

and

<math> \Inner{W}{W'}_{f}+\Inner{(W\bowtie_f{{W}'})}{{W}''}_g=
\Inner{W}{(W'\bowtie_g W'')}_f+\Inner{{W}'}{{W}''}_g.</math>
}}

{{Proof|
The first equation holds because open maximal paths in
<math>W\dblcolon_f{W'\bowtie_g}{{W}''}</math> correspond with those in
<math>W\dblcolon_f{(W'\dblcolon_g{{W}''})}</math>, hence in
<math>(W\dblcolon_f W')\dblcolon_g W''</math>, hence in
<math>{W\bowtie_f{{W}'}}\dblcolon_g{{W}''}</math>.
The second equation holds because both sides are two possible writings for
the number of loops in <math>{(W\dblcolon_f{{W}'})}\dblcolon_g{{W}''}</math>
}}

=== Nets ===

A ''signature'' is the data of a set
<math>\Sigma</math> of symbols, together with arity functions
<math>\alpha:\Sigma\to\mathbf{N}\setminus\{0\}</math> (number of
''active'' ports, or conclusions)
and <math>\pi:\Sigma\to\mathbf N</math> (number of
''passive'' ports, or hypotheses).
In the remaining, we assume
such a signature is given.

A ''cell'' <math>c</math> with ports in <math>P</math> is the data of
a symbol <math>\sigma\in\Sigma</math> and of two disjoint lists
of pairwise distinct ports:
<math>\alpha(c)\in P^{\alpha(\sigma)}</math>
is the list of ''active'' ports
and <math>\pi(c)\in P^{\pi(\sigma)}</math>
is the list of ''passive'' ports.

A ''net'' is the data of a wiring <math>(P,W)</math>, of a set <math>C</math> of disjoint cells on
<math>P</math>, and of a number <math>L\in\mathbf N</math> (the number of ''loops''). It follows
from the definitions that each port <math>p\in P</math> appears in exactly one wire and in
at most one cell: we say <math>p</math> is ''free'' if it is not part of a cell, and
<math>p</math> is ''internal'' otherwise. Moreover, we say <math>p</math> is ''dangling'' if
<math>p</math> is free and <math>W(p)</math> is internal. We write <math>\textrm{fp}(R)</math> for the set of
free ports of a net <math>R</math>.

Generally, the “names” of internal ports of a net are not relevant, but free
ports matter most often: internal ports are the analogue of bound variables in
<math>\lambda</math>-terms.
More formally, an ''isomorphism'' from net <math>R</math> to net <math>R'</math>
is the data of a bijection of ports <math>\phi:P\cong P'</math> and a bijection
of cells <math>\psi:C\cong C'</math> such that:

* for all <math>p\in P</math>, <math>W'(\phi(p))=\phi(W(p))</math>;
* for all <math>c\in C</math>:
** <math>\sigma_{\psi(c)}=\sigma_c</math>,
** for all <math>i\in\{0,\dotsc,\alpha(\sigma_c)-1\}</math>, <math>\alpha(\psi(c))_i=\phi(\alpha(c)_i)</math>,
** for all <math>j\in\{0,\dotsc,\pi(\sigma_c)-1\}</math>, <math>\pi(\psi(c))_j=\phi(\pi(c)_j)</math>;
* <math>L=L'</math>.
Observe that under these conditions <math>\psi</math> is uniquely induced by <math>\phi</math>.
We say that the isomorphism <math>\phi</math> is ''nominal'' if moreover <math>p\in\textrm{fp}(R)</math>
implies <math>p=\phi(p)</math>.

=== Subnets ===

We say two nets are disjoint when their sets of ports are.
Let <math>R</math> and <math>R'</math> be disjoint nets, and <math>(I,I',f)</math> be a
connection between <math>W</math> and <math>W'</math>, such that
<math>I\subseteq \textrm{fp}(R)</math> and <math>I'\subseteq \textrm{fp}(R')</math>.
We then write <math>R\bowtie_f{R'}</math> for the net
with wiring <math>W\bowtie_f{W'}</math>, cells
<math>C\cup C'</math> and loops <math>\Inner{R}{R'}_f=L+L'+\Inner{W}{W'}_f</math>.
We say this connection is ''orthogonal'' if <math>\Inner{W}{W'}_f=0</math>, and it is
''modular'' if the ports in <math>I\cup I'</math> are all dangling: a modular connection is
always orthogonal.

We say <math>R_0</math> is a ''subnet'' of <math>R</math>, if there exists a net <math>R'</math> and a connection
<math>(I,I',f)</math> between <math>R_0</math> and <math>R'</math> such that <math>R=R_0\bowtie_f{R'}</math>.

{{Lemma|
Let <math>R_0</math>, <math>R_1</math> and <math>R'</math> be nets such that <math>R_0</math> and <math>R_1</math>
are disjoint from <math>R</math>,
<math>(I,I',f)</math> be a connection <math>\textrm{fp}(R_0)\pinj \textrm{fp}(R')</math>
and <math>\phi</math> an isomorphism <math>R_0\cong R_1</math> such that
<math>\phi(p)=\phi(p')</math> for all <math>p\in\textrm{fp}(R_0)\setminus I</math>.
Then <math>R_0\bowtie_f{R'}</math> is nominally isomorphic to
<math>R_1\bowtie_{f\circ\phi^{-1}}{R'}</math>.
}}

=== Rewriting ===

A ''net rewriting rule'' is a pair <math>(r_0,r_1)</math> of nets
such that <math>\textrm{fp}(r_0)=\textrm{fp}(r_1)</math>. Then an instance of this rule
is a pair <math>(R_0,R_1)</math> such that there exist:

* nets <math>R'_0</math> and <math>R'_1</math> isomorphic to <math>r_0</math> and <math>r_1</math> respectively, namely <math>R'_i=\phi_i(r_i)</math>, so that moreover <math>\phi_0(p)=\phi_1(p)</math> for all <math>p\in\textrm{fp}(r_0)</math> (in particular, <math>\textrm{fp}(R'_0)=\textrm{fp}(R'_1)</math>);
* a net <math>R''</math>, disjoint from <math>R'_0</math> and <math>R'_1</math>;
* a connection <math>(\textrm{fp}(R'_0),J,f):\textrm{fp}(R'_0)\pinj \textrm{fp}(R'')</math>;
such that each <math>R_i</math> is nominally isomorphic to
<math>R'_i\bowtie_f{R''}</math>.

=== Typing ===

A typing system on signature <math>\Sigma</math> is the data of a
set <math>\Theta</math> of types, an involutive negation <math>\cdot\orth:\Theta\to\Theta</math>,
together with a typing discipline for each symbol, ''i.e.'' a relation
<math>\Theta(\sigma)\subseteq\Theta^{\alpha(\sigma)}\times\Theta^{\pi(\sigma)}</math>.
We then write <math>A_1,\cdots,A_{\pi(\sigma)}\vdash_\sigma
B_1,\cdots,B_{\alpha(\sigma)}</math> for <math>(\vec A,\vec B)\in\Theta(\sigma)</math>.

Then a ''typing'' for net <math>R=(P,W,C)</math> is a function <math>\tau:P\to \Theta</math>
such that:

* for all <math>p\in P</math>, <math>\tau(W(p))=\tau(p)\orth</math>;
* for all <math>c\in C</math> of symbol <math>\sigma</math>, <math>\tau(\pi(c))\vdash\tau(\alpha(c))\orth</math>;
where, in the last formula, we implicitly generalized
<math>\tau</math> to lists of ports and <math>\cdot\orth</math> to lists of formulas,
in the obvious, componentwise fashion.
The ''interface'' of the typed net <math>(R,\tau)</math> is then
the restriction of <math>\tau</math> to <math>\textrm{fp}(R)</math>.

The idea, is that a wire <math>\{p,q\}</math> bears the type <math>\tau(q)</math> (resp. <math>\tau(p)</math>) in
the direction <math>(p,q)</math> (resp. <math>(q,p)</math>), so that a rule
<math>\vec A\vdash_\sigma \vec B</math> reads as an inference from passive inputs (hypotheses)
to active outputs (conclusions).

Observe that if <math>(R,\tau)</math> is a typed net, and
<math>\phi:R\cong R'</math> is an isomorphism,
then <math>R'</math> is typed and its interface is <math>\tau\circ\phi^{-1}</math>:
in particular, if <math>\phi</math> is nominal, <math>R'</math> and <math>R</math> have the same interface.

Now let <math>(R,\tau)</math> and <math>(R',\tau')</math> be typed nets
and <math>(I,I',f)</math> a connection so that <math>\tau'\circ f</math> and
<math>\tau\orth=\cdot\orth\circ\tau</math> coincide on <math>I</math>.
Then this induces a typing of <math>R\bowtie_f{R'}</math>
preserving the interface on the remaining free ports.

=== Boxes ===

A signature with boxes is the data of a signature <math>\Sigma</math>, together
with a ''box arity'' <math>\beta(\sigma)</math> for all symbol
<math>\sigma\in\Sigma</math>.

Then a net on signature with boxes <math>(\Sigma,\beta)</math> is the same as a net
<math>R</math> on <math>\Sigma</math> plus, for each cell <math>c</math> of <math>R</math>, the data <math>\beta(c)</math> of a
<math>\beta(\sigma_c)</math>-tuple of nets (with boxes) with free ports the
internal ports of <math>c</math>.

Polarized linear logic

2011-10-04T22:47:47Z

Olivier Laurent: link to generalized structural rules

'''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 [[Positive_formula#Generalized_structural_rules|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 formula|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>

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>
}}

Terms of use

2011-02-17T11:14:55Z

Olivier Laurent: Protected "Terms of use": Administrative page [edit=sysop:move=sysop]

=== Information for contributors to the LLWiki ===

{{:Information for contributors}}

=== Information for users of the LLWiki ===

The content of the LLWiki is licensed under a ''Creative Commons Attribution-Noncommercial-Share Alike 2.0 France'' [http://creativecommons.org/licenses/by-nc-sa/2.0/fr/deed.en License].
This means you can share and adapt this content, under the following conditions:
* you must cite the ''“editorial board of the LLWiki”'' as the licensor;
* you may not use this content for commercial purposes;
* if you distribute a possibly modified version of this content, you must do so under the same or similar license.

=== Precedence of French terms ===

{{:Precedence of French terms}}

Conditions d'utilisation

2011-02-17T11:13:17Z

Olivier Laurent: Protected "Conditions d'utilisation": Administrative page [edit=sysop:move=sysop]

=== Information destinée aux contributeurs et futurs contributeurs du LLWiki ===

Le LLWiki est une œuvre collective créée sur l'initiative de son [[Editorial board|comité éditorial]].
Le comité éditorial est seul investi des droits sur le contenu de l'oeuvre collective.

Les contributeurs sont les personnes disposant d'un compte sur le LLWiki qui leur permet d'en éditer le contenu.
En demandant la création de leur compte, les candidats au statut de contributeur reconnaissent le droit exclusif du comité éditorial sur l'œuvre collective constituée par le LLWiki ; de plus, ils consentent à ce que leurs contributions soient distribuées selon les termes du [http://creativecommons.org/licenses/by-nc-sa/2.0/fr/ contrat] ''Creative Commons Paternité-Pas d'Utilisation Commerciale-Partage des Conditions Initiales à l'Identique'', version ''2.0 France'' avec le comité éditorial du LLWiki comme auteur.
Les contributeurs ne sont cependant pas privés pour autant de leurs droits sur leurs apports respectifs et restent libres de les exploiter individuellement.

=== Information destinée aux utilisateurs du projet LLWiki ===

Le contenu du LLWiki est mis à disposition sous un [http://creativecommons.org/licenses/by-nc-sa/2.0/fr/ contrat] ''Creative Commons Paternité-Pas d'Utilisation Commerciale-Partage des Conditions Initiales à l'Identique'', version ''2.0 France''.
Cela signifie que vous êtes libre de reproduire et distribuer ce contenu, y compris en le modifiant, tant que vous respectez les trois conditions suivantes :
* vous devez citer le ''« comité éditorial du LLWiki »'' comme l'auteur du LLWiki ;
* vous ne pouvez pas utiliser ce contenu à des fins commerciales ;
* si vous distribuez ce contenu ou une création dérivée de ce contenu vous devez le faire selon un contrat identique.

=== Prééminence de la version française ===
Les logiciels et contenus qui constituent le LLWiki sont hébergés en France.
En conséquence seule la présente version française des conditions d'utilisation
fait autorité et les éventuelles traductions ne sont proposées qu'à titre
indicatif.

Precedence of French terms

2011-02-17T11:10:40Z

Olivier Laurent: Protected "Precedence of French terms": Administrative page [edit=sysop:move=sysop]

The software and content that form the LLWiki are hosted in France.
Hence the official terms are given in the [[Conditions d'utilisation|French version of this page]] and this translation is only informative.
If there is any inconsistency between both texts, the French language version takes precedence.

Information for contributors

2011-02-17T11:08:23Z

Olivier Laurent: Protected "Information for contributors": Administrative page [edit=sysop:move=sysop]

The LLWiki is a collective work created under the authority of the [[Editorial board|editorial board]].
The editorial board is granted a monopoly of rights on the content of this collective work.

The contributors are the individuals owning an account on the LLWiki, which allows them to edit the content.
By applying for the creation of their account, the candidates to the status of contributor agree to grant the monopoly of rights on the LLWiki as a collective work to the editorial board; they moreover agree that their contributions are distributed under the terms of the ''Creative Commons Attribution-Noncommercial-Share Alike 2.0 France'' [http://creativecommons.org/licenses/by-nc-sa/2.0/fr/deed.en License], the editorial board being cited as the licensor.
The contributors however keep their rights on their respective contributions and are free to exploit them for their own sake.

Editorial board

2011-02-15T18:16:29Z

Olivier Laurent: Protected "Editorial board": Administrative page [edit=sysop:move=sysop]

The ''editorial board'' of the LLwiki is currently constituted of seven members:
* [http://iml.univ-mrs.fr/~beffara/ Emmanuel Beffara] (IML)
* [http://www.pps.jussieu.fr/~ehrhard/ Thomas Ehrhard] (PPS)
* [http://iml.univ-mrs.fr/~girard/ Jean-Yves Girard] (IML)
* [http://perso.ens-lyon.fr/olivier.laurent/ Olivier Laurent] (LIP)
* [http://www-lipn.univ-paris13.fr/~mazza/ Damiano Mazza] (LIPN)
* [http://iml.univ-mrs.fr/~regnier/ Laurent Regnier] (IML)
* [http://logica.uniroma3.it/~tortora/ Lorenzo Tortora de Falco] (Roma 3)

The size of the board is decided by its members.

In case of vacancy, new members of the editorial board are co-opted.

GoI for MELL: exponentials

2010-05-25T08:28:09Z

Laurent Regnier: definition of type !A

= The tensor product of Hilbert spaces =

Recall that we work in the Hilbert space <math>H=\ell^2(\mathbb{N})</math> endowed with its canonical hilbertian basis denoted by <math>(e_k)_{k\in\mathbb{N}}</math>.

The space <math>H\tens H</math> is the collection of sequences <math>(x_{np})_{n,p\in\mathbb{N}}</math> of complex numbers such that <math>\sum_{n,p}|x_{np}|^2</math> converges. The scalar product is defined just as before:
: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>.

If <math>x = (x_n)_{n\in\mathbb{N}}</math> and <math>y = (y_p)_{p\in\mathbb{N}}</math> are vectors in <math>H</math> then their tensor is the sequence:
: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>.

We define: <math>e_{np} = e_n\tens e_p</math> so that <math>e_{np}</math> is the sequence <math>(e_{npij})_{i,j\in\mathbb{N}}</math> of complex numbers given by <math>e_{npij} = \delta_{ni}\delta_{pj}</math>. By bilinearity of tensor we have:
: <math>x\tens y = \left(\sum_n x_ne_n\right)\tens\left(\sum_p y_pe_p\right) =
\sum_{n,p} x_ny_p\, e_n\tens e_p = \sum_{n,p} x_ny_p\,e_{np}</math>

Furthermore the system of vectors <math>(e_{np})</math> is a hilbertian basis of <math>H\tens H</math>: the sequence <math>x=(x_{np})_{n,p\in\mathbb{N}}</math> may be written:
: <math>x = \sum_{n,p\in\mathbb{N}}x_{np}\,e_{np}
= \sum_{n,p\in\mathbb{N}}x_{np}\,e_n\tens e_p</math>.

== An algebra isomorphism ==

Being both separable Hilbert spaces, <math>H</math> and <math>H\tens H</math> are isomorphic. We will now define explicitely an iso based on partial permutations.

We fix, once for all, a bijection from couples of natural numbers to natural
numbers that we will denote by <math>(n,p)\mapsto\langle n,p\rangle</math>. For
example set <math>\langle n,p\rangle = 2^n(2p+1) - 1</math>. Conversely, given
<math>n\in\mathbb{N}</math> we denote by <math>n_{(1)}</math> and
<math>n_{(2)}</math> the unique integers such that <math>\langle n_{(1)},
n_{(2)}\rangle = n</math>.

{{Remark|
just as it was convenient but actually not necessary to choose <math>p</math> and <math>q</math> so that <math>pp^* + qq^* = 1</math> it is actually not necessary to have a ''bijection'', a one-to-one mapping from <math>\mathbb{N}^2</math> ''into'' <math>\mathbb{N}</math> would be sufficient for our purpose.
}}

This bijection can be extended into a Hilbert space isomorphism <math>\Phi:H\tens H\rightarrow H</math> by defining:
: <math>e_n\tens e_p = e_{np} \mapsto e_{\langle n,p\rangle}</math>.

Now given an operator <math>u</math> on <math>H</math> we define the operator <math>!u</math> on <math>H</math> by:
: <math>!u(e_{\langle n,p\rangle}) = \Phi(e_n\tens u(e_p))</math>.

{{Remark|
The operator <math>!u</math> is defined by:
: <math>!u = \Phi\circ (1\tens u)\circ \Phi^{-1}</math>
where <math>1\tens u</math> denotes the operator on <math>H\tens H</math> defined by <math>(1\tens u)(x\tens y) = x\tens u(y)</math> for any <math>x,y</math> in <math>H</math>. However this notation must not be confused with the [[GoI for MELL: the *-autonomous structure#The tensor rule|tensor of operators]] that was defined in the previous section in order to interpret the tensor rule of linear logic; we therefore will not use it.
}}

One can check that given two operators <math>u</math> and <math>v</math> we have:
* <math>!u!v = {!(uv)}</math>;
* <math>!(u^*) = (!u)^*</math>.

Due to the fact that <math>\Phi</math> is an isomorphism ''onto'' we also have <math>!1=1</math>; this however will not be used.

We therefore have that <math>!</math> is a morphism on <math>\mathcal{B}(H)</math>; it is easily seen to be an iso (not ''onto'' though). As this is the crucial ingredient for interpreting the structural rules of linear logic, we will call it the ''copying iso''.

== Interpretation of exponentials ==

If we suppose that <math>u = u_\varphi</math> is a <math>p</math>-isometry generated by the partial permutation <math>\varphi</math> then we have:
: <math>!u(e_{\langle n,p\rangle}) = \Phi(e_n\tens u(e_p)) = \Phi(e_n\tens e_{\varphi(p)}) = e_{\langle n,\varphi(p)\rangle}</math>.
Thus <math>!u_\varphi</math> is itself a <math>p</math>-isometry generated by the
partial permutation <math>!\varphi:n\mapsto \langle n_{(1)}, \varphi(n_{(2)})\rangle</math>, which shows that the proof space is stable under the copying iso.

Given a type <math>A</math> we define the type <math>!A</math> by:
: <math>!A = \{!u, u\in A\}\biorth</math>

GoI for MELL: the *-autonomous structure

2010-05-15T11:04:03Z

Laurent Regnier: New page: Recall that when <math>u</math> and <math>v</math> are <math>p</math>-isometries we say they are dual when <math>uv</math> is nilpotent, and that <math>\bot</math> denotes the set of nilpo...

Recall that when <math>u</math> and <math>v</math> are <math>p</math>-isometries we say they are dual when <math>uv</math> is nilpotent, and that <math>\bot</math> denotes the set of nilpotent operators. A ''type'' is a subset of <math>\mathcal{P}</math> that is equal to its bidual. In particular <math>X\orth</math> is a type for any <math>X\subset\mathcal{P}</math>. We say that <math>X</math> ''generates'' the type <math>X\biorth</math>.

= The tensor and the linear application =

If <math>u</math> and <math>v</math> are two <math>p</math>-isometries summing them doesn't in general produces a <math>p</math>-isometry. However as <math>pup^*</math> and <math>qvq^*</math> have disjoint domains and disjoint codomains it is true that <math>pup^* + qvq^*</math> is a <math>p</math>-isometry. Given two types <math>A</math> and <math>B</math>, we thus define their ''tensor'' by:

: <math>A\tens B = \{pup^* + qvq^*, u\in A, v\in B\}\biorth</math>

Note the closure by bidual to make sure that we obtain a type.

From what precedes we see that <math>A\tens B</math> is generated by the internalizations of operators on <math>H\oplus H</math> of the form:
: <math>\begin{pmatrix}
u & 0\\
0 & v
\end{pmatrix}</math>

{{Remark|
This so-called tensor resembles a sum rather than a product. We will stick to this terminology though because it defines the interpretation of the tensor connective of linear logic.
}}

The linear implication is derived from the tensor by duality: given two types <math>A</math> and <math>B</math> the type <math>A\limp B</math> is defined by:
: <math>A\limp B = (A\tens B\orth)\orth</math>.

Unfolding this definition we get:
: <math>A\limp B = \{u\in\mathcal{P}\text{ s.t. } \forall v\in A, \forall w\in B\orth,\, u.(pvp^* + qwq^*) \in\bot\}</math>.

= The identity =

Given a type <math>A</math> we are to find an operator <math>\iota</math> in type <math>A\limp A</math>, thus satisfying:
: <math>\forall u\in A, v\in A\orth,\, \iota(pup^* + qvq^*)\in\bot</math>.

An easy solution is to take <math>\iota = pq^* + qp^*</math>. In this way we get <math>\iota(pup^* + qvq^*) = qup^* + pvq^*</math>. Therefore <math>(\iota(pup^* + qvq^*))^2 = quvq^* + pvup^*</math>, from which one deduces that this operator is nilpotent iff <math>uv</math> is nilpotent. It is the case since <math>u</math> is in <math>A</math> and <math>v</math> in <math>A\orth</math>.

It is interesting to note that the <math>\iota</math> thus defined is actually the internalization of the operator on <math>H\oplus H</math> given by the matrix:
: <math>\begin{pmatrix}0 & 1\\1 & 0\end{pmatrix}</math>.

We will see once the composition is defined that the <math>\iota</math> operator is the interpretation of the identity proof, as expected.

= The execution formula, version 1: application =

{{Definition|
Let <math>u</math> and <math>v</math> be two operators; as above denote by <math>u_{ij}</math> the external components of <math>u</math>. If <math>u_{11}v</math> is nilpotent we define the ''application of <math>u</math> to <math>v</math>'' by:
: <math>\mathrm{App}(u,v) = u_{22} + u_{21}v\sum_k(u_{11}v)^ku_{12}</math>.
}}

Note that the hypothesis that <math>u_{11}v</math> is nilpotent entails that the sum <math>\sum_k(u_{11}v)^k</math> is actually finite. It would be enough to assume that this sum converges. For simplicity we stick to the nilpotency condition, but we should mention that weak nilpotency would do as well.

{{Theorem|
If <math>u</math> and <math>v</math> are <math>p</math>-isometries such that <math>u_{11}v</math> is nilpotent, then <math>\mathrm{App}(u,v)</math> is also a <math>p</math>-isometry.
}}

{{Proof|
Let us note <math>E_k = u_{21}v(u_{11}v)^ku_{12}</math>. Recall that <math>u_{22}</math> and <math>u_{12}</math> being external components of the <math>p</math>-isometry <math>u</math>, they have disjoint domains. Thus it is also the case of <math>u_{22}</math> and <math>E_k</math>. Similarly <math>u_{22}</math> and <math>E_k</math> have disjoint codomains because <math>u_{22}</math> and <math>u_{21}</math> have disjoint codomains.

Let now <math>k</math> and <math>l</math> be two integers such that <math>k>l</math> and let us compute for example the intersection of the codomains of <math>E_k</math> and <math>E_l</math>:
: <math>
E_kE^*_kE_lE^*_l = (u_{21}v(u_{11}v)^ku_{12})(u^*_{12}(v^*u^*_{11})^kv^*u^*_{21})(u_{21}v(u_{11}v)^lu_{12})(u^*_{12}(v^*u^*_{11})^lv^*u_{21}^*)
</math>
As <math>k>l</math> we may write <math>(v^*u_{11}^*)^l = (v^*u^*_{11})^{k-l-1}v^*u^*_{11}(v^*u^*_{11})^l</math>. Let us note <math>E = u^*_{11}(v^*u^*_{11})^lv^*u_{21}^*u_{21}v(u_{11}v)^lu_{12}</math> so that <math>E_kE^*_kE_lE^*_l = u_{21}v(u_{11}v)^ku_{12}u^*_{12}(v^*u^*_{11})^{k-l-1}v^*Eu^*_{12}(v^*u^*_{11})^lv^*u_{21}^*</math>. We have:
: <math>\begin{align}
E &= u^*_{11}(v^*u^*_{11})^lv^*u_{21}^*u_{21}v(u_{11}v)^lu_{12}\\
&= (u^*_{11}u_{11}u^*_{11})(v^*u^*_{11})^lv^*u_{21}^*u_{21}v(u_{11}v)^lu_{12}\\
&= u^*_{11}(u_{11}u^*_{11})\bigl((v^*u^*_{11})^lv^*u_{21}^*u_{21}v(u_{11}v)^l\bigr)u_{12}\\
&= u^*_{11}\bigl((v^*u^*_{11})^lv^*u_{21}^*u_{21}v(u_{11}v)^l\bigr)(u_{11}u^*_{11})u_{12}\\
&= u^*_{11}(v^*u^*_{11})^lv^*u_{21}^*u_{21}v(u_{11}v)^lu_{11}u^*_{11}u_{12}\\
&= 0
\end{align}</math>
because <math>u_{11}</math> and <math>u_{12}</math> have disjoint codomains, thus <math>u^*_{11}u_{12} = 0</math>.

Similarly we can show that <math>E_k</math> and <math>E_l</math> have disjoint domains. Therefore we have proved that all terms of the sum <math>\mathrm{App}(u,v)</math> have disjoint domains and disjoint codomains. Consequently <math>\mathrm{App}(u,v)</math> is a <math>p</math>-isometry.
}}

{{Theorem|
Let <math>A</math> and <math>B</math> be two types and <math>u</math> a <math>p</math>-isometry. Then the two following conditions are equivalent:
# <math>u\in A\limp B</math>;
# for any <math>v\in A</math> we have:
#* <math>u_{11}v</math> is nilpotent and
#* <math>\mathrm{App}(u, v)\in B</math>.
}}

{{Proof|
Let <math>v</math> and <math>w</math> be two <math>p</math>-isometries. If we compute
: <math>(u.(pvp^* + qwq^*))^n = \bigl((pu_{11}p^* + pu_{12}q^* + qu_{21}p^* + qu_{22}q^*)(pvp^* + qwq^*)\bigr)^n</math>
we get a finite sum of monomial operators of the form:
# <math>p(u_{11}v)^{i_0}u_{12}w(u_{22}w)^{i_1}\dots u_{21}v(u_{11}v)^{i_m}p^*</math>
# <math>p(u_{11}v)^{i_0}u_{12}w(u_{22}w)^{i_1}\dots u_{12}w(u_{22}w)^{i_m}q^*</math>,
# <math>q(u_{22}w)^{i_0}u_{21}v(u_{11}v)^{i_1}\dots u_{21}v(u_{11}v)^{i_m}p^*</math> or
# <math>q(u_{22}w)^{i_0}u_{21}v(u_{11}v)^{i_1}\dots u_{12}w(u_{22}w)^{i_m}q^*</math>,
for all tuples of (nonnegative) integers <math>(i_1,\dots, i_m)</math> such that <math>i_0+\cdots+i_m+m = n</math>.

Each of these monomial is a <math>p</math>-isometry. Furthermore they have disjoint domains and disjoint codomains because their sum is the <math>p</math>-isometry <math>(u.(pvp^* + qwq^*))^n</math>. This entails that <math>(u.(pvp^* + qwq^*))^n = 0</math> iff all these monomials are null.

Suppose <math>u_{11}v</math> is nilpotent and consider:
: <math>\bigl(\mathrm{App}(u,v)w\bigr)^n = \biggl(\bigl(u_{22} + u_{21}v\sum_k(u_{11}v)^k u_{12}\bigr)w\biggr)^n</math>.
Developping we get a finite sum of monomials of the form:
: 5. <math>(u_{22}w)^{l_0}u_{21}v(u_{11}v)^{k_1}u_{12}w(u_{22}w)^{l_1}\dots u_{21}v(u_{11}v)^{k_m}u_{12}w(u_{22}w)^{l_m}</math>
for all tuples <math>(l_0, k_1, l_1,\dots, k_m, l_m)</math> such that <math>l_0\cdots l_m + m = n</math> and <math>k_i</math> is less than the degree of nilpotency of <math>u_{11}v</math> for all <math>i</math>.

Again as these monomials are <math>p</math>-isometries and their sum is the <math>p</math>-isometry <math>(\mathrm{App}(u,v)w)^n</math>, they have pairwise disjoint domains and pairwise disjoint codomains. Note that each of these monomial is equal to <math>q^*Mq</math> where <math>M</math> is a monomial of type 4 above.

As before we thus have that <math>\bigl(\mathrm{App}(u,v)w\bigr)^n = 0</math> iff all monomials of type 5 are null.

Suppose now that <math>u\in A\limp B</math> and <math>v\in A</math>. Then, since <math>0\in B\orth</math> (<math>0</math> belongs to any type) <math>u.(pvp^*) = pu_{11}vp^*</math> is nilpotent, thus <math>u_{11}v</math> is nilpotent.

Suppose further that <math>w\in B\orth</math>. Then <math>u.(pvp^*+qwq^*)</math> is nilpotent, thus there is a <math>N</math> such that <math>(u.(pvp^* + qwq^*))^n=0</math> for any <math>n\geq N</math>. This entails that all monomials of type 1 to 4 are null. Therefore all monomials appearing in the developpment of <math>(\mathrm{App}(u,v)w)^N</math> are null which proves that <math>\mathrm{App}(u,v)w</math> is nilpotent. Thus <math>\mathrm{App}(u,v)\in B</math>.

Conversely suppose for any <math>v\in A</math> and <math>w\in B\orth</math>, <math>u_{11}v</math> and <math>\mathrm{App}(u,v)w</math> are nilpotent. Let <math>P</math> and <math>N</math> be their respective degrees of nilpotency and put <math>n=N(P+1)+N</math>. Then we claim that all monomials of type 1 to 4 appearing in the development of <math>(u.(pvp^*+qwq^*))^n</math> are null.

Consider for example a monomial of type 1:
: <math>p(u_{11}v)^{i_0}u_{12}w(u_{22}w)^{i_1}\dots u_{21}v(u_{11}v)^{i_m}p^*</math>
with <math>i_0+\cdots+i_m + m = n</math>. Note that <math>m</math> must be even.

If <math>i_{2k}\geq P</math> for some <math>0\leq k\leq m/2</math> then <math>(u_{11}v)^{i_{2k}}=0</math> thus our monomial is null. Otherwise if <math>i_{2k}<P</math> for all <math>k</math> we have:
: <math>i_1+i_3+\cdots +i_{m-1} + m/2 = n - m/2 - (i_0+i_2+\cdots +i_m)</math>
thus:
: <math>i_1+i_3+\cdots +i_{m-1} + m/2\geq n - m/2 - (1+m/2)P</math>.
Now if <math>m/2\geq N</math> then <math>i_1+\cdots+i_{m-1}+m/2 \geq N</math>. Otherwise <math>1+m/2\leq N</math> thus
: <math>i_1+i_3+\cdots +i_{m-1} + m/2\geq n - N - NP = N</math>.
Since <math>N</math> is the degree of nilpotency of <math>\mathrm{App}(u,v)w</math> we have that the monomial:
: <math>(u_{22}w)^{i_1}u_{21}v(u_{11}v)^{i_2}u_{12}w\dots(u_{11}v)^{i_{m-2}}u_{12}w(u_{22}w)^{i_{m-1}}</math>
is null, thus also the monomial of type 1 we started with.
}}

{{Corollary|
If <math>A</math> and <math>B</math> are types then we have:
: <math>A\limp B = \{u\in\mathcal{P} \text{ such that }\forall v\in A: u_{11}v\in\bot\text{ and } \mathrm{App}(u, v)\in B\}</math>.
}}

As an example if we compute the application of the interpretation of the identity <math>\iota</math> in type <math>A\limp A</math> to the operator <math>v\in A</math> then we have:
: <math>\mathrm{App}(\iota, v) = \iota_{22} + \iota_{21}v\sum(\iota_{11}v)^k\iota_{12}</math>.
Now recall that <math>\iota = pq^* + qp^*</math> so that <math>\iota_{11} = \iota_{22} = 0</math> and <math>\iota_{12} = \iota_{21} = 1</math> and we thus get:
: <math>\mathrm{App}(\iota, v) = v</math>
as expected.

= The tensor rule =

Let now <math>A, A', B</math> and <math>B'</math> be types and consider two operators <math>u</math> and <math>u'</math> respectively in <math>A\limp B</math> and <math>A\limp B'</math>. We define an operator <math>u\tens u'</math> by:
: <math>\begin{align}
u\tens u' &= ppp^*upp^*p^* + qpq^*upp^*p^* + ppp^*uqp^*q^* + qpq^*uqp^*q^*\\
&+ pqp^*u'pq^*p^* + qqq^*u'pq^*p^* + pqp^*u'qq^*q^* + qqq^*u'qq^*q^*
\end{align}</math>

Once again the notation is motivated by linear logic syntax and is contradictory with linear algebra practice since what we denote by <math>u\tens u'</math> actually is the internalization of the direct sum <math>u\oplus u'</math>.

Indeed if we think of <math>u</math> and <math>u'</math> as the internalizations of the matrices:
: <math>
\begin{pmatrix}u_{11} & u_{12}\\
u_{21} & u_{22}
\end{pmatrix}
</math> and <math>
\begin{pmatrix}u'_{11} & u'_{12}\\
u'_{21} & u'_{22}
\end{pmatrix}</math>
then we may write:
: <math>\begin{align}
u\tens u' &= ppu_{11}p^*p^* + qpu_{21}p^*p^* + ppu_{12}p^*q^* + qpu_{22}p^*q^*\\
&+ pqu'_{11}q^*p^* + qqu'_{21}q^*p^* + pqu'_{12}q^*q^* + qqu'_{22}q^*q^*
\end{align}</math>

Thus the components of <math>u\tens u'</math> are given by:
: <math>(u\tens u')_{ij} = pu_{ij}p^* + qu'_{ij}q^*</math>.
and we see that <math>u\tens u'</math> is actually the internalization of the matrix:
: <math>
\begin{pmatrix}
u_{11} & 0 & u_{12} & 0 \\
0 & u'_{11} & 0 & u'_{12} \\
u_{21} & 0 & u_{22} & 0 \\
0 & u'_{21} & 0 & u'_{22} \\
\end{pmatrix}
</math>

We are now to show that if we suppose <math>u</math>and <math>u'</math> are in types <math>A\limp B</math> and <math>A'\limp B'</math>, then <math>u\tens u'</math> is in <math>A\tens A'\limp B\tens B'</math>. For this we consider <math>v</math> and <math>v'</math> respectively in <math>A</math> and <math>A'</math>, so that <math>pvp^* + qv'q^*</math> is in <math>A\tens A'</math>, and we show that <math>\mathrm{App}(u\tens u', pvp^* + qv'q^*)\in B\tens B'</math>.

Since <math>u</math> and <math>u'</math> are in <math>A\limp B</math> and <math>A'\limp B'</math> we have that <math>u_{11}v</math> and <math>u'_{11}v'</math> are nilpotent and that <math>\mathrm{App}(u, v)</math> and <math>\mathrm{App}(u', v')</math> are respectively in <math>B</math> and <math>B'</math>, thus:
: <math>p\mathrm{App}(u, v)p^* + q\mathrm{App}(u', v')q^* \in B\tens B'</math>.

But we have:
: <math>\begin{align}
\bigl((u\tens u')_{11}(pvp^* + qv'q^*)\bigr)^n
&= \bigl((pu_{11}p^* + qu'_{11}q^*)(pvp^* + qv'q^*)\bigr)^n\\
&= (pu_{11}vp^* + qu'_{11}v'q^*)^n\\
&= p(u_{11}v)^np^* + q(u'_{11}v')^nq^*
\end{align}</math>

Therefore <math>(u\tens u')_{11}(pvp^* + qv'q^*)</math> is nilpotent. So we can compute <math>\mathrm{App}(u\tens u', pvp^* + qv'q^*)</math>:
: <math>\begin{align}
&\mathrm{App}(u\tens u', pvp^* + qv'q^*)\\
&= (u\tens u')_{22} + (u\tens u')_{21}(pvp^* + qv'q^*)\sum\bigl((u\tens u')_{11}(pvp^* + qv'q^*)\bigr)^k(u\tens u')_{12}\\
&= pu_{22}p^* + qu'_{22}q^* + (pu_{21}p^* + qu'_{21}q^*)(pvp^* + qv'q^*)\sum\bigl((pu_{11}p^* + qu'_{11}q^*)(pvp^* + qv'q^*)\bigr)^k(pu_{12}p^* + qu'_{12}q^*)\\
&= p\bigl(u_{22} + u_{21}v\sum(u_{11}v)^ku_{12}\bigr)p^* + q\bigl(u'_{22} + u'_{21}v'\sum(u'_{11}v')^ku'_{12}\bigr)q^*\\
&= p\mathrm{App}(u, v)p^* + q\mathrm{App}(u', v')q^*
\end{align}</math>
thus lives in <math>B\tens B'</math>.

= Other monoidal constructions =

== Contraposition ==

Let <math>A</math> and <math>B</math> be some types; we have:
: <math>A\limp B = A\orth\limpinv B\orth</math>

Indeed, <math>u\in A\limp B</math> means that for any <math>v</math> and <math>w</math> in respectively <math>A</math> and <math>B\orth</math> we have <math>u.(pvp^* + qwq^*)\in\bot</math> which is exactly the definition of <math>A\orth\limpinv B\orth</math>.

We will denote <math>u\orth</math> the operator:
: <math>u\orth = pu_{22}p^* + pu_{12}q^* + qu_{12}p^* + qu_{11}q^*</math>
where <math>u_{ij}</math> is given by externalization. Therefore the externalization of <math>u\orth</math> is:
: <math>(u\orth)_{ij} = u_{\bar i\,\bar j}</math> where <math>\bar .</math> is defined by <math>\bar1 = 2, \bar2 = 1</math>.
From this we deduce that <math>u\orth\in B\orth\limp A\orth</math> and that <math>(u\orth)\orth = u</math>.

== Commutativity ==
Let <math>\sigma</math> be the operator:
: <math>\sigma = ppq^*q^* +pqp^*q^* + qpq^*p^* + qqp^*p^*</math>.
One can check that <math>\sigma</math> is the internalization of the operator <math>S</math> on <math>H\oplus H\oplus H\oplus H</math> defined by: <math>S(x_1\oplus x_2\oplus x_3\oplus x_4) = x_4\oplus x_3\oplus x_2\oplus x_1</math>. In particular the components of <math>\sigma</math> are:
: <math>\sigma_{11} = \sigma_{22} = 0</math>;
: <math>\sigma_{12} = \sigma_{21} = pq^* + qp^*</math>.

Let <math>A</math> and <math>B</math> be types and <math>u</math> and <math>v</math> be operators in <math>A</math> and <math>B</math>. Then <math>pup^* + qvq^*</math> is in <math>A\tens B</math> and as <math>\sigma_{11}.(pup^* + qvq^*) = 0</math> we may compute:
: <math>\begin{align}
\mathrm{App}(\sigma, pup^* + qvq^*)
&= \sigma_{22} + \sigma_{21}(pup^* + qvq^*)\sum(\sigma_{11}(pup^* + qvq^*))^k\sigma_{12}\\
&= (pq^* + qp^*)(pup^* + qvq^*)(pq^* + qp^*)\\
&= pvp^* + quq^*
\end{align}</math>
But <math>pvp^* + quq^*\in B\tens A</math>, thus we have shown that:
: <math>\sigma\in (A\tens B) \limp (B\tens A)</math>.

== Distributivity ==
We get distributivity by considering the operator:
: <math>\delta = ppp^*p^*q^* + pqpq^*p^*q^* + pqqq^*q^* + qppp^*p^* + qpqp^*q^*p^* + qqq^*q^*p^*</math>
that is similarly shown to be in type <math>A\tens(B\tens C)\limp(A\tens B)\tens C</math> for any types <math>A</math>, <math>B</math> and <math>C</math>.

== Weak distributivity ==
Similarly we get weak distributivity thanks to the operators:
: <math>\delta_1 = pppp^*q^* + ppqp^*q^*q^* + pqq^*q^*q^* + qpp^*p^*p^* + qqp q^*p^*p^* + qqq q^*p^*</math> and
: <math>\delta_2 = ppp^*p^*q^* + pqpq^*p^*q^* + pqqq^*q^* + qppp^*p^* + qpqp^*q^*p^* + qqq^*q^*p^*</math>.

Given three types <math>A</math>, <math>B</math> and <math>C</math> then one can show that:
: <math>\delta_1</math> has type <math>((A\limp B)\tens C)\limp A\limp (B\tens C)</math> and
: <math>\delta_2</math> has type <math>(A\tens(B\limp C))\limp (A\limp B)\limp C</math>.

= Execution formula, version 2: composition =

Let <math>A</math>, <math>B</math> and <math>C</math> be types and <math>u</math> and <math>v</math> be operators respectively in types <math>A\limp B</math> and <math>B\limp C</math>.

As usual we will denote <math>u_{ij}</math> and <math>v_{ij}</math> the operators obtained by externalization of <math>u</math> and <math>v</math>, eg, <math>u_{11} = p^*up</math>, ...

As <math>u</math> is in <math>A\limp B</math> we have that <math>\mathrm{App}(u, 0)=u_{22}\in B</math>; similarly as <math>v\in B\limp C</math>, thus <math>v\orth\in C\orth\limp B\orth</math>, we have <math>\mathrm{App}(v\orth, 0) = v_{11}\in B\orth</math>. Thus <math>u_{22}v_{11}</math> is nilpotent.

We define the operator <math>\mathrm{Comp}(u, v)</math> by:
: <math>\begin{align}
\mathrm{Comp}(u, v) &= p(u_{11} + u_{12}\sum(v_{11}u_{22})^k\,v_{11}u_{21})p^*\\
&+ p(u_{12}\sum(v_{11}u_{22})^k\,v_{12})q^*\\
&+ q(v_{21}\sum(u_{22}v_{11})^k\,u_{21})p^*\\
&+ q(v_{22} + v_{21}\sum(u_{22}v_{11})^k\,u_{22}v_{12})q^*
\end{align}</math>

This is well defined since <math>u_{11}v_{22}</math> is nilpotent. As an example let us compute the composition of <math>u</math> and <math>\iota</math> in type <math>B\limp B</math>; recall that <math>\iota_{ij} = \delta_{ij}</math>, so we get:
: <math>
\mathrm{Comp}(u, \iota) = pu_{11}p^* + pu_{12}q^* + qu_{21}p^* + qu_{22}q^* = u
</math>
Similar computation would show that <math>\mathrm{Comp}(\iota, v) = v</math> (we use <math>pp^* + qq^* = 1</math> here).

Coming back to the general case we claim that <math>\mathrm{Comp}(u, v)</math> is in <math>A\limp C</math>: let <math>a</math> be an operator in <math>A</math>. By computation we can check that:
: <math>\mathrm{App}(\mathrm{Comp}(u, v), a) = \mathrm{App}(v, \mathrm{App}(u, a))</math>.
Now since <math>u</math> is in <math>A\limp B</math>, <math>\mathrm{App}(u, a)</math> is in <math>B</math> and since <math>v</math> is in <math>B\limp C</math>, <math>\mathrm{App}(v, \mathrm{App}(u, a))</math> is in <math>C</math>.

If we now consider a type <math>D</math> and an operator <math>w</math> in <math>C\limp D</math> then we have:
: <math>\mathrm{Comp}(\mathrm{Comp}(u, v), w) = \mathrm{Comp}(u,
\mathrm{Comp}(v, w))</math>.

Putting together the results of this section we finally have:

{{Theorem|
Let GoI(H) be defined by:
* objects are types, ''ie'' sets <math>A</math> of <math>p</math>-isometries satisfying: <math>A\biorth = A</math>;
* morphisms from <math>A</math> to <math>B</math> are <math>p</math>-isometries in type <math>A\limp B</math>;
* composition is given by the formula above.

Then GoI(H) is a star-autonomous category.
}}

GoI for MELL: partial isometries

2010-05-15T11:03:54Z

Laurent Regnier: New page: = Operators, partial isometries = We will denote by <math>H</math> the Hilbert space <math>\ell^2(\mathbb{N})</math> of sequences <math>(x_n)_{n\in\mathbb{N}}</math> of complex numbers su...

= Operators, partial isometries =

We will denote by <math>H</math> the Hilbert space <math>\ell^2(\mathbb{N})</math> of sequences <math>(x_n)_{n\in\mathbb{N}}</math> of complex numbers such that the series <math>\sum_{n\in\mathbb{N}}|x_n|^2</math> converges. If <math>x = (x_n)_{n\in\mathbb{N}}</math> and <math>y = (y_n)_{n\in\mathbb{N}}</math> are two vectors of <math>H</math> their ''scalar product'' is:
: <math>\langle x, y\rangle = \sum_{n\in\mathbb{N}} x_n\bar y_n</math>.

Two vectors of <math>H</math> are ''othogonal'' if their scalar product is nul. We will say that two subspaces are ''disjoint'' when any two vectors taken in each subspace are orthorgonal. Note that this notion is different from the set theoretic one, in particular two disjoint subspaces always have exactly one vector in common: <math>0</math>.

The ''norm'' of a vector is the square root of the scalar product with itself:
: <math>\|x\| = \sqrt{\langle x, x\rangle}</math>.

Let us denote by <math>(e_k)_{k\in\mathbb{N}}</math> the canonical ''hilbertian basis'' of <math>H</math>: <math>e_k = (\delta_{kn})_{n\in\mathbb{N}}</math> where <math>\delta_{kn}</math> is the Kroenecker symbol: <math>\delta_{kn}=1</math> if <math>k=n</math>, <math>0</math> otherwise. Thus if <math>x=(x_n)_{n\in\mathbb{N}}</math> is a sequence in <math>H</math> we have:
: <math> x = \sum_{n\in\mathbb{N}} x_ne_n</math>.

An ''operator'' on <math>H</math> is a ''continuous'' linear map from <math>H</math> to <math>H</math>.<ref>Continuity is equivalent to the fact that operators are ''bounded'', which means that one may define the ''norm'' of an operator <math>u</math> as the sup on the unit ball of the norms of its values:
: <math>\|u\| = \sup_{\{x\in H,\, \|x\| = 1\}}\|u(x)\|</math>.</ref>The set of (bounded) operators is denoted by <math>\mathcal{B}(H)</math>.

The ''range'' or ''codomain'' of the operator <math>u</math> is the set of images of vectors; the ''kernel'' of <math>u</math> is the set of vectors that are anihilated by <math>u</math>; the ''domain'' of <math>u</math> is the set of vectors orthogonal to the kernel, ''ie'', the maximal subspace disjoint with the kernel:

* <math>\mathrm{Codom}(u) = \{u(x),\, x\in H\}</math>;
* <math>\mathrm{Ker}(u) = \{x\in H,\, u(x) = 0\}</math>;
* <math>\mathrm{Dom}(u) = \{x\in H,\, \forall y\in\mathrm{Ker}(u), \langle x, y\rangle = 0\}</math>.

These three sets are closed subspaces of <math>H</math>.

The ''adjoint'' of an operator <math>u</math> is the operator <math>u^*</math> defined by <math>\langle u(x), y\rangle = \langle x, u^*(y)\rangle</math> for any <math>x,y\in H</math>. Adjointness is well behaved w.r.t. composition of operators:
: <math>(uv)^* = v^*u^*</math>.

A ''projector'' is an idempotent operator of norm <math>0</math> (the projector
on the null subspace) or <math>1</math>, that is an operator <math>p</math>
such that <math>p^2 = p</math> and <math>\|p\| = 0</math> or <math>1</math>. A projector is auto-adjoint and its domain is equal to its codomain.

A ''partial isometry'' is an operator <math>u</math> satisfying <math>uu^* u =
u</math>; this condition entails that we also have <math>u^*uu^* =
u^*</math>. As a consequence <math>uu^*</math> and <math>uu^*</math> are both projectors, called respectively the ''initial'' and the ''final'' projector of <math>u</math> because their (co)domains are respectively the domain and the codomain of <math>u</math>:
* <math>\mathrm{Dom}(u^*u) = \mathrm{Codom}(u^*u) = \mathrm{Dom}(u)</math>;
* <math>\mathrm{Dom}(uu^*) = \mathrm{Codom}(uu^*) = \mathrm{Codom}(u)</math>.

The restriction of <math>u</math> to its domain is an isometry. Projectors are particular examples of partial isometries.

If <math>u</math> is a partial isometry then <math>u^*</math> is also a partial isometry the domain of which is the codomain of <math>u</math> and the codomain of which is the domain of <math>u</math>.

If the domain of <math>u</math> is <math>H</math> that is if <math>u^* u = 1</math> we say that <math>u</math> has ''full domain'', and similarly for codomain. If <math>u</math> and <math>v</math> are two partial isometries then we have:
* <math>uv^* = 0</math> iff <math>u^*uv^*v = 0</math> iff the domains of <math>u</math> and <math>v</math> are disjoint;
* <math>u^*v = 0</math> iff <math>uu^*vv^* = 0</math> iff the codomains of <math>u</math> and <math>v</math> are disjoint;
* <math>uu^* + vv^* = 1</math> iff the codomains of <math>u</math> and <math>v</math> are disjoint and their their direct sum is <math>H</math>.

= Partial permutations =

We will now define our proof space which turns out to be the set of partial isometries acting as permutations on the canonical basis <math>(e_n)_{n\in\mathbb{N}}</math>.

More precisely a ''partial permutation'' <math>\varphi</math> on <math>\mathbb{N}</math> is a one-to-one map defined on a subset <math>D_\varphi</math> of <math>\mathbb{N}</math> onto a subset <math>C_\varphi</math> of <math>\mathbb{N}</math>. <math>D_\varphi</math> is called the ''domain'' of <math>\varphi</math> and <math>C_\varphi</math> its ''codomain''. Partial permutations may be composed: if <math>\psi</math> is another partial permutation on <math>\mathbb{N}</math> then <math>\varphi\circ\psi</math> is defined by:

* <math>n\in D_{\varphi\circ\psi}</math> iff <math>n\in D_\psi</math> and <math>\psi(n)\in D_\varphi</math>;
* if <math>n\in D_{\varphi\circ\psi}</math> then <math>\varphi\circ\psi(n) = \varphi(\psi(n))</math>;
* the codomain of <math>\varphi\circ\psi</math> is the image of the domain: <math>C_{\varphi\circ\psi} = \{\varphi(\psi(n)), n\in D_{\varphi\circ\psi}\}</math>.

Partial permutations are well known to form a structure of ''inverse monoid'' that we detail now.

Given a a subset <math>D</math> of <math>\mathbb{N}</math>, the ''partial identity'' on <math>D</math> is the partial permutation <math>\varphi</math> defined by:
* <math>D_\varphi = D</math>;
* <math>\varphi(n) = n</math> for any <math>n\in D_\varphi</math>.
Thus the codomain of <math>\varphi</math> is <math>D</math>.

The partial identity on <math>D</math> will be denoted by <math>1_D</math>. Partial identities are idempotent for composition.

Among partial identities one finds the identity on the empty subset, that is the empty map, that we will denote by <math>0</math> and the identity on <math>\mathbb{N}</math> that we will denote by <math>1</math>. This latter permutation is the neutral for composition.

If <math>\varphi</math> is a partial permutation there is an inverse partial permutation <math>\varphi^{-1}</math> whose domain is <math>D_{\varphi^{-1}} = C_{\varphi}</math> and who satisfies:

: <math>\varphi^{-1}\circ\varphi = 1_{D_\varphi}</math>
: <math>\varphi\circ\varphi^{-1} = 1_{C_\varphi}</math>

= The proof space =

Given a partial permutation <math>\varphi</math> one defines a partial isometry <math>u_\varphi</math> by:
: <math>u_\varphi(e_n) =
\begin{cases}
e_{\varphi(n)} & \text{ if }n\in D_\varphi,\\
0 & \text{ otherwise.}
\end{cases}
</math>
In other terms if <math>x=(x_n)_{n\in\mathbb{N}}</math> is a sequence in <math>\ell^2</math> then <math>u_\varphi(x)</math> is the sequence <math>(y_n)_{n\in\mathbb{N}}</math> defined by:
: <math>y_n = x_{\varphi^{-1}(n)}</math> if <math>n\in C_\varphi</math>, <math>0</math> otherwise.

We will (not so abusively) write <math>e_{\varphi(n)} = 0</math> when <math>\varphi(n)</math> is undefined so that the definition of <math>u_\varphi</math> reads:
: <math>u_\varphi(e_n) = e_{\varphi(n)}</math>.

The domain of <math>u_\varphi</math> is the subspace spanned by the family <math>(e_n)_{n\in D_\varphi}</math> and the codomain of <math>u_\varphi</math> is the subspace spanned by <math>(e_n)_{n\in C_\varphi}</math>. In particular if <math>\varphi</math> is <math>1_D</math> then <math>u_\varphi</math> is the projector on the subspace spanned by <math>(e_n)_{n\in D}</math>.

{{Definition|
We call ''<math>p</math>-isometry'' a partial isometry of the form <math>u_\varphi</math> where <math>\varphi</math> is a partial permutation on <math>\mathbb{N}</math>. The ''proof space'' <math>\mathcal{P}</math> is the set of all <math>p</math>-isometries.
}}

{{Proposition|
Let <math>\varphi</math> and <math>\psi</math> be two partial permutations. We have:
: <math>u_\varphi u_\psi = u_{\varphi\circ\psi}</math>.

The adjoint of <math>u_\varphi</math> is:
: <math>u_\varphi^* = u_{\varphi^{-1}}</math>.

In particular the initial projector of <math>u_{\varphi}</math> is given by:
: <math>u_\varphi u^*_\varphi = u_{1_{D_\varphi}}</math>.

and the final projector of <math>u_\varphi</math> is:
: <math>u^*_\varphi u_\varphi = u_{1_{C_\varphi}}</math>.

If <math>p</math> is a projector in <math>\mathcal{P}</math> then there is a partial identity <math>1_D</math> such that <math>p= u_{1_D}</math>.

Projectors commute, in particular we have:
: <math>u_\varphi u_\varphi^*u_\psi u_\psi^* = u_\psi u_\psi^*u_\varphi u_\varphi^*</math>.
}}

Note that this entails all the other commutations of projectors: <math>u^*_\varphi u_\varphi u_\psi u^*_\psi = u_\psi u^*_\psi u^*_\varphi u_\varphi</math> and <math>u^*_\varphi u_\varphi u^*_\psi u\psi = u^*_\psi u_\psi u^*_\varphi u_\varphi</math>.

In particular note that <math>0</math> is a <math>p</math>-isometry. The set <math>\mathcal{P}</math> is a submonoid of <math>\mathcal{B}(H)</math> but it is not a subalgebra.<ref><math>\mathcal{P}</math> is the normalizing groupoid of the maximal commutative subalgebra of <math>\mathcal{B}(H)</math> consisiting of all operators ''diagonalizable'' in the canonical basis.</ref>In general given <math>u,v\in\mathcal{P}</math> we don't necessarily have <math>u+v\in\mathcal{P}</math>. However we have:

{{Proposition|
Let <math>u, v\in\mathcal{P}</math>. Then <math>u+v\in\mathcal{P}</math> iff <math>u</math> and <math>v</math> have disjoint domains and disjoint codomains, that is:
: <math>u+v\in\mathcal{P}</math> iff <math>uu^*vv^* = u^*uv^*v = 0</math>.
}}

{{Proof|
Suppose for contradiction that <math>e_n</math> is in the domains of <math>u</math> and <math>v</math>. There are integers <math>p</math> and <math>q</math> such that <math>u(e_n) = e_p</math> and <math>v(e_n) = e_q</math> thus <math>(u+v)(e_n) = e_p + e_q</math> which is not a basis vector; therefore <math>u+v</math> is not a <math>p</math>-permutation.
}}

As a corollary note that if <math>u+v=0</math> then <math>u=v=0</math>.

= From operators to matrices: internalization/externalization =

It will be convenient to view operators on <math>H</math> as acting on <math>H\oplus H</math>, and conversely. For this purpose we define an isomorphism <math>H\oplus H \cong H</math> by <math>x\oplus y\rightsquigarrow p(x)+q(y)</math> where <math>p:H\mapsto H</math> and <math>q:H\mapsto H</math> are partial isometries given by:

: <math>p(e_n) = e_{2n}</math>,
: <math>q(e_n) = e_{2n+1}</math>.

From the definition <math>p</math> and <math>q</math> have full domain, that is
satisfy <math>p^* p = q^* q = 1</math>. On the other hand their codomains are
disjoint, thus we have <math>p^*q = q^*p = 0</math>. As the sum of their
codomains is the full space <math>H</math> we also have <math>pp^* + qq^* = 1</math>.

Note that we have choosen <math>p</math> and <math>q</math> in <math>\mathcal{P}</math>. However the choice is arbitrary: any two <math>p</math>-isometries with full domain and disjoint codomains would do the job.

Given an operator <math>u</math> on <math>H</math> we may ''externalize'' it obtaining an operator <math>U</math> on <math>H\oplus H</math> defined by the matrix:
: <math>U = \begin{pmatrix}
u_{11} & u_{12}\\
u_{21} & u_{22}
\end{pmatrix}</math>
where the <math>u_{ij}</math>'s are given by:
: <math>u_{11} = p^*up</math>;
: <math>u_{12} = p^*uq</math>;
: <math>u_{21} = q^*up</math>;
: <math>u_{22} = q^*uq</math>.

The <math>u_{ij}</math>'s are called the ''external components'' of <math>u</math>. The externalization is functorial in the sense that if <math>v</math> is another operator externalized as:
: <math>V = \begin{pmatrix}
v_{11} & v_{12}\\
v_{21} & v_{22}
\end{pmatrix}
= \begin{pmatrix}
p^*vp & p^*vq\\
q^*vp & q^*vq
\end{pmatrix}
</math>
then the externalization of <math>uv</math> is the matrix product <math>UV</math>.

As <math>pp^* + qq^* = 1</math> we have:
: <math>u = (pp^*+qq^*)u(pp^*+qq^*) = pu_{11}p^* + pu_{12}q^* + qu_{21}p^* + qu_{22}q^*</math>
which entails that externalization is reversible, its converse being called ''internalization''.

If we suppose that <math>u</math> is a <math>p</math>-isometry then so are the components <math>u_{ij}</math>'s. Thus the formula above entails that the four terms of the sum have pairwise disjoint domains and pairwise disjoint codomains from which we deduce:

{{Proposition|
If <math>u</math> is a <math>p</math>-isometry and <math>u_{ij}</math> are its external components then:
* <math>u_{1j}</math> and <math>u_{2j}</math> have disjoint domains, that is <math>u_{1j}^*u_{1j}u_{2j}^*u_{2j} = 0</math> for <math>j=1,2</math>;
* <math>u_{i1}</math> and <math>u_{i2}</math> have disjoint codomains, that is <math>u_{i1}u_{i1}^*u_{i2}u_{i2}^* = 0</math> for <math>i=1,2</math>.
}}

As an example of computation in <math>\mathcal{P}</math> let us check that the product of the final projectors of <math>pu_{11}p^*</math> and <math>pu_{12}q^*</math> is null:
: <math>\begin{align}
(pu_{11}p^*)(pu^*_{11}p^*)(pu_{12}q^*)(qu_{12}^*p^*)
&= pu_{11}u_{11}^*u_{12}u_{12}^*p^*\\
&= pp^*upp^*u^*pp^*uqq^*u^*pp^*\\
&= pp^*u(pp^*)(u^*pp^*u)qq^*u^*pp^*\\
&= pp^*u(u^*pp^*u)(pp^*)qq^*u^*pp^*\\
&= pp^*uu^*pp^*u(pp^*)(qq^*)u^*pp^*\\
&= 0
\end{align}</math>
where we used the fact that all projectors in <math>\mathcal{P}</math> commute, which is in particular the case of <math>pp^*</math> and <math>u^*pp^*u</math>.

= Notes and references =

<references/>