Skip to main content
SpringerLink
Log in

Axiomatizing the Least Fixed Point Operation and Binary Supremum

  • Conference paper
  • First Online:
Computer Science Logic (CSL 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1862))

Included in the following conference series:

Abstract

The equational properties of the least fixed point operation on (ω-)continuous functions on (ω-)complete partially ordered sets are captured by the axioms of iteration algebras, or iteration theories. We show that the equational laws of the binary supremum operation in conjunction with the least fixed point operation on (ω-)continuous functions on (ω -)complete semilattices have a finite axiomatization over the equations of iteration algebras. As a byproduct of this relative axiomatizability result, we obtain complete infinite equational, and finite implicational axiomatizations.

Partially supported by grant no. FKFP 247/1999 from the Ministry of Education of Hungary and grant no. T30511 from the National Foundation of Hungary for Scientific Research.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Aceto, W.J. Fokkink and A. Ingólfsdóttir, A menagerie of non-finitely based process semantics over BPA*: from ready simulation to completed traces, Math. Struct. Comput. Sci., 8(1998), 193–230.

    Article  MATH  Google Scholar 

  2. L. Aceto, W.J. Fokkink and A. Ingólfsdóttir, On a question of A. Salomaa: The equational theory of regular expressions over a singleton alphabet is not finitely based, Theoret. Comput. Sci., 209(1998), 163–178.

    Article  MATH  MathSciNet  Google Scholar 

  3. J.W. De Bakker and D. Scott, A theory of programs, IBM Seminar, Vienna, 1969.

    Google Scholar 

  4. J. Balcazar, J. Gabarro and M. Santha, Deciding bisimilarity is P-complete, Formal Aspects of Computing, 4(1992), 638–648.

    Article  MATH  Google Scholar 

  5. H. Bekić, Definable operations in general algebras, and the theory of automata and flowcharts, Technical Report, IBM Laboratory, Vienna, 1969.

    Google Scholar 

  6. D. Benson and J. Tiuryn, Fixed points in free process algebras, Theoret. Comput. Sci., 63(1989), 275–294.

    Article  MATH  MathSciNet  Google Scholar 

  7. S.L. Bloom, Varieties of ordered algebras, J. Comput. System Sci., 13(1976), 200–212.

    MATH  MathSciNet  Google Scholar 

  8. S.L. Bloom and Z. Ésik, Iteration Theories, Springer-Verlag, 1993.

    Google Scholar 

  9. S.L. Bloom and Z. Ésik, The equational logic of fixed points, Theoret. Comput. Sci., 179(1997), 1–60.

    Article  MATH  MathSciNet  Google Scholar 

  10. J.H. Conway, Regular Algebra and Finite Machines, Chapman and Hall, London, 1971.

    MATH  Google Scholar 

  11. F. Corradini, R. De Nicola and A. Labella, Tree morphisms and bisimulations, in: Proc. MFCS’98 Workshop on Concurrency, ENTCS, 18(1998).

    Google Scholar 

  12. F. Corradini, R. De Nicola and A. Labella, A finite axiomatization of nondeterministic regular expressions, Theoret. Inform. Appl., 33(1999), 447–465.

    Article  MATH  Google Scholar 

  13. F. Corradini, R. De Nicola and A. Labella, Models of nondeterministic regular expressions. J. Comput. Sys. Sci., 59:412–449, 1999.

    Article  MATH  Google Scholar 

  14. Z. Ésik, Completeness of Park induction, Theoret. Comput. Sci., 177(1997), 217–283.

    Article  MATH  MathSciNet  Google Scholar 

  15. Z. Ésik, Group axioms for iteration, Inform. and Comput., 148(1999), 131–180.

    Article  MATH  MathSciNet  Google Scholar 

  16. W. Fokkink and H. Zantema, Basic process algebra with iteration: Completeness of its equational axioms. Computer Journal, 37(1994), 259–267.

    Article  Google Scholar 

  17. R.J.H. van Glabbeek, The linear time-branching time spectrum, Chapter 1 in: Comparative Concurrency Semantics and Refinement of Actions, R.J.H. van Glabbeek, CWI TRACT 109, 1996.

    Google Scholar 

  18. C.C. Gunter, Semantics of Programming Languages, MIT Press, 1992.

    Google Scholar 

  19. P.C. Kanellakis and S.A. Smolka, CCS expressions, finite state processes and three problems of equivalence, Inform. and Comput., 86(1990), 43–68.

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  22. R. Milner, A complete inference system for a class of regular behaviours, J. Comput. Syst. Sci., 28(1984), 439–466.

    Article  MATH  MathSciNet  Google Scholar 

  23. R. Milner, Communication and Concurrency, Prentice-Hall, 1989.

    Google Scholar 

  24. D.M.R. Park, Fixpoint induction and proofs of program properties, in: Machine Intelligence 5, D. Michie and B. Meltzer, Eds., Edinburgh Univ. Press, 1970, 59–78.

    Google Scholar 

  25. D.M.R. Park, Concurrency and automata on infinite sequences, in: Proc. GI Conference, P. Deussen, Ed., LNCS104, Springer-Verlag, 1981, 167–183.

    Google Scholar 

  26. A. Salomaa, Two complete axiom systems for the algebra of regular events. J. Assoc. Comput. Mach., 13(1966), 158–169.

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Szeged, P.O.B. 652, 6701, Szeged, Hungary

    Zoltán Ésik

Authors
  1. Zoltán Ésik
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Department of Biology, Boston College, Fulton Hall 410B, Chestnut Hill, MA, 02467, USA

    Peter G. Clote

  2. Mathematisches Institut, Ludwig-Maximilian-Universität München, Theresienstr. 39, 80333, München, Germany

    Helmut Schwichtenberg

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ésik, Z. (2000). Axiomatizing the Least Fixed Point Operation and Binary Supremum. In: Clote, P.G., Schwichtenberg, H. (eds) Computer Science Logic. CSL 2000. Lecture Notes in Computer Science, vol 1862. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44622-2_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-44622-2_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67895-3

  • Online ISBN: 978-3-540-44622-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation