Skip to main content

Set constraints in some equational theories

  • Conference paper
  • First Online:

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

Abstract

In this paper we start studies of set constraints in the environment given by equational specifications. We show that in case of associativity (i.e. in free monoids) as well as in case of associativity and commutativity (i.e. in commutative monoids) the problem of consistency of systems of set constraints is undecidable, and in linear non-erasing shallow theories it is NEXPTIME-complete.

This research was partially supported by KBN grants 2 1197 91 01 and 8 S503 022 07.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Aiken, D. Kozen, M. Vardi, and E. L. Wimmers. The complexity of set constraints. Technical Report 93-1352, Computer Science Department, Cornell University, May 1993.

    Google Scholar 

  2. A. Aiken, D. Kozen, and E. L. Wimmers. Decidability of systems of set constraints with negative constraints. Technical Report 93-1362, Computer Science Department, Cornell University, June 1993.

    Google Scholar 

  3. A. Aiken and B. Murphy. Implementing regular tree expressions. In ACM Conference on Functional Programming Languages and Computer Architecture, pages 427–447, August 1991.

    Google Scholar 

  4. A. Aiken and B. Murphy. Static type inference in a dynamically typed language. In Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 279–290, January 1991.

    Google Scholar 

  5. A. Aiken and E. L. Wimmers. Solving systems of set constraints (extended abstract). In Seventh Annual IEEE Symposium on Logic in Computer Science, pages 329–340, 1992.

    Google Scholar 

  6. L. Bachmair, H. Ganzinger, and U. Waldmann. Set constraints are the monadic class. In Eighth Annual IEEE Symposium on Logic in Computer Science, pages 75–83, 1993.

    Google Scholar 

  7. W. Charatonik and L. Pacholski. Negative set constraints with equality: an easy proof of decidability. In Ninth Annual IEEE Symposium on Logic in Computer Science, 1994.

    Google Scholar 

  8. A. Colmerauer. An introduction to PROLOG III. Communications of the ACM, 33:69–90, 1990.

    Google Scholar 

  9. H. Comon, M. Haberstrau, and J.-P. Jouannaud. Decidable problems in shallow equational theories (extended abstract). In Seventh Annual IEEE Symposium on Logic in Computer Science, pages 255–265, 1992.

    Google Scholar 

  10. R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints using tree automata. In 10th Annual Symposium on Theoretical Aspects of Computer Science, LNCS 665, pages 505–514. Springer-Verlag, 1993.

    Google Scholar 

  11. R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints with negated subset relationships. In Proceedings of the 34 th Symp. on Foundations of Computer Science, pages 372–380, 1993. A full version Technical report IT 247, Laboratoire d'Informatique Fondamentale de Lille.

    Google Scholar 

  12. N. Heintze. Set based analysis and arithmetic. Technical Report CMU-CS-93-193, School of Computer Science, Carnegie Mellon University, July 1993.

    Google Scholar 

  13. N. Heintze. Set constraints in program analysis. Draft manuscript, July 1993.

    Google Scholar 

  14. N. Heintze and J. Jaffar. A decision procedure for a class of set constraints (extended abstract). In Fifth Annual IEEE Symposium on Logic in Computer Science, pages 42–51, 1990.

    Google Scholar 

  15. N. Heintze and J. Jaffar. A finite presentation theorem for approximating logic programs. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 197–209, January 1990.

    Google Scholar 

  16. J. E. Hopcroft and J. D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley Publishing Company, Inc., 1979.

    Google Scholar 

  17. N. D. Jones and S. S. Muchnick. Flow analysis and optimization of lisp-like structures. In Sixth Annual ACM Symposium on Principles of Programming Languages, pages 244–256, January 1979.

    Google Scholar 

  18. H. R. Lewis. Complexity results for classes of quantificational formulas. Journal of Computer and System Sciences, 21:317–353, 1980.

    Google Scholar 

  19. P. Mishra and U. Reddy. Declaration-free type checking. In Twelfth Annual ACM Symposium on the Principles of Programming Languages, pages 7–21, 1985.

    Google Scholar 

  20. J. C. Reynolds. Automatic computation of data set definitions. Information Processing, 68:456–461, 1969.

    Google Scholar 

  21. J. Young and P. O'Keefe. Experience with a type evaluator. In D. Bjørner, A. P. Ershov, and N. D. Jones, editors, Partial Evaluation and Mixed Computation, pages 573–581. North-Holland, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Jean-Pierre Jouannaud

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Charatonik, W. (1994). Set constraints in some equational theories. In: Jouannaud, JP. (eds) Constraints in Computational Logics. CCL 1994. Lecture Notes in Computer Science, vol 845. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0016862

Download citation

  • DOI: https://doi.org/10.1007/BFb0016862

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58403-2

  • Online ISBN: 978-3-540-48699-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics