Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

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?

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

1 Answer 1

up vote 1 down vote accepted

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.

share|improve this answer
    
Nice reference, thanks! –  pedagand Feb 22 '13 at 1:28

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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