Jason (jcreed) wrote,

Two further thoughts:

(1) After remembering what the hell the exponential is in presheaf categories, I am pretty confident I have described a monoidal closed structure on Grph that is different from the cartesian closed structure.

(2) But nonetheless there is a cartesian closed structure there: the vertices of A ⇒ B are the graph homomorphisms from A to B, and the edges of A ⇒ B are the graph homomorphisms from 2 & A to B, where 2 is the one-arrow graph • → •. And this means A & — is the left adjoint of something, (namely A ⇒ —) and left adjoints preserve colimits, and in particular we must have distributivity
A & (B + C) ⊢ (A & B) + (A & C)
which means that you're no longer in linear logic kansas, but rather in some sort of bunched-logic Oz. But then again, I think I dimly knew this about ICFP paper semantics, too. If you just unwind the definitions of & and + you get distributivity staring you in the face.

Let me just toss in my intended definition of + here, anyhow, just to make that claim falsifiable:
(A, C, f) + (B, D, g) = (A + B, λv.case v of inl x ⇒ C(x) | inr y ⇒ D(y),
                         λv.λm.case v of inl x ⇒ f x m | inr y ⇒ g y m)
Tags: graphs, linear logic, logic, math
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded