Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Automata, Languages, and Programming

ICALP 1996: Automata, Languages and Programming pp 134–145Cite as

A complete gentzen-style axiomatization for set constraints

  • Session 3: Logic and Algebra
  • Conference paper
  • First Online:

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

Abstract

Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we provide a Gentzen-style axiomatization for sequents Φ ⊢ Ψ, where Φ and Ψ are finite sets of set constraints, based on the axioms of termset algebra. Sequents of the restricted form Φ ⊢ ⊥ correspond to positive set constraints, and those of the more general form Φ ⊢ Ψ correspond to systems of mixed positive and negative set constraints. We show that the deductive system is (i) complete for the restricted sequents Φ ⊢ ⊥ over standard models, (ii) incomplete for general sequents Φ ⊢ Ψ over standard models, but (iii) complete for general sequents over set-theoretic termset algebras.

Visiting from Aarhus, BRICS, Basic Research in Computer Science, Center of the Danish National Research Foundation.

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. Alexander Aiken, Dexter Kozen, Moshe Vardi, and Edward Wimmers. The complexity of set constraints. In E. Börger, Y. Gurevich, and K. Meinke, editors, Proc. 1993 Conf. Computer Science Logic (CSL'93), volume 832 of Lect. Notes in Comput. Sci., pages 1–17. Eur. Assoc. Comput. Sci. Logic, Springer, September 1993.

    Google Scholar 

  2. Alexander Aiken, Dexter Kozen, and Edward Wimmers. Decidability of systems of set constraints with negative constraints. Infor. and Comput., 122(1):30–44, October 1995.

    Google Scholar 

  3. A. Aiken and B. Murphy. Implementing regular tree expressions. In Proc. 1991 Conf. 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 Proc. 18th Symp. Principles of Programming Languages, pages 279–290. ACM, January 1991.

    Google Scholar 

  5. A. Aiken and E. Wimmers. Solving systems of set constraints. In Proc. 7th Symp. Logic in Computer Science, pages 329–340. IEEE, June 1992.

    Google Scholar 

  6. L. Bachmair, H. Ganzinger, and U. Waldmann. Set constraints are the monadic class. In Proc. 8th Symp. Logic in Computer Science, pages 75–83. IEEE, June 1993.

    Google Scholar 

  7. A. Cheng and D. Kozen. A Complete Gentzen-style Axiomatization for Set Constraints. Tech. Rep. 95-1518, Computer Science Department, Cornell University, May 1995.

    Google Scholar 

  8. A. Colmerauer. PROLOG and infinite trees. In S.-Å. Tärnlund and K. L. Clark, editors, Logic Programming, pages 231–251. Academic Press, January 1982.

    Google Scholar 

  9. Bruno Courcelle. Fundamental properties of infinite trees. Theor. Comput. Sci., 25:95–169, 1983.

    Google Scholar 

  10. W. Charatonik and L. Pacholski. Negative set constraints with equality. In Proc. 9th Symp. Logic in Computer Science, pages 128–136. IEEE, July 1994.

    Google Scholar 

  11. W. Charatonik and L. Pacholski. Set constraints with projections are in NEXPTIME. In Proc. 35th Symp. Foundations of Computer Science, pages 642–653. IEEE, November 1994.

    Google Scholar 

  12. Timothy G. Griffin. An environment for formal systems. Technical Report TR87-846, Cornell University, June 1987.

    Google Scholar 

  13. R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints using tree automata. In Proc. Symp. Theor. Aspects of Comput. Sci., volume 665, pages 505–514. Springer-Verlag Lect. Notes in Comput. Sci., February 1993.

    Google Scholar 

  14. R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints with negated subset relationships. In Proc. 34th Symp. Foundations of Comput. Sci., pages 372–380. IEEE, November 1993.

    Google Scholar 

  15. Nevin Heintze. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, 1993.

    Google Scholar 

  16. N. Heintze and J. Jaffar. A decision procedure for a class of set constraints. In Proc. 5th Symp. Logic in Computer Science, pages 42–51. IEEE, June 1990.

    Google Scholar 

  17. N. Heintze and J. Jaffar. A finite presentation theorem for approximating logic programs. In Proc. 17th Symp. Principles of Programming Languages, pages 197–209. ACM, January 1990.

    Google Scholar 

  18. N. D. Jones and S. S. Muchnick. Flow analysis and optimization of LISP-like structures. In Proc. 6th Symp. Principles of Programming Languages, pages 244–256. ACM, January 1979.

    Google Scholar 

  19. B. Jónsson and A. Tarski. Boolean algebras with operators. Amer. J. Math., 73:891–939, 1951.

    Google Scholar 

  20. B. Jónsson and A. Tarski. Boolean algebras with operators. Amer. J. Math., 74:127–162, 1952.

    Google Scholar 

  21. Dexter Kozen. Logical aspects of set constraints. In E. Börger, Y. Gurevich, and K. Meinke, editors, Proc. 1993 Conf. Computer Science Logic (CSL'93), volume 832 of Lect. Notes in Comput. Sci., pages 175–188. Eur. Assoc. Comput. Sci. Logic, Springer, September 1993.

    Google Scholar 

  22. Dexter Kozen. Set constraints and logic programming (abstract). In J.-P. Jouannaud, editor, Proc. First Conf. Constraints in Computational Logics (CCL'94), volume 845 of Lect. Notes in Comput. Sci., pages 302–303. ESPRIT, Springer, September 1994.

    Google Scholar 

  23. Dexter Kozen. Rational spaces and set constraints. In Peter D. Mosses, Mogens Nielsen, and Michael I. Schwartzbach, editors, Proc. Sixth Int. Joint Conf. Theory and Practice of Software Develop. (TAPSOFT'95), volume 915 of Lect. Notes in Comput. Sci., pages 42–61. Springer, May 1995.

    Google Scholar 

  24. Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. In Proc. 33rd Symp. Found. Comput. Sci., pages 363–371. IEEE, October 1992.

    Google Scholar 

  25. Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. In Proc. 20th Symp. Princip. Programming Lang., pages 419–428. ACM, January 1993.

    Google Scholar 

  26. Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. J. Comput. Syst. Sci., 49(2):306–324, October 1994.

    Google Scholar 

  27. P. Mishra. Towards a theory of types in PROLOG. In Proc. 1st Symp. Logic Programming, pages 289–298. IEEE, 1984.

    Google Scholar 

  28. P. Mishra and U. Reddy. Declaration-free type checking. In Proc. 12th Symp. Principles of Programming Languages, pages 7–21. ACM, 1985.

    Google Scholar 

  29. J. C. Reynolds. Automatic computation of data set definitions. In Information Processing 68, pages 456–461. North-Holland, 1969.

    Google Scholar 

  30. K. Stefánsson. Systems of set constraints with negative constraints are NEXPTIME-complete. In Proc. 9th Symp. Logic in Computer Science, pages 137–141. IEEE, June 1994.

    Google Scholar 

  31. 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

  1. Computer Science Department, Cornell University, 14853, Ithaca, New York, USA

    Allan Cheng & Dexter Kozen

Authors
  1. Allan Cheng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dexter Kozen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Friedhelm Meyer Burkhard Monien

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cheng, A., Kozen, D. (1996). A complete gentzen-style axiomatization for set constraints. In: Meyer, F., Monien, B. (eds) Automata, Languages and Programming. ICALP 1996. Lecture Notes in Computer Science, vol 1099. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61440-0_123

Download citation

  • DOI: https://doi.org/10.1007/3-540-61440-0_123

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61440-1

  • Online ISBN: 978-3-540-68580-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation