The category-theoretic solution of recursive program schemes. (English) Zbl 1154.68041
Summary: This paper provides a general account of the notion of recursive program schemes, studying both uninterpreted and interpreted solutions. It can be regarded as the category-theoretic version of the classical area of algebraic semantics. The overall assumptions needed are small indeed: working only in categories with “enough final coalgebras” we show how to formulate, solve, and study recursive program schemes. Our general theory is algebraic and so avoids using ordered or metric structures. Our work generalizes the previous approaches which do use this extra structure by isolating the key concepts needed to study substitution in infinite trees, including second-order substitution. As special cases of our interpreted solutions we obtain the usual denotational semantics using complete partial orders, and the one using complete metric spaces. Our theory also encompasses implicitly defined objects which are not usually taken to be related to recursive program schemes. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 18C10 | Theories (e.g., algebraic theories), structure, and semantics |
| 18C15 | Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads |
| 68Q55 | Semantics in the theory of computing |
Keywords:
recursive program scheme; Elgot algebra; coalgebra; completely iterative monad; algebraic trees; second-order substitutionReferences:
| [1] | Aczel, P., Non-Well-Founded Sets, CSLI Lecture Notes, Vol. 14 (1988), CSLI Publications: CSLI Publications Stanford · Zbl 0668.04001 |
| [2] | Aczel, P.; Adámek, J.; Milius, S.; Velebil, J., Infinite trees and completely iterative theoriesa coalgebraic view, Theoret. Comput. Sci., 300, 1-45 (2003) · Zbl 1028.68077 |
| [3] | P. Aczel, J. Adámek, J. Velebil, A coalgebraic view of infinite trees and iteration, Electron. Notes Theoret. Comput. Sci, Vol. 44, no. 1, 2001, 26pp.; P. Aczel, J. Adámek, J. Velebil, A coalgebraic view of infinite trees and iteration, Electron. Notes Theoret. Comput. Sci, Vol. 44, no. 1, 2001, 26pp. · Zbl 1260.68235 |
| [4] | Adámek, J.; Koubek, V., On the greatest fixed point of a set functor, Theoret. Comput. Sci., 150, 57-75 (1995) · Zbl 0874.18001 |
| [5] | J. Adámek, S. Milius, Terminal coalgebras and free iterative theories, Inform. and Comput. 204 (2006) 1139-1172.; J. Adámek, S. Milius, Terminal coalgebras and free iterative theories, Inform. and Comput. 204 (2006) 1139-1172. · Zbl 1104.68068 |
| [6] | Adámek, J.; Milius, S.; Velebil, J., Free iterative theories: a coalgebraic view, Math. Structures Comput. Sci., 13, 259-320 (2003) · Zbl 1030.18004 |
| [7] | J. Adámek, S. Milius, J. Velebil, Iterative algebras at work, Math. Struct. Comput. Sci., accepted for publication, available at the URL \(\langle;\rangle;\), extended abstract appeared in Electron. Notes Theoret. Comput. Sci. 106 (2004) 3-24.; J. Adámek, S. Milius, J. Velebil, Iterative algebras at work, Math. Struct. Comput. Sci., accepted for publication, available at the URL \(\langle;\rangle;\), extended abstract appeared in Electron. Notes Theoret. Comput. Sci. 106 (2004) 3-24. |
| [8] | Adámek, J.; Milius, S.; Velebil, J., On coalgebra based on classes, Theoret. Comput. Sci., 316, 3-23 (2004) · Zbl 1047.18005 |
| [9] | J. Adámek, S. Milius, J. Velebil, Elgot Algebras, full version submitted and available at the URL \(\langle;\rangle;\), extended abstract in Electron. Notes in Theor. Comput. Sci. 155 (2006) 87-109.; J. Adámek, S. Milius, J. Velebil, Elgot Algebras, full version submitted and available at the URL \(\langle;\rangle;\), extended abstract in Electron. Notes in Theor. Comput. Sci. 155 (2006) 87-109. |
| [10] | Adámek, J.; Porst, H.-E., On tree coalgebras and coalgebra presentations, Theoret. Comput. Sci., 311, 257-283 (2004) · Zbl 1086.68088 |
| [11] | Adámek, J.; Reitermann, J., Banach’s fixed-point theorem as a base for data-type equations, Appl. Categ. Struct., 2, 77-90 (1994) · Zbl 0802.18007 |
| [12] | Adámek, J.; Trnková, V., Automata and Algebras in Categories (1990), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht · Zbl 0698.18001 |
| [13] | America, P.; Rutten, J. J.M. M., Solving reflexive domain equations in a category of complete metric spaces, J. Comput. System Sci., 39, 343-375 (1989) · Zbl 0717.18002 |
| [14] | Arnold, A.; Nivat, M., The metric space of infinite trees. Algebraic and topological properties, Fund. Inform., III, 4, 445-476 (1980) · Zbl 0453.68021 |
| [15] | Barnsley, M. F., Fractals Everywhere (1988), Academic Press: Academic Press New York · Zbl 0691.58001 |
| [16] | Barr, M., Terminal coalgebras in well-founded set theory, Theoret. Comput. Sci., 114, 299-315 (1993) · Zbl 0779.18004 |
| [17] | Barwise, J.; Moss, L. S., Vicious Circles (1996), CSLI Publications: CSLI Publications Stanford · Zbl 0865.03002 |
| [18] | Bloom, S. L., All solutions of a system of recursion equations in infinite trees and other contraction theories, J. Comput. System Sci., 27, 225-255 (1983) · Zbl 0535.68006 |
| [19] | Bloom, S. L.; Ésik, Z., Iteration Theories: The Equational Logic of Iterative Processes, EATCS Monographs on Theoretical Computer Science (1993), Springer: Springer Berlin · Zbl 0773.03033 |
| [20] | Borceux, F., Handbook of categorical algebra 2: categories and structures, Encyclopedia of Mathematics and its Applications, Vol. 51 (1994), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0843.18001 |
| [21] | Courcelle, B., Fundamental properties of infinite trees, Theoret. Comput. Sci., 25, 2, 95-169 (1983) · Zbl 0521.68013 |
| [22] | 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 |
| [23] | Elgot, C. C.; Bloom, S. L.; Tindell, R., On the algebraic structure of rooted trees, J. Comput. System Sci., 16, 361-399 (1978) · Zbl 0389.68007 |
| [24] | Ghani, N.; Lüth, C.; De Marchi, F.; Power, A. J., Algebras, coalgebras, monads and comonads, Electron. Notes Theoret. Comput. Sci., 44, 1, 18 (2001) · Zbl 1260.68238 |
| [25] | Ghani, N.; Lüth, C.; De Marchi, F., Solving algebraic equations using coalgebra, Theoret. Inform. Appl., 37, 301-314 (2003) · Zbl 1038.18005 |
| [26] | Ghani, N.; Lüth, C.; De Marchi, F.; Power, A. J., Dualising initial algebras, Math. Struct. Comput. Sci., 13, 2, 349-370 (2003) · Zbl 1049.18005 |
| [27] | Guessarian, I., Algebraic Semantics, Lecture Notes in Computer Science, Vol. 99 (1981), Springer: Springer Berlin · Zbl 0474.68010 |
| [28] | Lambek, J., A fixpoint theorem for complete categories, Math. Z., 103, 151-161 (1968) · Zbl 0149.26105 |
| [29] | T. Leinster, General self-similarity: an overview, e-print math.DS/0411343 v1.; T. Leinster, General self-similarity: an overview, e-print math.DS/0411343 v1. · Zbl 1132.18008 |
| [30] | T. Leinster, A general theory of self-similarity I, e-print math.DS/041344.; T. Leinster, A general theory of self-similarity I, e-print math.DS/041344. · Zbl 1214.03049 |
| [31] | T. Leinster, A general theory of self-similarity II, e-print math.DS/0411345.; T. Leinster, A general theory of self-similarity II, e-print math.DS/0411345. · Zbl 1214.03049 |
| [32] | Mac Lane, S., Categories for the Working Mathematician (1998), Springer: Springer Berlin · Zbl 0906.18001 |
| [33] | R. Matthes, T. Uustalu, Substitution in non-wellfounded syntax with variable binding, in: H.P. Gumm (Ed.), Electronic Notes in Theoretical Computer Science, Vol. 82, no. 1, 2003, 15pp.; R. Matthes, T. Uustalu, Substitution in non-wellfounded syntax with variable binding, in: H.P. Gumm (Ed.), Electronic Notes in Theoretical Computer Science, Vol. 82, no. 1, 2003, 15pp. · Zbl 1270.68089 |
| [34] | S. Milius, On iteratable endofunctors, Electron. Notes Theoret. Comput. Sci, Vol. 69, 2002, 18pp.; S. Milius, On iteratable endofunctors, Electron. Notes Theoret. Comput. Sci, Vol. 69, 2002, 18pp. · Zbl 1270.18012 |
| [35] | Milius, S., Completely iterative algebras and completely iterative monads, Inform. and Comput., 196, 1-41 (2005) · Zbl 1062.68075 |
| [36] | Milius, S.; Moss, L. S., The category theoretic solution of recursive program schemes, extended abstract, (in: Proc. First Internat. Conf. on Algebra and Coalgebra in Computer Science (CALCO 2005), Lecture Notes in Computer Science, Vol. 3629 (2005), Springer: Springer Berlin), 293-312 · Zbl 1151.68376 |
| [37] | S. Milius, L.S. Moss, Equational properties of solutions to recursive program schemes, working draft.; S. Milius, L.S. Moss, Equational properties of solutions to recursive program schemes, working draft. · Zbl 1170.68009 |
| [38] | S. Milius, L.S. Moss, Recursive program scheme solutions in hypersets, working draft.; S. Milius, L.S. Moss, Recursive program scheme solutions in hypersets, working draft. · Zbl 1170.68009 |
| [39] | Moss, L. S., Parametric corecursion, Theoret. Comput. Sci., 260, 1-2, 139-163 (2001) · Zbl 0973.68134 |
| [40] | L.S. Moss, The coalgebraic treatment of second-order substitution and uninterpreted recursive program schemes, preprint, 2002.; L.S. Moss, The coalgebraic treatment of second-order substitution and uninterpreted recursive program schemes, preprint, 2002. |
| [41] | L.S. Moss, Uniform functors on sets, in: K. Futatsugi et al. (Eds.), Algebra, Meaning, and Computation: A Festschrift in Honor of Prof. Joseph Goguen, Lecture Notes in Computer Science, Vol. 4064, Springer, Berlin, 2006, pp. 420-448.; L.S. Moss, Uniform functors on sets, in: K. Futatsugi et al. (Eds.), Algebra, Meaning, and Computation: A Festschrift in Honor of Prof. Joseph Goguen, Lecture Notes in Computer Science, Vol. 4064, Springer, Berlin, 2006, pp. 420-448. · Zbl 1133.68047 |
| [42] | Nivat, M., On the interpretation of recursive polyadic program schemes, Symp. Math., XV, 255-281 (1975) · Zbl 0346.68041 |
| [43] | Worrell, J., On the final sequence of a finitary set functor, Theoret. 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.
