Set Constraint on:
[Wikipedia]
[Google]
[Amazon]
In mathematics and
In mathematics and theoretical computer science
Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory.
It is difficult to circumsc ...
, 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''(''E''1,...,''E''''n'')" is a set expression denoting the set , where ''E''1,...,''E''''n'' 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 term
In mathematical logic, a ground term of a formal system is a term that does not contain any variables. Similarly, a ground formula is a formula that does not contain any variables.
In first-order logic with identity, the sentence Q(a) \lor P( ...
s.This is similar to describing e.g. a rational number
In mathematics, a rational number is a number that can be expressed as the quotient or fraction of two integers, a numerator and a non-zero denominator . For example, is a rational number, as is every integer (e.g. ). The set of all ra ...
as a solution to an equation ''a''⋅''x'' + ''b'' = 0, with integer
An integer is the number zero (), a positive natural number (, , , etc.) or a negative integer with a minus sign ( −1, −2, −3, etc.). The negative numbers are the additive inverses of the corresponding positive numbers. In the language ...
coefficients ''a'', ''b''.
They arise in program analysis, abstract interpretation, and type inference
Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistics. ...
.
Relation to regular tree grammars
Eachregular tree grammar In theoretical computer science and formal language theory, a regular tree grammar is a formal grammar that describes a set of directed trees, or terms. A regular word grammar can be seen as a special kind of regular tree grammar, describing a se ...
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
:
is transformed to the set inclusion system (constants and variables indicated by lower and upper case initials, respectively):
:
This system has a minimal solution, viz. ("''L''(''N'')" denoting the tree language corresponding to the nonterminal ''N'' in the above tree grammar):
:
The maximal solution of the system is trivial; it assigns the set of all terms to every variable.
Literature
* * * * * * * * * * * * * * * * *Literature on negative constraints
* * * * * *Notes
Formal languages {{comp-sci-theory-stub