*********************************************
*********************************************
************* LINEAR LOGIC CATS *************
******************** OR *******************
******** CATEGORICAL SEMANTICS OF LL ********
*********************************************
*********************************************
DISCLAIMER: This note may be cryptic at times since it was
written for self-consumption. It is fundamentally a digest
of known results. I do not claim ownership of the results.
As usual, props are objects. Proofs A |- B are morphisms A -> B.
Composition is cut, identity is axiom.
Semantics of A \tensor B:
[A * B] = [A] * [B] in the category
Moreover, Given pi1 : A1 |- A2 and pi2 : B1 |- B2
the denotation of pi : A1 * B1 |- A2 * B2 should follow
from the denotations of pi1 and pi2 by applying * on the
denotations of proofs:
[pi] = [pi1] * [pi2]
Thus, linear conjunction * defines a bifunctor:
* commutes with composition:
(f3 * f4) o (f1 * f2) = (f3 o f1) * (f4 o f2)
* preserves identities:
id[A]*[B] = id[A] * id[B]
So * defines a bifunctor on the category of proofs.
The bifunctor defines a (nearly) monoidal category!
First choose a unit in the category: multiplicative
unit 1.
Construct 3 isos:
alpha: (A * B) * C -> A * (B * C)
lambda: 1 * A -> A rho: A * 1 -> A
which satisfy all the coherence and naturality
conditions of a monoidal category.
Naturality of alpha means that for any three proofs
pi1 A1 |- A2 pi2 B1 |- B2 pi3 C1 |- C2
the diagram (vertical arrows down):
(A1 * B1) * C1 - alpha -> A1 * (B1 * C1)
| |
(pi1*pi2)*pi3 pi1*(pi2*pi3)
| |
(A2 * B2) * C2 - alpha -> A2 * (B2 * C2)
commutes. alpha o (...) and (...) o alpha reduce by
cut-elim to the same proof.
To show that * defines a monoidal category of proof
denotations, need to show alpha , lambda and rho are
isos. However, this is not necessarily the case!
Let alpha',lambda' and rho' be the inverse morphisms
defined in the obvious way.
From invariance and modularity it follows easily that
lambda o lambda' = id_A rho o rho' = id_A
However (note that o is 'reversed' in cut) none of the
other four equalities hold.
To make sure that we obtain a monoidal category of denotations
we require beyond invariance [under cut elim.], modularity
[composition] and tensoriality [see above] a series of basic
equalities. For every two proofs p1 and p2, the proof:
pi1
Gamma,C,D |-A
-------------- pi2
Gamma,C*D |- A D |- B
-------------------------
Gamma,C*D,Delta |- A*B
has the same denotation as:
Gamma,C,D |- A Delta |- B
-----------------------------
Gamma,C,D,Delta |- A*B
----------------------
Gamma,C*D,Delta |- A*B
Symmetrically on permuting on the right.
Also needed is the permutation of 1L and *R on both
sides (in essence its modulo invertibility of rules).
With these in place, we can show that alpha lambda and
rho are isos and thus the cat. of denotations is
monoidal.
Note: This is due to cut-elim defined very carefully
avoiding a few unnecessary proof transformations which
makes the equalities no longer hold.
Without these restrictions, the category is indeed
monoidal without any extra conditions.
----
CATEGORICAL MODEL OF LL?
With a sufficiently permissive cut-elim. procedure,
every (invariant, modular, tensorial) denotation
defines a monoidal category of denotations.
Lets work backwards then: what axioms should a given
monoidal category C satisfy in order to define
a modular and tensorial invariant of proofs?
The general interpretation is that sequents
A1, ... , Am |- B of LL are to be interpreted
as morphisms
[A1] * ... * [Am] -> [B]
in the category C, where [A] is the object denoting
prop. A in C (computed by induction on the size of A).
Typically,
[A*B] = [A]*[B]
So the category C should admit, at least, a tensor product.
It is then customary to write
[Gamma] = [A1] * ... * [Am]
Allowing a sequent Gamma |- B to be interpreted as a morphism
[Gamma] -> [B]
in C.
The interpretation of a proof pi is defined by induction on
the depth of its derivation tree. The axiom rule is
interpreted as the identity morphism:
id_[A] : [A] -> [A]
and given two proofs pi1 Gamma |- A and pi2 Delta |- B
interpreted as morphisms f : [Gamma] -> [A] and g : [Gamma] -> [B]
in C, the proof obtained by *R pi1 pi2 is interpreted as the
morphism
[Gamma] * [Delta] - f*g -> [A]*[B]
in the monoidal category C.
Beyond these basic principles, the structures and properties required
of C in order to provide an invariant of proofs depends on the
particular variant of LL we consider: commutative or non-commutative,
classical or intuitionistic, additive or non-additive, etc.
COMMUTATIVE VS NON-COMMUTATIVE
LL is generally understood as a commutative logic, meaning that
there exists a canonical proof of A*B |- B*A for every A and B.
Thus, LL is usually interpreted in monoidal categories with a
notion of symmetry (called symmetric monoidal categories).
To account for non-commutative variants of LL (i.e. without
exchange or at least with restricted forms of it), we must
interpret into monoidal categories, possibly with a notion
of permutation, like a braiding.
CLASSICAL LINEAR LOGIC AND DUALITY
In Girard's TCS paper he introduced a classical LL, where
sequents are one-sided:
|- A1, ... , An
featuring a duality principle, based on an involutive negation
such that every prop A has a negation A^perp and A^perpperp is A.
From this, a new connective \par arises by duality:
(A par B) = (B^perp * A^perp)^perp
This leads to an alt. presentation of LL, based on two-sided
sequents:
A1, ... Am |- B1, ... Bn
where the sequent is intended to mean:
A1 * ... * Am -o B1 par ... par Bn
where -o is linear implication.
To interpret such a sequent into a category, we must use a
linearly distributive category [Cockett and Seely]. This
is a category equipped with two monoidal structures * and . whose
task is to interpret such a sequent as a morphism
[A1] * ... * [Am] -> [B1] . ... . [Bn]
in the category.
INTUITIONISTIC LINEAR LOGIC AND LINEAR IMPLICATION
The intuitionistic fragment of LL was later extracted from classical
LL by restricting the two-sided sequent above to those with a single
prop on the right.
In this setting, duality disappears in the typical accounts of ILL:
connectives are limited to tensor, unit and implication. The right
rule for -o is given by the expected rule which can be interpreted
in a monoidal closed category
ADDITIVE CONJUNCTION
The additive conjunction & ("with") behaves like a cartesian product
in linear algebra (opposed to * which behaves like a tensor product).
Thus, & is generally interpreted as a cartesian product in a monoidal
category.
To interpret the right & rule, we take the interpretation of two proofs
pi_A : Gamma |- A and pi_B : Gamma |- B and interpret the proof
of Gamma |- A&B via pi_A and pi_B by considering the interpretation
morphisms f : [Gamma] -> [A] and g : [Gamma] -> [B] and the existence
of cartesian products A&B, making it so that the pair of morphisms
f and g give rise to a unique morphism
: [Gamma] -> [A]&[B]
making the product diagram (with first and second projections) commute in C.
To interpret the left rules:
Gamma,A |- C
-------------
Gamma,A&B |- C
We interpret the proof above the line as f : [Gamma] * [A] -> [C] and
produce the morphism
[Gamma]*[A&B] --- [Gamma]*first_proj -> [Gamma] * [A] --- f --> [C]
The other left rule is interpreted identically.
EXPONENTIAL MODALITY
Interpreting the exponential is quite tricky as it turns out.
The consensus seems to be that the exponential can be interpreted
via a symmetric monoidal adjunction between:
- A symmetric monoidal closed category |L (interprets *, -o)
- A cartesian category |M
|M -- L --> |L ---- M ---> |M
Where cartesian means a category with finite products: a terminal object
and every pair of objects has a product.
An adjunction L -| M satisfying these properties is called a linear-non-linear
adjunction and provides a categorical model of ILL, becoming a model of CLL
when L is not only symmetric monoidal closed, but also *-autonomous. The !
modality is interpreted as the comonad
! = L o M
induced on L by the adjunction.
================== CATEGORY STUFFS =========================
MONOIDAL CATS
A monoidal category is a category C equipped with a bifunctor
* : C x C -> C
associative up to a natural isomorphism
alpha : (A*B)*C -> A*(B*C)
with a unit up to natural isos:
lambda : 1 * A -> A rho : A * 1 -> A
The 3 maps must satisfy two axioms.
First (we write *A instead of *id_A in morphisms):
(A * B) * (C * D) --- alpha --> A * (B * (C * D))
^ ^
/ |
alpha |
/ |
((A * B)* C)*D |
| |
alpha * D A*alpha
| |
(A * (B*C))*D ---- alpha ---> A * ((B * C) * D)
should commute for all objects A,B,C,D. Second, the diagram:
(A * 1) * B ---- alpha ---> A * (1 * B)
\ /
\rho*B / A*lambda
\ /
A*B
should commute for all objects A,B.
These axioms ensure that every diagram made of structure maps
commutes in C and is called the coherence property of monoidal cats.
Now the issue is that when encoding contexts we typically want to
combine objects A1,...,An using the tensor product of the category as
A1 * ... * An. Unfortunately, the tensor product is only associative
up-to natural isomorphism (alpha) which means that there are several
candidates for A1 * ... * An. That is, (A1 * A2) * A3 and A1 * (A2 *
A3) are two distinct yet isomorphic objects of C and both are
candidates for the tensor product of A1, A2 and A3. Coherence provides
a way of "identifying" candidates of big tensor products in a coherent
way.
A monoidal category is strict when its maps alpha, lambda and rho are
identities. Coherence ensures that every monoidal category is equivalent
to a strict one.
BRAIDED MONOIDAL CATEGORIES
As the name implies, a braided monoidal cat is a monoidal cat C equipped
with a *braiding*, that is, equipped with a natural isomorphism
gamma : A*B -> B*A
such that
alpha o gamma o alpha = B*gamma o alpha o gamma*C
and
alpha^-1 o gamma o alpha^-1 = gamma*B o alpha^-1 o A*gamma
The braiding is dubbed due to the "criss-cross" nature of the morphisms
when combined with associativity, where we go from (A*B)*C to B*(C*A).
The braiding is well-behaved with the unit with respect to the lambda and rho
morphisms in the expected way.
SYMMETRIC MONOIDAL CATEGORIES
A symmetric monoidal category is a braided monoidal category whose braiding
is a symmetry. A symmetry is a braiding satisfying
gamma_{B,A} = gamma^-1_{A,B}
for all A,B in the category.
The second law given above may be dropped in the def. of braiding since
that law holds iff the first commutes for gamma_{B,A} = gamma^-1_{A,B}.
MONOIDAL CLOSED CATEGORIES
A left closed structure in a monoidal cat is the data of:
- An object A -o B
- a morphism eval_{A,B} : A*(A-oB) -> B
for every two objects A and B of the category. The morphism
eval is called the left evaluation morphism and it must satisfy
the universal property:
For every
f : A*X -> B
there exists a unique morphism
h : X -> A-oB
such that
eval o A*h = f
A monoidal closed cat is a monoidal cat with a left closed structure.
MONOIDAL BICLOSED CATEGORIES
A right closed structure in a monoidal cat is the data of
- An object A o- B
- A morphism evar : (B o- A) * A -> B
for every A,B in the category. The right evaluation morphism
must satisfy a similar universal property:
For every
f : X*A -> B
there exists a unique morphism
h : X -> B o- A
such that
evar o h*A = f
A monoidal biclosed category is a monoidal cat with a left and right
closed structures.
SYMMETRIC MONOIDAL CLOSED CATEGORIES
A symmetric monoidal closed category is a monoidal category equipped
with a symmetry and a left closed structure. This implies it must also
have a right closed structure (where the object is the same as that
of the left closed structure and the evar morphism is constructed
with the symmetry).
Symmetric monoidal closed categories provide the necessary structure
to interpret props and proofs of the multiplicative and intuitionistic
fragments of LL.
*-AUTONOMOUS CATEGORIES (READ STAR AUTONOMOUS)
A *-autonomous category is a monoidal biclosed category equipped with
a dualizing object _|_. A dualizing object is an object of the category
such that the two morphisms:
si : A -> _|_ o- (A -o _|_) sibar : A -> (_|_ o- A) -o _|_
are isomorphisms.
In the special case where the category is is symmetric monoidal closed
the object _|_ is dualizing precisely when the morphism:
si : A -> (A -o _|_) -o _|_
is an isomorphism.
LINEARLY DISTRIBUTIVE CATEGORIES
A linearly distributive category is a monoidal category twice: once for
the bifunctor * with unit 1 and the expected natural isos and again
for the bifunctor . with unit u and the expected natural isos.
The tensor product is required to distribute over . by natural isos:
A*(B.C) -> (A*B).C
(A.B)*C -> A.(B*C)
The structural maps must satisfy a series of commutativity axioms [not
writing them out here].
DUALITY IN LDC
Let C be a linearly distributive category. A right duality in C is the
data of:
- Object A+
- morphisms ax : 1 -> A+ . A and cut : A*A+ -> u
for every A.
The morphisms must then be well-behaved with respect to the units.
BRAIDED LINEARLY DISTRIBUTIVE CATEGORIES
A braided linearly distributive category is a LDC in which
the two monoidal structures are braided.
SYMMETRIC LDC
A symmetric LDC is a braided LDC where the two braidings
are symmetries.
Summary:
What is the cat model of LL?
- Cat. of denotations L should be symmetric monoidal closed to
interpret ILL.
- *-autonomous to interpret CLL
- Cartesian for & and Cocartesian for \oplus
============ ADJUNCTIONS BETWEEN MONOIDAL CATS ==============
What about the exponential?
Later...