Skip to main content
SpringerLink
Log in

The Variable Hierarchy for the Lattice μ-Calculus

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5330))

Abstract

The variable hierarchy problem asks whether every μ-term t is equivalent to a μ-term t′ where the number of fixed-point variables in t′ is bounded by a constant. In this paper we prove that the variable hierarchy of the lattice μ -calculus – whose standard interpretation is over the class of all complete lattices – is infinite, meaning that such a constant does not exist if the μ-terms are built up using the basic lattice operations as well as the least and the greatest fixed point operators. The proof relies on the description of the lattice μ-calculus by means of games and strategies.

Research supported by the Agence Nationale de la Recherche, project SOAPDC.

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. Bloom, S.L., Ésik, Z.: Iteration theories. EATCS Monographs on Theoretical Computer Science. Springer, Berlin (1993)

    Book  MATH  Google Scholar 

  2. Arnold, A., Niwiński, D.: Rudiments of μ-calculus. Studies in Logic and the Foundations of Mathematics, vol. 146. North-Holland, Amsterdam (2001)

    MATH  Google Scholar 

  3. Bradfield, J.C.: The modal mu-calculus alternation hierarchy is strict. Theor. Comput. Sci. 195(2), 133–153 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  4. Arnold, A.: The μ-calculus alternation-depth hierarchy is strict on binary trees. Theor. Inform. Appl. 33(4-5), 329–339 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  5. Santocanale, L.: The alternation hierarchy for the theory of μ-lattices. Theory Appl. Categ. 9, 166–197 (2002)

    MathSciNet  MATH  Google Scholar 

  6. Santocanale, L., Arnold, A.: Ambiguous classes in μ-calculi hierarchies. Theor. Comput. Sci. 333(1-2), 265–296 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  7. Eggan, L.C.: Transition graphs and the star-height of regular events. Mich. Math. J. 10, 385–397 (1963)

    Article  MathSciNet  MATH  Google Scholar 

  8. Braquelaire, J.P., Courcelle, B.: The solutions of two star-height problems for regular trees. Theor. Comput. Sci. 30(2), 205–239 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  9. Berwanger, D., Grädel, E., Lenzi, G.: The variable hierarchy of the μ-calculus is strict. Theory Comput. Syst. 40(4), 437–466 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  10. Blass, A.: A game semantics for linear logic. Ann. Pure Appl. Logic 56(1-3), 183–220 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  11. Nerode, A., Yakhnis, A., Yakhnis, V.: Concurrent programs as strategies in games. In: Moschovakis, Y.N. (ed.) Logic from Computer Science, pp. 405–479. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  12. Abramsky, S., Jagadeesan, R.: Games and full completeness for multiplicative linear logic. J. Symb. Logic 59(2), 543–574 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  13. Joyal, A.: Free lattices, communication and money games. In: Logic and scientific methods. Synthese Lib, vol. 259, pp. 29–68. Kluwer Acad. Publ., Dordrecht (1997)

    Chapter  Google Scholar 

  14. Freese, R.: Free lattices. Math. Surveys and Monographs. vol. 42, AMS (1995)

    Google Scholar 

  15. Joyal, A.: Free bicomplete categories. C. R. Math. Canada 17(5), 219–224 (1995)

    MathSciNet  MATH  Google Scholar 

  16. Cockett, J.R.B., et al.: Finite sum-product logic. Theory Appl. Categ. 8, 63–99 (2001)

    MathSciNet  MATH  Google Scholar 

  17. Santocanale, L.: Free μ-lattices. Jour. of Pure and Applied Algebra 168(2-3), 227–264 (2002)

    Article  MATH  Google Scholar 

  18. Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 357–371. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Arnold, A., Santocanale, L.: Ambiguous classes in the games mgr-calculus hierarchy. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 70–86. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285–309 (1955)

    Article  MathSciNet  MATH  Google Scholar 

  21. Berwanger, D., Grädel, E.: Entanglement – A measure for the complexity of directed graphs with applications to logic and games. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 209–223. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d’Informatique Fondamentale de Marseille, Université de Provence, France

    Walid Belkhir & Luigi Santocanale

Authors
  1. Walid Belkhir
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luigi Santocanale
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Carnegie Mellon University, Doha, Qatar

    Iliano Cervesato

  2. Technische Universität Darmstadt, Germany

    Helmut Veith

  3. University of Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Belkhir, W., Santocanale, L. (2008). The Variable Hierarchy for the Lattice μ-Calculus . In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-89439-1_42

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-89438-4

  • Online ISBN: 978-3-540-89439-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation