Not signed in (Sign In)

Start a new discussion

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeJan 18th 2014
    • (edited Jan 18th 2014)

    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 ABA\multimap B as a morphism between objects AA and BB in a monoidal category as in categorical semantics, the Geometry of Interaction interprets it as an endomorphism on the object ABA\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).

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJan 18th 2014

    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.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeJan 18th 2014
    • (edited Jan 18th 2014)

    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 )(A^+, A^-) in 𝒞\mathcal{C} and morphisms (A +,A )(B +,B )(A^+, A^-) \to (B^+, B^-) are maps in 𝒞\mathcal{C} of the form

    A +B A B +. 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 ) *A +B +(B ) * (A^-)^\ast \otimes A^+ \longrightarrow B^+ \otimes (B^-)^\ast

    and composition with the symmetry makes that equivalently be of the form

    (A ) *A +(B ) *B +. (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 A +A^- \simeq A^+ and B B +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 +B A B +. 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.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 19th 2014

    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.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2014
    • (edited Jan 20th 2014)

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

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2014

    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…

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2014

    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)
    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2014
    • (edited Jan 20th 2014)

    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.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)