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

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded