You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Hendrik Boom (May 07 2020 at 22:47):Let's say one has {P}A{Q} and {P}B{Q}. Could there be any significant concept of a homotopy between A and B?
Sam Tenka (May 07 2020 at 22:55):I like this question. Perhaps one gets directed 2 cells from program-rewrite rules?
However, it might be better to work in the more "point-free" formalism of weakest preconditions instead of mentioning specific predicate pairs. Indeed, each program A imposes a relation between possible predicates P and Q. While a morphism determines its source and target, a program does not determine its pre and post conditions. Does this make sense? @Hendrik Boom
Sam Tenka (May 07 2020 at 22:58):Indeed, Dijkstra ("A Discipline Of Programming", 1976) regards the weakest precondition operator (and hence the semantics) of a program as an endofunctor F on the lattice C of predicates (that satisfies some axioms such as preserving meets). (He doesn't use this language). From this viewpoint, one can ask questions about natural transformations between these functors.
Sam Tenka (May 07 2020 at 23:06):Yeah, so in this setting, a natural map between two functors (two programs A, B) is just an assertion that "for any post condition Q: {the weakest precondition that through A guarantees Q} implies {the weakest precondition that through B guarantees Q}", i.e. that "for all P and Q: if {P}A{Q}, then {P}B{Q}". This is a relation between programs that might help us compare two programs that "do the same thing" except one of them doesn't always terminate.
sarahzrf (May 07 2020 at 23:08):there's a nice setup you can get which i was just mentioning in the topic for my talk which is semi relevant to this
sarahzrf (May 07 2020 at 23:09):form a category H where the objects are assertions, and Hom(P, Q) is the set of true hoare triples {P} C {Q}
sarahzrf (May 07 2020 at 23:09):composition is {P} C {Q} ; {Q} D {R} ↦ {P} C; D {R} and identity is {P} skip {P}
Sam Tenka (May 07 2020 at 23:09):Cool! Where can I learn more about this? (was this a talk in the MIT categories seminar?)
sarahzrf (May 07 2020 at 23:10):it's in the #ACT@UCR seminar stream!
Sam Tenka (May 07 2020 at 23:10):Oh darn it. I wish I hadn't missed it!
sarahzrf (May 07 2020 at 23:10):more info here https://johncarlosbaez.wordpress.com/2020/05/05/separation-logic-through-a-new-lens/
Sam Tenka (May 07 2020 at 23:11):@sarahzrf in this formalism, does "homotopy" between two programs mean something (per @Hendrik Boom 's question)?
sarahzrf (May 07 2020 at 23:11):i don't have that, no :) but such a homotopy would naturally fit as a notion of higher morphism in this category
sarahzrf (May 07 2020 at 23:11):anyway, there's a bit more to say: you have a projection from H to the monoid of commands, which forgets the pre & post
sarahzrf (May 07 2020 at 23:12):weakest pre and strongest post are exactly cleavages witnessing that this projection is a fibration and opfibration!
sarahzrf (May 07 2020 at 23:15):if you come at this starting the other way around: weakest pre and strongest post give functors from the monoid of commands to the category of categories, which send the unique object to the proset of assertions, and the endomorphism C to the wp_C or sp_C functor
sarahzrf (May 07 2020 at 23:15):and then H arises as the grothendieck construction of either
Sam Tenka (May 07 2020 at 23:16):What's a proset?
sarahzrf (May 07 2020 at 23:16):preordered set
sarahzrf (May 07 2020 at 23:17):finally, without privileging either variance: you can put it as a lax functor from the monoid of commands to the category of profunctors, which sends C to the profunctor H_C from assertions to assertions such that H_C(P, Q) is a singleton if {P} C {Q} is true and empty otherwise
sarahzrf (May 07 2020 at 23:18):and this is a "displayed category" since it sends the identity to the identity profunctor
Sam Tenka (May 07 2020 at 23:18):Cool! I wonder whether it is ever useful to consider enriching over something other than Bool. This would give enough structure to address @Hendrik Boom 's question in nontrivial ways, I think.
sarahzrf (May 07 2020 at 23:19):anyway, there's one more perspective, which was pointed out by @Mike Shulman in a question at my talk yesterday: in addition to H being a bifibration over the monoid of commands, it's also a promonad over the proset of assertions
sarahzrf (May 07 2020 at 23:21):a promonad on a category C is a monad on C in the bicategory of profunctors Prof, and it's equivalent to another category on the same objects of C equipped with a functor from C
sarahzrf (May 07 2020 at 23:22):so H is a category on the same objects as the proset of assertions, and all of the old morphisms—the entailments—become new morphisms—the hoare triples for skip. but we also have new morphisms
sarahzrf (May 07 2020 at 23:23):as a morphism in Prof, the promonad is the profunctor H from assertions to assertions where H(P, Q) is the set of commands C such that {P} C {D}
Sam Tenka (May 07 2020 at 23:26):(I'm not familiar with a lot of the words here. And that's okay! I'll learn slowly.) So can the story of "adding new morphisms to just the entailments" be understood as emphasizing the rule of consequence ({P}C{Q} implies {P'}C{Q'} when P'<P, Q<Q', which looks lensy?)
sarahzrf (May 07 2020 at 23:27):not sure
sarahzrf (May 07 2020 at 23:27):rule of consequence states that H_C above is a profunctor though
Mike Shulman (May 07 2020 at 23:27):Not sure how I feel about the word "promonad". Especially when combined with "proset", where the "pro" means something entirely different...
sarahzrf (May 07 2020 at 23:28):yeah, it's a little unfortunate :( but some people at least seem to have started using it...
sarahzrf (May 07 2020 at 23:28):grouse at @fosco about it rather than me :upside_down:
sarahzrf (May 07 2020 at 23:29):and like "pro" as a prefix for profunctor-y stuff has some other uses too i mean, like promonoidal or proarrow
Mike Shulman (May 07 2020 at 23:31):I guess my suggestion would be to stop using "proset", especially since it has another totally different meaning. I think just "preorder" is much more common in my experience.
sarahzrf (May 07 2020 at 23:32)::( but people distinguish between "poset" and "partial order"...
sarahzrf (May 07 2020 at 23:32):perhaps dropping "proset" is a better solution though
sarahzrf (May 07 2020 at 23:33):i think part of why i started saying "proset" all the time may have been purely because i needed a name to avoid an identifier clash with "preorder" itself in a coq development since computers are worse at that kind of overloading than humans >.>
Nathanael Arkor (May 07 2020 at 23:34):I think of posets and partial orders as synonyms too.
sarahzrf (May 07 2020 at 23:34):huh, i would say the former is a structure while the latter is a relation
sarahzrf (May 07 2020 at 23:34):i'm a huge pedant though
Mike Shulman (May 07 2020 at 23:35):Certainly a partial order can be a relation, but it's not uncommon to use it to refer to the structure too.
sarahzrf (May 07 2020 at 23:36):fair enough
Mike Shulman (May 07 2020 at 23:36):(Ironically, this is an abuse that makes more sense in material set theory, where the relation itself, as a set, completely determines the carrier.)
sarahzrf (May 07 2020 at 23:36):hah
Mike Shulman (May 07 2020 at 23:37):One can always say "preordered set". Or "thin category"...
Mike Shulman (May 07 2020 at 23:37):... or "-category"... (yes, I remember you having a conversation about that here on zulip before your talk)
Nathanael Arkor (May 07 2020 at 23:37):sarahzrf said:
huh, i would say the former is a structure while the latter is a relation
It's a little difficult to talk about a relation in isolation of the set it's defined on.
Nathanael Arkor (May 07 2020 at 23:39):Similarly to how a monoid is a set with operations, not just the operations themselves.
sarahzrf (May 07 2020 at 23:39):sure! i mean that it would sound odd to me to say something like "3 is an element of the partial order N"
Reid Barton (May 07 2020 at 23:39):In practice I think it's pretty common to say "poset" for "set equipped with a preorder" (I certainly do this)--assuming you only want to consider your preorders = (0,1)-categories up to equivalence this shouldn't do much harm.
sarahzrf (May 07 2020 at 23:39):to me, ≤ is the partial order, while N is a poset
sarahzrf (May 07 2020 at 23:39):but. this has become a huge tangent on a not-super-important (afaict) point
sarahzrf (May 07 2020 at 23:40):plus i need to eat dinner... bbl
Reid Barton (May 07 2020 at 23:40):Or common among category theorists, at any rate.
Mike Shulman (May 07 2020 at 23:41):@Reid Barton Yes, I agree this is reasonably common among category theorists. But there are certainly other people that it rubs the wrong way...
Morgan Rogers (he/him) (May 08 2020 at 09:41):Sam Tenka said:
(I'm not familiar with a lot of the words here. And that's okay! I'll learn slowly.)
As someone for whom the notation in the question at the top of the thread was meaningless, I strongly relate.
Morgan Rogers (he/him) (May 08 2020 at 09:56):Sam Tenka said:
Yeah, so in this setting, a natural map between two functors (two programs A, B) is just an assertion that "for any post condition Q: {the weakest precondition that through A guarantees Q} implies {the weakest precondition that through B guarantees Q}", i.e. that "for all P and Q: if {P}A{Q}, then {P}B{Q}". This is a relation between programs that might help us compare two programs that "do the same thing" except one of them doesn't always terminate.
The cleavages that @sarahzrf mentioned means that we could just as well talk about the implication on the other side, which is to say "for any pre-condition P: {the strongest post-condition that through A is guaranteed by P} implies {the strongest post-condition that through B is guaranteed by P}". To me this feel a lot like lifting the implications between conditions by applying quantifiers-as-adjunctions, and I suspect that intuition can be made formal. However, unless the structure of the relations between conditions can be enriched, there's not much hope of getting richer structure on these transformations.
Another option would be to explore substitution rules for the commands, which abstractly amounts to replacing the composition of commands with the monoidal product in a monoidal category. The morphisms in this category give candidate 2-cells in the category H that sarahzrf described.
John Baez (May 08 2020 at 17:49):Sam Tenka said:
Oh darn it. I wish I hadn't missed it!
It's been recorded:
https://www.youtube.com/watch?v=Aie82xGks-k&feature=emb_logo
and slides are here:
http://math.ucr.edu/home/baez/mathematical/ACTUCR/Rovner-Frydman_Separation_Logic.pdf
Almost as good as being there. :upside_down:
