Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
David C. has kindly created a list of references at Geometry of Interaction. I have now started there an Idea section:
What has been called Geometry of Interaction (Girard 89) is a kind of semantics for linear logic/linear type theory that is however different in method from the usual categorical semantics in monoidal categories. Instead of interpreting a proof of linear implication $A\multimap B$ as a morphism between objects $A$ and $B$ in a monoidal category as in categorical semantics, the Geometry of Interaction interprets it as an endomorphism on the object $A\multimap B$. This has been named operational semantics to contrast with the traditional denotational semantics.
That also the “operational semantics” of GoI has an interpretation in category theory, though, namely in traced monoidal categories was first suggested in (Joyal-Street-Verity 96) and then developed out in (Haghverdi 00, Abramsky-Haghverdi-Scott 02,Haghverdi-Scott 05).
I have started to look around through the references, but I still only have a vague idea of “what’s going on” and what the point and motivation is.
The “GoI construction” in def. 2.6 of Abramsky et al is vaguely reminiscent of quantum operations, but I am not sure if I am seeing yet where this is headed.
If anyone has a few words as to in which way GoI thinks of a proof as an endomorphism and in which way we are to think of this geometrically in a traced monoidal category, please give it a try.
Let me expand on that. It seems obvious that the “Geometry of Interaction” is about “quantum operations” in the sense as they are used in in the discussion of completely positive maps, as on the last pages of Selinger 05. Is that right? If so, where is this discussed explicitly (I can’t seem to see anything…)
To expand:
in terms of that categorical semantics, given a traced monoidal category, $\mathcal{C}$, then the “Geometry of Interaction”-category $\mathcal{G}(\mathcal{C})$ as in def. 2.6 of Abramsky et al.
has as obects pairs of objects $(A^+, A^-)$ in $\mathcal{C}$ and morphisms $(A^+, A^-) \to (B^+, B^-)$ are maps in $\mathcal{C}$ of the form
$A^+ \otimes B^- \longrightarrow A^- \otimes B^+ \,.$Now consider the special case that the traced structure on$\mathcal{C}$ does happen to come from a compact closed structure. In this case such a morphism is equivalently
$(A^-)^\ast \otimes A^+ \longrightarrow B^+ \otimes (B^-)^\ast$and composition with the symmetry makes that equivalently be of the form
$(A^-)^\ast \otimes A^+ \longrightarrow (B^-)^\ast \otimes B^+ \,.$Now this is a “quantum operation” (or a slight generalization thereof, it is a quantum operation proper in the usual sense only when $A^- \simeq A^+$ and $B^- \simeq B^+$. But this is not crucial for anything.)
Moreover, and that’s the (obvious) point which I mean to speak about here, the evident composition of the “quantum operations” (by manifest direct composition) translates under the above identification to that more intricate-looking composition by “symmetric feedback” of the original maps in the form
$A^+ \otimes B^- \longrightarrow A^- \otimes B^+ \,.$as in that def. 2.6 of Abramsky et al..
So I suppose in general we can view the “Geometry of Interaction”-category $\mathcal{G}(\mathcal{C})$ as a stand-in for the category of “quantum operations” in $\mathcal{C}$ for the case that $\mathcal{C}$ need not be compact closed.
Right? This is either trivial and well-discussed somewhere or else it is misled in some aspect.
I’m finding it hard to get any sense of the motivation for GoI. But perhaps the proof-theoretic origin doesn’t matter if the focus is on a linear homotopy type theory for physics.
Yes, me too. I was looking at section VI in Girard’s Lectures on Logic, but while I follow the “now we do this, then we do that”-pattern, I am not sure where we are coming from and where we are headed. And various secondary articles involving GoI that I turn to point the reader to these lectures for explanation…
But I am happy with the categorical semantics in Abramsky et al. According to them, whatever GoI is motivated by, it ends up essentially being the internal language of those compact closed categories which arise as $Int(\mathcal{C})$ freely from traced monoidal categories $\mathcal{C}$, as discussed there.
And (in the miniscule spare time that I have) I keep coming back to the observation mentioned above: if we want to really think about GoI in terms of interpretation in quantum physics here (my reading is that Girard really wanted to, though I am a bit puzzled about what he may have suggested that the upshot was, in this respect) then the $Int(-)$ construction is noteworthy as being very closely related to the construction of what are called “categories of quantum operations”.
I just found what I think is another example of that, see the fairly recent
First they review Selinger’s CPM construction, and one can see that this is a special case of the $Int(-)$-construction. Then they generalize the CPM construction in their Def. 1, and if you just put these pictures next to those in def. 2.6 of Abramsky et al., you see that this is still a special case of the $Int(-)$ construction (after allowing for some trivial re-identification of left and right etc.)
Now, in the context of quantum operations the whole point is that one restricts to those maps in (by the above) $Int(\mathcal{C})$ which are of a special form such as to be “completely positive maps”. Because that means they really have an interpretation of physical processes that take mixed states represented by density matrices to mixed states.
So it seems that in order to genuinely connect the GoI to quantum physics, all that would be necessary is to see what the syntactic logic is that expresses these positivity conditions. This should (and here I go again) be straightforward (if maybe tedious), since we already have that the linear logic here is equivalently just a syntactic representation of these categories.
I have now added a paragraph with some of these observations to
This is labeled “under construction”, since I still feel that either I am missing something or else some expert should come around and say “of course! we have always thought of it this way, and its explained here:…”.
I see that Bob Coecke at the very end of his Kindergarte QM mentions “Geometry of Interaction” very briefly in passing. But I can’t see from this what the intended message is. I’ll dig around a bit more now…
Hm, so essentially this statement is, I suppose, in some form in this article here:
I see on Bob’s home page a talk titled “Physical traces: Doing GoI in the Lab”, but I cannot find further details.
In any case, I conclude that Bob sort of has this relation in mind, though I am still looking for a place where he might have said it more explicitly.
1 to 8 of 8