Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeJan 18th 2014
   • (edited Jan 18th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexDavid 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](#Girard89)) 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](#JoyalStreetVerity96)) and then developed out in ([Haghverdi 00](#Haghverdi00), [Abramsky-Haghverdi-Scott 02](#AbramskyHaghverdiScott02),[Haghverdi-Scott 05](#HaghverdiScott05)).

   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).

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeJan 18th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.7818) 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.

   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.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeJan 18th 2014
   • (edited Jan 18th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexLet 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](http://ncatlab.org/nlab/show/quantum%20operation#Selinger). 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.](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.7818) 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.](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.7818). 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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 19th 2014
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI'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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeJan 19th 2014
   • (edited Jan 20th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexYes, 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.](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.7818) 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 * Bob Coecke, Chris Heunen, _Pictures of complete positivity in arbitrary dimension_ ([arXiv:1110.3055](http://arxiv.org/abs/1110.3055)) 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.](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.7818), 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.

   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

   • Bob Coecke, Chris Heunen, Pictures of complete positivity in arbitrary dimension (arXiv:1110.3055)

   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.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeJan 20th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have now added a paragraph with some of these observations to * [Geometry of Interactions -- Relation to Quantum Operations](http://ncatlab.org/nlab/show/Geometry+of+Interaction#RelationToQuantumOperations) 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](http://arxiv.org/abs/quant-ph/0510032) 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...

   I have now added a paragraph with some of these observations to

   • Geometry of Interactions – Relation to Quantum Operations

   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…

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeJan 20th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexHm, so essentially this statement is, I suppose, in some form in this article here: * Samson Abramsky, Bob Coecke, _Physical Traces: Quantum vs. Classical Information Processing_ ([arXiv:0207057](http://arxiv.org/abs/cs/0207057))

   Hm, so essentially this statement is, I suppose, in some form in this article here:

   • Samson Abramsky, Bob Coecke, Physical Traces: Quantum vs. Classical Information Processing (arXiv:0207057)
8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeJan 20th 2014
   • (edited Jan 20th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI see on [Bob's home page](http://www.vub.ac.be/CLEA/Bob/Coecke.html) 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorPeterHines
   • CommentTimeNov 30th 2021
   • PermaLink
   Author: PeterHines
   Format: TextHi. I've just been pointed to this page, and think it would be relevant to add a reference. It's my PhD thesis from 1997, which gave categorical semantics for the first three GoI papers, in terms of the categorical trace on the category of partial injections, Joyal, Street, & Verity's Int construction, and compact closed categories. (The thesis is here : https://peterhines.info/papers/phd.pdf ) Hopefully it should be o.k. to go ahead & add this?

   Hi. I've just been pointed to this page, and think it would be relevant to add a reference. It's my PhD thesis from 1997, which gave categorical semantics for the first three GoI papers, in terms of the categorical trace on the category of partial injections, Joyal, Street, & Verity's Int construction, and compact closed categories.
   
   (The thesis is here : https://peterhines.info/papers/phd.pdf )
   
   Hopefully it should be o.k. to go ahead & add this?
10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeNov 30th 2021
    • PermaLink
    Author: Urs
    Format: MarkdownItexPlease do!

    Please do!

11. • CommentRowNumber11.
    • CommentAuthornLab edit announcer
    • CommentTimeDec 15th 2021
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAs mentioned previously, I've just added my PhD thesis (Hines 97) to the list of early works on GoI and traces / compact closed categories. Peter Hines <a href="https://ncatlab.org/nlab/revision/diff/Geometry+of+Interaction/16">diff</a>, <a href="https://ncatlab.org/nlab/revision/Geometry+of+Interaction/16">v16</a>, <a href="https://ncatlab.org/nlab/show/Geometry+of+Interaction">current</a>

    As mentioned previously, I’ve just added my PhD thesis (Hines 97) to the list of early works on GoI and traces / compact closed categories.

    Peter Hines

    diff, v16, current