A Finite Presentation Theorem for

Approximating Logic Programs^{∗}

Nevin Heintze^{†} and Joxan Jaffar^{‡}

August 6, 1990

Abstract

In program analysis, a key notion used to approximate the meaning of a program is that of ignoring inter-variable dependencies. We formalize this notion in logic programming in order to define an approximation to the meaning of a program. The main result proves that this approximation is not only recursive, but that it can be finitely represented in the form of a cyclic term graph. This explicit representation can be used as a starting point for logic program analyzers.

∗A preliminary version appears in the Proceedings, 17^{th} ACM Symposium on POPL.

†School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213-3890 ‡IBM Thomas J. Watson Research Center, PO Box 218, Yorktown Heights, NY 10598

\underline{Section 1: Introduction} 1

1 Introduction

The problem at hand is: given a logic program, obtain an approximation of its meaning, that is, obtain an approximation of its least model. The definition of the approximation should be declarative (so that results can be proved about soundness and relative completeness); the approximation should be accurate (so that it is meaningful in program analysis), and finally, the approximated meaning should be a recursive set.

The notion of approximation used in this paper is based upon ignoring dependencies between program variables. Such dependencies are represented in the standard meaning of a logic program. For example, suppose that the least model of a program implies that some atom, with variables X and Y, is true just in case (X, Y) is (a, b) or (b, a). Then there is an inter-variable dependency between X and Y because assigning a value to one restricts the possible assignments to the other. A contrasting situation is when the atom is true just in case (X, Y) is (a, a), (a, b), (b, a) or (b, b). Now, the standard meaning of a logic program is the least amongst the collection of all its models. Analogously, our approximate meaning of a program is the least model obtained by ignoring inter-variable dependencies in the program. Consider two independent approaches to formalize this definition. The first approach is based on an appropriate method of representing models; the second approach is based on an appropriate interpretation of rules in a program.

A model of a logic program can be characterized as the union of several sets, one corresponding to each rule, and each such set represents the contribution of the corresponding rule to the model. Specifically, the set I_{R} corresponding to a rule R is such that if H ← Body is a ground instance of R where the atoms in Body are in the model, then H is in I_{R}. Traditionally, each such I_{R} is described by means of ground substitutions θ_{1}, θ_{2}, ⋯ so that I_{R} is {Hθ_{1}, Hθ_{2}, ⋯} ^{1}. Now, if I_{R} does not contain information about inter-variable dependencies, it can be described in a simpler way: use just one mapping which takes each rule variable into a set of elements as opposed an individual element. Such a mapping, call it a set-mapping, induces a mapping of the head atom of the rule into a set of ground atoms in an obvious way. For example, if α is the mapping [X ↦ {a, b}, Y ↦ {c}], then p(X, Y)α is {p(a, c), p(b, c)}^{2}. Call the class of models characterizable in this manner the set-based models. We can now define that the approximate meaning of a logic program is simply its least set-based model.

1Strictly speaking, some models can not be represented in this way. However, they are not important here.

2For obtaining the empty set, there is a distinguished mapping α such that tα = ◯̸ for any expression t.

Another approach to defining the approximate meaning of a program is to adapt the declarative reading of program rules. The standard reading of a rule H ← Body can be phrased as:

if the Body atoms, in the context of mappings θ_{1}, θ_{2}, ⋯, θ_{n} are true,
then the ground atoms Hθ_{1}, Hθ_{2}, ⋯, Hθ_{n} are true^{3}.

This reading embodies an inference which captures information about inter-variable dependencies; this information is represented in the mappings θ_{1}, θ_{2}, ⋯, θ_{n}. To ignore inter-variable dependencies, we collect together, for each variable X in the rule, the set S_{X} of possible values that X can take in the mappings. We then form a set-mapping α which maps each X into S_{X}, and apply this set-mapping to H. More formally, define α to be the set-mapping which maps X, for any variable X, into the set {Xθ_{1}, Xθ_{2}, ⋯, Xθ_{n}}. The declarative reading of a rule H ← Body thus becomes:

if the Body atoms, in the context of mappings θ_{1}, θ_{2}, ⋯, θ_{n} are true, then the ground atoms in Hα are true.

It can be proved that the least interpretation of a program which is consistent with this reading is indeed a model. Hence this interpretation conservatively approximates the meaning of the program. It can also be proved that this approach of defining the approximate meaning of a program is equivalent to the previous approach. That is, for any program, the least interpretation consistent with the above declarative reading of its rules is precisely the least set-based model.

\underline{Section 2: Preliminary Definitions} 3

In the logic programming literature, the notion of program approximation appears in the area of types (where sets of elements are associated to program entities such as variables and arguments of predicate and function symbols) and in the area of program analysis (where information about both semantic and runtime properties is sought). See, for example, [10, 3, 1, 14, 13, 6]. Two main approaches are used. In one [10, 14], a closure operator similar to α above is used. The closure here is at the level of tuples of predicate and function symbol arguments. For example, applying this argument-wise closure to the atom p(X, Y) in the context of the mappings [X ↦ f(a, b), Y ↦ c] and [X ↦ f(b, a), Y ↦ c], results in the set {p(f(a, b), c), p(f(b, a), c), p(f(a, a), c), p(f(b, b), c)}. Closure at the level of variables, on the other hand, gives {p(f(a, b), c), p(f(b, a), c)} instead. It is shown in [6] that the approximate meaning of a program defined using argument-wise closure is not as accurate as that defined using variable-wise closure^{4}.

3In the literature, n is 1 rather than an arbitrary finite number.

The other main approach to approximating the meaning of a program is based on abstract interpretation^{5} which involves treating several values as one abstract value [3, 1, 13]. This abstraction is chosen so that an iterative fixpoint computation, with respect to the underlying abstract semantic function, terminates. In terms of accuracy, these kinds of approximations are not directly comparable to that defined in this paper. For example, an abstract interpretation algorithm can reason exactly on the class of DATALOG programs, whereas the least set-based model of a DATALOG program is, in general, an approximation to its meaning. Conversely, the least set-based model of a unary program is exactly its meaning, whereas no standard abstract interpretation algorithm can be exact over all unary programs. In other words, while abstract interpretation algorithms can capture some information about inter-variable dependency, they must embody another form of approximation^{6}.

In summary, the starting point is the notion of approximation which is based upon ignoring inter-variable dependencies. This basic notion is not only highly intuitive, but has been shown to be important for efficiency reasons [8]. For logic programs, we formalize this notion in the form of set-based models, or equivalently, in the form of models consistent with an appropriate limitation on the inferences that a program rule can make. Our main result proves that this single limitation is sufficient to guarantee that the approximate meaning of any program is a recursive set. An important corollary of this result is a new and significant subclass of logic programs whose least models are recursive. This subclass, in which our program approximation is exact, is the class of programs whose head atoms are linear (no two occurrences of the same variable), and whose body atoms can be partitioned into groups such that (a) no two groups share a variable and (b) each group mentions only one head variable.

The most important aspect of our result, however, is an algorithm which outputs an explicit representation of the approximate meaning. This representation can be useful for logic program analysis. For example, most analyzers need to reason about the success set of a program. Hence an explicit representation of this set can be used as on oracle. Another example is that the representation can be used to identify appropriate abstractions of the underlying domain. These abstractions can then be used by standard abstraction interpretation algorithms.

4Even so, it is open as to whether or not argument-wise closure gives rise to an approximate meaning which is recursive.

5Abstract interpretation is also widely used to infer runtime properties.

6For efficiency most of these algorithms, e.g. [2], also ignore inter-variable dependencies.

2 Preliminary Definitions

See [7] for standard terminology and definitions about pure logic programs P. Let Σ and Π denote the functors, that is, the (nonempty) alphabet of predicate and function symbols respectively; let HU and HB then denote the resulting Herbrand universe and base. Let V AR_{t} and V AR_{a} denote denumerable sets of variables (which pertain to terms and atoms respectively) and let V AR denote their union. A logic program P consists of a finite number of rules made up from the alphabet Σ, Π and V AR_{t}. Assume, without losing generality, that no two rules in P have the same variable. Given a logic program P, we write (a) Π_{P}, Σ_{P} and V AR_{P} to respectively denote the finite sets of predicate symbols, function symbols and variables in P, (b) HU_{P} and HB_{P} to respectively denote the Herbrand universe and base arising from Π_{P} and Σ_{P}, and (c) P |_{p} denote those rules in P whose head atoms contain the predicate symbol p.

Where e is any expression, var(e) denotes its collection of variables, and e is ground if var(e) = ◯̸. A head-only variable in a rule is one which does not appear in the body. Similarly for body-only variables.

A substitution θ is a mapping from V AR into atoms and terms such that Xθ = X except for a finite number of variables. We write θ in the form [X_{1}/t_{1}, X_{2}/t_{2}, ⋯, X_{n}/t_{n}], n ≥ 0 to denote that θ maps X_{i} into t_{i}, 1 ≤ i ≤ n, and that θ is the identity mapping elsewhere. A substitution can be extended to be a mapping from atoms and terms into atoms and terms in an obvious way, and we write tθ to denote the image of the atom or term t under the substitution θ.

A set-substitution α is a mapping from V AR into sets of ground atoms and ground terms such that Xα = ◯̸ except for a finite number of variables. We write α in the form [X_{1}/S_{1}, X_{2}/S_{2}, ⋯ X_{n}/S_{n}], n ≥ 0 to denote that α maps X_{i} into the set S_{i}, 1 ≤ i ≤ n, and that α maps all other variables X into ◯̸. A set-substitution α can also be extended to be a mapping from atoms and terms into sets of ground atoms and ground terms by means of the rule: for any functor f,

f(t_{1}, ⋯, t_{n})α =^{def} {f(s_{1}, ⋯, s_{n}) : s_{1} ∈ t_{1}α, ⋯, s_{n} ∈ t_{n}α} .

An exception to this rule is a distinguished set-substitution ℧ which maps every atom or term, including ground atoms and terms, into ◯̸. (For example, if t is a ground term and α is a set substitution different from ℧, then by the above rules tα = {t}; however t℧ = ◯̸.)

We use the symbol ∼ to group atoms or terms into a possibly empty sequence or set, this choice being dictated by an obvious context. For example, we may write A ⟵ B̃ to denote a rule whose body atoms are represented by B̃. Writing B̃ ⊆ S, on the other hand, means that each atom in B̃ appears in S.

Where f is any function from 2^{HB_{P}} into 2^{HB_{P}}, let f↑n denote f^{n}(◯̸) when n ≥ 0, and let f↑ω denote ⋃_{i≥0} f^{i}(◯̸).

A set expression is constructed using given alphabets Π, Σ, V AR_{t} and V AR_{a}, and is defined to be either a set expression over terms or a set expression over atoms. A set expression over terms is one of the following:

• a special constant of the form ⊥ or ⊤;

• a variable in V AR_{t};

• f(t_{1}, ... , t_{n}) where f ∈ Σ is n-ary, n ≥ 0, and t_{1}, ⋯, t_{n} are set expressions over terms;

• t ∪ s or t ∩ s where t and s are set expressions over terms.

A set expression over atoms is one of the following:

• a variable in V AR_{a};

• p(t_{1}, ... , t_{n}) where p ∈ Π is n-ary, n ≥ 0, and t_{1}, ⋯, t_{n} are set expressions over terms constructed using Σ and V AR_{t};

• t ∪ s where t and s are set expressions over atoms.

A set equation is of the form s = t where s and t are both set expressions over atoms, or they are both set expressions over terms. An interpretation is a mapping from V AR_{a} into 2^{HB}, and from V AR_{t} into 2^{HU}. An interpretation I induces, in an obvious way, a mapping from set expressions t into 2^{HB} or 2^{HU} by means of the rule: if t is:

• a variable, then I(t) is already defined;

• the special constant ⊥, then I(t) is the empty set;

\underline{Section 3: The Approximate Meaning of a Logic Program} 6

• the special constant ⊤ then I(t) is HU; • a constant symbol c, then I(t) is {c};

• f(t_{1}, ... , t_{n}), where n ≥ 1 and f ∈ Π ∪ Σ, then I(t) is {f(s_{1}, ⋯, s_{n}) : s_{1} ∈ I(t_{1}), ⋯, s_{n} ∈ I(t_{n})};

• u ∪ s or u ∩ s, then I(t) is I(u) ∪ I(s) or I(u) ∩ I(s) respectively.

This mapping, in turn, induces a mapping from collections C of set equations into true or false in the obvious way. If I(C) is true, we say that I is a model of C^{7}.

Given two interpretations I and I′, the notation I ⊆_{V} I′ means I(X) ⊆ I′(X) for all X ∈ V, and the notation I ⊆ I′ abbreviates I ⊆_{V AR} I′. We write I =_{V} I′ to denote I ⊆_{V} I′ and I′ ⊆_{V} I. Where C is a collection of set equations, lm(C) denotes its least model, that is, lm(C) ⊆ I for any model I of C. Given two collections C and C′ of set equations, the notation C ⊧ C′ means that every model of C is a model of C′. The notation C ⟺_{V} C′ means that (a) for every model I of C there exists a model I′ of C′ such that I =_{V} I′, and (b) for every model I′ of C′ there exists a model I of C such that I =_{V} I′. Finally, we abbreviate ⟺_{V} by ⟺ when the set of variables in question is V AR.

3 The Approximate Meaning of a Logic Program

Define a set-based interpretation I of a logic program P to be a subset of HB_{P} which can be characterized as:

⋃_{1≤i≤N} H_{i}α_{i}

where each H_{i}, 1 ≤ i ≤ N, is a head atom in P, and each α_{i} is a set-substitution (possibly ℧). I is a set-based model if for each ground instance H ⟵ B̃ of R_{i}, 1 ≤ i ≤ N, H is in H_{i}α_{i} whenever B̃ ⊆ I.

Now, while the meaning of P is defined to be the smallest interpretation which models P, define the approximate meaning of P to be the smallest set-based model of P.

7The satisfiability problem for conjunctions of set equations is open. A decision procedure for a restricted class of equations appears in [5].

An equivalent definition of the exact meaning of P is that it is the least fixpoint of the following function which maps from and into interpretations of P:

T_{P} (I) =^{def} \left\{{Hβ : H ⟵ B̃ is in P, and \atop β ∈ \{θ : B̃θ ⊆ I\}}\right\}

where θ ranges over ground substitutions on var(P). Adapting this definition, one may obtain another definition of the approximate meaning of a program. Define an approximation operator A_{V} which maps a nonempty collection Θ of ground substitutions on V into the set-substitution α where

Xα = {Xθ : θ ∈ Θ}

for all variables X ∈ V. Further define that A_{V}(◯̸) is the distinguished setsubstitution ℧ which maps every atom or term (including ground atoms and terms) into ◯̸. Now define

τ_{P} (I) =^{def} \{a : a ∈ Hα where \begin{matrix}H ⟵ B̃ is in P, and \\ α = A_{var(H)}(\{θ : B̃θ ⊆ I\}) \end{matrix} \}

where θ ranges over ground substitutions on var(P). Note that τ_{P} ↑ω ⊇ T_{P} ↑ω for any P, and so the approximation defined by τ_{P} is conservative.

Proposition 1 For any logic program P, its least set-based model is τ_{P} ↑ω.

Proof: Let R_{1}, …, R_{N} comprise P, let R_{i} be of the form H_{i} ⟵ B̃_{i}, Let α_{i}, 1 ≤ i ≤ N, denote set substitutions. Let I ⊆ HB_{P}. The proposition follows from the fact that the least models of the following formulas are equivalent:

∃α_{1} … α_{N} (I = ⋃_{1≤i≤N}H_{i}α_{i} and ⋀_{1≤i≤N}H_{i}α_{i} ⊇ {H_{i}θ : B̃_{i}θ ⊆ I})  (3.1)

∃α_{1} … α_{N} (I = ⋃_{1≤i≤N}H_{i}α_{i} and \begin{matrix}/\ \\ 1 ≤ i ≤ N \\ X ∈ var(H_{i}) \end{matrix} Xα_{i} ⊆ \{Xθ : B̃_{i}θ ⊆ I\}) (3.2)

∃α_{1} … α_{N} (I = ⋃_{1≤i≤N}H_{i}α_{i} and \begin{matrix}/\ \\ 1 ≤ i ≤ N \\ X ∈ var(H_{i}) \end{matrix} Xα_{i} = \{Xθ : B̃_{i}θ ⊆ I\}) (3.3)

∃α_{1} … α_{N} (I = ⋃_{1≤i≤N}H_{i}α_{i} and ⋀_{1≤i≤N}α_{i} = A_{var(H_{i})} ({θ : B̃_{i}θ ⊆ I})) (3.4)
I = τ_{P} (I)  (3.5)

To show that (3.1) and (3.2) have the same least model, it suffices to prove that for any set substitution α, any set of substitutions Θ, and any atom or term t, that

tα ⊇ {tθ : θ ∈ Θ} iff ⋀_{X∈var(t)}Xα ⊇ {Xθ : θ ∈ Θ}.  (3.6)

Clearly (3.6) holds in the case that Θ is empty; now suppose otherwise. Proceeding by induction on the structure of t, we first note that (3.6) holds trivially in case t is a constant or variable because both sides of the above equivalence reduce to true. If t is of the form f(t_{1},…, t_{n}), then

f(t_{1},…, t_{n})α ⊇ {f(t_{1},…, t_{n})θ : θ ∈ Θ}
iff f(t_{1}α,…, t_{n}α) ⊇ f({t_{1}θ : θ ∈ Θ} ,…, {t_{n}θ : θ ∈ Θ})
iff t_{j}α ⊇ {t_{j}θ : θ ∈ Θ} , 1 ≤ j ≤ n (by definitions and Θ ≠ ◯̸)
iff ⋀_{X∈var(t_{j})}Xα ⊇ {Xθ : θ ∈ Θ} , 1 ≤ j ≤ n (by induction hypothesis)
iff ⋀_{X∈var(t)}Xα ⊇ {Xθ : θ ∈ Θ}

and so (3.6) is proved. This in turn proves that (3.1) and (3.2) have the same models, and hence they have the same least model.

To show that (3.2) and (3.3) have the same least model, it suffices to show that the least I satisfying (3.2) also satisfies (3.3). Let I be the least model of (3.2). Then there exist α_{1},…, α_{N} such that Xα_{i} ⊇ {Xθ : B̃_{i}θ ⊆ I} 1 ≤ i ≤ N,

X ∈ var(H_{i}) and I = ⋃_{1≤i≤N}H_{i}α_{i}. Now define α′_{i}, 1 ≤ i ≤ N, by

Xα′_{i} = {Xθ : B̃_{i}θ ⊆ I} X ∈ var(H_{i})

It follows that H_{i}α′_{i} ⊆ H_{i}α_{i}. Now define I′ to be ⋃_{1≤i≤N}H_{i}α_{i}. Clearly I′ ⊆ I. Also

I′ satisfies (3.2), and since I is the least model of (3.2), this implies I′ = I. This, in turn, implies that I satisfies (3.3), and hence that (3.2) and (3.3) have the same least model.

To show that (3.3) and (3.4) have the same least model, it suffices to prove the equivalence of the following for all 1 ≤ i ≤ N and all sets of substitutions Θ ground on var(H_{i}):

∃α_{i} (I ⊇ H_{i}α_{i} and ⋀_{X∈var(H_{i})}Xα_{i} = {Xθ : θ ∈ Θ});

∃α_{i} (I ⊇ H_{i}α_{i} and α_{i} = A_{var(H_{i})}(Θ)) .

In case Θ is empty, both these statements reduce to true (choose ℧ for α_{i}). Otherwise, α_{i} = A_{var(H_{i})}(Θ) is, by definition of A_{var(H_{i})}, such that Xα_{i} = {Xθ : θ ∈ Θ} for all X ∈ var(H_{i}).

Finally, (3.4) and (3.5) are equivalent, by definition. Hence we have proved that (3.1), (3.2), (3.3), (3.4) and (3.5) all have the same least model. To complete the proof, note that the least set-based model of P is the least model of (3.1) be definition. This means that the least set-based model of P is the least fixpoint of τ_{P}, and since τ_{P} is continuous (w.r.t. to ⊆), this is τ_{P} ↑ω.

The approximation operator A is a closure operator over a collection of substitutions. In the literature, the notion of closure has been applied over sets of terms and atoms rather than sets of substitutions. This notion can be realized by the operator ⋆ defined as follows: for any set S of ground terms or atoms,

S^{⋆} =^{def} {c : c is a constant in S} ∪ {f(t_{1}, ... , t_{n}) : t_{i} ∈ (f_{(i)}^{−1}(S))^{⋆}}

where f ranges over the function and predicate symbols in S, and f_{(i)}^{−1}(S) =^{def} {t_{i} : f(t_{1}, ⋯, t_{n}) ∈ S} denotes a projection of S. The work on types [14], for example, deals with the following function:

Y_{P} (I) =^{def} \{Hα : \begin{matrix}H ⟵ B̃ is in P, and \\ α ∈ \{θ : B̃θ ⊆ I\} \end{matrix} \}⋆

and so the approximate meaning of the program P is the least fixpoint Y_{P} ↑ω of Y_{P}. It is easy to see that Y_{P} is less accurate than τ_{P}. For example, the program P consisting of just two facts p(a, b) and p(b, a) is such that Y_{P} ↑ω = {p(a, a), p(a, b), p(b, a), p(b, b)} ⊃ T_{P} ↑ω whereas τ_{P} ↑ω = T_{P} ↑ω. The decidability of Y_{P} ↑ω was left open.

The earlier work in [10] associates to a program, not a function, but a formula in which variables range over sets. The approximate meaning of a program is then given by a certain model of these formulas. It turns out that this model is essentially a fixpoint of Y_{P}. The accuracy of the program approximation that this model defines is therefore bounded by Y_{P} ↑ω. In [10] and in a subsequent paper [11], algorithms were presented for solving subclasses of these set formulas. The solvability problem for the general class was left open.

We now conclude this section by illustrating the differences between Y_{P}, τ_{P} and T_{P} on an example program P:

    p(f(a, b)).
    p(f(b, a)).
    r(X) ⟵ p(f(X, X)).
    s(f(Y, Z)) ⟵ p(f(Y, Z)).

Here Y_{P} ↑ω is \{ \begin{matrix}p(f(a, a)), p(f(a, b)), p(f(b, a)), p(f(b, b)) \\ r(a), r(b) \\ s(f(a, a)), s(f(a, b)), s(f(b, a)), s(f(b, b)) \end{matrix} \} ,

τ_{P} ↑ω is \{ \begin{matrix}p(f(a, b)), p(f(b, a)) \\ s(f(a, a)), s(f(a, b)), s(f(b, a)), s(f(b, b)) \end{matrix} \}, and

T_{P} ↑ω is \{ \begin{matrix}p(f(a, b)), p(f(b, a)) \\ s(f(a, b)), s(f(b, a)) \end{matrix} \}.

In general, we have Y_{P} ↑ω ⊇ τ_{P} ↑ω ⊇ T_{P} ↑ω for any program P.

\underline{Section 4: A Closed Form Representation using Set Formulas} 11

In summary for this section, the approximate meaning of a program P is defined to be its least set-based model, or equivalently, the least fixpoint of τ_{P}. We argued that this formalizes the notion of ignoring inter-variable dependencies in logic programs, and further, that this approximation is more accurate than similar functions which have been used in logic program analysis. In what follows, the fixpoint formulation of approximate meaning will be used as the basis for the main algorithm.

4 A Closed Form Representation using Set Formulas

Our first step toward a finite representation of τ_{P} ↑ω is a formula containing quantified set equations. This formula contains certain distinguished variables. An interpretation I of the formula can then be viewed as a subset of HB_{P} by taking the union of the I-images of these distinguished variables. The essential property of the formula is that its models, thus viewed as subsets of HB_{P}, are precisely the fixpoints of τ_{P}.

This formula is comprised of two main parts. The first is a collection C_{P} of set equations, constructed from a given program P as follows. Let P contain the rules R_{1}, R_{2}, …, R_{N}, N ≥ 1. Associate to each predicate symbol p ∈ Π_{P}, a new variable Υ_{p} over atoms, and associate to each rule R_{i} a new variable ξ_{i} over atoms. C_{P} can now be defined as the union of equations of the form

Υ_{p} = \{ \begin{matrix}⋃_{i : R_{i} ∈ P |_{p}} ξ_{i} & if p is in a head atom in P; \\ ⊥ & otherwise; \end{matrix}

for all p ∈ Π_{P}. Let the distinguished variables of the form Υ_{p} be called the type variables corresponding to P.

The second part of the set formula makes a connection between (a) the variables ξ_{i} in C_{P} and the head atoms in P, and (b) the type variables in P and the body atoms in P. This set formula is a conjunction of several subformulas, one for each rule in P. Before introducing these subformulas, again let P be comprised of the rules R_{1}, …, R_{N}, and let the i^{th} rule R_{i} be of the form H ⟵ B̃. Now associate to the rule R_{i} the following collection of pairs:

{(ξ_{i}, H)} ⋃
{(p(t̃), Υ_{p}) : p(t̃) ∈ B̃} ⋃
{(X, ⊤_{t}) : X is a head-only variable in R_{i}} .

The subformula corresponding to each rule R_{i}, call it F(D_{P}^{i}), will be defined in terms of the pairs D_{P}^{i}. Before we formally define F(D_{P}^{i}), we consider some example programs. Let P be

    p(a).
    p(b).
    q(X) ⟵ p(X).

so that C_{P} is {Υ_{p} = ξ_{1} ∪ ξ_{2}, Υ_{q} = ξ_{3}}, D_{P}^{1} is {(ξ_{1}, p(a))}, D_{P}^{2} is {(ξ_{2}, p(b))}, and finally, D_{P}^{3} is {(ξ_{3}, q(X)), (p(X), Υ_{p})}. In this example, if it defined that a pair simply represents a set equation between its constituent parts, then

C_{P} ∧ F(D_{P}^{1} ) ∧ F(D_{P}^{2} ) ∧ F(D_{P}^{3} )

represents the set equations

\begin{aligned}Υ_{p} & = & ξ_{1} ∪ ξ_{2}, \\ Υ_{q} & = & ξ_{3}, \\ ξ_{1} & = & p(a), \\ ξ_{2} & = & p(b), \\ ξ_{3} & = & q(X), \\ p(X) & = & Υ_{p}. \end{aligned}

These equations capture τ_{P} ↑ω in the sense that the images of the type variables Υ_{p} and Υ_{q} in the least model of the equations (in which X = {a, b}) sums to become τ_{P} ↑ω. In general, however, obtaining a subformula F(D_{P}^{i}) by simply by making the pairs D_{P}^{i} into set equations will not work. Suppose P were

    p(a).
    p(b).
    q(a).
    q(c).
    r(X) ⟵ p(X), q(X).

Then C_{P} is {Υ_{p} = ξ_{1} ∪ ξ_{2}, Υ_{q} = ξ_{3} ∪ ξ_{4}, Υ_{r} = ξ_{5}}, D_{P}^{1} is {(ξ_{1}, p(a))},

D_{P}^{2} is {(ξ_{2}, p(b))},
D_{P}^{3} is {(ξ_{3}, q(a))},
D_{P}^{4} is {(ξ_{4}, q(c))}, and finally,
D_{P}^{5} is {(ξ_{5}, r(X)), (p(X), Υ_{p}), (q(X), Υ_{q})}.

Let the subformulas F(D_{P}^{1} ), F(D_{P}^{2} ), F(D_{P}^{3} ) and F(D_{P}^{4} ) be set equations as before. If F(D_{P}^{5} ) is also defined to be set equations, that is, {ξ_{5} = r(X), p(X) = Υ_{p}, q(X) = Υ_{q}}, then the entire subformula is inconsistent. For this example, an appropriate formulation of F(D_{P}^{5} ) is

\begin{aligned}ξ_{5} & = & \{u : ∃x ( \begin{matrix}u & ∈ & r(X), \\ p(x) & ∈ & Υ_{p}, \\ q(x) & ∈ & Υ_{q} \end{matrix} )\} \\ X & = & \{x : ∃u ( \begin{matrix}u & ∈ & r(X), \\ p(x) & ∈ & Υ_{p}, \\ q(x) & ∈ & Υ_{q} \end{matrix} )\} \end{aligned}

so that the least model of the subformula formula C_{P} ∧ F(D_{P}^{1} ) ∧ F(D_{P}^{2} ) ∧ F(D_{P}^{3} ) ∧ F(D_{P}^{4} ) ∧ F(D_{P}^{5} ) (in which X = {a}) captures τ_{P} ↑ω.

The above two examples only have one variable in the body atoms. Now suppose P were

    p(a, b).
    p(c, d).
    q(X, Y) ⟵ p(X, Y).

then C_{P} is {Υ_{p} = ξ_{1} ∪ ξ_{2}, Υ_{q} = ξ_{3}}, D_{P}^{1} is {(ξ_{1}, p(a, b))}, D_{P}^{2} is {(ξ_{2}, p(c, d))}, and finally, D_{P}^{3} is {(ξ_{3}, q(X, Y)), (p(X, Y), Υ_{p})}. Let F(D_{P}^{1} ) and F(D_{P}^{2} ) be set equations as before. An appropriate formulation of F(D_{P}^{3} ) is a conjunction of three equations

\begin{aligned}ξ_{3} & = & \{u : ∃xy ( \begin{matrix}u & ∈ & q(X, Y), \\ p(x, y) & ∈ & Υ_{p} \end{matrix} )\} , \\ X & = & \{x : ∃uy ( \begin{matrix}u & ∈ & q(X, Y), \\ p(x, y) & ∈ & Υ_{p} \end{matrix} )\} , \\ Y & = & \{y : ∃ux ( \begin{matrix}u & ∈ & q(X, Y), \\ p(x, y) & ∈ & Υ_{p} \end{matrix} )\} \end{aligned}

so that the least model of our formula C_{P} ∧ F(D_{P}^{1} ) ∧ F(D_{P}^{2} ) ∧ F(D_{P}^{3} ) (in which X = {a, c} and Y = {b, d}) captures τ_{P} ↑ω.

In general, the collection of pairs associated to a rule in the program is of the form {(a_{1}, sexp_{1}), ⋯, (a_{m}, sexp_{m})} where

• each a_{j}, for all 1 ≤ j ≤ m, is an atom or term, and

• each sexp_{j}, for all 1 ≤ j ≤ m, is a set expression.

Let D be such a collection of pairs {(a_{1}, sexp_{1}), ⋯, (a_{m}, sexp_{m})}, and let V = {X_{1}, ⋯, X_{k}} denote the variables in the l.h.s. of D. Now define F(D) to be following conjunction of k equations:

/\_{1 ≤ j ≤ k} X_{j} = {x_{j} : ∃x_{1} ⋯ x_{j−1}x_{j+1} ⋯ x_{k} ( a_{1}μ ∈ sexp_{1} ; ⋮ ; a_{m}μ ∈ sexp_{m} )}

where x_{1},…, x_{k} are new variables, and

μ denotes the renaming substitution [X_{1}/x_{1}, ⋯, X_{k}/x_{k}] .

We refer to equations appearing in F(D) as quantified equations. An interpretation and model of a collection of quantified equations are defined by extending, in the obvious way, the definitions given in section 2 for an interpretation and a model of set equations. Note that an interpretation of the r.h.s. of one of the above quantified equations is uniquely determined by an interpretation of the sexp_{i}, 1 ≤ i ≤ n. In other words, where D is a collection of pairs as described above, an interpretation of the r.h.s. of D uniquely determines an interpretation of the r.h.s. of F(D).

Summarizing, we obtain from a program P a formula whose least model characterizes the desired set τ_{P} ↑ω. Let R_{1},…, R_{N} denote the rules in P. This formula is

C_{P} ∧ F(D_{P}^{1} ) ∧ ⋯ ∧ F(D_{P}^{N})

where C_{P} is

/\_{p ∈ Π_{P}} Υ_{p} = ⋃_{i:R_{i}∈P |_{p}} ξ_{i}

and each D_{P}^{i}, 1 ≤ i ≤ N, is a collection of pairs associated to the rule R_{i}. Let R_{i} be of the form H_{i} ⟵ B̃_{i}. Then D_{P}^{i} is

{(ξ_{i}, H_{i})} ⋃
{(p(t̃), Υ_{p}) : p(t̃) ∈ B̃_{i}} ⋃
{(X, ⊤_{t}) : X is a head-only variable in R_{i}} .

For example, consider the program P:

    p(a, b).
    p(b, a).
    q(X, W) ⟵ p(X, X).
    r(Y, Z) ⟵ p(Y, Z).

\underline{Section 4: A Closed Form Representation using Set Formulas} 15 The set formula corresponding to P is given by first obtaining C_{P} = {Υ_{p} = ξ_{1} ∪ ξ_{2}, Υ_{q} = ξ_{3}, Υ_{r} = ξ_{4}}, and then obtaining

\begin{aligned}D_{P}^{1} & = & \{(ξ_{1}, p(a, b))\}, \\ D_{P}^{2} & = & \{(ξ_{2}, p(b, a))\}, \\ D_{P}^{3} & = & \{(ξ_{3}, q(X, W)), (p(X, X), Υ_{p}), (W, ⊤_{a})\}, \\ D_{P}^{4} & = & \{(ξ_{4}, r(Y, Z)), (p(Y, Z), Υ_{p})\}. \end{aligned}

The set formula corresponding to P is C_{P} ∧ F(D_{P}^{1} ) ∧ … ∧ F(D_{P}^{4} ), that is: Υ_{p} = ξ_{1} ∪ ξ_{2}, Υ_{q} = ξ_{3}, Υ_{r} = ξ_{4}, ξ_{1} = {u : u ∈ p(a, b)}, ξ_{2} = {u : u ∈ p(b, a)},

ξ_{3} = \{u : ∃xw ( \begin{matrix}u & ∈ & q(X, W), \\ p(x, x) & ∈ & Υ_{p} \\ w & ∈ & ⊤_{a} \end{matrix} )\} ,

X = \{x : ∃uw ( \begin{matrix}u & ∈ & q(X, W), \\ p(x, x) & ∈ & Υ_{p} \\ w & ∈ & ⊤_{a} \end{matrix} )\} ,

W = \{x : ∃ux ( \begin{matrix}u & ∈ & q(X, W), \\ p(x, x) & ∈ & Υ_{p} \\ w & ∈ & ⊤_{a} \end{matrix} )\} ,

ξ_{4} = \{u : ∃yz ( \begin{matrix}u & ∈ & r(Y, Z), \\ p(y, z) & ∈ & Υ_{p} \end{matrix} )\} ,

Y = \{y : ∃uz ( \begin{matrix}u & ∈ & r(Y, Z), \\ p(y, z) & ∈ & Υ_{p} \end{matrix} )\} ,

Z = \{z : ∃uy ( \begin{matrix}u & ∈ & r(Y, Z), \\ p(y, z) & ∈ & Υ_{p} \end{matrix} )\} .

The one and only model for this formula is given by

Υ_{p} = {p(a, b), p(b, a)},
Υ_{q} = ◯̸,
Υ_{r} = {r(a, a), r(b, b), r(a, b), r(b, a)},
X = ◯̸,
W = ◯̸,
Y = {a, b},
Z = {a, b}

and when this model is viewed as a subset of HB_{P}, we obtain

{p(a, b), p(b, a), r(a, a), r(b, b), r(a, b), r(b, a)}.

In what follows, we reserve the symbol N for the number of rules in the program P at hand, and we shall abbreviate the sequence D_{P}^{1} , ⋯, D_{P}^{N} by D̃_{P}, and the formula F(D_{P}^{1} ) ∧ ⋯ ∧ F(D_{P}^{N}) by F(D̃_{P}). We now prove that the models of the formula C_{P} ∧ F(D̃_{P}) correspond to the fixpoints of τ_{P} in the following sense:

Main Lemma 1 Let P be a logic program, and let I ⊆ HB_{P}. Then I is a fixpoint of τ_{P} iff there is model I′ of C_{P} ∧ F(D̃_{P}) such that

I = ⋃_{p∈Π_{P}} I′(Υ_{p}).

Proof: Let P contain the rules R_{1}, R_{2},…, R_{N}, and for each rule R_{i}, 1 ≤ i ≤ N, let H_{i} denote its head atom and let B̃_{i} denote its body atoms. In what follows, θ stands for a substitution which is ground on var(P), and β stands for a substitution which is ground on var(P) ∪ {ξ_{1},…, ξ_{N}}. Now consider the following chain of propositions:

1. I = τ_{P} (I)

2. I = \{a : a ∈ Hα where \begin{matrix}H ⟵ B̃ ∈ P, and \\ α = A_{var(H_{i})}(\{θ : B̃θ ⊆ I\}) \end{matrix} \}
3. I = ⋃_{1≤i≤N} {a : a ∈ H_{i}α where α = A_{var(H_{i})}({θ : B̃_{i}θ ⊆ I})}

4. I = ⋃_{1≤i≤N}H_{i}(A_{var(H_{i})}({θ : B̃_{i}θ ⊆ I}))

5. I = ⋃_{1≤i≤N}H_{i}α_{i}

where α_{i}, 1 ≤ i ≤ N, is ℧ in the case that ¬∃θ (B̃_{i}θ ⊆ I); otherwise, α_{i} is the set-substitution such that Xα_{i} = {Xθ : B̃_{i}θ ⊆ I} for all X ∈ var(R_{i}).

6. /\_{p ∈ Π_{P}} I|_{p} = ⋃_{R_{i} ∈ P |_{p}} H_{i}α_{i}

where α_{i}, 1 ≤ i ≤ N, is ℧ in the case that ¬∃θ (B̃_{i}θ ⊆ I); otherwise, α_{i} is the set-substitution such that Xα_{i} = {Xθ : B̃_{i}θ ⊆ I} for all X ∈ var(R_{i}).

7. \{ \begin{matrix}/\_{p ∈ Π_{P}} & Υ_{p} & = & ⋃ \{H_{i} : R_{i} ∈ P |_{p} and ∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}Υ_{p})\} \\ \begin{matrix}/\ \\ 1 ≤ i ≤ N \\ X ∈ var(R_{i}) \end{matrix} & X & = & \{Xθ : B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}Υ_{p}\} \end{matrix}

8. \{ \begin{matrix}/\_{p ∈ Π_{P}} & Υ_{p} & = & ⋃_{i : R_{i} ∈ P |_{p}} Υ_{i} \\ /\_{1 ≤ i ≤ N} & Υ_{i} & = & \{t : t ∈ H_{i} and ∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}Υ_{p})\} \\ \begin{matrix}/\ \\ 1 ≤ i ≤ N \\ X ∈ var(R_{i}) \end{matrix} & X & = & \{Xθ : B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}Υ_{p}\} \end{matrix}

9. \{ \begin{matrix}/\_{p ∈ Π_{P}} & Υ_{p} & = & ⋃_{i : R_{i} ∈ P |_{p}} Υ_{i} \\ \begin{matrix}/\ \\ 1 ≤ i ≤ N \\ W ∈ var(R_{i}) ∪ \{Υ_{i}\} \end{matrix} & W & = & \{W β : ( \begin{matrix}Υ_{i}β & ∈ & H_{i} \\ B̃_{i}β & ⊆ & ⋃_{p∈Π_{P}}Υ_{p} \end{matrix} )\} \end{matrix}

10. \{ \begin{matrix}/\_{p ∈ Π_{P}} & Υ_{p} & = & ⋃_{i : R_{i} ∈ P |_{p}} Υ_{i} \\ \begin{matrix}/\ \\ 1 ≤ i ≤ N \\ W ∈ var(R_{i}) ∪ \{Υ_{i}\} \end{matrix} & W & = & \{W β : ( \begin{matrix}& Υ_{i}β & ∈ & H_{i} \\ ⋀_{q(t̃)∈B̃_{i}} & q(t̃)β & ∈ & Υ_{q} \\ ⋀_{Z∈HEADONLY_{R_{i}}} & Zβ & ∈ & ⊤_{t} \end{matrix} )\} \end{matrix}

11. \{ \begin{matrix}/\_{p ∈ Π_{P}} & Υ_{p} & = & ⋃_{i : R_{i} ∈ P |_{p}} Υ_{i} \\ \begin{matrix}/\ \\ 1 ≤ i ≤ N \\ W ∈ var(R_{i}) ∪ \{Υ_{i}\} \end{matrix} & W & = & \{W β : ⋀_{(a,sexp)∈D_{P}^{i}} aβ ∈ sexp\} \end{matrix}

12. \{ \begin{matrix}/\_{p ∈ Π_{P}} & Υ_{p} & = & ⋃_{i : R_{i} ∈ P |_{p}} Υ_{i} \\ \begin{matrix}/\ \\ 1 ≤ i ≤ N \\ W ∈ var(R_{i}) ∪ \{Υ_{i}\} \end{matrix} & W & = & \{x : ∃y_{1}y_{2} ⋯ y_{m} ( ⋀_{(a,sexp)∈D_{P}^{i}} aμ ∈ sexp)\} \\ & & & where var(R̃_{i}) ∪ \{Υ_{i}\} = X, Y_{1}, ⋯, Y_{m}, \\ & & & x, y_{1}, ⋯, y_{m} are new variables, and \\ & & & μ denotes the renaming substitution \\ & & & [X/x, Y_{1}/y_{1}, ⋯, Y_{m}/y_{m}]. \end{matrix}

13. C_{P} ∧ F (D_{P}^{1} ) ∧ ⋯ ∧ F (D_{P}^{N} ).

The r.h.s. of proposition (2) is equal to the r.h.s. of (1) by the definition of τ_{P}. The r.h.s. of proposition (3) is a rewriting of the r.h.s. of (2) in such a way that the set generated by each individual rule is mentioned explicitly. That the r.h.s. of proposition (4) is equal to the r.h.s. of (3) is immediate. The r.h.s. of proposition (5) is equal to the r.h.s. of (4) because each set substitution α_{i} described in (5) is the same as the set substitution A_{var(H_{i})}({θ : B̃_{i}θ ⊆ I}) on the variables in R_{i}. Proposition (6) is merely a restatement of (5) in such a way that the sets associated to each predicate symbol in Π_{P} are mentioned individually. Combining these arguments, we have that propositions (1) through (6) are equivalent.

We now show that propositions (6) and (7) are equivalent in the sense that I ⊆ HB_{P} models (6) iff there is a model I′ of (7) such that I = ⋃_{p∈Π_{P}} I′(Υ_{p}).

Let I ⊆ HB_{P} satisfy (6), and define an interpretation I′ of (7) by first specifying that I′(Υ_{p}) =^{def} I|_{p} for all p ∈ Π_{P}, and then specifying that

I′(X) =^{def} {Xθ : B̃_{i}θ ⊆ ⋃_{p∈Π_{P}} I|_{p}} , 1 ≤ i ≤ N, X ∈ var(R_{i}). (4.7)

Thus I′ models the second conjunction in (7) by design. To see that I′ also models the first conjunction in (7), consider

I′(Υ_{p}) = I|_{p}
= ⋃_{R_{i}∈H|_{p}} H_{i}α_{i}
= ⋃ {I′(H_{i}) : R_{i} ∈ P |_{p} and ∃θ (B̃_{i}θ ⊆ I)}
= I′ (⋃ {H_{i} : R_{i} ∈ P |_{p} and ∃θ (B̃_{i}θ ⊆ I)}) .
= I′ (⋃ {H_{i} : R_{i} ∈ P |_{p} and ∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}Υ_{p})}) .

The first equation follows by design. The second equation follows from the fact that I satisfies (6). To prove the third equation, fix an i, 1 ≤ i ≤ N. In the case that ∃θ (B̃_{i}θ ⊆ I), we have Xα_{i} = I′(X) for all X ∈ var(R_{i}), and that α_{i} is different from ℧. Now, if a set substitution different from ℧ agrees with an interpretation on a set of variables, they both extend to the same mapping on atoms involving only these variables. Hence H_{i}α_{i} = I′(H_{i}). In the case that ¬∃θ (B̃_{i}θ ⊆ I), α_{i} is ℧, and there is no set corresponding to H_{i} in the r.h.s. In short, for every i, either there are equivalent sets in both sides of the third equation, or else H_{i}α_{i} is empty in the l.h.s. and there is no set for i in the r.h.s. The fourth equality follows from the general property that I(t_{1}) ∪ I(t_{2}) = I(t_{1} ∪ t_{2}) for any interpretation I and any atoms t_{1} and t_{2}. Finally, the fifth equation follows from the fact that

I′ ( ⋃_{p∈Π_{P}}Υ_{p}) = I.

Thus I′ models the first conjunction in (7) and so I′ models all of (7).

Conversely, suppose that I′ is a model of (7). Let I ⊆ HB_{P} be defined as the union of I′(Υ_{p}) over all p ∈ Π_{P}. Arguing like above, it can proved that

I|_{p} = I′(Υ_{p})
= I′ (⋃ {H_{i} : R_{i} ∈ P |_{p} and ∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}Υ_{p})})
= ⋃ {I′(H_{i}) : R_{i} ∈ P |_{p} and ∃θ (B̃_{i}θ ⊆ I)}
= ⋃_{1≤i≤N} H_{i}α_{i}.

Thus proposition (7) is equivalent to (6) in the sense that a subset I of HB_{P} satisfies (6) iff there is a model I′ of (7) such that I′(Υ_{p}) = I|_{p} for all p ∈ Π_{P}.

We now prove that proposition (7) and (8) are equivalent in the sense that I models (7) iff there is an adaptation I′ of I (to the variables Υ_{i}) such that I′ models (8). Let I be a model of (7). Construct I′ by

I′(Υ_{i}) =^{def} \{ \begin{matrix}I(H_{i}), & if ∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}I(Υ_{p})) \\ ◯̸, & otherwise. \end{matrix} (4.8)

I′ models the third conjunction in (8), which represent the second conjunction in (7), because it agrees with I on the variables in these equations. To show that I′ models the second conjunction in (8), consider the i^{th} equation therein. If ¬∃θ (B̃_{i}θ ⊆ I) then I′ maps the r.h.s. of this equation into ◯̸. In the alternative case, I′ maps the r.h.s. of the equation into I′({t : t ∈ H_{i}}), that is, I(H_{i}). Thus, in both cases, I′ maps the r.h.s. of the equation into I′(Υ_{i}). Finally, that I′ models the first conjunction of (8) can be shown by first fixing the value of p and then arguing as follows:

I′(Υ_{p}) = I(Υ_{p})
= I (⋃ {H_{i} : R_{i} ∈ P |_{p} and ∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}Υ_{p})})
= ⋃ {I (H_{i}) : R_{i} ∈ P |_{p} and ∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}I(Υ_{p}))}
= I′ ( ⋃_{R_{i}∈P |_{p}}Υ_{i})

The first equation follows the definition of I′. The second equation holds because I is a model of (7). The third equation merely involves a distribution of I. The final equation follows from the definition (4.8). Hence any model I of (7) can be adapted to become a model I′ of (8) such that both models agree on the variables Υ_{p}.

The converse argument, that any model of (8) is a model of (7), can be established by similar arguments. Thus proposition (8) is equivalent to (7) in the sense that an interpretation I is a model of (7) iff there is a model I′ of (8) such that I′(Υ_{p}) = I(Υ_{p}) for all p ∈ Π_{P}.

The difference between propositions (8) and (9) is that the second and third conjunctions in (8) are collapsed into one conjunction in (9). Specifically, for each i, 1 ≤ i ≤ N, the equations

Υ_{i} = {t : t ∈ H_{i} and ∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}Υ_{p})}
/\_{X ∈ var(R_{i})} X = {Xθ : B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}Υ_{p}}

(4.9) (4.10)

in the second and third conjunctions in (8) are replaced by

Υ_{i} = \{Υ_{i}β : ( \begin{matrix}Υ_{i}β & ∈ & H_{i} \\ B̃_{i}β & ⊆ & ⋃_{p∈Π_{P}}Υ_{p} \end{matrix} )\}

/\_{W ∈ var(R_{i})} W = \{W β : ( \begin{matrix}Υ_{i}β & ∈ & H_{i} \\ B̃_{i}β & ⊆ & ⋃_{p∈Π_{P}}Υ_{p} \end{matrix} )\}

(4.11) (4.12)

in (9). Let I be a model of (8). We now show that I models (9), and we proceed by case analysis.

First assume that ∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}I(Υ_{p})). In this case, the r.h.s. of (4.9)

and (4.11) respectively reduce to {t : t ∈ H_{i}} and {Υ_{i}β : (Υ_{i}β ∈ H_{i})} when interpreted by I. Thus I maps both the r.h.s. of (4.9) and (4.11) into I(H_{i}). Before considering (4.10) and (4.12), we note that since I models (4.10), it maps var(R_{i}) into nonempty sets and this, in turn, implies that I(H_{i}) is nonempty. Now consider the equation in (4.10) corresponding to a variable V ∈ var(R_{i}), and consider all the substitutions θ satisfying the condition in the r.h.s. of the equation. Since Υ_{i} ∉ var(R_{i}), we can define a substitution β corresponding to each substitution θ by extending θ so that Υ_{i}β ∈ I(H_{i}). Thus β satisfies the condition in the r.h.s. of the equation corresponding to V in (4.12). Conversely, any β satisfying (4.12) can be used as a θ in (4.10). It then easily follows that I maps the r.h.s of the equation for V in both (4.10) and (4.12) to the same set. Hence I models (4.11) and (4.12).

The alternative case, that ¬∃θ (B̃_{i}θ ⊆ ⋃_{p∈Π_{P}}I(Υ_{p})), is easy. The r.h.s. of

(4.9), (4.10), (4.11) and (4.12) are each mapped into ◯̸, and so I models (4.11) and (4.12).

Thus a model of (8) is also a model of (9). The converse proof is essentially similar and hence omitted. Hence the models of (8) are precisely the models of

Proposition (10) is essentially a restatement of (9) in such a way that the atoms in B̃_{i} are mentioned explicitly. Note that the extra condition Zβ ∈ ⊤_{t} is vacuous in the sense that it satisfied by any β. Proposition (11) is simply a restatement of (10) using the notation D_{P}^{i} introduced above for a set of pairs. Thus propositions (9) through (11) are mutually equivalent.

To see that proposition (12) is equivalent to (11), we note that the only difference between them is that in each equation in (11), the expression of the form

{W θ : ⋀_{(a,sexp)∈D_{P}^{i}} aθ ∈ sexp}  (4.13)

is replaced by the expression in (12):

{x : ∃y_{1}y_{2} ⋯ y_{m} ( ⋀_{(a,sexp)∈D_{P}^{i}} aμ ∈ sexp)} (4.14)

where var(R̃_{i}) = {W, Y_{1}, ⋯, Y_{m}}, x, y_{1}, ⋯, y_{m} are new variables, and μ denotes the renaming substitution [W/x, Y_{1}/y_{1}, ⋯, Y_{m}/y_{m}]. Let I′ be an interpretation of (4.13) and let g be an arbitrary element in I′(4.13). Therefore g = W θ, for some substitution θ = [W/g, Y_{1}/t_{1}, ⋯, Y_{m}/t_{m}, ⋯] which grounds {W, Y_{1}, ⋯, Y_{m}}, and aθ ∈ I(sexp) for each (a, sexp) ∈ D_{P}^{i}. Clearly g is in I′(4.14) because the assignment of the values g, t_{1}, ⋯, t_{m} to the variables x, y_{1}y_{2} ⋯ y_{m} satisfies aμ ∈ I(sexp), for each (a, sexp) ∈ D_{P}^{i}. The converse case is proved similarly by constructing an appropriate θ given an assignment of values to the variables x, y_{1}, ⋯, y_{m}. Hence proposition (12) is equivalent to (11).

The formula (13) is, by definition, the formula in (12). Summarizing all the above arguments, we have

• propositions (1) through (6) are mutually equivalent;

• a subset I of HB_{P} satisfies (6) iff there is model I′ of (7) such that I′(Υ_{p}) = I|_{p} for all p ∈ Π_{P};

• I′ models (7) iff there is a model I′′ of (8) such that I′′(Υ_{p}) = I′(Υ_{p}) for all p ∈ Π_{P};

• the models of (8) are precisely the models of (9); and

\underline{Section 5: A Simplification Algorithm for Set Equations} 23

• propositions (9) through (13) are essentially restatements of one another;

and so Main lemma 1 is proved.

In what follows, the problem at hand is an algorithm to construct the least model of the set formula C_{P} ∧ F(D̃_{P}) corresponding to a program P. The following corollary of the above lemma, whose proof is immediate, guarantees that this least model is, in essence, τ_{P} ↑ω.

Corollary 1 Let P be a logic program, and let I be the least model of the set formula C_{P} ∧ F(D̃_{P}) corresponding to P. Then

⋃_{p∈Π_{P}} I(Υ_{p}) = τ_{P} ↑ω.

5 A Simplification Algorithm for Set Equations

We shall deal with formulas of the form F \binom{}{D̃} in the next section. In this section, we present an algorithm which deals with collections of set equations C. This algorithm implements the function SIMP LIF Y (C) which transforms C into an equivalent collection written in a canonical “solved” form. The most important property of this form is that properties of its least model can be easily verified.

5.1 Normal Form, Solved Form and Explicit Form

This subsection contains the definitions of the input and output forms for the SIMP LIF Y algorithm. We begin with some preliminary notations and definitions.

Let C be the collection^{8} of equations {X_{1} = exp_{1}, ⋯, X_{n} = exp_{n}} such that exp_{1}, ⋯, exp_{n} are arbitrary expressions and X_{1}, ⋯, X_{n} are distinct variables called the solved variables. We write lhs(C) to denote the set of variables in the left-hand-sides of equations, that is the solved variables. We also write rhs(C)|_{X} to denote

• the set expression on the right-hand-side of the equation for X, if X is a solved variable in C;

8For convenience, we shall sometimes treat conjunctions such as C_{P} and F(D̃_{P}) as sets of equations.

• X itself, if X is not a solved variable in C.

An important part of the simplification algorithm described in this section involves the use of restricted forms of set equations. One restriction is on the depth of the nesting^{9} of set expressions. If t is a subexpression of a set expression sexp, then we say that this occurrence of t is nested if it occurs within the scope of a function or predicate symbol, and otherwise the occurrence is un-nested . For example in X ∪ p(X, Y) the first occurrence of X is un-nested, but the second is nested. We say that a set expression, set equation or a collection of set equations is deeply nested if it contains a nested occurrence of a non-variable term. For example f(U ∩ V) and g(U, a) are deeply nested, but X ∩ g(U, X) is not. In this section, no set equations will be deeply nested.

Another restriction relates to the occurrence of ∪ symbols inside the scope of ∩ symbols. We define

Definition 1 (DNF) An \underline{primitive} set expression is either a constant, a variable, or of the form f(t̃) where f ∈ Π_{P} ∪ Σ_{P} is n-ary and t̃ is a sequence of n primitive set expressions. A \underline{conjunction} of set expressions, or simply \underline{conjunct}, is of the form a_{1} ∩ a_{2} ∩ ⋯ ∩ a_{n} where each a_{i}, 1 ≤ i ≤ n, is an primitive set expression. A set expression is in \underline{disjunctive normal form} (or just DNF) if it is of the form sexp_{1} ∪ sexp_{2} ∪ ⋯ ∪ sexp_{n} where each sexp_{i}, 1 ≤ i ≤ n, is a conjunction of set expressions.

We note that when a set expression is not deeply nested (and this is the case in this section), it can be transformed using the usual distributive operation on ∩ over ∪ to obtain an equivalent expression in DNF. For a set expression sexp, we write DNF (sexp) to denote the corresponding DNF expression thus obtained. Clearly such a function is easily implementable. We note that this function may change the number of symbols in sexp however it preserves primitive subexpressions: an primitive expression a is a subexpression of sexp if and only if it is a subexpression of DNF (sexp). Furthermore, the DNF function does not change the meaning of an expression, that is, for any sexp and interpretation I, I(sexp) = I(DNF (sexp)). We are now in a position to define the form of the input to the SIMP LIF Y algorithm.

Definition 2 (Normal Form) A collection of set equations C is in \underline{normal form} if it is of the form X_{1} = sexp_{1}, X_{2} = sexp_{2}, ⋯, X_{n} = sexp_{n} where (a) the X_{i}, 1 ≤ i ≤ n, are distinct variables, and (b) the sexp_{i}, 1 ≤ i ≤ n, are set expressions which are in DNF and are not deeply nested.

9The term nesting is used throughout to mean encapsulation within the scope of a functor.

In what follows, we shall tacitly assume that the symbols ∪ and ∩ are associative, commutative and idempotent. Thus, for example, we may regard s ∩ (t ∩ u) and (s ∩ t) ∩ u as identical expressions.

The equations output by the SIMP LIF Y function are a restricted kind of normal form equations defined as follows:

Definition 3 (Solved Form) A collection of set equations C is in \underline{solved form} if it is in normal form, and every conjunct in rhs(C) is either (a) a constant (including ⊤ and ⊥), or (b) of the form f(Y_{1}, ⋯, Y_{n}) where f is an n-ary functor and Y_{1}, ⋯, Y_{n} are variables, or (c) a non-solved variable, or (d) of the form X ∩ sexp where X is a non-solved variable.

Where X = s_{1} ∪ ⋯ ∪ s_{n} is an equation in a solved form collection C, we write crhs(C) to denote the collection of the conjuncts in rhs(C) which fall into cases (a) and (b) above. Similarly, we define crhs(C)|_{X} to be the collection of the conjuncts in rhs(C)|_{X} which fall into cases (a) and (b) above.

Despite the above seemingly complicated definition of solved form, the main property that is required from equations C in solved form is that C can be written into a form such that the least model of C is explicitly represented:

Definition 4 (Explicit Form) A collection of set equations C is in \underline{explicit form} if it is in solved form, and every conjunct in rhs(C) is primitive and contains no non-solved variables.

Before giving the details of how a solved form collection can be rewritten into explicit form, consider some equivalent formulations of this notion of explicit form. First observe that an explicit form collection C can be considered as a cyclic termgraph representation of its least model. This graph can be informally described as follows:

• each node is labelled with a constant, functor, the symbol ∪, or a distinct variable; • each constant has no out-going edges, each n-ary functor has n out-going

edges to the nodes corresponding to its arguments, and similarly ∪ has two out-going edges; each variable has one out-going edge to the node corresponding to rhs(C)|_{X}.

Such a graph describes a model in an obvious way: every node in the graph can be interpreted as the set of ground terms which can be constructed by following paths from that node. Thus there is a set of ground terms associated to each solved variable.

Alternatively, an explicit form collection of equations can be viewed as a term grammar as follows:

for each equation X = t_{1} ∪… ∪ t_{n} in C, construct the productions X ⟹ t_{1}, …, X ⟹ t_{n}.

Such productions, in turn, can be viewed as a description of a non-deterministic tree automaton (see, for example, [4]). Hence standard algorithms can be applied to determine questions such as membership, inclusion and emptyness.

It can easily be proved that given an explicit form collection C, we can construct a term graph, a term grammar and a tree automaton, all of which describe the least model of C. It can also be proved that C has only one model. Summarizing, the essential property of an explicit form collection is that it is an unambiguous and explicit description of a model, that is:

• C has exactly one model with respect to var(C);

• this model can be viewed as a regular set [4] of terms; thus there are algorithms to decide questions about emptiness and containment.

We conclude this subsection by showing that a solved form collection of equations can be transformed into explicit form. Formally:

Proposition 2 A collection C of set equations in solved form has a least model. Furthermore, C can rewritten into an explicit form collection such that the least model is preserved.

Proof: Define that a set expression is non-empty with respect to a set of variables V if it is either (a) a constant different from ⊥, or (b) of the form f(X_{1}, ⋯, X_{n}) where each X_{i}, 1 ≤ i ≤ n, is in V, or (c) of the form t_{1} ∪ ⋯ ∪ t_{k} where some t_{i}, 1 ≤ i ≤ k, is non-empty w.r.t. V. Otherwise a set expression is empty w.r.t V. Thus, if a sexp is non-empty w.r.t. V then I(sexp) ≠ ◯̸ whenever I(X) ≠ ◯̸ for all X ∈ V. Finally, define that a solved variable X in a solved form C is non-empty (respectively empty) w.r.t. V if rhs(C)|_{X} is non-empty (respectively empty) w.r.t. V.

Now consider the following marking algorithm whose purpose is to identify those variables in var(C) which are empty in lm(C).

let all variables in C be unmarked;

while there is a solved variable X in C such that X is unmarked, and rhs(C)|_{X} is non-empty w.r.t. the marked variables

do

mark X;

endwhile

Clearly the algorithm terminates, returning two sets M and U of marked and unmarked variables respectively. It is easy to show by induction that every variable in M is indeed non-empty in every model of C. Using the set M, we now construct an explicit form collection C_{e} whose model is lm(C).

Construct C_{e} from C as follows. For each equation X = sexp in C, delete every conjunction in sexp which is empty with respect to M. In case sexp becomes empty as a result of such deletion, the equation becomes X = ⊥. The resulting collection C_{e} is in explicit form because every conjunction in rhs(C_{e}) is non-empty w.r.t. M and hence is primitive and contains no non-solved variables.

Let I_{e} denote lm(C_{e}), and we prove that I_{e} is a model of C. Corresponding to each equation X = sexp in C_{e} is an equation in C of the form X = sexp ∪ sexp′; and vice versa. Now, for any variable Y ∈ U, either Y does not appear in C or else Y = ⊥ appears in C_{e}; thus I_{e}(Y) = ◯̸. Next, each conjunction in sexp′ is empty w.r.t. M, and so the conjunction is either ⊥ or of the form f(Y_{1}, ⋯, Y_{k}) where one of the variables Y_{1}, ⋯, Y_{k} is in U. Thus I_{e} maps the conjunction into ◯̸. This, in turn, implies that I_{e}(sexp′) = ◯̸. Since I_{e} is also a model of X = sexp in C_{e}, I_{e} models the equation X = sexp ∪ sexp′ in C. Thus I_{e} models C.

To complete the proof, it remains to show that I_{e} = lm(C). Observe that for each variable X, if X ∈ lhs(C_{e}) then rhs(C_{e})|_{X} ⊆ rhs(C)|_{X}. We now use this fact to show by structural induction that for all terms t, for all models I of C and for all variables X, t ∈ I_{e}(X) implies t ∈ I(X). If t is a constant, say c, then

c ∈ I_{e}(X) implies c is a conjunct in rhs(C_{e})|_{X} implies c is a conjunct in rhs(C)|_{X} implies c ∈ I(X).

If t is of the form f(t_{1}, ⋯, t_{n}) then

f(t_{1}, ⋯, t_{n}) ∈ I_{e}(X) implies rhs(C_{e})|_{X} has a conjunct f(X_{1}, ⋯, X_{n}) s.t. t_{i} ∈ I_{e}(X), 1 ≤ i ≤ n implies rhs(C)|_{X} has a conjunct f(X_{1}, ⋯, X_{n}) s.t. t_{i} ∈ I(X), 1 ≤ i ≤ n implies f(t_{1}, ⋯, t_{n}) ∈ I(X)

Example 1 If C were ( \begin{matrix}X = f(Y) ∪ a \\ Y = g(X) ∪ (h(X) ∩ Z) \end{matrix} ) then C_{e} is ( \begin{matrix}X = f(Y) ∪ a \\ Y = g(X) \end{matrix} ).

A term graph corresponding to C_{e} can be constructed as follows:

[figure: f; a; g; ∪; Y; X]

We can also construct a term grammar and a frontier to root tree automaton (with start state q_{0}) corresponding to C_{e} as follows:

\begin{aligned}X & ⟹ & f(Y) \\ X & ⟹ & a \\ Y & ⟹ & g(X) \end{aligned}  \begin{matrix}q_{Y} & ⟶^{f} & q_{X} \\ q_{0} & ⟶^{a} & q_{X} \\ q_{X} & ⟶^{g} & q_{Y} \end{matrix}

The least model of C described by all the above is:

\begin{aligned}X & = & \{a, fg(a), ⋯ (fg)^{n}(a), ⋯\}. \\ Y & = & \{g(a), gfg(a), ⋯ (gf)^{n}g(a), ⋯\}. \end{aligned}

5.2 SIMPLIFY

Consider the following group of five transformation steps on a normal form collection C of set equations.

Transformation 1 (C-Substitute) If C contains two distinct equations X = sexp and Y = t such that sexp contains an un-nested occurrence of the variable Y, then replace the first equation by X = DNF (sexp′) where sexp′ is the result of replacing the occurrence of Y in sexp by t. We say that a C-substitution transformation \underline{using} Y was applied to C to obtain C′.

Transformation 2 (Cycle-Removal) If C contains the equation X = sexp, such that sexp contains an un-nested occurrence of the variable X, then replace that occurrence of X by a new variable.

Transformation 3 (Intersection Clash) If C contains an occurrence of the expression t∩s where t and s have distinct outermost functors, replace that occurrence by ⊥.

Transformation 4 (Intersection Simplification) If C contains an occurrence of the expression t ∩ ⊥ or t ∩⊤, then replace that occurrence by ⊥ or t respectively.

Transformation 5 (Intersection Distribution) If C contains an occurrence of the expression f(X_{1}, ⋯, X_{n})∩f(Y_{1}, ⋯, Y_{n}), and if there exist variables Z_{i}, 1 ≤ i ≤ n, such that C ⊧ Z_{i} = X_{i} ∩ Y_{i}, then replace that occurrence by f(Z_{1}, ⋯, Z_{n}).

The first two transformations implement a restricted form of substitution whose purpose is to remove all un-nested occurrences of solved variables on the righthand-sides of equations. The remaining three transformations perform obvious simplifications involving the ∩ symbol. We note that all five of the transformations preserve normal form, that is, the application of a transformation to a collection in normal form results in another collection in normal form. We now prove that the above transformations are correct in the sense that they preserve equivalence between the input and output collections of set equations. These proofs are straightforward. The exception is the proof for cycle-removal transformation where the transformation itself is somewhat surprising.

Lemma 1 (Correctness of Transformations 1 thru 5) Let C′ be obtained from C by using transformation 1, 2, 3, 4 or 5. Then

C ⟺_{var(C)} C′.

Proof for Transformations 1. Straightforward and hence omitted.

Proof for Transformation 2. The only difference between C and C′ is that the former contains an equation of the form X = (X ∩ sexp_{1}) ∪ sexp_{2} while the latter contains X = (Z ∩ sexp_{1}) ∪ sexp_{2} where Z is a new variable.

Now, given any model I of C, we can modify I to obtain a model I′ of C′ by changing the assignment for the variable Z so that I′(Z) = I(X). Clearly I and I′ agree on var(C). Hence we have proved that if I is a model of C then there exists a model I′ of C′ such that I =_{var(C)} I′.

To prove the converse (and complete the proof from transformation 2), we show that any model of C′ satisfies C. Let I′ be a model of C′. Hence I′ satisfies

I′(X) = (I′(Z) ∩ I′(sexp_{1})) ∪ I′(sexp_{2})

To show that I′ satisfies C, it suffices to show that I′ satisfies X = (X ∩ sexp_{1}) ∪ sexp_{2}, or equivalently, that I′ satisfies

I′(X) = (I′(X) ∩ I′(sexp_{1})) ∪ I′(sexp_{2})

To show this, first choose an arbitrary g ∈ I′(X), and consider the following chain of reasoning:

g ∈ I′(X) implies
g ∈ (I′(Z) ∩ I′(sexp_{1})) ∪ I′(sexp_{2}) and g ∈ I′(X) implies
g ∈ I′(sexp_{1}) ∪ I′(sexp_{2}) and g ∈ I′(X) implies
g ∈ (I′(X) ∩ I′(sexp_{1})) ∪ I′(sexp_{2}).

This proves that I′(X) ⊆ (I′(X) ∩ I′(sexp_{1})) ∪ I′(sexp_{2}). To show the converse, choose an arbitrary g ∈ (I′(X) ∩ I′(sexp_{1})) ∪ I′(sexp_{2}) and we have:

g ∈ (I′(X) ∩ I′(sexp_{1})) ∪ I′(sexp_{2}) implies
g ∈ I′(X) or g ∈ I′(sexp_{2}) implies

g ∈ (I′(Z) ∩ I′(sexp_{1})) ∪ I′(sexp_{2}) or g ∈ I′(sexp_{2}) implies

g ∈ (I′(Z) ∩ I′(sexp_{1})) ∪ I′(sexp_{2}) implies
g ∈ I′(X).

Hence I′ is a model of C and the proof is finished.

Proof for Transformations 3 and 4. The proof is straightforward from the observation that for any interpretation I of C, and for any set expressions t and s, (a) I(t ∩ s) = ◯̸ if t and s have different outermost functors, (b) I(t∩ ⊥) = ◯̸, and finally, (c) I(t ∩ ⊤) = I(t).

Proof for Transformation 5. The proof is straightforward from the observation that for any model I of C, I(f(X_{1}, ⋯, X_{n}) ∩ f(Y_{1}, ⋯, Y_{n})) is equal to I(f(X_{1} ∩ Y_{1}, ⋯, X_{n} ∩ Y_{n})) and by the hypothesis C ⊧ Z_{i} = X_{i} ∩ Y_{i}, this is equal to I(f(Z_{1}, ⋯, Z_{n})).

We present the SIMP LIF Y algorithm in figure 1. It is essentially an exhaustive application of the above transformations. Just above, we have argued that the transformations are correct in the sense that they preserve equivalence between the input and output collections of equations. To ensure that the final output is solved form, however, we require that transformation 5 above is, in fact, applicable whenever there exists a subexpression of the form f(X_{1}, ⋯, X_{n}) ∩ f(Y_{1}, ⋯, Y_{n}) in C. Toward this end, new variables may have to be introduced before transformation 5 is applied. However, the number of new variables introduced can be bounded by 2^{|V|} where V is the set of variables in the collection of set equations C just after the execution of line 3. This is because, after execution of line 3, the algorithm will only be dealing with variables of the form V_{S} where S ⊆ V. Intuitively, we start off by having a variable V_{{X}} corresponding to each variable X in the input equations. Whenever new variables are introduced, they will be of the form V_{{X_{1},···,X_{n}}} and their intended meaning is ∩V_{{X_{i}}} over 1 ≤ i ≤ n. The essential benefit in such a variable naming scheme is that the one variable can capture the meaning of several expressions. For example, V_{{X,Y,Z}} represents not just V_{{X}} ∩ V_{{Y }} ∩ V_{{Z}}, but also V_{{X,Y }} ∩ V_{{Z}} and V_{{X}} ∩ V_{{Y,Z}} ∩ V_{{Y }} ∩ V_{{X}} etc.

Lemma 2 Let C denote a normal form collection of set equations. Then the SIMP LIF Y algorithm, when input with C,

• terminates, and outputs a collection C_{s} of set equations;

• C_{s} is in solved form, and

• C ⟺_{var(C)} C_{s}.

input a collection C of set equations in normal form;

1. for each solved variable X in C do

2. exhaustively-apply transformation 2 to C;

3. exhaustively-apply transformation 1 using X to C; endfor

4. rename each variable X in C into V_{{X}};

5. repeat

6. exhaustively-apply transformations 3 and 4 to C;

7. if C contains a subexpression of the form f(V_{S_{1}}, V_{S_{2}}, ⋯, V_{S_{n}}) ∩ f(V_{T_{1}}, V_{T_{2}}, ⋯, V_{T_{n}})

8. then replace the above subexpression by f(V_{S_{1}∪T_{1}}, ⋯, V_{S_{n}∪T_{n}});

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

10. if V_{S_{i}∪T_{i}} is a non-solved variable then

11. add to C the set equation

V_{S_{i}∪T_{i}} = DNF (rhs(C)|_{V_{S_{i}}} ∩ rhs(C)|_{V_{T_{i}}}); endif

endfor endif

12. until none of transformations 3, 4 and 5 is applicable to C; rename each variable V_{{X}} in C into X; output C;

Figure 1: SIMPLIFY Proof: We first prove termination. The termination of the for-loop at line 1 is proven as follows. Firstly, transformation 2 cannot be repeated infinitely because each application removes one occurrence of a solved variable from C and does not introduce new solved variables. Next, each application of transformation 1 using a solved variable X removes one un-nested occurrence of X from the right-hand-sides in C. (This is guaranteed from the fact that transformation 2 has already been applied to C and so rhs(C)|_{X} does not contain any un-nested occurrences of X.) Therefore, the exhaustive application of transformation 1 using X terminates. Finally, that the for-loop on line 1 terminates, follows from the fact that neither transformation 1 nor 2 introduce new solved variables.

That line 4 terminates is clear. We now show that the repeat-loop at line 5 terminates.

• The step at line 6 clearly terminates because both transformations 3 and 4 diminish the size of expressions in C.

• The step at line 7 may enlarge the collection C with new equations. However, the total number of equations which can be added (line 11) is bounded by 2^{k}, where k is the number of variables in C on entry to the repeat-loop at line 5. Since transformation 5 diminishes the size of expressions in C, the loop at line 5 terminates.

Next we observe that the following loop invariant holds: at the end of each iteration of the repeat-loop, (a) C is in normal form and (b) all solved variables X appearing on the right-hand-sides of C are nested.

Clearly (a) holds just before execution of the for-loop at line 2, and it continues to hold throughout execution of this loop. Consider then property (b). Each iteration of the for-loop with respect to a solved variable X concludes with an exhaustive C-substitution for un-nested occurrences of X. Therefore, there are no un-nested occurrences of X in rhs(C) after this iteration. This, in turn, implies that further applications of transformations 1 or 2 (in other iterations of the for-loop) will not introduce any un-nested occurrences of X in rhs(C). Since the for-loop iterates over all the solved variables in C (and these variables are fixed throughout the for-loop), (b) holds after execution of the for-loop. Therefore, both properties (a) and (b) hold just before execution of the repeat-loop.

For the inductive step, we now show that these properties hold after an iteration of the repeat-loop. The step at line 6 does not violate the properties because transformations 3 and 4 only serve to delete subexpressions. The step at line 7 first applies transformation 5, and then may make V_{S_{i}∪T_{i}} into a solved variable by the addition of a new equation V_{S_{i}∪T_{i}} = DNF (rhs(C)|_{V_{S_{i}}} ∩ rhs(C)|_{V_{T_{i}}}). That (a) is not violated by this addition is clear. That (b) is not violated by this addition is an easy consequence of the fact that both rhs(C)|_{V_{S_{i}}} and rhs(C)|_{V_{T_{i}}} satisfy (b), and that the DNF operation does not alter nesting of terms (it only deals with distributing ∩ symbols over ∪ symbols). Thus the invariant holds at the end of each iteration of the repeat-loop.

That C_{s} is in solved form is now an easy consequence of the above invariant and the fact that none of transformations 3, 4 and 5 are applicable to C_{s}.

The remainder of the proof, that C ⟺_{var(C)} C_{s}, essentially follows from lemma 1. The only operation within SIMP LIF Y which is not directly stated as a transformation application is the if statement at line 7. This statement is in essence an application of transformation 5. To show that lemma 1 can be used, we now prove another invariant of the main loop: at the end of each iteration of the repeat-loop, each variable V_{{X_{1},···,X_{n}}} in C, n ≥ 1, is such that V_{S} = V_{{X_{1}}} ∩ ⋯ ∩ V_{{X_{n}}} holds in all models of C. This invariant clearly holds initially because all variables in C are of the form V_{{X}} where X ∈ V.

Now consider the inductive step. Clearly step 10 is the only step which may affect the invariant since it is the only step which introduces a new solved variable V_{S_{i}∪T_{i}} to C. Let S_{i} be {U_{1}, ⋯, U_{k}} and let T_{i} be {W_{1}, ⋯, W_{l}}. Since the invariant holds before the introduction of V_{S_{i}∪T_{i}}, V_{S_{i}} = V_{{U_{1}}} ∩ ⋯ ∩ V_{{U_{k}}} and V_{T_{i}} = V_{{W_{1}}} ∩ ⋯ ∩ V_{{W_{l}}} are satisfied in all models of C. Hence we have, in all models of C, that

V_{S_{i}∪T_{i}} = DNF (rhs(C)|_{V_{S_{i}}} ∩ rhs(C)_{V_{T_{i}}}), by construction;
= rhs(C)|_{V_{S_{i}}} ∩ rhs(C)|_{V_{T_{i}}}, since DNF preserves equivalence;
= V_{S_{i}} ∩ V_{T_{i}},
= V_{{U_{1}}} ∩ ⋯ ∩ V_{{U_{k}}} ∩ V_{{W_{1}}} ∩ ⋯ ∩ V_{{W_{l}}}, by induction hypothesis;
= V_{{X_{1}}} ∩ ⋯ ∩ V_{{X_{n}}}

where {X_{1}, ⋯, X_{n}} is {U_{1}, ⋯, U_{k}} ∪ {W_{1}, ⋯, W_{l}}. Thus the invariant holds.

Upon termination of the algorithm, this invariant and lemma 1 easily imply the desired result that C ⟺_{var(C)} C_{s}.

Corollary 2 Let C denote a normal form collection of set equations input to the SIMP LIF Y algorithm, and let SIMP LIF Y (C) denote the output. Then

• lhs(SIMP LIF Y (C)) ⊇ lhs(C) and

\underline{Section 6: The Main Result} 35

• any model of SIMP LIF Y (C) is a model of C.

6 The Main Result

Recall that in section 4, we defined, corresponding to a given program P, a formula consisting of solved form collection C_{P} of set equations, and a formula F(D̃_{P}) where D̃_{P} is a family of collections of pairs. We now present the algorithm which inputs such C_{P} and D̃_{P}, preprocesses these expressions to obtain C^{(0)} and D̃^{(0)}, and then performs a finite number of reduction steps

C^{(0)}, D̃^{(0)} ⟹ C^{(1)}, D̃^{(1)} ⟹ ⋯ ⟹ C^{(i)}, D̃^{(i)} ⟹ ⋯ ⟹ C^{(n)}, D̃^{(n)} (6.15)

to finally obtain a collection of solved form set equations C^{(n)} such that the least model of C^{(n)} is the same as the least model of the formula C_{P} ∧ F(D̃_{P}). The essence of the algorithm is that it progressively transfers information about the least model we seek from D̃^{(i)} to C^{(i)}. In the final step, therefore, C^{(n)} ∧ F(D̃^{(n)}) will be such that all the desired information will be in C^{(n)}.

The subsections below are organized as follows. In section 6.1, the main body of the algorithm which performs the reductions (6.15) is defined. Termination and correctness properties of the reductions are then established in sections 6.2 and 6.3 respectively. Finally, in section 6.4, we present a preprocessing algorithm which, when given C_{P} and D̃_{P} corresponding to a logic program P, outputs equivalent expressions C^{(0)} and D̃^{(0)} which may then be input to the main algorithm.

6.1 Description of Main Algorithm

We now describe the body of the main algorithm which starts with a collection of set equations C and a family of collections of pairs D̃ which satisfy certain initial conditions. Before formally stating these initial conditions, define that a collection of quantified equations F(D̃) is in normal form if it is of the form X_{1} = qexp_{1}, ⋯, X_{n} = qexp_{n} where the X_{i}, 1 ≤ i ≤ n, are distinct variables, and the r.h.s. of each pair in D̃ is not deeply nested. We also define that a collection E of set and quantified equations is in normal form if the collection of set equations in E is in normal form, the collection of quantified equations in E is in normal form, and no two equations in E have the same variable in the l.h.s. The initial conditions on C and D̃ can now be stated as:

Main Algorithm Precondition:

• C is in solved form, and

• C ∪ F(D̃) is in normal form.

The basis of this algorithm, as for the SIMP LIF Y algorithm described previously, is a group of transformations. Each transformation takes as input expressions C and D̃ described above, and outputs two items: (a) a new family D̃′ of collections of pairs, and (b) a collection δ of set equations in normal form. If a transformation is applied on C and D̃ to obtain δ and D̃′, we write

C, D̃ ⟹ D̃′, δ

and we say that a transformation is applied on D̃ in the context of C to obtain the the new family D̃′ and an extracted collection δ of set equations.

Transformation 6 (D-Substitution) If D̃ contains an un-nested occurrence of a C-solved variable Y in the r.h.s. of a pair, then replace the occurrence by rhs(C)|_{Y}. Output the resulting D̃, and δ = ◯̸.

Transformation 7 (Clash) If D_{j} ∈ D̃ contains a pair (f(s_{1}, ⋯, s_{n}), g(t_{1}, ⋯, t_{m})), where f ≠ g, or a pair (s, ⊥), then output D̃ − {D_{j}} and δ = {Y_{1} =⊥, ⋯, Y_{k} =⊥} where Y_{1}, ⋯, Y_{k} are the variables in the left-hand-sides of D_{j}.

Transformation 8 (Cancellation) If D̃ contains a pair (f(s_{1}, ⋯, s_{n}), f(t_{1}, ⋯, t_{n})), then replace the pair by the pairs (s_{1}, t_{1}), ⋯, (s_{n}, t_{n}). Output the resulting D̃ and δ = ◯̸.

The next transformation step is conditional on a relation NONEMP T Y which is defined as follows. Where C is a solved form collection of set equations and sexp is a set expression, NONEMP T Y (C, sexp) is true iff C ⊧ sexp ≠ ◯̸. Clearly NONEMP T Y (C, sexp) is equivalent to

NONEMP T Y (SIMP LIF Y (C ∪ {X = sexp}), X)

where X is a new variable. Thus the problem of implementing the function NONEMP T Y can be reduced to the problem of determining if a given variable is always non-empty in a given solved form. The proof of proposition 2 contains such an implementation: NONEMP T Y (C, X) iff X is marked non-empty after applying the marking algorithm to the collection SIMP LIF Y (C ∪ {X = sexp}).

Transformation 9 (Compaction) If D_{j} ∈ D̃ is of the form (X̃, Φ̃) and NONEMP T Y (C, ∩(Φ̃|_{Y_{1}})) ∧ ⋯ ∧ NONEMP T Y (C, ∩(Φ̃|_{Y_{k}})) where

• the notation X̃ denotes a sequence of variables (that is, the l.h.s. of each pair in D_{j} is a variable), and the variables in this sequence are Y_{1}, ⋯, Y_{k};

• the notation ∩(Φ̃|_{Y_{l}}), 1 ≤ l ≤ k, denotes the set expression ϕ_{1} ∩ ⋯ ∩ ϕ_{m} such that (Y_{l}, ϕ_{1}), ⋯, (Y_{l}, ϕ_{m}) are the pairs in D_{j} of the form (Y,_{l} ϕ)

then output D̃ − {D_{j}} and δ = {Y_{1} = DNF (∩(Φ̃|_{Y_{1}})), ⋯, Y_{k} = DNF (∩(Φ̃|_{Y_{k}}))}.

Example 2 Let C contain U = a and V = a, and let D_{j} be {(X, f(U)), (Y, g(V)), (X, f(V))}. Since NONEMP T Y (C, f(U) ∩ f(V)) ∧ NONEMP T Y (C, g(V)) is true, the compaction transformation deletes D_{j} and outputs δ = {X = f(U) ∩ f(V), Y = g(V)}. Note that F(D_{j}):

\begin{aligned}X & = & \{x : ∃y ( \begin{matrix}x & ∈ & f(U) \\ y & ∈ & g(V) \\ x & ∈ & f(V) \end{matrix} )\} \\ Y & = & \{y : ∃x ( \begin{matrix}x & ∈ & f(U) \\ y & ∈ & g(V) \\ x & ∈ & f(V) \end{matrix} )\} \end{aligned}

is equivalent to δ in all interpretations where f(U) ∩ f(V) and g(V) are nonempty (as is the case here in all models of C).

Transformation 10 (Union) If D_{j} ∈ D̃ is of the form {(s, t_{1} ∪ t_{2}), (Ψ̃, Φ̃)} then

• let Y_{1}, ⋯, Y_{k} be the variables in s and Ψ̃;

• let Y′_{1}, ⋯, Y′_{k}, Y′′_{1}, ⋯, Y′′_{k} be distinct new variables and let η_{1} and η_{2} denote the renaming substitutions [Y_{1}/Y′_{1}, ⋯, Y_{k}/Y′_{k}] and [Y_{1}/Y′′_{1}, ⋯, Y_{k}/Y′′_{k}];

• let D̃′ be D̃ − {D_{j}} ∪ {D′_{j}, D′′_{j}} where D′_{j} = {(sη_{1}, t_{1}), (Ψ̃η_{1}, Φ̃)} and D′′_{j} = {(sη_{2}, t_{2}), (Ψ̃η_{2}, Φ̃)}, and

• let δ be {Y_{1} = Y′_{1} ∪ Y′′_{1}, ⋯, Y_{k} = Y′_{k} ∪ Y′′_{k}};

and output D̃′ and δ.

Example 3 Suppose that D_{j} consists of the single pair (p(X), p(U)∪q(V)). Then the union transformation replaces D_{j} by two collections D′_{j} = {(p(X′), p(U))} and D′′_{j} = {(p(X′′), q(V))}, where X′ and X′′ are new variables. The equation in δ is X = X′ ∪ X′′. Note that F(D_{j}):

X = {x : p(x) ∈ p(U) ∪ q(V)}

is essentially equivalent to F(D′_{j}) ∧ F(D′′_{j}) ∧ δ:

\begin{aligned}X & = & X′ ∪ X′′ \\ X′ & = & \{x′ : p(x′) ∈ p(U)\} \\ X′′ & = & \{x′′ : p(x′′) ∈ p(U)\} \end{aligned}

Transformation 11 (Intersection) If D_{j} ∈ D̃ contains a pair (s, t_{1} ∩ t_{2}), then replace that pair by the two pairs (s, t_{1}), (s, t_{2}). Output the resulting D̃ and δ = ◯̸.

Whenever one of the above transformations is applied on D̃ in the context of C to obtain δ and D̃′, we may write C, D̃ ⟹_{tf} D̃, δ to indicate by tf the particular

transformation used. We say that D̃ is closed under a transformation if that transformation is not applicable to D̃.

We are now in a position to define, in figure 2, the reduction step of our algorithm. This step is described in the form of a function whose essential operation is an exhaustive application of the above transformations in the context of a fixed collection C of set constraints. For the sake of simpler proofs, however, the order in which transformations may be applied is restricted.

Our main algorithm can now be described in figure 3. We conclude this subsection by proving two properties of the algorithm. The first ensures that the SIMP LIF Y function is only applied to normal form set equations, and the second implies that a key correctness condition specified later in this section is well defined.

Proposition 3 (Main Loop Invariant) Let C^{(0)} and D̃^{(0)}, satisfying the main algorithm precondition, be input to the main algorithm. Then:

(a) just before every execution of SIMP LIF Y, C^{(i)} ∪ Δ^{(i+1)} ∪ F(D̃^{(i+1)}) is in normal form, and \underline{Section 6: The Main Result} 39

function REDUCE(C, D̃) {

Δ := ◯̸; 1 . repeat { 2 . while (the D-substitution transformation is applicable to C, D̃) do {

C, D̃ ⟹_{subs} D̃, δ

Δ := Δ ∪ δ;

}

3 . while (the union or intersection transformation is applicable to C, D̃) do {

C, D̃ ⟹_{union} D̃, δ or

C, D̃ ⟹_{intersect} D̃, δ accordingly;

Δ := Δ ∪ δ;

}

4 . while (the cancel or clash transformation is applicable to C, D̃) do {

C, D̃ ⟹_{cancel} D̃, δ or

C, D̃ ⟹_{clash} D̃, δ accordingly; Δ := Δ ∪ δ;

}

5 . while (the compaction transformation is applicable to C, D̃) do {

C, D̃ ⟹_{compact} D̃, δ

Δ := Δ ∪ δ;

}

} until (none of transformations 6–11 is applicable to C, D̃); 6 . return (D̃, Δ); }

Figure 2: REDUCE

input C^{(0)} and D̃^{(0)};

1. V^{⋆} := var(C^{(0)}) ∪ {V_{{X_{1},···,X_{k}}} : X_{i} ∈ var(C^{(0)}), 1 ≤ i ≤ k, k ≥ 2}^{a}; i := 0;

2. repeat {

3. (D̃^{(i+1)}, Δ^{(i+1)}) := REDUCE(C^{(i)}, D̃^{(i)});

4. C^{(i+1)} := SIMP LIF Y (C^{(i)} ∪ Δ^{(i+1)});

5. i := i + 1;

6. } until (crhs(C^{(i+1)})|_{X} = crhs(C^{(i)})|_{X} for all X ∈ V^{⋆}); output C^{(i)};

Figure 3: Main Algorithm

aThese are variables that SIMP LIF Y may introduce.

(b) just after every execution of the main loop, Δ^{(1)} ∪… ∪ Δ^{(i)} ∪ F(D̃^{(i)}) is in normal form.

Proof: The essence of the proof is in the following property about a single application of one of the transformations that make up REDUCE :

if C ∪ F(D̃) is in normal form and C, D̃ ⟹_{tf} D̃′, δ then

• C ∪ δ ∪ F(D̃′) is in normal form;

• lhs(δ) ⊆ lhs(F(D̃)), and

• for all X ∈ lhs(F(D̃′)), either X ∈ lhs(F(D̃)) or X is a new variable.

An easy induction argument using the above property then proves the following property about REDUCE as a whole:

if C ∪ F(D̃) is in normal form and (D̃′, δ) = REDUCE(C, D̃) then C ∪ Δ ∪ F(D̃′) is in normal form.

We now prove prove (a), that is the following holds just after the execution of line 3 in any iteration:

C^{(i)} ∪ Δ^{(i+1)} ∪ F(D̃^{(i+1)}) is in normal form. (6.16)

In the first iteration, C^{(0)}∪F(D̃^{(0)}) is in normal form just before the loop is executed because of the main algorithm precondition. By the above property of REDUCE, C^{(0)} ∪ Δ^{(1)} ∪ F(D̃^{(1)}) is in normal form just after line 3 is executed.

Now consider the n + 1^{th} iteration; thus i is n. Assume that (6.16) holds just after line 3 is executed. Thus after line 4 is executed, C^{(i+1)} ∪ F(D̃^{(i+1)}) is in normal form because C^{(i+1)} is in solved form and any variable in the l.h.s. of SIMP LIF Y (C^{(i)} ∪ Δ^{(i+1)}) is either a variable from lhs(C^{(i)} ∪ Δ^{(i+1)}) or a new variable. Thus after line 5 is executed, C^{(i)}∪F(D̃^{(i)}) is in normal form. This means that if there is an n + 2^{th} iteration, we can use the above property of REDUCE to show that (6.16) holds just after line 3 is executed again. Thus (a) is proved.

(b) Since (6.16) holds just after line 3 is executed, the following holds just after the subsequent execution of line 5:

C^{(i−1)} ∪ Δ^{(i)} ∪ F(D̃^{(i)}) is in normal form. (6.17)

Now, by corollary 2, SIMP LIF Y preserves solved variables in the sense that lhs(C) ⊆ lhs(C′) if C′ = SIMP LIF Y (C). Since C^{(1)} is built from C^{(0)} and Δ^{(1)}, C^{(2)} is built from C^{(1)} and Δ^{(2)}, …, it follows that lhs(Δ^{(1)}) ∪ … ∪ lhs(Δ^{(i)}) ⊆ lhs(C^{(i)}) and lhs(Δ^{(1)}), …, lhs(Δ^{(i)}) are mutually disjoint. This, (6.17), and the previously proven fact (a) that Δ^{(1)}, …, Δ^{(i)} are each in normal form, proves (b).

6.2 Termination

We prove, in two main parts, that REDUCE(C, D̃) terminates.

Lemma 3 (Termination of REDUCE)

(a) Each of the four while-loops terminates.

(b) The main repeat-loop terminates.

Proof: First consider the while-loop at line 2 which consists of applications of the D-substitution transformation. Since C is in solved form, each application of this transformation reduces the number of occurrences of un-nested C-solved variables in D̃. Thus this loop terminates.

Second, consider the while-loop at line 3 which consists of applications of the union and intersection transformations. Define #(D_{j}) where D_{j} is a collection of pairs, to be 3^{d} where d is the number of ∪ and ∩ symbols in D_{j}. Define ∇(D̃) to be

∑_{D_{j}∈D̃} #(D_{j}).

In the case that an intersection transformation is applied, the only change is that a collection of pairs D_{j} is replaced by another collection D′_{j} which has one less ∩ symbol. It follows that #(D′_{j}) < #(D_{j}). In the case than a union transformation is applied, the only change is that a collection of pairs D_{j}, with say d ∪ and ∩ symbols, is replaced by two collections D′_{j} and D′′_{j}, each of which has d − 1 ∪ and ∩ symbols. We thus have

#(D′_{j}) + #(D′′_{j}) = 3^{d−1} + 3^{d−1} < 3^{d} = #(D_{j})

and so, in the case of either transformation, ∇(D̃) strictly decreases. Termination of the step at line 3 is proved.

Third, consider the while-loop at line 4 which consists of applications of the clash and cancel transformations. Consider the total number of symbols appearing on the left hand sides of pairs in D̃. Since both the clash and cancel transformations strictly reduce this number, the termination of the step at line 4 is immediate.

Fourth, consider the while-loop at line 5 which consists of applications of the compaction transformation. Since each such application reduces the number of collections in D̃ by one, the termination of the step at line 5 is immediate.

Finally, we consider part (b) and prove that the main loop in step 1 terminates. Let depth(t) denote the maximum level of nesting within the term t; let depth(p), where p is a pair (a, sexp), be

\{ \begin{matrix}0 & if sexp is a variable, but not a C-solved variable; \\ depth(a) & otherwise. \end{matrix}

Let the metric ∇(D̃) be the largest depth of a pair in D̃. Suppose that one iteration of the main repeat-loop is executed upon the family D̃. Let D̃_{2} denote the result of applying the step at line 2 to D̃; let D̃_{3} denote the result of applying the step at line 3 to D̃_{3}; similarly define D̃_{4} and D̃_{5}.

That no transformation increases the metric of the family to which it is applied can be easily verified. This is essentially because no transformation increases the depth of the l.h.s. of any pair, and no transformation is applicable to a pair if its r.h.s. is a non-C-solved variable. Thus:

∇(D̃) ≥ ∇(D̃_{2}) ≥ ∇(D̃_{3}) ≥ ∇(D̃_{4}) ≥ ∇(D̃_{5}).

By design, D̃_{2} is closed under D-substitution. That is, the only variables appearing un-nested in the r.h.s. of pairs in D̃_{2} are non-C-solved variables. In fact, D̃_{3} is also closed under D-substitution. This is because in a single application of a union or intersection transformation, the only variables appearing un-nested after the transformation are those which appear un-nested before the transformation. Thus D̃_{3} is closed under all three of the transformations D-substitution, union and intersection. We now consider D̃_{3} in two main cases.

(a) Suppose that D̃_{3} is closed under both the clash and cancel transformations. Then the body of the loop at line 4 will not be executed, and so D̃_{4} is D̃_{3}. Thus D̃_{4} is closed under all but the compaction transformation. Now D̃_{5} is closed under the compaction transformation by design. Since D̃_{5} is obtained from D̃_{4} simply by the deletion of collections of pairs from the latter, D̃_{5} remains closed under the other transformations. Thus D̃_{5} is closed under all transformations, and the whole algorithm terminates.

(b) Now consider the alternative case in which a clash or cancel transformation is applicable to D̃_{3}. Thus ∇(D̃_{3}), call it k, is positive. Let (ψ_{1}, ϕ_{1}), ⋯, (ψ_{m}, ϕ_{m}), m ≥ 1, be those pairs in D̃_{3} whose depth is k (these are the pairs of maximal depth in D̃_{3}). Now, for all 1 ≤ i ≤ n:

• because k ≥ 1, ψ_{i} is of the form f(t̃);

• because k ≥ 1 and D̃_{3} is closed under the D-substitution, ϕ_{i} is not a variable; because D̃_{3} is also closed under the union and intersection transformations, ϕ_{i} is primitive; thus ϕ_{i} is of the form g(s̃).

It follows that, for all 1 ≤ i ≤ n, there is an application of the clash or cancel transformation on D̃_{3} which removes the pair (ψ_{i}, ϕ_{i}), and replaces it with zero or more pairs of strictly smaller depth. Thus ∇(D̃_{4}) < ∇(D̃_{3}).

In summary, if an iteration of the main repeat loop falls into the first case (a), then this is in fact the last iteration. If the iteration falls into the latter case (b) the value of ∇(D̃) strictly decreases. Thus the algorithm terminates.

We now consider the termination of the main algorithm. Crucial to our proof is the following property which must hold at the end of every iteration of the main loop:

Proposition 4 Each nested variable appearing in the r.h.s. of a pair in D̃^{(i)}, or in the r.h.s. of an equation in C^{(i)}, is a variable from V^{⋆}.

Proof: We proceed by induction. For the base case, it is immediate that the invariant is satisfied by C^{(0)} and D̃^{(0)}.

For the inductive step, we first note that the only transformations used in the main algorithm where nested variables may be introduced are (a) the D̃-substitute transformation, (b) the C-substitute transformation of the SIMP LIF Y routine, and (c) the ∩-simplification transformation of the SIMP LIF Y routine.

Suppose that the invariant is satisfied by C and D̃. Consider the application of the transformations noted in (a), (b) and (c) above to C and D̃. Suppose that a D̃- substitute transformation is applied. The effect of this transformation is to replace an un-nested variable with the r.h.s. of the corresponding equation in C. Since the only nested variables in this expression are from V^{⋆}, the invariant continues to hold after this transformation. The case of the application of a C-substitute transformation can similarly be argued. Finally, consider an application of the ∩-simplification transformation. Here, an expression of the form f(X_{1}, ⋯, X_{n}) ∩ f(X′_{1}, ⋯, X′_{n}), where X_{i}, X′_{i} ∈ V^{⋆}, 1 ≤ i ≤ n, is replaced by an expression of the form f(Y_{1}, ⋯, Y_{n}). Further, some equations may be added to C (line 11 of SIMP LIF Y). We note that (i) by the construction of the transformation, the variables Y_{1}, ⋯, Y_{n} are chosen to be from V^{⋆}, and (ii) if some equations are added to C, then the r.h.s. of each new equation satisfies the invariant by the induction hypothesis. Thus proposition 4 is proved.

Main Lemma 2 The main algorithm terminates.

Proof: Clearly it suffices to prove that the main loop at line 2 terminates. Toward this aim, we first note that every C^{(i)}, i ≥ 0, constructed by the algorithm, is in solved form. This is an immediate from lemma 2 on the correctness of SIMP LIF Y. By proposition 4, any expression t in crhs(C^{(i)})|_{X} is of the form f(Ỹ) where Ỹ ⊆ V^{⋆}. The termination of the main algorithm now easily follows from the two facts:

• There are a finite number of distinct expressions of the form f(Ỹ) where Ỹ ⊆ V^{⋆}, and therefore the number of possibilities for the sets crhs(C^{(i)})|_{X}, X ∈ V^{⋆} is bounded.

• crhs(C^{(i)})|_{X} ⊆ crhs(C^{(i+1)})|_{X}. This is because any difference between rhs(C^{(i+1)})|_{X} and rhs(C^{(i)})|_{X} is due to the SIMP LIF Y routine, and it easy to verify that SIMP LIF Y does not delete or rewrite any conjunct of the form f(Ỹ) where Ỹ are variables.

6.3 Correctness

We next prove a series of basic facts about the transformations 6-11. In the following propositions, we will use the notation and terminology established in the definitions of the transformations. Now suppose that

C, D̃ ⟹ D̃′, δ

that is, a transformation is applied in the context of C to D̃ in order to obtain a new family D̃′ and the extracted equations δ. Then:

Proposition 5 (D-Substitution) If the D-substitution transformation is used, then the only difference between F(D̃) and F(D̃′) is that some equations Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k} in F(D̃) are replaced by some equations Y_{1} = exp′_{1}, ⋯, Y_{k} = exp′_{k} in F(D̃′) such that

for all models I of C, I(exp_{i}) = I(exp′_{i}), 1 ≤ i ≤ k.

Proof: Straightforward and hence omitted.

Proposition 6 (Clash) If the clash transformation is used, then the only difference between F(D̃) and F(D̃′) is that some equations Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k} in F(D̃) do not appear in F(D̃′). Furthermore

for all interpretations I, I(exp_{i}) = ◯̸, 1 ≤ i ≤ k.

Proof: Recall that D_{j} is the collection of pairs removed by the transformation, and let it be denoted by (Ψ̃, Φ̃). F(D̃_{j}) is therefore

/\_{1 ≤ i ≤ k} Y_{i} = {y_{i} : ∃y_{1} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} (Ψ̃μ ∈ Φ̃)}

where μ is the renaming substitution [Y_{1}/y_{1}, ⋯, Y_{k}/y_{k}]. We now show that, in all interpretations I,

I({y_{i} : ∃y_{1} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} (Ψ̃μ ∈ Φ̃)}) = ◯̸, 1 ≤ i ≤ k.

Suppose otherwise; then there must exist a ground substitution on the variables y_{1}, ⋯, y_{k}, call it θ, such that Ψ̃μθ ∈ I(Φ̃) is true. Since (f(t_{1}, ⋯, t_{n}), g(s_{1}, ⋯, s_{m})) is a pair in (Ψ̃, Φ̃), we have that f(t_{1}, ⋯, t_{n})μθ ∈ I(g(s_{1}, ⋯, s_{m})). This is clearly absurd.

Proposition 7 (Cancellation) If the cancellation transformation is used, then the only difference between F(D̃) and F(D̃′) is that some equations Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k} in F(D̃) are replaced by some equations Y_{1} = exp′_{1}, ⋯, Y_{k} = exp′_{k} in F(D̃′) such that

for all interpretations I, I(exp_{i}) = I(exp′_{i}), 1 ≤ i ≤ k.

Proof: Let D_{j} be the collection in D̃ which contained the replaced pair (f(s̃), f(t̃)) where s̃ and t̃ respectively denote s_{1}, ⋯, s_{n} and t_{1}, ⋯, t_{n}. Thus the variables in the left-hand-sides of D_{j} are the abovementioned variables Y_{1}, ⋯, Y_{k}. Let the remaining pairs in D_{j} be denoted by (Ψ̃, Φ̃). Now, the only difference between F(D̃) and F(D̃′) is that

\begin{matrix}/\_{1 ≤ i ≤ k} Y_{i} = & \{y_{i} : ∃y_{1} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} ( \begin{matrix}f(s̃)μ & ∈ & f(t̃) \\ Ψ̃μ & ∈ & Φ̃ \end{matrix} )\} \\ & where y_{1}, ⋯, y_{k} are new variables, and \\ & μ denotes [Y_{1}/y_{1}, ⋯, Y_{k}/y_{k}] ; \end{matrix} (6.18)

appears in F(D̃), whereas

\begin{matrix}/\_{1 ≤ i ≤ k} Y_{i} = & \{y_{i} : ∃y_{1} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} ( \begin{matrix}s_{1}μ & ∈ & t_{1} \\ & ⋯ \\ s_{n}μ & ∈ & t_{n} \\ Ψ̃μ & ∈ & Φ̃ \end{matrix} )\} \\ & where y_{1}, ⋯, y_{k} are new variables, and \\ & μ denotes [Y_{1}/y_{1}, ⋯, Y_{k}/y_{k}] ; \end{matrix} (6.19)

appears in F(D̃′). Let I be any interpretation and fix i, 1 ≤ i ≤ k. The r.h.s. of the i^{th} equations in (6.18) and (6.19), when interpreted by I, respectively become

\begin{aligned}S_{1} & = & \{Y_{i}θ : ( \begin{matrix}f(s̃)θ & ∈ & I(f(t̃)) \\ Ψ̃θ & ∈ & I(Φ̃) \end{matrix} )\} , \\ S_{2} & = & \{Y_{i}θ : ( \begin{matrix}s_{1}θ & ∈ & I(t_{1}) \\ & ⋯ \\ s_{n}θ & ∈ & I(t_{n}) \\ Ψ̃θ & ∈ & I(Φ̃) \end{matrix} )\} . \end{aligned}

The remainder of the proof is simply that S_{1} = S_{2}, an obvious fact.

Proposition 8 (Compaction) If the compaction transformation is used, then the only difference between F(D̃) and F(D̃′) is that some equations Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k} in F(D̃) do not appear in F(D̃′). Furthermore, δ is of the form {Y_{1} = exp′_{1}, ⋯, Y_{k} = exp′_{k}} where

for all models I of C, I(exp_{i}) = I(exp′_{i}), 1 ≤ i ≤ k.

Proof: Recall that we denote D_{j} by (X̃, Φ̃); thus var(X̃) is {Y_{1}, ⋯ Y_{k}}. Now, the only difference between F(D̃) and F(D̃′) is that

\begin{matrix}/\_{1 ≤ i ≤ k} Y_{i} = & \{y_{i} : ∃y_{1}y_{2} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} ( X̃μ ∈ Φ̃ )\} \\ & where y_{1}, y_{2}, ⋯, y_{k} are new variables, and \\ & μ denotes [Y_{1}/y_{1}, ⋯, Y_{k}/y_{k}] ; \end{matrix} (6.20)

appears in F(D̃) but not in F(D̃′). It is thus sufficient to prove that the conjunction of the extracted equations in δ

/\_{1 ≤ i ≤ k} (Y_{i} = DNF ( ⋂_{(Y_{i},ϕ)∈D_{j}} ϕ)) (6.21)

is equivalent to the conjunction (6.20). Toward this aim, first rearrange the equations in (6.20) to obtain

\begin{matrix}/\_{1 ≤ i ≤ k} Y_{i} & = & \{y_{i} : ∃y_{1}y_{2} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} ( \begin{matrix}Ỹ_{1}μ & ∈ & Φ̃|_{Y_{1}} \\ & … \\ Ỹ_{k}μ & ∈ & Φ̃|_{Y_{k}} \end{matrix} )\} \\ & & where y_{1}, y_{2}, ⋯, y_{k} are new variables, and \\ & & μ denotes [Y_{1}/y_{1}, ⋯, Y_{k}/y_{k}] ; \end{matrix} (6.22)

where (Ỹ_{i}, Φ̃|_{Y_{i}}), 1 ≤ i ≤ k, denote the pairs in D_{j} whose l.h.s. is Y_{i}. We can further rewrite (6.22) into

/\_{1 ≤ i ≤ k} Y_{i} = \{y_{i} : ( \begin{matrix}∃y_{1} & ∈ & ∩ (Φ̃|_{Y_{1}}) \\ & … \\ ∃y_{i−1} & ∈ & ∩ (Φ̃|_{Y_{i−1}}) \\ y_{i} & ∈ & ∩ (Φ̃|_{Y_{i}}) \\ ∃y_{i+1} & ∈ & ∩ (Φ̃|_{Y_{i+1}}) \\ & … \\ ∃y_{k} & ∈ & ∩ (Φ̃|_{Y_{k}}) \end{matrix} )\} (6.23)

by (a) a suitable inward movement of quantifiers, and for all 1 ≤ l ≤ k, (b) replacing Ỹ_{l}μ ∈ Φ̃|_{Y_{l}} by Y_{l}μ ∈ ∩ (Φ̃|_{Y_{l}}), and (c) replacing Y_{l}μ by y_{l}.

Since NONEMP T Y (C, ∩(Φ̃|_{Y_{1}})) ∧ ⋯ ∧ NONEMP T Y (C, ∩(Φ̃|_{Y_{k}})) is true, ∃y_{l} ∈ I (∩ (Φ̃|_{Y_{l}})), 1 ≤ l ≤ k, is true in all models I of C. Thus (6.23) reduces to

/\_{1 ≤ i ≤ k} Y_{i} = {y_{i} : ( y_{i} ∈ ∩ (Φ̃|_{Y_{i}}) )}

in all models of C. It is now immediate that this formula is equivalent to (6.21).

Proposition 9 (Union) If the union transformation is used, then the only difference between F(D̃) and F(D̃′) is that the collection of equations F(D_{j}) is replaced in F(D̃) by two collections F(D′_{j}) and F(D′′_{j}) in F(D̃′). Furthermore, where F(D_{j}) is of the form Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k},

F(D′_{j}) is of the form Y′_{1} = exp′_{1}, ⋯, Y′_{k} = exp′_{k};
F(D′′_{j}) is of the form Y′′_{1} = exp′′_{1}, ⋯, Y′′_{k} = exp′′_{k}, and
for all interpretations I, I(exp_{i}) = I(exp′_{i} ∪ exp′′_{i}), 1 ≤ i ≤ k.

Proof: The only difference between F(D̃) and F(D̃′) is that the formula

\begin{matrix}/\_{1 ≤ i ≤ k} Y_{i} & = & \{y_{i} : ∃y_{1} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} ( \begin{matrix}sμ & ∈ & t_{1} ∪ t_{2} \\ Ψ̃μ & ∈ & Φ̃ \end{matrix} )\} \\ & & where y_{1}, y_{2}, ⋯, y_{k} are new variables, and \\ & & μ denotes [Y_{1}/y_{1}, Y_{2}/y_{2}, ⋯ Y_{k}/y_{k}] ; \end{matrix} (6.24)

appears in F(D̃), whereas the following two formulas

\begin{matrix}/\_{1 ≤ i ≤ k} Y′_{i} & = & \{y′_{i} : ∃y′_{1} ⋯ y′_{i−1}y′_{i+1} ⋯ y′_{k} ( \begin{matrix}sη_{1}μ_{1} & ∈ & t_{1} \\ Ψ̃η_{1}μ_{1} & ∈ & Φ̃ \end{matrix} )\} \\ & & where y′_{1}, y′_{2}, ⋯, y′_{k} are new variables, and \\ & & μ_{1} denotes [Y′_{1}/y′_{1}, Y′_{2}/y′_{2}, ⋯ Y′_{k}/y′_{k}] ; \end{matrix} (6.25)

\begin{matrix}/\_{1 ≤ i ≤ k} Y′′_{i} & = & \{y′′_{i} : ∃y′′_{1} ⋯ y′′_{i−1}y′′_{i+1} ⋯ y′′_{k} ( \begin{matrix}sη_{2}μ_{2} & ∈ & t_{2} \\ Ψ̃η_{2}μ_{2} & ∈ & Φ̃ \end{matrix} )\} \\ & & where y′′_{1}, y′′_{2}, ⋯, y′′_{k} are new variables, and \\ & & μ_{2} denotes [Y′′_{1}/y′′_{1}, Y′′_{2}/y′′_{2}, ⋯ Y′′_{k}/y′′_{k}] ; \end{matrix} (6.26)

appear in F(D̃′).

Fix an i, 1 ≤ i ≤ k. Let rhs, rhs_{1} and rhs_{2} denote the r.h.s. of the i^{th} equations of the conjunctions (6.24), (6.25) and (6.26) respectively. To prove the lemma, it suffices to prove for all interpretations I that I(rhs) = I(rhs_{1}) ∪ I(rhs_{2}).

Now let I be any interpretation; thus I(rhs) is

\{Y_{i}θ : ( \begin{matrix}sθ & ∈ & I(t_{1} ∪ t_{2}) \\ Ψ̃θ & ∈ & I(Φ̃) \end{matrix} )\} (6.27)

where θ ranges over ground substitutions on Y_{1}, Y_{2}, ⋯, Y_{k}. Similarly I(rhs_{1}) and I(rhs_{2}) respectively are

\{Y′_{i}θ_{1} : ( \begin{matrix}sη_{1}θ_{1} & ∈ & I(t_{1}) \\ Ψ̃η_{1}θ_{1} & ∈ & I(Φ̃) \end{matrix} )\} (6.28)

\{Y′′_{i}θ_{2} : ( \begin{matrix}sη_{2}θ_{2} & ∈ & I(t_{2}) \\ Ψ̃η_{2}θ_{2} & ∈ & I(Φ̃) \end{matrix} )\} (6.29)

where η_{1} is the renaming [Y_{1}/Y′_{1}, ⋯, Y_{k}/Y′_{k}], η_{2} is [Y_{1}/Y′′_{1}, ⋯, Y_{k}/Y′′_{k}], θ_{1} ranges over ground substitutions on Y′_{1}, ⋯, Y′_{k}, and finally, θ_{2} ranges over ground substitutions on Y′′_{1}, ⋯, Y′′_{k}.

Since η_{1} is a renaming, η_{1}θ_{1} ranges over all ground substitutions on Y_{1}, ⋯, Y_{k}. Thus (6.28) can be written in the form

\{Y_{i}θ : ( \begin{matrix}sθ & ∈ & I(t_{1}) \\ Ψ̃θ & ∈ & I(Φ̃) \end{matrix} )\} . (6.30)

Similarly (6.29) can be written in the form

\{Y_{i}θ : ( \begin{matrix}sθ & ∈ & I(t_{2}) \\ Ψ̃θ & ∈ & I(Φ̃) \end{matrix} )\} . (6.31)

Clearly (6.27) equals the union of (6.30) and (6.31), and so the proposition follows.

Proposition 10 (Intersection) If the intersection transformation is used, then the only difference between F(D̃) and F(D̃′) is that the collection of equations F(D̃) = {Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k}} is replaced by F(D̃′) = {Y_{1} = exp′_{1}, ⋯, Y_{k} = exp′_{k}}. Furthermore,

for all interpretations I, I(exp_{i}) = I(exp′_{i}), 1 ≤ i ≤ k.

Proof: Let D_{j} be of the form {(s, t_{1} ∩t_{2}), (Ψ̃, Φ̃)} so that this collection is replaced by {(s, t_{1}), (s, t_{2}), (Ψ̃, Φ̃)} in D̃′. Thus var(s)∪var(Ψ̃) is {Y_{1}, ⋯, Y_{k}}, and the only difference between F(D̃) and F(D̃′) is that

\begin{matrix}/\_{1 ≤ i ≤ k} Y_{i} & = & \{y_{i} : ∃y_{1} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} ( \begin{matrix}sμ & ∈ & t_{1} ∩ t_{2} \\ Ψ̃μ & ∈ & Φ̃ \end{matrix} )\} \\ & & where y_{1}, ⋯, y_{k} are new variables, and \\ & & μ denotes [Y_{1}/y_{1}, ⋯, Y_{k}/y_{k}] ; \end{matrix} (6.32)

appears in F(D̃), whereas the formula

\begin{matrix}/\_{1 ≤ i ≤ k} Y_{i} & = & \{y_{i} : ∃y_{1} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} ( \begin{matrix}sμ & ∈ & t_{1} \\ sμ & ∈ & t_{2} \\ Ψ̃μ & ∈ & Φ̃ \end{matrix} )\} \\ & & where y_{1}, ⋯, y_{k} are new variables, and \\ & & μ denotes [Y_{1}/y_{1}, ⋯, Y_{k}/y_{k}] ; \end{matrix} (6.33)

appears in F(D̃′).

Fix an i, 1 ≤ i ≤ k. Let rhs_{1} and rhs_{2} denote the r.h.s. of the i^{th} equations of the conjunctions (6.32) and (6.33) respectively. To prove the lemma it suffices to prove, for all interpretations I, that I(rhs_{1}) = I(rhs_{2}). Toward this aim, we rewrite I(rhs_{1}) and I(rhs_{2}) respectively into:

\{Y^{i}θ : ( \begin{matrix}sθ & ∈ & I(t_{1} ∩ t_{2}) \\ Ψ̃θ & ∈ & I(Φ̃) \end{matrix} )\} (6.34)

\{Y^{i}θ : ( \begin{matrix}sθ & ∈ & I(t_{1}) \\ sθ & ∈ & I(t_{2}) \\ Ψ̃θ & ∈ & I(Φ̃) \end{matrix} )\} (6.35)

where θ ranges over ground substitutions on the variables Y_{1}, ⋯, Y_{k}. That (6.34) and (6.35) are equivalent is evident.

An important part of the proof of correctness involves treating set equations, such as C and δ, and quantified equations, such as F(D̃), as mappings from interpretations into interpretations. To define this mapping, let S be a collection of set and quantified equations, and let S be in normal form. Let I be an arbitrary interpretation. Now define that [[S]](I) = I′ where

I′(X) =^{def} \{ \begin{matrix}I(exp) & if X = exp is an equation in S; \\ I(X) & if X ∉ lhs(S). \end{matrix}

Recalling the definition of rhs(C)|_{X}, the above definition can be more simply stated as ([[S]](I)) (X) =^{def} I(rhs(S)|_{X}). We write [[S]] = [[S′]] to denote that, for all interpretations I, [[S]](I) = [[S′]](I)

We now consider some basic properties of the [[ ]] mapping. In the following propositions, let T, S, S_{0}, S_{1}, …, be collections of equations in normal form. Let I, I_{1} and I_{2} denote interpretations. Our first proposition requires no proof:

Proposition 11 I is a model of S iff [[S]](I) = I.

Proposition 12 (Monotonicity of [[ ]]) I_{1} ⊆ I_{2} implies [[S]](I_{1}) ⊆ [[S]](I_{2}).

Proof: Assume that I_{1} ⊆ I_{2}. Observe that

(a) if exp is a set expression, then I_{1}(exp) ⊆ I_{2}(exp);

(b) if exp is the expression {y_{i} : ∃y_{1} … y_{i−1}y_{i+1} … y_{m} (Ψ̃μ ∈ Φ̃)} where {Y_{1}, ⋯, Y_{m}} denotes the variables in Ψ̃, y_{1}, y_{2}, ⋯, y_{m} are new variables, and μ denotes [Y_{1}/y_{1}, Y_{2}/y_{2}, ⋯ Y_{m}/y_{m}], then we first note that I_{1}(Φ̃) ⊆ I_{2}(Φ̃) by (a). It is now easy to see that I_{1}(exp) ⊆ I_{2}(exp).

Thus I_{1}(exp) ⊆ I_{2}(exp) in both the above cases. Hence, if X ∈ lhs(S), that is X = exp appears in S for some expression exp, then ([[S]](I_{1})) (X) = I_{1}(exp) ⊆ I_{2}(exp) = ([[S]](I_{2})) (X). If, on the other hand, X ∉ lhs(X), then ([[S]](I_{1})) (X) = I_{1}(X) ⊆ I_{2}(X) = ([[S]](I_{2})) (X). Hence [[S]](I_{1}) ⊆ [[S]](I_{2}).

Proposition 13 (Algebraic properties of [[ ]]) Let lhs(S_{0}), lhs(S_{1}), lhs(S_{2}), … be mutually disjoint.

(a) Let [[T]](I) =_{V} [[S_{1}]][[S_{2}]](I) for some V.

If lhs(T) is disjoint from lhs(S_{0}), and var(rhs(S_{1})) is disjoint from lhs(S_{0}), then [[S_{0} ∪ T]](I) =_{V} [[S_{1}]][[S_{0} ∪ S_{2}]](I)

(b) Let [[T]](I) = [[S_{1} ∪ S_{2}]](I).

If lhs(T) is disjoint from lhs(S_{0}), then [[S_{0} ∪ T]](I) = [[S_{0} ∪ S_{1} ∪ S_{2}]](I)

(c) Let T ⊆ S_{1} ∪ ⋯ ∪ S_{n}.

If I is a model of T, and I(X) = ◯̸ for all X ∈ lhs(S_{1} ∪ ⋯ ∪ S_{n}) − lhs(T), then I ⊆ [[S_{1}]][[S_{2}]] ⋯ [[S_{n}]](I)

Proof:

(a) Let I be an interpretation and let X be any variable in V. Consider now the exhaustive cases:

• X ∈ lhs(S_{0}):

Now ([[S_{0} ∪ T]](I)) (X) is I(rhs(S_{0} ∪T)|_{X}) by definition. Since X ∉ lhs(T), this reduces to I (rhs(S_{0})|_{X}). Similarly, ([[S_{1}]][[S_{0} ∪ S_{2}]](I)) (X) is ([[S_{0} ∪ S_{2}]](I)) (rhs(S_{1})|_{X}) by definition. Since X ∉ lhs(S_{1}), this reduces to ([[S_{0} ∪ S_{2}]](I)) (X) which is I(rhs(S_{0} ∪ S_{2})|_{X}) by definition. Since X ∉ lhs(S_{2}), this in turn reduces to I (rhs(S_{0})|_{X}).

• X ∈ lhs(S_{1}):

Now ([[S_{0} ∪ T]](I)) (X) is I(rhs(S_{0}∪T)|_{X}) by definition. Since X ∉ lhs(S_{0}), this reduces to I(rhs(T)|_{X}) which is ([[T]](I)) (X) by definition. By assumption this is equal to ([[S_{1}]][[S_{2}]](I)) (X) which can be rewritten in the form I′(rhs(S_{1})|_{X}) where I′ is [[S_{2}]](I). Similarly, ([[S_{1}]][[S_{0} ∪ S_{2}]](I)) (X) can be rewritten in the form I′′(rhs(S_{1})|_{X}) where I′′ is [[S_{0} ∪S_{2}]](I). The remainder of the proof is that I′(rhs(S_{1})|_{X}) = I′′(rhs(S_{1})|_{X}), and this follows from the fact that I′ and I′′ differ only on lhs(S_{0}).

• X ∉ lhs(S_{0}) and X ∉ lhs(S_{1}):

Above, we have shown that if X ∉ lhs(S_{0}), then ([[S_{0} ∪ T]](I)) (X) is ([[S_{1}]][[S_{2}]](I)) (X). This is ([[S_{2}]](I)) (rhs(S_{1})|_{X}) by definition. Since X ∉ lhs(S_{1}), this reduces to ([[S_{2}]](I)) (X). Similarly, we have shown above that if X ∉ lhs(S_{1}), ([[S_{1}]][[S_{0} ∪ S_{2}]](I)) (X) reduces to ([[S_{0} ∪ S_{2}]](I)) (X), which is I(rhs(S_{0} ∪ S_{2})|_{X}) by definition. Since X ∉ lhs(S_{0}), this reduces to I(rhs(S_{2})|_{X}), which is ([[S_{2}]](I)) (X) by definition.

Thus for all X ∈ V, ([[S_{0} ∪ T]](I)) (X) = ([[S_{1}]][[S_{0} ∪ S_{2}]](I)) (X) and so (a) is proved.

(b) Let I be an interpretation and let X be any variable. Suppose that X ∈ lhs(S_{0}). Now ([[S_{0} ∪ T]](I)) (X) is I (rhs(S_{0} ∪ T)|_{X})) by definition. Since X ∉ lhs(T), this reduces to I (rhs(S_{0})|_{X})). Similarly, ([[S_{0} ∪ S_{1} ∪ S_{2}]](I)) (X) is I (rhs(S_{0} ∪ S_{1} ∪ S_{2})|_{X})) by definition. Since X ∉ lhs(S_{1}) and X ∉ lhs(S_{2}), this reduces to I (rhs(S_{0})|_{X})), and the proof for this case is finished.

Suppose that X ∉ lhs(S_{0}). Arguing as above, we can show that ([[S_{0} ∪ T]](I)) (X) reduces to ([[T]](I)) (X), and similarly that ([[S_{0} ∪ S_{1} ∪ S_{2}]](I)) (X) reduces to ([[S_{1} ∪ S_{2}]](I)) (X). Since ([[T]](I)) (X) = ([[S_{1} ∪ S_{2}]](I)) (X) by assumption, we are done.

(c) We first show that [[S_{i}]](I) ⊇ I for all 1 ≤ i ≤ n. Let X be any variable. If X ∉ lhs(S_{i}), then ([[S_{i}]](I)) (X) reduces to I(X). If X ∈ lhs(S_{i}) but X ∉ lhs(T), then I(X) = ◯̸ by assumption. The remaining alternative is X ∈ lhs(S_{i}) and X ∈ lhs(T). Now ([[S_{i}]](I)) (X) is I(rhs(S_{i})|_{X}) by definition. This is equal to I(X) because the equation X = rhs(S_{i})|_{X} appears in T and I is a model of T. Thus [[S_{i}]](I) ⊇ I for all 1 ≤ i ≤ n.

Using the monotonicity of [[S_{1}]], ⋯, [[S_{i−1}]], we have

[[S_{1}]] ⋯ [[S_{i−1}]][[S_{i}]](I) ⊇ [[S_{1}]] ⋯ [[S_{i−1}]](I)

for all 1 ≤ i ≤ n. This, in turn, can be repeatedly used in the following chain of reasoning:

[[S_{1}]] ⋯ [[S_{n−1}]][[S_{n}]](I)
⊇ [[S_{1}]] ⋯ [[S_{n−1}]](I)
⋮
⊇ [[S_{1}]](I)
⊇ I.

and the proof of (c) is finished.

In what follows, the [[ ]] mapping will be used to relate two formulas where one is obtained from the other via a number of applications of the transformations. For example, let the result of REDUCE(C, D̃) be (D̃′, Δ). Consider the sequence δ_{1}, ⋯, δ_{n} of extracted collections, in chronological order, which constitute Δ. Let δ_{1}^{u}, ⋯, δ_{k}^{u} be subsequence of δ_{1}, ⋯, δ_{n} containing just those δ’s extracted by the union transformation; similarly define δ_{1}^{c}, ⋯, δ_{m}^{c} to be the subsequence extracted by the clash and compaction transformations. The relationship between the original formula and its REDUCE’d counterpart is essentially that

[[C]][[F(D)]] = [[C]][[δ_{1}^{u}]] ⋯ [[δ_{k}^{u}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m}^{c} ∪ F(D′)]].

We now formally prove that the transformations are correct in two senses: one, that they preserve models, and two, that they preserve the mapping [[ ]] as explained above. The next lemma deals with the base case in which just one transformation is applied.

Lemma 4 (Correctness of One Application of a Transformation) Let C, D̃ ⟹_{tf} D̃′, δ. Let V = V AR − (var(D̃ ∪ δ) − var(D̃)), that is, V contains all variables except the new variables introduced by this transformation. Then for all models I of C:

(a) C ∧ F(D̃) ⟺_{V} C ∧ δ ∧ F(D̃′);

(b) [[F(D̃)]](I) =_{V} \{ \begin{matrix}[[δ]][[F(D̃′)]](I) & if tf is the union transformation; \\ [[δ ∪ F(D̃′)]](I) & if tf is clash or compaction; \\ [[F(D̃′)]](I) & if tf is D-substitution, cancel \\ & or intersection. \end{matrix}

Proof: First, suppose that the transformation used is either D-substitution, cancellation or intersection. Then δ = ◯̸ and by propositions 5, 7 and 10, the only difference between F(D̃′) and F(D̃) is that some equations Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k} in F(D̃) are replaced by some equations Y_{1} = exp′_{1}, ⋯, Y_{k} = exp′_{k} in F(D̃′) such that for all models I of C, I(exp_{i}) = I(exp′_{i}), 1 ≤ i ≤ k. It follows that:

C ∧ F(D̃) ⟺ C ∧ F(D̃′)

and so (a) is proved. Consider now [[F(D̃)]] and [[F(D̃′)]], and let I be a model of C. If Y is one of Y_{1}, ⋯, Y_{k}, say Y_{i}, then

([[F(D̃)]](I)) (Y) = I(exp_{i}) = I(exp′_{i}) = ([[F(D̃′)]](I)) (Y).

If, however, Y is different from all of Y_{1}, ⋯, Y_{k}, then it follows immediately that

([[F(D̃)]](I)) (Y) = ([[F(D̃′)]](I)) (Y)

because Y = exp appearing in F(D̃) implies that Y = exp appears also in F(D̃′), and vice-versa. Hence [[F(D̃)]](I) = [[F(D̃′)]](I) and so (b) is proved. This completes the proof of the lemma in the case of the D-substitution, cancellation or intersection transformation.

Suppose now that the clash or compaction transformation is applied. Let δ be {Y_{1} = exp′_{1}, ⋯, Y_{k} = exp′_{k}}, and let {Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k}} be the equations whose l.h.s. are Y_{1}, ⋯, Y_{k} in F(D̃). (Thus, in the case of clash, the exp′_{i} are ⊥, and in the case of compaction, the exp′_{i} are conjunctions.) By the clash and compaction propositions 6 and 8, we have that:

C ∧ F(D̃)
⟺ C ∧ {Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k}} ∧ F(D̃′)
⟺ C ∧ {Y_{1} = exp′_{1}, ⋯, Y_{k} = exp′_{k}} ∧ F(D̃′)
⟺ C ∧ δ ∧ F(D̃′).

Condition (a) is thus proved. To show (b), let I be model of C. If Y is one of Y_{1}, ⋯, Y_{k}, say Y_{i}, then

([[F(D̃)]](I)) (Y) = I(exp′_{i}) = I(exp_{i}) = ([[δ ∪ F(D̃)]](I)) (Y)

If Y is not one of Y_{1}, ⋯, Y_{k}, then it is immediate that ([[F(D̃)]](I)) (Y) = ([[δ ∪ F(D̃)]](I)) (Y). This proves (b), and hence finishes the proof of the lemma for in the case of the clash and compaction transformations.

Suppose now that the union transformation is applied. From the definition of this transformation and from proposition 9 we have that:

• δ is {Y_{1} = Y′_{1} ∪ Y′′_{1}, ⋯, Y_{k} = Y′_{k} ∪ Y′′_{k}};

• F(D̃) is {Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k}} ∪ F(D̃′′);

• F(D̃′) is {Y′_{1} = exp′_{1}, Y′′_{1} = exp′′_{1}, ⋯, Y′_{k} = exp′_{k}, Y′′_{k} = exp′′_{k}} ∪ F(D̃′′); and

• I(exp_{i}) = I(exp′_{i}) ∪ I(exp′′_{i}), 1 ≤ i ≤ k, for any model I of C.

where D̃′′ is D̃ − {D_{j}}. Now let I be a model of C ∧ F(D̃). Adapt I to I′ by defining that I′(Y′_{i}) = I(exp′_{i}) and I′(Y′′_{i}) = I(exp′′_{i}), 1 ≤ i ≤ k. Clearly I′ satisfies

\begin{aligned}C & ∧ & \{Y_{1} = Y′_{1} ∪ Y′′_{1}, ⋯, Y_{k} = Y′_{k} ∪ Y′′_{k}\} \\ & ∧ & \{Y′_{1} = exp′_{1}, Y′′_{1} = exp′′_{1}, ⋯, Y′_{k} = exp′_{k}, Y′′_{k} = exp′′_{k}\} ∧ F(D̃′′) \end{aligned}

and so one direction of (a) is proved. The other direction can be shown as follows. Let I be model of the formula immediately above. Clearly I models {Y_{1} = exp_{1}, ⋯, Y_{k} = exp_{k}} because

I(Y_{i}) = I(Y′_{i}) ∪ I(Y′′_{i}) = I(exp′_{i}) ∪ I(exp′′_{i}) = I(exp_{i}).

We now show that (b) holds in the case of the union transformation. If Y is one of Y_{1}, ⋯, Y_{k}, say Y_{i}, then

([[F(D̃)]](I)) (Y)
= I(exp_{i})
= I(exp′_{i}) ∪ I(exp′′_{i})
= ([[F(D̃′)]](I)) (Y′_{i} ∪ Y′′_{i})
= ([[F(D̃′)]](I)) (rhs(δ)|_{Y})
= ([[δ]][[F(D̃′)]](I)) (Y).

If Y ∈ lhs(F(D̃)) − {Y_{1}, ⋯, Y_{k}}, then it is immediate that ([[F(D̃)]](I)) (Y) = ([[δ]][[F(D̃′)]](I)) (Y) because the equation for Y in F(D̃) and F(D̃′) is the same, and there is no equation for Y in δ. The remaining case, that of Y ∈ V −lhs(F(D̃)), is also immediate because there is no equation for Y anywhere. This proves (b), and hence the lemma is proved.

The above lemma proved equivalences of [[]] mappings for a single application of a transformation. The equivalences were defined in three different ways depending on which transformation was used. The following lemma combines these equivalences over single applications into an equivalence over the sequence of applications generated by the entire algorithm.

Lemma 5 (Correctness of a Series of Transformations) Let C^{(0)} and D̃^{(0)}, satisfying the main algorithm precondition, be input to the main algorithm, and let the algorithm terminate after n + 1 iterations, n ≥ 0. Let δ_{1}^{u}, δ_{2}^{u}, ⋯, δ_{k}^{u} denote the sequence of equations extracted by applications of the union transformation, and similarly, let δ_{1}^{c}, δ_{2}^{c}, ⋯, δ_{m}^{c} denote the sequence of equations extracted by applications of the clash and compaction transformations. Then, for all models I of C^{(n)}:

[[F(D̃^{(0)})]](I) =_{var(C^{(0)},D̃^{(0)})} [[δ_{1}^{u}]] ⋯ [[δ_{k}^{u}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m}^{c} ∪ F(D̃^{(n+1)})]](I). (6.36)

Proof: First, note that the main loop invariant (proposition 3) implies that the k + 1 collections δ_{1}^{u}, …, δ_{k}^{u}, and δ_{1}^{c} ∪ ⋯ ∪ δ_{m}^{c} ∪ F(D̃_{p}) are in normal form. This proves that all of the [[ ]] expressions in equation (6.36) are well defined.

Before proving (6.36) we establish some notation. Let C_{j}, D̃_{j} ⟹ D̃_{j+1}, δ_{j+1}, 0 ≤ j ≤ p − 1, describe the sequence of transformations applied during the execution of the algorithm. Thus, by appropriate grouping, the sequence C_{0}, C_{1}, ⋯ C_{p−1} may be written as

C^{(0)}, C^{(0)}, ⋯ C^{(0)}, (Π_{1} copies, during first invocation of REDUCE)
C^{(1)}, C^{(1)}, ⋯ C^{(1)}, (Π_{2} copies, during second invocation of REDUCE)
⋮
C^{(n)}, C^{(n)}, ⋯ C^{(n)}, (Π_{n+1} copies, during (n + 1)^{th} invocation of REDUCE)

where p = Π_{1} + ⋯ + Π_{n+1}, and each Π_{i} denotes the number of transformations applied during the i^{th} invocation of REDUCE. We also have that

Δ^{(1)} = δ_{1} ∪ ⋯ ∪ δ_{Π_{1}},
C^{(1)} = SIMP LIF Y (C^{(0)} ∪ δ_{1} ∪ ⋯ ∪ δ_{Π_{1}}),
Δ^{(2)} = δ_{Π_{1}+1} ∪ ⋯ ∪ δ_{Π_{2}}
C^{(2)} = SIMP LIF Y (C^{(1)} ∪ δ_{Π_{1}+1} ∪ ⋯ ∪ δ_{Π_{2}}),
⋯
Δ^{(n+1)} = δ_{Π_{n}+1} ∪ ⋯ ∪ δ_{Π_{n+1}},
C^{(n+1)} = SIMP LIF Y (C^{(n)} ∪ δ_{Π_{n}+1} ∪ ⋯ ∪ δ_{Π_{n+1}}),

Now, from corollary 2, if C′ = SIMP LIF Y (C) then any model of C′ is a model of C. Repeated application of this fact proves that I is not only a model of C^{(n)}, but also a model of C^{(0)}, …, C^{(n−1)}. Hence I is a model of C_{0}, …, C_{p−1}.

To prove equation (6.36) we prove by induction that for all 0 ≤ j ≤ p,

[[F(D̃_{0})]](I) =_{var(C^{(0)},D̃^{(0)})} [[δ_{1}^{u}]] ⋯ [[δ_{k′}^{u}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} ∪ F(D̃_{j})]](I)

where δ_{1}^{u}, δ_{2}^{u}, ⋯, δ_{k′}^{u}, 1 ≤ k′ ≤ k, is the subsequence of δ_{1}, δ_{2}, ⋯, δ_{j} corresponding to applications of the union transformation and similarly δ_{1}^{c}, δ_{2}^{c}, ⋯, δ_{m′}^{c}, 1 ≤ m′ ≤ m, is the subsequence corresponding to applications of the clash and compaction transformations. The lemma is then immediate from the case of j = p.

The base case of j = 0 is trivially true. Assume now that the lemma holds for a given j. The (j + 1)^{th} transformation is either (a) a union transformation, (b) a clash or compaction transformation, or (c) one of the remaining transformations. Let δ_{j+1} be the equations extracted by this transformation, and consider these cases in turn:

(a) Let V_{new} be the new variables introduced by this application of the union transformation, that is, the variables (var(D̃_{j+1}) ∪ var(δ_{j+1})) − var(D̃_{j}). Let V_{old} denote V AR − V_{new}. By lemma 4, we then have

[[F(D̃_{j})]](I) =_{V_{old}} [[δ_{j+1}]][[F(D̃_{j+1})]](I).

By inspection of the union transformation, we have that rhs(δ_{j+1}) contains only new variables, that is, var(rhs(δ_{j+1})) ⊆ V_{new}. This means that var(rhs(δ_{j+1}) and lhs(δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c}) are disjoint. We can therefore apply proposition 13(a) (by substituting F(D̃_{j}), δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c}, δ_{j+1} and F(D̃_{j+1}) for T, S_{0}, S_{1} and S_{2} in the proposition) to obtain

[[δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} ∪ F(D̃_{j})]](I) =_{V_{old}} [[δ_{j+1}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} ∪ F(D̃_{j+1})]](I).

Now since [[δ_{1}^{u}]][[δ_{2}^{u}]] ⋯ [[δ_{k′}^{u}]] contains only variables from V_{old}, we have

\begin{aligned}& [[δ_{1}^{u}]] ⋯ [[δ_{k′}^{u}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} ∪ F(D̃_{j})]](I) \\ =_{V_{old}} & [[δ_{1}^{u}]] ⋯ [[δ_{k′}^{u}]][[δ_{j+1}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} ∪ F(D̃_{j+1})]](I). \end{aligned}

On renaming δ_{j+1} into δ_{k′+1}^{u}, and noting that var(C^{(0)}, D̃^{(0)}) ⊆ V_{old}, the hypothesis for j + 1 follows directly from the hypothesis for j.

(b) By lemma 4, we have that

[[F(D̃_{j})]](I) = [[δ_{j+1} ∪ F(D̃_{j+1})]](I),

and so by proposition 13(b) (in which we substitute F(D̃_{j}) for T, δ_{j+1} for S_{1}, F(D̃_{j+1}) for S_{2} and δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} for S_{0})

[[δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} ∪ F(D̃_{j})]](I) = [[δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} ∪ δ_{j+1} ∪ F(D̃_{j+1})]](I).

On applying [[δ_{1}^{u}]][[δ_{2}^{u}]] ⋯ [[δ_{k′}^{u}]] to both sides of this equation and renaming δ_{j+1} into δ_{m′+1}^{u}, the hypothesis for j + 1 follows directly from the hypothesis for j.

(c) In the case that the transformation is not union, clash or compaction, lemma 4 implies that [[F(D̃_{j+1})]](I) = [[F(D̃_{j})]](I). By proposition 13(b) (in which S_{1} is substituted by ◯̸) we have

[[δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} ∪ F(D̃_{j})]](I) = [[δ_{1}^{c} ∪ ⋯ ∪ δ_{m′}^{c} ∪ F(D̃_{j+1})]](I).

Once again, on applying [[δ_{1}^{u}]][[δ_{2}^{u}]] ⋯ [[δ_{k′}^{u}]] to both sides of this equation, the hypothesis for j + 1 follows directly from the hypothesis for j.

Lemma 6 (Termination Property of Transformations) If no transformations are applicable on D̃ in the context of C then [[F(D̃)]](lm(C)) assigns ◯̸ to all variables in lhs(F(D̃)).

Proof: Let Y_{i} = exp be an equation in F(D̃). Then exp is of the form

{y_{i} : ∃y_{1} ⋯ y_{i−1}y_{i+1} ⋯ y_{k} ( Ψ̃μ, Φ̃ ) }

where var(Ψ̃) = {Y_{1}, ⋯, Y_{k}}, y_{1}, ⋯, y_{k} are new variables, and μ denotes the renaming substitution

[Y_{1}/y_{1}, ⋯ Y_{k}/y_{k}] .

Since no transformation is applicable to (Ψ̃, Φ̃) in the context of C, then (Ψ̃, Φ̃) cannot contain any pairs of the form (t, s ∪ s′), (t, s ∩ s′), (f(t̃), f′(s̃)), or (t, V) where V is a solved variable in C. In fact, either:

• (Ψ̃, Φ̃) contains a pair of the form (t, V), for some variable V, and V is not a solved variable in C; or

• (Ψ̃, Φ̃) is of the form (X̃, Φ̃) and for some variable Y in X̃, it is not the case that

NONEMP T Y (C, ⋂_{(Y,ϕ)∈(Ψ̃,Φ̃)} ϕ).

In either case, we have that there are no values for the variables in Ψ̃ such that Ψ̃ ∈ (lm(C))(Φ̃)). Hence lm(C)(exp) is empty, and the result follows.

Using this notation, the next proposition states an obvious property of the collections C^{(i)}.

Main Lemma 3 (Correctness of Main Algorithm) Let C^{(0)} and D̃^{(0)} satisfy the main algorithm precondition. Let C^{(0)} and D̃^{(0)} be input to the main algorithm, and let C be output. Then,

• lm(C) =_{var(C^{(0)},D̃^{(0)})} lm(C^{(0)} ∧ F(D̃^{(0)})), and

• C is in solved form

Proof: We first dispense with proving that C is in solved form. This follows directly from the fact that SIMP LIF Y returns equations in solved form. The remainder of this proof is that lm(C) =_{var(C^{(0)},D̃^{(0)})} lm(C^{(0)} ∧ F(D̃^{(0)})).

Suppose that the algorithm terminates after n + 1 iterations. Let δ_{1}, δ_{2}, ⋯, δ_{p} denote the sequence of extracted collections obtained during execution of the algorithm. Let δ_{1}^{u}, δ_{2}^{u}, ⋯, δ_{k}^{u} be the subsequence of this consisting of just those extracted collections obtained via the union transformation. Similarly, let δ_{1}^{c}, δ_{2}^{c}, ⋯, δ_{m}^{c} be corresponding subsequence with respect to the clash and compaction transformations.

We now show that lm(C^{(n)}) is a model of C^{(0)} ∧ F(D̃^{(0)}). That lm(C^{(n)}) is a model of C^{(0)} follows from repeated application of corollary 2. We now show that lm(C^{(n)}) is a model of F(D̃^{(0)}). Let I_{n} and I_{n+1} abbreviate lm(C^{(n)}) and lm(C^{(n+1)}) respectively, and let V_{0} abbreviate var(C^{(0)}, D̃^{(0)}). We proceed in three parts. First we show that

I_{n} =_{V_{0}} I_{n+1}. (6.37)

Obtain from C^{(n)} a collection Ĉ^{(n)} by truncating each equation X = sexp in C^{(n)} into X = crhs(C^{(n)})|_{X}. Partition Ĉ^{(n)} to obtain \overline{C}^{(n)} and \overline{\overline{C}}^{(n)} where the first partition \overline{C}^{(n)} contains all the equations whose l.h.s. is a variable from V^{⋆}. Similarly obtain the sets Ĉ^{(n+1)}, \overline{C}^{(n+1)} and \overline{\overline{C}}^{(n+1)}. Now, by the construction of the least model given in proposition 2 lm(Ĉ^{(n)}) = lm(C^{(n)}) (the deleted expressions are empty in the least model). Similarly, we have lm(Ĉ^{(n+1)}) = lm(C^{(n+1)}). Now by proposition 4, all of the variables in \overline{C}^{(n)} are in V^{⋆}. Thus the least model of Ĉ^{(n)} restricted to V^{⋆} is defined by \overline{C}^{(n)} alone. That is, lm(Ĉ^{(n)}) =_{V^{⋆}} lm(\overline{C}^{(n)}). Similarly, we have lm(Ĉ^{(n+1)}) =_{V^{⋆}} lm(\overline{C}^{(n+1)}). Finally, by the termination condition of the main algorithm, (crhs(C^{(n+1)})|_{X} = crhs(C^{(n)})|_{X} for all X ∈ V^{⋆}), which implies that \overline{C}^{(n)} = \overline{C}^{(n+1)}. Thus I_{n+1} =_{V^{⋆}} I_{n}, and since V_{0} ⊆ V^{⋆}, this implies (6.37).

Second, we use (6.37) to show that

I_{n} =_{V_{0}} [[δ_{1}^{u}]] ⋯ [[δ_{k}^{u}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m}^{c}]](I_{n}) (6.38)

Consider the following chain of inclusions.

\begin{matrix}& I_{n} \\ ⊆_{V_{0}} & [[δ_{1}^{u}]] ⋯ [[δ_{k}^{u}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m}^{c}]](I_{n}) \\ ⊆_{V_{0}} & [[δ_{1}^{u}]] ⋯ [[δ_{k}^{u}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m}^{c}]](I_{n+1}) \\ ⊆_{V_{0}} & I_{n+1} \\ ⊆_{V_{0}} & I_{n} \end{matrix} (6.39)

To prove the first inclusion, let δ_{1}, ⋯, δ_{p′}, p′ ≤ p, be the equations extracted in all but the last iteration of the main loop. By repeated application of corollary 2, I_{n} is a model of δ_{1} ∪ ⋯ ∪ δ_{p′}. Also, for p′ < l ≤ p, none of the variables in lhs(δ_{i}) appear in C_{n}. Hence I_{n} maps all such variables to ◯̸. By proposition 13(c) (in which δ_{1} ∪ ⋯ ∪ δ_{p′} is substituted for S), we obtain the first inclusion in (6.39).

To prove the second inclusion of (6.39), note that from corollary 2, C^{(n+1)} ⊧ C^{(n)}. Hence I_{n} ⊆ I_{n+1}. The inclusion then follows from easily from proposition 12 (monotonicity of [[ ]]).

To prove the third inclusion of (6.39), note that I_{n+1} is a model of δ_{1}, ⋯, δ_{p}, and hence the required inclusion follows from repeated application of proposition 11.

The final inclusion of (6.39) follows immediately from (6.37). Hence, we have proved each of the inclusions in (6.39). But this means that each inclusion in (6.39) is in fact an equality, and this therefore proves (6.38).

The final part of the proof that I_{n} is a model of F(D̃^{(0)}) uses (6.38) in the following chain of reasoning:

\begin{aligned}[[F(D̃^{(0)})]](I_{n}) & =_{V_{0}} & [[δ_{1}^{u}]] ⋯ [[δ_{k}^{u}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m}^{c} ∪ F(D̃^{(n+1)})]](I_{n}) \\ & =_{V_{0}} & [[δ_{1}^{u}]] ⋯ [[δ_{k}^{u}]][[δ_{1}^{c} ∪ ⋯ ∪ δ_{m}^{c}]](I_{n}) \\ & =_{V_{0}} & I_{n}. \end{aligned} \begin{matrix}(6.40) \\ (6.41) \\ (6.42) \end{matrix}

The equality (6.40) follows directly from lemma 5. We now prove the equality (6.41). By lemma 6, we have, for all equations X = exp in F(D̃^{(n+1)}), that I_{n}(exp) = ◯̸. By the main loop invariant (proposition 3), X does not appear in lhs(C^{(n)}) and so I_{n}(X) = ◯̸. Thus F(D̃^{(n+1)}) can be removed from the r.h.s. of (6.40), and (6.41) follows. The final equality, (6.42) has already been proved in (6.38). Since lhs(F(D̃^{(0)})) ⊆ V_{0}, the above equalities imply [[F(D̃^{(0)})]](I_{n}) = I_{n}. By proposition 11, I_{n} is a model of F(D̃^{(0)}). Hence I_{n} is a model of C^{(0)} ∧F(D̃^{(0)}).

It remains to show that I_{n}, is not just a model, but the least model of C^{(0)} ∧ F(D̃^{(0)}). Now, by lemma 4,

C^{(0)} ∧ F(D̃^{(0)}) ⟺_{V_{0}} C^{(n)} ∧ F(D̃_{n}).

which means that for each model of C^{(0)} ∧F(D̃^{(0)}), there is a model of C^{(n)} ∧F(D̃_{n}) such that the two models agree on V_{0}. Hence corresponding to the least model I_{0} of C^{(0)} ∧ F(D̃^{(0)}), is a model I′_{0} of C^{(n)} ∧ F(D̃_{n}) such that I′_{0} =_{V_{0}} I_{0}. Since I_{n} is the least model of C^{(n)} ∧ F(D̃_{n}), I_{n} ⊆ I′_{0} which in turn implies I_{n} ⊆_{V_{0}} I_{0}. Now, it is already proved above that I_{n} is a model of C^{(0)} ∧ F(D̃^{(0)}), and so I_{0} ⊆_{V_{0}} I_{n}. Thus I_{n} =_{V_{0}} I_{0}.

6.4 The Final Algorithm

Given a program P, let C_{P} ∧ F(D̃_{P}) denote the associated set formula. The main algorithm cannot, in general, be directly applied to the expressions C_{P} and D̃_{P}

input an arbitrary logic program P;

1. obtain the set formula C_{P} ∧ F(D̃_{P}) associated with P;

2. apply the preprocessing algorithm to C_{P} and D̃_{P} to obtain C^{(0)} and D̃^{(0)};

3. apply the main algorithm to C^{(0)} and D̃^{(0)} to obtain C; output C;

Figure 4: Final Algorithm

because the main algorithm precondition may not be satisfied. More precisely, this precondition may be violated only because the r.h.s. of a pair in D̃_{P} may be deeply nested. Hence the following preprocessing algorithm which transforms C_{P} and D̃_{P} into equivalent expressions C^{(0)} and D̃^{(0)} which satisfy the precondition.

Replace each pair (ψ, ϕ) in D̃_{P} by the pair (ψ, Z) where Z is a new variable, and add to C_{P} the equation Z = ϕ. Next, exhaustively apply the following transformation: if C_{P} contains a subexpression f(t_{1}, ⋯, t_{n}) where some t_{i}, 1 ≤ i ≤ n, is not a variable, then replace that occurrence of t_{i} by a new variable X and add the equation X = t_{i}. Next, rewrite the r.h.s. of each equation in C_{P} into DNF. Finally, apply SIMP LIF Y to C_{P}. Let the expressions resulting from all these steps be denoted C^{(0)} and D̃^{(0)}. It is easy to prove

Proposition 14

(a) var(C_{P} , D̃_{P}) ⊆ var(C^{(0)}, D̃^{(0)});

(b) lm (C^{(0)} ∧ F(D̃^{(0)})) =_{var(C_{P} ,D̃_{P})} lm (C_{P} ∧ F(D̃_{P})), and

(c) C^{(0)} and D̃^{(0)} satisfy the main algorithm precondition.

The algorithm is presented in its entirety in figure 4. We now conclude this section with the main result of this paper.

Theorem:

Let P be an arbitrary logic program input to the final algorithm. Then (i) the final algorithm terminates, returning a formula C;

(ii) C is a solved form collection of set equations, and

(iii) ⋃_{p∈Π_{P}} (lm(C)) (Υ_{p}) = τ_{P} ↑ω.

\underline{Section 7: Conclusion} 64

Proof: First note that by proposition 14(c) the main algorithm is applied appropriately. Now, the proof of termination follows essentially from main lemma 2. That C is a solved form collection of set equations follows from two facts: (a) SIMP LIF Y is only applied to a normal form collection (and this is guaranteed by the main loop invariant), and (b) lemma 2, which states the output of SIMP LIF Y is a solved form collection of set equations. Thus only (iii) remains to be proved. Now,

lm(C) =_{var(C_{P} ,D̃_{P})} lm (C^{(0)} ∧ F(D̃^{(0)})) , by lemma 3 and prop^{n} 14(a);
=_{var(C_{P} ,D̃_{P})} lm (C_{P} ∧ F(D̃_{P})) , by prop^{n} 14(b);

and by main lemma 1, we have

⋃_{p∈Π_{P}}lm(C_{P} ∧ F(D̃_{P}))(Υ_{p}) = τ_{P} ↑ω.

Since Υ_{p} ∈ var(C_{P} , D̃_{P}) for all p ∈ Π_{P}, the two interpretations lm(C) and lm(C_{P} ∧ F(D̃_{P})) agree on all such Υ_{p}. Thus (iii) follows.

7 Conclusion

In program analysis, a key notion used to approximate the meaning of a program is that of ignoring inter-variable dependencies. We formalized this notion for logic programs using an approximation operator on term substitutions. We argued that this formalization produced more accurate approximations than similar formalizations in the literature. We then proved that the approximate meaning of a logic program can be equivalently formalized as the least model of a set formula associated with the program. The main result proved that such least models are not only recursive sets, but they are recognizable by tree automata. This result is essentially an algorithm consisting of two main parts.

The first part of our algorithm, called SIMPLIFY, was a decision procedure for a class of set equations, that is, set equations in normal form. Earlier related work is that of Reynolds [12] and [9], the latter being an independent treatise of work similar to the former. In these works, the set expressions were allowed to contain projection functions, but they were not allowed to contain the intersection function (these works were not concerned with problem of shared variables inherent in logic programs). Thus their transformations mainly served to eliminate occurrences of projection functions while ours mainly served to eliminate occurrences of the intersection function^{10}.

The second and main part of our algorithm is also based upon a group of transformations. When used directly, these transformations do not always lead to a terminating computation. The key aspect of the main algorithm, therefore, is in its controlled use of the transformations. This is realized by the function REDUCE each of whose invocations performed transformations local to a fixed collection of set equations. The main loop in the main algorithm then ensured that REDUCE is invoked sufficiently often.

We finally note that two important practical issues have yet to be addressed: the first is efficiency; second, our algorithm does not, in general, return a minimal representation of τ_{P} ↑ω.

References

[1] M. Bruynooghe, “A Practical Framework for the Abstract Interpretation of Logic Programs”, revised version of report CW-62, Dept. Comp. Sci., K.U. Leuven, 33 pages, October 1987.

[2] M. Bruynooghe and G. Janssens, “An Instance of Abstract Interpretation integrating Type and Mode Inference”, Proceedings 5^{th} Int. Conf. on Logic Programming, K.A. Bowen and R.A. Kowalski (eds), MIT Press, pp 669 - 683, August 1988.

[3] S.K. Debray, “Global Optimization of Logic Programs”, Ph.D. Thesis, Department of Computer Science, SUNY at Stony Brook, 233 pages, December 1986.

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

[5] N.C. Heintze and J. Jaffar, “A Decision Procedure for a Class of Herbrand Set Constraints”, draft manuscript (extended abstract to appear in Proceedings 5^{th} IEEE Symposium on Logic in Computer Science June 1990).

[6] N.C. Heintze and J. Jaffar, “Semantic Types for Logic Programs”, draft manuscript (submitted for publication), March 1990.

[7] J.W. Lloyd, “Foundations of Logic Programming”, Second Edition, Springer-Verlag Series on Symbolic Computation, 1987.

[8] N.D. Jones and S.S. Muchnick, “Complexity of Flow Analysis, Inductive Assertion Synthesis, and a Language due to Dijkstra”, Proceedings 20^{th} Conference on Foundations of Computer Science, pp 185 - 190, also in, Program Flow Analysis: Theory and Applications, N.D. Jones and S.S. Muchnick (eds), Prentice-Hall, 1981.

10In [5], we present a decision procedure which deals with both projection and intersection functions.

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

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

[11] P. Mishra and U.S. Reddy, “Declaration-free Type Checking”, Proceedings 12^{th} ACM Symposium on Principles of Programming Languages, New Orleans, pp 7 - 21, 1985.

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

[13] J. Xu and D.S. Warren, “A Type Inference System for PROLOG”, Proceedings 5^{th} Intl. Conf. and Symp. on Logic Programming, MIT Press, pp 604 - 619. July 1988.

[14] E. Yardeni and E.Y. Shapiro, “A Type System for Logic Programs”, in Concurrent PROLOG: Collected Papers, Vol. 2, MIT Press, pp 211 - 244, 1987.