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: deprecated: our papers

Topic: A unified treatment of structural definitions on syntax

Tom Hirschowitz (Apr 08 2022 at 08:12):

@Ambroise and I just released a preprint we've been (intermittently) working on for the last two years or so.
It's called A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on, in humble reference to Kelly's mythical paper.

Rather than copy-pasting the abstract, let me explain the basic idea from a different point of view. As previously discussed here, one of the main categorical approaches to generating syntaxes from basic data is Fiore, Plotkin, and Turi (FPT)'s $\Sigma$-monoids:

• a signature is a pointed strong endofunctor $\Sigma$ on a nice monoidal category;
• each such functor has a category of models, called $\Sigma$-monoids, which are $\Sigma$-algebras equipped with compatible monoid structure;
• monoid structure models capture-avoiding substitution (it is substitution in examples);
• the main theorem is that the initial $(I+\Sigma)$-algebra is in fact (uniquely) an initial $\Sigma$-monoid, which means that it freely comes with substitution.

Our work widely generalises the approach, and at the same time attempts to clarify it.

Let me explain the latter point first.
One aspect that has always bugged me about FPT is the status of pointed strengths. Very roughly, they amount to assuming that certain objects already have part of the $\Sigma$-algebra structure in order for substitution to make sense, which seems rather arbitrary.

In our work, we instead work with all objects, and consider the free $(I+\Sigma)$-algebra structure on them. This makes the whole framework more straightforward, I think, albeit perhaps a bit more low-level.

Finally, in what sense do we generalise FPT? Well, FPT merely deals with capture-avoiding substitution, which is in fact only one of the many auxiliary operations that operational semanticists define on syntax every day: we start investigating other auxiliary operations. We do not yet cover all of them, but we catch a fairly large class.

We'd be very interested in hearing constructive comments! (Maybe I'll ping some of the local experts: @Nathanael Arkor, @Jon Sterling, @Marcelo Fiore, @Sam Staton, @Damiano Mazza, are you around?)

Jon Sterling (Apr 08 2022 at 15:10):

Thanks for sharing, I'm excited to take some time to read your paper!

Nathanael Arkor (Apr 12 2022 at 11:07):

Thanks for pinging me – I'm looking forward to taking a look when I have some time!