Coherent semantics - Revision history

Laurent Regnier: /* After coherent semantics */ link

2011-10-15T09:13:40Z

‎After coherent semantics: link

Laurent Regnier: /* The failure of coherent semantics */ change the title, the term failure seems unappropriate; reformulated the intro accordingly.

2011-10-15T09:00:58Z

‎The failure of coherent semantics: change the title, the term failure seems unappropriate; reformulated the intro accordingly.

Pierre-Marie Pédrot at 22:48, 4 October 2011

2011-10-04T22:48:27Z

Pierre-Marie Pédrot: ortho

2011-10-04T22:02:17Z

ortho

Pierre-Marie Pédrot: replaced paragraph with a link

2011-09-30T14:51:35Z

replaced paragraph with a link

Olivier Laurent: /* Multiplicative neutrals and the mix rule */ link to "Mix" page added

2011-03-14T13:49:49Z

‎Multiplicative neutrals and the mix rule: link to "Mix" page added

Laurent Regnier: /* Tensor product */ link to the definition of monoidal symetric closed categories

2009-03-25T21:33:48Z

‎Tensor product: link to the definition of monoidal symetric closed categories

Laurent Regnier: resectionning the mix rule

2009-03-14T11:45:32Z

resectionning the mix rule

Laurent Regnier: The mix rule

2009-03-14T11:43:41Z

The mix rule

Laurent Regnier: The Gustave function

2009-03-12T21:33:20Z

The Gustave function

@@ Line 293: / Line 293: @@
 == After coherent semantics ==
-Coherent semantics was an important milestone in the modern theory of logic of programs, in particular because it leaded to the invention of Linear Logic, and more generally because it establishes a strong link between logic and linear algebra; this link is nowadays aknowledged by the customary use of ''monoidal categories'' in logic. In some sense coherent semantics is a precursor of many forthcoming works that explore the linear nature of logic as for example [[geometry of interaction]] which interprets proofs by operators or [[finiteness semantics]] which interprets formulas as vector spaces and resulted in [[differential linear logic]]...
+Coherent semantics was an important milestone in the modern theory of logic of programs, in particular because it leaded to the invention of Linear Logic, and more generally because it establishes a strong link between logic and linear algebra; this link is nowadays aknowledged by the customary use of [[Categorical semantics|monoidal categories]] in logic. In some sense coherent semantics is a precursor of many forthcoming works that explore the linear nature of logic as for example [[geometry of interaction]] which interprets proofs by operators or [[finiteness semantics]] which interprets formulas as vector spaces and resulted in [[differential linear logic]]...
 Lots of this work have been motivated by the fact that coherent semantics is not complete as a semantics of programs (technically one says that it is not ''fully abstract''). In order to see this, let us firts come back on the origin of the central concept of ''stability'' which as pointed above originated in the study of the sequentiality in programs.

@@ Line 291: / Line 291: @@
 It is one of the main defect of coherent semantics w.r.t. linear logic that it identifies the neutrals: in coherent semantics <math>\zero = \top</math> and <math>\one = \bot</math>. However there is no known semantics of LL that solves this problem in a satisfactory way.}}
-== The failure of coherent semantics ==
+== After coherent semantics ==
-Coherent semantics was an important milestone in the modern theory of logic of programs. However it suffers from a number of defects the correction of which have motivated lots of work.
+Coherent semantics was an important milestone in the modern theory of logic of programs, in particular because it leaded to the invention of Linear Logic, and more generally because it establishes a strong link between logic and linear algebra; this link is nowadays aknowledged by the customary use of ''monoidal categories'' in logic. In some sense coherent semantics is a precursor of many forthcoming works that explore the linear nature of logic as for example [[geometry of interaction]] which interprets proofs by operators or [[finiteness semantics]] which interprets formulas as vector spaces and resulted in [[differential linear logic]]...
 === Sequentiality ===

@@ Line 396: / Line 396: @@
 </math>
-None of the two principles <math>1\limp\bot</math> and <math>\bot\limp\one</math> are valid in linear logic. To correct this one could extend the syntax of linear logic by adding the mix-rule. This is not very satisfactory as the mix rule violates some principles of [[Polarized Linear Logic]], typically the fact that as sequent of the form <math>\vdash P_1, P_2</math> where <math>P_1</math> and <math>P_2</math> are positive, is never provable.
+None of the two principles <math>1\limp\bot</math> and <math>\bot\limp\one</math> are valid in linear logic. To correct this one could extend the syntax of linear logic by adding the mix-rule. This is not very satisfactory as the mix rule violates some principles of [[Polarized linear logic]], typically the fact that as sequent of the form <math>\vdash P_1, P_2</math> where <math>P_1</math> and <math>P_2</math> are positive, is never provable.
 On the other hand the mix-rule is valid in coherent semantics so one could try to find some other model that invalidates the mix-rule. For example Girard's Coherent Banach spaces were an attempt to address this issue.

@@ Line 396: / Line 396: @@
 </math>
-None of the two principles <math>1\limp\bot</math> and <math>\bot\limp\one</math> are valid in linear logic. To correct this one could extend the syntax of linear logic by adding the mix-rule. This is not very satisfactory as the mix rule violates some principles of [[Polarised Linear Logic]], typically the fact that as sequent of the form <math>\vdash P_1, P_2</math> where <math>P_1</math> and <math>P_2</math> are positive, is never provable.
+None of the two principles <math>1\limp\bot</math> and <math>\bot\limp\one</math> are valid in linear logic. To correct this one could extend the syntax of linear logic by adding the mix-rule. This is not very satisfactory as the mix rule violates some principles of [[Polarized Linear Logic]], typically the fact that as sequent of the form <math>\vdash P_1, P_2</math> where <math>P_1</math> and <math>P_2</math> are positive, is never provable.
 On the other hand the mix-rule is valid in coherent semantics so one could try to find some other model that invalidates the mix-rule. For example Girard's Coherent Banach spaces were an attempt to address this issue.

@@ Line 37: / Line 37: @@
 {{Definition|title=Duality|
-Let <math>x</math> and <math>y</math> be two sets. We will say that they are dual, written <math>x\perp y</math> if their intersection contains at most one element: <math>\mathrm{Card}(x\cap y)\leq 1</math>.
+Let <math>x, y\subseteq \web{X}</math> be two sets. We will say that they are dual, written <math>x\perp y</math> if their intersection contains at most one element: <math>\mathrm{Card}(x\cap y)\leq 1</math>. As usual, it defines an [[orthogonality relation]] over <math>\powerset{\web{X}}</math>.}}
-Let <math>T</math> be a set and <math>X</math> be a family of subsets of <math>T</math>. We define the dual of <math>X</math> to be the collection <math>X\orth</math> of subsets of <math>T</math> that are dual to all elements of <math>X</math>:
+The last way to express the conditions on the cliques of a coherent space <math>X</math> is simply to say that we must have <math>X\biorth = X</math>.
-  <math>X\orth = \{y\subset T \text{  s.t. for any } x\in X,\, y\perp x\}</math>
+==== Equivalence of definitions ====
 Let <math>X</math> be a cliqued space and define a relation on <math>\web X</math> by setting <math>a\coh_X b</math> iff there is <math>x\in X</math> such that <math>a, b\in x</math>. This relation is obviously symetric; it is also reflexive because all singletons belong to <math>X</math>: if <math>a\in \web X</math> then <math>\{a\}</math> is dual to any element of <math>X\orth</math> (actually <math>\{a\}</math> is dual to any subset of <math>\web X</math>), thus <math>\{a\}</math> is in <math>X\biorth</math>, thus in <math>X</math>.

@@ Line 377: / Line 377: @@
 The first consequence of the identity <math>\one = \bot</math> is that the formula <math>\one\limp\bot</math> becomes provable, and so does the formula <math>\bot</math>. Note that this doesn't entail (as in classical logic or intuitionnistic logic) that linear logic is incoherent because the principle <math>\bot\limp A</math> for any formula <math>A</math> is still not provable.
-The equality <math>\one = \bot</math> has also as consequence the fact that <math>\bot\limp\one</math> (or equivalently the formula <math>\one\parr\one</math>) is provable. This principle is also known as the ''mix rule''
+The equality <math>\one = \bot</math> has also as consequence the fact that <math>\bot\limp\one</math> (or equivalently the formula <math>\one\parr\one</math>) is provable. This principle is also known as the [[Mix|mix rule]]
 <math>

@@ Line 191: / Line 191: @@
 {{Theorem|
-The category of coherent spaces with linear maps and tensor product is monoidal symetric closed.
+The category of coherent spaces with linear maps and tensor product is [[Categorical semantics#Modeling IMLL|monoidal symetric closed]].
 }}

@@ Line 371: / Line 371: @@
 Antonio Bucciarelli and Thomas Ehrhard.
-== The mix rule ==
+=== Multiplicative neutrals and the mix rule ===
 Coherent semantics is slightly degenerated w.r.t. linear logic because it identifies multiplicative neutrals (it also identifies additive neutrals but that's yet another problem): the coherent spaces <math>\one</math> and <math>\bot</math> are equal.

@@ Line 365: / Line 365: @@
 In other terms there is no way to implement the Gustave function by a lambda-term (or in any sequential programming language). Thus coherent semantics is not complete w.r.t. lambda-calculus.
-The research for finding a right model for sequentiality was the motivation for lots of work, ''e.g.'', ''sequential algorithms'' by Gérard Bérry and Pierre-Louis Currien in the early eighties, that were more recently reformulated as a kind of [[Game semantics|game model]], and the theory of ''hypercoherent spaces'' by Antonio Bucciarelli and Thomas Ehrhard.
+The research for a right model for sequentiality was the motivation for lot of
 == References ==

@@ Line 304: / Line 304: @@
 === Sequentiality ===
-For a while one may have believed that the stability condition on which coherent semantics is built was enough to capture the notion of ''sequentiality'' of programs. A hint was the already mentionned fact that the parallel or, the typical non sequential program, is not stable. This diserves a bit of explanation.
+Sequentiality is a property that we will not define here (it would diserve its own article). We rely on the intuition that a function of <math>n</math> arguments is sequential if one can determine which of these argument is examined first during the computation. Obviously any function implemented in a functionnal language is sequential; for example the function ''or'' defined à la CAML by:
 ==== The parallel or is not stable ====
@@ Line 329: / Line 329: @@
 Another way to see this is: suppose <math>x</math> and <math>y</math> are two cliques of <math>B</math> such that <math>tt\in \mathrm{Por}\langle x, y\rangle</math>, which means that <math>\mathrm{Por}\langle x, y\rangle = T</math>; according to the [[#Stable functions|caracterisation theorem of stable functions]], if <math>\mathrm{Por}</math> were stable then there would be a unique minimum <math>x_0</math> included in <math>x</math>, and a unique minimum <math>y_0</math> included in <math>y</math> such that <math>\mathrm{Por}\langle x_0, y_0\rangle = T</math>. This is not the case because both <math>\langle T,\bot\rangle</math> and <math>\langle T,\bot\rangle</math> are minimal such that their value is <math>T</math>.
-In other terms, knowing that <math>\mathrm{Por}\langle x, y\rangle = T</math> doesn't tell which of <math>x</math> of <math>y</math> is responsible for that, although we know by the definition of <math>\mathrm{Por}</math> that only one of them is. This example is the typical non sequential function. Indeed the <math>\mathrm{Por}</math> function is not representable in sequential programming languages such as (typed) lambda-calculus.
+In other terms, knowing that <math>\mathrm{Por}\langle x, y\rangle = T</math> doesn't tell which of <math>x</math> of <math>y</math> is responsible for that, although we know by the definition of <math>\mathrm{Por}</math> that only one of them is. Indeed the <math>\mathrm{Por}</math> function is not representable in sequential programming languages such as (typed) lambda-calculus.
 So the first genuine idea would be that stability caracterises sequentiality; but...
 ==== The Gustave function is stable ====
 == References ==