Hostname: page-component-586b7cd67f-gb8f7 Total loading time: 0 Render date: 2024-11-24T22:56:29.640Z Has data issue: false hasContentIssue false
  • English
  • Français

Equational properties of fixed-point operations in cartesian categories: An overview

Published online by Cambridge University Press:  24 May 2019

Z Ésik
Z Ésik*
Affiliation:
Department of Computer Science, University of Szeged, Hungary Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Several fixed-point models share the equational properties of iteration theories, or iteration categories, which are cartesian categories equipped with a fixed point or dagger operation subject to certain axioms. After discussing some of the basic models, we provide equational bases for iteration categories and offer an analysis of the axioms. Although iteration categories have no finite base for their identities, there exist finitely based implicational theories that capture their equational theory. We exhibit several such systems. Then we enrich iteration categories with an additive structure and exhibit interesting cases where the interaction between the iteration category structure and the additive structure can be captured by a finite number of identities. This includes the iteration category of monotonic or continuous functions over complete lattices equipped with the least fixed-point operation and the binary supremum operation as addition, the categories of simulation, bisimulation, or language equivalence classes of processes, context-free languages, and others. Finally, we exhibit a finite equational system involving residuals, which is sound and complete for monotonic or continuous functions over complete lattices in the sense that it proves all of their identities involving the operations and constants of cartesian categories, the least fixed-point operation and binary supremum, but not involving residuals.

Keywords

Fixed point theoriesiteration categoriesautomata theoryConway categories
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 29 , Issue 6 , June 2019 , pp. 909 - 925
Copyright
© Cambridge University Press 2019 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

*

Partially supported by grant no. ANN 110883 from the National Foundation for Scientific Research of Hungary

References

Aceto, L., Ésik, Z. and Ingólfsdóttir, A. (2002). Equational axioms for probabilistic bisimilarity. In: AMAST 2002, Lecture Notes in Computer Science, vol. 2422, 239–253.Google Scholar
Arkhangelsky, K. B. and Gorshkov, P. V. (1967). Implicational axioms for the algebra of regular languages (in Russian). Doklady Akademii Nauk USSR, Ser A. 10 67–69.Google Scholar
Arnold, A. and Nivat, M. (1980). Metric interpretations of infinite trees and semantics of non deterministic recursive programs. Theoretical Computer Science 11 181–205.CrossRefGoogle Scholar
Arnold, A. and Niwinski, D. (2001). Rudiments of μ-calculus, North-Holland.Google Scholar
Barr, M. and Wells, C. (2012). Category theory for computing science. Theory and Applications of Categories 22 168.Google Scholar
Bartha, M. (1987). A finite axiomatization of flowchart schemes. Acta Cybernetica 8 203–217.Google Scholar
Bekić, H. (1969). Definable Operation in General Algebras, and the Theory of Automata and Flowcharts. Technical report, IBM Vienna. Reprinted in: Programming Languages and Their Definition– Hans Bekić (1936–1982) (1984). Lecture Notes in Computer Science, vol. 177, Springer, 30–55.CrossRefGoogle Scholar
Bernátsky, L. and Ésik, Z. (1998). Semantics on flowchart programs and the free Conway theories. Informatique Théorique et Applications 32 35–78.CrossRefGoogle Scholar
Bloom, S. L., Elgot, C. and Wright, J. B. (1980). Solutions of the iteration equation and extensions of the scalar iteration operation. SIAM Journal on Computing 9 25–45.CrossRefGoogle Scholar
Bloom, S. L. and Ésik, Z. (1989). Equational logic of circular data type specification. Theoretical Computer Science 63 303–331.CrossRefGoogle Scholar
Bloom, S. L. and Ésik, Z. (1991). Floyd-Hoare logic in iteration theories. Journal of the ACM 38 887–934.CrossRefGoogle Scholar
Bloom, S. L. and Ésik, Z. (1993). Iteration Theories, Springer.CrossRefGoogle Scholar
Bloom, S. L. and Ésik, Z. (1994). Some quasi-varieties of iteration theories. In: MFPS 1993, Lecture Notes in Computer Science, vol. 802, Springer, 378–409.Google Scholar
Bloom, S. L. and Ésik, Z. (1997). The equational logic of fixed points (Tutorial). Theoretical Computer Science 179 1–60.CrossRefGoogle Scholar
Bloom, S. L. and Ésik, Z. (2000). Iteration algebras are not finitely axiomatizable. In: LATIN 2000, Lecture Notes in Computer Science, vol. 1776, Springer, 367–376.Google Scholar
Bloom, S. L. and Ésik, Z. (2003). An extension theorem with an application to formal tree series. Journal of Automata, Languages and Combinatorics 8 145–185.Google Scholar
Bloom, S. L. and Ésik, Z. (2009). Axiomatizing rational power series over natural numbers. Information and Computation 207 793–811.CrossRefGoogle Scholar
Bloom, S. L., Ésik, Z., Labella, A. and Manes, E. G. (2001). Iteration 2-theories. Applied Categorical Structures 9 173–216.CrossRefGoogle Scholar
Bloom, S. L., Ésik, Z. and Taubner, D. (1993). Iteration theories of synchronization trees. Information and Computation 102 1–55.CrossRefGoogle Scholar
Boffa, M. (1990). Une remarque sur les systémes complets d’identités rationnelles. Informatique Théorique et Applications 24 419–428.CrossRefGoogle Scholar
Boffa, M. (1995). Une condition impliquant toutes les identités rationnelles. Informatique Théorique et Applications 29 515–518.CrossRefGoogle Scholar
Cazanescu, V. E. and Stefanescu, Gh. (1990). Towards a new algebraic foundation of flowchart scheme theory. Fundamenta Informaticae 13 171–210.Google Scholar
Cohn, P. M. (1981). Universal Algebra. 2nd edition, D Reidel.CrossRefGoogle Scholar
Davey, B. A. and Priestly, H. A. (1990). Introduction to Lattices and Order, Cambridge University Press.Google Scholar
De Bakker, J. W. and Scott, D. (1969). A Theory of Programs. Technical Report, IBM, Vienna.Google Scholar
Elgot, C. C. (1975). Monadic computation and iterative algebraic theories. In: Logic Colloquium 1973, Bristol, Studies in Logic and the Foundations of Mathematics, vol. 80, North-Holland, Amsterdam, 175–230.Google Scholar
Ésik, Z. (1980). Identities in iterative and rational theories. Computational Linguistics and Computer Languages 14 183–207.Google Scholar
Ésik, Z. (1988). Independence of the equational axioms of iteration theories. Journal of Computer and System Sciences 36 66–76.CrossRefGoogle Scholar
Ésik, Z. (1990). A note on the axiomatization of iteration theories. Acta Cybernetica 9 375–384.Google Scholar
Ésik, Z. (1997). Completeness of Park induction. Theoretical Computer Science 177 217–283.CrossRefGoogle Scholar
Ésik, Z. (1998). Axiomatizing the equational theory of regular tree languages (Extended abstract). In: STACS 1998, Lecture Notes in Computer Science, vol. 1373, Springer, 455–465.Google Scholar
Ésik, Z. (1999a). Group axioms for iteration. Information and Computation 148 131–180.CrossRefGoogle Scholar
Ésik, Z. (1999b). Axiomatizing iteration categories. Acta Cybernetica 14 65–82.Google Scholar
Ésik, Z. (2000a). Axiomatizing the least fixed point operation and binary supremum. In: CSL 2000, Lecture Notes in Computer Science, vol. 1862, Springer, 302–316.Google Scholar
Ésik, Z. (2000b). A proof of the Krohn-Rhodes decomposition theorem. Theoretical Computer Science 234 287–300.CrossRefGoogle Scholar
Ésik, Z. (2000c). The power of the group axioms for iteration. International Journal of Algebra and Computation 10 349–373.CrossRefGoogle Scholar
Ésik, Z. (2010). Axiomatizing the equational theory of regular tree languages. Journal of Logic and Algebraic Programming 79 189–213.CrossRefGoogle Scholar
Ésik, Z. (2011). Multi-linear iterative K-Îč-semialgebras. Electronic Notes in Theoretical Computer Science 276 159–170.CrossRefGoogle Scholar
Ésik, Z. (2013). A connection between concurrency and language theory. Electronic Notes in Theoretical Computer Science 298 143–164.CrossRefGoogle Scholar
Ésik, Z. (2014). Axiomatizing weighted synchronization trees and weighted bisimilarity. Theoretical Computer Science 534 2–23.CrossRefGoogle Scholar
Ésik, Z. (2015). Residuated Park theories. Journal of Logic and Computation 25 453–471.CrossRefGoogle Scholar
Ésik, Z. (2015). Equational properties of stratified least fixed points. In: WoLLIC 2015, Lecture Notes in Computer Science Bloomington, IN, USA, July 20–33, Springer, 174–188.Google Scholar
Ésik, Z. (2017). Equational axioms associated with finite automata for fixed point operations in cartesian categories. Mathematical Structures in Computer Science 27 54–69.CrossRefGoogle Scholar
Ésik, Z. and Bernátsky, L. (1985). Scott induction and equational proofs. Electronic Notes in Theoretical Computer Science 1 154–181.CrossRefGoogle Scholar
Ésik, Z. and Kuich, W. (2004). Inductive star-semirings. Theoretical Computer Science 324 3–33.CrossRefGoogle Scholar
Ésik, Z. and Kuich, W. (2012). Free iterative and iteration K–semialgebras. Algebra Universalis 67 141–162.CrossRefGoogle Scholar
Ésik, Z. and Kuich, W. (2013). Free inductive K-semialgebras. Journal of Logic and Algebraic Programming 8 111–122.CrossRefGoogle Scholar
Ésik, Z. and Kuich, W. (2017). Solving fixed-point equations over complete semirings. The Role of Theory in Computer Science - Essays Dedicated to Janusz Brzozowski. 33–58.CrossRefGoogle Scholar
Ésik, Z. and Labella, A. (1998). Equational properties of iteration in algebraically complete categories. Theoretical Computer Science 195 61–89.CrossRefGoogle Scholar
Ésik, Z. and Rondogiannis, P. (2015). A fixed point theorem for non-monotonic functions. Theoretical Computer Science 574 18–38.CrossRefGoogle Scholar
Gécseg, F. (1986). Products of Automata, Springer.CrossRefGoogle Scholar
Ginzburg, A. (1968). Algebraic Theory of Automata, Academic Press.Google Scholar
Goguen, J. A., Thatcher, J. W., Wagner, E. G. and Wright, J. B. (1977). Initial algebra semantics and continuous algebras. Journal of the ACM 24 68–95.CrossRefGoogle Scholar
Hasegawa, M. (1997). Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi. In: TLCA 1997, Lecture Notes in Computer Science, vol. 1210, Springer, 196–213.Google Scholar
Hyland, M. and Power, J. (2007). The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science 172 437–458.CrossRefGoogle Scholar
Joyal, A., Street, R. and Verity, D. (1996). Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society 3 447–468.CrossRefGoogle Scholar
Kozen, D. (1991). A completeness theorem for Kleene algebras and the algebra of regular events. In: LICS 1991, IEEP Press, 214–225.Google Scholar
Kozen, D. (1994). A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110 366–390.CrossRefGoogle Scholar
Krob, D. (1990). A complete system of B-rational identities. In: ICALP 1990, Lecture Notes in Computer Science, vol. 443, Springer, 60–73.Google Scholar
Krob, D. (1991). Complete systems of B-rational identities. Theoretical Computer Science 89 207–343.CrossRefGoogle Scholar
Krohn, K. and Rhodes, J. L. (1965). Algebraic theory of machines, I, Principles of finite semigroups and machines. Transactions of the American Mathematical Society 116 450–464.CrossRefGoogle Scholar
Lawvere, F. W. (1963). Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America 50 869–872.CrossRefGoogle ScholarPubMed
Lehmann, D. and Smyth, M. B. (1981). Algebraic specification of data types: A synthetic approach. Mathematical Systems Theory 14 97–139.CrossRefGoogle Scholar
Milner, R. (1989). Communication and Concurrency, Prentice-Hall.Google Scholar
Niwinski, D. (1985). Equational μ-calculus. In: Computation Theory, Lecture Notes in Computer Science, vol. 208, Springer, 169–176.CrossRefGoogle Scholar
Niwinski, D. (1986). On fixed-point clones (Extended abstract). In: ICALP’86, Lecture Notes in Computer Science, vol. 226, Springer, 464–473.Google Scholar
Park, D. M. R. (1981). Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science, Lecture Notes in Computer Science, vol. 104, Springer, 167–183.CrossRefGoogle Scholar
Plotkin, G. (1983). Domains. The Pisa Notes, The University of Edinburgh.Google Scholar
Pratt, V. (1990). Action logic and pure induction. In: Logics in AI 1990, Lecture Notes in Computer Science, vol. 478, Springer, 97–120.Google Scholar
Santocanale, L. (2003). On the equational definition of the least prefixed point. Theoretical Computer Science 295 341–370.CrossRefGoogle Scholar
Simpson, A. K. and Plotkin, G. D. (2000). Complete axioms for categorical fixed-point operators. In: LICS 2000, IEEE Press, 30–41.Google Scholar
Wagner, E. G., Bloom, S. L. and Thatcher, J. W. (1986). Why algebraic theories. In: Algebraic Methods in Semantics, Cambridge University Press, 607–634.Google Scholar
Wright, J. B., Thatcher, J. W., Wagner, E. G. and Goguen, J. A. (1976). Rational algebraic theories and fixed-point solutions. In: FOCS 1976, IEEE Press, 147–158.Google Scholar