Substitution by structural recursion

Question

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?

Answer 1

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.