A new foundation for finitary corecursion and iterative algebras. (English) Zbl 1435.68208
Summary: This paper contributes to a generic theory of behaviour of “finite-state” systems. Systems are coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to the locally finite fixpoint (LFF), a new fixpoint of the endofunctor. The LFF exists provided that the endofunctor is finitary and preserves monomorphisms, is a subcoalgebra of the final coalgebra, i.e. it is fully abstract w.r.t. behavioural equivalence, and it is characterized by two universal properties: as the final locally finitely generated coalgebra, and as the initial fg-iterative algebra. Instances of the LFF are: regular languages, rational streams, rational formal power-series, regular trees etc. Moreover, we obtain e.g. (realtime deterministic resp. non-deterministic) context-free languages, constructively \(S\)-algebraic formal power-series (in general, the behaviour of finite coalgebras under the coalgebraic language semantics arising from the generalized powerset construction by A. Silva et al. [Log. Methods Comput. Sci. 9, No. 1, Paper No. 9, 23 p. (2013; Zbl 1262.18002)]), and the monad of Courcelle’s algebraic trees.
Citations:
Zbl 1262.18002References:
| [1] | 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 |
| [2] | Adámek, J., Free algebras and automata realizations in the language of categories, Comment. Math. Univ. Carol., 015, 4, 589-602 (1974) · Zbl 0293.18006 |
| [3] | Adámek, J.; Herrlich, H.; Strecker, G. E., Abstract and Concrete Categories: the Joy of Cats (2009), Dover Publications · Zbl 0695.18001 |
| [4] | Adámek, Jiří; Milius, Stefan; Moss, Lawrence S., Fixed points of functors, J. Log. Algebr. Methods Program., 95, 41-81 (2018) |
| [5] | Adámek, J.; Milius, S.; Sousa, L.; Wißmann, T., Finitely Presentable Algebras For Finitary Monads (2019), submitted, available at · Zbl 1468.18006 |
| [6] | Adámek, J.; Milius, S.; Sousa, L.; Wißmann, T., On Finitary Functors (2019), submitted, available at · Zbl 1470.18006 |
| [7] | Adámek, J.; Milius, S.; Velebil, J., Iterative algebras at work, Math. Struct. Comput. Sci., 16, 6, 1085-1131 (2006) · Zbl 1112.18005 |
| [8] | Adámek, J.; Milius, S.; Velebil, J., Equational properties of iterative monads, Inf. Comput., 208, 1306-1348 (2010) · Zbl 1234.68271 |
| [9] | Adámek, J.; Milius, S.; Velebil, J., Elgot theories: a new perspective of the equational properties of iteration, Math. Struct. Comput. Sci., 21, 2, 417-480 (2011) · Zbl 1222.18002 |
| [10] | Adámek, J.; Milius, S.; Velebil, J., On second-order iterative monads, Theor. Comput. Sci., 412, 38, 4969-4988 (2011) · Zbl 1243.68206 |
| [11] | Adámek, J.; Milius, S.; Velebil, J., Semantics of higher-order recursion schemes, Log. Methods Comput. Sci., 7, 1 (2011) · Zbl 1218.03013 |
| [12] | Adámek, J.; Milius, S.; Velebil, J., Semantics of higher-order recursion schemes, Log. Methods Comput. Sci., 1, 15 (2011), 43 pp · Zbl 1218.03013 |
| [13] | Adámek, J.; Rosický, J., Locally Presentable and Accessible Categories (1994), Cambridge University Press · Zbl 0795.18007 |
| [14] | Awodey, S., Category Theory, Oxford Logic Guides (2010), OUP Oxford · Zbl 1194.18001 |
| [15] | Barr, M., Coequalizers and free triples, Math. Z., 116, 307-322 (1970) · Zbl 0194.01701 |
| [16] | Bartels, F., On Generalized Coinduction and Probabilistic Specification Formats: Distributive Laws in Coalgebraic Modelling (2004), Vrije Universiteit Amsterdam, Ph.D. thesis |
| [17] | Bloom, S. L.; Ésik, Z., Iteration Theories: The Equational Logic of Iterative Processes, EATCS Monographs on Theoretical Computer Science (1993), Springer · Zbl 0773.03033 |
| [18] | Bonsangue, M. M.; Milius, S.; Rot, J., On the specification of operations on the rational behaviour of systems, (Luttik, B.; Reniers, M. A., Proc. Combined Workshop on Expressiveness in Concurrency and Structural Operational Semantics. Proc. Combined Workshop on Expressiveness in Concurrency and Structural Operational Semantics, EXPRESS/SOS’12. Proc. Combined Workshop on Expressiveness in Concurrency and Structural Operational Semantics. Proc. Combined Workshop on Expressiveness in Concurrency and Structural Operational Semantics, EXPRESS/SOS’12, Electron. Proc. Theoret. Comput. Sci., vol. 89 (2012)), 3-18 · Zbl 1459.68124 |
| [19] | Bonsangue, M. M.; Milius, S.; Silva, A., Sound and complete axiomatizations of coalgebraic language equivalence, ACM Trans. Comput. Log., 1, 7 (2013), 52 pp · Zbl 1353.68186 |
| [20] | Borceux, F., Handbook of Categorical Algebra: Volume 1, Basic Category Theory, Encyclopedia of Mathematics and its Applications (1994), Cambridge University Press · Zbl 0803.18001 |
| [21] | 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 |
| [22] | Cenciarelli, P.; Moggi, E., A syntactic approach to modularity in denotational semantic, (Proc. 5th CTCS (1993)), CWI Technical Report |
| [23] | Courcelle, B., Fundamental properties of infinite trees, Theor. Comput. Sci., 25, 95-169 (1983) · Zbl 0521.68013 |
| [24] | Droste, M.; Kuich, W.; Vogler, H., Handbook of Weighted Automata (2009), Springer Publishing Company, Incorporated · Zbl 1200.68001 |
| [25] | Elgot, C., Monadic computation and iterative algebraic theories, (Rose, H. E.; Sheperdson, J. C., Logic Colloquium ’73, vol. 80 (1975), North-Holland Publishers: North-Holland Publishers Amsterdam), 175-230 · Zbl 0327.02040 |
| [26] | Fliess, M., Sur divers produits de séries formelles, Bull. Soc. Math. Fr., 102, 181-191 (1974) · Zbl 0313.13021 |
| [27] | Gabriel, P.; Ulmer, F., Lokal präsentierbare Kategorien, Lecture Notes Math., vol. 221 (1971), Springer-Verlag · Zbl 0225.18004 |
| [28] | Ghani, N.; Lüth, C.; Marchi, F. D., Monads of coalgebras: rational terms and term graphs, Math. Struct. Comput. Sci., 15, 433-451 (2005) · Zbl 1169.18303 |
| [29] | Ginali, S., Regular trees and the free iterative theory, J. Comput. Syst. Sci., 18, 228-242 (1979) · Zbl 0495.68042 |
| [30] | Goncharov, S., Trace semantics via generic observations, (Heckel, R.; Milius, S., Algebra and Coalgebra in Computer Science (CALCO 2013). Algebra and Coalgebra in Computer Science (CALCO 2013), Lecture Notes Comput. Sci., vol. 8089 (2013), Springer), 158-174 · Zbl 1394.68218 |
| [31] | Goncharov, S.; Milius, S.; Silva, A., Towards a coalgebraic Chomsky hierarchy, (Diaz, J.; Lanese, I.; Sangiorgi, D., Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science. Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science, TCS’14. Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science. Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science, TCS’14, Lecture Notes Comput. Sci., vol. 8705 (2014), Springer), 265-280 · Zbl 1417.68085 |
| [32] | Harrison, M. A.; Havel, I. M., Real-time strict deterministic languages, SIAM J. Comput., 1, 4, 333-349 (1972) · Zbl 0267.68034 |
| [33] | Hyland, M.; Plotkin, G.; Power, J., Combining effects: sum and tensor, Theor. Comput. Sci., 357, 1-3, 70-99 (2006) · Zbl 1096.68088 |
| [34] | Jacobs, B., A bialgebraic review of regular expressions, deterministic automata and languages, (K. F.; etal., Goguen Festschrift. Goguen Festschrift, Lecture Notes Comput. Sci., vol. 4060 (2006)), 375-404 · Zbl 1133.68049 |
| [35] | Kelly, G. M., A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on, Bull. Aust. Math. Soc., 22, 1-83 (1980) · Zbl 0437.18004 |
| [36] | Klin, B., Bialgebras for structural operational semantics: an introduction, Theor. Comput. Sci., 412, 38, 5043-5069 (2011) · Zbl 1246.68150 |
| [37] | Lambek, J., A fixpoint theorem for complete categories, Math. Z., 103, 151-161 (1968) · Zbl 0149.26105 |
| [38] | MacLane, S., Categories for the Working Mathematician, Graduate Texts in Mathematics (1998), Springer: Springer New York · Zbl 0906.18001 |
| [39] | Milius, S., Completely iterative algebras and completely iterative monads, Inf. Comput., 196, 1-41 (2005) · Zbl 1062.68075 |
| [40] | Milius, S., A sound and complete calculus for finite stream circuits, (Proc. 25th Annual Symposium on Logic in Computer Science. Proc. 25th Annual Symposium on Logic in Computer Science, LICS’10 (2010)), 449-458 |
| [41] | Milius, S., Proper functors and their rational fixed point, (Bonchi, F.; König, B., Proc. 7th Conference on Algebra and Coalgebra in Computer Science. Proc. 7th Conference on Algebra and Coalgebra in Computer Science, CALCO’17. Proc. 7th Conference on Algebra and Coalgebra in Computer Science. Proc. 7th Conference on Algebra and Coalgebra in Computer Science, CALCO’17, LIPIcs, vol. 72 (2017), Schloss Dagstuhl), Article 18 pp., in press · Zbl 1433.18001 |
| [42] | Milius, S., Proper functors and fixed points for finite behaviour, Log. Methods Comput. Sci., 3, 22 (2018), 32 pp · Zbl 1448.18008 |
| [43] | Milius, S.; Bonsangue, M. M.; Myers, R. S.; Rot, J., Rational operation models, (Mislove, M., Proc. 29th conference on Mathematical Foundations of Programming Science. Proc. 29th conference on Mathematical Foundations of Programming Science, MFPS XXIX. Proc. 29th conference on Mathematical Foundations of Programming Science. Proc. 29th conference on Mathematical Foundations of Programming Science, MFPS XXIX, Electron. Notes Theor. Comput. Sci., vol. 298 (2013)), 257-282 · Zbl 1334.68137 |
| [44] | Milius, S.; Moss, L. S., The category theoretic solution of recursive program schemes, Theor. Comput. Sci., 366, 3-59 (2006) · Zbl 1154.68041 |
| [45] | Milius, S.; Pattinson, D.; Wißmann, T., A new foundation for finitary corecursion: The locally finite fixpoint and its properties, (Proc. 19th International Conference on Foundations of Software Science and Computation Structures. Proc. 19th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS’16. Proc. 19th International Conference on Foundations of Software Science and Computation Structures. Proc. 19th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS’16, Lecture Notes Comput. Sci. (ARCoSS), vol. 19 (2016)), 107-125 · Zbl 1475.68196 |
| [46] | Milius, S.; Wißmann, T., Finitary corecursion for the infinitary lambda calculus, (Moss, L. S.; Sobocinski, P., Proc. Coalgebraic and Algebraic Methods in Computer Science. Proc. Coalgebraic and Algebraic Methods in Computer Science, CALCO’15. Proc. Coalgebraic and Algebraic Methods in Computer Science. Proc. Coalgebraic and Algebraic Methods in Computer Science, CALCO’15, LIPICS, vol. 35 (2015)), 336-351 · Zbl 1366.03172 |
| [47] | Myers, R., Rational Coalgebraic Machines in Varieties: Languages, Completeness and Automatic Proofs (2011), Imperial College London, Department of Computing, Ph.D. thesis |
| [48] | Petre, I.; Salomaa, A., Algebraic systems and pushdown automata, (Handbook of Weighted Automata (2009), Springer), 257-289 · Zbl 1484.68109 |
| [49] | Plotkin, G.; Turi, D., Towards a mathematical operational semantics, (Proc. 12th LICS Conf. (1997), IEEE, Computer Society Press), 280-291 |
| [50] | Rot, J.; Bonsangue, M.; Rutten, J., Coalgebraic bisimulation-up-to, (van Emde Boas, P.; etal., Proc. SOFSEM 2013. Proc. SOFSEM 2013, Lecture Notes Comput. Sci., vol. 7741 (2013), Springer), 369-381 · Zbl 1303.68088 |
| [51] | Rutten, J., Automata and coinduction (an exercise in coalgebra), (Sangiorgi, D.; de Simone, R., Proc. CONCUR 1998. Proc. CONCUR 1998, LNCS, vol. 1466 (1998), Springer), 194-218 · Zbl 0940.68085 |
| [52] | Rutten, J., Universal coalgebra: a theory of systems, Theor. Comput. Sci., 249, 1, 3-80 (2000) · Zbl 0951.68038 |
| [53] | Silva, A.; Bonchi, F.; Bonsangue, M. M.; Rutten, J. J.M. M., Quantitative Kleene coalgebras, Inf. Comput., 209, 5, 822-849 (2011) · Zbl 1227.68075 |
| [54] | Silva, A.; Bonchi, F.; Bonsangue, M. M.; Rutten, J. J.M. M., Generalizing determinization from automata to coalgebras, Log. Methods Comput. Sci., 1, 9 (2013), 27 pp · Zbl 1262.18002 |
| [55] | Silva, A.; Bonsangue, M. M.; Rutten, J. J.M. M., Non-deterministic Kleene coalgebras, Log. Methods Comput. Sci., 3, 23 (2010), 39 pp · Zbl 1208.68141 |
| [56] | Urbat, H., Finite behaviours and finitary corecursion, (Proc. CALCO’17. Proc. CALCO’17, LIPIcs, vol. 72 (2017)), Article 24 pp. · Zbl 1433.68207 |
| [57] | Winter, J.; Bonsangue, M.; Rutten, J., Coalgebraic characterizations of context-free languages, Log. Methods Comput. Sci., 9, 3 (September 2013) · Zbl 1274.68215 |
| [58] | Winter, J.; Bonsangue, M. M.; Rutten, J. J., Context-free coalgebras, J. Comput. Syst. Sci., 81, 5, 911-939 (2015) · Zbl 1328.68133 |
| [59] | Winter, J.; Bonsangue, M. M.; Rutten, J. J.M. M., Coalgebraic characterizations of context-free languages, Log. Methods Comput. Sci., 9, 3 (2013) · Zbl 1274.68215 |
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.
