13
$\begingroup$

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). 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. URL: http://iml.univ-mrs.fr/~girard/longo1.pdf

$\endgroup$
  • $\begingroup$ Have you checked Girard's original Linear Logic paper? $\endgroup$ – Kaveh Mar 30 '16 at 23:51
  • $\begingroup$ @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. $\endgroup$ – valya Mar 30 '16 at 23:54
  • 2
    $\begingroup$ 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.) $\endgroup$ – Kaveh Mar 31 '16 at 0:10
  • $\begingroup$ 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. $\endgroup$ – valya Mar 31 '16 at 1:10
  • $\begingroup$ (And I'll take a good look on the paper too, thanks - it turns out I skimmed the wrong one) $\endgroup$ – valya Mar 31 '16 at 1:17
10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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)... $\endgroup$ – valya Apr 2 '16 at 19:57
  • $\begingroup$ 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 $\endgroup$ – valya Apr 2 '16 at 20:07
6
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.