Equational properties of iterative monads. (English) Zbl 1234.68271
Summary: Iterative monads of Calvin Elgot were introduced to treat the semantics of recursive equations purely algebraically. They are Lawvere theories with the property that all ideal systems of recursive equations have unique solutions. We prove that the unique solutions in iterative monads satisfy all the equational properties of iteration monads of Stephen Bloom and Zoltán Ésik, whenever the base category is hyper-extensive and locally finitely presentable. This result is a step towards proving that functorial iteration monads form a monadic category over sets in context. This shows that functoriality is an equational property when considered w.r.t. sets in context.
MSC:
| 68Q65 | Abstract data types; algebraic specification |
| 18C50 | Categorical semantics of formal languages |
References:
| [1] | Aczel, P.; Adámek, J.; Velebil, J., A coalgebraic view of infinite trees and iteration, Electron. Notes Theor. Comput. Sci., 44, 1, 26 (2001) · Zbl 1260.68235 |
| [2] | Aczel, P.; Adámek, J.; Milius, S.; Velebil, J., Infinite trees and completely iterative theories: a coalgebraic view, Theor. Comput. Sci., 300, 1-45 (2003) · Zbl 1028.68077 |
| [3] | Adámek, J.; Börger, R.; Milius, S.; Velebil, J., Iterative algebras: how iterative are they?, Theory Appl. Categ., 19, 61-92 (2008) · Zbl 1137.68042 |
| [4] | Wright, J. B.; Thatcher, J. W.; Wagner, E. G.; Goguen, J. A., Rational algebraic theories and fixed-point solutions, (Proceedings of the 17th IEEE Symposium on Foundations of Computing, Houston, Texas (1976), IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos), 147-158 |
| [5] | Adámek, J.; Milius, S.; Velebil, J., Iterative algebras at work, Math. Struct. Comput. Sci., 16, 6, 1085-1131 (2006) · Zbl 1112.18005 |
| [6] | Adámek, J.; Milius, S.; Velebil, J., What are iteration theories?, (Kučera, L.; Kučera, A., Proceedings of MFCS 2007. Proceedings of MFCS 2007, Lecture Notes in Computer Science, vol. 4708 (2007), Springer), 240-252 · Zbl 1147.18301 |
| [7] | Adámek, J.; Milius, S.; Velebil, J., Iterative reflection of monads, Math. Struct. Comput. Sci., 20, 3, 419-452 (2010) · Zbl 1239.18005 |
| [9] | Adámek, J.; Rosický, J., Locally Presentable and Accessible Categories (1994), Cambridge University Press · Zbl 0795.18007 |
| [10] | Badouel, E., Terms and infinite trees as monads over a signature, TAPSOFT, vol. 1, Lect. Notes Comput. Sci., 351, 89-103 (1989) |
| [11] | Barr, M., Coequalizers and free triples, Math. Z., 116, 307-322 (1970) · Zbl 0194.01701 |
| [12] | Bloom, S. L.; Ésik, Z., Iteration Theories: The Equational Logic of Iterative Processes, EATCS Monograph Series on Theoretical Computer Science (1993), Springer-Verlag · Zbl 0796.68153 |
| [14] | Carboni, A.; Lack, S.; Walters, R. F.C., Introduction to extensive and distributive categories, J. Pure Appl. Algebra, 84, 145-158 (1993) · Zbl 0784.18001 |
| [15] | Elgot, C. C., Monadic computation and iterative algebraic theories, (Rose, H. E.; Shepherdson, J. C., Logic Colloquium ’73 (1975), North Holland Publishers: North Holland Publishers Amsterdam) · Zbl 0123.33502 |
| [16] | Elgot, C. C.; Bloom, S. L.; Tindell, R., On the algebraic structure of rooted trees, J. Comput. Syst. Sci., 16, 361-399 (1978) · Zbl 0389.68007 |
| [17] | Ésik, Z., Axiomatizing iteration categories, Acta Cybenet., 14, 1, 65-82 (1999) · Zbl 0959.68059 |
| [19] | Gabriel, P.; Ulmer, F., Lokal präsentierbare Kategorien, Lecture Notes in Mathematics, vol. 221 (1971), Springer-Verlag: Springer-Verlag Berlin · Zbl 0225.18004 |
| [20] | Ghani, N.; Lüth, C.; DeMarchi, F.; Power, A. J., Algebras, coalgebras, monads and comonads, Electron. Notes Theor. Comput. Sci., 44, 1, 18 (2001) · Zbl 1260.68238 |
| [21] | Ginali, S., Regular trees and the free iterative theory, J. Comput. Syst. Sci., 18, 228-242 (1979) · Zbl 0495.68042 |
| [22] | Kelly, G. M.; Power, A. J., Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads, J. Pure Appl. Algebra, 89, 163-179 (1993) · Zbl 0779.18003 |
| [25] | Mac Lane, S., Categories for the Working Mathematician (1998), Springer-Verlag · Zbl 0906.18001 |
| [26] | Milius, S., Completely iterative algebras and completely iterative monads, Inform. Comput., 196, 1-41 (2005) · Zbl 1062.68075 |
| [27] | Moss, L., Parametric corecursion, Theor. Comput. Sci., 260, 1-2, 139-163 (2001) · Zbl 0973.68134 |
| [28] | Moss, L., Recursion and corecursion have the same equational logic, Theor. Comput. Sci, 294, 233-267 (2003) · Zbl 1029.03018 |
| [29] | Nelson, E., Iterative algebras, Theor. Comput. Sci., 25, 67-94 (1983) · Zbl 0533.03014 |
| [31] | Tiuryn, J., Unique fixed points vs. least fixed points, Theor. Comput. Sci., 12, 229-254 (1980) · Zbl 0439.68026 |
| [32] | Worrell, J., On the final sequence of a finitary set functor, Theor. Comput. Sci., 338, 184-199 (2005) · Zbl 1070.18004 |
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.
