Category Theory
Zulip Server
Archive

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.

Stream: theory: type theory & logic

Topic: W-types and CFGs

Andre Knispel (Apr 02 2020 at 11:43):

Let the $\mathbf{CFG}$ be category of context-free grammars, defined as the free SMC where the object generators are what I like to call open CFGs (where we only define rules for a single non-terminal but can use non-terminals corresponding to other open CFGs) and morphisms $G_1 \otimes \cdots \otimes G_k \to G_0$ are parsing rules of the form $N_0 \to t_{01}\cdots t_{0i_0} N_1 t_{11} \cdots N_k t_{k1} \cdots t_{ki_k}$ where the $t$'s are terminal symbols and the $N$'s are non-terminal symbols such that $N_l$ correspond to $G_l$. You could define an open CFG to be just a list of the rules corresponding to morphisms pointing into it.

This category has a subcategory of CFG's that don's parse anything, i.e. the rules contain no terminals. I assume this is a reflective subcategory but I haven't checked the details yet. What is interesting about this though is that this subcategory is embeds into categories associated with programming languages, by mapping a CFG to a W-type with constructors corresponding to the parsing rules of that CFG (exactly how they form arrows in $\mathbf{CFG}$ and by mapping the generating arrows to constructors.

Has been studied somewhere already?

Dan Doel (Apr 02 2020 at 14:23):

Possibly.

Dan Doel (Apr 02 2020 at 14:23):

https://www.cl.cam.ac.uk/~nk480/parsing.pdf

Dan Doel (Apr 02 2020 at 14:26):

That paper is focused on other stuff, but one of the first ideas it introduces is that CFGs can be described using the constructs of regular grammars plus a fixed point operator μ. I think that result is actually not original to that paper (since it's no proof is presented).

Dan Doel (Apr 02 2020 at 14:28):

Anyhow, the fixed point operators seem like they're probably related to the W type you're talking about. Probably not a perfect correspondence, but related. So maybe digging into the associated research would be valuable.

Andre Knispel (Apr 02 2020 at 14:28):

That's interesting, thanks!

Dan Doel (Apr 02 2020 at 14:29):

I think you can probably also lift all fixed point operators to the top level, too, since that can usually be done.

Dan Doel (Apr 02 2020 at 14:49):

I suppose in some ways the lifting observation isn't novel, because that's kind of what CFGs are already. So the fact that μ is the only missing piece added by CFGs is the novel thing.

Bob Atkey (Apr 02 2020 at 14:51):

I did something like a translation from CFGs with data-dependent RHSs to inductive types in my paper on parsing such grammars: https://bentnib.org/semantic-actions.pdf , though it wasn't very exciting, and I didn't consider any kind of morphisms between grammars.

Andre Knispel (Apr 02 2020 at 15:58):

@Bob Atkey good to know that there is some prior work there! I also didn't really consider morphisms much here, I just realized that there was some categorical structure which might be interesting to some people.

Andre Knispel (Apr 02 2020 at 16:00):

I'm using this to power a type theory with metaprogramming which I might talk about more here at some point