Generalizing substitution

Tarmo Uustalu

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2003)

  • Volume: 37, Issue: 4, page 315-336
  • ISSN: 0988-3754

Abstract

top
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 ' ( A , - ) -algebras resp. the inverses of the final T ' ( A , - ) -coalgebras for any endobifunctor T ' on any category such that the functors T ' ( - , X ) uniformly carry a monad structure.

How to cite

top

Uustalu, Tarmo. "Generalizing substitution." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 37.4 (2003): 315-336. <http://eudml.org/doc/244874>.

@article{Uustalu2003,
abstract = {It is well known that, given an endofunctor $H$ on a category $\mathbb \{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 [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^\{\prime \}(A,\{-\})$-algebras resp. the inverses of the final $T^\{\prime \}(A,\{-\})$-coalgebras for any endobifunctor $T^\{\prime \}$ on any category $\mathbb \{C\}$ such that the functors $T^\{\prime \}(\{-\}, X)$ uniformly carry a monad structure.},
author = {Uustalu, Tarmo},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {algebras of terms; non-wellfounded terms; substitution; iteration of guarded substitution rules; monads; hyperfunctions; finitely or possibly infinitely branching trees; terms; guarded substitution},
language = {eng},
number = {4},
pages = {315-336},
publisher = {EDP-Sciences},
title = {Generalizing substitution},
url = {http://eudml.org/doc/244874},
volume = {37},
year = {2003},
}

TY - JOUR
AU - Uustalu, Tarmo
TI - Generalizing substitution
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2003
PB - EDP-Sciences
VL - 37
IS - 4
SP - 315
EP - 336
AB - It is well known that, given an endofunctor $H$ on a category $\mathbb {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 [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^{\prime }(A,{-})$-algebras resp. the inverses of the final $T^{\prime }(A,{-})$-coalgebras for any endobifunctor $T^{\prime }$ on any category $\mathbb {C}$ such that the functors $T^{\prime }({-}, X)$ uniformly carry a monad structure.
LA - eng
KW - algebras of terms; non-wellfounded terms; substitution; iteration of guarded substitution rules; monads; hyperfunctions; finitely or possibly infinitely branching trees; terms; guarded substitution
UR - http://eudml.org/doc/244874
ER -

References

top
  1. [1] P. Aczel, Algebras and coalgebras, in Revised Lectures from Int. Summer School and Wksh. on Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, ACMMPC 2000 (Oxford, April 2000), edited by R. Backhouse, R. Crole and J. Gibbons. Springer-Verlag, Lecture Notes in Comput. Sci. 2297 (2002) 79–88. Zbl1065.68512
  2. [2] P. Aczel, J. Adámek, S. Milius and J. Velebil, Infinite trees and completely iterative theories: a coalgebraic view. Theor. Comput. Sci. 300 (2003) 1–45. Zbl1028.68077
  3. [3] J. Adámek, S. Milius and J. Velebil, Free iterative theories: a coalgebraic view. Math. Struct. Comput. Sci. 13 (2003) 259–320. Zbl1030.18004
  4. [4] J. Adámek, S. Milius and J. Velebil, On rational monads and free iterative theories, in Proc. of 9th Int. Conf. on Category Theory and Computer Science, CTCS’02 (Ottawa, Aug. 2002), edited by R. Blute and P. Selinger. Elsevier, Electron. Notes Theor. Comput. Sci. 69 (2003). Zbl1270.18010
  5. [5] M. Barr, Coequalizers and free triples. Math. Z. 116 (1970) 307–322. Zbl0194.01701
  6. [6] F. Bartels, Generalized coinduction. Math. Struct. Comput. Sci. 13 (2003) 321–348. Zbl1025.18002
  7. [7] D. Cancila, F. Honsell and M. Lenisa, Generalized coiteration schemata, in Proc. of 6th Wksh. on Coalgebraic Methods in Computer Science, CMCS’03 (Warsaw, Apr. 2003), edited by H.P. Gumm. Elsevier, Electron. Notes Theor. Comput. Sci. 82 (2003). Zbl1270.68188
  8. [8] C.C. Elgot, Monadic computation and iterative algebraic theories, in Proc. of Logic Colloquium ’73 (Bristol, July 1973), edited by H.E. Rose and J.C. Shepherdson. North-Holland, Stud. Logic Found Math. 80 (1975) 175–230. Zbl0327.02040
  9. [9] C.C. Elgot, S.L. Bloom and R. Tindell, On the algebraic structure of rooted trees. J. Comput. Syst. Sci. 16 (1978) 362–399. Zbl0389.68007
  10. [10] N. Ghani, C. Lüth, F. de Marchi and J. Power, Dualising initial algebras. Math. Struct. Comput. Sci. 13 (2003) 349–370. Zbl1049.18005
  11. [11] N. Ghani, C. Lüth and F. de Marchi, Coalgebraic monads, in Proc. of 5th Wksh. on Coalgebraic Methods in Computer Science, CMCS’02 (Grenoble, Apr. 2001), edited by L.S. Moss. Elsevier, Electron. Notes Theor. Comput. Sci. 65 (2002). Zbl1270.18011
  12. [12] S. Krstić, J. Launchbury and D. Pavlović, Categories of processes enriched in final coalgebras, in Proc. of 4th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS’01 (Genova, Apr. 2001), edited by F. Honsell and M. Miculan. Springer-Verlag, Lecture Notes in Comput. Sci. 2030 (2001) 303–317. Zbl0978.68101
  13. [13] M. Lenisa, From set-theoretic coinduction to coalgebraic coinduction: some results, some problems, in Proc. of 2nd Wksh. on Coalgebraic Methods in Computer Science, CMCS’99 (Amsterdam, March 1999), edited by B. Jacobs and J. Rutten. Elsevier, Electron. Notes Theor. Comput. Sci. 19 (1999). Zbl0918.68029
  14. [14] E.G. Manes, Algebraic theories, Graduate Texts in Mathematics 26. Springer-Verlag, New York (1976). Zbl0353.18007MR419557
  15. [15] R. Matthes and T. Uustalu, Substitution in non-wellfounded syntax with variable binding, in Proc. of 6th Wksh. on Coalgebraic Methods in Computer Science, CMCS’03 (Warsaw, Apr. 2003), edited by H.P. Gumm. Elsevier, Electron. Notes Theor. Comput. Sci. 82 (2003). Zbl1071.68063
  16. [16] S. Milius, On iteratable endofunctors, in Proc. of 9th Int. Conf. on Category Theory and Computer Science, CTCS’02 (Ottawa, Aug. 2002), edited by R. Blute and P. Selinger. Elsevier, Electron. Notes Theor. Comput. Science 69 (2003). Zbl1270.18012
  17. [17] L.S. Moss, Parametric corecursion. Theor. Comput. Sci. 260 (2001) 139–163. Zbl0973.68134
  18. [18] R. Paterson, Notes on monads for functional programming, unpublished draft (1995). 
  19. [19] T. Uustalu, (Co)monads from inductive and coinductive types, in Proc. of 2001 APPIA-GULP-PRODE Joint Conf. on Declarative Programming, AGP’01 (Évora, Sept. 2001), edited by L.M. Pereira and P. Quaresma. Dep. de Informática, Univ. do Évora (2001) 47–61. 
  20. [20] T. Uustalu and V. Vene, Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica 10 (1999) 5–26. Zbl0935.68011
  21. [21] T. Uustalu and V. Vene, The dual of substitution is redecoration, in Trends in Functional Programming 3, edited by K. Hammond and S. Curtis. Intellect, Bristol & Portland, OR (2002) 99–110. 
  22. [22] T. Uustalu, V. Vene and A. Pardo, Recursion schemes from comonads. Nordic J. Comput. 8 (2001) 366–390. Zbl0994.68018

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.