Phase semantics

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

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 $(a,b) \in R$ or $a\mathrel{R} b$ to say that $a\in X$ and $b\in Y$ are related.

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

Such a relation yields three interesting operators acting on subsets of Y:

Definition

Let $R\subseteq X\times Y$ be a relation, define the operators $\langle R\rangle$, [R] and _^R taking subsets of X to subsets of Y as follows:

1. $b\in\langle R\rangle(x)$ iff $\exists a\in X,\ (a,b)\in R \land a\in x$
2. $b\in[R](x)$ iff $\forall a\in Y,\ (a,b)\in R \implies a\in x$
3. $b\in x^R$ iff $\forall a\in x, (a,b)\in R$
   

The operator $\langle R\rangle$ 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 $\langle R\rangle$ and [R] are covariant (increasing for the $\subseteq$ relation) while _^R is contravariant (decreasing for the $\subseteq$ relation). More interesting:

Lemma (Galois Connections)

1. $\langle R\rangle$ is right-adjoint to [R^˜]: for any $x\subseteq X$ and $y\subseteq Y$, we have $[R^\sim]y \subseteq x$ iff $y\subseteq \langle R\rangle(x)$
2. we have $y\subseteq x^R$ iff $x\subseteq y^{R^\sim}$
   

This implies directly that $\langle R\rangle$ 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 $\langle R\rangle$ (resp. [R]).

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

Closure operators

Definition

A closure operator on $\mathcal{P}(X)$ is an monotonic increasing operator P on the subsets of X which satisfies:

1. for all $x\subseteq X$, we have $x\subseteq P(x)$
2. for all $x\subseteq X$, we have $P(P(x))\subseteq P(x)$
   

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

Lemma

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

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

Lemma

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

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

Proof.  easy.

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

Lemma

The operator and $\langle R\rangle \circ [R^\sim]$ and the operator $x\mapsto {x^R}^{R^\sim}$ are closures.

A last trivial lemma:

Lemma

We have $x^R = {{x^R}^{R^\sim}}^{R}$.

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

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 $\_\cdot\_$ s.t.:

1. the operation is associative
2. there is a neutral element $1\in X$

The monoid is commutative when the binary operation is commutative.

Definition (Phase space)

A phase space is given by:

1. a commutative monoid $(X,1,\cdot)$,
2. together with a subset $\bot\!\!\!\bot\subseteq X$.

The elements of X are called phases.

We write $\bot$ for the relation $\{(a,b)\ |\ a\cdot b \in \bot\!\!\!\bot\}$. This relation is symmetric.

A fact in a phase space is simply a fixed point for the closure operator $x\mapsto x^{\bot\bot}$.

Thanks to the preliminary work, we have:

Corollary

The set of facts of a phase space is a complete lattice where:

1. $\bigwedge$ is simply $\bigcap$,
2. $\bigvee$ is $\left(\bigcup ...\right)^{\bot\bot}$.
   

Additive connectives

The previous corollary makes the following definition correct:

Definition (additive connectives)

If $(X,1,\cdot,\bot\!\!\bot$ is a phase space, we define the following facts and operations on facts:

1. $\top = X = \emptyset^\bot$
2. $\zero = \emptyset^{\bot\bot} = X^\bot$
3. $x\plus y = (x\cup y)^{\bot\bot}$
4. $x\with y = x\cap y$
   

Once again, the next lemma follows from previous observations:

Lemma (additive de Morgan laws)

We have

1. $\zero^\bot = \top$
2. $\top^\bot = \zero$
3. $(x\plus y)^\bot = x^\bot \with y^\bot$
4. $(x\with y)^\bot = x^\bot \plus y^\bot$
   

Multiplicative connectives

In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space.

--- TODO ---