BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1362
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Decidability of Systems of Set Constraints with Negative Constraints
AUTHOR:: Aiken, Alexander
AUTHOR:: Kozen, Dexter 
AUTHOR:: Wimmers, Ed
DATE:: June 1993
PAGES:: 34
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.
END:: CORNELLCS//TR93-1362
BODY::
Decidability of Systems of Set Constraints
With Negative Constraints
Alexander Alken*
Dexter Kozen**
Ed Wimmers*
TR 93-1362
June1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*IBM Almaden Research Center, 650 Harry Rd?, San Jose, CA 95120
**Computer Science Department, Cornell University, Ithaca, NY 14853.
Decidability
with
of Systems of Set Constraints
Negative Constraints
Alexander Aiken*
aiken?alrnaden.ibm
Dexter Kozent
kozen?cs.cornell.edu
corn
Ed wimmers*
wimmers?almaden.ibm.corn
June 19,1993
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 consid-
erably 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 expres-
sions representing subsets of T?, the set of ground terms over a finite ranked
alphabet ?. Formally, a positive set constraint is of the form  c F and a
*IBM Almaden Research Center, 650 Harry Road, San Jose, CA 95120
tComputer Science Department, Cornell University, Ithaca, NY 14853
negative set constraint is of the form E ? F, where E and F are expressions
built from a set X = [x, .... .? of variables ranging over subsets of T?, the
usual set-theoretic operators 0, 1, U, fl, and N, and an n-ary set operator f
for each n-ary symbol f Ei ? with semantics
f(A1,. . ,An) = ffti . . In I 1i Ei Aj, 1 < i ?
A system 8 of constraints is satisfiable if there is an assignment of subsets
of T? to the variables satisfying all the constraints in 8.
Set constraints have numerous applications in program analysis and type
inference [16, 12,14, 15,17,11, 2, 3, 6]. Most of these systems deal with pos-
itive constraints only. Several algorithms for determining the satisfiability of
general systems of positive constraints have appeared [4,10, 8, 5,1]. In [1],
the satisfiability problem for a system 8 of positive constraints is shown to be
equivalent to deciding whether a certain finite hypergraph constructed from
8 has an induced subhypergraph that is closed (see Section 4). This char-
acterization 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 with both positive and negative con-
straints. Negative constraints considerably increase the power of the con-
straint language and have important applications in program analysis. For
example, in [2, 3], opportunities for program optimization are identified by
an ad hoc technique for checking the satisfiability of systems of negative con-
straints. Set constraints with only nullary symbols correspond to Boolean
algebras over a finite set of atoms; in [13] 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 positive and negative constraints over an arbitrary signa-
ture is satisfiable. The proof reduces the satisfiability problem to a reachabil-
ity 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
[9] using automata-theoretic techniques.
2
2 Set Expressions and Set Constraints
Let ? be a finite ranked alphabet consisting of symbols f, each with an
associated arity arityf E N. Symbols in ? of arity 0,1, 2, 3, 4, and n are
called nuttary, unary, binary, ternary, quaternary, and n-ary, respectively.
Nullary elements of ? are often called constants. The set of elements of ? of
arity n is denoted ?n.
The set of ground terms over Z is denoted T?. This is the smallest set such
that if ti,...,tn ? T? and f E Zn, then fti...tn E T?. If X =
is a set of variables, then T?(X) denotes the set of terms over Z and X,
considering the elements of X as symbols of arity 0.
Let B = (u, fl, N, 0, 1) be the usual signature of Boolean algebra. 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(xUy),?g(xfly)) U a
where f Ei ?2, g E Z1, a e ??, and x,y ? X. Set expressions are denoted
E, FA Boolean express'on over X is any element of TB(X).
A positive set constraint is a formal inclusion E C F where E and F
are set expressions. We also allow equational constraints  = F, although
inclusions and equations are interdefinable. A negative set constraint is the
negation of a positive set constraint: E ?
We interpret set expressions over the powerset 2T? of T?. This forms
an algebra of signature ? + B where the Boolean operators have their usual
set-theoretic interpretations and elements f ? are interpreted as functions
f : (2T?)n H 2T?
f(A1,. . ,An) = Ift1 . . . tn tj E Aj, 1 < i < n?
A set assignment is a map
a : X H 2Th
assigning a subset of T? to each variable in X. Any set assignment a extends
uniquely to a (? + B)-homomorphism
a: T?+B(X) H 2T?
3
by induction on the structure of the set expression in the usual way. The set
assignment a satisfies the positive constraint E C F if a(F) C a(F), and
satisfies the negative constraint E ? F if a(E) ? a(F). We write a y if
the set assignment a satisfies the constraint y. A family S of set constraints
is satisfiable if there is a set assignment that satisfies afl constraints in S
simultaneously. If ? is a constraint, we write S ? y if all set assignments that
satisfy Z also satisfy y. 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 = ?O, 1 J is the two-element Boolean algebra. Any truth assignment
u extends uniquely to a B-homomorphism
u:T?(X) H 2
inductively according to the rules of Boolean algebra. If X = ....... , Xmt,
we use the notation
B[xj			a?j
to denote the truth value of the Boolean formula B under the truth assign-
ment Xj H a?, 1 <i ?
3 Expressibility
Positive and negative constraints together are strictly more expressive than
positive constraints alone. We wili 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 j all finite subsets of S are satisfiable.
Proof The implication (?) is straightforward. Now suppose 8 is finitely
satisfiable. We wish to construct a satisfying set assignment for 8. By Zorn's
Lemma, there exists a maximal finitely satisfiable set 8 of positive constraints
containing 8. One can show that for all ground terms t and set expressions
E, exactly one of the constraints t C F I C E is in 8; if neither are in
4
&, then & is not maximal, and if both are, then & is not finitely satisfiable.
Now define a map
a(E) =			C E ?
One can show by induction on the structure of set expressions that a is a
valid set assignment and satisfies S. For example, to show that
a(fE1 ... En) = ....... In I 1i c a(E?), 1 < i ?
note
I E a(fEi... En) ? I C ..... . En ? &
Then I must be of the form f11. . In, otherwise & would not be finitely
satisfiable. Now we use the fact that
..... . In C ..... . En 1= 1i C Ej, 1<i?n
fli C Ej 1 < i < n? = fli . In C fE1. En
to argue that I C fE1. . En C & iff Ii C Ej ? &, 1 ? i < n, otherwise &
would not be finitely satisfiable. Thus
I ? a(fE1 . En) ? I C ..... . En e &
? Ii C Ej ? &, 1 <i <n
Ij ? a(E?), 1 <i ? n
To show that a satisfies all constraints of &, let E C F be any constraint
in 8. For any term I,
I E a(E) ? I C E E 8
? I E F E &			(1)
? a(F);
the reason for the implication (1) is that
fI C E E C Fl # I C F,
and if I C F were not in &? then I C NF would be, and & would not be
finitely satisfiable.
5
Corollary 3.2 Positive and negative constraints are strictly more erpress?ve
than positive constraints only.
Proof. Consider the negative constraint ? ? 0 over any ranked alphabet
? with at least one constant and at least one symbol of higher arity. Solu-
tions are a : txl H T? with a(?) nonempty. Let 8 be any set of positive
constraints over any set of variables X containing x. We claim that it is not
the case that the set
fa(x) a : X			T?, a
is exactly the set of nonempty subsets of T?.
Consider the infinite set of positive constraints
8 u ft C Nr			e
Either this is satisfiable or not. If so, then there is a satisfying assignment a.
But t c a(?x) for all terms t, so a(r) ? and the claim is verified. If not,
then by compactness there is a finite subset F C T? such that
8 u ft C Nx			? FJ
is not satisfiable. Therefore there is no solution a of 8 with a(x) = fi),
where t is any term not in F.			E
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 C Z, let
Zj = f%?x I 0 ? i ? arityf, x e X?
be a set of variables such that the sets X and Zj, f C ? are pairwise disjoint.
A system of set constraints in normal form (with respect to X and the Zj)
consists of
6
o+ a positive constraint B = 1, where B Ei TB(X)
o+ for each f C ?, a positive constraint Cj = 1, where Cj C TB(ZJ)
o+ positive constraints
Zo1x			= f 1...1 fl r
n
Zix			= fl...lxl...1
for each f E ?? and each 1 <i < n and x ? X
o+ a finite set of negative constraints D # 0, where D E TB(X), D E D.
The last component is absent with positive constraints only.
As described in [1], a system of set constraints 8 in normal form deter-
mines a hypergraph
H = (U, E1 f ?
as follows. The vertex set U is the set of all truth assignments a : X H 2
satisfying B. Each such truth assignment corresponds to a conjunction of
literals (also denoted a) in which each variable in X occurs exactly once,
either positively or negatively, such that a C 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. Each Boolean expression over X is
equivalent modulo B = 1 to a disjunction of atoms.
For each f E ??, the hyperedge relation E1 of H is defined to be the set
of all (n t 1)-tuples (ao, . . , a?) c U? such that
Cj[Z(x := ui(x)] = 1			(2)
Intuitively, we think of the formula C1 as a Boolean-valued mapping on
+ 1)-tuples of truth assignments to X. To emphasize this intuition, we
abbreviate the left hand side of (2) by
C1[a0,...,a?j
7
Thus
(u0,...,un)EEj iff Cj[uo,...,u?]=1
In general, the size of H can be exponential in the size of S.
An (n + 1)-ary hyperedge relation E1 of the hypergraph H is said to be
closed if for each n-tuple ...... , Ei U?, there exists a u0 E U such that
(uo, ui,. . , Un) Ei Fy. In the case n = 0, this definition just says Ej A U #
Abusing notation, we can think of Ef as a function
where
Ej : H
Ef(ui,.. .,un) = ftio (u0,u1,. ..,un) C Fit
In this view, Ej is closed iff Ej(u1,... , Un) # ? for each n-tuple ...... , ?n C
U?. The hypergraph H is said to be closed if all its hyperedge relations are
closed.
The induced subhypergraph of H on vertices U' C U is the hypergraph
= (U', E1, f E Z)
such that Ej' = E1 A (U?)n+l for f ? Zn.
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 II corresponding to a system 8 of positive set
constraints has a closed induced subhypergraph f and only if 8 is satisfiable.
In brief, the proof of [1] establishes a one-to-one correspondence between
set assignments a satisfying 8 and maps
0: T? H U
such that for all f c ? and for all terms ..... . tn,
0(ft1 . . . tn) E Fj(0(ti), . . . , O(tn)) (3)
8
The set assignment corresponding to 0 is
cr(?) = ft I O(1)(x) =
= a(f1...1x????1)
i--Hi			n--Ht
= a(fl...1 flx).
Thus deciding the satisfiability of 8 is tantamount to determining the exis-
tence of a map 0 satisfying (3). In turn, this is equivalent to the hypergraph
closure problem: if such a 0 exists, then the induced subhypergraph of H on
the image of 0 is closed, and conversely, if there exists a closed induced sub-
hypergraph on vertices tJ' C U then one can inductively define O(fli... In)
to be the lexicographically first element of U' n Ej(O(Ii),. . , 0(m)).
In the presence of negative constraints D ? 0, D Ei D, the map 0 must not
only satisfy (3), but must also take on some value u such that u(D) = 1 for
each D E D. Thus in the presence of negative constraints, the satisfiability
problem becomes:
Given a finite set D of Boolean formulas D c TB(X) and a hy-
pergraph
H = (U, Ej f ?
specified by B E TB(X) and Cj ? TB(ZJ), f ? ?, determine
whether there exists a map
0: T? H U
satisfying (3) such that for each D Ei D there exists an atom u in
0(T?) satisfying D, where O(T?) denotes the image of T? under
the map 0.
5 A Reachability Problem
Our decision procedure first reduces the satisfiability problem for mixed sys-
tems of set constraints to the following reachability problem involving Dio-
phantine inequalities.
9
Let X be a set of variables ranging over N, 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 N such that
o+ each left hand side p is a sum of variables in X
o+ each variable occurs in at most one left hand side.
Each valuation u extends uniquely to a
A variable x is said to be enabled under
A valuation is a map u : X H
semiring morphism u : N[X] H
a valuation u if either
o+ the variable u does not occur on any left hand side of an inequality in
or
o+ the unique inequality in C in which x appears on the left hand side is
a strict inequality under the valuation u.
Consider the following nondeterministic procedure. Starting with the
zero valuation, repeatedly choose a variable that is enabled and "fire" it by
adding 1 to it. The problem is to decide whether there exists a sequence of
firings that allows a particular distinguished variable to be fired.
We will give a more rigorous presentation of this problem below, then
reduce the satisfiability problem to this problem, then finally show that this
problem is decidable.
5.1 Polynomials and Valuations
We use the term semimny to mean commutative semiring with unit.
Let X be a finite set of variables and let N[XJ denote the semiring of
polynomials in the indeterminates X with coefficients in N. This is the free
semiring on generators X.
Any map u X H R to a semiring R extends uniquely to a semiring
morphism u : N[X] H R. Such a map is called a valuation if R = N.
Composition of polynomials is effected by taking R = N[Xj.
Let v be any valuation, and let ?flCv : N[Xj H N[X] be the unique
semiring homomorphism such that
lflCv(X) = x + v(x) , x E X
10
For q Ei N[X], the constant coefficient of inc?(q) is
O(inc?(q)) = v(q)
where 0 is the zero valuation. Let ?flC'v be the map on valuations defined by
iflcv'(U) =			U0?flCv (4)
Then for x C X and q E N[X],
iflCv(U)(X) = u(x)+v(x)
iflcv'(O) =			0 0 ?flCv
= v
One example of particular importance will be incrementing the value of a
variable x under a valuation u by 1. This is obtained by taking v = & in the
above construction, where ?(x) = 1 and ?(y) = 0 for y $ ?. This case gets
a special concise notation:
= inc'6?(u)
= U 0 inc6?			(5)
q[x/r + 1] = inc??(q)
In this case (4) takes the form
ux(q) = u(q[?/x + 1]).			(6)
We extend the definition of ux to ua for a C X* by taking
= u
u(ax) = (ua)x
5.2 Systems of Diophantine Inequalities
We consider finite systems C of Diophantine inequalities of the form p < q
where p, q E N[X] such that
o+ each left hand side p is a sum of distinct variables; and
11
0 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 N[X]. The inequalities in C are called (Diophantine) constraints. A
variable x ? X is said to be constrained in C if x occurs in some left hand
side of a constraint in C. In this case we denote the unique such constraint
by con (x, C) = Px ? q?. If x does not occur in any left hand side of
an inequality in C, then x is said to be unconstrained in C, and we write
con(x,C) =
We say that the valuation
u satisfies the inequality p < q if
u(p) ? u(q)
We say that u satisfies C if u satisfies all the inequalities in C. The set of
all valuations satisfying C is denoted Vc.
5.3 The Nonlinear Reachability Problem
Definition 5.1 Let u E Vc. The inequality p ? q E C is said to be u-
enabled if u(p) < u(q); i.e., the inequality is strict under the valuation u.
The variable x E X is said to be (u, C)-enabled if either
o+ x is unconstrained in C, or
o+ x is constrained in C and con (x, C) is u-enabled.
We write
-+ v
c
if x is (u, C)-enabled and v = ux. For a ? we write
u			v
if a = ....... X?? fl > 0, and there exist valuations ..... . , U?? such that
u = u0, v = U?? and
%`i--Hi			_
? Uj? 1 <i ? n
12
c
Note that if u#v then v = ua. Note also that if u ? Vc and u#v,
then v E Vc. In other words, if v satisfies C and x is (v, C)-enabled, then we
can increment the value of x by 1 and the resulting valuation still satisfies C.
Informally we refer to this action as firing x. The converse is false in general;
i.e., it is possible that v and ux both satisfy C but r is not (v, C)-enabled:
consider the constraint r _
Any set C of constraints gives rise to a (possibly infinite) labeled directed
acyclic graph Cc with vertices Vc and labeled directed edges ->cX, r E X.
Definition 5.2 The Nonlinear Reachability Problem (NRP) is to determine,
given C and s E Vc, whether there is a vertex t reachable from s in the graph
Cc such that t(x0) > 0, where xo is some distinguished variable of X. In
other words, determine whether there exists a a Ei X* such that 5 sa and
sa(x0) > 0. Such a a is called a solution of the instance (s, C) of the NRP.
E
Note that if s(x0) > 0 already, then the null string e is a solution of (s, C);
otherwise a is a solution iff x0 occurs in a.
If s Ei Vc, we define the graph C(s, C) to be the induced subgraph of Cc
on all vertices reachable from 5. In other words, the vertices of C(s, C) are
(11 sD>I for some a ? X*J
The graph G(s, C) is rooted at 5. A path in G(s, C), otherwise unspecified,
will always mean a path starting at the root. We also abuse notation and
identify paths with their labels; thus we may use the term path to refer to
an element a ? X* such that 5#?5a.
5.4 Order
Definition 5.3 For C a system of contraints and valuations v, v, define
o+ v v if v(x) < v(x) for all x ? X
o+ v <?c vifu(q--Hp) < v(q--Hp) for Jlp?q ? c
o+ v <xc v if both v v and v <c v.
We write v =c v if both v ?c v and v ?c v.
13
0
Note that if um>uv then u v. The same statement is not true in
general for <c.
Lemma 5.4 Let x ? X, u, v valuations such that u <x v, and p ? q E C.
Then
tix(q--Hp) --H u(q--Hp) < vx(q--Hp) --Hv(q--Hp)
Proof Since p is a sum of distinct variables,
?			ifroccursinp
vx(p) --H v(p) = ux(p) --H u(p) =			o,			otherwise.
Then
vx(q --H			--H v(q --H			--H ux(q --H p) + u(q --H
vx(q) --H vx(p) --H v(q) + v(p) --H ux(q) + ur(p) + u(q) --H u(p)
vx(q) --H v(q) --H ux(q) + u(q)
v(q[x/x + 1]) --H v(q) --H u(q[?/? + 1]) + u(q) by (6)
v(q[x/x + 1] --H --H u(q[x/x + 1] --H
>0
sinceu <xv and q[x/x +1]--H q ? N[Xj. 5
LemmaSS Letu,veVc andx?X.
(i) If x is (u, C)-enabled and ? <c v, then x is (v, C)-enabled.
(ji) If u <x v then ux <x vx
(iii) If u <xcv, then ux <xc vx.
Proof The assertions (i) and (ii) are straightforward consequences of the
definitions. The assertion (iii) follows from (ii) and Lemma 5.4. 5
14
5.5
Reduction of Set Constraint Satisfiability to Non-
linear Reachability
Theorem 5.6 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 the fotlowing prob-
lem:
Given a finite set D of I3oolean formulas D ? TB(X) and a hy-
pergraph
H = (U, Ej f ?
specified by Boolean formulas B c TB(X) and Cj E TB(ZJ),
f Ei ?, determine whether there exists a map
0: T? H
such that
(i) for all f ? ?? and for all terms fli ...
0(fti .. . tn) C Ej(0(ti), . .. , 0(tn)) (7)
(ii) for each D Ei D there exists an atom u in O(T?) with u(D) =
1.
Let V be the set of all subsets V C U such that for all V E D there exists
a v ? V with v(D) = 1. The problem above is equivalent to the disjunction
over all V Ei V of instances of the same problem with property (ii) replaced
by the property
(ii') V c
Furthermore, we will only need to construct a finite partial approximation
0' to 0 satisfying (i)"and (ii'), provided
. the domain of 0' is closed downward under the subterm relation
15
o+ there is a closed induced subhypergraph of il containing the image of
0'.
The second property will allow 0' to be completed to a total function 0.
Thus the problem now becomes:
Given a hypergraph
H = (U, Fj f E ?)
specified by B and Cj, f c ?, and a subset V c u determine
whether there exist U' C U and a partial map 0 : H U1 with
finite domain such that
the induced subhypergraph on U' is closed
domain 0 is closed downward under the subterm relation
0
o+ 0 satisfies (7) on all terms in its domain
o+ V C 0(T?) c u'.
Consider the following nondeterministic procedure for constructing 0. We
first guess the subset U' containing the target set V and check that it is
closed. We start with 0 totally undefined. At any point, say we have a
partial 0 with finite domain closed downward under the subterm relation.
We nondeterministically pick some term .1.... tn such that the O(l?) are
defined but 0(fti... In) is not yet defined, nondeterministically choose some
u in Ej(0(Ii),... , 0(tn)) fl U', and assign 0(ft1... In) := 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 0(t) for some I.
During this process, we use an integer variable
ru?f?u1
where n = arity f, to count the number of terms of the form ..... . I? such
that
o+ O(I?) exists and equals Uj, 1 ? _ n and
o+ 0(ft1... In) exists and equals u.
16
There is one such variable for each choice of f in ?, ....... , E U' where
n = arityf, and u E U' n Ej(ui, . , Un)
Now for each f Ei ?? and u1...., u? Ei U', consider the formal inequality
Xuj,?,v1?			(8)
n			M
Xuj,?			< II ?
uEU'nEj(uiUn)			i=1 m=O v1Vm E U'
? E ?m
where M is the maximum arity of symbols in ?. This inequality has the
following significance. Given a partial map 0, let
Aj,u1un = ffli . tn 0(li) exists and equals Uj? 1 < i <
The value of the right hand side of (8) is the size of Aj,uiV?? and the value
of the left hand side of (8) is the size of the subset of Aj,uiun consisting
of all elements t for which 0(t) is defined. The inequality expresses the fact
that 0 is defined on the subterms of I before being defined on 1.
Consider the collection C of all such inequalities (8). To say that a
variable Xu,J,u1u? 15 enabled says that there exists a term I with head sym-
bol f such that 0 is defined on the n immediate subterms and takes values
..... . , U? on those subterms respectively, but 0(1) is not yet defined. To fire
Xu,f,uiU? says that we choose one such I and define 0(1) :=
The process of defining 0 from the bottom up as described above corre-
sponds to a sequence of legal firings Conversely, any legal sequence of firings
gives a corresponding sequence of definitions of 0 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 C V there are f and ..... . , U? such that
the value of Xv,J,u1U? is nonzero.
We reduce this problem to a finite disjunction of instances of the NRP
as follows, For each v Ei V, choose f and Ul,. . , , U? and let Yv = Xv,J,u1Un'
Add the constraint
x0 < H Yv
vEV
where x0 is a new variable, and make x0 the distinguished variable of the
NRP so obtained. The variable ro can be fired only after all the Yv have
17
been fired. The problem above is equivalent to the disjunction of all such
instances of the NRP over all possible choices of the Yv 0
6 Decidability of the Nonlinear Reachability
Problem
6.1 Well Partial Orders and Dickson's Lemma
A well partial order is a partially ordered set in which every infinite se-
quence has an infinite monotone nondecreasing subsequence. That is, for
every infinite sequence d0,d1,..., there exist indices i0 < i1 ? ... such that
dj0 < di1 <????.
Lemma 6.1 (Dickson's Lemma) The set Nk of k-tuples of natural num-
bers under the componeniwise order is a well partial order.
For a proof of Dickson's Lemma, see [7].
6.2 Reset
Let C be a system of inequalities. Let v be any valuation in Vc, and let iflCv
and iflCv be as in Section 5.1. Let iflcv(C) be the system of inequalities
incv(C) = fp ? in?(q) v(p) p < q E
The right hand sides inc?(q)--Hv(p) are in N[X], since the constant coefficient
of inc?(q) is at least v(p). This is a consequence of the fact that v satisfies
v(p) ? v(q) = O(inc?(q))
where 0 is the zero valuation. Moreover, x is constrained in C iff it is con-
strained in iflcv(C), since the left hand sides are the same.
Lemma 6.2 The graphs G(1, incv(C)) and G(iflc'v(t), C) are isomorphic un-
der the map ?flCv'
`s
Proof It follows easily from the definitions that the map ?flCv'?5 one-to-
one. We need to show
u satisfies incv(C) iff iflcv'(?i) satisfies C
(ii) x is (u, incv(C))-enabled iff x is (iflc'v(U), C)-enabled
(iii) (iflc'v(U))X = iflCv(UX)
For any inequality p < q E C, by (4) and the fact that p is linear we have
inC?(u)(q)			=			u(in?(q))
inQ'(u)(p)			=			u(p)+v(p)
from which it follows that
inc'?(u)(q --H			=			u(inc?(q)) --H u(p + v(p))
--H			u(incv(q)--Hv(p)--Hp)
--H			u(inc?(q--Hp))
The assertions (i) and (ii) follow. For (iii), we use the fact that ?flC'v and
?flC'6x commute:
(iflcv'(U))X = ?flC'6(?flCv'(U))
= flCv1flC?U
= lflCvUX
c
We will apply this lemma as follows. If (s, C) is any instance of the NRP,
take t = 0 and v = s in Lemma 6.2, and we obtain an isomorphism
inc'8 : G(O, inc8(C)) H G(s, C)
Informally, we refer to the operation of passing from G(s, C) to the iso-
morphic graph G(o, inc8(C)) as a reset. This will allow us to restrict our
attention to instances of the NRP of the form (0, C) without loss of general-
ity.
19
6.3 Exposed Variables
Definition 6.3 Let x E X q C N[X], and u E Vc. We say that x is u-
exposed in q if u(q?) > 0 for some 1 ? i < n, where ..... . , q? are the unique
polynomials in N[X --H fxj] such that
q =
i=O
We say that x is (u, C)-exposed if x is u-exposed in q for some p ? q E C.
E)
Lemma 6.4 Let x ? X, q E NFY], and u E V0. Then x is u-exposed in q
iff u(q) <ux(q).
Proof. Let the q? be as in Definition 6.3. Since q? E N[X --H fxj], u(q?) =
ux(q?). Then
--H			= uy(?qjxi) --H u(?qjxi)
i=O			i=O
--H ?(ux(qj)ux(x)i --H u(qj)u(x)i)
--H ? u(q?)((u(x) + 1)? --H
--H ? u(q?)((u(x) + 1)? --H
>
t=1
>0,
with equality holding iff u(q?) = 0 1 <i <n.
For u a valuation, let sign u be the valuation
1 if u(y) > 0,
signu(y) = ol if u(y) = 0.
Lemma 6.5 Let x ? X, p ? q E C, and u ? V0.
El
20
If sign v(y) < signv(y) for ally E X --H fxj and x is v-exposed in q,
then x is v-exposed in q. In particular, ifsignu(y) = signv(y) for all
y E X --H fxj, then x is v-exposed in q iff x is v-exposed in q.
(ii) If x is v-exposed in q and v ?x v, then x is v-exposed in q (once
exposed, always exposed).
(iii) If p ? q is v-enabled and x is v-exposed in q, then p ? q is ux-enabled.
(iv) If x is v-exposed in q and x does not appear in p, then p < q is ux-
enabled.
(v) If x is not (v,C)-exposed, then ux _ v.
(vi) The property of exposure in the right hand side of a constraint p < q E
C is preserved under the isomorphism of Lemma 6.2. In other words,
x is inc\)(u)-exposed in q iffx is v-exposed in inc?(q) --H
(vii) If v(x) > 0, x is not v-exposed in q, and x is vy-exposed in q, then y
is v-exposed in q.
Proof Except for (i), (vi), and (vii), all statements are direct conse-
quences of Definition 6.3 and Lemma 6.4.
To prove (i), we observe first that for any r E N[x?, sign v(r) = 0 iff
v(r) = 0, since any term of r is nonzero under the valuation v iff it is
nonzero under the valuation sign v. Thus if sign v(y) ? sign v(y) for all
y E X --H txj, then v(q) > 0 implies v(q) > 0 for any q ? N[X --H fx?]. We
obtain the desired conclusion by applying this to the q? of Definition 6.3.
To prove (vi), we use (4):
vx(inc?(q) --H v(p)) --H v(inq(q)
= vx(inq(q)) --H v(inc?(q))
= in?'(vx)(q) --H inC?(v)(q)
= inc'?(v)x(q) --H inc'?(v)(q)
--Hv(p))
For (vii), by (i), y $ x. Let the q? be as in Definition 6.3. There must be
a q?, i > 0, such that v(q?) = 0 and vy(q?) > 0. Since v(x) = vy(x) > 0, we
have v(qjxi) = 0 and vy(qjxi) > 0, thus vy(q) > v(q). By Lemma 6.4, y is
v-exposed in q.			5
21
6.4 Inhibited Variables and Admissible Paths
Definition 6.6 Let C be a system of constraints and u E Vc. We say x ? X
is (u, C)-inhibited if
o+ X 15 unconstrained in C,
o+ x is not (ti, C)-exposed, and
o+ u(x) > 0.
We say that a path in G(u, C) is (u, C)?admissibTh if no inhibited variable is
ever ?red. In other words, ? E X* is (u, C)-admissible if u tia, and for
all pre?xes ry of a, y is not (ur, C)-inhibited. E]
Lemma 6.7 (i) If y is (ti, C)-inhibited, then u(p) = uy(p) and u(q) =
uy(q) for all constraints p ? q E C. In particular, uy =c U
(ii) If y,z are (u,C)-inhibited, then z is (uy,C)-inhibited.
Proof
(i) Since y is unconstrained, it does not appear in p, therefore u(p) = uy(p).
Since y is not ti-exposed in q, we have u(q) = tiy(q) by Lemma 6.4.
(ii) Surely uy(z) > u(z) > 0 and z is still unconstrained in C, so it remains
to show that z is not (uy, C)-exposed. This follows from Lemma 6.5(i)
and the facts that z is not (ti, C)-exposed and sign ti = sign uy.
0
The following two lemmas imply that we can restrict our attention to
admissible paths when looking for solutions.
Lemma 6.8 For every path a of C(u, C), there exists a (ti, C)-admissible
path r in G(u,C) such that tia _ tiT.
Proof Let us call a prefix a1y of a bad if y is (tiai, C)-inhibited. The
proof is by lexicographical induction on the length of a; among paths of
the same length, the number of bad prefixes; and among paths of the same
length and same number of bad prefixes, the length of the longest bad prefix.
22
If a is null or has no bad prefix, there is nothing to prove. If the longest
bad prefix aiy is a itself, then since y is not (uai, C)-exposed, we have
by Lemma 6.?5(v) that uaiy <c ua1, and we are done by the induction
hypothesis. Otherwise, there exists a z and a2 such that a = aiyza2. Now z
is not (uaiy, C)-inhibited, by the maximality of aiy. Neither is it (uai, C)-
inhibited, by Lemma 6.7(ii). Moreover, z is (uai, C)-enabled, by Lemma
6.7(i) and the fact that it is (uaiy, C)-enaUed, and y is (uaiz, C)-enabled
since it is unconstrained. Therefore aizya2 is a path in G(u, C) of the same
length as a, but with either strictly fewer bad prefixes (if aizy is not a bad
prefix) or the same number of bad prefixes and a strictly longer maximal one
(if it is).			0
Lemma 6.9 If(u, C) has a solution, then it has a (u, C)-admissible solution.
Proof Let a be a solution of minimal length. If a is null, i.e. if u(x0) > 0
already, then we are done. Otherwise a is of the form rx0 and ur(x0) = 0.
By Lemma 6.8, there exists a (u, C)-admissible path p such that ur <c up.
If up(xo) > 0, then p is the desired admissible solution. Otherwise, x0 is
(up, C)-enabled (since ur ?c up and x0 is (ur, C)-enabled) and not (up, C)-
inhibited (since up(x0) = 0), therefore pxo is the desired admissible solution.
0
A valuation u is said to be useless (with respect to C) if all (u, C)-
enabled variables are (u, C)-inhibited. It follows from Lemma 6.7(ii) that if
u is useless, then so is ux for any (u, C)-enabled x; moreover, by Lemma
6.7(i), ux =c u. Thus if u is useless, then either
o+ u(xo) > 0, in which case the null path is a solution of the instance
(u, C) of the NRP; or
o+ x0 is (u, C)-enabled, in which case the path x0 is a solution; or
o+ neither of the above, in which case (u, C) has no solution.
6.5 The Graph H(u, C)
For a system C of inequalities and u E Vc, construct a finite labeled directed
graph H(u, C) as follows. The vertices of H(u, C) are C u f*J. For each
23
p ? q E C and x E X such that r is u-exposed in q, there is an edge
labeled x from con (x, C) to p ? q. (Recall that con (?, C) is * if x is
unconstrained in C, otherwise con (r, C) is Px < qx.) Self-loops are allowed
in this de?nition: if x is constrained in C and x is u-exposed in q?, H(u, C)
has a self-loop labeled x on vertex con (x, C).
Lemma 6.10 (i) If u E Vc, x is (u, C)-enabled, and H(u, C) contains an
edge labeled x into p < q, then p < q is ux-enabled.
(ii) If u <xv then H(u,C) is a subgraph of H(v,C).
Proof.
(i) Either r does not occur in p? in which case
ux(p) u(p) < u(q) < ux(q)
or x does occur in p, in which case
ux(p) = u(p) + 1 < u(q) < ux(q)
(ii) This follows immediately from Lemma 6.5(ii).
Lemma 6.11 Let u ? Vc and a E X+ such that u#ua and u <c ua.
Assume further that a contains at least one variable constrained in C. Then
H(uo, C) contains either a cycle all of whose labels are in a or an edge out
of* whose label is in a.
Proof Let x be constrained in C such that r occurs in a at least once.
Then
U(Px) < ua(p?)
< ua(q?--Hp?)
24
Also,
since u ua. Combining these inequalities, we obtain
< u?(q?)
By Lemma 6.4, there must be a y ? X and a prefix T? of a such that y is
u?-exposed in q?. Then H(ur, C) contains an edge labeled y from con (y, C)
to con (x, C). By Lemma 6.10(ii), this edge also exists in H(ua, 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. E
6.6 Equivalence of Problem Instances
Definition 6.12 Let C, D be systems of inequalities. We write C ? D if for
every path a of G(o, 0) there is a path r of 0(0, D) such that Oa <x OT.
We write 0 =--H D and say that 0 and D are equivalent if both 0 < D and
D <0.
The following lemma is immediate.
Lemma 6.13 If 0=--H D, then (0,0) has a solution iff(O,D) does.
6.7 Proof of Decidability
Let 0 be a system of inequalities.
Lemma 6.14 Letp < q E 0. If 0 has an unconstrained variable 0-exposed
in q, then
0 =--H
Proof Let 0' = 0 --H fp < qJ. The easier direction is 0 < 0'. If u E Vc
then u E Vc', since 0' C 0; and if y is (ti, 0)-enabled then y is also (u, 0')-
enabled, since y is either constrained by the same inequality in 0 and 0' or
unconstrained in 0'. It follows that if a is a path in 0(0, 0) then it is also
a path in 0(0,0').
25
For the other direction, suppose a is a path in &(0, C'). Let r be a
C-unconstrained variable 0-exposed in q. Let n = lal and let
T = xx???xa = x?a
Then a <x r. We show that r is a path in G(0, C). Certainly x? is a
path in G(0, C), since x is unconstrained. It remains to show that a is a
path in &(0x?, C), or equivalently by Lemma 6.2 in the isomorphic graph
G(0, incn&(C)). Thus we need to show that for any prefix py of a, y is
(Op, incn&(C))-enabled. This follows from the fact that y is (Op, C')-enabled:
for any f < g ?
Op(incn&(g --H			=			Opxn(g --H			by (5)
--H			Opx?(g) --H Op(f)			since x does not occur in f
>			Op(g --H
and for the constraint p <
Op(inc?s?(q --H
--H Opxn(q?p)
--H Oprn(q) --H 0p(p)
> Op(q)+n--HOp(p)
> Op(q) + n --H I?I
>0
by (5)
since x does not occur in p
by Lemmas 6.4 and 6.5(ii)
since p is linear
since I?I < n
Lemma 6.15 If H(0, C) has a self-loop labeled x on verlex p < q, and if r
is (0, C)-enabled, let
= ?(C?ytfpPyq;)U?P?x???xJ , $t?);4$N[X]
Then C =--H
Proof Since x is 0-exposed in q, it follows from Definition 6.3 that q has
a term of the form axk where a, k ? N and a k > 1; i.e., q can be written
26
q1+xk with q' E N[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' E N[x].
First we show C ? C'. This is immediate for case (ii) as in Lemma
6.14. For case (i), note that Vc = Vci, since u(q --H = u(q' --H p') for all
valuations u. Now for any variable y ? X --H fxl and any valuation u, y is
(u, C)-enabled iff it is (ti, C')-enabled: either con (y, C) is p < q, in which
case con (y, C') is p' < q' and u(q --H = u(q' --H ?`); or not, in which case
con (y, C) = con (y, C'). Since x is unconstrained in C', x is always (u, C')-
enabled. Thus any variable that is (u, C)-enabled is also (u, C')-enabled. It
follows that any path a of G(0, C) is also a path of G(0, C'), thus C <C'.
Now we show C' < C for both cases. Let a be any path of G(0, C'), and
let n = max2, Ia. Let a' be obtained by deleting all occurrences of x from a,
and let T = x?a'. Then a <x T. We claim that r is a path of G(0, C). Since
x is 0-exposed in q and (0, C)-enabled, by Lemmas 6.4 and 6.5(ii), x? is a
path in G(0, C), so we need only prove that a' is a path of &(0r?, C). Using
Lemma 6.2 to reset, it suffices to prove that a' is a path of &(0,inc?6?(C)).
We need to show that for any prefix p1y of a', y is (Op', inc?6?(C))-enabled.
This will follow from the fact that y is (Op, C'))-enabled, where py is the
unique prefix of a such that p1y is py with all occurrences of x removed (note
y # x, since it occurs in a').
Suppose p has rn occurrences of x. For any f ? g ? C --H fp ?
Op'(inc??(g --H f)) = Op'x?(g --H f) by (5)
--H 0p'x?(g) --H 0p(f) since x does not occur in f
--H			Opxfl?m(g)?()p(f)
>			0p(g)--H0p(f)
--H			0p(g--Hf)
For the final argument involving constraint P < q, we split on cases. In case
Op'(incn??(q --H p)) = Oplxn(q --H P) by (5)
--H			Oplxn(qI??I)
--H			Op%n(qI) --H Op(p')			since x does not occur in p'
27
In case
Op1(illCn6?(q --H P)) =
--H opxn?m(qI) --H 0p(pI)
> Op(q') --H Op(p')
--H Op(q' --H
op?xn(q --H
oplxn(ql) + oplxn(xk) --H 0p1r?(P1) --H Op1x?(x)
oxn(xk) --H Op'(p') --H Ox?(r)
k
0.
Lemma 6.16 If there is a cycte in H(O,C) on vertices
D = fPo ? q0,.. ,Pn--Hi < qn--HiJ
then C = C' where
PI =
CI =
pi
ffiq?
(C--HD)ufp1<q1J
1:]
Proof First we show C ? C'. As above, it suffices to show that for
any valuation u E Vc and variable y, if y is (u, C)-enabled then y is (u, C')-
enabled. If con (y, C) ? D, then con (y, C') = con (y, C), thus y is (u, C)-
enabled iff it is (u, C')- enabled. Otherwise, if con (y, C) ? D, say Pk ? qk,
then con (y, C') is p' < q1. Since u ? Vc, we have
U(Pi) < u(q?) , 0 ? i ? n --H 1
Moreover, since y is (u, C)-enabled, we have u(Pk) < u(q?). Thus u(p') <
u(q1), so y is (u, C1)-enabled.
28
Now we show C' < C. Assume that the vertices in D occur on the cycle
of H(0, C) in the order Po < q0, o+, Pn--Hi ? q??1 and that y? is the label on
the edge from p? < q? to Pi+1 < ?i+1, 0 < i < n --H 1 (arithmetic on subscripts
?s modulo n).
Let a be any path of G(0, C'). We construct by induction on the length
of a a path a' of G(0, C) such that 0a ?x ci 0a'. Define C = ?. Now suppose
a' has been defined. By the induction hypothesis,
(i) 0a ?x ci 0a'
(ii) 0a' ? Vc
Since y is (0a, C')-enabled, by (i) we have that y is (0a', C')-enabled.
If con (y, C) is in C --H D, let (ay)' = a'y. Then Oay ?x 0(ay)', and since
con (y, C) = con (y, C'), y is (0a', C)-enabled. Moreover, Oay ?ci Oa'y by
Lemma 5.4.
If con (y, C) is in D, say Pk ? q?, then con (y, C') is p' ? q'. By (i) and
(ii),
0a'(p') ? Oa'(q')
0a'(p?) < 0a'(q?)			0 ? _ n --H 1
It follows that there must exist an i 0 < i < n --H 1 such that
0a'(p?) ? 0a'(q?)
Define
= &YiYi+1Yi+2???Yk?1Y
(9)
(the sequence i, i ...... , k --H 1 wraps modulo n if necessary). Then Oay <x
O(ay)'. By (9), y? is (0a',C)-enahled. Since each y? is 0-exposed in Q+i,
o ? _ n --H 1, it follows inductively that each y? is (0a'yiy?+i... Yj--Hi, C)-
enabled, and y is (0a'y?y?+1... Yk-?, C)-enabled. Thus &yiyi+i?? Yk-lY is a
path of G(0, C).
It remains to show that Oay ?ci O(ay)'. For p <q in C --H
0(ay)'(q --H p) = 0(ay)'(q) --H 0(ay)'(p)
>			Oay(q) --H 0(ay)'(p)
=			Oay(q) --H Oay(p)
=			Oay(q --H
since the yj do not appear in p
29
For p' ? q", since each y? is 0-exposed in q5+i and hence also in q', we have
O(ay)'(q' --H p') = Oa1y?y?+iy?+2.. yk--Hly(qI --H p1)
_ Oa1y?+1y?+2			y?--Hiy(q1 --H
_ 0?1Yi+2			y?--Hiy(q1 --H
_ o?y(qI--HPI)			(10)
By Lemma 5.4 and the induction hypothesis, (10) is bounded below by
O?y(q1 --H P1).			E
Theorem 6.17 It is decidable whether a given instance (u, C) of the NJ?P
has a solution.
Proof. Assume that u(xo) = 0, otherwise there is nothing to prove. By
Lemma 6.2, we may also assume without loss of generality that u = 0. We
proceed by induction. If C = ?, then all variables are unconstrained and
therefore enabted, thus we can increment x0 immediately. Otherwise assume
C is nonempty.
We identify a number of cases below, each of which allows us to reduce
the size of the system in some respect (either fewer inequalities or fewer
constrained variables). In each case, the induction hypothesis gives a pro-
cedure for deciding whether the smaller system has a solution, and this will
determine whether (0, C) has a solution.
Case 1 C contains an unconstrained (0, C)-exposed variable. By Lemma
6.14, C is equivalent to a system with fewer inequalities.
Case 2 H(o, C) has a self-loop labeled ?, and ? is (0, C)-enabled. By
Lemma 6.15, C is equivalent to a system with either fewer constrained var?-
ables or fewer inequalities.
Case 3 H(o, C) has a cycle on a set of at least two vertices. By Lemma
6.16, C is equivalent to a system with fewer inequalities.
30
Case 4 None of Cases 1,2, or 3 occur. In this case, consider the tree
T C X* consisting of all (0, C)-admissible paths a E X* The tree T
contains ?he empty string ? and is closed under the prefix relation, and for
any a ? T, ax c T iff x is (Oa, C)-enabled but not (Oa, C)-inhibited. By
Lemma 6.9, (0, C) has a solution if and only if it has one in T.
Now let T' be the subtree of T obtained by deleting all strings containing
a proper prefix of the form aT, where IT > X and Oa <c Oar. By Dickson's
Lemma, T' has no infinite paths, and by K5nig's Lemma, T' is finite. T' can
be constructed effectively since the conditions for extending a branch and for
halting along any path are effective,
Now (0, C) has a solution iff (Oa, C) has a solution for some leaf a of T'
Thus we can consider each leaf separately. The leaves are of two types:
(i)
The leaf is a and the valuation Oa is useless; i.e., all (Oa, C)-enabled
variables are (Oa, C)-inhibited. This is a "natural" leaf, since it has no
(0, C)-admissible extensions.
(ii) The leaf is of the form ar where Oa <c Oar. This is an "artificial"
leaf, since it was obtained by pruning T.
If Oa(xo) > 0 or x0 is (Oa, C)-enabled for some leaf a, we are done.
Otherwise, by Lemma 6.9, leaves of the form (i) have no solution. Thus we
are left with leaves of the form (ii). F?or each such leaf aT, we have
Oa			Oar
Oa			<c			Oar
Since ar is (0, C)-admissible, for every prefix px of r, either
o+ r is constrained in C,
o+ x is (Oap, C)-exposed, or
o+ Oap(x) = 0.
Suppose r contains a variable constrained in C. By Lemma 6.11, H(Oar, C)
contains either an edge out of * or a cycle whose labels are in r. If the former,
we revert to Case 1. If the latter and the cycle is of length at least two, we
revert to Case 3. Otherwise there is a self-loop in H(Oar, C) with label x,
31
where px is a prefix of T. If that self-loop already exists in H(Oap, C), then
since x is Oap-enabled, we revert to Case 2. Otherwise, let vy be the shortest
prefix of T such that H(Oavy, C) contains that self-loop. By Lemma 6.5(vii),
x is Oavy-enaMed, and we revert to Case 2.
If all variables occurring in T are unconstrained in C and at least one is
(Oap, C)-exposed for some prefix p of T, then by Lemma 6.10(ii), H(Oar, C)
has an edge out of *, and we revert to Case 1.
Finally, if all variables occurring in T are unconstrained in C and not
(Oar, C)-exposed, we must have Oap(x) = 0 for every prefix px of r, otherwise
the path would not be admissible. But since Ir > X?, this is impossible.
5
Acknowledgement5
We are indebted to Moshe Vardi for many valuable ideas.
Dexter Kozen was supported by the Danish Research Academy, the Na-
tional Science 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 con-
straints. Technical Report 93-1352, Computer Science Department, Cornell
University, May 1993.
[2]
[3]
A. Aiken and B. Murphy. Implementing regular tree expressions. In Proc.
1991 Conf. Functional Progmmming Languages and Computer Architecture,
pages 427--H447, August 1991.
A. Aiken and B. Murphy. Static type inference in a dynamically typed lan-
guage. In Proc. 18th Symp. Principles of Programming Languages, pages
279--H290. ACM, January 1991.
[4] A. Aiken and E. Wimmers. Solving systems of set constraints. In Proc. 7th
Symp. Logic in Computer Science, pages 329--H340. IEEE, June 1992.
32
[5] Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Set constraints are
the monadic class. In Proc. 8th Symp. Logic in Computer Science. lEEF,
June 1993. to appear.
[6] J. A. Brzozowski and E. Leiss. On equations for regular languages, flMte
automata, and sequential networks. Theor. Cornput. Sci., 10:19--H35, 1980.
[7] D. Cox, J. Little, and D. O'Shea. Ideals, Varieties, and Algorithms. Springer-
Verlag, 1992.
[8] R. Gilleron, 5. Tison, and M. Tommasi. Solving systems of set constraints
using tree automata. In Proc. Symp. Theor. Aspects of Comput. Sci., volume
665, pages 505--H514. Springer-Verlag Lect. Notes in Comput. Sci., February
1993.
[9] R. Gilleron, 5. Tison, and M. Tommasi. Solving systems of set constraints
with negated subset relationships. Technical Report LIFL IT 247, Lille 1
University, March 1993.
[10] N. Heintze and J. Jaffar. A decision procedure for a class of set constraints. In
Proc. 5th Symp. Logic in Computer Science, pages 42--H51. IEEE, June 1990.
[11]
[12]
[13]
N. Heintze and J. Jaffar. A fInite presentation theorem for approximating
logic programs. In Proc. 17th Symp. Principles of Programming Languages,
pages 197--H209. ACM, January 1990.
N. D. Jones and 5. 5. Muchnick. Flow analysis and optimization of LISP-like
structures. In Proc. 6th Symp. Principles of Programming Languages, pages
244--H256. ACM, January 1979.
K. Marriott and M. Odersky. Systems of negative boolean constraints. Techni-
cal Report YALEU/DCS/RR-900, Computer Science Department, Yale Uni-
versity, April 1992.
[14] P. Mishra. Towards a theory of types in PRO LOG. In Proc. 1st Symp. Logic
Programming, pages 289-298. IEEE, 1984.
[15] P. Mishra and U. Reddy. Declaration-free type checking. In Proc. 12th Symp.
Principles of Programming Languages, pages 7--H21. ACM, 1985.
[16] J. C. Reynolds. Automatic computation of data set defInitions. In Information
Processing 68, pages 456--H461. North-Holland, 1969.
33
[17] 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 Corn
putation, pages 573--H581. North-Holland, 1988.
34
