<p>The intuition behind coherence spaces is that the elements of a coherence space represent observations of some underlying data, and the coherence relation tells you whether two observations could have come from the same piece of data.</p>

<p>Concretely, suppose we have a set of animals</p>

<pre><code>Animals = {cat, duck, fish}
</code></pre>

<p>Now, we can have a set of observations:</p>

<pre><code>Observations = {warm-blooded, swims, water-breathing, furry}
</code></pre>

<p>Let us say that two observations are <em>compatible</em> if they could both be made of the same animal. Every observation is compatible with itself, and in addition:</p>

<ul>
<li>warm-blooded $\stackrel{{\large\frown}}{{\small\smile}}$ furry</li>
<li>warm-blooded $\stackrel{{\large\frown}}{{\small\smile}}$ swims</li>
<li>warm-blooded $\stackrel{{\large\frown}}{{\small\smile}}$ furry</li>
<li>swims $\stackrel{{\large\frown}}{{\small\smile}}$ water-breathing</li>
</ul>

<p>We know that being warm-blooded is compatible with swimming, because ducks are both warm-blooded and swim. But being warm-blooded and water-breathing are not compatible, since we have no animals which are both warm-blooded and water-breathing.</p>

<p>At this point, we have defined a coherence space (<code>Observations</code>, $\stackrel{{\large\frown}}{{\small\smile}}$), where <code>Observations</code> is the web, and $\stackrel{{\large\frown}}{{\small\smile}}$ is the coherence relation.</p>

CC BY-SA 3.0
2016-04-02T19:57:48.993Z
but as I understand, the value of type `Observations` would be a clique – thus not an observation, but a set of them. so it's more like `[Observation]`, right? the same with `Animals` (the cliques would be singletones, but still)...
valya
CC BY-SA 3.0
2016-04-02T20:07:36.390Z
of course, not even exactly `[Observation]`, but still... I'm having trouble finding an example where a non-singleton clique would make sense a value
valya
CC BY-SA 4.0
2024-02-27T10:59:32.273Z
What if there are 3 possible observations of which any 2 are compatible with each other, but all 3 together are not?
Alexey
CC BY-SA 3.0
2016-04-01T10:17:10.067Z
2016-04-01T15:57:21.527Z
2016-04-01T15:57:21.527Z
Neel Krishnaswami
<p>I always had trouble forming an intuition for coherence spaces, until I became more familiar with domain theory and read Girard's &quot;The System F of variable types, fifteen years later&quot;. Coherence spaces are just a special kind of domain, and I found it much easier to understand what coherence means starting from there. I'll try to give an explanation that made more-or-less sense to me.</p>
<p>Imagine that you want to study programs that take integer inputs to integer outputs. In general, these programs may loop forever, so it makes sense to model them mathematically as <em>partial functions</em> from integers to integers: if the program loops, the corresponding partial function is undefined on that input. We can view such a partial function <span class="math-container">$f$</span> as a <em>graph</em>: a set of pairs of integers <span class="math-container">$(n, m)$</span> such that <span class="math-container">$f$</span> is defined on <span class="math-container">$n$</span> and equal to <span class="math-container">$m$</span>. This allows us to represent these functions as a coherence space:</p>
<ul>
<li>The web of the coherence space is the set of pairs of integers <span class="math-container">$(n, m)$</span>.</li>
<li>Two pairs <span class="math-container">$(n, m)$</span> and <span class="math-container">$(n', m')$</span> are coherent if and only if <span class="math-container">$n$</span> and <span class="math-container">$n'$</span> are different, or <span class="math-container">$m$</span> and <span class="math-container">$m'$</span> are equal.</li>
</ul>
<p>By unpacking definitions, we see that every clique of this coherence space is the graph of a partial functions, and vice versa. We can interpret the coherence relation as saying that, one a partial function is defined on an input, it produces only <em>one</em> result for that input. If you're used to other kinds of domain-theoretic semantics, inclusion of cliques corresponds to the usual Scott order on partial functions on integers.</p>
<p><strong>Edit</strong></p>
<p>The above example is actually a particular case of a more general construction on coherence spaces, which is used to represent functions on coherence spaces that behave somewhat like computable functions. This construction is described in Girard's paper mentioned above, though with a slightly different terminology.</p>
<p>Let's say that <span class="math-container">$X$</span> and <span class="math-container">$Y$</span> are coherence spaces. A <em>stable function</em> of type <span class="math-container">$X \to Y$</span> is a function from cliques of <span class="math-container">$X$</span> to cliques of <span class="math-container">$Y$</span> that satisfies the following two conditions:</p>
<ol>
<li>If <span class="math-container">$a \subseteq b$</span> are cliques of <span class="math-container">$X$</span>, then <span class="math-container">$f(a) \subseteq f(b)$</span>.</li>
<li>If <span class="math-container">$(a_i)_{i \in I}$</span> is a nonempty directed family of cliques of <span class="math-container">$X$</span>, then <span class="math-container">$f\left(\bigcup_i a_i\right) = \bigcup_i f(a_i)$</span>. (&quot;Directed&quot; means that, for every <span class="math-container">$i, j \in I$</span>, there is some <span class="math-container">$k \in I$</span> such that <span class="math-container">$a_i \subseteq a_j$</span> and <span class="math-container">$a_j \subseteq a_k$</span>.)</li>
<li>If <span class="math-container">$a \cup b$</span> is a clique of <span class="math-container">$X$</span>, then <span class="math-container">$f(a \cap b) = f(a) \cap f(b)$</span>.</li>
</ol>
<hr />
<p>This definition might look weird, but simple instances are much more familiar. Let us define the following coherence space <span class="math-container">$N$</span>:</p>
<ul>
<li>The web of <span class="math-container">$N$</span> is the set of natural numbers <span class="math-container">$\mathbb{N}$</span>.</li>
<li>Two elements of the web are coherent if and only if they are equal.</li>
</ul>
<p>The cliques of <span class="math-container">$N$</span> are either singletons <span class="math-container">$\{n\}$</span> or the empty set.  Thus, we can show that a partial function of type <span class="math-container">$\mathbb{N} \to \mathbb{N}$</span> is the same thing as a stable function of type <span class="math-container">$N \to N$</span>.  More precisely, note that, in this case, the conditions 2 and 3 in the above definition are automatically satisfied. Thus, if <span class="math-container">$f : N \to N$</span> is a stable function, then we can define a partial function <span class="math-container">$g : \mathbb{N} \to \mathbb{N}$</span> by defining <span class="math-container">$g(n) = m$</span> if and only if <span class="math-container">$f(\{n\}) = \{m\}$</span>. Conversely, we can show that any partial function <span class="math-container">$g$</span> corresponds uniquely to some stable function <span class="math-container">$f$</span>.</p>
<hr />
<p>One fundamental result about coherence spaces is that stable functions between them can be represented as coherence spaces.  This is proved in Girard's paper (cf. Theorem 1.4), but here is a high-level overview. First, we can prove that every stable function <span class="math-container">$f : X \to Y$</span> is entirely determined by the set <span class="math-container">$F$</span> of pairs <span class="math-container">$(a, b)$</span> such that <span class="math-container">$a$</span> is a <em>finite</em> clique of <span class="math-container">$X$</span>, <span class="math-container">$b \in f(a)$</span>, and <span class="math-container">$b \notin f(a')$</span> for any <span class="math-container">$a' \subsetneq a$</span>. Next, we define a coherence space <span class="math-container">$X \Rightarrow Y$</span> as follows:</p>
<ul>
<li><p>The web <span class="math-container">$|X \Rightarrow Y|$</span> is the set <span class="math-container">$X_{\mathit{fin}} \times |Y|$</span>, where <span class="math-container">$X_{\mathit{fin}}$</span> denotes the set of finite cliques of <span class="math-container">$X$</span>.</p>
</li>
<li><p>Two pairs <span class="math-container">$(a, b)$</span> and <span class="math-container">$(a', b')$</span> are coherent if and only if either (1) <span class="math-container">$a = a'$</span> and <span class="math-container">$b = b'$</span>; or (2) if <span class="math-container">$a \cup a'$</span> is a clique of <span class="math-container">$X$</span>, then <span class="math-container">$b \neq b'$</span> and <span class="math-container">$b$</span> is coherent with <span class="math-container">$b'$</span>.</p>
</li>
</ul>
<p>Finally, we can show that the set of pairs <span class="math-container">$F$</span> constructed above is a clique of <span class="math-container">$X \Rightarrow Y$</span>, and that every clique of <span class="math-container">$X \Rightarrow Y$</span> arises uniquely in this way.</p>
<hr />
<p>In terms of the above example, when <span class="math-container">$X$</span> and <span class="math-container">$Y$</span> are <span class="math-container">$N$</span>, the web of the coherence space consists of pairs of the form <span class="math-container">$(\{n\}, m)$</span>, and  we can show that two pairs <span class="math-container">$(\{n\}, m)$</span> and <span class="math-container">$(\{n'\}, m')$</span> are coherent if and only if either <span class="math-container">$n \neq n'$</span> or <span class="math-container">$m = m'$</span>.  This is essentially the definition of the coherence space of partial functions on natural numbers that we gave above.</p>

CC BY-SA 4.0
2024-02-27T12:02:34.843Z
Does you example of a coherence space on pairs of integers come from Girard? Can I find it or something similar in the literature?
Alexey
CC BY-SA 4.0
2024-02-28T17:10:21.977Z
@Alexey I don't know if Girard worked out this example explicitly, but it is a particular case of a construction that appears in that paper. I have edited my answer to explain the connection.
Arthur Azevedo De Amorim
CC BY-SA 4.0
2016-08-29T17:12:26.363Z
2024-02-28T17:09:26.803Z
2024-02-28T17:09:26.803Z
Arthur Azevedo De Amorim
<p>Linear Logic is interpreted using <strong>coherent spaces</strong>, and they feature prominently in Girard's papers. I know all the three main ways to formally define them, and they don't really pose any problem to use and prove stuff about, but I just can't understand <em>what they mean</em>.</p>
<p>It really feels like there is some kind of a way to <em>understand</em> them. First of all, there're some examples about them which use functions on booleans (like at a <a href="http://llwiki.ens-lyon.fr/mediawiki/index.php/Coherent_spaces" rel="nofollow noreferrer">wiki somewhere</a>). And it hints at something interesting and meaningful behind the formal definition. However, <code>bool</code> is a very simple coherent space, with no clique of size <code>&gt; 1</code>. Can someone elaborate?</p>
<p>Another thing Girard says somewhere that every point of a coherent space represents a specific &quot;sequence of questions/answers&quot;, with two points being coherent if they &quot;bifurcate negatively (i.e., on different questions)&quot;, and incoherent if they bifurcate on different answers [1]. It seems like an easy to grasp idea but I just can't invent an example so it means I don't really get it...</p>
<p>Could someone please help me with that?</p>
<p>[1] J-Y Girard, <a href="https://girard.perso.math.cnrs.fr/longo1.pdf" rel="nofollow noreferrer">The phantom of transparency</a></p>

CC BY-SA 3.0
2016-03-30T23:51:22.037Z
Have you checked Girard's original [Linear Logic](http://iml.univ-mrs.fr/~girard/linear.pdf) paper?
Kaveh
CC BY-SA 3.0
2016-03-30T23:54:28.153Z
@Kaveh I skimmed (fastly) through it but it doesn't seem to offer anything that "The Blind Spot" doesn't have (which I read)... It has definition, but not any metaphor/interpretation/explanation.
valya
CC BY-SA 3.0
2016-03-31T00:10:36.663Z
It has been long time since I have looked at these, but I think if you really want to understand where these come from you have to go back to complete Heyting algebra and Scott domain semantics of intuitionistic logic. Domains (dcpo) are generally used for expressing partial information, two items x and y are compatible if their information can be combined, i.e. {x,y} has a sup. Coherence is just this compatibility of information. (I think the Linear Logic paper worth reading to understand where Girard's ideas are coming from.)
Kaveh
CC BY-SA 3.0
2016-03-31T01:10:34.550Z
That sound about what I should do, with domains, yeah... Thank you! I'll go wander in that direction and then, if noone answers, maybe  one day I'll write the answer myself.
valya
CC BY-SA 3.0
2016-03-31T01:17:18.510Z
(And I'll take a good look on the paper too, thanks - it turns out I skimmed the wrong one)
valya
<lo.logic><linear-logic>
How to think about coherent spaces intuitively?
valya
# How to think about coherent spaces intuitively?

(Asked by: username_0 on 2016-03-30)

Linear Logic is interpreted using **coherent spaces**, and they feature prominently in Girard's papers. I know all the three main ways to formally define them, and they don't really pose any problem to use and prove stuff about, but I just can't understand *what they mean*.

It really feels like there is some kind of a way to *understand* them. First of all, there're some examples about them which use functions on booleans (like at a [wiki somewhere](http://llwiki.ens-lyon.fr/mediawiki/index.php/Coherent_spaces)). And it hints at something interesting and meaningful behind the formal definition. However, `bool` is a very simple coherent space, with no clique of size `> 1`. Can someone elaborate?

Another thing Girard says somewhere that every point of a coherent space represents a specific "sequence of questions/answers", with two points being coherent if they "bifurcate negatively (i.e., on different questions)", and incoherent if they bifurcate on different answers [1]. It seems like an easy to grasp idea but I just can't invent an example so it means I don't really get it...

Could someone please help me with that?

[1] J-Y Girard, [The phantom of transparency](https://girard.perso.math.cnrs.fr/longo1.pdf)

**Tags:** lo.logic, linear-logic
> **Comments:**
> **username_1**: Have you checked Girard's original [Linear Logic](http://iml.univ-mrs.fr/~girard/linear.pdf) paper?  
> **username_0**: @Kaveh I skimmed (fastly) through it but it doesn't seem to offer anything that "The Blind Spot" doesn't have (which I read)... It has definition, but not any metaphor/interpretation/explanation.  
> **username_1**: It has been long time since I have looked at these, but I think if you really want to understand where these come from you have to go back to complete Heyting algebra and Scott domain semantics of intuitionistic logic. Domains (dcpo) are generally used for expressing partial information, two items x and y are compatible if their information can be combined, i.e. {x,y} has a sup. Coherence is just this compatibility of information. (I think the Linear Logic paper worth reading to understand where Girard's ideas are coming from.)  
> **username_0**: That sound about what I should do, with domains, yeah... Thank you! I'll go wander in that direction and then, if noone answers, maybe  one day I'll write the answer myself.  
> **username_0**: (And I'll take a good look on the paper too, thanks - it turns out I skimmed the wrong one)  

---

## 2 answers

### Answer by username_2 on 2016-04-01. Score: 13

The intuition behind coherence spaces is that the elements of a coherence space represent observations of some underlying data, and the coherence relation tells you whether two observations could have come from the same piece of data.
Concretely, suppose we have a set of animals
Animals = {cat, duck, fish}

Now, we can have a set of observations:
Observations = {warm-blooded, swims, water-breathing, furry}

Let us say that two observations are compatible if they could both be made of the same animal. Every observation is compatible with itself, and in addition:

warm-blooded $\stackrel{{\large\frown}}{{\small\smile}}$ furry
warm-blooded $\stackrel{{\large\frown}}{{\small\smile}}$ swims
warm-blooded $\stackrel{{\large\frown}}{{\small\smile}}$ furry
swims $\stackrel{{\large\frown}}{{\small\smile}}$ water-breathing

We know that being warm-blooded is compatible with swimming, because ducks are both warm-blooded and swim. But being warm-blooded and water-breathing are not compatible, since we have no animals which are both warm-blooded and water-breathing.
At this point, we have defined a coherence space (Observations, $\stackrel{{\large\frown}}{{\small\smile}}$), where Observations is the web, and $\stackrel{{\large\frown}}{{\small\smile}}$ is the coherence relation.

> **Comments:**
> **username_0**: but as I understand, the value of type `Observations` would be a clique – thus not an observation, but a set of them. so it's more like `[Observation]`, right? the same with `Animals` (the cliques would be singletones, but still)...  
> **username_0**: of course, not even exactly `[Observation]`, but still... I'm having trouble finding an example where a non-singleton clique would make sense a value  
> **username_3**: What if there are 3 possible observations of which any 2 are compatible with each other, but all 3 together are not?  

---

### Answer by username_4 on 2016-08-29. Score: 10

I always had trouble forming an intuition for coherence spaces, until I became more familiar with domain theory and read Girard's "The System F of variable types, fifteen years later". Coherence spaces are just a special kind of domain, and I found it much easier to understand what coherence means starting from there. I'll try to give an explanation that made more-or-less sense to me.

Imagine that you want to study programs that take integer inputs to integer outputs. In general, these programs may loop forever, so it makes sense to model them mathematically as *partial functions* from integers to integers: if the program loops, the corresponding partial function is undefined on that input. We can view such a partial function $f$ as a *graph*: a set of pairs of integers $(n, m)$ such that $f$ is defined on $n$ and equal to $m$. This allows us to represent these functions as a coherence space:

* The web of the coherence space is the set of pairs of integers $(n, m)$.
* Two pairs $(n, m)$ and $(n', m')$ are coherent if and only if $n$ and $n'$ are different, or $m$ and $m'$ are equal.

By unpacking definitions, we see that every clique of this coherence space is the graph of a partial functions, and vice versa. We can interpret the coherence relation as saying that, one a partial function is defined on an input, it produces only *one* result for that input. If you're used to other kinds of domain-theoretic semantics, inclusion of cliques corresponds to the usual Scott order on partial functions on integers.

**Edit**

The above example is actually a particular case of a more general construction on coherence spaces, which is used to represent functions on coherence spaces that behave somewhat like computable functions. This construction is described in Girard's paper mentioned above, though with a slightly different terminology.

Let's say that $X$ and $Y$ are coherence spaces. A *stable function* of type $X \to Y$ is a function from cliques of $X$ to cliques of $Y$ that satisfies the following two conditions:

1. If $a \subseteq b$ are cliques of $X$, then $f(a) \subseteq f(b)$.
2. If $(a\_i)\_{i \in I}$ is a nonempty directed family of cliques of $X$, then $f\left(\bigcup\_i a\_i\right) = \bigcup\_i f(a\_i)$. ("Directed" means that, for every $i, j \in I$, there is some $k \in I$ such that $a\_i \subseteq a\_j$ and $a\_j \subseteq a\_k$.)
3. If $a \cup b$ is a clique of $X$, then $f(a \cap b) = f(a) \cap f(b)$.

---

This definition might look weird, but simple instances are much more familiar. Let us define the following coherence space $N$:

* The web of $N$ is the set of natural numbers $\mathbb{N}$.
* Two elements of the web are coherent if and only if they are equal.

The cliques of $N$ are either singletons $\{n\}$ or the empty set. Thus, we can show that a partial function of type $\mathbb{N} \to \mathbb{N}$ is the same thing as a stable function of type $N \to N$. More precisely, note that, in this case, the conditions 2 and 3 in the above definition are automatically satisfied. Thus, if $f : N \to N$ is a stable function, then we can define a partial function $g : \mathbb{N} \to \mathbb{N}$ by defining $g(n) = m$ if and only if $f(\{n\}) = \{m\}$. Conversely, we can show that any partial function $g$ corresponds uniquely to some stable function $f$.

---

One fundamental result about coherence spaces is that stable functions between them can be represented as coherence spaces. This is proved in Girard's paper (cf. Theorem 1.4), but here is a high-level overview. First, we can prove that every stable function $f : X \to Y$ is entirely determined by the set $F$ of pairs $(a, b)$ such that $a$ is a *finite* clique of $X$, $b \in f(a)$, and $b \notin f(a')$ for any $a' \subsetneq a$. Next, we define a coherence space $X \Rightarrow Y$ as follows:

* The web $|X \Rightarrow Y|$ is the set $X\_{\mathit{fin}} \times |Y|$, where $X\_{\mathit{fin}}$ denotes the set of finite cliques of $X$.
* Two pairs $(a, b)$ and $(a', b')$ are coherent if and only if either (1) $a = a'$ and $b = b'$; or (2) if $a \cup a'$ is a clique of $X$, then $b \neq b'$ and $b$ is coherent with $b'$.

Finally, we can show that the set of pairs $F$ constructed above is a clique of $X \Rightarrow Y$, and that every clique of $X \Rightarrow Y$ arises uniquely in this way.

---

In terms of the above example, when $X$ and $Y$ are $N$, the web of the coherence space consists of pairs of the form $(\{n\}, m)$, and we can show that two pairs $(\{n\}, m)$ and $(\{n'\}, m')$ are coherent if and only if either $n \neq n'$ or $m = m'$. This is essentially the definition of the coherence space of partial functions on natural numbers that we gave above.

> **Comments:**
> **username_3**: Does you example of a coherence space on pairs of integers come from Girard? Can I find it or something similar in the literature?  
> **username_4**: @Alexey I don't know if Girard worked out this example explicitly, but it is a particular case of a construction that appears in that paper. I have edited my answer to explain the connection.  

---

