Relational semantics
Contents |
Relational semantics
This is the simplest denotational semantics of linear logic. It consists in interpreting a formula A as a set A * and a proof π of A as a subset π * of A * .
The category of sets and relations
It is the category whose objects are sets, and such that
. Composition is the ordinary composition of relations: given
and
, one
sets
and the identity morphism is the diagonal relation
.
An isomorphism in the category is a relation which is a bijection, as easily checked.
Monoidal structure
The tensor product is the usual cartesian product of sets (which is not a cartesian product in the category
in the categorical sense). It is a bifunctor: given
(for i = 1,2), one sets
. The unit of this tensor product is
where * is an arbitrary element.
For defining a monoidal category, it is not sufficient to provide the definition of the tensor product functor and its unit
, one has also to provide natural isomorphisms
,
(left and right neutrality of
for
) and
(associativity of
). All these isomorphisms have to satisfy a number of commutations. In the present case, they are defined in the obvious way.
This monoidal category is symmetric, meaning that it is endowed with an additional natural isomorphism
, also subject to some commutations. Here, again, this isomorphism is defined in the obvious way (symmetry of the cartesian product). So, to be precise, the SMCC (symmetric monoidal closed category)
is the tuple
, but we shall simply denote it as
.
The SMCC is closed. This means that, given any object X of
(a set), the functor
(from
to
) admits a right adjoint
(from
to
). In other words, for any objects X and Y, we are given an object
and a morphism
with the following universal property: for any morphism
, there is a unique morphism
such that
.
The definition of all these data is quite simple in :
,
and
.
Let . Then we have
and hence
. It is clear that
and hence η is a natural isomorphism: one says that the SMCC
is a *-autonomous category, with
as dualizing object.
Additives
Given a family , let
. Let
given by
. Then
is the cartesian product of the Xis in the category
.
Exponentials
One defines as the set of all finite multisets of elements of X. Given
, one defines
where
is the multiset containing
, taking multiplicities into account. This defines a functor
, that we endow with a comonad structure as follows:
- the counit, called dereliction, is the natural transformation
, given by
- the comultiplication, called digging, is the natural transformation
, given by
Interpretation of propositional linear logic (LL0)
The structure described above gives rise to the following interpretation of formulas and proofs of linear logic.
For all propositional variable X, fix a set .
Then with each formula A, we associate a set
as follows:
-
;
-
;
-
;
-
.
We then interpret the proofs of LL0 as follows: with each proof
π of sequent , we associate a
subset
.
- Identity group:
-
- Multiplicative group:
-
- Additive group:
-
- Exponential group:
-
Theorem
If proof π' is obtained from π by eliminating a cut,
then .