×

Generalizing substitution. (English) Zbl 1042.18003

From the abstract: It is well known that, given an endofunctor \(H\) on a category \(\mathcal{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 extention operation (the free monad induced by the functor \(H\)). L. S. Moss [Lect. Notes Comput Sci. 283, 158–181 (1987; Zbl 0639.68026)] and P. Aczel, J. Adámek, M. Milius and J. Velebil [Theor. Comput Sci. 300, 1–45 (2003; Zbl 1028.68077)] 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 \(\mathcal{C}\) such that the functors \(T'(-, X)\) uniformly carry a monad structure.
This generalization has been well received (see forthcoming papers by Adámek, Milius and others).

MSC:

18B20 Categories of machines, automata
18C50 Categorical semantics of formal languages
08B20 Free algebras
68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI Numdam Numdam EuDML

References:

[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 . Zbl 1065.68512 · Zbl 1065.68512
[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 . Zbl 1028.68077 · Zbl 1028.68077 · doi:10.1016/S0304-3975(02)00728-4
[3] J. Adámek , S. Milius and J. Velebil , Free iterative theories: a coalgebraic view . Math. Struct. Comput. Sci. 13 ( 2003 ) 259 - 320 . Zbl 1030.18004 · Zbl 1030.18004 · doi:10.1017/S0960129502003924
[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 ).
[5] M. Barr , Coequalizers and free triples . Math. Z. 116 ( 1970 ) 307 - 322 . Article | Zbl 0194.01701 · Zbl 0194.01701 · doi:10.1007/BF01111838
[6] F. Bartels , Generalized coinduction . Math. Struct. Comput. Sci. 13 ( 2003 ) 321 - 348 . Zbl 1025.18002 · Zbl 1025.18002 · doi:10.1017/S0960129502003900
[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 ). · Zbl 1270.68188
[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 . Zbl 0327.02040 · Zbl 0327.02040
[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 . Zbl 0389.68007 · Zbl 0389.68007 · doi:10.1016/0022-0000(78)90024-7
[10] N. Ghani , C. Lüth , F. de Marchi and J. Power , Dualising initial algebras . Math. Struct. Comput. Sci. 13 ( 2003 ) 349 - 370 . Zbl 1049.18005 · Zbl 1049.18005 · doi:10.1017/S0960129502003912
[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 ). · Zbl 1270.18011
[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 . Zbl 0978.68101 · Zbl 0978.68101
[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 ). Zbl 0918.68029 · Zbl 0918.68029
[14] E.G. Manes , Algebraic theories , Graduate Texts in Mathematics 26. Springer-Verlag, New York ( 1976 ). MR 419557 | Zbl 0353.18007 · Zbl 0353.18007
[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 ). Zbl 1071.68063 · Zbl 1071.68063 · doi:10.1016/j.tcs.2004.07.025
[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 ). · Zbl 1270.18012
[17] L.S. Moss , Parametric corecursion . Theor. Comput. Sci. 260 ( 2001 ) 139 - 163 . Zbl 0973.68134 · Zbl 0973.68134 · doi:10.1016/S0304-3975(00)00126-2
[18] R. Paterson , Notes on monads for functional programming, unpublished draft (1995).
[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] T. Uustalu and V. Vene , Primitive (co)recursion and course-of-value (co)iteration, categorically . Informatica 10 ( 1999 ) 5 - 26 . Zbl 0935.68011 · Zbl 0935.68011
[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] T. Uustalu , V. Vene and A. Pardo , Recursion schemes from comonads . Nordic J. Comput. 8 ( 2001 ) 366 - 390 . Zbl 0994.68018 · Zbl 0994.68018
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.