TY - JOUR

T1 - Generalizing substitution

AU - Uustalu, Tarmo

PY - 2003

Y1 - 2003

N2 - It is well known that, given an endofunctor H on a. category C, 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 and Aczel, Adámek, Milius and Velebil 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′(A, -)-algebras resp. the inverses of the final T′(A, -)-coalgebras for any endobifunctor T′ on any category C such that the functors T′(-, X) uniformly carry a monad structure.

AB - It is well known that, given an endofunctor H on a. category C, 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 and Aczel, Adámek, Milius and Velebil 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′(A, -)-algebras resp. the inverses of the final T′(A, -)-coalgebras for any endobifunctor T′ on any category C such that the functors T′(-, X) uniformly carry a monad structure.

KW - Algebras of terms

KW - Finitely or possibly infinitely branching trees

KW - Hyperfunctions

KW - Iteration of guarded substitution rules

KW - Monads

KW - Non-wellfounded terms

KW - Substitution

UR - http://www.scopus.com/inward/record.url?scp=0942267770&partnerID=8YFLogxK

U2 - 10.1051/ita:2003022

DO - 10.1051/ita:2003022

M3 - Article

AN - SCOPUS:0942267770

VL - 37

SP - 315

EP - 336

JO - RAIRO - Theoretical Informatics and Applications

JF - RAIRO - Theoretical Informatics and Applications

SN - 0988-3754

IS - 4

ER -