Phase semantics
m (→Phase spaces) |
m (→Additive connectives) |
||
Line 121: | Line 121: | ||
{{Definition|title=additive connectives| |
{{Definition|title=additive connectives| |
||
− | If <math>(X,1,\cdot,\bot\!\!\bot</math> is a phase space, we define the following facts and operations on facts: |
+ | If <math>(X,1,\cdot,\bot\!\!\bot)</math> is a phase space, we define the following facts and operations on facts: |
# <math>\top = X = \emptyset^\bot</math> |
# <math>\top = X = \emptyset^\bot</math> |
||
# <math>\zero = \emptyset^{\bot\bot} = X^\bot</math> |
# <math>\zero = \emptyset^{\bot\bot} = X^\bot</math> |
||
+ | # <math>x\with y = x\cap y</math> |
||
# <math>x\plus y = (x\cup y)^{\bot\bot}</math> |
# <math>x\plus y = (x\cup y)^{\bot\bot}</math> |
||
− | # <math>x\with y = x\cap y</math> |
||
}} |
}} |
||
Line 134: | Line 134: | ||
# <math>\zero^\bot = \top</math> |
# <math>\zero^\bot = \top</math> |
||
# <math>\top^\bot = \zero</math> |
# <math>\top^\bot = \zero</math> |
||
+ | # <math>(x\with y)^\bot = x^\bot \plus y^\bot</math> |
||
# <math>(x\plus y)^\bot = x^\bot \with y^\bot</math> |
# <math>(x\plus y)^\bot = x^\bot \with y^\bot</math> |
||
− | # <math>(x\with y)^\bot = x^\bot \plus y^\bot</math> |
||
}} |
}} |
||
− | |||
− | |||
==Multiplicative connectives== |
==Multiplicative connectives== |
Revision as of 13:42, 8 February 2009
Contents |
Introduction
The semantics given by phase spaces is a kind of "formula and provability semantics", and is thus quite different in spirit from the more usual denotational semantics of linear logic. (Those are rather some "formulas and proofs semantics".)
--- probably a whole lot more of blabla to put here... ---
Preliminaries: relation and closure operators
Part of the structure obtained from phase semantics works in a very general framework and relies solely on the notion of relation between two sets.
Relations and operators on subsets
The starting point of phase semantics is the notion of duality. The structure needed to talk about duality is very simple: one just needs a relation R between two sets X and Y. Using standard mathematical practice, we can write either or
to say that
and
are related.
Definition
If is a relation, we write
for the converse relation:
iff
.
Such a relation yields three interesting operators sending subsets of X to subsets of Y:
Definition
Let be a relation, define the operators
, [R] and _R taking subsets of X to subsets of Y as follows:
-
iff
-
iff
-
iff
The operator is usually called the direct image of the relation, [R] is sometimes called the universal image of the relation.
It is trivial to check that and [R] are covariant (increasing for the
relation) while _R is contravariant (decreasing for the
relation). More interesting:
Lemma (Galois Connections)
-
is right-adjoint to [R˜]: for any
and
, we have
iff
- we have
iff
This implies directly that commutes with arbitrary unions and [R] commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form
(resp. [R]).
- Remark: the operator _R sends unions to intersections because
is right adjoint to
...
- Remark: the operator _R sends unions to intersections because
Closure operators
Definition
A closure operator on is an monotonic increasing operator P on the subsets of X which satisfies:
- for all
, we have
- for all
, we have
Closure operators are quite common in mathematics and computer science. They correspond exactly to the notion of monad on a preorder...
Lemma
Write for the collection of fixed points of a closure operator P. We have that
is a complete inf-lattice.
Since any complete inf-lattice is automatically a complete sup-lattice, is also a complete sup-lattice. However, the sup operation isn't given by plain union:
Lemma
If P is a closure operator on , and if
is a (possibly infinite) family of subsets of X, we write
.
We have is a complete lattice.
Proof. easy.
A rather direct consequence of the Galois connections of the previous section is:
Lemma
The operator and and the operator
are closures.
A last trivial lemma:
Lemma
We have .
As a consequence, a subset is in
iff it is of the form
.
- Remark: everything gets a little simpler when R is a symmetric relation on X.
Phase Semantics
Phase spaces
Definition (monoid)
A monoid is simply a set X equipped with a binary operation s.t.:
- the operation is associative
- there is a neutral element
The monoid is commutative when the binary operation is commutative.
Definition (Phase space)
A phase space is given by:
- a commutative monoid
,
- together with a subset
.
The elements of X are called phases.
We write for the relation
. This relation is symmetric.
A fact in a phase space is simply a fixed point for the closure operator .
Thanks to the preliminary work, we have:
Corollary
The set of facts of a phase space is a complete lattice where:
-
is simply
,
-
is
.
Additive connectives
The previous corollary makes the following definition correct:
Definition (additive connectives)
If is a phase space, we define the following facts and operations on facts:
Once again, the next lemma follows from previous observations:
Lemma (additive de Morgan laws)
We have
Multiplicative connectives
In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space.
--- TODO ---