BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR94-1421
ENTRY:: 1994-06-27
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Logical Aspects of Set Constraints
AUTHOR:: Kozen, Dexter
DATE:: May 1994
PAGES::: 14
ABSTRACT::
Set constraints are inclusion relations between sets of ground terms over a 
ranked alphabet. They have been used extensively in program analysis and type 
inference. Here we present an equational axiomatization of the algebra of set 
constraints. Models of these axioms are called termset algebras. They 
are related to the Boolean algebras with operators of Jonsson and Tarski. We 
also define a family of combinatorial models called topological term 
automata, which are essentially the term automata studied by Kozen, Palsberg, 
and Schwartzbach endowed with a topology such that all relevant operations are 
continuous. These models are similar to Kripke frames for modal or dynamic 
logic. We establish a Stone duality between termset algebras and topological 
term automata, and use time to derive a completeness theorem for a related 
multidimensional modal logic. Finally, we prove a small model property by 
filtration, and argue that this result contains the essence of several 
algorithms appearing in the literature on set constraints.
END:: CORNELLCS//TR94-1421
BODY::
Logical Aspects of Set Constraints*
Dexter Kozen
TR 94-1421
May 1994
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
* Proc. 1993 Conf. Computer Science Logic (CSL `93), Eur. Assoc. Cornput. Sci.
Logic, September 1993.
Logical Aspects of Set Constraints*
Dexter Kozen
Computer Sdence Department
Cornell University
Ithaca, New York 14853, USA
kozenOcs cornell. edu
Abstract. Set constraints are inclusion relations between sets of ground
terms over a ranked alphabet. They have been used extensively in pro
gram analysis and type inference. Here we present an equational axiom-
atization of the algebra of set constraints. Models of these axioms are
called tcrmset aigebras. They are related to the Boolean algebru with
operators of J6nsson and Tarski. We also define a family of combinato
rial models called topologica! term automata, which are essentially the
term automata studied by Kozen, Palsberg, and Schwartzbach endowed
with a topology such that all relevant operations are continuous. These
models are similar to Kripke frames for modal or dynamic logic. We ?
tablish a Stone duality between termset algebras and topological term
automata, and use this to derive a completeness theorem for a related
multidimensional modal logic. Finally, we prove a small model property
by filtration, and argue that this result contains the essence of several
algorithms appearing in the literature on set constraints.
1 Introduction
Set constraintsare inclusion relations between sets of ground terms over a ranked
alphabet. They have been used extensively in program analysis and type infer-
ence [29, 21, 27, 28, 32, 20, 3, 4].
Several algorithms for solving general systems of set constraints have ap-
peared [5, I, 2, 7,14, 15, 30, 9]. These algorithms use a variety of interesting
techniques and expose a rich structure touching on monadic second-order logic,
automata on infinite trees, and combinatorics on hypergraphs. Although these
several approaches may appear to differ radically, there are common threads that
underlie them all.
When working with set constraints, it is soon apparent that many basic
properties follow from a few simple algebraic laws, and that a large part of the
basic theory can be developed from a purely algebraic standpoint, independent of
the standard set-theoretic interpretation. In the process of developing this theory,
one discovers that some constructions in the recent literature on set constraints
*
Proc. 1993 Conf. Computer Science Logic (CSL'93), Eur. Assoc. Comput. Sd. Logic,
September, 1993.
can be recast in more classical contexts. One rather unexpected connection is
that the algebraic models presented here and the term automata of [25], which
were developed independently in a completely different context, turn out to be
Stone duals.
In this paper, we present an equational axiomatization of the algebra of sets
of ground terms over a ranked alphabet. We call the models of these axioms
termset algebras. These models form an equational variety and are related to
the Boolean algebras with operators and complex algebras (algebras of subsets
of another algebra) introduced by J6nsson and Tarski [22, 23]; see also [16]. We
also define a family of topological models called topological term astomata, which
are essentially the term automata of [25] endowed with a topology such that all
relevant operations are continuous. We show that these two classes of structures
are Stone duals (see (18, 17]).
We also identify a subfamily of term automata in which the topology is
induced by labelings on the states. These models are quite similar to Kripke
frames for modal or dynamic logic (see [10, 31,17, 26]) and provide a semantics
for a kind of multidimensional modal logic (cf. [31]). We give a completeness
result for this logic. Finally, we prove a small model property by filtration, a
classical technique of modal logic, and argue that this result contains the essence
of [1, Theorem 5.1], [14, Proposition 14], and the proof of decidability of the
Monadic Class given in [13, 2.1] on which the algorithm of [7] is based.
2 Termset Algebras
Let B denote the usual signature of Boolean algebra consisting of symbols +
(join), . (meet), (negation), 0 (bottom), and 1 (top). The operators (impli-
cation), --H (difference), and ? (symmetric difference) are defined as usual:
z			y = ?x + y
x --H y = ?(x y) = x
z e y = (z --H y) + (y --H
The expressions x < y and zy are used to abbreviate x + y = y and z
respectively.
Let ? be a finite ranked alphabet disjoint from B consisting of various func-
tion symbols f, 2,h,..., each with an associated finite arity. Constants are sym-
bols of arity 0 and are denoted a, b,.,... In general, the use of any expression
of the form f(ri,..., rn) carries the implicit assumption that f is of arity n.
Definition 1. A (?.)termset algebra is a structure A of signature ? + B such
that A is a Boolean algebra with respect to the operators B and satisfies
(1)
(2)
(3)
fEE
2
(4)
The ellipses in (1) and (2) indicate that the explicitly given arguments occur in
corresponding places, and that implicit arguments in corresponding places agree.
These axioms define an equational variety. Some immediate consequences are
2.1 Examples
= 0
(5)
(6)
(7)
(8)
(9)
The standard interpretation of set expressions found in the literature on set
constraints (see e.g. [5, 1]) is a model of these axioms. We call this model the
standard tennset algebra. Elements are the subsets of T?, the set of ground terms
over ?. The Boolean operators have their usual set-theoretic interpretations, and
f(A1,...,An)=(f(t1,...,tn)ET? jtiEAi, 1<i<?n)			(10)
The set f(A1,... , An) can be viewed as a marked direct product of the A?;
elements are n-tuples marked with f.
We can also define similar termset algebras consisting of sets of finite and
infinite terms or sets of regular terms [12]. We discuss these models further in
4.2.
There are other examples of termset algebras that have no representation as
sets of terms. We will see several of these examples in the sequel.
2.2 Nondeterministic Termset Algebras
Later in the course of this exposition we will consider a weaker axiomatization
in which equation (2) is replaced by the inequality
(11)
and (5), which no longer follows, is postulated as an axiom. Algebraic models of
these axioms are called nondeterministic termset algebras.
2.3 Boolean Algebras with Operators
Termset algebras are a special case of the Boolean algebras with operators intro
duced by J6nsson and Tarski [22, 23]. These are Boolean algebras satisfying (1)
and (5). An example of a Boolean algebra with operators is the cornpie: algebra
or algebra of subsets of another algebra [16]. We need not postulate (5) as an
axiom for termset algebras, since it follows from (2).
The two chief features that distinguish termset algebras from Boolean alge-
bras with operators and complex algebras are characterized by axiom (2) and
3
axioms (3) and (4). We discuss the former in 3 below. To explain the latter,
note that in the standard termset algebra, the expression .??,..., 1) denotes the
set of all ground terms with head symbol f. Axioms (3) and (4) then capture
the intuition that every term has exactly one head symbol.
2.4 Homomorphisms, Ideals, Ultrafilters
A (terinset algebra) komomorphism is a Boolean algebra homomorphism h
A B such that for all f E ?,
h(!A(zi,...,zn))=!B(h(zi),...,h(xn))
An (termset algebra) ideal in A is a Boolean algebra ideal I with the extra
property
(12)
ideals are kernels of homomorphisms. Maximal ideals are kernels of homomor-
phisms into simple termset algebras, i.e. those with no nontrivial ideals. A dual
ideal in A is a set of the form [?x x E I), where I is a termset algebra ideal.
An filter in A is a Boolean algebra filter (dual Boolean algebra ideal). An
ultrafilter is a maximal filter.
To avoid confusion, we always use the terms filter and ultrafilter in the
Boolean algebra sense and dual ideal and marimal dual ideal in the termset
algebra sense. They are not the same: for example, there is an ultrafilter con-
taining J(a), but no dual ideal contains f(a) (for the same reason that the set
constraint f(a) = 1 is not satisfiable, although here one can give a short algebraic
proof using (12)).
Every filter extends to an ultrafilter; this is a standard application of Zorn's
Lemma [18]. By the same technique one can show that every dual ideal extends
to a maximal dual ideal.
It follows from axioms (3) and (4) that for every ultrafilter u there is exactly
onefE?withA1,...,1)Eu.
3 Connections with Modal Logic
The operator f in a termset algebra behaves like a deterministic modal possibility
operator in each place. If we fix ..... . , Xj?1, Xj+1X? and define
= !(:iXj?1,?,Xj+1xn)
oy =
then ? and 0 satisfy the usual laws of the minimal normal modal logic K [10, 17]:
=0
(oy) < ?(zy)
O(r			y) < Ox			Oy
4
(13)
(14)
(15)
(16)
In addition, because of axiom (2), ? is a deterministic modality in the sense
used in dynamic logic to model deterministic computation (see [26]):
?x < 0:			(17)
o+ (oy) > ?(xy)			(18)
o(x			y) > 0:			Oy			(19)
The laws (17)--H(19) are equivalent in the sense that they are interderivable in
the presence of (13)--H(16).
4 Term Automata
4.1 Infinite Terms
Infinite terms and regular terms are useful in program logic, program specific?
tion and type theory. Regular terms are commonly used to represent recursive
types [6, 8, 24, 25]. The following definition is from Courcelle [12].
Definition 2. Let ? denote the set of natural numbers and let ? be a ranked al-
phabet. A (?-)tenn is a partial function t : ??;* ? whose domain is nonempty,
prefix-closed, and respects arities in the sense that if t(a) is defined then
fi t(ai) is defined) = (1,2,..., arity(t(a)))
A term is regniar if it has only finitely many subterms up to isomorphism.
Example 1. The finite term f(g(a), f(a, 9(b))) is formally a partial map t with
domain fe, 1,2,11,21,22,221) such that t(e) = t(2) = f, t(1) = t(22) =
t(11) = t(21) = a, and t(221) = b. The infinite term f(a,f(a,f(a,...))) is
formally a map 8 whose domain is the infinite set described by the regular
expression 2* + 2*1 such that s(a) = f for a E 2* and s(a) = a for a E 2*1.
The infinite term 8 is regular since it has two subterms up to isomorphism,
namely s and a.
4.2 Term Automata
It is well known that an infinite regular term can be represented by a finite
labeled graph such that the infinite term is obtained by "unwinding" the graph
(see [12,11]). We use the automat?theoretic formulation introduced in [24] of
this idea.
Definition 3. A (?-)term automaton is a tuple
M = (Q, ?, e, 6)
where:
--H Q is a set of states (not necessarily finite)
5
is a ranked alphabet
e : Q I; is a ia?e1ing
6 : Q x ??			Q is a partial function such that for all q E Q,
6(q, i) is definedj = (1, 2,.. ., anty((q)))
The function 6 extends uniquely to a partial function ?: Q x w* Q according
to the inductive definition
= q
?(q,ai) =
with the understanding that 6 is strict (undefined if one of its arguments is
undefined). For each q E Q, the partial function
tq = Aa.?(i(q, a))
is a 1'-term in the sense of Definition 2.
Every term in the sense of Definition 2 is tq for some state q of some term
automaton. In fact, t = tc in the syntactic term automaton
= ((?-terms), ?, ?, 6)
where t(t) = t(E) and 6(t, i) = Aa.t(ic), 1 < i < arity((t)). In this sense the
notion of term automaton (Definition 3) is a generalization of the notion of term
(Definition 2).
A term is regular iff it is tq for some state q of some finite term automaton
[25, Lemma 8]. For example, if q is the state labeled f in the term automaton
a
then tq is the infinite regular term s of Example 1 of 4.1.
The syntactic term automaton I? defined above has a subautomaton RE
consisting of the regular terms, which in turn has a subautomaton TE consisting
of the finite terms.
4.3 Term Automata and Set-Theoretic Termset Algebras
Let M = (Q, ?, e, 6) be a term automaton. For f E ?, define the partial
function R1M : Q Qfl and the set-theoretic function 1M : (2Q)fl 2q by
RjM(q)=			(20)
fM(Ai,...,An)=
(6(q,1),...,6(q,n)) ,if?(q) = I
undefined ,			otherwise.
fqEQt(q)=fand6(q,i)EAi 1<i<n)
= (RM,)-1(A1 ?.. x An).
6
(21)
The family of subsets of Q can be endowed with a termset algebra structure
by giving the Boolean operators their usual set-theoretic interpretations and
interpreting f as fM. One can show that this gives a termset algebra. Such
an algebra, or a subalgebra of such an algebra, is called a set-theoretic termset
algebra.
4.4 Topological Term Automata
Let ? have the discrete topology. A topological term astomaton is a term au-
tomaton
M = (Q, ?, e, 6)
endowed with a topology on Q such that the functions e and Aq.6(q, i) are contin-
uous; equivalently, such that the partial maps R1M defined in (20) are continuous
in the product topology on Qn
The topological term automaton M gives rise to a particular se?theoretic
termset algebra Cl M whose elements are the clopen (closed and open) subsets
of Q. These sets form a Boolean algebra, and the continuity of e and 6 insure
that the operations fOl M defined by (21) preserve clopen sets.
Morphisms of topological term automata are continuous maps h : M1 M2
preserving e and 6 in the sense that
h(6i(q, i)) = 62(h(q), i)
5 Stone Representation and Duality
5.1 A Representation Theorem
The following representation theorem says that every termset algebra is rep-
resented by a topological term automaton. The proof is a standard ultrafilter
construction (see [18, 17]).
Theorem4. Every termset algebra is isomoryhic to a set-theoretic termset al-
gebra.
Proof. Given a termset algebra A, define the term automaton
stA=(U, 1', e, 6)
where U is the set of ultrafilters of A, (?) is the unique f E ? such that
fA(1,...,1)Et,and
6(u,i)=(xEAIfA(?:?.,1,r,m).,1EuJ
i--Hi			n--Ht
7
One must show that the set 6(u, i) is an ultrafilter; this follows from the elemen-
tary properties of termset algebras. Now for x E A, define
h(x) = ?u E U x E t)
and let the sets h(r) generate a topology on St A. Then cl St A forms a set-
theoretic termset algebra as described in 4.4 and h : A cl St A is a termset
algebra isomorphism.
We argue explicitly that h is a homomorphism with respect to f E 1::
fCl St A(h(x1),..., h(:n))
= flu) = f and 6(u,i) E h(xi), 1 <i < n?
(uI!A(1,...,1)EuandriE6(u,i), 1<i?<n)
??uIfA(11)EuandfA(1,...,1,xj,1,...,1)Eu 1<i<n)
i--Hi			fl--HI
= (1 fA(:1xn) E u)
That h is one-t?one follows from the fact that every filter extends to an ultr?
filter.
5.2
Duality
Let A be a termset algebra and let St A be its associated topological term
automaton as constructed in 5.1. As a topological space, St A is compact,
Hausdorff, and has a base of clopen sets (namely fh(r) x E A?). A topological
term automaton with these properties is called Stone.
Let STA denote the category of Stone automata and continuous maps pre-
serving e and 6, and let TSA denote the category of termset algebras and termset
algebra homomorphisms. Defining St h --H h-1 for a termset algebra homomor-
phism h, the construction St becomes a contravariant functor TSA STA.
Similarly, defining Cl g = g?1 for a morphism g : M N of topological term
automata, the construction Cl becomes a contravariant functor STA TSA.
Moreover, these functors are bijections on the homsets of TSA and STA, and
are inverses up to isomorphism, thus constitute a Stone duality (see [18]).
6 Completeness
6.1 Annotated Term Automata
Definition 5. Let X=fP,Q,...) be a set ofpropositional letters. An annotated
term atttomaton is a tuple
M = (Q, ?, ?, 6, X, p)
where (Q, ?, e, 6) is a term automaton and p : X 2Q. We topologize M
by taking the weakest topology such that all p(P) are clopen and e and 6 are
continuous.
8
Annotated term automata provide a Kripke frame semantics for the mul-
tidimensional propositional modal logic discussed in 3. Syntactically, we may
view formulas ? as ground terms over the ranked alphabet ? u x1 where the
propositional letters X have arity 0. From a technical standpoint, however, it
will be more convenient to use a more abstract syntax in which formulas are
elements of ?x, the free termset algebra on generators X, and work implicitly
modulo the axioms of termset algebra.
To define satisfaction over M, extend p uniquely by induction to a termset
algebra homomorphism p : Cl M. We write M, q k ? and say ? is
satisfied at q in M if q E p(?). We write M k o and say that tp is realized in M
if p(tp) = Q. Define Th M, the theory of M, to be the set of formulas realized by
M. This is a dual ideal (?o tp E ker pJ. Since p is onto, ?x/Th M ? Cl M.
The free termset algebra ?? on generators X naturally gives rise to an
annotated term automaton (St Yx, X, p), where p(P) = P E uJ. For this
structure, p(o) = fu tp E t), thus p is just the Stone isomorphism p : Yx
Cl St ?x.
6.2 Completeness
We consider a proof system consisting of the axioms of termset algebra and the
usual rules of modal logic, namely modus ponens and modal generalization. The
latter rule takes the form
0
(22)
in this context. A set of formulas is consistent if its deductive closure does not
contain 0. The following lemma and theorem establish deductive completeness
of this system over annotated term automata.
Lemma6. A set of formulas is consistent and deductively closed if and only if
it is a dual ideal in ?x.
In the proof of this lemma, the rule of modal generalization (22) corresponds
directly to the property 2.4(12) of termset algebra ideals.
If ? is consistent, let ?x/? denote the quotient of ?x modulo the deductive
closure of ?, which is a dual ideal by Lemma 6.
Theorem 7. A set offormulas is consistent if and only if it is realizable.
Proof Let ? be a given consistent set of formulas. The Stone dual St ?x/? of
the quotient ?x/? with annotations
p(P) = (u P E uJ
is the desired annotated term automaton realizing ?. Conversely, any Th M is
a dual ideal and thus consistent by Lemma 6.
9
7 Solutions of Set Constraints
In [19, 5,1, 2, 7, 9, 14, 15, 30], various techniques for the solution of systems of
set constraints are given. Here we introduce yet another approach.
Let ? be a set of formulas `0 (representing the set constraints (p = 1 in
the sense of [1]) and let X be the set of propositional letters occurring in ?. A
standard solution of the constraints ? is an annotation of the finite syntactic term
automaton T? defined in 4.2 such that the resulting annotated term automaton
realizes ?.
Definition 8. A term automaton M = (Q, ?, e, 6) is said to be closed if for
all qi,. . ., q? E Q and f E ? of arity n, fM([q1),..., fq?)) is nonempty; i.e.,
there exists q E Q such that ?(q) = f and 6(q,i) = q?, 1 <i <n.
This notion of closure corresponds directly to the notion of closure in hyper-
graphs defined in [1]. We can characterize this property algebraically:
Definition 9. A termset algebra is closed provided it satisfies the property
f(xi,...,:n)=O?V(xi=O)			(23)
i=i
A dual ideal ? is closed provided
(24)
i=i
Thus the quotient A/? is closed iff the dual ideal ? is. The following lemma says
that the algebraic and combinatorial notions of closure defined above coincide
under Stone duality.
Lemma 10. A termset algebra A is closed in the sense of Definition 9 iff its
Stone dual St A is closed in the sense of Definition 8. For any closed topological
term automaton M, Stone or not, Cl M is closed.
Theorem 11. Let ? be a set of formulas. The following statements are equiva-
lent:
has a standard solution
(ii) ? has a consistent extension ? satisfying (24)
(iii) St ?x/? has a closed subautomaton.
Proof. (i) (ii): Let p be an annotation of T? realizing ?, and let M be the
resulting annotated term automaton. Then Th M is a dual ideal extending ?,
and satisfies (24) by Lemma 10.
(ii) (iii): By Stone duality, St ?x/? embeds into St ?x/?, and by Lemma
10, St ?x/? is closed.
10
(iii) (i): Let M be a minimal closed subautomaton of St ?x/? One can
construct by induction a map o': T? M such that
6(ff(f(t1,...,tn)),i)=?(tj) 1<i<n
rinsed sub.			of M
The image of ff is a ?LwflaLull , and since M is minimal, 0' is
onto, Also, ? is one-toone, since 0'(t) satisfies the formula t, and these formulas
are pairwise inconsistent. The annotation of TE realizing ? is inherited from M
under the bijection 0'.
7.1 Filtration
In [1], an exponential-size hypergraph H for a given finite collection of set con-
straints ? was constructed by ad hoc means. The hypergraph H is described by
Boolean formulas obtained from ?. It was proved that ? has a solution iff H has
a closed induced subhypergraph [1, Theorem 5.1].
The graph H is essentially a filtrate of ?x/? and can be obtained by a
standard filtration construction of modal logic (see [10, 17, 26]), which we outline
here.
Determinacy is not preserved under the filtration construction. Thus we must
work with nondeterministic termset algebras as defined in 2.2.
Definition 12. A nondeterministic term a?tomaton is a frame
N = (Q, i:, e, R)
such that for each f E L, R gives a total map R1 : Q 2? (instead of a
partial map Q Qfl as with deterministic term automata). Analogous to (21),
forA1,...,A? c Qwedefine
fN(A1...,A?)=[qEQRf(q)nA1x...xAn??.
Lemma 13. The frame N gives a set-theoretic nondeterministic termset algebra
under the construction of 4.3.
Given an annotation p : X 2?, we define satisfaction as in 6.1, except
here we must consider formulas as elements of the free nondeterministic termset
algebra instead of Yx.
Let ? be a set of formulas over atomic formulas X. Let ? be the smallest set
of formulas containing ? such that
A1,...,1)E?forallfE?
1<i<n
i--Hi
--H any subformula of a formula in ? is in ?.
Let M = (QM, ,"`, eM, 6M, ?, PM) be an annotated term automaton. The
standard filtration construction of modal logic applied to M yields an annotated
nondeterministic term automaton N --H (QN ,"`, eN, RN, x, pN), where
11
--H [q]=(pIforalloE??pEpM(o)?qEpM(o))
--H QN=[[q]?qEQM)
--H eN([q]) --H
(q1,...,q?)ERMj(q))
--H ?1N([p])=((?1],...,??])??qEQM [q]=[p],
--H pW(p)=([q]jqEpM(P)).
Lemmal4. ForoE? [q] EpN(o) if and onl? if q?pM(o).
Proof. Induction on the structure of 0 (see [17,101).
The following theorem is a restatement of [1 Theorem 5.1].
Theorem 15. A set ? of fonnttlas has a standard solution if and only if the
filtrate N of St ?x/? by ? has a closed subautomaton.
Proof. By Lemma 11, ? has a standard solution iff St Yx/? has a closed subau-
tomaton. The image of any closed subautomaton of St ?x/? under the filtration
map q [q] is a closed subautomaton of N. Conversely, if N has a closed sub
automaton, as in the proof of Theorem 11 we can define a map ?: T? N by
induction such that
ff(f(titn)) E fN([g(t1)),...,[ff??)))
The annotation of TE realizing ? is inherited from N under ?. Let
T
p r(P)=(tI?(t)EpN(P))
One can argue inductively that for all t E T? and for all ? E ?,
t E pTE(0) ? ff(t) E pN(0) .			(25)
The argument is straightforward except for the case o=f(oi,.. , on) which
we argue explicitly. For the direction (?),
tEpTL(Aol,...,on))
??=f?1,..,t?)Atj?pT?(0j), l<i<n
= f(t1,...,tn) A?(ti) E pN(0j), 1 <i < n (induction hypothesis)
? ?(t) EpN(f(ol,...,on))
Conversely,
t?pTEU(olon))
?tEpTn(Zg(1,...,1)+?f(m.,1?oi,A)..,1)
g#J			i=1			i--Hi			fl--Hi
ff(t)			______			______
I#f
i--Hi
12
by the preceding argument. But then ff(t) ? pN(f(?1,... , o?)), since
pN(?g(1,...,1)+?f(?.,1, ?(pi,&w.,1)npN(f(tpl,...,?n)) =
g$f			i=1			i--Hi			fl--HI
because by Lemma 14 this set is the image under the ffltration map t [t'] of
i=1
i--Hi			fl--HI
Since St ?x/? realizes ?, so does N by Lemma 14, and so does T? by (25).
References
1. A. AiKEN, D. KoZEN, M. VARDI, AND E. WiLorEus, The complerity of set con-
straints. This volume.
2. A. AIKEN, D. KoZEN, AND E. WIMMERS, Decidability of systems of set constraints
with negative constraints, Tech. Rep. 9?1362, Computer Science Department, Cor-
nell University, June 1993.
3. A. AIKEN AND B. Mui?HY, Implementing regular tree erpressions, in Proc. 1991
Conf. Functional Programming Languages and Computer Architecture, August
1991, pp. 427447.
4. , Static type inference in a dynamically typed language, in Proc. 18th Symp.
Principles of Programming Languages, ACM, January 1991, pp. 279--H290.
5. A. AIKEN AND E. WIMMERS, Solving systems of set constraints, in Proc. 7th Symp.
Logic in Computer Science, IEEE, June 1992, pp. 329--H340.
6. R. M. AMADlo AND L. C??ELLi, Subtyping recursive types, in Proc. 18th Symp.
Princip. Programrning Lang., ACM, January 1991, pp. 104-118.
7. L. BAcHMAnt, II. GANzrNGER, AND U. WALDMANN, Set constraints are the
monadic class, in Proc. 8th Symp. Logic in Computer Science, IEEE, June 1993,
pp. 75--H83.
8. L. CARDELLI AND P. WEGNER, On understanding types, data abstraction, and
polymorphism, Computing Surveys, 17:4 (1985), pp. 471--H522.
9. W. CHARAToNIK AND L. PAcHoLsKi, Negative set constraints with equality, in
Proc. 9th Symp. Logic in Computer Science, lEEE, July 1994. To appear. Also,
Max-Planck-Institut fur Informatik Technical Report MPI-I-93-265.
10. B. F. CHELLAS, Modal Logic: An Introduction, Cambridge University Press, 1980.
11. A. CoLMERAUER, FROLOG and infinite trees, in Logic Programming, 5.-A.
Tarnlund and K. L. Clark, eds., Academic Press, January 1982, pp. 231--H251.
12. B. Coui?CELLE, Fundamental properties of infinite trees, Theor. Comput. Sci., 25
(1983), pp. 95--H169.
13. B. DREBEN AND W. D. GoLDFARB, The Decision Problem: Solvable Classes of
Quantificational formulas, Addison Wesley, 1979.
14. R. GILLERoN, 5. 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--H514.
15. , Solving systems of set constraints with negated subset relationships, in Proc.
34th Symp. Foundations of Comput. Sci., IEEE, November 1993, pp. 372--H380.
13
16.
17.
18.
19.
20.
21.
R. GowBLATT, Varieties of complex algebras, Annals of Pure and Applied Logic,
44 (1989), pp. 173--H242.
Mathematics of Modality, vol. 43 of CSLI Lecture Notes, Center for the
Study of Language and Information, 1993.
P. R. HALMOS, Lectures on Boolean algebras, Springer-Verlag, 1974.
N. HErNTzE AND 3. JAFFAR, A decision procedure for a class of set constraints, in
Proc. 5th Symp. Logic in Computer Science, IEEE, June 1990, pp. 42--H51.
A finite presentation theorem for approximating logic programs, in Proc.
17th Symp. Principles of Programming Languages, ACM, January 1990, pp. 197--H
209.
N. D. J0?Es AND 5. 5. MucHNicK, Flow analysis and optimization of LISP-like
structures, in Proc. 6th Symp. Principles of Programming Languages, ACM, Jan-
uary 1979, pp. 24?256.
22. B. J6NSSON AND A. T??xi, Boolean algebras with operators, Amer. 3. Math., 73
(1951), pp. 891--H939.
23. , Boolean algebras with operators, Amer. 3. Math., 74 (1952), pp. 127--H162.
24. D. KOzEN, 3. PALsBERG, AND M. I. Sc?ARTzBAcH, Efficient inference of partial
types, in Proc. 33rd Symp. Found. Comput. Sci., IEEE, October 1992, pp. 363--H371.
25. , Efficient recursive subtyping, in Proc. 20th Symp. Princip. Programming
Lang., ACM, January 1993, pp. 419428.
26. D. KOZEN AND 3. TwayN, Logics of programs, in Handbook of Theoretical Com-
puter Science, van Leeuwen, ed., vol. B, North Holland, 1990, pp. 789--H840.
27. P. MisHitA, Towards a theory of types in PROLOG, in Proc. 1st Symp. Logic
Programming, IEEE, 1984, pp. 289--H298.
28. P. MiS?A AND U. RDDY, Declaration-free type checking, in Proc. 12th Symp.
Principles of Programming Languages, ACM, 1985, pp. 7-21.
29. 3. C. RE?oLDS, Automatic computation of data set definitions, in Information
Procesring 68, North-Holland, 1969, pp. 456461.
30. K. STEFAuSSON, Systems of set constraints with negative constraints are
NEXPTIME-complete, in Proc. 9th Symp. Logic in Computer Science, IEEE, June
1994. To appear. Also Cornell University TR93-1380, August 1993.
31. Y. VENEMA, Many-Dimensional Modal Logic, PhD thesis, Universiteit van Am?
terdam, January 1992.
32. J. YOuNG AND P. O'KEEFE, Experience with a type evaluator, in Partial Evalu-
ation and Mixed Computation, D. Bj?rner, A. P. Ershov, and N. D. Jones, eds.,
North-Holland, 1988, pp. 573--H581.
This article was processed using the ?T? macro package with LLNCS style
14
