MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Negative set constraints: an easy proof of decidability

Witold Charatonik Leszek Pacholski

MPI–I–93–265 December 1993

[figure: I N F O R M A T I K]

Im Stadtwald D 66123 Saarbrücken

Germany Authors’ Addresses

Witold Charatonik Institute of Computer Science University of Wrocław Przesmyckiego 20 51–151 Wrocław, Poland

wch@ii.uni.wroc.pl

Leszek Pacholski Institute of Mathematics Polish Academy of Sciences Kopernika 18 51–617 Wrocław, Poland

pacholsk@ii.uni.wroc.pl

Publication Notes

This paper has been submitted for publication elsewhere and will be copyrighted if accepted.

Acknowledgements

We are indebted to Harald Ganzinger for several interesting conversations on the subject of set constraints.

The first author would like to thank Krzysiek Loryś for many hours he spend listening to consecutive version of the proof and first of all for his encouragement.

This research was partially supported by KBN grants 2 1197 91 01 and 2 1368 91 01.

This research was conducted while Witold Charatonik visited Max-Planck-Institut für Informatik (Saarbrücken). His stay there was supported by TEMPUS JEP 1941.

During the final stage of preparation of this paper Leszek Pacholski visited INRIA-Lorraine (Nancy) supported by CRNS through a research project EURECA. He would like to thank Pierre Lescanne for his hospitality.

The responsibility for the contents of this publication lies with the authors.

Abstract

Systems of set constraints describe relations between sets of ground terms. They have been successfuly used in program analysis and type inference. So far two proofs of decidability of mixed set constraints have been given: by R. Gilleron, S. Tison and M. Tommasi [12] and A. Aiken, D. Kozen, and E.L. Wimmers [3], but both these proofs are very long, involved and difficult to follow.

We first give a new, simple proof of decidability of systems of mixed positive and negative set constraints. We explicitely describe a very simple algorithm working in NEXPTIME and we give in all detail a relatively easy proof of its correctness. Then we sketch how our technique can be applied to get various extensions of this result. In particular we prove that the problem of consistency of mixed set constraints with restricted projections and unrestricted diagonalization is decidable. Diagonalization here represents a decidable part of equality. It is known that the equality of terms can not be directly included in the language of set constraints. Our approach is based on a reduction of set constraints to the monadic class given in a recent paper by L. Bachmair, H. Ganzinger, and U. Waldmann [7].

To save space we assume that the reader is familiar with the main ideas of the method introduced in [7] of using the monadic class to study set constraints. We shall drop this assumption in the full paper.

1 Introduction

Set constraints give a natural formalism for many problems in program analysis and type inference. They have been studied and applied in many papers including [5], [4], [14], [15], [17], [18], [20].

The first general results concerning the decidability of set constraints were obtained by Heintze and Jaffar [13], who studied the so-called definite set constraints. The decidability of systems of positive set constraints was established by A. Aiken and E.L. Wimmers [6]. Later other proofs have been obtained. R. Gilleron, S. Tison, and M. Tommasi [11] gave a proof based on automata theoretic techniques and L. Bachmair, H. Ganzinger, and U. Waldmann [7] gave a simple and very elegant proof using the decision procedure for the first order theory of monadic predicates, providing also NEXPTIME-completeness of the problem of solvability of positive set constraints. In a paper by A. Aiken, D. Kozen, M. Vardi, and E.L. Wimmers [2], yet another algorithm has been presented and a detailed analysis of the complexity of positive set constrains has been given.

The problem of the decidability of sets constraints with negated inclusion was more difficult. Two solutions were obtained independently by Aiken, Kozen, and Wimmers [3], and Gilleron, Tison and Tommasi [12]. Both solutions are quite difficult and involved.

The solution by Aiken, Kozen and Wimmers uses ideas of [2] and goes through normal forms, a reduction to another problem concerning hypergraphs, a reduction to the Diophantine (nonlinear) reachability problem, and solving the last one in some sense again using graph-theoretic tools. Later an improvement of this result was obtained by K. Stefansson [19], who simplified the last part of the proof, obtained NP-completeness of the Diophantine reachability problem, and thus established NEXPTIME-completeness of the original problem.

The solution by Gilleron, Tison and Tommasi extends ideas of [11] and is based on the notion of a tree set automaton. It is quite involved, the paper presenting the proof is rather long and contains a difficult combinatorial lemma whose proof is very long and rather difficult to follow.

Our proof is based on the idea of L. Bachmair, H. Ganzinger, and U. Waldmann [7] to reduce the decidability problem for positive set constraints to the problem of consistency of first order theories of unary predicates. It has been known for some time (see [1], [16]), that it is decidable if a finite set of first order sentences in a language L having only unary predicates has a model. Moreover, for sentences without equality the size of such a model can be bounded by 2^{N}, where N is the number of predicate symbols in L. In [7] a simple method was given for translating the problem of consistency of positive set constraitns to the problem of consistency of finite sets of sentences in a first order unary language, and a method of obtaining solutions of systems of positive set constraints from the corresponding finite models of monadic theories.

The translation of set constraints to monadic theories works also for negative set constraints. Our extension solves the problem of how to use a finite model of a monadic theory to get a solution of the corresponding system of set constraints. The main problem is to make sure that some sets of terms are non empty. The first observation is that each solution of a system of set constraints gives a finite approximation, called a history which is sufficient to reconstruct a (perhaps different) regular solution. Then, the proof proceeds by distinguishing a small subset, the skeleton of a history, which is small, is not always a history, but can be collapsed to obtain a small history. Now, what is left, is to make an exhaustive search through all small histories, which is described below in the algorithm EASY.

In the last section we consider set constraints with projections and diagonalizations. First, just by changing some parameters in EASY, we prove that we can extend to the case of mixed constraints some results of [7] on positive set constraints with restricted projection and diagonalization. Then we sketch a proof of a theorem saying that in fact the restrictions on diagonalizations can be lifted. The diagonalization is a way of introducing a weak form of equality which allows to compare brothers in a term. It has been proved by B. Bogaert and S. Tison [8] that if the comparison of cousins is allowed, then the problem (or even its special case) becomes undecidable.

2 Basic definitions

Let Σ = {a_{1}^{0}, …, a_{i_{0}}^{0}, f_{1}^{1}, …, f_{i_{1}}^{1}, …, f_{1}^{m}, …, f_{i_{m}}^{m}}, where a_{1}^{0}, …, a_{i_{0}}^{0} are constant symbols, f_{i_{1}}^{1}, …, f_{1}^{m}, …, f_{i_{m}}^{m} are function symbols and f_{j}^{i} stands for j-th symbol of arity i in Σ, and let V be a set of second order variables. Set expressions are defined by the grammar

E ::= 0 | 1 | α | E ∪ E | E ∩ E | Ē | f_{i}^{k}(E_{1}, ..., E_{k})

where α is a set variable in V and f_{i}^{k} ∈ Σ. A positive set constraint is a relation of the form E ⊆ E′, and a negative set constraint has a form E ⊈ E′.

Consider a system of set constraints

(SC)  E_{1} ⊈ E′_{1} ∧ … ∧ E_{l} ⊈ E′_{l} ∧ E_{l+1} ⊆ E′_{l+1} ∧ … ∧ E_{k} ⊆ E′_{k}.

Let E(SC) denote set of all subexpressions of E_{1}, E′_{1}, …, E_{k}, E′_{k}. Following [7] for each expression E ∈ E(SC) we introduce a predicate symbol P_{E}. Let φ′ be the universal closure of the conjunction of the formulas defining predicates P_{E} for all E ∈ E(SC) (i.e. formulas of the form P_{E_{1}∪E_{2}}(y_{1}) ↔ P_{E_{1}}(y_{1}) ∨ P_{E_{2}}(y_{1}), …, P_{f_{j}^{i}(E_{1},...,E_{i})}(f(y_{1}, …, y_{i})) ↔ P_{E_{1}}(y_{1}) ∧ … ∧ P_{E_{i}}(y_{i}), P_{f_{j}^{i}(E_{1},...,E_{i})}(g(y_{1}, …, y_{i′})) ↔ false for g ∈ Σ \ {f_{j}^{i}}). For the system (SC) the formula

∃x_{1} … ∃x_{l}∀y_{1}(P_{E_{1}}(x_{1}) ∧ ¬P_{E′_{1}}(x_{1})) ∧ … ∧ (P_{E_{l}}(x_{l}) ∧ ¬P_{E′_{l}}(x_{l}))∧
∧(P_{E_{l+1}}(y_{1}) → P_{E′_{l+1}}(y_{1})) ∧ … ∧ (P_{E_{k}}(y_{1}) → P_{E′_{k}}(y_{1})) ∧ φ′

expresses the satisfiability of (SC). Moving the quantifiers of φ′ outward, we obtain a formula of the form

∃x_{1} … ∃x_{l}∀y_{1} … ∀y_{m}φ(x_{1}, …, x_{l}, y_{1}, …, y_{m}, a_{1}^{0}, …, a_{i_{0}}^{0}, f_{1}^{1}(y_{1}), …, f_{i_{m}}^{m}(y_{1}, …, y_{m})),

with φ built using only monadic predicate symbols (and the symbols listed above). It can easily be seen that this formula is a (partial) skolemization of the formula ψ below.

∃x_{1} … ∃x_{l}∃x_{1}^{0} … ∃x_{i_{0}}^{0}∀y_{1}∃x_{1}^{1} … ∃x_{i_{1}}^{1}∀y_{2}∃x_{1}^{2} … ∃x_{i_{2}}^{2} … ∀y_{m}∃x_{1}^{m} … ∃x_{i_{m}}^{m} φ(x_{1}, …, x_{l}, y_{1}, …, y_{m}, x_{1}^{0}, …, x_{i_{0}}^{0}, x_{1}^{1}, …, x_{i_{m}}^{m})

Let N be the number of predicate symbols in P = {P_{E} | E ∈ E(SC)}. If I is a model of ψ then we consider the equivalence relation ≡ in I such that x ≡ y if and only if for all P ∈ P we have P^{I}(x) ↔ P^{I}(y), where P^{I} is the interpretation of P in I. Let M be the number of different nonempty equivalence classes of the relation ≡. We will often identify the interpretation of a unary predicate symbol P^{I} with the subset {x | P (x)} of the domain of I.

Lemma 2.1 (see [1], p.34) A monadic formula (without equality) is satisfiable if and only if it has a finite model (of cardinality M ≤ 2^{N}) such that in each equivalence class of the relation ≡ there is at most one element.

3 The algorithm

In this section we give an algorithm solving set constraints with negated inclusion. The algorithm is nondeterministic with exponential time complexity. This together with the results from [7] gives NEXPTIME-completeness of the problem. Note that except the first step, when we choose a model of a monadic formula (which requires nondeterministic exponential time, see [16] for details), the algorithm is nondeterministic polynomial.

Steps 2 and 3 implement a standard method of building Herbrand models. Step 4 gives a definition of a solution, if one exists. Note that in this step we do not compute the whole solution, we just give a description of how to compute it. Since this description is finite, the solution is regular (see [12] for a definition of regularity).

algorithm EASY input: formula ψ representing set constraint (SC) output: solution of (SC) if such a solution exists, ”NO SOLUTION” if it does not exist

1. Nondeterministically choose a model of ψ consisting of a finite domain D (of cardinality M ≤ 2^{N}) and a subset P_{E}^{D} of D, for each E ∈ E(SC), such that in each equivalence class there is at most one element. If such a model does not exist then return(”NO SOLUTION”).

2. Nondeterministically choose d_{1}^{0}, … d_{i_{0}}^{0} ∈ D such that

∃x_{1} … ∃x_{l}∀y_{1}∃x_{1}^{1} … ∃x_{i_{1}}^{1}∀y_{2} … ∃x_{i_{m}}^{m} φ(x_{1}, …, x_{l}, y_{1}, …, y_{m}, d_{1}^{0}, …, d_{i_{0}}^{0}, x_{1}^{1}, …, x_{i_{m}}^{m})

holds in D. Such d_{1}^{0}, … d_{i_{0}}^{0} exist because ψ is satisfied in our interpretation. Put Φ(a_{j}^{0}) = d_{j}^{0} and H = {a_{1}^{0}, … a_{i_{0}}^{0}}.

3. Repeat this step until |H| ≥ 2M^{3} or Φ(H) = D:

Choose a function symbol f_{j}^{k} ∈ Σ and a sequence t_{1}, … t_{k} of terms from H such that Φ(f_{j}^{k}(t_{1}, … t_{k})) has not yet been defined. Choose d_{j}^{k} ∈ D such that

∃x_{1} … ∃x_{l}∃x_{1}^{1} … ∃x_{j−1}^{k}∃x_{j+1}^{k} … ∃x_{j_{k}}^{k}∀y_{k+1} … ∃x_{i_{m}}^{m}

φ(x_{1}, …, x_{l}, Φ(t_{1}), …, Φ(t_{k}), y_{k+1}, …, y_{m}, d_{1}^{0}, …, d_{i_{0}}^{0}, x_{1}^{1}, …, d_{j}^{k}, …, x_{i_{m}}^{m})

holds in D. Add f_{j}^{k}(t_{1}, …, t_{k}) to H and define Φ(f_{j}^{k}(t_{1}, …, t_{k})) = d_{j}^{k} .

4. If Φ(H) = D then fix terms t^{1}, …, t^{M} ∈ H such that Φ({t^{1}, …, t^{M}}) = D. If Φ(f_{j}^{i}(t^{j_{1}}, …, t^{j_{i}})) is not defined for some f_{j}^{i} ∈ Σ and some t^{j_{1}}, …, t^{j_{i}} among t^{1}, …, t^{M}, then define it in the same way as in the step 3. Extend Φ to T (Σ) by defining Φ(f_{j}^{i}(t_{1}, …, t_{i})) = Φ(f_{j}^{i}(t^{j_{1}}, …, t^{j_{i}})) where Φ(t^{j_{k}}) = Φ(t_{k}).

Now for each set variable X ∈ E(SC) return(”SOLUTION:” X = Φ^{−1}(P_{X}^{D})).

If for all nondeterministic choices in steps 1–3 Φ(H) ⊆_{/}D then return(”NO SOLUTION”).

4 Correctness of the algorithm

4.1 Soundness

Theorem 4.1 The algorithm gives only correct solutions.

Proof. Consider an interpretation with the domain T (Σ) and predicates P_{E}^{T (Σ)} for E ∈ E(SC) defined as follows: P_{E}^{T (Σ)}(t) ↔ P_{E}^{D}(Φ(t)). It suffices to show that under this interpretation the formula

∃x_{1} … ∃x_{l}∀y_{1} … ∀y_{m} φ^{T (Σ)}(x_{1}, …, x_{l}, y_{1}, …, y_{m}, a_{1}^{0}, …, a_{i_{0}}^{0}, f_{1}^{1}(y_{1}), …, f_{i_{m}}^{m}(y_{1}, …, y_{m}))

is satisfied. Take d_{1}, … d_{l} ∈ D such that the formula

∃x_{1}^{0} … ∃x_{i_{0}}^{0}∀y_{1}∃x_{1}^{1} … ∃x_{i_{m}}^{m}φ(d_{1}, …, d_{l}, y_{1}, …, y_{m}, x_{1}^{0}, …, x_{i_{0}}^{0}, x_{1}^{1}, …, x_{i_{m}}^{m})

is satisfied, and x_{i} ∈ Φ^{−1}(d_{i}). Then for any t_{1}, …, t_{m} ∈ T (Σ) we get

φ^{T (Σ)}(x_{1}, …, x_{l}, t_{1}, …, t_{m}, a_{1}^{0}, …, a_{i_{0}}^{0}, f_{1}^{1}(t_{1}), …, f_{i_{m}}^{m}(t_{1}, …, t_{m})) ↔
↔ φ^{D}(Φ(x_{1}), …, Φ(x_{l}), Φ(t_{1}), …, Φ(t_{m}), Φ(a_{1}^{0}), …
…, Φ(a_{i_{0}}^{0}), Φ(f_{1}^{1}(t_{1})), …, Φ(f_{i_{m}}^{m}(t_{1}, …, t_{m}))) ↔
↔ φ^{D}(d_{1}, …, d_{l}, Φ(t_{1}), …, Φ(t_{m}), d_{1}^{0}, …, d_{i_{0}}^{0}, d_{1}^{1}, …, d_{i_{m}}^{m}) ↔
↔ true
□

4.2 Completeness

A solution of (SC) is a function S : X → P(T (Σ)), where X is the set of variables occurring in (SC). This function can be extended in a unique way to a function from E(SC) to P(T (Σ)). If E(SC) = {E_{1}, …, E_{N}}, then let D = {S(ε(E_{1})) ∩ … ∩ S(ε(E_{N})) | ε(E_{i}) ∈ \{E_{i}, \overline{E_{i}}\}\}. We can identify D with the set T (Σ)/≡ of equivalence classes of the relation ≡, so D contains at most 2^{N} elements which are disjoint subsets of T (Σ). Let Φ be the quotient mapping from T (Σ) into D, i.e. Φ(t) = d ∈ D if t ∈ d, so the sentence Φ(t_{1}) = Φ(t_{2}) is equivalent to the sentence t_{1} ≡ t_{2}. In this section while talking about a solution of (SC) we will think of a function Φ rather then of S. Of course if we have the function Φ we can reconstruct the function S putting for all X ∈ X S(X) = Φ^{−1}(⋃{ε(E_{1}) ∩ … ∩ ε(E_{N}) ∈ D | ε(X) = X}).

We fix a linear ordering ≺ on terms such that if t is a term of depth lower then the depth of s, then t ≺ s. The maximal subterm of a term f(s_{1}, …, s_{k}) is a term s_{j} among s_{1}, …, s_{k} such that for all i ≤ k, s_{i} ≺ s_{j} (if there are two maximal subterms s_{j} = s_{l} with j < l then the first occurrence, i.e. s_{j} is the maximal subterm).

Definition 4.2 A history of a solution Φ of (SC) is a finite set of terms (labeled by their image under Φ) containing the minimal terms in each equivalence class and closed under taking subterms.

Lemma 4.3 A history of a solution gives all necessary information to construct a (perhaps different, regular) solution.

Proof. With a history of solution on input, EASY does not need to proceed with steps 1–3; it can at once go to step 4 and extend this information to a solution. □

In this subsection we will show that if this set is too big then we are able to construct a new solution with a smaller one. The key observation here is that if f(s_{1}, …, t, …, s_{n}) belongs to the history H and there is no other term in H containing t as a subterm, then if we can replace f(s_{1}, …, t, …, s_{n}) by f(s′_{1}, …, t, …, s′_{n}) where s_{i} ≡ s′_{i} and s′_{i} are minimal in their equivalence classes, we obtain a smaller history.

In the text below c[i] denotes the i-th term (according to the ordering ≺) in the set Φ^{−1}(c), and the set of milestones is a subset of the history (defined in the background of the definitions below). We call a term composed if it is not a constant symbol.

Definition 4.4 The semi-skeleton of a history of a solution Φ of (SC) is a labeled graph M constructed in the following way:

• initialize the set of milestones as the set containing all the minimal terms in each equivalence class,

• initialize the set of nodes of M as the minimal set containing the set of milestones and closed under the operation of taking the maximal subterm,

• label each node t in M with Φ(t),

• connect each composed term in M with its maximal subterm by an edge directed from a term to its superterm, • label each edge t → f(s_{1}, …, t, …, s_{n}) with the rule

f(Φ(s_{1})[1], …, ∗, …, Φ(s_{n})[1]).

Before we say how to extend the semi-skeleton to a skeleton, we want to give some intuition of how to interpret this graph. A label of an edge can be interpreted as information for the algorithm from section 3 what to choose in its nondeterministic choice to get a solution. The rule f(c_{1}[1], …, ∗, …, c_{n}[1]) says: take the predecessor t of the edge and first ([1] indicates the first term) terms t_{1}, …, t_{n} from the sets Φ^{−1}(c_{1}), …, Φ^{−1}(c_{n}) and define Φ(f(t_{1}, …, t, …, t_{n})) as the label of the successor of the edge. Of course we have to decide what to do if conflict arises, i.e. if we are to define Φ on one term in several different ways.

Definition 4.5 A fork of degree k ≥ 2 is a term t such that in the semi-skeleton there are k edges connecting t with k its superterms, labeled with the same rule.

Definition 4.6 A skeleton of a history is a graph with the following properties:

• it is a forest with directed edges leading from roots to leaves

• it contains the semi-skeleton (with changed labels of egdges) as a subgraph

• labels of edges outgoing from a single node are different

• labels of edges are compatible with the sentence ψ defined in the section 2, i.e. if f_{j}^{k}(c_{1}[j_{1}], …, ∗, …, c_{k}[j_{k}]) is a label of an edge t → s, then the formula ψ with c_{1}, …, Φ(t), …, c_{k} substituted for y_{1}, …, y_{k} and Φ(s) substituted for x_{j}^{k} is satisfied

• if c[j] is used in a label of an edge t → s then there are at least j milestones labeled by c, and each of these nodes (according to the linear ordering ≺) is a term lower then t

• all leaves are milestones

Lemma 4.7 If Φ is a solution of (SC), then there exists a skeleton of the history of Φ.

Proof. If t is a fork of degree k, then we have in original history k different terms f(s_{1}^{1}, …, t, …, s_{n}^{1}), …, f(s_{1}^{k}, …, t, …, s_{n}^{k}), with s_{j}^{i} ≺ t. Without loss of generality we can assume that the terms s_{1}^{1} and s_{1}^{2} are different. Now if the terms s_{1}^{1}, …, s_{1}^{k} are different, then we add k − 1 minimal terms from Φ^{−1}(Φ(s_{1}^{1})) to the set of milestones (remember that Φ(s_{1}^{i}) = Φ(s_{1}^{j}), so we have at least k terms in this set) and replace the labels of edges with k different rules f(Φ(s_{1}^{1})[1], …, ∗, …, Φ(s_{n}^{1})[1]), …, f(Φ(s_{1}^{1})[k], …, ∗, …, Φ(s_{n}^{1})[1]). If there are less then k terms among s_{1}^{1}, …, s_{1}^{k}, then it is even better, because we need less new milestones. Consider the following examples

Example 1 t is a fork of degree 4 and we have the following four terms as nodes in the skeleton of the history of a solution Φ: f(t, x_{1}, y), f(t, x_{2}, y), f(t, x_{3}, y), f(t, x_{4}, y) with Φ(x_{1}) = Φ(x_{2}) = Φ(x_{3}) = Φ(x_{4}) = x. Then we label edges t → f(t, x_{j}, y) with the rules f(∗, x[j], Φ(y)[1]) which (while executing step 3 of EASY and building a new solution Φ′) we interpret as follows: take the term t (predecessor of these edges), the four minimal terms t_{1}, …, t_{4} from the set Φ^{−1}(x) (these are also four minimal terms from Φ^{′−1}(x)), the minimal term s in Φ^{−1}(Φ(y)) and define Φ′(f(t, t_{j}, s)) = Φ(f(t, x_{j}, y))

Example 2 t is a fork of degree 4 and we have the following four terms as nodes in the skeleton of the history of solution Φ: f(t, x_{1}, y_{1}), f(t, x_{2}, y_{1}), f(t, x_{1}, y_{2}),f(t, x_{2}, y_{2}) with Φ(x_{1}) = Φ(x_{2}) = x and Φ(y_{1}) = Φ(y_{2}) = y. Then we have to create only two new milestones - the second minimal terms from the sets Φ^{−1}(x) and Φ^{−1}(y) and label the four edges with the rules f(∗, x[1], y[1]), f(∗, x[2], y[1]), f(∗, x[1], y[2]), f(∗, x[2], y[2])

Note that if we have a fork of degree k then we introduce at most k − 1 new milestones, which are among the first k − 1 terms in some equivalence classes. Moreover, these milestones are of depth less then or equal to the depth of the fork. □

Below we shall prove that a solution of a system of set constraints can be reconstructed from a skeleton of a history. In fact a solution can be reconstructed from any labeled graph satisfying all the conditions described in Definition 4.6 except containing the semi-skeleton, slightly extended to allow dealing with constants in the definition below.

Definition 4.8 Given a skeleton S we say that a term t′ is a collapse of a node t ∈ S if either t is a constant symbol and t′ = t or t′ = f(t_{1}, …, s′ …, t_{k}) and there is an edge s → t labeled with f(c_{1}[j_{1}], …, ∗, …, c_{k}[j_{k}]), the term s′ is the collapse of the node s and t_{1}, …, t_{k} are collapses of respective milestones. The collapsing function is a function mapping each node of the skeleton of the history to its collapse.

Lemma 4.9 The collapsing function is 1 to 1.

Proof. (induction on depth of terms) It is obvious that a constant symbol cannot be a collapse of two different nodes. Let us suppose that all collapsed terms of depth less than or equal to n are collapses of at most one node and there is a term of depth n + 1 which is a collapse of two different nodes. Without loss of generality we can assume that this is a term of the form f(t′, s′) where t′ and s′ are collapses of nodes t and s respectively, with s ≺ t. f(t′, s′) must be produced with the two rules of the form f(c_{1}[k], ∗) and f(∗, c_{2}[l]), so t′ must be the collapse of the k-th milestone from Φ^{−1}(c_{1}) which is not t (because s ≺ t and this k-th milestone is a term lower then s). Hence t′ is a collapse of two different nodes which is impossible. □

Lemma 4.10 If Φ is a solution of (SC) then the collapse of the skeleton of a history of Φ is a history of a solution Φ′.

Proof. Consider the following path of choices of EASY:

1. choose the model with domain D consisting of the set of equivalence classes of the equivalence relation defined by Φ.

2. choose d_{1}^{0}, …, d_{i_{0}}^{0} as Φ(a_{0}^{0}), …, Φ(a_{i_{0}}^{0}) (note that now Φ′ is defined on all the roots of the skeleton of the history).

3. if Φ′ is defined on a collapse t′ of a node t in the skeleton of the history and there is an edge t → s labeled with a rule f_{j}^{k}(c_{1}[j_{1}], …, ∗, …, c_{k}[j_{k}]) then choose the function symbol f_{j}^{k}, terms t_{i} as the j_{i}-th minimal terms from the set Φ^{′−1}(c_{i}) (and the term t′) and d_{j}^{k} as Φ(s). If we define Φ′ on s_{1} before defining it on s_{2} whenever s_{1} ≺ s_{2} then we are sure that Φ′ is already defined on the terms t_{1}, … t_{k} when we want to define it on f_{j}^{k}(t_{1}, …, t′, …, t_{k}). Lemma 4.9 ensures us that when we want to define Φ′ on any term, it was not defined earlier.

4. since the skeleton of a history contains nodes labeled with all elements of D, then EASY, with the bound 2M^{3} omitted, ends with success.

From the theorem 4.1 it follows that Φ′ is a solution of (SC). □

Lemma 4.11 There are at most M^{2} milestones.

Proof. We start building the skeleton of a history (from a semi-skeleton) with M milestones. This gives for each number d at most M different terms of depth d in the semi-skeleton. Then we add new milestones only if a fork is encountered. Let t be a fork of degree k and let d denotes its depth. We have in the skeleton at least k superterms of t of depth d + 1 and t is the only one their subterm of depth d. Then we add at most k − 1 new terms (milestones) of depth less than or equal to d. Hence still we have at most M terms of depth d in the skeleton, which means that degrees of forks are bounded by M and the set of milestones has at most M minimal terms in each equivalence class. So the cardinality of this set is bounded by M^{2}. □

Lemma 4.12 There are at most M^{2} nodes of outdegree greater than one.

Proof. In a forest the number of nodes of outdegree greater than one is less then the number of leaves. Each leaf of the skeleton of the history is a milestone. □

Lemma 4.13 If a system of set constraints (SC) has a solution, then it has one with the history consisting of at most 2M^{3} terms.

Proof. Assume that Φ is a solution of (SC). By lemma 4.10 we can assume that all terms in the history of Φ belong to the skeleton of this history. Suppose that there are more than 2M^{3} nodes. By lemmas 4.11 and 4.12 the number of milestones and the nodes of outdegree greater than one is bounded by 2M^{2}, so there exists a path u_{1} → … → u_{m} with m ≥ M such that u_{1}, …, u_{m} are terms of outdegree one and none of them is a milestone. So, there are two terms u_{i} and u_{j} with 1 ≤ i < j ≤ m such that Φ(u_{i}) = Φ(u_{j}). Now, we can cut off the path u_{i} → … → u_{j−1} thus obtaining a smaller skeleton of a history. In fact, to build a new solution Φ′ of (SC) with a lower number of terms in its history we proceed as in the proof of lemma 4.10. We have only to show that in step 3 we can assume that Φ′ is not yet defined on f_{j}^{k}(t_{1}, …, t_{k}), and that Φ′ is defined on t_{1}, …, t_{k}. The former condition is fulfilled since different nodes collapse to different terms - if a term s′ is a collapse of two nodes s_{1}, s_{2} then s′[u_{i}/u_{j}] is a collapse of two nodes s_{1}[u_{i}/u_{j}] and s_{2}[u_{i}/u_{j}] where s[u_{i}/u_{j}] denotes a term with all occurrences of u_{i} replaced by u_{j}, which contradicts Lemma 4.9. The latter condition is satisfied since Φ is defined on s[u_{i}/u_{j}].

Repeating the procedure described above we can find a solution with at most 2M^{3} different terms in its history. □

As corollaries to lemma 4.13 we get Theorem 4.14 If a system of set constraints (SC) has a solution then EASY provides one.

Theorem 4.15 The problem if a system of set constraints has a solution is NEXPTIME-complete.

5 Extensions

In [7] Bachmair, Ganzinger and Waldmann proved that for positive set constraints some extensions of the problem are also decidable. These were the satisfiability problems for set constraints without positive occurrences of projections for nonmonadic function symbols and for set constraints without positive occurrences of diagonalizations. These extensions are decidable also in the case of mixed (positive and negative) set constraints.

Theorem 5.1 The problem of satisfiability of mixed set constraints with projections where projections of non-monadic function symbols occur only negatively in positive inclusions is NEXPTIME-complete.

Proof. The transformation described in the section 2 gives for such a system a monadic formula (note that projections for monadic function symbols are not restricted here). We can just proceed with EASY, the arguments given in section 4 work here without any change. □

The case with diagonalization requires more arguments. If diagonalization operators do not occur positively (this time they may occur in negative inclusions too) we get a monadic formula with equality, without positive occurrences of the equality predicate. We need an extension of Lemma 2.1 to deal with the equality.

Definition 5.2 Let ψ be a monadic formula of quantifier depth at most q, with equality. Two interpretations I, J of ψ are similar if for each pair c_{I}, c_{J} of corresponding equivalence classes of the relations ≡_{I} and ≡_{J} either |c_{I}| = |c_{J}| or both c_{I} and c_{J} have at least q elements.

As an immediate application of Ehrenfeucht games [10] one can prove (see also [9]) that if I is a model of ψ and I is similar to J, then J is also a model of ψ. If ψ has no positive occurrences of the equality predicate, the similarity condition can be weakened: for J to be a model of ψ it suffices that for each pair of corresponding equivalence classes we have |c_{I}| ≤ |c_{J}|.

Now, to check that a finite model I of ψ (of cardinality less then or equal to Mq) corresponds to a Herbrand model, we have to define Φ in such a way, that for each c in the domain of I we have |Φ^{−1}(c)| ≥ |c|. Replacing in EASY the condition Φ(D) = D (which is equivalent to |Φ^{−1}(c)| ≥ 1 for each c ∈ D) by |Φ^{−1}(c)| ≥ |c| for each c ∈ D, and 2M^{3} by 2M^{3}q^{2}, we get the algorithm solving extended systems of set constraints. The proof of correctness of this algorithm is just the same as in Section 4. The only difference is that we start building the skeleton of the history with (at most) Mq milestones, getting at most 2(Mq)^{2}M terms in the collapse of the skeleton of the history. As a corollary we get Theorem 5.3 The problem of satisfiability of mixed set constraints with negative diagonalizations is NEXPTIME-complete.

Using the method presented here we can also solve the satisfiability problem for systems of set constraints with unrestricted diagonalization. The main new problem here is to make sure that in the process of construction, when Φ^{−1}(c) has reached the desired cardinality, then we can extend Φ to a solution without adding any new terms to Φ^{−1}(c).

We have two solutions. The simpler is as follows. Given a set T of terms, by Σ(T ) we denote the set of terms of the form f(t_{1}, ..., t_{k}), where f ∈ Σ and t_{i} ∈ T . Using the techniques of Section 4 we can easily prove that if a set T and Φ have been constructed so that all finite (and bounded) classes have been saturated (i.e. have the desired number of elements), then it suffices to make sure that Φ can be extended to all terms of Σ^{M+1}(T ) without adding new elements to the saturated classes. Therefore the problem of consistency reduces to the problem of finding a set T and a function Φ on Σ^{M+1}(T ) as described above, which can be obtained by an extension of EASY. This unfortunately leads to a nondeterministic double exponential algorithm.

There is, however, a more subtle solution which gives a NEXPTIME decision procedure. The details will be presented in the full version of the paper.

Theorem 5.4 The problem of satisfiability of mixed set constraints with projections for non-monadic function symbols occurring only negatively in positive inclusions and with unrestricted diagonalizations is decidable.

References

[1] W. Ackermann. Solvable Cases of the Decision Problem. North-Holland, Amsterdam, 1954.

[2] A. Aiken, D. Kozen, M. Vardi, and E. L. Wimmers. The complexity of set constraints. Technical Report 93-1352, Computer Science Department, Cornell University, May 1993.

[3] A. Aiken, D. Kozen, and E. L. Wimmers. Decidability of systems of set constraints with negative constraints. Technical Report 93-1362, Computer Science Department, Cornell University, June 1993.

[4] A. Aiken and B. Murphy. Implementing regular tree expressions. In ACM Conference on Functional Programming Languages and Computer Architecture, pages 427–447, August 1991.

[5] 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.

[6] 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.

[7] L. Bachmair, H. Ganzinger, and U. Waldmann. Set constraints are the monadic class. In Eight Annual IEEE Symposium on Logic in Computer Science, pages 75–83, 1993.

[8] B. Bogaert and S. Tison. Automata with equality tests. Technical Report IT 207, Laboratoire d’Informatique Fondamentale de Lille, 1991.

[9] B. Dreben and W. D. Goldfarb. The Decision Problem. Solvable Classes of Quantificational Formulas. Addison-Wesley Publishing Company, Inc., 1979.

[10] A. Ehrenfeucht. An application of games to the completeness problems for fromalized theories. Fundamenta Mathematicae, 49:129–141, 1961.

[11] 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.

[12] R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints with negated subset relationships. In Proceedings of the 34^{th} Symp. on Foundations of Computer Science, pages 372–380, 1993. A full version Technical report IT 247, Laboratoire d’Informatique Fondamentale de Lille.

[13] 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.

[14] 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.

[15] 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.

[16] H. R. Lewis. Complexity results for classes of quantificational formulas. Journal of Computer and System Sciences, 21:317–353, 1980.

[17] P. Mishra and U. Reddy. Declaration-free type checking. In Twelfth Annual ACM Symposium on the Principles of Programming Languages, pages 7–21, 1985.

[18] J. C. Reynolds. Automatic computation of data set definitions. Information Processing, 68:456–461, 1969.

[19] K. Stefansson. Systems of set constraints with negative constraints are NEXPTIME-complete. Technical Report 93-1380, Computer Science Department, Cornell University, August 1993.

[20] 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.