LLWiki - User contributions [en]

Talk:Phase semantics

2009-02-08T21:13:50Z

Pierre Hyvernat: /* Phase semantics */ new section

== Preliminaries: relations and closures ==

===References===

I think everything I write in the preliminaries can be found in Birkhoff, "Lattice theory". Can anyone check? (I don't think I have easy access to a copy.

In particular, I think <math>x^R</math> was written <math>x^{\leftarrow}</math>, with the relation <math>R</math> being implicit.

If so, we should add a reference to that.

-- [[User:Pierre Hyvernat|Pierre Hyvernat]] 11:22, 8 February 2009 (UTC)

===Notation===

The refinement calculus people use the relation in the reverse order: what I write <math>\langle R\rangle</math>, they write <math>\langle R^\sim\rangle</math>. (The same is true of <math>[R]</math>.) I find it confusing, and since this is hardly "standard" notation one way or the other, I don't think this is important...

-- [[User:Pierre Hyvernat|Pierre Hyvernat]] 11:27, 8 February 2009 (UTC)

== Phase semantics ==

===Realisability===

I put the remark

:{{Remark|
:Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}}

at the end of the subsection "multiplicative connectives".

Has anybody heard the same about Tait proof and biorthogonal?

-- [[User:Pierre Hyvernat|Pierre Hyvernat]] 21:13, 8 February 2009 (UTC)

Phase semantics

2009-02-08T21:08:19Z

Pierre Hyvernat: /* Exponentials */

=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 <math>R</math> between two sets <math>X</math> and <math>Y</math>. Using standard mathematical practice, we can write either <math>(a,b) \in R</math> or <math>a\mathrel{R} b</math> to say that <math>a\in X</math> and <math>b\in Y</math> are related.

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

Such a relation yields three interesting operators sending subsets of <math>X</math> to subsets of <math>Y</math>:

{{Definition|
Let <math>R\subseteq X\times Y</math> be a relation, define the operators <math>\langle R\rangle</math>, <math>[R]</math> and <math>\_^R</math> taking subsets of <math>X</math> to subsets of <math>Y</math> as follows:
# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in X,\ (a,b)\in R \land a\in x</math>
# <math>b\in[R](x)</math> iff <math>\forall a\in X,\ (a,b)\in R \implies a\in x</math>
# <math>b\in x^R</math> iff <math>\forall a\in x, (a,b)\in R</math>
}}

The operator <math>\langle R\rangle</math> is usually called the ''direct image'' of the relation, <math>[R]</math> is sometimes called the ''universal image'' of the relation.

It is trivial to check that <math>\langle R\rangle</math> and <math>[R]</math> are covariant (increasing for the <math>\subseteq</math> relation) while <math>\_^R</math> is contravariant (decreasing for the <math>\subseteq</math> relation). More interesting:

{{Lemma|title=Galois Connections|
# <math>\langle R\rangle</math> is right-adjoint to <math>[R^\sim]</math>: for any <math>x\subseteq X</math> and <math>y\subseteq Y</math>, we have <math>[R^\sim]y \subseteq x</math> iff <math>y\subseteq \langle R\rangle(x)</math>
# we have <math>y\subseteq x^R</math> iff <math>x\subseteq y^{R^\sim}</math>
}}

This implies directly that <math>\langle R\rangle</math> commutes with arbitrary unions and <math>[R]</math> commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form <math>\langle R\rangle</math> (resp. <math>[R]</math>).

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

==Closure operators==

{{Definition|
A closure operator on <math>\mathcal{P}(X)</math> is an monotonic increasing operator <math>P</math> on the subsets of <math>X</math> which satisfies:
# for all <math>x\subseteq X</math>, we have <math>x\subseteq P(x)</math>
# for all <math>x\subseteq X</math>, we have <math>P(P(x))\subseteq P(x)</math>
}}

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

It follows directly from the definition that for any closure operator <math>P</math>, the image <math>P(x)</math> is a fixed point of <math>P</math>. Moreover:
{Lemma|
<math>P(x)</math> is the smallest fixed point of <math>P</math> containing <math>x</math>.
}}

One other important property is the following:

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

{{Remark|
A closure operator is in fact determined by its set of fixed points: we have <math>P(x) = \bigcup \{ y\ |\ y\in\mathcal{F}(P),\,y\subseteq x\}</math>}}

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

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

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

{{Proof|
easy.
}}

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

{{Lemma|
The operator and <math>\langle R\rangle \circ [R^\sim]</math> and the operator <math>x\mapsto {x^R}^{R^\sim}</math> are closures.
}}

A last trivial lemma:

{{Lemma|
We have <math>x^R = {{x^R}^{R^\sim}}^{R}</math>.

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

{{Remark|everything gets a little simpler when <math>R</math> is a symmetric relation on <math>X</math>.}}

=Phase Semantics=

==Phase spaces==

{{Definition|title=monoid|
A monoid is simply a set <math>X</math> equipped with a binary operation <math>\_\cdot\_</math> s.t.:
# the operation is associative
# there is a neutral element <math>1\in X</math>
The monoid is ''commutative'' when the binary operation is commutative.
}}

{{Definition|title=Phase space|
A phase space is given by:
# a commutative monoid <math>(X,1,\cdot)</math>,
# together with a subset <math>\Bot\subseteq X</math>.
The elements of <math>X</math> are called ''phases''.

We write <math>\bot</math> for the relation <math>\{(a,b)\ |\ a\cdot b \in \Bot\}</math>. This relation is symmetric.

A ''fact'' in a phase space is simply a fixed point for the closure operator <math>x\mapsto x\biorth</math>.
}}

Thanks to the preliminary work, we have:

{{Corollary|
The set of facts of a phase space is a complete lattice where:
# <math>\bigwedge_{i\in I} x_i</math> is simply <math>\bigcap_{i\in I} x_i</math>,
# <math>\bigvee_{i\in I} x_i</math> is <math>\left(\bigcup_{i\in I} x_i\right)\biorth</math>.
}}

==Additive connectives==

The previous corollary makes the following definition correct:

{{Definition|title=additive connectives|
If <math>(X,1,\cdot,\Bot)</math> is a phase space, we define the following facts and operations on facts:
# <math>\top = X = \emptyset\orth</math>
# <math>\zero = \emptyset\biorth = X\orth</math>
# <math>x\with y = x\cap y</math>
# <math>x\plus y = (x\cup y)\biorth</math>
}}

Once again, the next lemma follows from previous observations:

{{Lemma|title=additive de Morgan laws|
We have
# <math>\zero\orth = \top</math>
# <math>\top\orth = \zero</math>
# <math>(x\with y)\orth = x\orth \plus y\orth</math>
# <math>(x\plus y)\orth = x\orth \with y\orth</math>
}}

==Multiplicative connectives==

In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space. One interpretation that is reminiscent in phase semantics is that our spaces are collections of ''tests'' / programs / proofs / ''strategies'' that can interact with each other. The result of the interaction between <math>a</math> and <math>b</math> is simply <math>a\cdot b</math>.

The set <math>\Bot</math> can be thought of as the set of "good" things, and we thus have <math>a\in x\orth</math> iff "<math>a</math> interacts correctly with all the elements of <math>x</math>".

{{Definition|
If <math>x</math> and <math>y</math> are two subsets of a phase space, we write <math>x\cdot y</math> for the set <math>\{a\cdot b\ |\ a\in x, b\in y\}</math>.
}}
Thus <math>x\cdot y</math> contains all the possible interactions between one element of <math>x</math> and one element of <math>y</math>.

The tensor connective of linear logic is now defined as:

{{Definition| title=multiplicative connectives|
If <math>x</math> and <math>y</math> are facts in a phase space, we define
* <math>\one = \{1\}\orth</math>;
* <math>\bot = \one\orth</math>;
* the tensor <math>x\tens y</math> to be the fact <math>(x\cdot y)\biorth</math>;
* the par connective is the de Morgan dual of the tensor: <math>x\parr y = (x\orth \tens y\orth)\orth</math>;
* the linear arrow is just <math>x\limp y = (x\tens y\orth)\orth</math>.
}}

Note that by unfolding the definition of <math>\limp</math>, we have the following, "intuitive" definition of <math>x\limp y</math>:

{{Lemma|
If <math>x</math> and <math>y</math> are facts, we have <math>a\in x\limp y</math> iff <math>\forall b\in x,\,a\cdot b\in y</math>
}}

{{Proof|
easy exercise. }}

Readers familiar with realisability will appreciate...

{{Remark|
Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}}

==Properties==

All the expected properties hold:

{{Lemma|
* The operations <math>\tens</math>, <math>\parr</math>, <math>\plus</math> and <math>\with</math> are commutative and associative,
* They have respectively <math>\one</math>, <math>\bot</math>, <math>\zero</math> and <math>\top</math> for neutral element,
* <math>\zero</math> is absorbant for <math>\tens</math>,
* <math>\top</math> is absorbant for <math>\parr</math>,
* <math>\tens</math> distributes over <math>\plus</math>,
* <math>\parr</math> distributes over <math>\with</math>.
}}

==Exponentials==

{{Definition|title=Exponentials|
Write <math>I</math> for the set of idempotents of a phase space: <math>I=\{a\ |\ a\cdot a=a\}</math>. We put:
# <math>\oc x = (x\cap I\cap \one)\biorth</math>,
# <math>\wn x = (x\orth\cap I\cap\one)\orth</math>.
}}

This definition captures precisely the intuition behind the exponentials:
* we need to have contraction, hence we restrict to indempotents in <math>x</math>,
* and weakening, hence we restrict to <math>\one</math>.
Since <math>I</math> isn't necessarily a fact, we then take the biorthogonal to get a fact...

=Completeness=

=The Rest=

Phase semantics

2009-02-08T20:59:40Z

Pierre Hyvernat: /* Closure operators */

Phase semantics

2009-02-08T20:52:52Z

Pierre Hyvernat: /* Multiplicative connectives */

=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 <math>R</math> between two sets <math>X</math> and <math>Y</math>. Using standard mathematical practice, we can write either <math>(a,b) \in R</math> or <math>a\mathrel{R} b</math> to say that <math>a\in X</math> and <math>b\in Y</math> are related.

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

Such a relation yields three interesting operators sending subsets of <math>X</math> to subsets of <math>Y</math>:

{{Definition|
Let <math>R\subseteq X\times Y</math> be a relation, define the operators <math>\langle R\rangle</math>, <math>[R]</math> and <math>\_^R</math> taking subsets of <math>X</math> to subsets of <math>Y</math> as follows:
# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in X,\ (a,b)\in R \land a\in x</math>
# <math>b\in[R](x)</math> iff <math>\forall a\in X,\ (a,b)\in R \implies a\in x</math>
# <math>b\in x^R</math> iff <math>\forall a\in x, (a,b)\in R</math>
}}

The operator <math>\langle R\rangle</math> is usually called the ''direct image'' of the relation, <math>[R]</math> is sometimes called the ''universal image'' of the relation.

It is trivial to check that <math>\langle R\rangle</math> and <math>[R]</math> are covariant (increasing for the <math>\subseteq</math> relation) while <math>\_^R</math> is contravariant (decreasing for the <math>\subseteq</math> relation). More interesting:

{{Lemma|title=Galois Connections|
# <math>\langle R\rangle</math> is right-adjoint to <math>[R^\sim]</math>: for any <math>x\subseteq X</math> and <math>y\subseteq Y</math>, we have <math>[R^\sim]y \subseteq x</math> iff <math>y\subseteq \langle R\rangle(x)</math>
# we have <math>y\subseteq x^R</math> iff <math>x\subseteq y^{R^\sim}</math>
}}

This implies directly that <math>\langle R\rangle</math> commutes with arbitrary unions and <math>[R]</math> commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form <math>\langle R\rangle</math> (resp. <math>[R]</math>).

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

==Closure operators==

{{Definition|
A closure operator on <math>\mathcal{P}(X)</math> is an monotonic increasing operator <math>P</math> on the subsets of <math>X</math> which satisfies:
# for all <math>x\subseteq X</math>, we have <math>x\subseteq P(x)</math>
# for all <math>x\subseteq X</math>, we have <math>P(P(x))\subseteq P(x)</math>
}}

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

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

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

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

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

{{Proof|
easy.
}}

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

{{Lemma|
The operator and <math>\langle R\rangle \circ [R^\sim]</math> and the operator <math>x\mapsto {x^R}^{R^\sim}</math> are closures.
}}

A last trivial lemma:

{{Lemma|
We have <math>x^R = {{x^R}^{R^\sim}}^{R}</math>.

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

{{Remark|everything gets a little simpler when <math>R</math> is a symmetric relation on <math>X</math>.}}

=Phase Semantics=

==Phase spaces==

{{Definition|title=monoid|
A monoid is simply a set <math>X</math> equipped with a binary operation <math>\_\cdot\_</math> s.t.:
# the operation is associative
# there is a neutral element <math>1\in X</math>
The monoid is ''commutative'' when the binary operation is commutative.
}}

{{Definition|title=Phase space|
A phase space is given by:
# a commutative monoid <math>(X,1,\cdot)</math>,
# together with a subset <math>\Bot\subseteq X</math>.
The elements of <math>X</math> are called ''phases''.

We write <math>\bot</math> for the relation <math>\{(a,b)\ |\ a\cdot b \in \Bot\}</math>. This relation is symmetric.

A ''fact'' in a phase space is simply a fixed point for the closure operator <math>x\mapsto x\biorth</math>.
}}

Thanks to the preliminary work, we have:

{{Corollary|
The set of facts of a phase space is a complete lattice where:
# <math>\bigwedge_{i\in I} x_i</math> is simply <math>\bigcap_{i\in I} x_i</math>,
# <math>\bigvee_{i\in I} x_i</math> is <math>\left(\bigcup_{i\in I} x_i\right)\biorth</math>.
}}

==Additive connectives==

The previous corollary makes the following definition correct:

{{Definition|title=additive connectives|
If <math>(X,1,\cdot,\Bot)</math> is a phase space, we define the following facts and operations on facts:
# <math>\top = X = \emptyset\orth</math>
# <math>\zero = \emptyset\biorth = X\orth</math>
# <math>x\with y = x\cap y</math>
# <math>x\plus y = (x\cup y)\biorth</math>
}}

Once again, the next lemma follows from previous observations:

{{Lemma|title=additive de Morgan laws|
We have
# <math>\zero\orth = \top</math>
# <math>\top\orth = \zero</math>
# <math>(x\with y)\orth = x\orth \plus y\orth</math>
# <math>(x\plus y)\orth = x\orth \with y\orth</math>
}}

==Multiplicative connectives==

In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space. One interpretation that is reminiscent in phase semantics is that our spaces are collections of ''tests'' / programs / proofs / ''strategies'' that can interact with each other. The result of the interaction between <math>a</math> and <math>b</math> is simply <math>a\cdot b</math>.

The set <math>\Bot</math> can be thought of as the set of "good" things, and we thus have <math>a\in x\orth</math> iff "<math>a</math> interacts correctly with all the elements of <math>x</math>".

{{Definition|
If <math>x</math> and <math>y</math> are two subsets of a phase space, we write <math>x\cdot y</math> for the set <math>\{a\cdot b\ |\ a\in x, b\in y\}</math>.
}}
Thus <math>x\cdot y</math> contains all the possible interactions between one element of <math>x</math> and one element of <math>y</math>.

The tensor connective of linear logic is now defined as:

{{Definition| title=multiplicative connectives|
If <math>x</math> and <math>y</math> are facts in a phase space, we define
* <math>\one = \{1\}\orth</math>;
* <math>\bot = \one\orth</math>;
* the tensor <math>x\tens y</math> to be the fact <math>(x\cdot y)\biorth</math>;
* the par connective is the de Morgan dual of the tensor: <math>x\parr y = (x\orth \tens y\orth)\orth</math>;
* the linear arrow is just <math>x\limp y = (x\tens y\orth)\orth</math>.
}}

Note that by unfolding the definition of <math>\limp</math>, we have the following, "intuitive" definition of <math>x\limp y</math>:

{{Lemma|
If <math>x</math> and <math>y</math> are facts, we have <math>a\in x\limp y</math> iff <math>\forall b\in x,\,a\cdot b\in y</math>
}}

{{Proof|
easy exercise. }}

Readers familiar with realisability will appreciate...

{{Remark|
Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}}

==Properties==

All the expected properties hold:

{{Lemma|
* The operations <math>\tens</math>, <math>\parr</math>, <math>\plus</math> and <math>\with</math> are commutative and associative,
* They have respectively <math>\one</math>, <math>\bot</math>, <math>\zero</math> and <math>\top</math> for neutral element,
* <math>\zero</math> is absorbant for <math>\tens</math>,
* <math>\top</math> is absorbant for <math>\parr</math>,
* <math>\tens</math> distributes over <math>\plus</math>,
* <math>\parr</math> distributes over <math>\with</math>.
}}

==Exponentials==

=Completeness=

=The Rest=

Phase semantics

2009-02-08T11:50:06Z

Pierre Hyvernat: /* Multiplicative connectives */

Phase semantics

2009-02-08T11:42:27Z

Pierre Hyvernat: /* Additive connectives */

Phase semantics

2009-02-08T11:40:54Z

Pierre Hyvernat: /* Phase spaces */

Phase semantics

2009-02-08T11:38:22Z

Pierre Hyvernat: /* Closure operators */

Phase semantics

2009-02-08T11:36:33Z

Pierre Hyvernat: /* Relations and operators on subsets */

User:Pierre Hyvernat

2009-02-08T11:30:15Z

Pierre Hyvernat: New page: You're probably better of looking at my official [http://www.lama.univ-savoie.fr/~hyvernat/ web page]...

You're probably better of looking at my official [http://www.lama.univ-savoie.fr/~hyvernat/ web page]...

Talk:Phase semantics

2009-02-08T11:27:56Z

Pierre Hyvernat: /* Preliminaries: relations and closures */

Talk:Phase semantics

2009-02-08T11:22:57Z

Pierre Hyvernat: Preliminaries: relations and closures

== Preliminaries: relations and closures ==

I think everything I write in the preliminaries can be found in Birkhoff, "Lattice theory". Can anyone check? (I don't think I have easy access to a copy.

In particular, I think <math>x^R</math> was written <math>x^{\leftarrow}</math>, with the relation <math>R</math> being implicit.

If so, we should add a reference to that.

-- [[User:Pierre Hyvernat|Pierre Hyvernat]] 11:22, 8 February 2009 (UTC)

Phase semantics

2009-02-08T11:17:37Z

Pierre Hyvernat: /* Preliminaries: relation and closure operators */

Phase semantics

2009-02-08T11:13:24Z

Pierre Hyvernat: /* Introduction */

Phase semantics

2009-02-08T11:12:12Z

Pierre Hyvernat: initial page: preliminaries and additives

=Introduction=

The semantics given by phase spaces is a kind of "truth semantics", and is thus quite different from the more usual denotational semantics of linear logic. (Those are rather some "proof 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 <math>R</math> between two sets <math>X</math> and <math>Y</math>. Using standard mathematical practice, we can write either <math>(a,b) \in R</math> or <math>a\mathrel{R} b</math> to say that <math>a\in X</math> and <math>b\in Y</math> are related.

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

Such a relation yields three interesting operators acting on subsets of <math>Y</math>:

{{Definition|
Let <math>R\subseteq X\times Y</math> be a relation, define the operators <math>\langle R\rangle</math>, <math>[R]</math> and <math>\_^R</math> taking subsets of <math>X</math> to subsets of <math>Y</math> as follows:
# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in X,\ (a,b)\in R \land a\in x</math>
# <math>b\in[R](x)</math> iff <math>\forall a\in Y,\ (a,b)\in R \implies a\in x</math>
# <math>b\in x^R</math> iff <math>\forall a\in x, (a,b)\in R</math>
}}

The operator <math>\langle R\rangle</math> is usually called the direct image of the relation, <math>[R]</math> is sometimes called the universal image of the relation.

It is trivial to check that <math>\langle R\rangle</math> and <math>[R]</math> are covariant (increasing for the <math>\subseteq</math> relation) while <math>\_^R</math> is contravariant (decreasing for the <math>\subseteq</math> relation). More interesting:

{{Lemma|title=Galois Connections|
# <math>\langle R\rangle</math> is right-adjoint to <math>[R^\sim]</math>: for any <math>x\subseteq X</math> and <math>y\subseteq Y</math>, we have <math>[R^\sim]y \subseteq x</math> iff <math>y\subseteq \langle R\rangle(x)</math>
# we have <math>y\subseteq x^R</math> iff <math>x\subseteq y^{R^\sim}</math>
}}

This implies directly that <math>\langle R\rangle</math> commutes with arbitrary unions and <math>[R]</math> commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form <math>\langle R\rangle</math> (resp. <math>[R]</math>).

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

==Closure operators==

{{Definition|
A closure operator on <math>\mathcal{P}(X)</math> is an monotonic increasing operator <math>P</math> on the subsets of <math>X</math> which satisfies:
# for all <math>x\subseteq X</math>, we have <math>x\subseteq P(x)</math>
# for all <math>x\subseteq X</math>, we have <math>P(P(x))\subseteq P(x)</math>
}}

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

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

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

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

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

{{Proof|
easy.
}}

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

{{Lemma|
The operator and <math>\langle R\rangle \circ [R^\sim]</math> and the operator <math>x\mapsto {x^R}^{R^\sim}</math> are closures.
}}

A last trivial lemma:

{{Lemma|
We have <math>x^R = {{x^R}^{R^\sim}}^{R}</math>.

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

::''Remark:'' everything gets a little simpler when <math>R</math> is a symmetric relation on <math>X</math>.

=Phase Semantics=

==Phase spaces==

{{Definition|title=monoid|
A monoid is simply a set <math>X</math> equipped with a binary operation <math>\_\cdot\_</math> s.t.:
# the operation is associative
# there is a neutral element <math>1\in X</math>
The monoid is ''commutative'' when the binary operation is commutative.
}}

{{Definition|title=Phase space|
A phase space is given by:
# a commutative monoid <math>(X,1,\cdot)</math>,
# together with a subset <math>\bot\!\!\!\bot\subseteq X</math>.
The elements of <math>X</math> are called ''phases''.

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

A ''fact'' in a phase space is simply a fixed point for the closure operator <math>x\mapsto x^{\bot\bot}</math>.
}}

Thanks to the preliminary work, we have:

{{Corollary|
The set of facts of a phase space is a complete lattice where:
# <math>\bigwedge</math> is simply <math>\bigcap</math>,
# <math>\bigvee</math> is <math>\left(\bigcup ...\right)^{\bot\bot}</math>.
}}

==Additive connectives==

The previous corollary makes the following definition correct:

{{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:
# <math>\top = X = \emptyset^\bot</math>
# <math>\zero = \emptyset^{\bot\bot} = X^\bot</math>
# <math>x\plus y = (x\cup y)^{\bot\bot}</math>
# <math>x\with y = x\cap y</math>
}}

Once again, the next lemma follows from previous observations:

{{Lemma|title=additive de Morgan laws|
We have
# <math>\zero^\bot = \top</math>
# <math>\top^\bot = \zero</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==

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

--- TODO ---

==Exponentials==

=Completeness=

=The Rest=