Set constraint
{{No footnotes|date=November 2024}}
File:SetConstraintsAbstractInterpretation svg.svg of the Collatz algorithm]]
In mathematics and theoretical computer science, a set constraint is an equation or an inequation between sets of terms.
Similar to systems of (in)equations between numbers, methods are studied for solving systems of set constraints.
Different approaches admit different operators (like "∪", "∩", "\", and function application)If f is an n-ary function symbol admitted in a term, then "f(E1,...,En)" is a set expression denoting the set { f(t1,...,tn) : t1∈E1 and ... and tn∈En }, where E1,...,En are set expressions in turn. on sets and different (in)equation relations (like "=", "⊆", and "⊈") between set expressions.
Systems of set constraints are useful to describe (in particular infinite) sets of ground terms.This is similar to describing e.g. a rational number as a solution to an equation a⋅x + b = 0, with integer coefficients a, b.
They arise in program analysis, abstract interpretation, and type inference.
Relation to regular tree grammars
Each regular tree grammar can be systematically transformed into a system of set inclusions such that its minimal solution corresponds to the tree language of the grammar.
For example, the grammar (terminal and nonterminal symbols indicated by lower and upper case initials, respectively) with the rules
:
| BoolG | → false |
| BoolG | → true |
| BListG | → nil |
| BListG | → cons(BoolG,BListG) |
| BList1G | → cons(true,BListG) |
| BList1G | → cons(false,BList1G) |
is transformed to the set inclusion system (constants and variables indicated by lower and upper case initials, respectively):
:
| BoolS | ⊇ false |
| BoolS | ⊇ true |
| BListS | ⊇ nil |
| BListS | ⊇ cons(BoolS,BListS) |
| BList1S | ⊇ cons(true,BListS) |
| BList1S | ⊇ cons(false,BList1S) |
This system has a minimal solution, viz. ("L(N)" denoting the tree language corresponding to the nonterminal N in the above tree grammar):
:
| BoolS | = L(BoolG) | = { false, true } |
| BListS | = L(BListG) | = { nil, cons(false,nil), cons(true,nil), cons(false,cons(false,nil)), ... } |
| BList1S | = L(BList1G) | = { nil, cons(true,nil), cons(true,cons(false,nil)),... } |
The maximal solution of the system is trivial; it assigns the set of all terms to every variable.
Literature
- {{cite tech report| author=Aiken, A.| title=Set Constraints: Results, Applications and Future Directions| year=1995| institution=Univ. Berkeley| url=http://citeseer.uark.edu:8080/citeseerx/viewdoc/summary;jsessionid=01CAFC5839497EE6030F707B5B5C9CAA?doi=10.1.1.47.537}}
- {{cite tech report| author=Aiken, A., Kozen, D., Vardi, M., Wimmers, E.L.| title=The Complexity of Set Constraints|date=May 1993| number=93–1352| institution=Computer Science Department, Cornell University| url=http://theory.stanford.edu/~aiken/publications/papers/csl93.ps}}
- {{cite book| author=Aiken, A., Kozen, D., Vardi, M., Wimmers, E.L.| chapter=The Complexity of Set Constraints| title=Computer Science Logic'93| year=1994| volume=832| pages=1–17| publisher=Springer| series=LNCS}}
- {{cite book| author=Aiken, A., Wimmers, E.L.| chapter=Solving Systems of Set Constraints (Extended Abstract)| title=Seventh Annual IEEE Symposium on Logic in Computer Science| year=1992| pages=329–340}}
- {{cite tech report| author=Bachmair, Leo, Ganzinger, Harald, Waldmann, Uwe| title=Set Constraints are the Monadic Class| year=1992| number=MPI-I-92-240| pages=13| institution=Max-Planck-Institut für Informatik| citeseerx=10.1.1.32.3739}}
- {{cite book| author=Bachmair, Leo, Ganzinger, Harald, Waldmann, Uwe| chapter=Set Constraints are the Monadic Class| title=Eight Annual IEEE Symposium on Logic in Computer Science| year=1993| pages=75–83}}
- {{cite book| author=Charatonik, W.| chapter=Set Constraints in Some Equational Theories| title=Proc. 1st Int. Conf. on Constraints in Computational Logics (CCL)|date=Sep 1994| volume=845| pages=304–319| publisher=Springer| series=LNCS}}
- {{cite journal |first1=Witold |last1=Charatonik |first2=Andreas |last2=Podelski |title=Set Constraints with Intersection| journal=Information and Computation| year=2002| volume=179|issue=2 | pages=213–229| doi=10.1006/inco.2001.2952|doi-access=free}}
- {{cite book| author=Charatonik, W., Podelski, A.| title=Co-definite Set Constraints| year=1998| pages=211–225| publisher=Springer-Verlag| editor=Tobias Nipkow| editor-link=Tobias Nipkow| series=LNCS 1379}}
- {{cite book| author=Charatonik, W., Talbot, J.-M.| title=Atomic Set Constraints with Projection| year=2002| pages=311–325| publisher=Springer| editor=Tison, S.| series=LNCS 2378}}
- {{cite book| author=Gilleron, R., Tison, S., Tommasi, M.| chapter=Solving Systems of Set Constraints using Tree Automata| title=10th Annual Symposium on Theoretical Aspects of Computer Science| year=1993| volume=665| pages=505–514| publisher=Springer| series=LNCS}}
- {{cite book| author=Heintze, N., Jaffar, J.| chapter=A Decision Procedure for a Class of Set Constraints (Extended Abstract)| title=Fifth Annual IEEE Symposium on Logic in Computer Science| year=1990| pages=42–51}}
- {{cite tech report| author=Heintze, N., Jaffar, J.| title=A Decision Procedure for a Class of Set Constraints|date=Feb 1991| institution=School of Computer Science, Carnegie Mellon University}}
- {{cite book| author=Kozen, D.| chapter=Logical Aspects of Set Constraints| title=Computer Science Logic'93| year=1993| volume=832| pages=175–188| series=LNCS| chapter-url=http://www.cs.cornell.edu/~kozen/papers/lasc.pdf}}
- {{cite book| author=Kozen, D.| chapter=Set Constraints and Logic Programming| title=CCL| year=1994| volume=845| series=LNCS}}
- {{cite journal| author=Dexter Kozen| title=Set Constraints and Logic Programming| journal=Information and Computation| year=1998| volume=142| pages=2–25| doi=10.1006/inco.1997.2694| doi-access=free}}
- {{cite book| author=Uribe, T.E.| chapter=Sorted Unification Using Set Constraints| title=Proc. CADE–11| year=1992| volume=607| pages=163–177| series=LNCS |chapter-url=http://theory.stanford.edu/~uribe/papers/unification.ps.Z}}
=Literature on negative constraints=
- {{cite tech report| author=Aiken, A., Kozen, D., Wimmers, E.L.| title=Decidability of Systems of Set Constraints with Negative Constraints|date=Jun 1993| number=93–1362| institution=Computer Science Department, Cornell University |url=http://theory.stanford.edu/~aiken/publications/papers/ic95.ps}}
- {{cite book| author=Charatonik, W., Pacholski, L.| chapter=Negative Set Constraints with Equality| title=Ninth Annual IEEE Symposium on Logic in Computer Science|date=Jul 1994| pages=128–136}}
- {{cite book|author1=R. Gilleron |author2=S. Tison |author3=M. Tommasi | chapter=Solving Systems of Set Constraints with Negated Subset Relationships| title=Proceedings of the 34th Symp. on Foundations of Computer Science| year=1993| pages=372–380}}
- {{cite tech report| author=Gilleron, R., Tison, S., Tommasi, M.| title=Solving Systems of Set Constraints with Negated Subset Relationships| year=1993| number=IT 247| institution=Laboratoire d'Informatique Fondamentale de Lille}}
- {{cite tech report| author=Stefansson, K.| title=Systems of Set Constraints with Negative Constraints are NEXPTIME-Complete|date=Aug 1993| number=93–1380| institution=Computer Science Department, Cornell University}}
- {{cite book| author=Stefansson, K.| chapter=Systems of Set Constraints with Negative Constraints are NEXPTIME-Complete| title=Ninth Annual IEEE Symposium on Logic in Computer Science| year=1994| pages=137–141}}