Generalizing substitution

Uustalu, Tarmo 

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 37 (2003) no. 4, pp. 315-336

Résumé

It is well known that, given an endofunctor $H$ on a category $ℂ$, the initial $(A+H-)$-algebras (if existing), i.e., the algebras of (wellfounded) $H$-terms over different variable supplies $A$, give rise to a monad with substitution as the extension operation (the free monad induced by the functor $H$). Moss [17] and Aczel, Adámek, Milius and Velebil [2] have shown that a similar monad, which even enjoys the additional special property of having iterations for all guarded substitution rules (complete iterativeness), arises from the inverses of the final $(A+H-)$-coalgebras (if existing), i.e., the algebras of non-wellfounded $H$-terms. We show that, upon an appropriate generalization of the notion of substitution, the same can more generally be said about the initial $T^{\text{'}}(A,-)$-algebras resp. the inverses of the final $T^{\text{'}}(A,-)$-coalgebras for any endobifunctor $T^{\text{'}}$ on any category $ℂ$ such that the functors $T^{\text{'}}(-,X)$ uniformly carry a monad structure.

Détail

DOI : 10.1051/ita:2003022

Classification : 08B20, 18C15, 18C50
Keywords: algebras of terms, non-wellfounded terms, substitution, iteration of guarded substitution rules, monads, hyperfunctions, finitely or possibly infinitely branching trees