In questo articolo riassumiamo brevemente alcuni dei problemi piu` interessanti che nascono quando si permette di trattare gli insiemi come oggetti di “prima classe” in un linguaggio logico, dall’unificazione di insiemi ben-fondati e non alla soluzioni di vincoli su insiemi. In this paper, we briefly summarize some of the most challenging issues that arise when allowing sets to be dealt with as first-class objects in a logic language, ranging from set unification of well-founded and non-well-founded sets to set constraint solving. 1
Sets are familiar mathematical objects, and they are often used as a high-level abstraction to represent complex data structures, whenever the order and repetitions of elements are immaterial.
In the last two decades, a number of proposals have emerged where sets are dealt with as primitive objects of a (first-order) logic language. In this context, sets are often represented as first-order terms, called set terms, built from symbols of a suitable alphabet, using selected function symbols as set constructors. Furthermore, the language usually provides the typical set-theoretic operations to manipulate set objects.
These short notes summarize some of the most challenging issues arising when manipulating finite sets in a logic language. In Section 2 we briefly review set unification, i.e., the key problem of solving equations between set terms. In Section 3 the unification problem is extended to the case of non-well-founded sets. In Section 4 we introduce set constraints as a way to allow set-theoretic operations other than set equality to be taken into account. Finally, in Section 5 we briefly review proposals aiming at making set constraint solving more effective. 2
Intuitively, the set unification problem is the problem of computing (or simply testing the existence of) an assignment of values to the variables occurring in two set terms which makes them denote the same set.
Various forms of set unification have been used in
various application areas, such as (see [
Set unification can be thought of as an instance of Eunification, i.e., unification modulo an equational theory E, where the identities in E capture the properties of set terms—i.e., the fact that the ordering and repetitions of elements in a set are immaterial.
The equational theory E is strongly related to the
representation adopted for set terms. Two main approaches
have been presented in the literature: the union-based
representation, and the list-like representation. The
unionbased representation makes use of the union operator (∪)
to construct sets. This representation has been often used
when dealing with the problem of set unification on its
own, where set unification is dealt with as an ACI
unification problem—i.e., unification in presence of operators
satisfying the Associativity, Commutativity, and
Idempotence properties (e.g., [
The list-like representation builds sets using an element insertion constructor (typically denoted by {· | ·}). With this approach, the finite set {t0, . . . , tn} is represented by a sequence of element insertions
{t0 | {· · · {tn | ∅} · · ·}},
where t0, . . . , tn are either individuals or sets. While this
representation restricts the number of set variables which
can occur in each set term to one, on the other hand it
allows sets to be viewed and manipulated in a fashion
similar to lists. As a matter of fact, this representation has
been adopted in a number of logic and functional-logic
programming languages with sets (e.g., CLP (SE T ) [
Various authors have investigated the problem of set
unification using the list-like representation [
A general survey of the problem of unification in
presence of sets, across different set representations and
different admissible classes of set terms, can be found in [
The computational complexity properties of the set
unification have been investigated by Kapur and
Narendran [
Various authors have considered simplified versions of
the (Ab)(C`) problem obtained by imposing restrictions
on the form of the set terms. In particular, various works
have been proposed to study the simpler cases of
matching1 and unification of Bound Simple set terms, i.e., bound
set terms of the form {s1, . . . , sn}, where each si is either
a constant or a variable [
1Set matching can be seen as a special case of set unification, where variables are allowed to occur in only one of the two set terms which are compared. 3
Sets considered so far are the so called hereditarily finite sets, i.e. sets with a finite number of elements, all of which are themselves hereditarily finite. This definition leaves still a further possibility for infinity. Let us consider the sets x and y that satisfy the equations x = {∅, y}, y = {x}. They are hereditarily finite, but they hide an infinite descending chain x 3 y 3 x 3 y 3 · · ·. These sets in which, roughly speaking, membership can form cycles are called non-well-founded sets (or hypersets). Hypersets are very important in some areas, such as concurrency theory, but hyperset theory has been applied in a number of areas of logic, linguistics, and computer science, as well.
Introducing hypersets as a data structure in a logic programming language requires a unification algorithm that is able to deal with objects denoting hypersets. All set unification algorithms cited in the previous section, however, consider well-founded sets only.
An hyperset unification algorithm is shown in [
The algorithm in [
The algorithms cited above focus only on equality between set terms. Besides equality, however, other basic set operations, such as membership, inclusion, union, etc., are usually required for dealing with sets in a more general way.
A number of proposals have been put forward in the last
fifteen years in which general set-based formulae are
considered and procedures to check their consistency are
developed. Most of these proposals have emerged in the
context of Constraint (Logic) Programming (see, e.g., [
X ∈ S ∧ T = S ∪ R ∧ X 6∈ T is a set constraint, where R, S, and T are set variables, that the set constraint solver can reduce to false.
Set based formalisms allow a natural formulation of a number of problems, in quite different areas: combinatorial search problems, warehouse location problems, diagnostic related problems (e.g., VLSI circuit verification), program analysis, network design problems (e.g., weight setting). Dealing with such formulations as constraints allow, on the one hand, to solve these problems even if not all sets are (fully) known a priori, and, on the other hand, to compute solutions efficiently, provided constraint reasoning enables the solver to prune the search space.
As an example, the following is a very compact formulation as a set constraint of the well-known map coloring problem for a map of three regions, R1, R2, R3 (where R1 borders R2 and R2 borders R3), using two colors, c1 and c2: {R1, R2, R3} = {c1, c2} ∧ M = {{R1, R2}, {R2, R3}} ∧ {c1} 6∈ M ∧ {c2} 6∈ M.
A complete set constraint solver, i.e., one which is
always able to decide if a given constraint is satisfiable
or not is presented in [
This constraint structure has been exploited to obtain a
specific instance of the general Constraint Logic
Programming scheme, called CLP(SE T ) [
The study of set constraints is strongly related to work in
the so-called Computable Set Theory area (C.S.T.), a
fruitful research stream born in the 1970’s at the New York
University thanks to the initial ideas and subsequent
stimulus of J. T. Schwartz (see [
Other classes of aggregates (akin to sets) have also been
considered in the literature. In particular, various
frameworks have introduced the use of multisets where repeated
elements are allowed to appear in the collection. An
analysis of the problems concerned with the introduction of
multisets—as well as sets and lists—is reported in [
The proposals for (general) set constraints cited above do not take into account efficiency adequately to allow them to be effectively applied in many concrete applications. For example the CLP(SE T ) solvers often use a generate & test approach, that non-deterministically assigns values to variables as soon as those values are available. For instance, given the constraint X ∈ {1, 2, 3, 4, 5} ∧ X 6= 10, the CLP(SE T ) solver enumerates all possible values of X before asserting that the constraint holds.
A number of proposals have been developed in the last
fifteen years that consider more restricted forms of set
constraints but equipped with constraint solving techniques
that allow them to be processed in a quite more effective
way. Works along these lines include [
In these proposals constraint variables have a finite domain attached to them. In the case of set constraints, the domain is a collection of sets, usually specified as a set interval [l, u], where l and u are known sets (typically, of integers). [l, u] represents a lattice of sets induced by the subset partial ordering relation ⊆ having l and u as the greatest lower bound and the least upper bound, respectively. The constraint solver exploits the information that the domain of variables provides to efficiently compute simplified forms of the original constraint or to detect failures. In its simplest form, the solver uses a local propagation algorithm that attempts to enforce consistency on the values in the variable domains by removing values that cannot form part of a solution to the system of constraints. For example, given the set constraint
S ∈ {1}..{1, 2, 3, 4} ∧ X ⊆ S ∧ Y ⊆ S
∧ #X = 2 ∧ Z = Y \X
where S, X, Y , and Z are set variables and #X denotes
the cardinality of the set X, the constraint solver in [
While these constraint languages turn out to allow more
efficient handling of set constraints with respect to the
proposals cited in the previous section (e.g., CLP(SE T )), the
latter allows more general form of sets to be dealt with:
elements can be of any type, possibly other sets, and possibly
unknown (e.g., {X, {a, 1}}). For example the set-based
formulation of the map coloring problem shown above can
be written—and solved—using CLP(SE T ) but not using
the constraint language in [
A current line of research (see [
7
Gianfranco Rossi received a degree in Computer Science from the University of Pisa in 1979. Since November 2001 he is a Full Professor of Computer Science at the University of Parma. His research activity has been mainly devoted to Programming Languages, with special attention to Logic Programming languages. Since December 2006 he is President of the Association of Logic Programming (GULP).