Set constraint

Set constraints obtained from abstract interpretation 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)[note 1] 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.[note 2] 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

Literature on negative constraints

Notes

  1. 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) : t1E1 and ... and tnEn }, where E1,...,En are set expressions in turn.
  2. This is similar to describing e.g. a rational number as a solution to an equation ax + b = 0, with integer coefficients a, b.


This article is issued from Wikipedia - version of the 6/5/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.