Generalizing Substitution
Tarmo Uustalu (2010)
RAIRO - Theoretical Informatics and Applications
Similarity:
It is well known that, given an endofunctor on a category , the initial -algebras (if existing), , the algebras of (wellfounded) -terms over different variable supplies , give rise to a monad with substitution as the extension operation (the free monad induced by the functor ). Moss [17] and Aczel, Adámek, Milius and Velebil [12] have shown that a similar monad, which even enjoys the additional special property of having iterations for all guarded substitution rules (complete...