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.
Todd Schmid (he/they) (Apr 12 2020 at 12:23):I'm looking out for an intro to programming language semantics appropriate for a first/second year grad student, specifically something that covers algebraic or categorical semantics. I've heard that automata have a semantics-type role in programming language theory; is this true? If so, I'd like to know more!
Ralph Sarkis (Apr 12 2020 at 13:07):If you'd like a reading partner, I might join in. I am doing a research internship in semantics (probabilistic and non-deterministic systems with Matteo Mio) this summer, so I will have a lot of paper to read already, but I could spend some time discussing other readings with you :) How much semantics have you done already? I have course notes on parts of Principles of Model Checking by Baier, C. and Katoen, J.-P which I found to be a good intro to semantics while mainly on the logical side (no category or algebra), it uses automata a bit.
Todd Schmid (he/they) (Apr 12 2020 at 14:00):Ralph Sarkis I am quite new to formal computer science, but I do have a background in model theory and topos theory (I'm not sure how much this helps, yet). I have also spent the last few months with automata, proof theory, and modal logic, so I feel pretty ready to give it a go. I will check out your reference (thank you!). I sincerely would love a reading partner.
James Wood (Apr 12 2020 at 14:18):Programming languages is a very broad area, and likewise there are all sorts of different semanticses. What kind of programming languages/models are you interested in? In any case, I guess simply typed lambda calculus and its semantics in Cartesian closed categories (or just Set) is a good place to start. Not sure of any particular reference, though.
Todd Schmid (he/they) (Apr 13 2020 at 09:49):@James Wood I've actually spent quite a bit of time with Lambek and Scott's book, so I think the λ-calculus story (and the CHL-correspondance) isn't quite what I'm after. I had something more coalgebraic in mind, and more geared to "abstract machines", if that makes any sense. To be honest, I'm not sure exactly what I'm looking for (which is why I started this, I guess)! That being said, I imagine I'll have to learn about the μ-calculus at some point, so I also welcome suggestions in that direction.
Ralph Sarkis (Apr 13 2020 at 11:27):Another recommendation: While not strictly semantics, this paper has been one of my favorites for a while. It uses the coalgberaic representation of automata to prove correctness of the Brzozowski's algorithm to minimize an automata. It is very basic, but they describe many different machines and the references probably have more stuff to look at in this direction.
(You might have read it already as Alexandra Silva is a co-author; at least three other authors are in this community :)
Todd Schmid (he/they) (Apr 13 2020 at 12:27):@Ralph Sarkis Oh, yeah! Embarrassingly, I haven't read this paper yet, though I should probably make that a priority sooner than later. This is certainly the direction I'm going for.
Gershom (Apr 13 2020 at 15:22):The classic more rigorous texts for programming language semantics for early graduate students are Mitchell's "Foundations for Programming Languages" and Reynolds' "Theories of Programming Languages". There's also "Advanced Topics in Types and Programming Languages." None of these hit the categorical stuff at the level you'd want, I think, but they do give an overview of the field. Rutten (one of the authors of the paper above) is one of the go-to references on coalgebraic stuff.
For something that scratches your itch directly, you may want to look at Joyal, Nielson, Winskel's "Bisimulation from Open Maps" and then work backwards and forward from there: https://www.brics.dk/RS/94/7/BRICS-RS-94-7.pdf
Todd Schmid (he/they) (Apr 13 2020 at 15:54):@Gershom Thank you for all of the references! It's nice to see Joyal's name again, haha. I will have to take a look at the open maps paper.
John Baez (Apr 13 2020 at 16:54):Brzozowski's algorithm to minimize an automaton
What does it mean to "minimize" an automaton. I can guess... and I could look it up... but I'll ask anyway.
Dan Doel (Apr 13 2020 at 16:57):Find an automaton that does the same work, but with the fewest possible states.
Dan Doel (Apr 13 2020 at 16:58):'Does the same work' is rather coalgebraic.
Maybe that's still to vague, though. Decides the same language is the work. :slight_smile:
Gershom (Apr 13 2020 at 22:18):A bit handwavy here, but it seems pretty clear to me that Deterministic Finite Automata are in some sense a reflective subcategory of Nondeterministic Finite Automata, and there's a a lovely contraction operator called "determinization" that preserves "meaning". What makes Brzozowski’s algorithm so beautiful is that there's an involution operator "reverse" on NFA that doesn't stay within the DFA subcategory, and the chain reverse -> determinize -> reverse -> determinize somehow pulls you into an even tighter reflective subcategory, which is "minimal DFA". I've had the rutten, silva et. al paper on my "to read" list for a little time now, because I want to see if how they analyze it can be fitted into my handwavy intuition above. (Additionally it seems to me that "determinize" should really end up being some variant of the yoneda lemma, if one examines what the algorithm does, and I'd like to understand just that portion alone more categorically).
John Baez (Apr 13 2020 at 22:24):All this sounds pretty interesting. Trying to find the automaton with the fewest states that decides a given language sounds like a horrendously tricky problem that's not likely to have a good answer or support an interesting theory - sort of like finding the minimal presentation of a group. But it sounds like there is something good to say about this!
sarahzrf (Apr 13 2020 at 23:18):man, i dont know that much about automata :/
sarahzrf (Apr 13 2020 at 23:18):i should fix that someday...
Cody Roux (Apr 15 2020 at 20:45):This is definitely true in general, except that for some reason, there are algorithms for this for regular languages! Given that, and how incredibly useful such an algorithm is, it's worth trying to see if there is some general pattern. For Finite Automata, minimizing involves computing the largest possible equivalence class of a set of states, which feels nicely algebraic in nature.
Gershom (Apr 15 2020 at 22:39):I mean for finite automata, minimizing can be done by the Brzozowski algorithm I sketched above (the handwavey bit being I didn't specify the categories which make the above "reflective" characterization of it work, but the algorithm itself is a classic solid result), which is even more ridiculously algebraic, and which relates to the manes stuff about observability and reachability as duals as in the paper above-above.
Todd Schmid (he/they) (Apr 16 2020 at 11:17):I actually just finished reading the Duality in Brzozowski's Minimization Algorithm paper, and it seems pretty general! It works for finite automata of many different flavours. I think the algorithm is a little different than @Gershom stated it, though: For deterministic finite automata, accepting a specific language , there's a dual adjunction which swaps reachability maps for observability maps, and injective maps for surjective maps (the functor at play is the contravariant powerset functor). So, the algorithm is
After step 1, we have a DFA on our hands that accepts the reversed language. Since the dual adjunction swaps reachability and observability, step 3 produces an observable automaton accepting , so taking the reachable component (step 4) produces a minimal automaton for . For other flavours of automaton, step 1 needs to be replaced by a determinization process that reverses the language. Is this what you were talking about @Gershom ?
Gershom (Apr 16 2020 at 15:55):I was simply describing the classic algorithm, not the paper's treatment of it. The classic algorithm as far as I know is the four steps I describe. I have no doubt the paper generalizes it in the way you describe. As the paper states in the abstract, it gives not only a new proof of correctness, but a new presentation in terms of reachability and observability.
Gershom (Apr 21 2020 at 19:57):Here is another interesting categorical approach to minimization I just came across: https://arxiv.org/abs/1712.07121v3
Gershom (Apr 21 2020 at 22:13):In fact, the factorization given in that paper gives reflective subcategories of the form I was after!
Todd Schmid (he/they) (Apr 28 2020 at 10:45):Oh, nice! Sorry I didn't see this earlier. I will have to check this out.