×

On second-order iterative monads. (English) Zbl 1243.68206

The object of this work is a categorical generalization of results by B. Courcelle on solutions of recursive program schemes [Theor. Comput. Sci. 25, 95–169 (1983; Zbl 0521.68013)]. The setting of the generalization is to replace algebraic signatures with finitary endofunctors on locally finitely presentable categories, and then study the property of such functors being second-order iterative monads, i.e., admitting unique solutions of all guarded recursive program schemes, the latter referring to a natural categorical abstraction of the classical concept. Specifically, the authors construct, given a finitary endofunctor \(H\) on a locally presentable category, two second-order iterative monads over \(H\), the second order rational monad \(S^H\) and the context-free monad \(C^H\), which arises as the image of \(S^H\) in the free completely iterative monad \(T^H\) over \(H\) [P.Aczel and the authors, Theor. Comput. Sci. 300, No.1–3, 1–45 (2003; Zbl 1028.68077)]. The monad \(S^H\) is then shown to be the initial second-order iterative monad over \(H\); moreover, both \(S^H\) and \(C^H\) are shown to be ideal in the sense of C. C. Elgot [Logic Colloq. ’73, Proc., Bristol 1973, 175–230 (1975; Zbl 0327.02040)]. In the classical case, i.e., when \(H\) is a polynomial endofunctor on \(\mathsf{Set}\), \(S^H\) coincides with Courcelle’s monad of algebraic trees, where a tree is called algebraic if it can be defined by a guarded recursive program scheme. Several open problems are stated, in particular whether \(C^H\) is iterative and closed under second-order substitution, and whether \(S^H=C^H\).

MSC:

68Q55 Semantics in the theory of computing
03D75 Abstract and axiomatic computability and recursion theory
68Q65 Abstract data types; algebraic specification
18C35 Accessible and locally presentable categories
18C15 Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
Full Text: DOI

References:

[1] Aczel, P.; Adámek, J.; Milius, S.; Velebil, J., Infinite trees and completely iterative theories: a coalgebraic view, Theoret. Comput. Sci., 300, 1-45 (2003) · Zbl 1028.68077
[2] P. Aczel, J. Adámek, J. Velebil, A coalgebraic view of infinite trees and iteration, in: Proc. Coalgebraic Methods in Computer Science, CMCS’01, Electron. Notes Theor. Comput. Sci., vol. 44, 2001, pp. 1-26.; P. Aczel, J. Adámek, J. Velebil, A coalgebraic view of infinite trees and iteration, in: Proc. Coalgebraic Methods in Computer Science, CMCS’01, Electron. Notes Theor. Comput. Sci., vol. 44, 2001, pp. 1-26. · Zbl 1260.68235
[3] Adámek, J., Free algebras and automata realizations in the language of categories, Comment. Math. Univ. Carolin., 15, 589-602 (1974) · Zbl 0293.18006
[4] Adámek, J.; Milius, S.; Velebil, J., Iterative algebras at work, Math. Structures Comput. Sci., 16, 6, 1085-1131 (2006) · Zbl 1112.18005
[5] Adámek, J.; Milius, S.; Velebil, J., Semantics of higher-order recursion schemes, Log. Methods Comput. Sci., 7, 1:15, 43 (2011) · Zbl 1218.03013
[6] Adámek, J.; Milius, S.; Velebil, J., Recursive program schemes and context-free monads, Proc. Coalgebraic Methods in Computer Science, CMCS’10. Proc. Coalgebraic Methods in Computer Science, CMCS’10, Electron. Notes Theor. Comput. Sci., 264, 3-23 (2010) · Zbl 1247.68049
[7] Adámek, J.; Milius, S.; Velebil, J., Iterative reflections of monads, Math. Structures Comput. Sci., 20, 3, 419-452 (2010) · Zbl 1239.18005
[8] Adámek, J.; Milius, S.; Velebil, J., Some remarks on finitary and iterative monads, Appl. Categ. Structures, 11, 6, 521-541 (2003) · Zbl 1035.18002
[9] Adámek, J.; Rosický, J., Locally Presentable and Accessible Categories (1994), Cambridge University Press · Zbl 0795.18007
[10] Barr, M., Coequalizers and free triples, Math. Z., 116, 307-322 (1970) · Zbl 0194.01701
[11] Courcelle, B., Fundamental properties of infinite trees, Theoret. Comput. Sci., 25, 95-169 (1983) · Zbl 0521.68013
[12] Elgot, C. C., Monadic computation and iterative algebraic theories, (Rose, H. E.; Sheperdson, J. C., Logic Colloquium ’73 (1975), North-Holland Publishers: North-Holland Publishers Amsterdam) · Zbl 0123.33502
[13] Gallier, J. H., DPBS’a in atomic normal form and applications to equivalence problems, Theoret. Comput. Sci., 14, 155-186 (1981) · Zbl 0474.68065
[14] Ghani, N.; Lüth, C.; De Marchi, F., Solving algebraic equations using coalgebra, Theor. Inform. Appl., 37, 301-314 (2003) · Zbl 1038.18005
[15] Ghani, N.; Lüth, C.; De Marchi, F., Monads of coalgebras: rational terms and term graphs, Math. Structures Comput. Sci., 15, 3, 433-451 (2005) · Zbl 1169.18303
[16] N. Ghani, C. Lüth, F. De Marchi, A.J. Power, Algebras, coalgebras, monads and comonads, in: Proc. Coalgebraic Methods in Computer Science, CMCS’01, Electron. Notes Theor. Comput. Sci., vol. 44, 2001, pp. 128-145.; N. Ghani, C. Lüth, F. De Marchi, A.J. Power, Algebras, coalgebras, monads and comonads, in: Proc. Coalgebraic Methods in Computer Science, CMCS’01, Electron. Notes Theor. Comput. Sci., vol. 44, 2001, pp. 128-145. · Zbl 1260.68238
[17] Ghani, N.; Lüth, C.; De Marchi, F.; Power, A. J., Dualizing initial algebras, Math. Structures Comput. Sci., 13, 2, 349-370 (2003) · Zbl 1049.18005
[18] Ghani, N.; Uustalu, T., Coproducts of ideal monads, Theor. Inform. Appl., 38, 4, 321-342 (2004) · Zbl 1072.18006
[19] Ginali, S., Regular trees and the free iterative theory, J. Comput. System Sci., 18, 228-242 (1979) · Zbl 0495.68042
[20] Guessarian, I., (Algebraic Semantics. Algebraic Semantics, Lecture Notes in Comput. Sci., vol. 99 (1981), Springer) · Zbl 0474.68010
[21] Lack, S., On the monadicity of finitary monads, J. Pure Appl. Algebra, 140, 65-73 (1999) · Zbl 0974.18005
[22] Lambek, J., A fixpoint theorem for complete categories, Math. Z., 103, 151-161 (1968) · Zbl 0149.26105
[23] Milius, S., Completely iterative algebras and completely iterative monads, Inform. and Comput., 196, 1-41 (2005) · Zbl 1062.68075
[24] Milius, S.; Moss, L. S., The category theoretic solution of recursive program schemes, Theoret. Comput. Sci., 366, 3-59 (2006) · Zbl 1154.68041
[25] Moss, L. S., Parametric corecursion, Theoret. Comput. Sci., 260, 1-2, 139-163 (2001) · Zbl 0973.68134
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.