Skip to main content
SpringerLink
Log in

Equational Properties of Fixed Point Operations in Cartesian Categories: An Overview

  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 2015 (MFCS 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9234))

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.

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

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Aceto, L., Ésik, Z., Ingólfsdóttir, A.: Equational axioms for probabilistic bisimilarity. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 239–254. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Arkhangelsky, K.B., Gorshkov, P.V.: Implicational axioms for the algebra of regular languages. Dokl. Akad. Nauk USSR Ser. A 10, 67–69 (1967). (in Russian)

    Google Scholar 

  3. Arnold, A., Nivat, M.: Metric interpretations of infinite trees and semantics of non deterministic recursive programs. Theor. Comput. Sci. 11, 181–205 (1980)

    Article  MathSciNet  Google Scholar 

  4. Arnold, A., Niwinski, D.: Rudiments of \(\mu \)-Calculus. North-Holland, Amsterdam (2001)

    Google Scholar 

  5. Barr, M., Wells, C.: Category theory for computing science. Reprints Theory Appl. Categories (22), 172 (2012)

    Google Scholar 

  6. Bartha, M.: A finite axiomatization of flowchart schemes. Acta Cybern. 8, 203–217 (1987)

    MathSciNet  Google Scholar 

  7. Bekić, H.: Definable operation in general algebras, and the theory of automata and flowcharts. Technical report, IBM Vienna (1969). Reprinted in: Programming Languages and Their Definition - Hans Bekić (1936–1982). LNCS, vol. 177, pp. 30–55. Springer, Heidelberg (1984)

    Google Scholar 

  8. Bernátsky, L., Ésik, Z.: Semantics on flowchart programs and the free Conway theories. ITA 32, 35–78 (1998)

    Google Scholar 

  9. Bloom, S.L., Elgot, C., Wright, J.B.: Solutions of the iteration equation and extensions of the scalar iteration operation. SIAM J. Comput. 9, 25–45 (1980)

    Article  MathSciNet  Google Scholar 

  10. Bloom, S.L., Ésik, Z.: Equational logic of circular data type specification. Theor. Comput. Sci. 63, 303–331 (1989)

    Article  Google Scholar 

  11. Bloom, S.L., Ésik, Z.: Floyd-Hoare logic in iteration theories. J. ACM 38, 887–934 (1991)

    Article  Google Scholar 

  12. Bloom, S.L., Ésik, Z.: Iteration Theories. Springer, Heidelberg (1993)

    Book  Google Scholar 

  13. Bloom, S.L., Ésik, Z., Taubner, D.: Iteration theories of synchronization trees. Inf. Comput. 102, 1–55 (1993)

    Article  Google Scholar 

  14. Bloom, S.L., Ésik, Z.: Some quasi-varieties of iteration theories. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 378–409. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  15. Bloom, S.L., Ésik, Z.: The equational logic of fixed points (Tutorial). Theor. Comput. Sci. 179, 1–60 (1997)

    Article  Google Scholar 

  16. Bloom, S.L., Ésik, Z.: An extension theorem with an application to formal tree series. J. Automata Lang. Comb. 8, 145–185 (2003)

    Google Scholar 

  17. Bloom, S.L., Ésik, Z.: Axiomatizing rational power series over natural numbers. Inf. Comput. 207, 793–811 (2009)

    Article  Google Scholar 

  18. Bloom, S.L., Ésik, Z.: Iteration algebras are not finitely axiomatizable. In: Gonnet, G.H., Viola, A. (eds.) LATIN 2000. LNCS, vol. 1776, pp. 367–376. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Bloom, S.L., Ésik, Z., Labella, A., Manes, E.G.: Iteration 2-theories. Appl. Categorical Struct. 9, 173–216 (2001)

    Article  Google Scholar 

  20. Boffa, M.: Une remarque sur les systémes complets d’identités rationnelles. ITA 24, 419–428 (1990)

    MathSciNet  Google Scholar 

  21. Boffa, M.: Une condition impliquant toutes les identités rationnelles. ITA 29, 515–518 (1995)

    MathSciNet  Google Scholar 

  22. Cazanescu, V.E., Stefanescu, G.: Towards a new algebraic foundation of flowchart scheme theory. Fund. Inform. 13, 171–210 (1990)

    MathSciNet  Google Scholar 

  23. Cohn, P.M.: Universal algebra, 2nd edn. D. Reidel, Dordrecht (1981)

    Book  Google Scholar 

  24. Davey, B.A., Priestly, H.A.: Introduction to lattices and order. Cambridge Univ. Press, Cambridge (1990)

    Google Scholar 

  25. De Bakker, J.W., Scott, D.: A theory of programs. Technical report, IBM Vienna (1969)

    Google Scholar 

  26. Elgot, C.C.: Monadic computation and iterative algebraic theories. In: Logic Colloquium 1973, Bristol. Studies in Logic and the Foundations of Mathematics, vol. 80, pp. 175–230. North-Holland, Amsterdam (1975)

    Google Scholar 

  27. Ésik, Z.: Identities in iterative and rational theories. Comput. Linguist. Comput. Lang. 14, 183–207 (1980)

    MathSciNet  Google Scholar 

  28. Ésik, Z.: Independence of the equational axioms of iteration theories. JCSS 36, 66–76 (1988)

    Google Scholar 

  29. Ésik, Z.: A note on the axiomatization of iteration theories. Acta Cybern. 9, 375–384 (1990)

    Google Scholar 

  30. Ésik, Z.: Completeness of park induction. Theor. Comput. Sci. 177, 217–283 (1997)

    Article  Google Scholar 

  31. Ésik, Z.: Axiomatizing the equational theory of regular tree languages (Extended abstract). In: Meinel, C., Morvan, M. (eds.) STACS 1998. LNCS, vol. 1373, pp. 455–465. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  32. Ésik, Z.: Group axioms for iteration. Inf. Comput. 148, 131–180 (1999)

    Article  Google Scholar 

  33. Ésik, Z.: Axiomatizing iteration categories. Acta Cybern. 14, 65–82 (1999)

    Google Scholar 

  34. Ésik, Z.: Axiomatizing the least fixed point operation and binary supremum. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 302–316. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  35. Ésik, Z.: A proof of the Krohn-Rhodes decomposition theorem. Theor. Comput. Sci. 234, 287–300 (2000)

    Article  Google Scholar 

  36. Ésik, Z.: The power of the group axioms for iteration. Int. J. Algebr. Comput. 10, 349–373 (2000)

    Google Scholar 

  37. Ésik, Z.: Axiomatizing the equational theory of regular tree languages. J. Log. Algebr. Program. 79, 189–213 (2010)

    Article  MathSciNet  Google Scholar 

  38. Ésik, Z.: Multi-linear iterative K-semialgebras. Electr. Notes Theor. Comput. Sci. 276, 159–170 (2011)

    Article  Google Scholar 

  39. Ésik, Z.: A connection between concurrency and language theory. Electr. Notes Theor. Comput. Sci. 298, 143–164 (2013)

    Article  Google Scholar 

  40. Ésik, Z.: Axiomatizing weighted synchronization trees and weighted bisimilarity. Theor. Comput. Sci. 534, 2–23 (2014)

    Article  Google Scholar 

  41. Ésik, Z.: Residuated park theories. J. Log. Comput. 25, 453–471 (2015)

    Article  Google Scholar 

  42. Ésik, Z.: Equational axioms associated with finite automata for fixed point operations in cartesian categories. Math. Struct. Comput. Sci. (to appear)

    Google Scholar 

  43. Ésik, Z.: Equational properties of stratified least fixed points (extended abstract). In: de Paiva, V., de Queiroz, R., Moss, L.S., Leivant, D., de Oliveira, A. (eds.) WoLLIC 2015. LNCS, vol. 9160, pp. 174–188. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  44. Ésik, Z., Bernátsky, L.: Scott induction and equational proofs. Electr. Notes Theor. Comput. Sci. 1, 154–181 (1985)

    Article  Google Scholar 

  45. Ésik, Z., Kuich, W.: Inductive star-semirings. Theor. Comput. Sci. 324, 3–33 (2004)

    Article  Google Scholar 

  46. Ésik, Z., Kuich, W.: Free iterative and iteration K-semialgebras. Algebra Univers. 67, 141–162 (2012)

    Article  Google Scholar 

  47. Ésik, Z., Kuich, W.: Free inductive K-semialgebras. J. Log. Algebr. Program. 82, 111–122 (2013)

    Article  MathSciNet  Google Scholar 

  48. Ésik, Z., Kuich, W.: Solving fixed-point equations over complete semirings (to appear)

    Google Scholar 

  49. Ésik, Z., Labella, A.: Equational properties of iteration in algebraically complete categories. Theor. Comput. Sci. 195, 61–89 (1998)

    Article  Google Scholar 

  50. Ésik, Z., Rondogiannis, P.: A fixed point theorem for non-monotonic functions. Theor. Comput. Sci. 574, 18–38 (2015)

    Article  Google Scholar 

  51. Gécseg, F.: Products of Automata. Springer, Berlin (1986)

    Book  Google Scholar 

  52. Ginzburg, A.: Algebraic Theory of Automata. Academic Press, New-York (1968)

    Google Scholar 

  53. Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Initial algebra semantics and continuous algebras. J. ACM 24, 68–95 (1977)

    Article  MathSciNet  Google Scholar 

  54. Hasegawa, M.: Recursion from cyclic sharing: traced monoidal categories and models of cyclic lambda calculi. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 196–213. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  55. Hyland, M., Power, J.: The category theoretic understanding of universal algebra: Lawvere theories and monads. Electr. Notes Theor. Comput. Sci. 172, 437–458 (2007)

    Article  MathSciNet  Google Scholar 

  56. Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Math. Proc. Camb. Philos. Soc. 3, 447–468 (1996)

    Article  MathSciNet  Google Scholar 

  57. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. In: LICS 1991, pp. 214–225. IEEP Press (1991)

    Google Scholar 

  58. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)

    Article  MathSciNet  Google Scholar 

  59. Krob, D.: A complete system of B-rational identities. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 60–73. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  60. Krob, D.: Complete systems of B-rational identities. Theor. Comput. Sci. 89, 207–343 (1991)

    Article  MathSciNet  Google Scholar 

  61. Krohn, K., Rhodes, J.L.: Algebraic theory of machines, I, principles of finite semigroups and machines. Trans. Am. Math. Soc. 116, 450–464 (1965)

    Article  MathSciNet  Google Scholar 

  62. Lawvere, F.W.: Functorial semantics of algebraic theories. Proc. Nat. Acad. Sci. (USA) 50, 869–872 (1963)

    Article  MathSciNet  Google Scholar 

  63. Lehmann, D., Smyth, M.B.: Algebraic specification of data types: a synthetic approach. Math. Sys. Theory 14, 97–139 (1981)

    Article  MathSciNet  Google Scholar 

  64. Milner, R.: Communication and Concurrency. Prentice-Hall, New York (1989)

    Google Scholar 

  65. Niwinski, D.: Equational \(\mu \)-calculus. In: Skowron, A. (ed.) Computation Theory. LNCS, vol. 208, pp. 169–176. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  66. Niwinski, D.: On fixed-point clones (extended abstract). In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 464–473. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

  67. Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Theoretical Computer Science. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  68. Plotkin, G.: Domains. The Pisa notes. The University of Edinburgh, Edinburgh (1983)

    Google Scholar 

  69. Pratt, V.: Action logic and pure induction. In: van Eijck, J. (ed.) Logics in AI 1990. LNCS, vol. 478, pp. 97–120. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  70. Santocanale, L.: On the equational definition of the least prefixed point. Theor. Comput. Sci. 295, 341–370 (2003)

    Article  MathSciNet  Google Scholar 

  71. Simpson, A.K., Plotkin, G.D.: Complete axioms for categorical fixed-point operators. In: LICS 2000, pp. 30–41. IEEE Press (2000)

    Google Scholar 

  72. Wagner, E.G., Bloom, S.L., Thatcher, J.W.: Why algebraic theories. In: Algebraic Methods in Semantics, pp. 607–634. Cambridge University Press, New York (1986)

    Google Scholar 

  73. Wright, J.B., Thatcher, J.W., Wagner, E.G., Goguen, J.A.: Rational algebraic theories and fixed-point solutions. In: FOCS 1976, pp. 147–158. IEEE Press (1976)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Szeged, Szeged, Hungary

    Zoltán Ésik

Authors
  1. Zoltán Ésik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zoltán Ésik .

Editor information

Editors and Affiliations

  1. Università di Roma "Tor Vergata", Rome, Italy

    Giuseppe F Italiano

  2. Università degli Studi di Milano, Milan, Italy

    Giovanni Pighizzini

  3. University of Edinburgh, Edinburgh, United Kingdom

    Donald T. Sannella

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ésik, Z. (2015). Equational Properties of Fixed Point Operations in Cartesian Categories: An Overview. In: Italiano, G., Pighizzini, G., Sannella, D. (eds) Mathematical Foundations of Computer Science 2015. MFCS 2015. Lecture Notes in Computer Science(), vol 9234. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48057-1_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48057-1_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48056-4

  • Online ISBN: 978-3-662-48057-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation