A Decision Procedure for a Class of Set Constraints

Nevin Heintze^{1} and Joxan Jaffar^{2} February 14, 1991

CMU-CS-91-110

School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213

A preliminary version of this paper appears in the Proceedings, 5^{th} IEEE Symposium on LICS.

1The first author is supported by an IBM Graduate Fellowship. 2IBM Thomas J. Watson Research Center, PO Box 218, Yorktown Heights, NY 10598

Keywords: set constraints, program analysis, decision procedures

Abstract

A set constraint is of the form exp_{1} ⊇ exp_{2} where exp_{1} and exp_{2} are set expressions constructed using variables, function symbols, projection symbols, and the set union, intersection and complement symbols. While the satisfiability problem for such constraints is open, restricted classes have been useful in program analysis. The main result herein is a decision procedure for definite set constraints which are of the restricted form a ⊇ exp where a contains only constants, variables and function symbols, and exp is a positive set expression (that is, it does not contain the complement symbol). A conjunction of such constraints, whenever satisfiable, has a least model and the algorithm will output an explicit representation of this model.

1 Introduction

We consider a formalism for elementary set algebra which is useful for describing properties of programs whose underlying domain of computation is a Herbrand universe. The domain of discourse for this formalism is the powerset of this universe. Its functions include set union, intersection and complement, in addition to a family Σ of functions intended to be the set-based counterparts of the functions used in the program. More specifically, all functions f in Σ satisfy a distributive property such as f(X∪Y) = f(X)∪f(Y). Finally, for each n-ary symbol f in Σ, we have a conjunction f_{(1)}^{−1}, ⋯, f_{(n)}^{−1} representing the projections of f. A set constraint is of the form sexp_{1} ⊇ sexp_{2} where sexp_{1} and sexp_{2} are set expressions constructed using the above function symbols and variables. The satisfiability problem for a conjunction of set constraints is open; the rest of this section discusses important decidable sub-classes.

Set based reasoning can be expressed in the predicate calculus by regarding a unary predicate as the set of values on which it is true. There are decidability results which deal with cases where the symbols are unary; see [1] for example. (These results were in fact shown for the second-order calculus.) Rabin [8], using the second-order theory of k successors and a standard interpretation, showed that the sets definable are recursive, and furthermore, he showed that there are algorithms to decide questions such as emptiness and containment. These works, however, have limited application to reasoning about programs since they are restricted to unary symbols.

Decision procedures have been obtained for set constraints involving function symbols of arbitrary arity, but at the cost of restricting the use of quantifiers, logical connectives, complement and intersection. Such procedures have been useful in an area of program analysis concerned with approximating the set of values that a variable may take at runtime. These approximations can be described using set constraints by first associating a set variable with each program variable. Set constraints can then be used to impose relationships between the set variables so that any model of these constraints defines a superset of the actual run-time values. In summary, set constraints provide a methodology of program approximation which ignores dependencies between variables.

Reynolds [9] and Jones and Muchnick [5], for example, considered functional programs and used a class of set constraints whose satisfiability is guaranteed. The focus of these works was to provide an explicit representation of the model defined by the constraints. Mishra [7], in his framework for type inference in logic programs, used set constraints to model a superset of the success set of a program.

Though a full decision procedure was not presented, algorithms for subcases were investigated. Heintze and Jaffar [4] used set constraints to obtain a recursive and accurate approximation of the meaning of a logic program.

In this paper, a decision procedure is presented for the class of definite set constraints which have the form a ⊇ sexp where a contains only constants, variables and function symbols, and sexp is a positive set expression. Restriction to definite constraints is analogous to the restriction to definite clauses from general clauses in the sense that a definite set constraint has a least model whenever it has a model. This class of constraints is expressive enough to be useful for modeling program properties via constraints (for example, see the references cited above). An important aspect of the procedure presented is that if the input constraints are satisfiable, then the procedure constructs an explicit representation of the least model of the constraints.

The following section contains some initial definitions, and some basic properties of set expressions. Section 3 describes a grammar formalism based on set expressions which is a generalization of term grammars. In essence, the main algorithm of this paper is a transformation system based on set expression grammars. Section 4 deals with a subclass of definite set constraints which alway have least models. This section contains the core algorithm. Section 5 then applies this algorithm to obtain the main result. Finally, appendix I gives some example of executions of one of the main algorithms presented, and appendix II gives some examples of how definite set constraints can be used to analyze program properties.

2 Preliminaries

Let V denote a denumerable set of variables, and let Σ denote a denumerable set of function and constant symbols; we assume that Σ contains at least one constant. Let τ(Σ) and τ(Σ ∪ V) and denote the corresponding Herbrand universe (HU)^{1} and Herbrand terms. Let var(t), where t is any expression, denote the set of variables appearing in t. If var(t) is the empty set, then t is said to be ground. Let A, A_{1}, ⋯, A_{n} ⊆ τ(Σ), n ≥ 1, and let f be an n-ary symbol in Σ. Then

f(A_{1}, ⋯, A_{n}) =^{def} {f(a_{1}, ⋯, a_{n}) : a_{i} ∈ A_{i}}, and f_{(i)}^{−1}(A) =^{def} {a_{i} : f(a_{1}, ⋯, a_{n}) ∈

A}.

A set expression is defined to be either a variable or constant, the special constant ⊥ or ⊤, or of one of the forms f(sexp_{1}, ⋯, sexp_{n}), f_{(i)}^{−1}(sexp), sexp ∪ sexp′, sexp ∩ sexp′ and \overline{sexp} where 1 ≤ i ≤ n, f ∈ Σ is n-ary, and sexp, sexp′, sexp_{1}, ⋯, sexp_{n} are set expressions. A set expression is atomic if it does not contain any union, intersection, projection or complement symbols. An occurrence of an expression in a set expression is nested if it occurs within the scope of a function or projection symbol. A set constraint is of the form sexp_{1} ⊇ sexp_{2}; if sexp_{1} is atomic and sexp_{2} does not contain the complement symbol, then we say that the set constraint is definite.

1We assume throughout that HU contains at least two elements.

An interpretation is a map from V ⟶ 2^{HU}. An interpretation I, induces, in an obvious way, a mapping from set expressions sexp into 2^{HU} as follows. I(⊥) = ◯̸; I(⊤) = HU; I(c) = {c} where c ∈ Σ is a constant; I(f_{(i)}^{−1}(sexp′)) = f_{(i)}^{−1}(I(sexp′)) and I(f(sexp_{1}, ⋯, sexp_{n})) = f(I(sexp_{1}), ⋯, I(sexp_{n})) where f ∈ Σ is n-ary; and finally, I(sexp_{1}∪sexp_{2}) = I(sexp_{1})∪I(sexp_{2}) and I(sexp_{1}∩sexp_{2}) = I(sexp_{1}) ∩ I(sexp_{2}) and I(\overline{sexp′}) = HU − I(sexp′). This mapping, in turn, induces a mapping from conjunctions of set constraints C into true or false in the obvious way. If I maps C into true, we say that I is a model of C. We write I ⊇ I′ if I(X) ⊇ I′(X) for all X ∈ V. Where C and C′ are conjunctions of set constraints and S is a set of variables, we write C ⟺_{S} C′ if C and C′ are equivalent in the sense that for any model I of C, there is a model I′ of C′ such that I′(X) = I(X) for all X ∈ S, and symmetrically, for any model I′ of C′, there is a model I of C such that I(X) = I′(X) for all X ∈ S.

In the remainder of the paper, we consider only set expressions which do not contain the complement symbol, and adopt the convention that, unless otherwise specified, a set expression sexp does not contain this symbol. Such expressions satisfy some basic monotonicity properties, which can be proved using simple structural induction arguments.

Proposition 1 (Monotonicity) If I_{1} ⊆ I_{2} then I_{1}(sexp) ⊆ I_{2}(sexp).

Proposition 2 (Substitition) Let sexp′ be the result of replacing an occurrence of a sub-expression t in sexp by t′. Then I(t′) ⊆ I(t) implies I(sexp′) ⊆ I(sexp).

The following are some basic properties about interpretations on ground set expressions sexp and sexp′: (a) I(sexp) denotes a unique set regardless of the choice of I – denote this by [[sexp]]; (b) if sexp does not contain any union symbols, then there is a unique ground atomic set expression a such that [[sexp]] = [[a]]; (c) if sexp is atomic and different from the symbols ⊥ and ⊤, then [[sexp]] = {sexp}.

Consider next the problem of explicitly representing a given interpretation. What is required is a representation which can be used to verify whether or not an arbitrary set constraint is true in the interpretation. Toward this aim, define that a term grammar ([3], p.67) is a grammar G whose nonterminals are variables in V, and each rule is of the form X ⟹ t where X is a variable and t is an atomic set expression. Derivability =G⇒ is defined in an obvious way: sexp =G⇒ sexp′ if sexp′ is the result of replacing one occurrence of a variable X in sexp by t, and X ⟹ t is a rule in G. A term grammar G then defines an interpretation I_{G} since it associates to each variable a set of ground terms as follows:

I_{G}(X) = ⋃_{X =G⇒⋆ t}[[t]]

where t ranges over ground terms and =G⇒⋆ is the reflexive and transitive closure of =G⇒^{2}.

We note that a term grammar is essentially a parenthesis grammars [6]. The class of languages definable by term grammars is exactly the class accepted by tree automata^{3}. Moreover a term grammar can be viewed as a description of a non-deterministic finite tree automata and vice-versa. Hence there are algorithms for combining term grammars over the boolean and projection operations, and for testing emptyness and containment (see [10], [2]; also see [3] for a survey of relevant results). This means that, given a representation of an interpretation I in the form of a term grammar, standard algorithms from the literature can be used to check whether a given set constraint, sexp_{1} ⊇ sexp_{2}, is true in I.

The main result of this paper can now be stated as follows. Given a conjunction of definite set constraints, the algorithm presented in this paper:

(a) determines if the conjunction is satisfiable, and

(b) if so, outputs a term grammar which represents its least model. Now, since any term grammar for a language L can be used to build a conjunction of definite set constraints whose least model is L, it follows that the sets definable as the least model of definite set constraints are exactly those definable by regular term grammars.

2In what follows, we may abbreviate =G⇒⋆ by ⟹^{⋆} whenever there is only one grammar G in context.

3In terms of later definitions (e.g. [3]), these automata are the frontier-to-root tree automata.

3 Set Expression Grammars

We now define a class of grammars, generalizing term grammars, intended to provide a representation of an interpretation which is more explicit than the conjunction of set constraints at hand, but not necessarily as explicit as a term grammar. That is, we cannot, in general, directly determine whether or not a given set constraint is true in the interpretation defined by a set expression grammar. (This is in contrast to a term grammar representation of an interpretation.) A key result of this paper, presented in the next section, is that a set expression grammar can be transformed into an equivalent term grammar.

A set expression grammar G is defined to be like a term grammar except that each rule X ⟹ sexp in G is such that sexp may contain intersection and projection symbols^{4}. As with term grammars, G defines an interpretation, call it I_{G},

I_{G}(X) =^{def} ⋃_{X⟹^{⋆}sexp}[[sexp]]

where X ∈ V AR and sexp is a ground set expression. Consider for example the set expression grammar G consisting of the two rules X ⟹ f(X)∩f(a) and X ⟹ a. Here the only ground set expressions derivable from X are f(a) ∩ f(a) and a, and so I_{G} maps X to the set {f(a), a} and all other variables to ◯̸. We conclude with three properties of a set expression grammar G.

Proposition 3 Let ψ be a function symbol, a projection symbol or an intersection symbol. Let the arity of ψ be n and let t_{1}, ⋯, t_{n}, t′_{1}, ⋯, t′_{n} be set expressions. Then

ψ(t_{1}, ⋯, t_{n}) ⟹^{⋆} ψ(t′_{1}, ⋯, t′_{n}) iff t_{1} ⟹^{⋆} t′_{1}, ⋯, t_{n} ⟹^{⋆} t′_{n}.

Proof: One direction is clear: the derivations t_{1} ⟹^{⋆} t′_{1}, ⋯, t_{n} ⟹^{⋆} t′_{n} can be immediately combined to yield a derivation ψ(t_{1}, ⋯, t_{n}) ⟹^{⋆} ψ(t′_{1}, ⋯, t′_{n}). Conversely, suppose that ψ(t_{1}, ⋯, t_{n}) ⟹^{⋆} ψ(t′_{1}, ⋯, t′_{n}). Then there must be a derivation of the form

ψ(t_{1}, ⋯, t_{n}) ⟹ ψ(t_{1}^{(1)}, ⋯, t_{n}^{(1)}) ⟹ ψ(t_{1}^{(2)}, ⋯, t_{n}^{(2)}) ⟹… ⟹ ψ(t_{1}^{(k)}, ⋯, t_{n}^{(k)})

where ψ(t_{1}^{(k)}, ⋯, t_{n}^{(k)}) is ψ(t′_{1}, ⋯, t′_{n}) and k ≥ 0. Then, for each 1 ≤ i ≤ n, this defines a sequence t_{i}, t_{i}^{(1)}, t_{i}^{(2)},…, t_{i}^{(k)} such that if s is immediately after some t in this sequence then either s is equal to t or t ⟹ s. It then follows that we can construct a derivation t_{i} ⟹ … ⟹ t′_{i}, and so t_{i} ⟹^{⋆} t′_{i}, as required.

4The union and complement symbols are still omitted.

Note that the next property may not hold if sexp contains the union symbol; for example, if G consists of the single rule X ⟹ a then I_{G}(X ∪ Z) is {a}, but there are no ground expressions derivable from X ∪ Z and so ⋃_{X∪Z⟹^{⋆}sexp′}[[sexp′]] is

the empty set.

Proposition 4 Let sexp be a set expression which does not contain the union symbol^{5}. Then, where sexp′ ranges over ground set expressions,

I_{G}(sexp) = ⋃_{sexp⟹^{⋆}sexp′}[[sexp′]]

Proof: The proof is by structural induction on sexp. The base cases are as follows: if sexp is a variable, then the proposition follows immediately from the definition of I_{G}; if sexp is a constant, then sexp ⟹^{⋆} sexp′ implies that sexp′ = sexp, and so the result follows from the fact that I_{G}(sexp) = [[sexp]].

To prove the induction case, suppose that sexp is the set expression ψ(t_{1},…, t_{n}) where the proposition holds for t_{1}, ⋯, t_{n}, and let ψ be a function, projection or intersection symbol of arity n. Then:

I_{G}(ψ(t_{1}, ⋯, t_{n})) = ψ(I_{G}(t_{1}), ⋯, I_{G}(t_{n}))
= ψ( ⋃_{t_{1}⟹^{⋆}t′_{1}}[[t′_{1}]], ⋯, ⋃_{t_{n}⟹^{⋆}t′_{n}}[[t′_{n}]])
= ⋃_{ψ(t_{1},···,t_{n})⟹^{⋆}ψ(t′_{1},···,t′_{n})}[[ψ(t′_{1}, ⋯, t′_{n})]]

where t′_{1},…, t′_{n} range over ground set expressions. The first equality is just the definition of interpretation. The second equality follows from the induction assumption. To prove the third and last equality, we show that any element of the left hand side (l.h.s.) must be an element of the right hand side (r.h.s.) and viceversa. First, let g be an element of the l.h.s. Since ψ is either a function, projection or intersection symbol, it is easy to verify that there must exist t′_{1}, ⋯, t′_{n} such that t_{i} ⟹^{⋆} t′_{i}, 1 ≤ i ≤ n, and g ∈ ψ([[t′_{1}]],…, [[t′_{n}]]). From proposition 3, ψ(t_{1},…, t_{n}) ⟹^{⋆} ψ(t′_{1},…, t′_{n}). That g is an element of the r.h.s. then follows from the equality ψ([[t′_{1}]],…, [[t′_{n}]]) = [[ψ(t′_{1},…, t′_{n})]]. Now let g be an element of the r.h.s.

Then there must exist ψ(t′_{1}, ⋯, t′_{n}) such that ψ(t_{1}, ⋯, t_{n}) ⟹^{⋆} ψ(t′_{1}, ⋯, t′_{n}) and

g ∈ [[ψ(t′_{1},…, t′_{n})]]. Again, using the equality ψ([[t′_{1}]],…, [[t′_{n}]]) = [[ψ(t′_{1},…, t′_{n})]] and proposition 3, proves that t_{i} ⟹^{⋆} t′_{i}, 1 ≤ i ≤ n and that g ∈ ψ([[t′_{1}]],…, [[t′_{n}]]). It is easy to verify that this implies that g is an element of the l.h.s. of the final equality.

5By our convention, sexp also does not contain the complement symbol.

Proposition 5 If sexp_{1} ⟹^{⋆} sexp_{2} then I_{G}(sexp_{1}) ⊇ I_{G}(sexp_{2}).

Proof: We first prove the proposition in the case that sexp_{1} is a variable, say X. In this case, neither sexp_{1} nor sexp_{2} contain the union symbol, and so proposition 4 may be applied to obtain:

\begin{aligned}I_{G}(X) & = & ⋃_{X⟹^{⋆}sexp′}[[sexp′]] \\ I_{G}(sexp_{2}) & = & ⋃_{sexp_{2}⟹^{⋆}sexp′}[[sexp′]] \end{aligned}

Now, since sexp_{2} ⟹^{⋆} sexp′ implies X ⟹^{⋆} sexp′, it follows that I_{G}(X) ⊇ I_{G}(sexp_{2}).

To complete the proof, let V_{1},…, V_{n} denote the occurrences of variables in sexp_{1}. Then, the derivation sexp_{1} ⟹^{⋆} sexp_{2} may be decomposed into applications of rules corresponding to each V_{i}. These define, for each 1 ≤ i ≤ n a derivation V_{i} ⟹^{⋆} t_{i} such that the result of replacing each occurrence V_{i} in sexp_{1} by t_{i} results in the expression sexp_{2}. Now, applying the part of the current proposition which has already been completed (that is the case where sexp_{1} is a variable), proves that I_{G}(V_{i}) ⊇ I_{G}(t_{i}). Hence the substitution proposition may be applied to sexp_{1} and sexp_{2} to prove that I_{G}(sexp_{1}) ⊇ I_{G}(sexp_{2}), and so the entire proof is complete.

4 Reduced Form Set Constraints

A conjunction C of set constraints is in reduced form if each constraint is of the form X ⊇ sexp where X is a variable and sexp is a set expression. Reduced form constraints always have at least one model since the interpretation which maps each variable into HU is trivially a model of any constraint of the form X ⊇ sexp. In fact they always have a least model (we delay the proof of this until proposition 13, where we prove the more general property that a collection of definite constraints has a least model whenever it has a model). The problem at hand is: find an explicit representation of the least model of a reduced form conjunction^{6} C, hereafter denoted lm_{C}, or simply lm_{C}.

In case C does not contain any intersection or projection symbols, then C itself is an explicit representation of lm_{C}. In case C does not contain any intersection symbols (but may contain projection symbols), early work by Reynolds [9], and later by Jones and Muchnick [5], gave algorithms for the explicit representation of lm_{C}. The representations used in these papers are equivalent to term grammars. If, on the other hand, C does not contain any projection symbols (but may contain intersection), then a simplification algorithm contained in [4] solves the problem for lm_{C}. Once again, the explicit representation used there is the same as a term grammar.

However, these results cannot be combined to deal with the case where C may contain both kinds of symbols because of the interaction between intersection and projection. The main contribution of this section is an algorithm to deal with this combination.

The section consists of two parts. The first part involves constructing a set expression grammar which defines lm_{C}. The second part (and the bulk of the section) then deals with the problem of converting this set expression grammar into an equivalent term grammar.

We begin by transforming C into grammar form; this form is defined as a conjunction, each of whose constraints is of the form X ⊇ sexp, where sexp does not contain the union symbol. This is achieved by the algorithm in figure 1. The conjunction C obtained by this algorithm has essentially the same model as the original conjunction. Specifically:

Proposition 6 Let C be an reduced form conjunction of set constraints input to the grammar form algorithm. Then the algorithm terminates and outputs a grammar form conjunction C′ such that lm_{C′}(U) = lm_{C}(U) for all U ∈ var(C).

Proof: We show that each iteration of the while statement preserves the least model of C. Consider a single iteration and let X ⊇ sexp be the constraint replaced during this iteration, let sexp′ be the result of replacing the occurrence of s ∪ t in sexp by Z, and let C_{u} be the constraints in C which are unchanged by this iteration. That is:

6We remark that the least model problem for the class of reduced form conjunctions is equivalent to the least model problem for the class of solved form conjunctions. A solved form conjunction of constraints has the form X_{1} = sexp_{1} ∧ ⋯ ∧ X_{n} = sexp_{n}, where the X_{i} are distinct variables and the sexp_{i} are set expressions.

input C;

while C contains a union symbol do

choose an ocurrence of an expression

of the form s ∪ t in C; replace this occurrence by a new variable, Z; add the constraints Z ⊇ s and Z ⊇ t;

endwhile output C;

Figure 1: Grammar Form Algorithm

C before iteration is: C_{u} ∧ X ⊇ sexp
C after iteration is: C_{u} ∧ X ⊇ sexp′ ∧ Z ⊇ s ∧ Z ⊇ t

It is sufficient to prove that

C_{u} ∧ X ⊇ sexp ⟺_{V} C_{u} ∧ X ⊇ sexp′ ∧ Z ⊇ s ∧ Z ⊇ t (4.1)

where V = var(C_{u}, X, sexp). Let I be a model of the l.h.s. of (4.1). Define I′ to be the same as I except that on the new variable Z,

I′(Z) =^{def} I(s ∪ t).

Since I′(s ∪ t) = I(s ∪ t), it is immediate that I′(s ∪ t) = I′(Z), and so by the substitution proposition, I′(sexp) = I′(sexp′). Now I′ is also a model of X ⊇ sexp since Z does not appear in this constraint. Hence I′(X) ⊇ I′(sexp) = I′(sexp′), which proves that I′ is a model of the r.h.s. of (4.1).

To prove the converse, let I be a model of r.h.s. of (4.1). This implies that I(Z) ⊇ I(s ∪ t), and this implies, by the substitution proposition, that I(sexp′) ⊇ I(sexp). Combining this with the fact that I is a model of X ⊇ sexp′ proves that I(X) ⊇ I(sexp′) ⊇ I(sexp), and so I is also a model of the l.h.s. of (4.1).

The essential benefit of a conjunction C being in grammar form is that we can construct a grammar which represents the least model of C by replacing ⊇ by ⟹. Specifically, define that a grammar G and a conjunction C correspond if

X ⟹ sexp appears in C iff X ⊇ sexp appears in G Proposition 7 Let G be a set expression grammar and let G be a grammar form conjunction of set constraints. If C and G correspond then I_{G} = lm_{C}.

Proof: We first prove that I_{G} models C. Let X ⊇ sexp be an arbitrary constraint in C. Then X ⟹ sexp is a rule in G and so X ⟹^{⋆} sexp. This implies, by proposition 5, that I_{G}(X) ⊇ I_{G}(sexp). Hence I_{G} is a model of each constraint in C.

We now prove that I_{G} is the least model of C. Let I be any model of C. We show that for any ground set expression t,

X ⟹^{⋆} t implies I(X) ⊇ I(t) (4.2)

by using induction on the length of the derivation X ⟹^{⋆} t. If the derivation is of length 1, then X ⟹ t is a rule in G. Hence X ⊇ t is a constraint in C, and so I(X) ⊇ I(t) because I is a model of C. This proves the base case.

Suppose now that the derivation X ⟹^{⋆} t is of the form X ⟹ sexp_{1} ⟹ … ⟹ sexp_{k−1} ⟹ t and that the property (4.2) holds for all derivations of length less than k. Let X_{1},…, X_{n} denote the occurrences of variables in sexp_{1}, and let X_{1} ⟹^{⋆} t_{1}, …, X_{n} ⟹^{⋆} t_{n} be the respective subderivations for these variables in the derivation sexp_{1} ⟹^{⋆} sexp_{k}. This means that if each variable occurrence X_{i} in sexp_{1} is replaced by the expression t_{i}, 1 ≤ i ≤ n, then the result is t. Now each expression t_{i} is ground since sexp is a ground expression. Also the derivations X_{i} ⟹^{⋆} t_{i} are all of length less than k. Hence, by the induction hypothesis, I(X_{i}) ⊇ I(t_{i}). This implies, by repeated application of the substitution proposition, that I(sexp_{1}) ⊇ I(t). Combining this with the fact that X ⟹ sexp_{1} is a rule in G, and hence I is a model of X ⊇ sexp_{1}, proves that I(X) ⊇ I(sexp_{1}) ⊇ I(t). This completes the induction argument, and proves property (4.2).

To complete the proof that I_{G} is the least model of C, we now use property (4.2) to show that I ⊇ I_{G}. Since I_{G}(X) is defined as the union of the sets [[t]] where t is a ground expression derivable from X, it is sufficient to show the following: for all ground t

X ⟹^{⋆} t implies I(X) ⊇ [[t]]

This follows immediately from property (4.2), since for any ground expression t, I(t) = [[t]].

From the correctness of the algorithm above (proposition 2) and proposition 7, we have

Lemma 1 Let C be in reduced form. Then a set expression grammar G can be constructed such that I_{G}(X) = lm_{C}(X) for all X ∈ var(C).

We now deal with the problem of converting a set expression grammar into an equivalent term grammar. We first apply the preprocessing algorithm described in figure 2 to remove nested occurrences of intersection and projection symbols. The required property of this algorithm is:

Proposition 8 Let G be a set expression grammar input to the grammar preprocessing algorithm. Then the algorithm terminates and outputs a set expression grammar G′, whose nested expressions are all atomic, which is equivalent to G in the sense that

for all X ∈ var(G), I_{G}(X) = I_{G′}(X).

Proof: The grammar preprocessing algorithm clearly terminates because each iteration of the while loop reduces the total number of nested intersection and projection symbols. Furthermore, on termination, all nested occurrences of intersection or projection symbols have been removed.

The correctness of the algorithm is proved by showing that each replacement step of the algorithm (which corresponds to one step of the while loop) preserves the meaning of the grammar in the following sense: if G_{1} and G_{2} respectively denote the grammar just before and just after an iteration, and if X is a variable in var(G_{1}), then, for all ground set expressions t,

X =G_{1}⇒⋆ t iff X =G_{2}⇒⋆ t. (4.3)

To prove this statement, let Y ⟹ sexp be the rule which contains the occurrence of s replaced during this iteration of the while loop, and let sexp′ be the result of replacing this occurrence of s in sexp by Z. Then, the only difference between G_{1} and G_{2} is that the rule Y ⟹ sexp is replaced by the two rules Y ⟹ sexp′ and Z ⟹ s. The proof that the l.h.s. of (4.3) implies the r.h.s. is easy, since any application of the rule Y ⟹ sexp in a derivation X =G_{1}⇒⋆ t can be replaced by successive applications of Y ⟹ sexp′ and Z ⟹ s to obtain a derivation X =G_{2}⇒⋆ t.

To prove the converse, note that if X =G_{2}⇒⋆ t, then (i) any application of the rule Z ⟹ s replaces an occurrence of the variable Z and such an occurrence can

input G;

while G contains a nested intersection or projection symbol do

choose a nested ocurrence of an expression s

of the form t_{1} ∩ t_{2} or f_{(i)}^{−1}(t) in G; replace this occurrence by a new variable, Z; add the rule Z ⟹ s;

endwhile output G;

Figure 2: Grammar Preprocessing Algorithm

only be introduced by an earlier application of the rule Y ⟹ sexp′, and (ii) any application of the rule Y ⟹ sexp′ introduces an occurrence of the variable Z, and since t is ground, this occurrence must be removed by a subsequent applications of the rule Z ⟹ s. Hence applications of the rules Y ⟹ sexp′ and Z ⟹ s must occur in pairs in such a way that an occurrence of the first introduces an occurrence of the variable Z which is removed by a subsequent application of the second. It follows that any derivation X =G_{2}⇒⋆ t can be reorganized so that each application of Y ⟹ sexp′ is followed immediately by the matching application of Z ⟹ s, and so these pairs can be replaced by a single application of Y ⟹ sexp. Repeated application of such a replacement step yields a derivation X =G_{1}⇒⋆ t.

We now describe the main algorithm of this section. This algorithm converts a set expression grammar, whose nested expressions are atomic, into a term grammar. The algorithm is essentially based on an exhaustive application of a series of transformations. Each transformation is simple; the main difficulty is termination. Let G be a set expression grammar in which all nested expressions are atomic. The first transformation serves to implement an obvious notion of substitution.

Transformation 1 (Substitute) If G contains a rule X ⟹ sexp such that

• sexp contains an occurrence of a variable Y and this occurrence is not within the scope of a function symbol (but it may occur inside the scope of a projection or union symbol), and

• Y ⟹ f(s_{1}, ⋯, s_{n}) is a rule in G and f ∈ Σ is n-ary, n ≥ 0, then let sexp′ be the result of replacing the occurrence of Y in sexp by f(s_{1}, ⋯, s_{n}) and add the rule X ⟹ sexp′ to G.

The next transformation deals with the elimination of projection symbols. In condition (b) below, we assume that there exists a recursive function ORACLE(G, s) which returns true if and only if s ⟹^{⋆} t for some ground atomic set expression such that [[t]] ≠ ◯̸. We provide an implementation of ORACLE later.

Transformation 2 (Projection-Elimination) If G contains a rule X ⟹ sexp such that

(a) sexp contains an expression of the form f_{(i)}^{−1}(f(s_{1},…, s_{n})), where f ∈ Σ is n-ary, 1 ≤ i ≤ n, and

(b) ORACLE(G, f(s_{1},…, s_{n})), then let sexp′ be the result of replacing the occurrence of f_{(i)}^{−1}(f(s_{1},…, s_{n})) in sexp by s_{i} and add the rule X ⟹ sexp′ to G.

The next transformation deals with eliminating intersection symbols. We note that given two term grammars, we can construct a third grammar whose language is the intersection of the first two [10] [2]. We cannot, however, use this result to eliminate occurrences of the intersection symbol and reduce a set expression grammar into a term grammar. This is because a grammar which has intersection symbols within its rules cannot, in general, be broken into intersection-free parts whose languages combine to equal the original language. Hence:

Transformation 3 (∩-distribution) If G contains a rule X ⟹ sexp such that sexp contains an occurrence of an expression of the form f(s_{1}, ⋯, s_{n}) ∩ f(t_{1}, ⋯, t_{n}) then let sexp′ denote the result of replacing this occurrence in sexp by f(Z_{1},…, Z_{n}), where Z_{1},…, Z_{n} are new variables, and add the following rules to G:

• X ⟹ sexp′, and

• Z_{i} ⟹ s_{i} ∩ t_{i}, 1 ≤ i ≤ n.

The final transformation deals with ⊤ symbol. It is essentially describes special cases of the above transformations for expressions such as sexp ∩ ⊤ and f_{(i)}^{−1}(⊤).

Transformation 4 (⊤-distribution) If G contains a rule X ⟹ sexp such that sexp contains an expression of the form s ∩ ⊤ or f_{(i)}^{−1}(⊤), then let sexp′ denote the result of replacing this occurrence in sexp by s or ⊤ respectively, and add the rule X ⟹ sexp′ to G.

Let G → G′ denote that the grammar G′ is obtained from the grammar G by a single application of one of transformations 1-4. We now prove that transformations 1-4 preserve the meaning of a grammar in the following sense:

Proposition 9 (Correctness of a Single Transformation) If G → G′ then

I_{G′}(X) = I_{G}(X) for all X ∈ var(G).

Proof: We first prove the following substitution property for set expression grammars.

[Grammar Substitution Property]: Let X ⟹ sexp be a rule in a set expression grammar G, let t be a subexpression of sexp and let sexp′ be the result of replacing an occurrence of t in sexp by t′. Then I_{G}(t′) ⊆ I_{G}(t) implies I_{G∪{X⟹sexp′}} = I_{G}.

To prove this property, let C be the grammar form constraints corresponding to G. By proposition 7, lm_{C} = I_{G}. Since X ⊇ sexp is a constraint in C and I_{G} is a model of C, I_{G}(X) ⊇ I_{G}(sexp). Also, by the substitution property, I_{G}(sexp) ⊇ I_{G}(sexp′). Hence I_{G} satisfies X ⊇ sexp′. Combining this with proposition 7 gives the following chain of equalities, and this proves the grammar substitution property.

I_{G∪{X⊇sexp′}} = lm (C ∪ {X ⊇ sexp′}) = lm (C) = I_{G}.

The proposition can now be proved by four applications of the grammar substitution property, one for each of the possible transformations. Suppose that transformation 1 (substitution) is applied. Since Y ⟹ f(s_{1}, ⋯, s_{n}) is a rule in G, I_{G}(Y) ⊇ I_{G}(f(s_{1}, ⋯, s_{n})) by proposition 7. Recalling that sexp′ is obtained from sexp by replacing an occurrence of Y by f(s_{1}, ⋯, s_{n}), we have, on applying the above grammar substitution property, that

I_{G∪{X⟹sexp′}} = I_{G},

and this proves the proposition for the case of the substitution transformation.

Suppose that the transformation applied is transformation 2 (projection elimination). Since ORACLE(G, f(s_{1},…, s_{n})), it follows that I_{G}(f(s_{1}, ⋯, s_{n})) ≠ ◯̸, and so

I_{G}(f_{(i)}^{−1}(f(s_{1}, ⋯, s_{n}))) = I_{G}(s_{i})

The grammar substitution property can now be applied to complete the proof for this case.

Suppose that the transformation applied is transformation 3 (∩-distribution). Let G′ denote the grammar G ∪ {Z_{i} ⟹ s_{i} ∩ t_{i} : 1 ≤ i ≤ n}. It is clear that

I_{G′}(X) = I_{G}(X), X ∈ var(G)

since G′ is obtained from G by adding rules for the variables Z_{1},…, Z_{n}, and these variables do not appear in G. To complete the proof for this transformation, we now show that I_{G′} = I_{G′∪{X⟹sexp′}}. First, note that the only rule for each variable Z_{i} is Z_{i} ⟹ s_{i} ∩t_{i}. Hence if f(Z_{1},…, Z_{n}) =G′⇒⋆ sexp where sexp is some ground expression, then by rearranging this derivation so that the rules replacing the variables Z_{i} are used first, it is clear that there is a derivation f(s_{1} ∩t_{1},…, s_{n} ∩t_{n}) =G′⇒⋆ sexp. It follows, using proposition 4, that

I_{G′}(f(Z_{1},…, Z_{n})) ⊆ I_{G′}(f(s_{1} ∩ t_{1},…, s_{n} ∩ t_{n})).

Combining this with the easily verifiable distributivity property of ∩ over f, we have

I_{G′}(f(Z_{1},…, Z_{n})) ⊆ I_{G′}(f(s_{1} ∩ t_{1},…, s_{n} ∩ t_{n})) = I_{G′}(f(s_{1},…, s_{n}) ∩ f(t_{1},…, t_{n})).

Again the grammar substitution property can be applied to complete the proof for this case.

Finally, suppose that the transformation applied is transformation 4. Now, for any interpretation I, I(s ∩ ⊤) = I(s) and I(f_{(i)}^{−1}(⊤)) = I(⊤). Hence the correctness for this transformation follows easily from the grammar substitution property.

The main algorithm for this section can now be presented in figure 3. This algorithm is essentially an exhaustive application of transformations 1 - 4, with three modifications. The first involves the removal of duplicate expressions before adding a rule to G. Specifically, any rule can be written in the form X ⟹ t_{1} ∩…∩t_{n}, where t_{1},…, t_{n} do not contain the ∩ symbol. The removal of duplicate expressions can then be defined by the rule: delete all t_{i} such that there is a t_{j}, j < i, and t_{i} = t_{j}.

The second modification involves restricting the use of transformations which do not add new rules. Specifically, define that a transformation is applicable to G if the pre-conditions of the transformation are satisfied and the transformation adds some new rules^{7} to G. Also, define that G is closed under a transformation τ if the transformation τ is not applicable to G. The restricted use of transformations can now be characterized as: a transformation is only used when it is applicable.

The third modification involves carefully controlling the new variables added by the ∩-distribution transformation so that only a finite number of these variables need to be introduced. The essential idea behind this mechanism is a special naming scheme: each introduced variable is of the form V_{{t_{1},···,t_{n}}} where t_{1}, ⋯, t_{n} are atomic expressions appearing in G at the start of the algorithm. The intention here is that such a variable is equivalent to the expression t_{1} ∩ ⋯ ∩ t_{n}. Thus a variable such as V_{{f(X),Y,f(Z)}} not only represents f(X) ∩ Y ∩ f(Z), but also expressions such as V_{{f(X),Y }} ∩ f(Z) and V_{{f(X),f(Z)}} ∩ V_{{f(X),Y }}. To facilitate the use of this naming scheme, let N denote the mapping from an expression (including a variable of the form V_{T}) to the set of atomic expressions it represents^{8}:

N (t) = \{ \begin{matrix}T & if t is V_{T}; \\ N (t_{1}) ∪ N (t_{2}) & if t is t_{1} ∩ t_{2}; \\ \{t\} & otherwise. \end{matrix}

For example, N (V_{{f(X),f(Z)}}∩V_{{f(X),Y }}) = {f(X), Y, f(Z)}. Similarly N (V_{{f(X),Y }}∩ f(Z)) and N (f(X) ∩ Y ∩ f(Z)) are also equal to {f(X), Y, f(Z)}.

We now prove that the grammar simplification algorithm terminates and is correct in the sense that the grammar output by the algorithm is a term grammar which describes the least model of the input set expression grammar. In a number of the following arguments dealing with properties of rules added by transformations, we will, for notational convenience, ignore the fact that duplicate terms are deleted from the r.h.s. of a rule before it is added to G. It is straightforward, but tedious, to expand the proofs to deal with this issue, since the absence or presence of duplicate expressions in rules is of no consequence. One exception to this is the argument for termination, where the proof explicitly depends on the deletion of duplicate terms.

We start by establishing an important invariant of the algorithm. One main purpose of this invariant is to bound the number of new variables that are introduced during the algorithm.

Proposition 10 (Subexpression-Invariant) Let G_{0} be a set expression grammar in which all nested expressions are atomic and let G_{0} be input to the grammar

7This test is made after duplicate expressions have been removed from the potentially new rules.

8N is well defined since N ((t_{1} ∩ t_{2}) ∩ t_{3}) = N (t_{1}) ∪ N (t_{2}) ∪ N (t_{3}) = N (t_{1} ∩ (t_{2} ∩ t_{3})).

input G;

1. repeat

2. exhaustively-apply transformations 1, 2 and 4 to G;

3. if transformation 3 is applicable to G (that is, G contains a rule X ⟹ sexp such that sexp contains an occurrence of the expression f(s_{1}, ⋯, s_{n}) ∩ f(t_{1}, ⋯, t_{n}))

then

4. add X ⟹ sexp′ to G where sexp′ is obtained by replacing the occurrence of f(s_{1}, ⋯, s_{n}) ∩ f(t_{1}, ⋯, t_{n}) in sexp

by f(V_{N (t_{1})∪N (s_{1})}, ⋯, V_{N (t_{n})∪N (s_{n})});

5. for each i : 1 ≤ i ≤ n do

6. if V_{N (t_{i})∪N (s_{i})} is a new variable in G then

7. add V_{N (t_{i})∪N (s_{i})} ⟹ t_{i} ∩ s_{i} to G

endif endfor

endif until neither transformation 1, 2, 3 nor 4 is applicable to G; output the rules in G which do not contain intersection or projection symbols;

Figure 3: Grammar Simplification Algorithm simplification algorithm. Then, at all times during execution of the algorithm, all nested expressions sexp of G are atomic and are such that N (sexp) contains only atomic subexpressions of G_{0}.

Proof: We say that G satisfies the invariant if all nested subexpressions sexp of G are atomic and such that N (sexp) contains only subexpressions from G_{0}. The proposition can then be restated as: G satisfies the invariant at all times during execution of the algorithm.

Clearly G satisfies the invariant at the start of line 1 of the algorithm. Suppose now that the invariant holds at some stage during execution of the algorithm. Since each step of the algorithm is essentially an application of one of the transformations substitute, projection elimination, ∩-distribution or ⊤-distribution, it suffices to show that the rules added by a single application of one of these transformations satisfies the invariant, given that G satisfies the invariant. Let atomic(G_{0}) denote the atomic subexpressions of G_{0}, and consider the four cases.

Consider a single application of the substitution transformations. In this case the only rule added is X ⟹ sexp′ where sexp′ is the result of replacing an unnested occurrence of a variable by f(t_{1}, ⋯, t_{n}). Hence the only nested expressions in this rule which did not already appear in X ⟹ sexp are those that appear in f(t_{1}, ⋯, t_{n}). However f(t_{1}, ⋯, t_{n}) is obtained from the r.h.s. of some other rule in G. Hence any rule added by the substitution transformation also satisfies the invariant.

Consider a single application of the projection-elimination transformation. In this case the only rule added is X ⟹ sexp′ where sexp′ is the result of replacing an un-nested occurrence of the form f_{(i)}^{−1}(f(s_{1}, ⋯, s_{n})) in sexp by s_{i}. Hence no new nested expressions are introduced.

Consider a single application of the ∩-distribution transformation. We refer to the modified version of this transformation given in lines 4-7 of the algorithm. This transformation adds a new rule at line 4 and may also add new rules at line 7. Now the only nested expressions in a rule added at line 4 are of the form V_{N (t_{i})∪N (s_{i})} where s_{i} and t_{i} are nested expressions in G. Since G satisfies the invariant, s_{i} and t_{i} are both atomic expressions such that N (t_{i}) and N (s_{i}) are subsets of atomic(G_{0}). Hence N (V_{N (t_{i})∪N (s_{i})}) = N (t_{i}) ∪ N (s_{i}) ⊆ atomic(G_{0}), and so any rule added at line 4 must satisfy the invariant. Consider now a rule added at line 7. The only nested subexpressions of such a rule appear as nested subexpressions of s_{i} and t_{i}, and since s_{i} and t_{i} appear in G, this case is proved.

Consider a single application of the ⊤-distribution transformation. In this case the only rule added is X ⟹ sexp′ where sexp′ is the result of replacing an unnested expression of the form s ∩ ⊤ or f_{(i)}^{−1}(⊤) by s or ⊤ respectively. Hence no new nested expressions are added, and so any rule added by the ⊤-distribution transformation also satisfies the invariant.

We now justify the modified application of transformation 3 in the grammar simplification algorithm by proving the following invariant. In essence it establishes the correctness of the introduced variables V_{S} by showing that V_{N (s)∪N (t)} and s ∩ t are equivalent under I_{G}.

Proposition 11 Let the grammar simplification algorithm be input with a set expression grammar in which all nested expressions are atomic. Let G be the grammar obtained after any completed iteration^{9} of the repeat loop. If V_{T} is a variable in G and sexp is a set expression containing only variables from G such that T = N (sexp) then I_{G}(V_{T}) = I_{G}(sexp).

Proof: Let s be a set expression such that N (s) is {t_{1}, ⋯, t_{n}} where the t_{j} are distinct atomic expressions which appear in G. We prove that

I_{G}(s) = I_{G}(t_{1} ∩ ⋯ ∩ t_{n}). (4.4)

The proposition then follows by applying (4.4) twice, once with s = V_{T} and the other with s = sexp, noting that since V_{T} is a variable in G, T contains only atomic expressions which appear in G.

We now prove (4.4). Let G_{0}, G_{1}, ⋯, G_{l}, ⋯ denote the sequence of grammars produced by the algorithm such that G_{l} is the grammar produced after l iterations. Since G is G_{l} for some l, it suffices to show, for all iterations l, that if s is restricted to contain only variables from G_{l} then

I_{G_{l}}(s) = I_{G_{l}}(t_{1} ∩ ⋯ ∩ t_{n}). (4.5)

We proceed by induction. If l = 0 then s does not contain any variables of the form V_{T}. Clearly it can be written as s_{1} ∩ ⋯ ∩ s_{m} such that {s_{1}, ⋯, s_{m}} = {t_{1}, ⋯, t_{n}}. Suppose that d is an element of the l.h.s. of (4.5). Then d ∈ I_{G_{l}}(s_{i}) for all 1 ≤ i ≤ m. Since each s_{i} appears as some t_{j} and vice-versa, this implies that d ∈ I_{G_{l}}(t_{j}) for all 1 ≤ j ≤ n. Hence d ∈ I_{G_{l}}(t_{1} ∩ ⋯ ∩ t_{n}), the r.h.s. of (4.5). The converse proof, that any d in the r.h.s. of (4.5) is also in the l.h.s., is identical. This proves the base case.

9An iteration here refers to a complete execution of the body of the repeat loop (lines 2 – 7) of the grammar simplification algorithm.

Now consider the l^{th} iteration, and suppose that (4.5) holds for all iterations before the l^{th}. Again s can be written as s_{1} ∩ ⋯ ∩ s_{m} where the s_{i} are atomic. Now suppose that s contains a variable which does not appear in G_{l−1}. Such a variable must be a variable of the form V_{T}, and this variable must appear as one of the s_{i}, 1 ≤ i ≤ m. Moreover, this variable must have been introduced during the l^{th} iteration, and hence during this iteration a rule of the form V_{T} ⟹ u ∩ v is added such that T = N (u) ∪ N (v). This is the only rule for V_{T} in G_{l} and so I_{G_{l}}(V_{T}) = I_{G_{l}}(u ∩ v). Now, on setting

s′ = s_{1} ∩ s_{i−1} ∩ (u ∩ v) ∩ s_{i+1} ∩ ⋯ ∩ s_{m}

it is clear that N (s′) = N (s) and I_{G_{l}}(s′) = I_{G_{l}}(s). This step can be repeated to remove all of the variables which are introduced in the l^{th} iteration. The resulting expression, call it s′′ has the property that N (s′′) = N (s) and I_{G_{l}}(s′′) = I_{G_{l}}(s). Finally, since all variables in s′′ appear in G_{l−1}, the induction hypothesis can be applied to obtained

I_{G_{l}}(s) = I_{G_{l}}(s′′) = I_{G_{l}}(t_{1} ∩ ⋯ ∩ t_{n}),

The next proposition establishes a property used in the following lemma.

Proposition 12 (Exhaustive Application of Substitution) Let G be a set expression grammar which is closed under the substitution transformation, let X be a variable, and let sexp be a ground atomic set expression. If X ⟹^{⋆} sexp is the shortest derivation of a ground expression sexp from X, then the first rule used in this derivation is of the form X ⟹ sexp′ such that sexp′ is a non-variable atomic expression.

Proof: The proof is an easy induction on the length of the derivation X ⟹^{⋆} sexp. If the length is 0 or 1, then the result is immediate. Now suppose that the result holds for derivations of length n ≥ 1, and consider a derivation of length n + 1. This derivation is of the form:

X ⟹ sexp′ ⟹ sexp′′ ⟹^{⋆} sexp

where the derivation sexp′ ⟹^{⋆} sexp of length n and is the shortest derivation of sexp from sexp′. Suppose that sexp′ is a variable. Then by the induction hypothesis sexp′′ is a non-variable atomic set expression. Hence the pre-conditions of the substitution transformation are satisfied, and since G is closed under the substitution transformation, the rule X ⟹ sexp′′ must already appear in G. However this gives a shorter derivation of X ⟹^{⋆} sexp. Hence it must be the case that sexp′ is not a variable. Also, since sexp is atomic, sexp′ must be atomic.

The following lemma is a core part of the correctness of the grammar simplification algorithm. Each part of the lemma makes an incremental step towards part (d), which essentially says that at the end of the repeat loop of the algorithm, all information about the least model is contained in “explicit” derivations of the form X ⟹^{⋆} a such that a does not contain any projection or intersection symbols. This means that after the repeat loop, the “non-explicit” part of G can be simply deleted, and this is the effect of the final output step of the grammar simplification algorithm. The main difficulty in the proof involves the variables of the form V_{T}. The introduction of this variable scheme^{10} needed for termination reasons and its purpose was to provide a representation for expressions of the form s_{i} ∩ t_{i} introduced by the ∩-distribution transformation. However, given a derivation of the form

X ⟹ f(s) ∩ f(t) ⟹^{⋆} f(s′) ∩ f(t′)

we can argue that the ∩-distribution transformation adds a rule of the form X ⟹ f(V_{N (s)∪N (t)}), but we cannot argue that therefore there exists a derivation of the form X ⟹^{⋆} f(s′ ∩ t′), because in general there will not be a derivation V_{N (s)∪N (t)} ⟹^{⋆} s′ ∩ t′. Fortunately we can construct an “equivalent” derivation. Establishing an appropriate notion of equivalence is part of the following lemma.

Lemma 2 (Exhaustive Transformation Application) Let the algorithm be input with a set expression grammar in which all nested expressions are atomic. Then, if the repeat loop of the algorithm terminates, the following properties hold of the resulting grammar G:

(a) If t_{1}, ⋯, t_{n} is a sequence of atomic expressions appearing in G, sexp is an

expression such that N (sexp) = {t_{1}, ⋯, t_{n}}, and t_{i} ⟹^{⋆} t′_{i}, 1 ≤ i ≤ n

then there is a derivation sexp ⟹^{⋆} v_{1} ∩ ⋯ ∩ v_{m} such that {v_{1}, ⋯, v_{m}} = {t′_{1}, ⋯, t′_{n}}^{11}

(b) If sexp ⟹^{⋆} sexp′ where sexp′ is a ground expression not containing union or projection symbols and d ∈ [[sexp′]], then there is a derivation sexp ⟹^{⋆} t_{1} ∩ ⋯ ∩ t_{n} ⟹^{⋆} sexp′′ such that sexp′′ is a ground expression not containing union or projection symbols, d ∈ [[sexp′′]] and {t_{1}, ⋯, t_{n}} = N (sexp).

(c) For all variables X, if X ⟹^{⋆} sexp, sexp is a ground expression not containing projection symbols and d ∈ [[sexp]], then there exists a ground atomic set expression a such that X ⟹^{⋆} a and d ∈ [[a]].

10We remark that the variable scheme V_{T} is somewhat analogous to the powerset construction used to transform an NFA to a DFA.

11The sequences t_{1}, ⋯, t_{n} and t′_{1}, ⋯, t′_{n} and v_{1}, ⋯, v_{m} may have duplicate elements.

(d) For all variables X, if X ⟹^{⋆} sexp for some ground sexp such that d ∈ [[sexp]], then there exists a ground atomic set expression a such that d ∈ [[a]]

and X ⟹^{⋆} a.

Proof for part (a): Let V_{T} be a variable in G which is introduced by the algorithm during an application of the ∩-distribution transformation. When the variable is first introduced, a rule of the form V_{T} ⟹ s ∩ t is added to G such that T = N (s) ∪ N (t) (see line 7 of the grammar simplification algorithm). Let initial(V_{T}) denote this rule. Now, starting with the expression sexp, pick an occurrence of a variable of the form V_{T}, and replace this occurrence using the rule initial(V_{T}). Let sexp_{1} denote the result. Now repeat this process to obtain sexp_{2}, sexp_{3}, ⋯ Eventually this process must terminate since if a variable of the form V_{T′} appears in the r.h.s. of a rule initial(V_{T}), then the variable V_{T′} must have been introduced before V_{T}. Let the number of replacement steps used be k. It is easy to verify that these replacement steps replace only un-nested variables, since no nested occurrences of variables of the form V_{T} can be introduced. Also, each rule used is of the form V ⟹ s∩t such that N (V) = N (s∩t). It follows that N (sexp) = N (sexp_{1}) = N (sexp_{2}) = ⋯ = N (sexp_{k}). Finally, write sexp_{k} as u_{1} ∩ ⋯ ∩ u_{m} where the u_{i} are atomic. Then since sexp_{k} does not contain any variables of the form V_{S}, N (sexp_{k}) = {u_{1}, ⋯, u_{m}}. Hence, this yields a derivation

sexp ⟹^{⋆} u_{1} ∩ ⋯ ∩ u_{m}

such that {u_{1}, ⋯, u_{m}} = {t_{1}, ⋯, t_{n}}. Hence, u_{1} ∩ ⋯ ∩ u_{m} can be written as t_{i_{1}} ∩ ⋯ ∩ t_{i_{m}}, where each i_{j} is such that 1 ≤ i_{j} ≤ n, and each t_{i} appears in

t_{i_{1}} ∩ ⋯ ∩ t_{i_{m}}. Hence t_{i_{1}} ∩ ⋯ ∩ t_{i_{m}} ⟹^{⋆} t′_{i_{1}} ∩ ⋯ ∩ t′_{i_{m}}. Since {t′_{i_{1}}, ⋯, t′_{i_{m}}} =

{t′_{1}, ⋯, t′_{n}}, part (a) is proved.

Proof for part (b): Since sexp is assumed not to contain union or projection symbols, it can be written as s_{1} ∩ ⋯ ∩ s_{m} where each s_{i} is an atomic expression. Then there exist s′_{i} such that s_{i} ⟹^{⋆} s′_{i} and sexp′ is s′_{1} ∩ ⋯ ∩ s′_{m}. The remainder of the proof involves showing constructing, for each 1 ≤ i ≤ m, a derivation s_{i} ⟹^{⋆} t_{i,1} ∩ ⋯ ∩ t_{i,n_{i}} ⟹^{⋆} s′′_{i} such that s′′_{i} does not contain any projection or union symbols, d ∈ [[s′′_{i}]] and {t_{i,1}, ⋯, t_{i,n_{i}}} = N (s_{i}). Part (b) then follows immediately by composing these derivations.

To construct these derivations, first note that if s_{i} is not a variable of the form V_{T}, then the derivation s_{i} ⟹^{⋆} s′_{i} will do, since N (s_{i}) = {s_{i}}. It is therefore sufficient to prove the following for each variable of the form V_{T} appearing in G:

\begin{matrix}If V_{T} ⟹^{⋆} s such that s does not contain the projection \\ symbol and d ∈ [[s]] then there exists a derivation \\ V_{T} ⟹^{⋆} t_{1} ∩ ⋯ ∩ t_{n} ⟹^{⋆} s′ such that s′ does not contain \\ any projection symbols, d ∈ [[s′]] and \{t_{1}, ⋯, t_{n}\} = T. \end{matrix} (4.6)

To prove this property let G_{0}, G_{1}, ⋯, G_{i}, ⋯, G_{N} denote the sequence of grammars obtained after each \underline{transformation} application; that is, G_{0} is the input grammar, G_{i} is the grammar obtained after i transformation applications, and G_{N} is the resultant grammar G at the end of the repeat loop, where N is the total number of transformation applications. Now, each variable of the form V_{T} can be identified with the transformation application which introduced this variable. Write η(V_{T}) = n to denote that the variable V_{T} is introduced by the n^{th} transformation application. Clearly the only rule for V_{T} in G_{η(V_{T})} is of the form V_{T} ⟹ u_{1}∩u_{2} such that u_{1} and u_{2} are atomic expression and T = N (u_{1}) ∪ N (u_{2}). Hence there are no subexpressions of the form f_{(j)}^{−1}(w) in this rule, and so transformations dealing with projection (specifically, the projection elimination transformation and the part of the ⊤-distribution transformation dealing with expressions of the form f_{(j)}^{−1}(⊤)) cannot be applied to such a rule. Also, any transformation application to a rule of this form yields a rule of the form V_{T} ⟹ sexp where sexp is an atomic expression, or sexp is of the form a ∩ a′, for some atomic expressions a and a′. By repeatedly applying these observations, it is easy to verify that, for i ≥ η(V_{T}), all transformations in G_{i} for V_{T} are of the form V_{T} ⟹ sexp where sexp is either an atomic expression, or of the form a ∩ a′ for some atomic expression a and a′ which appear in G_{i−1}. Therefore, if V_{T} ⟹ sexp is a rule in G_{i} for some i, then either

(i) sexp is of the form u_{1} ∩ u_{2} where T = N (u_{1}) ∪ N (u_{2}) and u_{1} and u_{2} are expressions which appear in G_{i−1}, or

(ii) there exists a rule V_{T} ⟹ sexp′ in G_{j} for some j < i such that V_{T} ⟹ sexp is obtained from V_{T} ⟹ sexp′ by an application of the ∩-distribution transformation, or

(iii) there exists a rule V_{T} ⟹ sexp′ in G_{j} for some j < i such that V_{T} ⟹ sexp is obtained from V_{T} ⟹ sexp′ by an application of the ⊤-distribution transformation, or

(iv) there exist rules V_{T} ⟹ sexp′ and X ⟹ t in G_{j} for some j < i such that V_{T} ⟹ sexp is obtained from V_{T} ⟹ sexp′ and X ⟹ t by an application of the substitution transformation.

We now use this case analysis to prove the property (4.6). The argument is essentially an induction argument on V_{T} ⟹^{⋆} s.

Where d ∈ HU , V_{T} is a variable appearing in G and s is a ground expression, let ∇(d, V_{T} ⟹^{⋆} s) be (α, β, γ) such that α is the number of symbols in d, β is η(V_{T}) and γ is the smallest integer such that the first rule in the derivation V_{T} ⟹^{⋆} s appears in G_{γ}. We proceed by induction on ∇. The base case, where α = 0 or β = 0 or γ is 0, is vacuous since there are no terms with 0 symbols and no variables in G_{0} of the form V_{T}. Now consider ∇(d, V_{T} ⟹^{⋆} s) = (α, β, γ) such that (4.6) holds for (α′, β′, γ′) if either α′ < α or α′ = α and β′ < β, or α′ = α and β′ = β and

γ′ < γ. Write V_{T} ⟹^{⋆} s as

V_{T} ⟹ sexp ⟹^{⋆} s

and consider the cases as outlined above. In case (i), sexp is of the form u_{1} ∩ u_{2} where T = N (u_{1}) ∪ N (u_{2}), u_{i} appears in G_{α−1}, i = 1, 2, and there exists u′_{i}, i = 1, 2 such that u_{i} ⟹^{⋆} u′_{i}, d ∈ [[u′_{i}]] and u′_{1} ∩ u′_{2} is s. If u_{i} is of the form V_{S} then since it appears in G_{α−1}, the induction hypothesis can be applied to obtain u_{i} ⟹^{⋆} t_{1} ∩ ⋯ ∩ t_{n} ⟹^{⋆} u′′_{i} where u′′_{i} does not contain any projection symbols, d ∈ [[u′′_{i}]], and {t_{1}, ⋯, t_{n}} is N (u_{i}). On the other hand, if u_{i} is not of the form V_{S}, then N (u_{i}) = {u_{i}}. Hence in either case there exists a derivation u_{i} ⟹^{⋆} t_{i,1} ∩ ⋯ ∩ t_{i,n_{i}} ⟹^{⋆} u′′_{i} such that u′′_{i} does not contain any projection symbols, d ∈ [[u′′_{i}]] and {t_{i,1}, ⋯, t_{i,n_{i}}} is N (u_{i}). Combining these facts proves first that

V_{T} ⟹ u_{1} ∩ u_{2} ⟹^{⋆} t_{1,1}, ⋯, t_{1,n_{1}} ∩ t_{2,1}, ⋯, t_{2,n_{2}} ⟹^{⋆} u′′_{1} ∩ u′′_{2}.

Second u′′_{1} ∩ u′′_{2} does not contain any projections symbols. Third d ∈ [[u′′_{1} ∩ u′′_{2}]]. Finally, T = N (u_{1}) ∪ N (s_{2}) = {t_{1,1}, ⋯, t_{1,n_{1}}, t_{2,1}, ⋯, t_{2,n_{2}}}. This proves (4.6) in case (i).

In case (ii), sexp is of the form f(V_{N (v_{1})∩N (w_{1})}, ⋯, V_{N (v_{k})∩N (w_{k})}) and G contains a rule of the form V_{T} ⟹^{⋆} f(v_{1}, ⋯, v_{k}) ∩ f(w_{1}, ⋯, w_{k}). Also, there exist ground u_{i} which do not contain any projection symbols, such that V_{N (v_{i})∩N (w_{i})} ⟹^{⋆} u_{i}, 1 ≤ i ≤ k, and s is f(u_{1}, ⋯, u_{k}). Now, since d ∈ [[f(u_{1}, ⋯, u_{k})]], d is of the form f(d_{1}, ⋯, d_{k}) and d_{i} ∈ [[u_{i}]], 1 ≤ i ≤ k. Hence the induction hypothesis can be applied, and so, for 1 ≤ i ≤ k, there exists a derivation V_{N (v_{i})∩N (w_{i})} ⟹^{⋆} t_{i,1} ∩ ⋯ ∩ t_{i,n_{i}} ⟹^{⋆} s′_{i} such that the s′_{i} are ground expressions not containing projection symbols, d ∈ [[s′_{i}]] and {t_{i,1}, ⋯, t_{i,n_{i}}} = N (v_{i}) ∩ N (w_{i}). Further, each

s′_{i} can be written as s_{i,1}, ⋯, s_{i,n_{i}} such that t_{i,j} ⟹^{⋆} s_{i,j}, 1 ≤ j ≤ n_{i}. Now, for

1 ≤ i ≤ k, N (v_{i}) and N (w_{i}) are both subsets of {t_{i,1}, ⋯, t_{i,n_{i}}}. Hence by part (a), there exist derivations

v_{i} ⟹^{⋆} v′_{i} such that d_{i} ∈ [[v′_{i}]] , 1 ≤ i ≤ k,

w_{i} ⟹^{⋆} w′_{i} such that d_{i} ∈ [[w′_{i}]] , 1 ≤ i ≤ k,

such that the v′_{i} and w′_{i} do not contain any projection symbols. Hence there is a derivation

V_{T} ⟹ f(v_{1}, ⋯, v_{k}) ∩ f(w_{1}, ⋯, w_{k}) ⟹^{⋆} f(v′_{1}, ⋯, v′_{k}) ∩ f(w′_{1}, ⋯, w′_{k})

where f(v′_{1}, ⋯, v′_{k}) ∩ f(w′_{1}, ⋯, w′_{k}) is a ground expression which does not contain any projection symbols such that f(d_{1}, ⋯, d_{k}) ∈ [[f(v′_{1}, ⋯, v′_{k}) ∩ f(w′_{1}, ⋯, w′_{k})]]. Since T = {f(v_{1}, ⋯, v_{k}), f(w_{1}, ⋯, w_{k})}, the proof for case (ii) is complete.

In case (iii), there is a rule of the form V_{T} ⟹ ⊤ ∩ sexp or V_{T} ⟹ sexp ∩ ⊤ in G_{α−1}. Now, since V_{T} ⟹ sexp ⟹^{⋆} s, either the derivation V_{T} ⟹ sexp ∩ ⊤ ⟹^{⋆} s ∩ ⊤ or V_{T} ⟹ ⊤ ∩ sexp ⟹^{⋆} ⊤ ∩ s can be constructed. In either case, d is an element of [[⊤ ∩ sexp]] and [[sexp ∩ ⊤]]. Now the first rule used in these derivations appears in G_{α−1}, and hence the induction hypothesis can be applied to prove this case.

In case (iv), there are rules V_{T} ⟹ u and X ⟹ v in G_{α−1} such that the result of replacing an occurrence of X in u by v is sexp. Now since V_{T} ⟹ sexp ⟹^{⋆} s, the derivation V_{T} ⟹ u ⟹ sexp ⟹^{⋆} s can be constructed, where the first rule used is V_{T} ⟹ u and the second is X ⟹ v. Now these rule both appear in G_{α−1}, and hence the induction hypothesis can be again be applied to prove this case.

Proof for part (c): Where d ∈ HU , X is a variable and sexp is a ground expression define ∇(d, X, sexp) to be (α, β) such that α is the number of symbols in d and β is the length of the derivation X ⟹^{⋆} sexp. We proceed by induction on ∇. The base case, where α = 0 or β = 0, is vacuous since there are no terms with 0 symbols and no derivations of sexp from X of 0 length because sexp is ground expression and X is a variable. Now consider ∇(d, X, sexp) = (α, β) such that part (c) holds for (α′, β′) if either α′ < α or α′ = α and β′ < β. Let X ⟹^{⋆} sexp be a minimal length derivation of sexp from X, and write this derivation as

X ⟹ s_{1} ∩ ⋯ ∩ s_{n} ⟹^{⋆} sexp

where the s_{i}, 1 ≤ i ≤ n are atomic expressions. Then there exist t_{i}, 1 ≤ i ≤ n,

such that s_{i} ⟹^{⋆} t_{i} and sexp is t_{1} ∩ ⋯ ∩ t_{n}. Since d ∈ [[sexp]], d ∈ [[t_{i}]], 1 ≤ i ≤ n.

Suppose that one of the s_{i} is a variable. Since s_{i} ⟹^{⋆} t_{i} is a shorter derivation than the derivation X ⟹^{⋆} sexp then the induction hypothesis may be applied (using the fixed d) to obtain an atomic a_{i} such that s_{i} ⟹^{⋆} a_{i} and d ∈ [[a_{i}]]. Pick the shortest such derivation of a_{i} from s_{i}. By proposition 12, this derivation must be of the form s_{i} ⟹ s′_{i} ⟹^{⋆} a_{i} where s′_{i} is a non-variable atomic expression (i.e. of the form f(⋯), f ∈ Σ). Hence a derivation of the following form can be constructed:

X ⟹ s′_{1} ∩ ⋯ ∩ s′_{m} ⟹^{⋆} sexp′ (4.7)

where d ∈ [[sexp′]] and each s′_{i}, 1 ≤ i ≤ m is a non-variable atomic expression. Let d be f(d_{1}, ⋯, d_{k}). This means that the top-most symbol of each s′_{i} must either be f or ⊤. Now, suppose that for some of the s′_{i} are ⊤. Then the ⊤-distribution transformation can be used repeatedly to yield a rule

X ⟹ s′_{i_{1}} ∩ ⋯ ∩ s′_{i_{m}}, 1 ≤ i_{1} < i_{2} < ⋯ < i_{m} ≤ n

Since G is closed under the ⊤-distribution transformation, this rule must already be present. Using this rule, a new derivation of the form (4.7) can be constructed where each s′_{i}, is a non-variable atomic expression, 1 ≤ i ≤ m. Therefore, each of the s′_{i} must be of the form f(⋯). Hence s′_{1} ∩ ⋯ ∩ s′_{n} can be written in the form f(u_{1,1}, ⋯, u_{k,1}) ∩ ⋯ ∩ f(u_{m,1}, ⋯, u_{m,k}) for some u_{i,j}, 1 ≤ i ≤ k, 1 ≤ j ≤ m. In particular, the repeated application of the the ∩-distribution transformation yields the following rule:

X ⟹ f(V_{T_{1}}, ⋯, V_{T_{k}})

where T_{i} = N (u_{i,1}) ∪ ⋯ ∪ N (u_{i,k}), 1 ≤ i ≤ k. Now, since sexp′ is derivable from f(u_{1,1}, ⋯, u_{k,1}) ∩ ⋯ ∩ f(u_{m,1}, ⋯, u_{m,k}) it must be the case that there exist v_{i,j} such that 1 ≤ i ≤ m and 1 ≤ j ≤ k such that

• sexp′ is of the form f(v_{1,1}, ⋯, v_{k,1}) ∩ ⋯ ∩ f(v_{m,1}, ⋯, v_{m,k})

• u_{i,j} ⟹^{⋆} v_{i,j}, 1 ≤ i ≤ m, 1 ≤ j ≤ k

• d_{i} ∈ [[v_{i,j}]], 1 ≤ i ≤ m, 1 ≤ j ≤ k

Now, fix i, 1 ≤ i ≤ k. Clearly u_{i,1} ∩ ⋯ ∩ u_{i,m} ⟹^{⋆} v_{i,1} ∩ ⋯ ∩ v_{i,m}. Hence by (b)

there exists a derivation of the form

u_{i,1} ∩ ⋯ ∩ u_{i,m} ⟹^{⋆} t_{1} ∩ ⋯ ∩ t_{l} ⟹^{⋆} sexp′′

for some t_{j}, 1 ≤ j ≤ l, such that d_{i} ∈ [[sexp′′]], N (u_{i,1}∩⋯∩u_{i,m}) = {t_{1}, ⋯, t_{l}}, and sexp′′ does not contain any projection symbols. Hence there exist t′_{j}, 1 ≤ j ≤ l such

that t_{j} ⟹^{⋆} t′_{j} and sexp′′ is t_{1}∩⋯∩t_{l} and d_{i} ∈ [[t′_{j}]]. Now T_{i} = N (u_{i,1}∩⋯∩u_{i,m}), and

hence by (a), V_{T_{i}} ⟹^{⋆} v_{1}∩⋯∩v_{p} such that {v_{1}, ⋯, v_{p}} = {t′_{1}, ⋯, t′_{l}}. In particular

v_{1} ∩⋯∩v_{p} does not contain any projection symbols since t′_{1}, ⋯, t′_{l} appear in sexp′′ and sexp′′ does not contain any projection symbols. Also d_{i} ∈ [[v_{1} ∩⋯∩v_{p}]]. Since d_{i} has fewer symbols than d, the induction hypothesis may be applied to yield a derivation V_{T_{i}} ⟹^{⋆} a_{i} such that a_{i} is atomic and d_{i} ∈ [[a_{i}]]. Summarizing:

V_{T} ⟹ f(V_{T_{1}}, ⋯, V_{T_{k}})
V_{T_{1}} ⟹^{⋆} a_{1}
⋯
V_{T_{k}} ⟹^{⋆} a_{k}

Hence there is a derivation V_{T} ⟹^{⋆} f(a_{1}, ⋯, a_{k}) where f(a_{1}, ⋯, a_{k}) is atomic and f(d_{1}, ⋯, d_{k}) ∈ [[f(a_{1}, ⋯, a_{k})]].

Proof for part (d): The proof proceeds by induction on the length of the derivation X ⟹^{⋆} sexp. The base case, where the derivation is of length 0 is vacuous since a derivation X ⟹^{⋆} sexp of length 0 implies that X is sexp, however sexp is ground and X is a variable. Now suppose that part (d) holds for derivations of length less than κ, let X ⟹^{⋆} sexp be a derivation of length κ, and let d ∈ [[sexp]]. Write the derivation X ⟹^{⋆} sexp as

X ⟹ s_{1} ∩ ⋯ ∩ s_{n} ⟹^{⋆} sexp

where the s_{i} do not contain the intersection symbol. That the derivation can be written this way follows from the fact that any expressions which appear nested in G are atomic (see proposition 10). Let X_{1}, ⋯, X_{m} denote the occurrences of variables in s_{1} ∩ ⋯ ∩ s_{n}. For each occurrence X_{i}, there is an expression x_{i} such that X_{i} ⟹^{⋆} x_{i} and such that sexp is the result of replacing each occurrence X_{i} in s_{1} ∩ ⋯ ∩ s_{n} by x_{i}. Since the length of the derivations X_{i} ⟹^{⋆} x_{i}, 1 ≤ i ≤ m, are each less than κ, the induction hypothesis can be applied to obtain

\begin{matrix}If d ∈ [[x_{i}]], then there exists an atomic a \\ such that d ∈ [[a]] and X_{i} ⟹^{⋆} a. \end{matrix} (4.8)

We now prove by induction that for each j, 1 ≤ j ≤ n, there exists a derivation of the form

X ⟹ t_{1} ∩ ⋯ ∩ t_{j} ∩ s_{j+1} ∩ ⋯ ∩ s_{n} ⟹^{⋆} u_{1} ∩ ⋯ ∩ u_{n} (4.9)

such that t_{1}, ⋯, t_{j} are are non-variable atomic expressions, u_{1}, ⋯, u_{n} are ground expressions, and

• d ∈ [[u_{i}]], 1 ≤ i ≤ n;

• t_{i} ⟹^{⋆} u_{i}, 1 ≤ i ≤ j;

• s_{i} ⟹^{⋆} u_{i}, j + 1 ≤ i ≤ n, and

• u_{1}, ⋯, u_{j} are atomic expressions.

The case where j = 0 is immediate. Now suppose that (4.9) holds for α, and consider α + 1 ≤ n. The expression s_{α+1} is either (i) a variable, (ii) a nonvariable atomic expression, or (iii) of the form f^{−1}(s). In case (i), s_{α+1} is one of the X_{i}. Hence by (4.8) there is an atomic a such that a is derivable from X_{i} and d ∈ [[a]]. Pick a minimum length derivation of a from X_{i}. Then, by proposition 12, this derivation has the form s_{α+1} ⟹ u ⟹^{⋆} a such that u is a non-variable atomic expression. Since G is closed under the substitution transformation, G must contain the transformation

X ⟹ t_{1} ∩ ⋯ ∩ t_{α} ∩ u ∩ s_{α+2} ∩ ⋯ ∩ s_{n},

and hence the following derivation can be constructed in G

X ⟹ t_{1} ∩ ⋯ ∩ t_{α} ∩ u ∩ s_{α+2} ∩ ⋯ ∩ s_{n} ⟹^{⋆} u_{1} ∩ ⋯ ∩ u_{α} ∩ a ∩ u_{α+1} ∩ ⋯ ∩ u_{n}

and this proves (4.9) for j = α + 1.

In case (ii), the proof is immediate, since s_{α+1} is already a non-variable atomic expression, and hence t_{α+1} can be set to s_{α+1}.

Finally, in case (iii), s_{α+1} is of the form f_{(l)}^{−1}(v) for some k-ary function symbol f such that 1 ≤ l ≤ k and f_{(l)}^{−1}(v) ⟹^{⋆} u_{α+1} and d ∈ [[u_{α+1}]]. This means that u_{α+1} must be of the form f_{(l)}^{−1}(u) such that v ⟹^{⋆} u and there exists a term of the form d′ = f(d_{1}, ⋯, d_{k}) ∈ [[u]] such that d_{l} is d. Now, since v is a nested expression in G, it must be an atomic expression. Also, each variable in v is one of the occurrences X_{i}. Recall that the occurrences of variables in v are denoted by X_{1}, ⋯, X_{m}. Now, where w is a subexpression of v, define that w[y_{1}, ⋯ y_{m}] is the expression obtained by replacing any occurrence X_{i} which also appears within w by y_{i}. In particular X_{i}[y_{1}, ⋯ y_{m}] = y_{i}. Also, if f(w_{1}, ⋯, w_{k}) is a subexpression of v, then f(w_{1}, ⋯, w_{k})[y_{1}, ⋯ y_{m}] = f(w_{1}[y_{1}, ⋯ y_{m}], ⋯, w_{k}[y_{1}, ⋯ y_{m}]). We now prove, for all subexpressions w of v, that

\begin{matrix}If e ∈ [[w[x_{1}, ⋯, x_{m}]]] then there exists an atomic a \\ such that w ⟹^{⋆} a and e ∈ [[a]] \end{matrix} (4.10)

The proof is by structural induction on subexpressions w of v. If w is a variable, then w is X_{i} for some i. Hence w[x_{1}, ⋯, x_{m}] is just x_{i}. But x_{i} is atomic, and so a can be chosen as x_{i}. If w is ⊥, then e ∈ [[w]] is not possible and so no a is needed. If w is ⊤, then a can be chosen to be ⊤. Finally, suppose that w is of the form f(w_{1}, ⋯, w_{k}) such that (4.10) holds for w_{1}, ⋯, w_{k}. If e ∈ f(w_{1}, ⋯, w_{k})[x_{1}, ⋯, x_{m}], then e is of the form f(e_{1}, ⋯, e_{k}) and e_{i} ∈ w_{i}[x_{1}, ⋯, x_{m}], 1 ≤ i ≤ k. Hence applying the assumption that (4.10) holds for w_{1}, ⋯, w_{k} implies that there exist a_{1}, ⋯, a_{k} such that e_{i} ∈ [[a_{i}]] and w_{i} ⟹^{⋆} a_{i},

1 ≤ i ≤ k. Clearly f(a_{1}, ⋯, a_{k}) is atomic, w ⟹^{⋆} f(a_{1}, ⋯, a_{k}) and f(e_{1}, ⋯, e_{k}) ∈

[[f(a_{1}, ⋯, a_{k})]]. This proves that (4.10) holds for all subexpressions w of v. In particular it holds for v. Hence there exists an atomic a_{v} such that v ⟹^{⋆} a_{v} and d ∈ [[a_{v}]].

We now show that G must contain a rule of the form

X ⟹ t_{1} ∩ ⋯ ∩ t_{α} ∩ f_{(l)}^{−1}(v′) ∩ u_{α+2} ∩ ⋯ ∩ s_{n} (4.11)

such that v′ ⟹^{⋆} a_{v} and v′ is not a variable. If v is already a variable, then there is nothing to show. If v is a variable, then choose the derivation v ⟹^{⋆} a_{v} to be a minimal length derivation of a_{v} from v. Now, by proposition 12 this derivation is of the form v ⟹ v′ ⟹^{⋆} a_{v} such that v′ is not a variable. Hence G contains the rules

\begin{aligned}X & ⟹ & t_{1} ∩ ⋯ ∩ t_{α} ∩ ∩f_{(l)}^{−1}(v) ∩ u_{α+2} ∩ ⋯ ∩ s_{n} \\ v & ⟹ & v′ \end{aligned}

and since G is closed under the substitution transformation, it must also contain the rule (4.11).

Since d′ ∈ f_{(l)}^{−1}(a_{v}), v′ must either be ⊤ or f(v′_{1}, ⋯, v′_{k}). Also v′ ⟹^{⋆} a_{v},

and so ORACLE(G, v′) is true. Hence if v′ is ⊤, then the preconditions of the ⊤-distribution transformation are satisfied, and if v′ is f(v′_{1}, ⋯, v′_{k}) then the preconditions of the ∩-distribution transformation are satisfied. Since G is closed under both transformations, it must contain a rule of the form

X ⟹ t_{1} ∩ ⋯ ∩ t_{α} ∩ t_{α+1} ∩ u_{α+2} ∩ ⋯ ∩ s_{n} (4.12)

where t_{α+1} is either ⊤ or v′_{l}. Recalling the d′ is of the form f(d_{1}, ⋯, d_{k}) such that d_{l} is d, f(v_{1}, ⋯, v_{k}) ⟹^{⋆} a_{v}, a_{v} is atomic and d′ ∈ [[a_{v}]], it follows that a_{v} is of the form f(a_{1}, ⋯, a_{k}) such that a_{1}, ⋯, a_{k} are atomic, v_{i} ⟹^{⋆} a_{i}, and d_{i} ∈ [[a_{i}]]. Hence v_{l} ⟹^{⋆} a_{l} for some atomic a_{l} such that d = d_{l} ∈ [[a_{l}]]. This completes case (iii), and also completes the proof that (4.9) holds for all 1 ≤ j ≤ n.

We now use (4.9) to complete the proof for part (d). In the case where j = n, (4.9) implies that there is a derivation X ⟹ t_{1} ∩ ⋯ ∩ t_{n} such that t_{i} ⟹^{⋆} u_{i}, 1 ≤ i ≤ n, the u_{i} are atomic and d ∈ [[u_{i}]]. Hence there exists an expression sexp′ which does not contain any projection symbols such that X ⟹^{⋆} sexp′ and d ∈ [[sexp′]]. Hence part (c) can be applied to complete the proof for part (d).

Combining these three propositions, we have

Lemma 3 (Grammar Simplification Algorithm) Let G be a set expression grammar in which all nested expressions are atomic and let G be input to the grammar simplification algorithm. Then

• the algorithm terminates and outputs some set expression grammar G′;

• G′ is a term grammar;

• G′ is equivalent to G in the sense that:

for all X ∈ var(G), I_{G′}(X) = I_{G}(X).

Proof: We first prove that the algorithm terminates. Let G_{0} denote the grammar input to the algorithm. Execution of the repeat loop of the algorithm then defines a sequence of grammars G_{0}, G_{1}, G_{2}, … such that

G_{0} → G_{1} → G_{2} → …

Furthermore, each G_{i}, i ≥ 1 contains all the rules in G_{i−1} plus at least one new rule. Now, the subexpression invariant proposition proves that, for all i ≥ 0, all nested expressions sexp of G_{i} are atomic and are such that N (sexp) contains only atomic subexpressions of G_{0}. This means that if X ⟹ sexp is a rule added during the algorithm, then

• any occurrence in sexp of an expression of the form s ∩ t or f_{(i)}^{−1}(s) cannot appear inside the scope of a function or projection symbol, but it may appear inside the scope of an ∩ symbol, and

• any occurrence in sexp of an expression of the form f_{(i)}^{−1}(s) is such that s is atomic.

Hence any rule added during execution of the algorithm must be of the form

X ⟹ a_{1} ∩… ∩ a_{k}, k ≥ 1

where each a_{j}, 1 ≤ j ≤ k is either

• an atomic expression, in which case it must also appear in G_{0}; • of the form f_{(i)}^{−1}(a) where a is an atomic expression which appears in G_{0}, f

is an n-ary function symbol which appears in G_{0} and 1 ≤ i ≤ n;

• a variable which appears in G_{0}, or

• a introduced variable of the form V_{S} such that S ⊆ atomic(G_{0}).

Furthermore, because duplicate expressions are removed from a rule before the rule is added to the grammar by the algorithm, the a_{j} must be distinct. It follows that there are only a finite number of distinct rules that can be added during execution of the algorithm. Since only new rules are added, it must eventually be the case that a grammar G_{m} is obtained such that no transformation is applicable. The main loop of the algorithm will then terminate, and a grammar G′ ⊆ G_{m} is output.

That the output grammar G′ is in fact a term grammar is clear since each rule X ⟹ sexp in G′ is a rule from G_{m} which satisfies the extra property that sexp does not contain intersection or projection symbols (that is, sexp is atomic).

To complete the proof, it remains to show that G′ is equivalent to G. Now, repeated application of the correctness of the individual transformations (proposition 9) proves that

for all X ∈ var(G), I_{G_{m}}(X) = I_{G}(X)

Therefore, it is sufficient to prove that I_{G′} = I_{G_{m}}. First, I_{G′} ⊆ I_{G_{m}} because G′ is a subset of G_{m} and so any derivation X ⟹^{⋆} sexp in G′ is also a derivation in G_{m}. Now, to prove I_{G′} ⊇ I_{G_{m}}, let X be a variable and let d ∈ I_{G_{m}}(X). This implies that there exists an ground expression such that X =Gm⇒⋆ sexp and d ∈ [[sexp]]. Since none of the transformations are applicable to G_{m}, lemma 2 is applicable. Hence there exists a ground atomic expression t such that X =G_{m}⇒⋆ t and d ∈ [[t]]. Now if the derivation X =G_{m}⇒⋆ t used rules which contained intersection or projection symbols, then the result of the derivation would also contain such symbols. However, t is atomic, and so each rule used must be of the form Y ⟹ a where a is atomic. Hence all such rules are present in G′. Therefore X =G′⇒⋆ t, which implies that d ∈ I_{G′}(X). This completes the proof that I_{G′} = I_{G_{m}}.

We now return to the problem of showing that the function ORACLE used in transformation 2 is recursive. We recall that ORACLE(G, X) is true iff there exists a ground atomic set expression such that X ⟹^{⋆} t and [[t]] ≠ ◯̸. Since t does not contain projection or intersection symbols, its derivation from X in G cannot involve rules which contain a projection symbol or intersection symbol. Hence ORACLE(G, X) iff ORACLE(G′, X) where G′ is the subset of rules from G which do not contain the projection symbol or intersection symbol. Such a grammar G′ is in fact a term grammar. Hence standard algorithms can be used to determine whether or not I_{G′}(X) = ◯̸, and this completes an implementation of ORACLE. Summarizing the sub-algorithms described in this subsection, we have:

Theorem 1 Let C be a reduced form conjunction of set constraints. The algorithm described in this subsection, when input with C:

• terminates, yielding a term grammar G, and

• I_{G}(X) = lm_{C}(X) for all X ∈ var(C).

5 Definite Set Constraints

We now apply the algorithms developed in section 4 to the the satisfiability problem for set constraints. We first prove a least model property.

Proposition 13 A conjunction C of definite set constraints has a least model whenever it has a model.

Proof: Let M be the collection of models of C. We prove that the intersection of these models defined by

(⋂ M) (X) =^{def} ⋂_{I∈M} I(X), X ∈ V AR

is also a model of C. Since this model is contained in all models in M, the proposition then follows. This model intersection property is proved using the following two facts^{12}

(⋂ M) (a) = ⋂_{I∈M} I(a)

(⋂ M) (sexp) ⊆ ⋂_{I∈M} I(sexp)

where a and sexp are an atomic set expression and a set expression respectively. These two facts can be easily verified using a structural induction argument on a and sexp respectively.

12Note that ⊇ in the second fact cannot be strengthened to equality.

Now, let a ⊇ sexp be a constraint in C. Then I(a) ⊇ I(sexp) for all I ∈ M. Combining this with the above two facts gives:

(⋂ M) (a) = ⋂_{I∈M} I(a)
⊇ ⋂_{I∈M} I(sexp)
⊇ (⋂ M) (sexp).

It follows that ⋂ M is a model of each constraint in C. Hence ⋂ M is the least model of C.

The following transformation serves to simplify the l.h.s. of each expressions in a conjunction of definite set constraints.

Transformation 5 (Flattening) Let C be a conjunction of definite constraints, and let f(t_{1}, ⋯, t_{n}) ⊇ sexp, n ≥ 1, be a constraint in C. Then replace this constraint with the constraints t_{1} ⊇ f_{(1)}^{−1}(sexp), ⋯, t_{n} ⊇ f_{(n)}^{−1}(sexp).

This transformation does not preserve equivalence because the transformed conjunction admits, in general, more models than the original conjunction possesses. However, we do have

Lemma 4 Let C be a conjunction of definite set constraints, and let C′ be the result of one or more applications of the flattening transformation on C. Then

• if C′ is unsatisfiable, then C is unsatisfiable;

• if lm_{C′} |̸= C, then C is unsatisfiable;

• if lm_{C′} ⊧ C, then lm_{C′} = lm_{C}.

Proof: Let application of the flattening transformation replace the constraint

f(t_{1}, ⋯, t_{n}) ⊇ sexp (5.13)

by the constraints

t_{1} ⊇ f_{(1)}^{−1}(sexp), ⋯, t_{n} ⊇ f_{(n)}^{−1}(sexp) (5.14)

We first show that (a) If I is a model of (5.13) then it is a model of (5.14).

(b) If I is a model of (5.14) such that I(sexp) ⊆ f(HU, ⋯, HU), then I is a model of (5.13).

To show (a), suppose that I is a model of (5.13). We now show that this implies that I is a model of t_{i} ⊇ f_{(i)}^{−1}(sexp), 1 ≤ i ≤ n. Suppose that d ∈ I(f_{(i)}^{−1}(sexp)). Then there must exist a term f(d_{1}, ⋯, d_{n}) in I(sexp) such that d = d_{i}. Now since I(f(t_{1}, ⋯, t_{n})) ⊇ I(sexp), f(d_{1}, ⋯, d_{n}) ∈ I(f(t_{1}, ⋯, t_{n})), and so d = d_{i} ∈ I(t_{i}). Hence I is a model of t_{i} ⊇ f_{(i)}^{−1}(sexp) over all i. It follows that I is a model of C′.

To show (b), suppose that I is a model of (5.14). Since I(sexp) ⊆ f(HU, ⋯, HU) we have that

f(f_{(1)}^{−1}(I(sexp)), ⋯, f_{(n)}^{−1}(I(sexp))) = I(sexp).

Now I(t_{i}) ⊇ I(f_{(i)}^{−1}(sexp)), 1 ≤ i ≤ n, and hence:

I(f(t_{1}, ⋯, t_{n})) = f(I(t_{1}), ⋯, I(t_{n}))
⊇ f(I(f_{(1)}^{−1}(sexp)), ⋯, I(f_{(n)}^{−1}(sexp)))
= f(f_{(1)}^{−1}(I(sexp)), ⋯, f_{(n)}^{−1}(I(sexp)))
= I(sexp)

We now complete the proof by showing that (a) and (b) imply the lemma. First, if (5.14) has no models, then (a) implies that (5.13) cannot have any models. This proves the first part of the lemma. Second, suppose that lm_{C′} |̸= C. Then, applying (b) with I replaced by lm_{C′}, proves that lm_{C′} must map sexp into a set which is not contained in f(HU,…, HU). This means that there exists a term d ∈ lm_{C′}(sexp) whose top-most symbol is not f. Let I be a model of C. By (a) I is a model of C′ and so I ⊇ lm_{C′}. Since d ∈ lm_{C′}(sexp), d ∈ I(sexp). But d cannot be an element of I(f(t_{1},…, f_{n})), and so I cannot be a model of C, which contradicts the choice of I. Hence C cannot have any models. This proves the second part of the lemma.

To prove the third part of the lemma, suppose that lm_{C′} ⊧ C. This implies that lm_{C} ⊆ lm_{C′}. Also, from (a), lm_{C′} ⊆ lm_{C}. Thus lm_{C} = lm_{C′}, and the third and final part of the lemma is proved.

An exhaustive application of the flattening transformation on a conjunction C can be easily shown to terminate. Constraints in the resulting conjunction C′ are of the form (a) X ⊇ sexp or (b) c ⊇ sexp where X is variable, c is a constant and sexp is a set expression. Let active(C′) denote the subset of C′ corresponding to (a). The following is the key property we require of constraints like C′:

Lemma 5 Let C be a conjunction of definite set constraints where each constraint is of the form X ⊇ sexp or c ⊇ sexp such that sexp is a set expression, X is a variable and c is a constant. Then

• lm(active(C)) exists;

• if lm(active(C)) |̸= C, then C is unsatisfiable;

• if lm(active(C)) ⊧ C, then lm(active(C)) = lm_{C}.

Proof: It is clear that lm(active(C)) exists since active(C) is a reduced form conjunction of constraints. To prove the remaining two parts of the lemma, let c ⊇ sexp be a constraint in C − active(C). Since active(C) ⊆ C, lm(active(C)) ⊆ I where I is any model of C. Hence if C has a model I, then lm_{C} satisfies c ⊇ sexp because

lm_{C}(c) = I(c) ⊇ I(sexp) ⊇ lm_{C}(sexp).

In summary then, if C has a model, then lm(active(C)) is also a model of C. Hence C is satisfiable if and only if lm(active(C)) is also a model of C. Moreover, if C has a model, then lm(active(C)) ⊇ lm_{C} and lm(active(C)) ⊆ lm_{C}.

Recall that given a term grammar representation of an interpretation I, we can determine whether or not an arbitrary set constraint is true in I. Combining this with Theorem 1 and the above lemmas, we have that the following algorithm decides the satisfiability of an input conjunction C of definite set constraints.

exhaustively-apply the flattening transformation to C to obtain C′; run the grammar simplification algorithm on active(C′) to obtain grammar G; if I_{G} ⊧ C then output G; else output “unsatisfiable”;

Theorem 2 Let C be a conjunction of definite set constraints. Then • the above algorithm terminates terminates on input C;

• if C is satisfiable, the algorithm outputs a term grammar G such that I_{G}(X) = lm_{C}(X) for all X ∈ var(C);

• if C is unsatisfiable, the algorithm outputs “unsatisfiable”.

Proof: It is clear that the algorithm terminates since (i) an exhaustive application of the flattening transformation clearly terminates (each application removes one function symbol from the l.h.s. of the constraints), and (ii) lemma 3 proves that the grammar simplification algorithm terminates. That the algorithm is correct can be proved as follows. Let C′ and I_{G} be as constructed by the grammar above algorithm. Then

I_{G}(X) = (lm(active(C′))) (X) for all X ∈ var(active(C′)).

We further assume that the new variables introduced by the grammar simplification algorithm are different from those in var(C) − var(active(C′)). Clearly it is always possible to choose the new variables so that this is the case. Hence I_{G}(X) = (lm(active(C′))) (X) for all X ∈ var(C), and so I_{G} satisfies C if and only if lm(active(C′)) satisfies C. From lemma 5 and repeated application of lemma 4, we have

C is satisfiable iff lm_{active(C′)} ⊧ C iff I_{G} satisfies C.

Also, if C is satisfiable, then

lm_{C}(X) = lm_{C′}(X) = I_{G}(X) for all X ∈ var(C).

References

[1] W. Ackermann, “Solvable Cases of the Decision Problem”, Studies in Logic and Foundations of Mathematics, North-Holland, 1962.

[2] J. Doner, “Tree Acceptors and Some of their Applications”, Journal of Computer and System Sciences 4, pp 406 - 451, 1970.

[3] F. Gècseg and M. Steinby, “Tree Automata”, Akadèmiai Kiadò, Budapest, 1984.

[4] N. Heintze and J. Jaffar, “A Finite Presentation Theorem for Approximating Logic Programs”, IBM technical report RC 16089 (# 71415), August 1990, 66 pp. (An abstract of this paper appears in Proc. ACM-POPL-90, pp. 197-209.)

[5] N.D. Jones and S.S. Muchnick, “Flow Analysis and Optimization of LISP-like Structures”, Proceedings 6^{th} ACM Symposium on Principles of Programming Languages, pp 244 - 256, 1979.

[6] R. McNaughton, “Parenthesis Grammars”, Journal of the ACM 14(3), pp 490 - 500, 1967.

[7] P. Mishra, “Toward a Theory of Types in PROLOG”, Proceedings 1^{st} IEEE Symposium on Logic Programming, Atlantic City, pp 289 - 298, 1984.

[8] M.O. Rabin, “Decidability of Second-order Theories and Automata on Infinite Trees”, Transactions of the American Math. Society 141, pp 1 - 35, 1969.

[9] J.C. Reynolds, “Automatic Computation of Data Set Definitions”, Information Processing 68, North-Holland, pp 456 - 461, 1969.

[10] J.W. Thatcher and J.B. Wright, “Generalized Finite Automata with an Application to a Decision Problem of Second-order Logic”, Mathematical Systems Theory 2, pp 57 - 82, 1968.

Appendix I: Grammar Simplification Examples

This appendix contains two examples illustrating the construction of the least model of reduced form set constraints. The relevant algorithms here are the grammar form algorithm and the grammar simplification algorithm (see section 4). Relevant transformations are indicated in parenthesis. Rules added by multiple applications of the substitution transformation are denote by (substitution*), and the intermediate rules are omitted. Finally, the rules which are output by the grammar simplification algorithm are indicated by †.

Example 1 Consider the following conjunction of constraints

\begin{aligned}X & ⊇ & (f(X, Y) ∩ f(Y, Z)) ∪ a \\ Y & ⊇ & a ∪ f(Y, Y) \\ Z & ⊇ & a \end{aligned}

After the preprocessing steps, the following set expression grammar is obtained and input to the grammar simplification algorithm.

X ⟹ f(X, Y) ∩ f(Y, Z)
† X ⟹ a
† Y ⟹ a
† Y ⟹ f(Y, Y)
† Z ⟹ a

The grammar simplification algorithm then adds the following rules.

†  X ⟹ f(Z_{{X,Y }}, Z_{{Y,Z}})  (∩-distribution)
Z_{{X,Y }} ⟹ X ∩ Y
Z_{{Y,Z}} ⟹ Y ∩ Z
Z_{{X,Y }} ⟹ a ∩ a  (substitution*)
Z_{{X,Y }} ⟹ a ∩ f(Y, Y)  (substitution*)
Z_{{X,Y }} ⟹ f(Z_{{X,Y }}, Z_{{Y,Z}}) ∩ a  (substitution*)
Z_{{X,Y }} ⟹ f(Z_{{X,Y }}, Z_{{Y,Z}}) ∩ f(Y, Y) (substitution*)
Z_{{Y,Z}} ⟹ f(Y, Y) ∩ a  (substitution*)
Z_{{Y,Z}} ⟹ a ∩ a  (substitution*)
† Z_{{X,Y }} ⟹ f(Z_{{X,Y }}, Z_{{Y,Z}})  (∩-distribution)
† Z_{{X,Y }} ⟹ a  (∩-distribution)
† Z_{{Y,Z}} ⟹ a  (∩-distribution)

Example 2 This example illustrates the simplification of constraints involving projection symbols. Consider the constraint X ⊇ a∪f(f(f(f(X))))∪f^{−1}(f^{−1}(X)). After the preprocessing steps, the following grammar is obtained

† X ⟹ a
† X ⟹ f(f(f(f(X))))
X ⟹ f^{−1}(X_{1})
X_{1} ⟹ f^{−1}(X)

The grammar simplification algorithm then adds the following rules.

X_{1} ⟹ f^{−1}(f(f(f(f(X))))) (substitution)
† X_{1} ⟹ f(f(f(X)))  (projection elimination)
X ⟹ f^{−1}(f(f(f(X))))  (substitution)
† X ⟹ f(f(X))  (projection elimination)
X_{1} ⟹ f^{−1}(f(f(X)))  (substitution)
† X_{1} ⟹ f(X)  (projection elimination)
X ⟹ f^{−1}(f(X))  (substitution)
X ⟹ X  (projection elimination)

Appendix II: Program Approximation Examples

One application of set constraints is in the approximate modeling of programs. The idea here is to extract from a program a conjunction of constraints which capture an approximation of the desired program property. In this section we will use this approach to obtain a conservative approximation of the values that program variables may assume during execution. We give only an informal outline of how the appropriate set constraints may be obtained from a program; a more detailed formulation of the extraction process is currently being investigated.

Example 3 Consider a simple imperative programming language with basic facilities for data structure creation (e.g. cons and nil for list creation) and data destructuring/projection (e.g. car and cdr for list destructuring). We also assume a simple template matching facility. This takes the form of a condition, x == template, which is true if the value of x is an instance of template. Now, let P be the program

0. x := cons(1, cons(2, cons(3, nil)));

1. while (x == cons(z_{1}, cons(z_{2}, z_{3}))) {

2. y := car(x);

3. x := cdr(x);

4. }

The focus of this example is the while loop at lines 1-4 which, for concreteness, we have preceded by a very simple initialization to the variable x. The general idea, however, is that the loop will be in the context of some larger program. Then, the possible values for x on entry to the loop will be determined, not by a simple initialization, but by set constraints corresponding to the rest of the program^{13}.

To model the above program P, we first introducing set variables, corresponding to the program variables, whose intent is to capture the possible values that the program variables may take. Constraints corresponding to P may then be written^{14}:

13In particular, the set of possible values for x may be infinite.

14The specific use of the complement symbol here is inconsequential, and the algorithms described in this paper can be easily adapted to solve these constraints.

(A) X_{entry} ⊇ cons(1, cons(2, cons(3, nil)))
(B) X_{while} ⊇ X_{entry}
(C) X_{body} ⊇ X_{while} ∩ cons(⊤, cons(⊤, ⊤))
(D) Y  ⊇ cons_{(1)}^{−1}(X_{body})
(E) X_{while} ⊇ cons_{(2)}^{−1}(X_{body})
(F) X_{exit} ⊇ X_{while} ∩ \overline{cons(⊤, cons(⊤, ⊤))}

where cons_{(1)}^{−1} and cons_{(2)}^{−1} respectively model car and cdr. Constraint (A) corresponds to line 0; constraints (B) and (C) correspond to line 1; constraints (D) and (E) correspond to lines 2 and 3 respectively; and constraint (F) corresponds to lines 1-4. The four variables X_{entry}, X_{while}, X_{body} and X_{exit} are intended to capture, respectively, the values of the variable X (a) before the execution of the while statement, (b) at the head of the while statement (c) at the start of the body of the while statement and (d) after execution of the while statement. (A single set variable could be used to capture all of these uses of X, resulting in a simpler, but less accurate, analysis.) The set of values of y is modeled by the set variable Y. The least model of the above constraints describes a conservative approximations to program variable values and is given by

X_{entry} = {cons(1, cons(2, cons(3, nil)))}
X_{while} = {cons(1, cons(2, cons(3, nil))),
cons(2, cons(3, nil)),
cons(3, nil)}
X_{body} = {cons(1, cons(2, cons(3, nil))),
cons(2, cons(3, nil))}
Y  = {1, 2}
X_{exit} = {cons(3, nil)}.

Example 4 An important aspect of the set constraint approach to program approximation which is not illustrated example 1, is the ability to uniformly deal with infinite sets of values. We conclude with a simple example of an analysis to approximate the success set of a logic program. Let m and n be some given positive integers. Let P_{m,n} be the logic program

p(a).
p(s^{m}(X)) ← p(X).
p(Y) ← p(s^{n}(Y)).

Then, on letting Υ denote an approximation to the set of terms t such that p(t) is true, we obtain an approximation to the meaning of p by noting that either (a) t is a; (b) t is s^{m}(t′) such that t′ is in Υ; or (c) t is such that s^{n}(t) is in Υ. Writing this as a set constraint, we obtain:

Υ ⊇ a ∪ s^{m}(Υ) ∪ s^{−n}(Υ).

The least model of this constraint gives Υ = {s^{αk}(a)} where k is the greatest common factor of m and n, and α ranges over the natural numbers. Hence, for this example, we have in fact obtained an exact description of the success set of P_{m,n}.