Advertisement

Set constraints: A pearl in research on constraints

  • Leszek Pacholski
  • Andreas Podelski
Tutorial
Part of the Lecture Notes in Computer Science book series (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.

Keywords

Logic Program Constraint Programming Type Inference Tree Automaton Annual IEEE Symposium 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    W. Ackermann. Solvable Cases of the Decision Problem. North-Holland, Amsterdam, 1954.Google Scholar
  2. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 14.
    B. Bogaert and S. Tison. Automata with equality tests. Technical Report IT 207, Laboratoire d'Informatique Fondamentale de Lille, 1991.Google Scholar
  15. 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. 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. 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. 18.
    W. Charatonik. Set constraints in some equational theories. PhD thesis, Polish Academy of Sciences, 1995.Google Scholar
  19. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 30.
    A. Dovier. Computable Set Theory and Logic Programming. PhD thesis, Dipartimento di Informatica, Universitá di Pisa, 1996.Google Scholar
  31. 31.
    A. Dovier and G. Rossi. Embedding Extensional Finite Sets in CLP. In International Logic Programming Symposium, 1993.Google Scholar
  32. 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. 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. 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 1996Google Scholar
  35. 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. 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. 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. 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. 39.
    F. Gécseg and M. Steinby. Tree Automata. Akademiai Kiado, Budapest, 1984.Google Scholar
  40. 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. 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. 42.
    C. Gervet. Interval Propagation to Reason about Sets: Definition and Implementation of a Practical Language. Constraints, l(2), 1997.Google Scholar
  43. 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. 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. 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. 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. 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. 48.
    N. Heintze. Set based program analysis. PhD thesis, School of Computer Science, Carnegie Mellon University, 1992.Google Scholar
  49. 49.
    N. Heintze. Set based analysis of arithmetic. Draft manuscript, July 1993.Google Scholar
  50. 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. 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. 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. 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. 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. 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. 56.
    N. Heintze and J. Jaffar. Semantic Types for Logic Programs, chapter 4, pages 141–156. MIT Press, 1992.Google Scholar
  57. 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. 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. 59.
    ILOG. ILOG SOLVER 3.2 user manual.www.ilog.com.Google Scholar
  60. 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. 61.
    W. Joyner. Resolution strategies as decision procedures. Journal of the Association for Computing Machinery, 23(3):398–417, 1979.Google Scholar
  62. 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. 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. 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. 65.
    D. Kozen. Rational spaces and set constraints. Theoretical Computer Science, 167(1-2):73–94, October 1996.Google Scholar
  66. 66.
    G. Kuper. Logic programming with sets. New York, NY, 1990. Academic Press.Google Scholar
  67. 67.
    B. Legeard and E. Legros. Short Overview of the CLPS System. 1991.Google Scholar
  68. 68.
    L. Löwenheim. Über Möglichkeiten im Relativkalkül. Mathematische Annalen, 76:228–251, 1915.Google Scholar
  69. 69.
    D. McAllester and N. Heintze. On the complexity of set-based analysis. www.ai.mit.edu/people/dam/setbased.ps.Google Scholar
  70. 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. 71.
    P. Mishra. Towards a theory of types in Prolog. In IEEE International Symposium on Logic Programming, pages 289–298, 1984.Google Scholar
  72. 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. 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. 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. 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. 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. 77.
    M. Nivat and A. Podelski. Tree Automata and Languages. North-Holland, Amsterdam, 1992.Google Scholar
  78. 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. 79.
    J. Palsberg and M. Schwartzbach. Safety analysis versus type inference. Information and Computation, 118(1):128–141, April 1995.Google Scholar
  80. 80.
    A. Podelski, W. Charatonik, and M. Müller. Set-based analysis of reactive infinite-state systems. Submitted for publication, 1997.Google Scholar
  81. 81.
    J. F. Puget. Finite Set Intervals. In Proceedings of the Second International Workshop on Set Constraints, Cambridge, Massachusetts, 1996.Google Scholar
  82. 82.
    J. C. Reynolds. Automatic computation of data set definitions. Information Processing, 68:456–461, 1969.Google Scholar
  83. 83.
    H. Seidl. Haskell overloading is DEXPTIME-complete. Information Processing Letters, 52:57–60, 1994.Google Scholar
  84. 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. 85.
    G. Slutzki. Alternating tree automata. Theoretical Computer Science, 41:305–318, 1985.Google Scholar
  86. 86.
    G. Smolka. The Oz programming model. In Volume 1000 of Lecture Notes in Computer Science, 1995.Google Scholar
  87. 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. 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. 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. 90.
    W. Thomas. Handbook of Theoretical Computer Science, volume B, chapter Automata on Infinite Objects, pages 134–191. Elsevier, 1990.Google Scholar
  91. 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. 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. 93.
    M. Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci., 32, 1986.Google Scholar
  94. 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. 95.
    E. Yardeni,, T. Frühwirth, and E. Shapiro. Polymorphically typed logic programs, chapter 2, pages 157–188. MIT Press, 1992.Google Scholar
  96. 96.
    E. Yardeni. A type system for logic programs. Master's thesis, Weizmann Institute of Science, 1987.Google Scholar
  97. 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. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Leszek Pacholski
    • 1
  • Andreas Podelski
    • 2
  1. 1.Institute of Computer ScienceUniversity of WroclawWroclawPoland
  2. 2.Max-Planck-Institut für Informatik Im StadtwaldSaarbrückenGermany

Personalised recommendations