Following the article's notation, I write $\mathcal{F}$ for the category of presheaves on a (suitable) category $\mathbb{F}$, $TV$ for the presheaf of terms, $\delta$ for the context extension, and $\bullet$ for the product of the $\mathcal{F}$-monoid.

In Abstract Syntax and Variable Binding [Fiore, Plotkin, Turi], the authors set out to define substitution by structural recursion (Section 3). I was expecting to see substitution expressed as an initial algebra of some sort.

Instead, from what I understand, the authors:

  1. Construct the substitution $\sigma : \delta(TV) \times TV \to TV$ by some universal construction ("Definition of substitution by structural recursion")
  2. Show that it forms a substitution algebra (Theorem 3.2)
  3. Show that the categories of substitution algebras and clones are equivalent (Theorem 3.3)
  4. Show that the categories of clones and monoids in $\mathcal{F}$ are equivalent (Proposition 3.4)
  5. Show that subtitution is the multiplication of such a monoid (Proposition 3.5)
  6. Conclude that $\sigma$, the substitution, is defined by structural recursion (Corollary 3.6).

I'm failing to appreciate their motive in moving from substitution algebras to clones to monoids. Is that a natural thing to do for a mathematician?

In particular, why not stay focused on substitution algebras and, I guess, present substitution as the initial one?

Conversely, they claim that Corollary 3.6 gives a definition of substitution by structural recursion: how is that? It is just said that "$\sigma$ is the unique homomorphic extension of $V \bullet TV \cong TV$": how did they derive their example (substitution for the lambda calculus, very end of Section 3) from this statement?

  • $\begingroup$ You could write to the authors, they are still alive. Marcelo and Daniele would probably find the time to answer more easily than Gordon. $\endgroup$ Feb 17 '13 at 23:38
  • $\begingroup$ @andrej I did send this page to two of Gordon's (academic) heirs ;-) But they are pretty busy. $\endgroup$
    – pedagand
    Feb 22 '13 at 1:36

A more tutorial-paced presentation of the same/related material is available in: Roy L. Crole: Basic Category Theory for Models of Syntax. Generic Programming 2003: 133-177. This should help.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.