Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Set constraints: A pearl in research on constraints

  • Tutorial
  • Conference paper
  • First Online:
Principles and Practice of Constraint Programming-CP97 (CP 1997)

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

Abstract

The topic of set constraints is a pearl among the research topics on constraints. It combines theoretical investigations (ranging from logical expressiveness, decidability, algorithms and complexity analysis to program semantics and domain theory) with practical experiments in building systems for program analysis, addressing questions like implementation issues and scalability. The research has its direct applications in type inference, optimization and verification of imperative, functional, logic and reactive programs.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. W. Ackermann. Solvable Cases of the Decision Problem. North-Holland, Amsterdam, 1954.

    Google Scholar 

  2. A. Aiken. Set constraints: Results, applications and future directions. In Proceedings of the Workshop on Principles and Practice of Constraint Programming, LNCS 874, pages 326–335. Springer-Verlag, 1994.

    Google Scholar 

  3. A. Aiken, D. Kozen, M. Y. Vardi, and E. L. Wimmers. The complexity of set constraints. In 1993 Conference on Computer Science Logic, LNCS 832, pages 1–17. Springer-Verlag, Sept. 1993.

    Google Scholar 

  4. A. Aiken, D. Kozen, and E. L. Wimmers. Decidability of systems of set constraints with negative constraints. Information and Computation, 122(1):30–44, Oct. 1995.

    Google Scholar 

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

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

  7. A. Aiken and E. Wimmers. Type inclusion constraints and type inference. In Proceedings of the 1993 Conference on Functional Programming Languages and Computer Architecture, pages 31–41, Copenhagen, Denmark, June 1993.

    Google Scholar 

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

  9. A. Aiken, E. L. Wimmers, and T. Lakshman. Soft typing with conditional types. In Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, Oregon, Jan. 1994.

    Google Scholar 

  10. D. Arden. Delayed logic and finite state machines. In Proceedings of the 2nd Annual Symposium on Switching Circuit Theory and Logical Design, pages 133—151, 1961.

    Google Scholar 

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

  12. C. Beeri, S. Nagvi, O. Schmueli, and S. Tsur. Set constructors in a logic database language. The Journal of Logic Programming, pages 181–232, 1991.

    Google Scholar 

  13. S. K. Biswas. A demand-driven set-based analysis. In The 24th ACM Symposium on Principles of Programming Languages POPL '97, pages 372–385, Paris, France, January 1997.

    Google Scholar 

  14. B. Bogaert and S. Tison. Automata with equality tests. Technical Report IT 207, Laboratoire d'Informatique Fondamentale de Lille, 1991.

    Google Scholar 

  15. P. Bruscoli, A. Dovier, E. Pontelli, and G. Rossi. Compiling intensional sets in CLP. In Proceedings of the International Conference on Logic Programming, pages 647–661. The MIT Press, 1994.

    Google Scholar 

  16. J. Brzozowski and E. Leiss. On equations for regular languages, finite automata, and sequential networks. Theorical Computer Science, 10:19–35, 1980.

    Google Scholar 

  17. W. Charatonik. Set constraints in some equational theories. In 1st International Conference Constraints in Computational Logics, LNCS 845, pages 304–319. Springer-Verlag, 1994. Also to appear in Information and Computation.

    Google Scholar 

  18. W. Charatonik. Set constraints in some equational theories. PhD thesis, Polish Academy of Sciences, 1995.

    Google Scholar 

  19. W. Charatonik and L. Pacholski. Negative set constraints with equality. In Ninth Annual IEEE Symposium on Logic in Computer Science, pages 128–136, 1994.

    Google Scholar 

  20. W. Charatonik and L. Pacholski. Set constraints with projections are in NEXPTIME. In Proceedings of the 35 th Symposium on Foundations of Computer Science, pages 642–653, 1994.

    Google Scholar 

  21. W. Charatonik and L. Pacholski. Negative set constraints: an easy proof of decidability. Technical Report MPI-I-93-265, Max-Planck Institute für Informatik, December 1993.

    Google Scholar 

  22. W. Charatonik and A. Podelski. The independence property of a class of set constraints. In Conference on Principles and Practice of Constraint Programming, LNCS 1118, pages 76–90. Springer-Verlag, 1996.

    Google Scholar 

  23. W. Charatonik and A. Podelski. Set constraints for greatest models. Technical Report MPI-I-97-2-004, Max-Planck-Institut fiir Informatik, April 1997. http://www.mpi-sb.mpg.de/-podelski/papers/greatest.html.

    Google Scholar 

  24. W. Charatonik and A. Podelski. Set constraints with intersection. In G. Winskel, editor, Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 362–372. IEEE, June 1997.

    Google Scholar 

  25. A. Cheng and D. Kozen. A complete Gentzen-style axiomatization for set constraints. In ICALP: Annual International Colloquium on Automata, Languages and Programming, LNCS 1099, 1996.

    Google Scholar 

  26. P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Proc. POPL '92, pages 83–94. ACM Press, 1992.

    Google Scholar 

  27. P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Record of FPCA '95-Conference on Functional Programming and Computer Architecture, pages 170–181, La Jolla, California, USA, 25–28 June 1995. SIGPLAN/SIGARCH/WG2.8, ACM Press, New York, USA.

    Google Scholar 

  28. P. W. Dart and J. Zobel. A regular type language for logic programs, chapter 5, pages 157–188. MIT Press, 1992.

    Google Scholar 

  29. P. Devienne, J.-M. Talbot, and S. Tison. Solving classes of set constraints with tree automata. In G. Smolka, editor, Proceedings of the Third International Conference on Principles and Practice of Constraint Programming — CP97, LNCS, Berlin, Germany, October 1997. Springer-Verlag. To appear.

    Google Scholar 

  30. A. Dovier. Computable Set Theory and Logic Programming. PhD thesis, Dipartimento di Informatica, Universitá di Pisa, 1996.

    Google Scholar 

  31. A. Dovier and G. Rossi. Embedding Extensional Finite Sets in CLP. In International Logic Programming Symposium, 1993.

    Google Scholar 

  32. M. Fiihndrich and A. Aiken. Making set-constraint based program analyses scale. Computer Science Division Tech Report 96-917, Computer Science Division, University of California at Berkeley, September 1996. Also presented at the Workshop on Set Constraints, Cambridge MA, August 1996.

    Google Scholar 

  33. J. S. Foster. CLP(SC): Implementation and efficiency considerations. workshop on set constraints. Available at http://http.cs.berkeley.edu/~jfoster/. Presented at the Workshop on Set Constraints, Cambridge MA, August 1996, August 1996.

    Google Scholar 

  34. J. S. Foster, M. Fähndrich, and A. Aiken. Flow-insensitive points-to analysis with term and set constraints. Computer Science Division Tech Report 97-964,, University of California at Berkeley, September 1997. Also presented at the Workshop on Set Constraints, Cambridge MA, August 1996

    Google Scholar 

  35. T. Frühwirth, E. Shapiro, M. Y. Vardi, and E. Yardeni. Logic programs as types for logic programs. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 300–309, July 1991.

    Google Scholar 

  36. J. P. Gallagher, D. Boulanger, and H. Saglam. Practical model-based static analysis for definite logic programs. In Proceedings of the 1995 International Symposium on Logic Programming, pages 351–368.

    Google Scholar 

  37. J. P. Gallagher and L. Lafave. Regular approximation of computation paths in logic and functional languages. In Proceedings of the Dagstuhl Workshop on Partial Evaluation, pages 1–16. Springer-Verlag, February 1996.

    Google Scholar 

  38. K. L. S. Gasser, F. Nielson, and H. R. Nielson. Systematic realisation of control flow analyses for CML. In Proceedings of ICFP'97, pages 38–51. ACM Press, 1997.

    Google Scholar 

  39. F. Gécseg and M. Steinby. Tree Automata. Akademiai Kiado, Budapest, 1984.

    Google Scholar 

  40. C. Gervet. Conjunto: Constraint logic programming with finite set domains. In M. Bruynooghe, editor, Proceedings of the International Logic Programming Symposium, pages 339–358, 1994.

    Google Scholar 

  41. C. Gervet. Set Intervals in Constraint-Logic Programming: Definition and Implementation of a Language. PhD thesis, Université de Franche-Compté, 1995. European Thesis.

    Google Scholar 

  42. C. Gervet. Interval Propagation to Reason about Sets: Definition and Implementation of a Practical Language. Constraints, l(2), 1997.

    Google Scholar 

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

  44. R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints with negated subset relationships. In Proceedings of the 34th Symp. on Foundations of Computer Science, pages 372–380, 1993. Full version in [45].

    Google Scholar 

  45. R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints with negated subset relationships. Technical Report IT 247, Laboratoire d'Informatique Fondamentale de Lille, 1993.

    Google Scholar 

  46. R. Gilleron, S. Tison, and M. Tommasi. Set constraints and automata. Technical Report IT 292, Laboratoire d'Informatique Fondamentale de Lille, 1996.

    Google Scholar 

  47. R. Gilleron, S. Tison, and M. Tommassi. Some new decidability results on positive and negative set constraints. In 1st International Conference Constraints in Computational Logics, LNCS 845, pages 336–351. Springer-Verlag, 1994.

    Google Scholar 

  48. N. Heintze. Set based program analysis. PhD thesis, School of Computer Science, Carnegie Mellon University, 1992.

    Google Scholar 

  49. N. Heintze. Set based analysis of arithmetic. Draft manuscript, July 1993.

    Google Scholar 

  50. N. Heintze. Set based analysis of ML programs. Technical Report CMU-CS-93193, School of Computer Science, Carnegie Mellon University, July 1993.

    Google Scholar 

  51. N. Heintze. Set based analysis of ML programs. In Conference on Lisp and Functional Programming, pages 306–317. ACM, 1994. Preliminary version in [50].

    Google Scholar 

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

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

  54. N. Heintze and J. Jaffar. A finite presentation theorem for approximating logic programs. Technical report, School of Computer Science, Carnegie Mellon University, Aug. 1990. 66 pages.

    Google Scholar 

  55. N. Heintze and J. Jaffar. An engine for logic program analysis. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 318–328, 1992.

    Google Scholar 

  56. N. Heintze and J. Jaffar. Semantic Types for Logic Programs, chapter 4, pages 141–156. MIT Press, 1992.

    Google Scholar 

  57. N. Heintze and D. McAllester. Linear-time subtransitive control-flow analysis. In ACM Conference on Programming Language Design and Implementation, 1997. To appear.

    Google Scholar 

  58. N. Heintze and D. McAllester. On the cubic bottleneck in subtyping and flow analysis. In G. Winskel, editor, Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 342–351. IEEE, June 1997.

    Google Scholar 

  59. ILOG. ILOG SOLVER 3.2 user manual.www.ilog.com.

    Google Scholar 

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

  61. W. Joyner. Resolution strategies as decision procedures. Journal of the Association for Computing Machinery, 23(3):398–417, 1979.

    Google Scholar 

  62. D. Kozen. Logical aspects of set constraints. In 1993 Conference on Computer Science Logic, LNCS 832, pages 175–188. Springer-Verlag, Sept. 1993.

    Google Scholar 

  63. D. Kozen. Set constraints and logic programming (abstract). In 1st International Conference Constraints in Computational Logics, LNCS 845. Springer-Verlag, 1994. Also to appear in Information and Computation.

    Google Scholar 

  64. D. Kozen. Rational spaces and set constraints. In TAPSOFT: 6th International Joint Conference on Theory and Practice of Software Development, LNCS 915, pages 42–61. Springer-Verlag, 1995.

    Google Scholar 

  65. D. Kozen. Rational spaces and set constraints. Theoretical Computer Science, 167(1-2):73–94, October 1996.

    Google Scholar 

  66. G. Kuper. Logic programming with sets. New York, NY, 1990. Academic Press.

    Google Scholar 

  67. B. Legeard and E. Legros. Short Overview of the CLPS System. 1991.

    Google Scholar 

  68. L. Löwenheim. Über Möglichkeiten im Relativkalkül. Mathematische Annalen, 76:228–251, 1915.

    Google Scholar 

  69. D. McAllester and N. Heintze. On the complexity of set-based analysis. www.ai.mit.edu/people/dam/setbased.ps.

    Google Scholar 

  70. D. A. McAllester, R. Givan, C. Witty, and D. Kozen. Tarskian set constraints. In Proceedings, 11 th Annual IEEE Symposium on Logic in Computer Science, pages 138–147, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.

    Google Scholar 

  71. P. Mishra. Towards a theory of types in Prolog. In IEEE International Symposium on Logic Programming, pages 289–298, 1984.

    Google Scholar 

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

  73. M. Müller. Type Analysis for a Higher-Order Concurrent Constraint Language. PhD thesis, Universität des Saarlandes, Technische Fakultät, 66041 Saarbrücken, Germany, expected 1997.

    Google Scholar 

  74. M. Müller, J. Niehren, and A. Podelski. Inclusion constraints over non-empty sets of trees. In M. Bidoit and M. Dauchet, editors, Proceedings of the 9th International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 1214 of LNCS, pages 345–356, Berlin, April 1997. Springer-Verlag.

    Google Scholar 

  75. M. Müller, J. Niehren, and A. Podelski. Ordering constraints over feature trees. In G. Smolka, editor, Proceedings of the Third International Conference on Principles and Practice of Constraint Programming — CP97, LNCS, Berlin, Germany, October 1997. Springer-Verlag. To appear.

    Google Scholar 

  76. T. Müller and M. Müller. Finite set constraints in Oz. In 13. Workshop Logische Programmierung, Technische Universität München, September 1997. to appear.

    Google Scholar 

  77. M. Nivat and A. Podelski. Tree Automata and Languages. North-Holland, Amsterdam, 1992.

    Google Scholar 

  78. J. Palsberg and O'Keefe. A type system equivalent to flow analysis. In Symposium of Principles of Programming Languages, pages 367–378. ACM, 1995.

    Google Scholar 

  79. J. Palsberg and M. Schwartzbach. Safety analysis versus type inference. Information and Computation, 118(1):128–141, April 1995.

    Google Scholar 

  80. A. Podelski, W. Charatonik, and M. Müller. Set-based analysis of reactive infinite-state systems. Submitted for publication, 1997.

    Google Scholar 

  81. J. F. Puget. Finite Set Intervals. In Proceedings of the Second International Workshop on Set Constraints, Cambridge, Massachusetts, 1996.

    Google Scholar 

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

    Google Scholar 

  83. H. Seidl. Haskell overloading is DEXPTIME-complete. Information Processing Letters, 52:57–60, 1994.

    Google Scholar 

  84. F. Seynhave, M. Tommasi, and R. Treinen. Grid structures and undecidable constraint theories. In M. Bidoit and M. Dauchet, editors, Proceedings of the 9th International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 1214 of LNCS, pages 357–368, Berlin, April 1997. Springer-Verlag.

    Google Scholar 

  85. G. Slutzki. Alternating tree automata. Theoretical Computer Science, 41:305–318, 1985.

    Google Scholar 

  86. G. Smolka. The Oz programming model. In Volume 1000 of Lecture Notes in Computer Science, 1995.

    Google Scholar 

  87. K. Stefansson. Systems of set constraints with negative constraints are NEXPTIME-complete. In Ninth Annual IEEE Symposium on Logic in Computer Science, pages 137–141, 1994.

    Google Scholar 

  88. F. Stolzenburg. Membership-constraints and complexity in logic programming with sets. In F. Baader and K. U. Schulz, editors, Frontiers in Combining Systems, pages 285–302. Kluwer Academic, Dordrecht, The Netherlands, 1996.

    Google Scholar 

  89. S. Thatte. Type inference with partial types. In 15th International Colloquium on Automata, Languages and Programming, volume 317 of LNCS, pages 615–629. Springer-Verlag, 1988.

    Google Scholar 

  90. W. Thomas. Handbook of Theoretical Computer Science, volume B, chapter Automata on Infinite Objects, pages 134–191. Elsevier, 1990.

    Google Scholar 

  91. T. E. Uribe. Sorted unification using set constraints. In 11th International Conference on Automated Deduction, LNAI 607, pages 163–177. Springer-Verlag, 1992.

    Google Scholar 

  92. M. Y. Vardi. An automata-theoretic approach to linear-temporal logic. In Logics for Concurrency: Structure versus Automata. LNCS, 1043:238–266, 1996.

    Google Scholar 

  93. M. Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci., 32, 1986.

    Google Scholar 

  94. C. Walinsky. CLP(ΣE *): Constraint Logic Programming with Regular Sets. In Proceedings of the International Conference on Logic Programming, pages 181–190, 1989.

    Google Scholar 

  95. E. Yardeni,, T. Frühwirth, and E. Shapiro. Polymorphically typed logic programs, chapter 2, pages 157–188. MIT Press, 1992.

    Google Scholar 

  96. E. Yardeni. A type system for logic programs. Master's thesis, Weizmann Institute of Science, 1987.

    Google Scholar 

  97. E. Yardeni and E. Shapiro. A type system for logic programs, volume 2, chapter 28, pages 211–244. The MIT Press, 1987.

    Google Scholar 

  98. E. Yardeni and E. Shapiro. A type system for logic programs. Journal of Logic Programming, 10:125–153, 1991. Preliminary version in [97].

    Google Scholar 

  99. 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. Institute of Computer Science, University of Wroclaw, Przesmyckiego 20, PL-51-151, Wroclaw, Poland

    Leszek Pacholski

  2. Max-Planck-Institut für Informatik Im Stadtwald, D-66123, Saarbrücken, Germany

    Andreas Podelski

Authors
  1. Leszek Pacholski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andreas Podelski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Gert Smolka

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pacholski, L., Podelski, A. (1997). Set constraints: A pearl in research on constraints. In: Smolka, G. (eds) Principles and Practice of Constraint Programming-CP97. CP 1997. Lecture Notes in Computer Science, vol 1330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0017466

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63753-0

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation