BRICS RS-94-32 Aiken et al.: Decidability of Systems of Set Constraints with Negative Constraints

BRICS

Basic Research in Computer Science

Decidability of Systems of Set Constraints with Negative Constraints

Alexander Aiken Dexter Kozen Ed Wimmers

BRICS Report Series RS-94-32 ISSN 0909-0878 October 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

Decidability of Systems of Set Constraints with Negative Constraints^{∗}

Alexander Aiken^{†} University of California, Berkeley

           aiken@cs.berkeley.edu

Dexter Kozen^{‡} Cornell University

kozen@cs.cornell.edu

Ed Wimmers^{§} IBM Almaden Research Center

                      wimmers@almaden.ibm.com

Abstract

Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general systems of positive set constraints have appeared. In this paper we consider systems of mixed positive and negative constraints, which are considerably more expressive than positive constraints alone. We show that it is decidable whether a given such system has a solution. The proof involves a reduction to a number-theoretic decision problem that may be of independent interest.

1 Introduction

Set constraints are formal inclusions or negated inclusions between expressions representing subsets of T_{Σ}, the set of ground terms over a finite ranked alphabet Σ. Formally, a positive set constraint is of the form E ⊆ F and a negative set constraint is of the form E ⊈ F, where E and F are expressions built from a set X = {x, y, …} of variables ranging over subsets of T_{Σ}, the usual set-theoretic operators 0, 1, ∪, ∩, and ∼, and an n-ary set operator f for each n-ary symbol f ∈ Σ with semantics

∗Revised and expanded version of [2].

†EECS Division, University of California, Berkeley, CA 94720 ‡Computer Science Department, Cornell University, Ithaca, NY 14853 §IBM Almaden Research Center, 650 Harry Road, San Jose, CA 95120

f(A_{1}, …, A_{n}) = {ft_{1} … t_{n} | t_{i} ∈ A_{i}, 1 ≤ i ≤ n} .

A system S of constraints is satisfiable if there is an assignment of subsets of T_{Σ} to the variables satisfying all the constraints in S.

Set constraints have numerous applications in program analysis and type inference [3, 4, 7, 12, 13, 15, 16, 17, 18]. Most of these systems deal with positive constraints only. Several algorithms for determining the satisfiability of general systems of positive constraints have appeared [1, 5, 6, 9, 11]. In [1], the satisfiability problem for a system S of positive constraints is shown to be equivalent to deciding whether a certain finite hypergraph constructed from S has an induced subhypergraph that is closed (see Section 4). This characterization is used to obtain an exhaustive hierarchy of complexity results depending on the number of elements of Σ of each arity.

In this paper we consider systems of mixed positive and negative constraints. Negative constraints considerably increase the power of the constraint language and have important applications in program analysis. For example, in [3, 4], opportunities for program optimization are identified by an ad hoc technique for checking the satisfiability of systems of negative constraints. Set constraints with only nullary symbols correspond to Boolean algebras over a finite set of atoms; in [14] general results on solving negative constraints in arbitrary Boolean algebras are given.

In this paper we give a general decision procedure for determining whether a given system of mixed positive and negative constraints over an arbitrary signature is satisfiable. The proof reduces the satisfiability problem to a reachability problem involving Diophantine inequalities which may be of independent interest. We reduce the satisfiability problem to the Diophantine problem and then show that the Diophantine problem is decidable. The proof has a nonconstructive step involving Dickson’s Lemma and does not give any complexity bounds.

The decidability result for systems of positive and negative set constraints has recently been obtained independently by Gilleron, Tison, and Tommasi [10] using automata-theoretic techniques.

2 Set Expressions and Set Constraints

There is some variation in the literature regarding the definition of set expressions and set constraints, depending on the operations allowed. The following definition is taken from [1].

Let Σ be a finite ranked alphabet consisting of symbols f, each with an associated arity arity(f) ∈ ℕ. Symbols in Σ of arity 0, 1, 2, and n are called nullary, unary, binary, and n-ary, respectively. Nullary elements are often called constants. The set of elements of Σ of arity n is denoted Σ_{n}.

The set of ground terms over Σ is denoted T_{Σ}. This is the smallest set such that if t_{1}, …, t_{n} ∈ T_{Σ} and f ∈ Σ_{n}, then ft_{1} … t_{n} ∈ T_{Σ}. If X = {x, y, …} is a set of variables, then T_{Σ}(X) denotes the set of terms over Σ and X, considering the elements of X as symbols of arity 0.

Let B = (∪, ∩, ∼, 0, 1) be the usual signature of Boolean algebra. Other Boolean operators such as ⊕ (symmetric difference) are defined from these as usual. Let Σ + B denote the signature consisting of the disjoint union of Σ and B. A set expression over X is any element of T_{Σ+B}(X). The following is a typical set expression:

f(g(x ∪ y), ∼g(x ∩ y)) ∪ a

where f ∈ Σ_{2}, g ∈ Σ_{1}, a ∈ Σ_{0}, and x, y ∈ X. We use E, F, … to denote set expressions. A Boolean expression over X is any element of T_{B}(X).

A positive set constraint is a formal inclusion E ⊆ F, where E and F are set expressions. We also allow equational constraints E = F, although inclusions and equations are interdefinable: E ⊆ F is equivalent to E ∪ F = F, and E = F is equivalent to E ⊕ F ⊆ 0. A negative set constraint is the negation of a positive set constraint: E ⊈ F or E ≠ F.

We interpret set expressions over the powerset 2^{T_{Σ}} of T_{Σ}. This forms an algebra of signature Σ + B where the Boolean operators have their usual settheoretic interpretations and elements f ∈ Σ_{n} are interpreted as functions f : (2^{T_{Σ}})^{n} → 2^{T_{Σ}} such that

f(A_{1}, …, A_{n}) = {ft_{1} … t_{n} | t_{i} ∈ A_{i}, 1 ≤ i ≤ n} .

A set assignment is a map

σ : X → 2^{T_{Σ}}

assigning a subset of T_{Σ} to each variable in X. Any set assignment σ extends uniquely to a (Σ + B)-homomorphism

σ : T_{Σ+B}(X) → 2^{T_{Σ}}

by induction on the structure of the set expression in the usual way. The set assignment σ satisfies the positive constraint E ⊆ F if σ(E) ⊆ σ(F), and satisfies the negative constraint E ⊈ F if σ(E) ⊈ σ(F). We write σ ⊧ φ if the set assignment σ satisfies the constraint φ. A system S of set constraints is satisfiable if there is a set assignment σ that satisfies all the constraints in S; in this case we write σ ⊧ S. We write S ⊧ φ if all set assignments that satisfy S also satisfy φ. The satisfiability problem is to determine whether a given finite system S of set constraints over Σ is satisfiable.

A truth assignment is a map u : X → 2 where 2 = {0, 1} is the twoelement Boolean algebra. Any truth assignment u extends uniquely to a Bhomomorphism u : T_{B}(X) → 2 inductively according to the rules of Boolean algebra. If X = {x_{1}, …, x_{m}}, we use the notation

B[x_{i} := a_{i}]

to denote the truth value of the Boolean formula B under the truth assignment x_{i} ↦ a_{i}, 1 ≤ i ≤ m.

3 Expressibility

Systems of mixed positive and negative constraints are strictly more expressive than systems of positive constraints alone. We will prove this as a corollary of a general compactness theorem for positive constraints.

Theorem 3.1 (Compactness) A system S of positive set constraints is satisfiable if and only if all finite subsets of S are satisfiable.

Proof. The implication (⇒) is straightforward. For the other direction, suppose S is finitely satisfiable. We wish to construct a satisfying set assignment for S. By Zorn’s Lemma, there exists a maximal finitely satisfiable set Ŝ of positive constraints containing S. One can show that for all ground terms t and set expressions E, exactly one of the constraints t ⊆ E, t ⊆ ∼E is in Ŝ; if neither is in Ŝ, then Ŝ is not maximal, and if both are, then Ŝ is not finitely satisfiable. Now define a map

σ(E) = {t | t ⊆ E ∈ Ŝ} .

One can show by induction on the structure of set expressions that σ is a valid set assignment and satisfies Ŝ. For example, to show that

σ(fE_{1} … E_{n}) = {ft_{1} … t_{n} | t_{i} ∈ σ(E_{i}), 1 ≤ i ≤ n} ,

note

t ∈ σ(fE_{1} … E_{n}) ⟺ t ⊆ fE_{1} … E_{n} ∈ Ŝ .  (3.1)

Then t must be of the form ft_{1} … t_{n}, otherwise Ŝ would not be finitely satisfiable. Now we use the fact that

ft_{1} … t_{n} ⊆ fE_{1} … E_{n} ⊧ t_{i} ⊆ E_{i} , 1 ≤ i ≤ n
{t_{i} ⊆ E_{i} | 1 ≤ i ≤ n} ⊧ ft_{1} … t_{n} ⊆ fE_{1} … E_{n}

to argue that t ⊆ fE_{1} … E_{n} ∈ Ŝ iff t_{i} ⊆ E_{i} ∈ Ŝ, 1 ≤ i ≤ n, otherwise Ŝ would not be finitely satisfiable. Combining this with (3.1) and using the induction hypothesis, we get

t ∈ σ(fE_{1} … E_{n}) ⟺ t_{i} ∈ σ(E_{i}) , 1 ≤ i ≤ n .

To show that σ satisfies all constraints of Ŝ, let E ⊆ F be any constraint in Ŝ. For any term t,

t ∈ σ(E) ⇒ t ⊆ E ∈ Ŝ
⇒ t ⊆ F ∈ Ŝ  (3.2)
⇒ t ∈ σ(F) ;

the reason for the implication (3.2) is that

{t ⊆ E, E ⊆ F } ⊧ t ⊆ F ,

and if t ⊆ F were not in Ŝ, then t ⊆ ∼F would be, and Ŝ would not be finitely satisfiable. □

Corollary 3.2 Finite systems of mixed positive and negative constraints are strictly more expressive than systems of positive constraints only.

Proof. Consider the single negative constraint x ≠ 0 over any ranked alphabet Σ with at least one constant and at least one symbol of higher arity. Solutions are σ : {x} → T_{Σ} with σ(x) nonempty. Let S be any set, finite or infinite, of positive constraints over any set of variables X containing x. We claim that it is not the case that the set

{σ(x) | σ : X → T_{Σ}, σ ⊧ S}

is exactly the set of nonempty subsets of T_{Σ}.

Consider the infinite set of positive constraints

S ∪ {t ⊆ ∼x | t ∈ T_{Σ}} .

Either this is satisfiable or not. If so, then there is a satisfying set assignment σ. But t ∈ σ(∼x) for all terms t, so σ(x) = ∅ and σ ⊧ S, and the claim is verified. If not, then by compactness there is a finite subset F ⊆ T_{Σ} such that

S ∪ {t ⊆ ∼x | t ∈ F }

is not satisfiable. Therefore there is no solution σ of S with σ(x) = {t}, where t is any term not in F. □

4 Set Constraints and Hypergraph Closure

In [1] it is shown how to transform a given system of positive set constraints into an equivalent system in a special normal form. The transformation does not significantly increase the size of the system. Applying this transformation to a system containing negative constraints, we obtain the following normal form. Let X be a set of variables, and for each f ∈ Σ, let

Z_{f} = {z_{ix}^{f} | 0 ≤ i ≤ arity(f), x ∈ X}

be a set of variables such that the sets X and Z_{f}, f ∈ Σ are pairwise disjoint. A system of set constraints in normal form (with respect to X and the Z_{f}) consists of • a positive constraint B = 1, B ∈ T_{B}(X)

• for each f ∈ Σ, a positive constraint C_{f} = 1, C_{f} ∈ T_{B}(Z_{f})

• positive constraints

z_{0x}^{f} = f \underbrace{1 … 1}_{n} ∩ x
z_{ix}^{f} = f \underbrace{1 … 1}_{i−1} x \underbrace{1 … 1}_{n−i}

for each f ∈ Σ_{n} and each 1 ≤ i ≤ n and x ∈ X

• a finite set of negative constraints D ≠ 0, one for each element D of a given finite set D ⊆ T_{B}(X).

The last component is absent with positive constraints only.

As described in [1], a system of set constraints S in normal form determines a hypergraph

H = (U, E_{f} | f ∈ Σ)

as follows. The vertex set U is the set of all truth assignments u : X → 2 satisfying B. Each such truth assignment corresponds to a conjunction of literals (also denoted u) in which each variable in X occurs exactly once, either positively or negatively, such that u ⊆ B tautologically. The variable x occurs positively iff u(x) = 1. We often call the elements of U atoms because they represent atoms (minimal nonzero elements) of the free Boolean algebra on generators X modulo B = 1, where “minimal” is in the sense of the natural order on the Boolean algebra. It follows from elementary Boolean algebra that each Boolean expression over X is equivalent modulo B = 1 to a disjunction of atoms.

For each f ∈ Σ_{n}, the hyperedge relation E_{f} of H is defined to be the set of all (n + 1)-tuples (u_{0}, …, u_{n}) ∈ U^{n+1} such that

C_{f}[z_{ix}^{f} := u_{i}(x)] = 1 .  (4.3)

Intuitively, we think of the formula C_{f} as a Boolean-valued mapping on (n + 1)-tuples of truth assignments to X. To emphasize this intuition, we abbreviate the left hand side of (4.3) by

C_{f}[u_{0}, …, u_{n}] .

Thus

(u_{0}, …, u_{n}) ∈ E_{f} iff C_{f}[u_{0}, …, u_{n}] = 1 .

In general, the size of H can be exponential in the size of S.

An (n + 1)-ary hyperedge relation E_{f} of the hypergraph H is said to be closed if for each n-tuple u_{1}, …, u_{n} ∈ U^{n}, there exists u_{0} ∈ U such that (u_{0}, u_{1}, …, u_{n}) ∈ E_{f}. In the case n = 0, this definition just says E_{f} ∩ U ≠ ∅. Abusing notation, we can think of E_{f} as a function

E_{f} : U^{n} → 2^{U}

where

E_{f}(u_{1}, …, u_{n}) = {u_{0} | (u_{0}, u_{1}, …, u_{n}) ∈ E_{f}} .

In this view, E_{f} is closed iff E_{f}(u_{1}, …, u_{n}) ≠ ∅ for each n-tuple u_{1}, …, u_{n} ∈ U^{n}. The hypergraph H is said to be closed if all its hyperedge relations are closed.

The induced subhypergraph of H on vertices U′ ⊆ U is the hypergraph

H′ = (U′, E′_{f} | f ∈ Σ)

such that E′_{f} = E_{f} ∩ (U′)^{n+1} for f ∈ Σ_{n}.

The hypergraph closure problem is the problem of determining whether a given hypergraph H has a closed induced subhypergraph.

The following theorem was proved in [1].

Theorem 4.1 The hypergraph H corresponding to a system S of positive set constraints has a closed induced subhypergraph if and only if S is satisfiable.

In brief, the proof of [1] establishes a one-to-one correspondence between set assignments σ satisfying S and maps θ : T_{Σ} → U such that for all f ∈ Σ and for all terms ft_{1} … t_{n},

θ(ft_{1} … t_{n}) ∈ E_{f}(θ(t_{1}), …, θ(t_{n})) .  (4.4)

The set assignment corresponding to θ is

σ(x) = {t | θ(t)(x) = 1}
σ(z_{ix}^{f}) = σ(f \underbrace{1 … 1}_{i−1} x \underbrace{1 … 1}_{n−i})
σ(z_{0x}^{f}) = σ(f \underbrace{1 … 1}_{n} ∩ x) .

Thus deciding the satisfiability of S is tantamount to determining the existence of a map θ satisfying (4.4). In turn, this is equivalent to the hypergraph closure problem: if such a θ exists, then the induced subhypergraph of H on the image of θ is closed, and conversely, if there exists a closed induced subhypergraph on vertices U′ ⊆ U, then one can inductively define θ(ft_{1} … t_{n}) to be the lexicographically first element of U′ ∩ E_{f}(θ(t_{1}), …, θ(t_{n})).

In the presence of negative constraints D ≠ 0, D ∈ D, the map θ must not only satisfy (4.4), but must also take on some value u such that u(D) = 1 for each D ∈ D. Thus in the presence of negative constraints, the satisfiability problem becomes:

Problem 4.2 Given a finite set D of Boolean formulas D ∈ T_{B}(X) and a hypergraph H = (U, E_{f} | f ∈ Σ) specified by B ∈ T_{B}(X) and C_{f} ∈ T_{B}(Z_{f}), f ∈ Σ, determine whether there exists a map θ : T_{Σ} → U satisfying (4.4) such that

for each D ∈ D there exists an atom u in θ(T_{Σ}) satisfying D,  (4.5)

where θ(T_{Σ}) denotes the image of T_{Σ} under the map θ.

5 A Reachability Problem

Our decision procedure first reduces the satisfiability problem for mixed systems of positive and negative set constraints to a certain reachability problem involving Diophantine inequalities. In this section we define the reachability problem and give the reduction.

First we describe the reachability problem on an intuitive level. Let X be a set of variables ranging over ℕ, the natural numbers. Suppose we are given a finite system C of formal inequalities p ≤ q, where p and q are polynomials in the variables X with coefficients in ℕ, such that

• each left hand side p is a sum of variables in X

• each variable occurs in at most one left hand side.

An assignment is a map u : X → ℕ. Each assignment u extends uniquely to an evaluation morphism u : ℕ[X] → ℕ which evaluates polynomials at u. A variable x is said to be enabled under an assignment u if either • the variable x does not occur on the left hand side of any constraint in

C; or

• the unique constraint in C in which x appears on the left hand side is a strict inequality under the assignment u.

Consider the following nondeterministic procedure. Starting with the zero assignment, repeatedly choose a variable that is enabled and “fire” it by incrementing it by 1. The reachability problem is to decide whether there exists a sequence of legal firings that allows a particular distinguished variable to be fired.

We give a more rigorous presentation of this problem below, then reduce the satisfiability problem to this problem. In Section 6 we show that the reachability problem is decidable.

5.1 Polynomials and Assignments

We use the term ring to mean commutative ring with unit and semiring to mean commutative semiring with unit.

Let ℤ denote the ring of integers and ℕ ⊆ ℤ the semiring of natural numbers with the usual addition and multiplication operations. For X a finite set of variables, let ℤ[X] denote the ring of polynomials in the variables X with integer coefficients and ℕ[X] ⊆ ℤ[X] the semiring of polynomials with positive coefficients. The ring ℤ[X] is the free ring on generators X and the semiring ℕ[X] is the free semiring on generators X.

Any map u : X → R to a ring R extends uniquely to a ring homomorphism u : ℤ[X] → R. If S is a semiring and S ⊆ R, and if u(x) ∈ S for x ∈ X, then the restriction of u : ℤ[X] → R to domain ℕ[X] is a semiring homomorphism ℕ[X] → S, and is the unique semiring homomorphism extending u : X → S. We will concentrate on the case S = ℕ and R = ℤ; we call such a map an assignment. However, functional composition of polynomials is effected by the same construction with S = ℕ[X] and R = ℤ[X].

Intuitively, an assignment u : X → ℕ should be regarded as an assignment of values to the variables, and u(q) the result of evaluating the polynomial q on those values.

The set of assignments, considered as functions of X, forms a commutative monoid V under pointwise addition u + v : x ↦ u(x) + v(x), x ∈ X, with identity element the zero assignment 0 : x ↦ 0, x ∈ X. The monoid V is isomorphic to the commutative monoid ℕ^{|X|} with ordinary addition under the map v ↦ (v(x) | x ∈ X).

Care must be taken here: it is not the case that (u + v)(q) = u(q) + v(q) for q ∈ ℤ[X] in general. The value of (u + v)(q) is governed by the definition of the unique extension of assignments to homomorphisms. For example,

(u + v)(x + 1) = (u + v)(x) + (u + v)(1) = u(x) + v(x) + 1 ,

whereas

u(x + 1) + v(x + 1) = u(x) + v(x) + 2 .

However, we do have the following useful inequality:

Lemma 5.1 For any q ∈ ℕ[X],

(u + v)(q) ≥ u(q) + v(q) − 0(q)

with equality holding if q is affine (i.e., linear plus a constant term).

Proof. This can be proved by induction on the form of q. Note that 0(q) is the constant term of q. For x ∈ X, we have (u + v)(x) = u(x) + v(x), and for constants a ∈ ℕ, (u + v)(a) = a = u(a) + v(a) − 0(a). For polynomials of the form pq where neither p nor q has a constant term,

(u + v)(pq) = (u + v)(p) · (u + v)(q)
≥ (u(p) + v(p)) · (u(q) + v(q))
≥ u(p) · u(q) + v(p) · v(q)
= u(pq) + v(pq) .

Finally, for polynomials of the form p + q,

(u + v)(p + q) = (u + v)(p) + (u + v)(q)
≥ u(p) + v(p) − 0(p) + u(q) + v(q) − 0(q)
= u(p + q) + v(p + q) − 0(p + q)

with equality holding if p and q are affine, by the induction hypothesis. □

In particular, (u + v)(q) = u(q) + v(q) if q is linear with constant coefficient 0.

For v : X → ℕ an assignment, let inc_{v} : ℤ[X] → ℤ[X] be the unique ring homomorphism such that

inc_{v}(x) = x + v(x) , x ∈ X .

Informally, inc_{v}(p) is the polynomial obtained from p by substituting x+v(x) for x. Intuitively, inc_{v} says, “Automatically increase the value of x ∈ X by v(x).” Restricted to domain ℕ[X], inc_{v} is a semiring homomorphism ℕ[X] → ℕ[X], for which we use the same name.

The homomorphism inc_{v} is the unique map such that the diagram

[figure: ℤ[X]; ℤ[X]; ℤ; u + v; u; inc_{v}]  (5.6)

commutes, i.e. such that u ∘ inc_{v} = u + v: for x ∈ X,

(u + v)(x) = u(x) + v(x)
= u(x + v(x))  (5.7)
= u(inc_{v}(x)) .

Equation (5.7) holds since v(x) is a constant. Since the homomorphisms u+v and u ∘ inc_{v} agree on X, they agree everywhere. The homomorphism inc_{v} is unique, since it is determined by its values on x ∈ X, and the polynomial inc_{v}(x) is determined by its set of values u(inc_{v}(x)) = u(x) + v(x).

By composing two copies of (5.6), one observes that the set

I = {inc_{v} | v an assignment}

forms a monoid under functional composition ∘ with identity inc_{0}. Moreover, I is isomorphic to the monoid of assignments V under the map v ↦ inc_{v}; i.e.,

inc_{u+v} = inc_{u} ∘ inc_{v} .

The map v ↦ inc_{v} is bijective, since v can be recovered uniquely from inc_{v} by taking u = 0 in (5.7).

It follows immediately that inc_{u} and inc_{v} commute under composition, i.e. inc_{u} ∘ inc_{v} = inc_{v} ∘ inc_{u}.

One application of particular importance will be incrementing the value of a variable x under an assignment u by 1. The new assignment is u + δ_{x}, where δ_{x}(x) = 1 and δ_{x}(y) = 0 for y ≠ x. The effect of applying inc_{δ_{x}} to a polynomial q is the same as substituting x + 1 for x in q.

Let X∗ denote the monoid of finite-length strings over X. This is the free monoid on generators X. Elements of X∗ will be denoted σ, τ, ρ, …

There is a unique monoid homomorphism [[ ]] : X∗ → V extending the map x → δ_{x}, x ∈ X. The image of σ = x_{1} ⋯ x_{n} under this map is [[σ]] = ∑_{i=1}^{n} δ_{x_{i}}. Applied to x, the function [[σ]] gives the number of occurrences of x in the string σ. This is known in formal language theory as the Parikh map. By a slight abuse of notation, we omit the braces [[ ]] when using [[σ]] as a function; thus σ(x) denotes the number of occurrences of x in σ, and σ(q) is the value of the polynomial q under the assignment [[σ]].

5.2 Systems of Diophantine Inequalities

We consider finite systems C of Diophantine inequalities of the form p ≤ q where p, q ∈ ℕ[X] such that

• each left hand side p is a sum of distinct variables; and

• each variable in X occurs in at most one left hand side.

There is no restriction on the form of the right hand sides q except that they be in ℕ[X]. The inequalities in C are called (Diophantine) constraints. A variable x ∈ X is said to be constrained in C if x occurs on the left hand side of some constraint in C. In this case we denote the unique such constraint by con (x, C). If x does not occur on the left hand side of any constraint in C, then x is said to be unconstrained in C, and we write con (x, C) = ∗.

We say that the assignment u satisfies the constraint p ≤ q if u(p) ≤ u(q). We say that u satisfies C if u satisfies all the constraints in C. We say that σ ∈ X∗ satisfies a constraint or set of constraints if [[σ]] does.

5.3 The Nonlinear Reachability Problem

Let C be a system of Diophantine constraints as described above and let x_{0} ∈ X be a fixed distinguished variable.

Definition 5.2 Let σ ∈ X∗. The constraint p ≤ q ∈ C is said to be σenabled if σ(p) < σ(q); i.e., the inequality is strict under the assignment [[σ]]. The variable x ∈ X is said to be (σ, C)-enabled if either

• x is unconstrained in C, or

• x is constrained in C and con (x, C) is σ-enabled.

□

A tree, for our purposes, is a nonempty prefix-closed subset T of X∗. The root of T is ϵ. The parent of σ ≠ ϵ is the longest proper prefix of σ. A leaf of T is an element of T that is not a parent. A path of T is a maximal subset of T linearly ordered by the prefix relation.

The system C gives rise to a tree

T_{C} = {σ ∈ X∗ | for all prefixes τx of σ, x is (τ, C)-enabled.}

The tree T_{C} describes the possible legal sequences of firings that can take place according to the informal description of the nonlinear reachability problem given in Section 5.

Definition 5.3 The Nonlinear Reachability Problem (NRP) is to determine, given C, whether T_{C} contains an element σ such that σ(x_{0}) > 0. Such a σ is called a solution of the given instance C of the NRP. □

In other words, determine whether there exists a legal firing sequence such that the distinguished variable x_{0} is fired.

Note that ϵ satisfies C since [[ϵ]] = 0, and if σ satisfies C and x is (σ, C)- enabled, then σx satisfies C, since [[σx]] = [[σ]] + δ_{x}. It follows by induction that σ satisfies C for every σ ∈ T_{C}. In other words, if σ satisfies C and x is (σ, C)-enabled, then we can fire x and the resulting assignment still satisfies C. The converse is false in general; i.e., it is possible that both σ and σx satisfy C but x is not (σ, C)-enabled: consider the constraint x ≤ x.

5.4 Reduction of Set Constraint Satisfiability to Nonlinear Reachability

Theorem 5.4 The satisfiability problem for systems of mixed positive and negative set constraints reduces effectively to a finite disjunction of instances of the Nonlinear Reachability Problem.

Proof. As argued in Section 4, the satisfiability problem for systems of mixed positive and negative constraints is equivalent to Problem 4.2. Using the notation of Problem 4.2, let U be the set of all subsets V ⊆ U such that for all D ∈ D there exists a v ∈ V with v(D) = 1. Consider a modified version of Problem 4.2 in which condition (4.5) is replaced by the condition

V ⊆ θ(T_{Σ}) .  (5.8)

Then Problem 4.2 is equivalent to the disjunction over all V ∈ U of instances of the modified version. Furthermore, we will only need to construct a finite partial approximation θ′ to θ satisfying (4.4) and (5.8), provided

• the domain of θ′ is closed downward under the subterm relation

• there is a closed induced subhypergraph of H containing the image of θ′.

The second property will allow θ′ to be completed to a total function θ, as described below.

Thus the problem now becomes:

Problem 5.5 Given a hypergraph H = (U, E_{f} | f ∈ Σ) specified by B and C_{f}, f ∈ Σ, and a subset V ⊆ U, determine whether there exist U′ ⊆ U and a partial map θ : T_{Σ} → U′ with finite domain such that

• the induced subhypergraph on U′ is closed

• the domain of θ is closed downward under the subterm relation

• θ satisfies (4.4) on all terms in its domain

• V ⊆ θ(T_{Σ}) ⊆ U′.

Consider the following nondeterministic procedure for constructing θ. We first guess the subset U′ containing the target set V and check that it is closed. We start with θ totally undefined. At any point, say we have a partial θ with finite domain closed downward under the subterm relation. We nondeterministically pick some term ft_{1} … t_{n} such that the θ(t_{i}) are defined but θ(ft_{1} … t_{n}) is not yet defined, nondeterministically choose some u in E_{f}(θ(t_{1}), …, θ(t_{n})) ∩ U′, and assign θ(ft_{1} … t_{n}) := u. We are always able to continue, since U′ is closed. We halt successfully when and if all elements of V have been chosen as θ(t) for some t.

During this process, we use an integer variable x_{u,f,u_{1},...,u_{n}}, n = arity(f), to count the number of terms of the form ft_{1} … t_{n} such that

• θ(t_{i}) exists and equals u_{i}, 1 ≤ i ≤ n, and

• θ(ft_{1} … t_{n}) exists and equals u.

There is one such variable for each choice of f in Σ, u_{1}, …, u_{n} ∈ U′ where n = arity(f), and u ∈ U′ ∩ E_{f}(u_{1}, …, u_{n}).

Now for each f ∈ Σ_{n} and u_{1}, …, u_{n} ∈ U′, consider the formal inequality

∑_{u∈U′∩E_{f} (u_{1},...,u_{n})} x_{u,f,u_{1},...,u_{n}} ≤ ∏_{i=1}^{n} ∑_{m=0}^{M} ∑_{\begin{matrix}v_{1}, …, v_{m} ∈ U′ \\ g ∈ Σ_{m} \end{matrix}} x_{u_{i},g,v_{1},...,v_{m}} (5.9)

where M is the maximum arity of symbols in Σ. This inequality has the following significance. Given a partial map θ, let

B_{u} = {t | θ(t) exists and equals u}
A_{f,u_{1},...,u_{n}} = {ft_{1} … t_{n} | t_{i} ∈ B_{u_{i}}, 1 ≤ i ≤ n} .

The value of the right hand side of (5.9) is the size of A_{f,u_{1},...,u_{n}}, which is the the size of the direct product B_{u_{1}} × ⋯ × B_{u_{n}}. The value of the left hand side of (5.9) is the size of the subset of A_{f,u_{1},...,u_{n}} consisting of all elements t for which θ(t) is defined. The inequality expresses the fact that θ is defined on the subterms of t before being defined on t.

Consider the collection C of all such inequalities (5.9). To say that a variable x_{u,f,u_{1},...,u_{n}} is enabled says that there exists a term t with head symbol f such that θ is defined on the n immediate subterms and takes values u_{1}, …, u_{n} on those subterms respectively, but θ(t) is not yet defined. To fire x_{u,f,u_{1},...,u_{n}} says that we choose one such t and define θ(t) := u.

The process of defining θ from the bottom up as described above corresponds to a sequence of legal firings. Conversely, any legal sequence of firings gives a corresponding sequence of definitions of θ starting with the totally undefined map.

We have thus reduced the satisfiability problem for systems of mixed positive and negative set constraints to a disjunction of instances of the problem of determining, given C and V, whether there is a finite sequence of legal firings after which for all v ∈ V there are f and u_{1}, …, u_{n} such that the value of x_{v,f,u_{1},...,u_{n}} is nonzero.

We reduce this problem to a finite disjunction of instances of the NRP as follows. For each v ∈ V, choose f and u_{1}, …, u_{n} and let y_{v} = x_{v,f,u_{1},...,u_{n}}. Add the constraint

x_{0} ≤ ∏_{v∈V} y_{v}

where x_{0} is a new variable, and make x_{0} the distinguished variable of the NRP so obtained. The variable x_{0} can be fired only after all the y_{v} have been fired. The problem above is equivalent to the disjunction of all such instances of the NRP over all possible choices of the y_{v}. □

6 Decidability of the Nonlinear Reachability Problem

In this section we prove the decidability of the NRP. We will start by defining several technical concepts on which our proof is based and deriving their basic properties. The most important of these concepts are the notions of exposed and inhibited variables and admissible strings. Intuitively, a variable is exposed in a polynomial q if incrementing it causes the value of q to increase. The intuition behind the definition inhibited variable is that it does no good to increment such a variable under the current state of affairs. A string σ is admissible if it never increments any inhibited variable. We show that if there exists a solution, then there exists an admissible one. The final argument shows that if we construct the tree T_{C} breadth-first, ignoring nonadmissible strings, then along any path we will eventually encounter either a solution, a leaf with no admissible extensions, or a configuration that allows us to reduce the size of the system.

6.1 Reset

We first describe a useful technical device called a reset. Intuitively, after executing a firing sequence σ that is legal with respect to a set of constraints C, we can construct a new instance of the problem inc_{σ}(C) (defined below) which allows us to proceed as if we were starting afresh.

Definition 6.1 Let C be a system of Diophantine constraints as defined in Section 5.2. If σ ∈ T_{C}, we define T_{C}^{σ} to be the subtree of T_{C} rooted at σ:

T_{C}^{σ} = {τ ∈ X∗ | στ ∈ T_{C}} .

This set is nonempty and prefix-closed, therefore a tree. □

Note that [[σ]] alone determines whether a variable is σ-enabled. It follows inductively that if σ, τ ∈ T_{C} and [[σ]] = [[τ]], then T_{C}^{σ} = T_{C}^{τ}.

Let v be any assignment satisfying C, and let inc_{v} be as in Section 5.1. Let inc_{v}(C) denote the system of constraints

inc_{v}(C) = {p ≤ inc_{v}(q) − v(p) | p ≤ q ∈ C} .

The right hand sides inc_{v}(q)−v(p) are in ℕ[X], since the constant coefficient of inc_{v}(q) is at least v(p). This is a consequence of the fact that v satisfies C:

v(p) ≤ v(q) = 0(inc_{v}(q)) .

Moreover, x is constrained in C iff it is constrained in inc_{v}(C), since all the left hand sides are the same.

Note also that the constraint p ≤ inc_{v}(q) − v(p) ∈ inc_{v}(C) is equivalent to inc_{v}(p) ≤ inc_{v}(q), since inc_{v}(p) = p + v(p) for p a sum of variables.

Lemma 6.2 Let C be a set of constraints and σ ∈ T_{C}. Then

T_{C}^{σ} = T_{inc_{σ}(C)} .

Proof. Certainly ϵ is a member of both trees. Moreover, for any constraint p ≤ q ∈ C, we have from (5.6) that

τ(inc_{σ}(q − p)) = στ(q − p) ,

and con (x, C) = con (x, inc_{σ}(C)), thus x is (τ, inc_{σ}(C))-enabled iff x is (στ, C)-enabled. Thus the trees are identical. □

6.2 Order

Our algorithm will construct part of the tree T_{C}. During this construction, we will want to keep track of the values of q − p for p ≤ q ∈ C, since this information will help us determine when we have reached a situation in which progress has been made. We define the order ≤_{C} for this purpose. We also define the order ≤_{X}, which is just the natural order on the set of assignments.

Definition 6.3 For C a system of constraints and σ, τ ∈ X∗, define

• σ ≤_{X} τ if σ(x) ≤ τ(x) for all x ∈ X

• σ ≤_{C} τ if σ(q − p) ≤ τ(q − p) for all p ≤ q ∈ C

• σ ≤_{X,C} τ if both σ ≤_{X} τ and σ ≤_{C} τ

• σ ≡_{C} τ if both σ ≤_{C} τ and τ ≤_{C} σ.

□

It follows from Lemma 5.1 and the observation that 0(q) is the constant coefficient of q that for q ∈ ℕ[X], if σ ≤_{X} τ then σ(q) ≤ τ(q).

Note that the relations ≤_{X} and ≤_{C} depend only on the assignments [[σ]] and not on the strings σ themselves. Note also that if στ ∈ T_{C} then σ ≤_{X} στ. The same statement is not true in general for ≤_{C}; for example, take σ = ϵ, τ = x, and C = {x ≤ y + 1}.

Lemma 6.4 Let x ∈ X, σ, τ ∈ X∗ such that σ ≤_{X} τ, and p ≤ q ∈ C. Then

σx(q − p) − σ(q − p) ≤ τx(q − p) − τ(q − p) .

Proof. Using Lemma 5.1 and the facts that [[σx]] = [[σ]]+δ_{x} and p is linear, it follows that the inequality in the statement of the Lemma is equivalent to

σx(q) − σ(q) ≤ τx(q) − τ(q) .

By (5.6), this is equivalent to

σ(inc_{x}(q) − q) ≤ τ(inc_{x}(q) − q) .

But this inequality follows from the assumptions of the Lemma, since σ ≤_{X} τ and inc_{x}(q) − q ∈ ℕ[X]. □

Lemma 6.5 Let σ, τ ∈ T_{C} and x ∈ X.

(i) If x is (σ, C)-enabled and σ ≤_{C} τ, then x is (τ, C)-enabled.

(ii) If σ ≤_{X} τ then σx ≤_{X} τx.

(iii) If σ ≤_{X,C} τ, then σx ≤_{X,C} τx.

Proof. The assertions (i) and (ii) are straightforward consequences of the definitions. The assertion (iii) follows from (ii) and Lemma 6.4. □

6.3 Well Partial Orders and Dickson’s Lemma

A well partial order is a partially ordered set in which every infinite sequence has an infinite monotone nondecreasing subsequence. That is, for every infinite sequence d_{0}, d_{1}, …, there exist indices i_{0} < i_{1} < ⋯ such that d_{i_{0}} ≤ d_{i_{1}} ≤ · · ·.

Lemma 6.6 (Dickson’s Lemma) The set ℕ^{k} of k-tuples of natural numbers under the componentwise order is a well partial order.

For a proof of Dickson’s Lemma, see [8].

We will use Dickson’s Lemma in the argument below to conclude that along any infinite path in T_{C}, we must eventually have σ ≤_{C} στ. Here we are taking k = |C| and comparing the k-tuples (σ(q − p) | p ≤ q ∈ C).

6.4 Exposed Variables

Intuitively, a variable x is σ-exposed in a polynomial q iff, after executing σ, firing x would cause the value of q to increase strictly. The following definition and lemma make this intuition precise.

Definition 6.7 Let x ∈ X and σ ∈ T_{C}. We say that x is σ-exposed in a monomial qx^{i}, where x does not appear in q, if i ≥ 1 and σ(q) ≠ 0. For q ∈ ℕ[X], we say that x is σ-exposed in q if x is σ-exposed in some monomial of q. We say that x is (σ, C)-exposed if x is σ-exposed in q for some p ≤ q ∈ C.

□

Lemma 6.8 Let x ∈ X, q ∈ ℕ[X], and σ ∈ T_{C}. Then x is σ-exposed in q iff σ(q) < σx(q).

Proof. Since σ and σx are homomorphisms and all values are nonnegative, it suffices to show the result for monomials ax^{i}, a ∈ ℕ[X − {x}]. Since σx(a) = σ(a),

σx(ax^{i}) − σ(ax^{i}) = σ(a)((σ(x) + 1)^{i} − σ(x)^{i}) ≥ 0 ,

with equality holding iff i = 0 or σ(a) = 0. □

The following lemma establishes some basic properties of the notion of exposure and its relation to enabling and the relation ≤_{C}.

Lemma 6.9 Let x ∈ X, p ≤ q ∈ C, and σ, τ ∈ T_{C}.

(i) If x is σ-exposed in q and σ ≤_{X} τ, then x is τ-exposed in q (once exposed, always exposed).

(ii) If x is σ-exposed in q, then σx(q − p) ≥ σ(q − p); moreover, if x does not occur in p, then the inequality is strict.

(iii) If x is not (σ, C)-exposed, then σx ≤_{C} σ.

(iv) The property of exposure in the right hand side of a constraint p ≤ q ∈ C is preserved under a reset. Formally, x is στ-exposed in q iff x is τ-exposed in inc_{σ}(q) − σ(p).

(v) If σ(x) > 0, x is not σ-exposed in q, and x is σy-exposed in q, then y is σ-exposed in q.

Proof. Except for (iv) and (v), all statements are direct consequences of Definition 6.7 and Lemma 6.8.

To prove (iv), we use (5.6) and Lemma 6.8:

στx(q) − στ(q) = τx(inc_{σ}(q)) − τ(inc_{σ}(q))
= τx(inc_{σ}(q) − σ(p)) − τ(inc_{σ}(q) − σ(p)) ,

since σ(p) is a constant.

For (v), there must be a monomial ax^{i} of q, i ≥ 1, a ∈ ℕ[X − {x}], such that σ(a) = 0 and σy(a) > 0. Then y ≠ x, since x does not appear in a. Since σ(x) = σy(x) > 0, we have σ(ax^{i}) = 0 and σy(ax^{i}) > 0, thus σy(q) > σ(q). By Lemma 6.8, y is σ-exposed in q. □

6.5 Inhibited Variables and Admissible Strings

The technical notion of an inhibited variable captures the idea that, under the current state of affairs, firing the variable makes no progress toward a solution. Intuitively, firing a variable makes progress only if the variable is exposed, so that firing it might enable another variable, or has value 0, so that firing it might contribute to the exposure of another variable.

We will formalize and prove a result that says intuitively that any string σ can be simulated by another string τ in which no inhibited variable is ever fired. Such a string τ is called admissible.

Definition 6.10 Let C be a system of Diophantine constraints and σ ∈ T_{C}. We say x ∈ X is (σ, C)-inhibited if

• x is unconstrained in C,

• x is not (σ, C)-exposed, and

• σ(x) > 0.

We say that σ ∈ X∗ is C-admissible if σ ∈ T_{C}, and for all prefixes τy of σ, y is not (τ, C)-inhibited. □

Lemma 6.11 (i) If y is (σ, C)-inhibited, then σ(p) = σy(p) and σ(q) = σy(q) for all constraints p ≤ q ∈ C. In particular, σy ≡_{C} σ.

(ii) If y, z are (σ, C)-inhibited, then z is (σy, C)-inhibited. (This also applies to the case y = z.)

Proof.

(i) Since y is unconstrained, it does not appear in p, therefore σ(p) = σy(p). Since y is not σ-exposed in q, we have σ(q) = σy(q) by Lemma 6.8.

(ii) Surely σy(z) ≥ σ(z) > 0 and z is still unconstrained in C. To show that z is not (σy, C)-exposed, consider an arbitrary term ay^{i}z^{j} of q, where p ≤ q ∈ C, j ≥ 1, and a ∈ ℕ[X − {y, z}]. (If y = z, take i = 0.) We want to show that σy(ay^{i}) = 0. Since z is (σ, C)-inhibited, we have σ(ay^{i}) = 0. Since y is (σ, C)-inhibited, we have σ(y) > 0, thus σ(a) = 0. Since y does not occur in a, we have σy(a) = σ(inc_{y}(a)) = 0, therefore σy(ay^{i}) = σy(a) · σy(y^{i}) = 0.

□

The following two lemmas imply that we can restrict our attention to admissible strings when looking for solutions.

Lemma 6.12 For every σ ∈ T_{C}, there exists a C-admissible string τ ∈ T_{C} such that σ ≤_{C} τ.

Proof. Let us call a prefix σ_{1}y of σ bad if y is (σ_{1}, C)-inhibited. The proof is by lexicographical induction on the length of σ; among strings of the same length, the number of bad prefixes; and among strings of the same length and same number of bad prefixes, the length of the longest bad prefix (“longer” is “smaller” in the induction). If σ is null or has no bad prefix, there is nothing to prove. If the longest bad prefix σ_{1}y is σ itself, then since y is not (σ_{1}, C)-exposed, we have by Lemma 6.9(iii) that σ_{1}y ≤_{C} σ_{1}, and we are done by the induction hypothesis. Otherwise, there exists a z and σ_{2} such that σ = σ_{1}yzσ_{2}. Now z is not (σ_{1}y, C)-inhibited, by the maximality of σ_{1}y. Neither is it (σ_{1}, C)-inhibited, by Lemma 6.11(ii). Moreover, z is (σ_{1}, C)-enabled, by Lemma 6.11(i) and the fact that it is (σ_{1}y, C)-enabled, and y is (σ_{1}z, C)-enabled since it is unconstrained. Therefore σ_{1}zyσ_{2} ∈ T_{C} is of the same length as σ, but with either strictly fewer bad prefixes (if σ_{1}zy is not a bad prefix) or the same number of bad prefixes and a strictly longer maximal one (if it is). The result follows from the induction hypothesis. □

Lemma 6.13 If a given instance of the NRP with constraints C has a solution, then it has an admissible solution.

Proof. Let σ be a solution of minimal length. Then σ is of the form τx_{0} and τ(x_{0}) = 0. By Lemma 6.12, there exists an admissible ρ such that τ ≤_{C} ρ. If ρ(x_{0}) > 0, then ρ is the desired admissible solution. Otherwise, x_{0} is (ρ, C)-enabled (since τ ≤_{C} ρ and x_{0} is (τ, C)-enabled) and not (ρ, C)- inhibited (since ρ(x_{0}) = 0), therefore ρx_{0} is the desired admissible solution.

□

6.6 The Graphs H(σ, C)

We now describe a family of graphs H(σ, C) defined in terms of a given system C of constraints and σ ∈ T_{C}. The purpose of these graphs is to keep track of the exposed variables and how firing them can enable other constraints, so that we can monitor the progress of a firing sequence.

Formally, H(σ, C) is a finite labeled directed graph with vertices C ∪ {∗}. For each p ≤ q ∈ C and x ∈ X such that x is σ-exposed in q, there is an edge labeled x from con (x, C) to p ≤ q. (Recall that con (x, C) is ∗ if x is unconstrained in C, otherwise con (x, C) is some constraint p ≤ q ∈ C.) Selfloops are allowed in this definition: if x is constrained in C by the constraint p ≤ q and x is σ-exposed in q, H(σ, C) has a self-loop labeled x on the vertex p ≤ q.

It follows from Lemma 6.9(i) that if σ ≤_{X} τ then H(σ, C) is a subgraph of H(τ, C). In particular, H(σ, C) is a subgraph of H(σx, C). Moreover, it follows from Lemma 6.9(ii) that if σ ∈ T_{C}, x is (σ, C)-enabled, and H(σ, C) contains an edge labeled x into p ≤ q, then p ≤ q is σx-enabled.

We can think of H(σ, C) as a net in which tokens are passed around as variables are fired. Firing a variable x causes at least one token to be passed from con (x, C) along all edges labeled x to other constraints in which x is exposed, enabling those constraints. The number of tokens that are passed depends on the values of σ(q − p) for p ≤ q ∈ C, but by Lemma 6.9(ii), it is always at least one.

Lemma 6.14 Let στ ∈ T_{C} such that σ ≤_{C} στ. Assume further that τ contains at least one variable constrained in C. Then H(στ, C) contains either a cycle all of whose labels are in τ or an edge out of ∗ whose label is in τ.

Proof. Let x be constrained in C by the constraint p ≤ q, and suppose that x occurs in τ at least once. Then σ(p) < στ(p). Also, σ(q −p) ≤ στ(q − p), since σ ≤_{C} στ. Combining these inequalities, we obtain σ(q) < στ(q). By Lemma 6.8, there must be a y ∈ X and a prefix ρy of τ such that y is σρ-exposed in q. Then H(σρ, C) contains an edge labeled y from con (y, C) to con (x, C). Since H(σρ, C) is a subgraph of H(στ, C), this edge also exists in H(στ, C).

Now either y is unconstrained in C, in which case con (y, C) = ∗ and we are done, or we can continue in the same fashion with y. Following these edges backwards, we must eventually either arrive at ∗ or cycle. □

6.7 Equivalence of Problem Instances

In our decidability proof, we will show that as a computation σ unfolds, the graph H(σ, C) develops in certain ways that occasionally allow us to simplify C, for instance by discarding a constraint or a variable. In such cases we will construct a new system D that is structurally simpler than C but equivalent in the sense that D has a solution iff C does. The following definition gives the formal notion of equivalence of systems that we have in mind.

Definition 6.15 Let C, D be systems of constraints. We write C ≤ D if for every σ ∈ T_{C} there is a τ ∈ T_{D} such that σ ≤_{X} τ. We write C ≡ D and say that C and D are equivalent if both C ≤ D and D ≤ C. □

It follows immediately from this definition that if C ≡ D, then C has a solution if and only if D does.

6.8 Proof of Decidability

Let C be a system of Diophantine constraints. The following three lemmas, Lemmas 6.16, 6.17, and 6.18, identify three situations that will allow a structural simplification of the system C. We suggest that the reader skip the proofs of these lemmas on first reading and go directly to Theorem 6.19.

Lemma 6.16 Let p ≤ q ∈ C. If C has an unconstrained variable 0-exposed in q, then

C ≡ C − {p ≤ q} .

Proof. Let C′ = C − {p ≤ q}. The easier direction is C ≤ C′. If y is (σ, C)-enabled then y is also (σ, C′)-enabled, since y is either constrained by the same constraint in C and C′ or unconstrained in C′. It follows that T_{C} ⊆ T_{C′}.

For the other direction, suppose σ ∈ T_{C′}. Let x be a C-unconstrained variable 0-exposed in q. Let n = |σ| and let

τ = \underbrace{xx ⋯ x}_{n} σ = x^{n}σ .

Then σ ≤_{X} τ. We show that τ ∈ T_{C}. Certainly x^{n} ∈ T_{C}, since x is unconstrained. It remains to show that σ ∈ T_{C}^{x^{n}}. Resetting and using Lemma 6.2, it suffices to show σ ∈ T_{inc_{x^{n}}(C)}. Thus we need to show that for any prefix ρy of σ, y is (ρ, inc_{x^{n}}(C))-enabled. This follows from the fact that y is (ρ, C′)-enabled: for any f ≤ g ∈ C′,

ρ(inc_{x^{n}}(g − f)) = ρx^{n}(g) − ρ(f)  since x does not occur in f
≥ ρ(g − f) ,

and for the constraint p ≤ q,

ρ(inc_{x^{n}}(q − p)) = ρx^{n}(q) − ρ(p)  since x does not occur in p
≥ ρ(q) + n − ρ(p)  by Lemmas 6.8 and 6.9(i)
≥ ρ(q) + n − |ρ|  since p is linear
> 0  since |ρ| < n.
□

Lemmas 6.17 and 6.18 deal with two different kinds of cycles that can arise in H(σ, C). The first is used when the cycle is a self-loop on a single vertex, and the latter is used when the cycle has at least two vertices.

Lemma 6.17 If H(ϵ, C) has a self-loop labeled x on vertex p ≤ q, and if x is (0, C)-enabled, let

C′ = \{ \begin{matrix}(C − \{p ≤ q\}) ∪ \{p − x ≤ q − x\} , & if q − x ∈ ℕ[X] \\ C − \{p ≤ q\} , & otherwise. \end{matrix}

Then C ≡ C′.

Proof. Since x is 0-exposed in q, by Definition 6.7 that q has a term of the form ax^{k} where a, k ∈ ℕ and a, k ≥ 1; i.e., q can be written q′ + x^{k} with q′ ∈ ℕ[X]. If the first alternative in the definition of C′ holds, i.e. if q has a linear term ax, then we can take k = 1. If the second alternative holds, we can take k > 1. Let us call these two cases (i) and (ii), respectively. Either way, since con (x, C) is p ≤ q, x also occurs in p, and since p is linear, p = p′ + x for some p′ ∈ ℕ[X].

First we show C ≤ C′. This is immediate for case (ii) as in Lemma 6.16. For case (i), note that q − p = q′ − p′. Thus for any σ ∈ X∗, any variable y ∈ X − {x} is (σ, C)-enabled iff it is (σ, C′)-enabled, and since x is unconstrained in C′, x is always (σ, C′)-enabled. It follows that T_{C} ⊆ T_{C′}, thus C ≤ C′.

Now we show C′ ≤ C for both cases. Let σ ∈ T_{C′}, and let n = max{2, |σ|}. Let σ′ be obtained by deleting all occurrences of x from σ, and let τ = x^{n}σ′. Then σ ≤_{X} τ. We claim that τ ∈ T_{C}. Since x is 0-exposed in q and (0, C)- enabled, by Lemmas 6.8 and 6.9(i), x^{n} ∈ T_{C}, so we need only prove that σ′ ∈ T_{C}^{x^{n}}. Resetting by Lemma 6.2, it suffices to prove that σ′ ∈ T_{inc_{x^{n}}(C)}. We need to show that for any prefix ρ′y of σ′, y is (ρ′, inc_{x^{n}}(C))-enabled. This will follow from the fact that y is (ρ, C′)-enabled, where ρy is the unique prefix of σ such that ρ′y is ρy with all occurrences of x removed (note y ≠ x, since it occurs in σ′).

Suppose ρ has m occurrences of x. For any f ≤ g ∈ C − {p ≤ q},

ρ′(inc_{x^{n}}(g − f)) = ρ′x^{n}(g) − ρ(f)  since x does not occur in f
= ρx^{n−m}(g) − ρ(f)
≥ ρ(g) − ρ(f)
= ρ(g − f) .

For the argument involving constraint p ≤ q, we split on cases. In case (i),

ρ′(inc_{x^{n}}(q − p)) = ρ′x^{n}(q′ − p′)
= ρ′x^{n}(q′) − ρ(p′)  since x does not occur in p′
= ρx^{n−m}(q′) − ρ(p′)
≥ ρ(q′) − ρ(p′)
= ρ(q′ − p′) .

In case (ii),

ρ′(inc_{x^{n}}(q − p)) = ρ′x^{n}(q − p)
= ρ′x^{n}(q′) + ρ′x^{n}(x^{k}) − ρ′x^{n}(p′) − ρ′x^{n}(x)
≥ δ_{x}^{n}(x^{k}) − ρ′(p′) − δ_{x}^{n}(x)
≥ n^{k} − (n − 1) − n
≥ (n − 1)^{2}
> 0 .
□

Lemma 6.18 If there is a cycle in H(ϵ, C) on vertices

D = {p_{0} ≤ q_{0}, …, p_{n−1} ≤ q_{n−1}} ,

then C ≡ C′, where

p′ = ∑_{i=0}^{n−1} p_{i}
q′ = ∑_{i=0}^{n−1} q_{i}
C′ = (C − D) ∪ {p′ ≤ q′} .

Proof. First we show C ≤ C′. As above, it suffices to show that for any assignment σ ∈ T_{C} and variable y, if y is (σ, C)-enabled then y is (σ, C′)- enabled. If con (y, C) ∉ D, then con (y, C′) = con (y, C), thus y is (σ, C)- enabled iff it is (σ, C′)-enabled. Otherwise, if con (y, C) ∈ D, say p_{k} ≤ q_{k} for some 0 ≤ k ≤ n − 1, then con (y, C′) is p′ ≤ q′. Since σ ∈ T_{C}, we have σ(p_{i}) ≤ σ(q_{i}), 0 ≤ i ≤ n − 1. Moreover, since y is (σ, C)-enabled, we have σ(p_{k}) < σ(q_{k}). Thus σ(p′) < σ(q′), so y is (σ, C′)-enabled.

Now we show C′ ≤ C. Assume without loss of generality that the vertices in D occur on the cycle of H(ϵ, C) in the order p_{0} ≤ q_{0}, …, p_{n−1} ≤ q_{n−1} and that y_{i} is the label on the edge from p_{i} ≤ q_{i} to p_{i+1} ≤ q_{i+1}, 0 ≤ i ≤ n − 1 (arithmetic on subscripts is modulo n).

The intuitive idea behind the following argument is that if some y_{i} is enabled, then firing y_{i} enables y_{i+1}, and so on; thus we can imagine a token being passed around the cycle D, enabling whichever p_{j} ≤ q_{j} ∈ D is needed.

Let σ ∈ T_{C′}. We construct by induction on the length of σ a string σ′ ∈ T_{C} such that σ ≤_{X,C′} σ′. Define ϵ′ = ϵ. Now suppose σy ∈ T_{C′} and σ′ has been defined. By the induction hypothesis,

(i) σ ≤_{X,C′} σ′

(ii) σ′ ∈ T_{C}.

Since y is (σ, C′)-enabled, by (i) we have that y is (σ′, C′)-enabled.

If con (y, C) is in C − D or con (y, C) = ∗, let (σy)′ = σ′y. Then σy ≤_{X} (σy)′, and since con (y, C) = con (y, C′), y is (σ′, C)-enabled. Moreover, σy ≤_{C′} σ′y by Lemma 6.5(iii).

If con (y, C) is in D, say p_{k} ≤ q_{k}, then con (y, C′) is p′ ≤ q′. By (i) and (ii),

σ′(p′) < σ′(q′) ,
σ′(p_{i}) ≤ σ′(q_{i}) , 0 ≤ i ≤ n − 1 .

It follows that there must exist an i, 0 ≤ i ≤ n − 1, such that

σ′(p_{i}) < σ′(q_{i}) .  (6.10)

Define

(σy)′ = σ′y_{i}y_{i+1}y_{i+2} ⋯ y_{k−1}y

(the sequence i, i + 1, …, k − 1 wraps modulo n if necessary). Then σy ≤_{X} (σy)′. By (6.10), y_{i} is (σ′, C)-enabled. Since each y_{j} is 0-exposed in q_{j+1}, 0 ≤ j ≤ n − 1, it follows inductively that each y_{j} is (σ′y_{i}y_{i+1} ⋯ y_{j−1}, C)- enabled, and y is (σ′y_{i}y_{i+1} ⋯ y_{k−1}, C)-enabled. Thus σ′y_{i}y_{i+1} ⋯ y_{k−1}y ∈ T_{C}.

It remains to show that σy ≤_{C′} (σy)′. For p ≤ q in C − D,

(σy)′(q − p) = (σy)′(q) − (σy)′(p)
≥ σy(q) − (σy)′(p)
= σy(q) − σy(p)  since the y_{i} do not appear in p
= σy(q − p) .

For p′ ≤ q′, since each y_{j} is 0-exposed in q_{j+1} and hence also in q′, by Lemma 6.9(ii) we have

(σy)′(q′ − p′) = σ′y_{i}y_{i+1}y_{i+2} ⋯ y_{k−1}y(q′ − p′)
≥ σ′y_{i+1}y_{i+2} ⋯ y_{k−1}y(q′ − p′)
≥ σ′y_{i+2} ⋯ y_{k−1}y(q′ − p′)
≥ ⋯
≥ σ′y(q′ − p′)  (6.11)

By Lemma 6.5(iii) and the induction hypothesis, (6.11) is bounded below by σy(q′ − p′). □

Theorem 6.19 It is decidable whether a given instance C of the NRP has a solution.

Proof. We proceed by induction on the complexity of C. If C = ∅, then all variables are unconstrained and therefore enabled, thus we can increment x_{0} immediately. Otherwise assume C is nonempty.

We identify a number of cases below, each of which allows us to reduce the size of C in some respect (either fewer constraints or fewer constrained variables). In each case, the induction hypothesis gives a procedure for deciding whether the smaller system has a solution, and this will determine whether C has a solution.

Case 1 C contains an unconstrained (0, C)-exposed variable. By Lemma 6.16, C is equivalent to a system with fewer constraints.

Case 2 H(ϵ, C) has a self-loop labeled x, and x is (0, C)-enabled. By Lemma 6.17, C is equivalent to a system with either fewer constrained variables or fewer constraints.

Case 3 H(ϵ, C) has a cycle on a set of at least two vertices. By Lemma 6.18, C is equivalent to a system with fewer constraints.

Case 4 None of Cases 1, 2, or 3 apply. In this case, consider the set T_{C}^{adm} consisting of all admissible strings in T_{C}. The set T_{C}^{adm} contains the empty string ϵ and is closed under the prefix relation, so it is a tree. For any σ ∈ T_{C}^{adm}, σx ∈ T_{C}^{adm} iff x is (σ, C)-enabled but not (σ, C)-inhibited. By Lemma 6.13, C has a solution if and only if it has one in T_{C}^{adm}.

Now let T′_{C} be the subtree of T_{C}^{adm} obtained by deleting all strings containing a proper prefix of the form στ, where |τ| > |X| and σ ≤_{C} στ. The tree T′_{C} has no infinite paths, since Dickson’s Lemma (Lemma 6.6) says that any infinite path must contain υ_{0}, υ_{1}, υ_{2}, … such that each υ_{i} is a proper prefix of υ_{i+1} and each υ_{i} ≤_{C} υ_{i+1}; thus υ_{0} ≤_{C} υ_{|X|+1} and the difference in their lengths is at least |X| + 1, so this infinite path would be pruned in the construction of T′_{C}. By König’s Lemma, T′_{C} is finite, since it is finitely branching. The tree T′_{C} can be constructed effectively since the conditions for extending a branch and for pruning are effective.

Since any extension in T_{C} of a solution is a solution, C has a solution iff it has a solution of the form στ ∈ T_{C}^{adm} for some leaf σ of T′_{C}. The leaves σ are of two types, not necessarily mutually exclusive:

(i) All (σ, C)-enabled variables are (σ, C)-inhibited. Leaves of this form are leaves of T_{C}^{adm}, since they have no C-admissible extensions.

(ii) The leaf σ is of the form τρ, where τ ≤_{C} τρ and |ρ| > |X|. Leaves of this form are not necessarily leaves of T_{C}^{adm}, but are obtained by pruning T_{C}^{adm} in the construction of T′_{C}.

If σ(x_{0}) > 0 or x_{0} is (σ, C)-enabled for some leaf σ, we are done: in the former case, σ is a solution, and in the latter, σx_{0} is a solution. Otherwise, there is no admissible solution extending a leaf of the form (i). Thus we are left with leaves of the form (ii). For each such leaf τρ, where τ ≤_{C} τρ and |ρ| > |X|, since τρ is C-admissible, for every prefix υx of ρ, either

• x is constrained in C,

• x is (τυ, C)-exposed, or

• τυ(x) = 0.

Suppose ρ contains a variable constrained in C. By Lemma 6.14, H(τρ, C) contains either an edge out of ∗ or a cycle whose labels are in ρ. If the former, we revert to Case 1 after resetting. If the latter and the cycle is of length at least two, we revert to Case 3 after resetting. Otherwise there is a self-loop in H(τρ, C) with label x, where υx is a prefix of ρ. If that self-loop already exists in H(τυ, C), then since x is τυ-enabled, we revert to Case 2 after resetting. Otherwise, let υy be the shortest prefix of ρ such that H(τυy, C) contains that self-loop. By Lemma 6.9(v), x is τυy-enabled, and we revert to Case 2 after resetting.

If all variables occurring in ρ are unconstrained in C and at least one is (τυ, C)-exposed for some prefix υ of ρ, then H(τυ, C) has an edge out of ∗, and we revert to Case 1 after resetting.

Finally, if all variables occurring in ρ are unconstrained in C and not (τρ, C)-exposed, we must have τυ(x) = 0 for every prefix υx of ρ, otherwise the string would not be admissible. But since |ρ| > |X|, at least one variable must be fired twice, so this situation cannot occur. □

Acknowledgements

We are indebted to Moshe Vardi for many valuable ideas and the anonymous referees for a thorough reading and excellent suggestions that substantially improved the presentation.

We gratefully acknowledge the support of the National Science Foundation under grant CCR-9317320, BRICS (Basic Research in Computer Science), a Centre of the Danish National Research Foundation, the John Simon Guggenheim Foundation, and the U.S. Army Research Office through the ACSyAM branch of the Mathematical Sciences Institute of Cornell University under contract DAAL03-91-C-0027.

References

[1] A. Aiken, D. Kozen, M. Vardi, and E. Wimmers, The complexity of set constraints, in Proc. 1993 Conf. Computer Science Logic (CSL’93), Eur. Assoc. Comput. Sci. Logic, September 1993. To appear. Also, Cornell University tech. report 93-1352, May 1993.

[2] A. Aiken, D. Kozen, and E. Wimmers, Decidability of systems of set constraints with negative constraints, Tech. Rep. 93-1362, Computer Science Department, Cornell University, June 1993. Information and Computation, to appear.

[3] A. Aiken and B. Murphy, Implementing regular tree expressions, in Proc. 1991 Conf. Functional Programming Languages and Computer Architecture, August 1991, pp. 427–447.

[4] , Static type inference in a dynamically typed language, in Proc. 18th Symp. Principles of Programming Languages, ACM, January 1991, pp. 279– 290.

[5] A. Aiken and E. Wimmers, Solving systems of set constraints, in Proc. 7th Symp. Logic in Computer Science, IEEE, June 1992, pp. 329–340.

[6] L. Bachmair, H. Ganzinger, and U. Waldmann, Set constraints are the monadic class, in Proc. 8th Symp. Logic in Computer Science, IEEE, June 1993, pp. 75–83.

[7] J. A. Brzozowski and E. Leiss, On equations for regular languages, finite automata, and sequential networks, Theor. Comput. Sci., 10 (1980), pp. 19– 35.

[8] D. Cox, J. Little, and D. O’Shea, Ideals, Varieties, and Algorithms, Springer-Verlag, 1992.

[9] R. Gilleron, S. Tison, and M. Tommasi, Solving systems of set constraints using tree automata, in Proc. Symp. Theor. Aspects of Comput. Sci., vol. 665, Springer-Verlag Lect. Notes in Comput. Sci., February 1993, pp. 505– 514.

[10] , Solving systems of set constraints with negated subset relationships, in Proc. 34th Symp. Foundations of Comput. Sci., IEEE, November 1993, pp. 372–380.

[11] N. Heintze and J. Jaffar, A decision procedure for a class of set constraints, in Proc. 5th Symp. Logic in Computer Science, IEEE, June 1990, pp. 42–51.

[12] , A finite presentation theorem for approximating logic programs, in Proc. 17th Symp. Principles of Programming Languages, ACM, January 1990, pp. 197–209.

[13] N. D. Jones and S. S. Muchnick, Flow analysis and optimization of LISPlike structures, in Proc. 6th Symp. Principles of Programming Languages, ACM, January 1979, pp. 244–256.

[14] K. Marriott and M. Odersky, Systems of negative Boolean constraints, Tech. Rep. YALEU/DCS/RR-900, Computer Science Department, Yale University, April 1992.

[15] P. Mishra, Towards a theory of types in PROLOG, in Proc. 1st Symp. Logic Programming, IEEE, 1984, pp. 289–298.

[16] P. Mishra and U. Reddy, Declaration-free type checking, in Proc. 12th Symp. Principles of Programming Languages, ACM, 1985, pp. 7–21.

[17] J. C. Reynolds, Automatic computation of data set definitions, in Information Processing 68, North-Holland, 1969, pp. 456–461.

[18] J. Young and P. O’Keefe, Experience with a type evaluator, in Partial Evaluation and Mixed Computation, D. Bjørner, A. P. Ershov, and N. D. Jones, eds., North-Holland, 1988, pp. 573–581.

Recent Publications in the BRICS Report Series

RS-94-32 Alexander Aiken, Dexter Kozen, and Ed Wimmers. Decidability of Systems of Set Constraints with Negative Constraints. October 1994. 33 pp.

RS-94-31 Noam Nisan and Amnon Ta-Shma. Symmetric Logspace is Closed Under Complement. September 1994. 8 pp.

RS-94-30 Thore Husfeldt. Fully Dynamic Transitive Closure in Plane Dags with one Source and one Sink. September 1994. 26 pp.

RS-94-29 Ronald Cramer and Ivan Damg� ard. Secure Signature Schemes Based on Interactive Protocols. September 1994. 24 pp.

RS-94-28 Oded Goldreich. Probabilistic Proof Systems. September 1994. 19 pp.

RS-94-27 Torben Bra� uner. A Model of Intuitionistic Af�ne Logic from Stable Domain Theory (Revised and Expanded Version). September 1994. 19 pp. Full version of paper appearing in: ICALP ’94, LNCS 820, 1994.

RS-94-26 S�ren Riis. Count(q) versus the Pigeon-Hole Principle. August 1994. 3 pp.

RS-94-25 S�ren Riis. Bootstrapping the Primitive Recursive Functions by 47 Colors. August 1994. 5 pp.

RS-94-24 S�ren Riis. A Fractal which violates the Axiom of Determinacy. August 1994. 3 pp.

RS-94-23 S�ren Riis. Finitisation in Bounded Arithmetic. August 1994. 31 pp.

RS-94-22 Torben Bra� uner. A General Adequacy Result for a Linear Functional Language. August 1994. 39 pp. Presented at MFPS ’94.

RS-94-21 S�ren Riis. Count(q) does not imply Count(p). July 1994. 55 pp.