A Decision Procedure for a Class of Set Constraints

(Extended Abstract)

Nevin Heintze

School of Computer Science Carnegie Mellon University

Pittsburgh, PA 15213 (nch@cs.cmu.edu)

Joxan Jaffar

IBM T.J. Watson Research Center

P.O. Box 218 Yorktown Heights, NY 10598

(joxan@ibm.com)

Summary

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

An additional feature of the algorithm is that it deals with another important class of set constraints. These are the solved form set constraints which have the form X_{1} = exp_{1}, ⋯, X_{n} = exp_{n} where the X_{i} are distinct variables and the exp_{i} are positive set expressions. A solved form constraint is always satisfiable and possesses a least and a greatest model. Our algorithm can output explicit representations of both.

1 Introduction

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

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

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

Reynolds [9] and Jones and Muchnick [5], for example, considered functional programs and used a class of set constraints whose satisfiability is guaranteed. The focus of these works was to provide an explicit representation of the model defined by the constraints. Mishra [7], in his framework for type inference in logic programs, used set constraints to model a superset of the success set of a program. Though a full decision procedure was not presented, algorithms for subcases were investigated. Heintze and Jaffar [4] used set constraints to obtain a recursive and accurate approximation of the meaning of a logic program.

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

The decision procedure presented is constructive because it outputs an explicit representation of the least model of a given conjunction of definite set constraints. An additional feature of the algorithm is that it deals with another important class of set constraints. These are the solved form set constraints which have the form X_{1} = exp_{1}, ⋯, X_{n} = exp_{n} where = denotes the obvious abbreviation of two ⊇ constraints, the X_{i} are distinct variables and the exp_{i} are set expressions. A solved form constraint is always satisfiable and possesses a least and a greatest model. The algorithm can output explicit representations of both.

2 Preliminaries

Let V and Σ respectively denote denumerable sets of variables and functors; we assume that Σ contains at least one constant. Let τ(Σ) and τ(Σ ∪ V) and denote the corresponding Herbrand universe (HU) and Herbrand terms. Let var(t), where t is any expression, denote the set of variables appearing in t. Let A, A_{1}, ⋯, A_{n} ⊆ τ(Σ), n ≥ 1. Then

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

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

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

An interpretation is a map from V ⟶ 2^{HU}. An interpretation I, induces, in an obvious way, a mapping from set expressions sexp into 2^{HU} as follows. I(⊥) = ◯̸; I(⊤) = HU; I(c) = {c} where c ∈ Σ is a constant; I(f_{(i)}^{−1}(t)) = f_{(i)}^{−1}(I(t)) and I(f(t_{1}, ⋯, t_{n})) = f(I(t_{1}), ⋯, I(t_{n}) where f ∈ Σ is n-ary; and finally, I(t ∪ t′) = I(t) ∪ I(t′) and I(t ∩ t′) = I(t) ∩ I(t′) and I(\overline{t}) = HU − I(t). This mapping, in turn, induces a mapping from collections C of set constraints into true or false in the obvious way. If I maps C into true, we say that I is a model of C. We write I ⊇ I′ if I(X) ⊇ I′(X) for all X ∈ V^{1}. The following are some basic properties about interpretations on ground set expressions t and t′: (a) I(t) denotes a unique value regardless of the choice of I – denote this by [[t]]; (b) if t does not contain any union symbols, there exists a unique ground term t′′ such that I(t) = I(t′′) for all I; (c) if t and t′ are different and are both terms, then I(t) ≠ I(t′).

Consider next the problem of explicitly representing a given interpretation. A criteria is that the representation can be used to check whether or not an arbitrary set constraint is true in the interpretation. Toward this aim, define that a term grammar is a grammar G whose nonterminals are variables in V, and each production X ⟹ t satisfies: t is either a constant, a special constant or of the form f(X_{1}, ⋯, X_{n}), where f ∈ Σ is n-ary, and the variables X_{1}, ⋯, X_{n} appear in lhs(G), the left-hand-sides of G. Derivability =G⇒ is defined in an obvious way: sexp =G⇒ sexp′ if sexp′ is the result of replacing one occurrence of a variable X in sexp by t, and X ⟹ t is a production in G. A term grammar G then defines an interpretation I_{G} since it associates to each variable a set of ground terms as follows:

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

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

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

The main result of this paper can now be stated as follows: Given a conjunction of definite set constraints, the algorithm presented below (a) determines if the conjunction is satisfiable, and (b) if so, outputs a term grammar which represents its least model.

3 Set Expression Grammars

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

A set expression grammar G is defined to be like a term grammar except that each production X ⟹ sexp in G is such that sexp may contain the intersection or projection symbols^{3}. As with term grammars, G defines an interpretation, call it I_{G}, defined as follows:

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

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

The following two propositions pertain to a set expression G, and are easy to verify.

1I ⊇ I′ implies, by monotonicity, that I(sexp) ⊇ I′(sexp) for any sexp.

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

3The union and complement symbols are still omitted.

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

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

⋯, t_{n} ⟹^{⋆} t′_{n}.

Proposition 2 Let t be a set expression. Then

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

where t′ ranges over ground set expressions.

4 Solved Form Set Constraints

A conjunction C of set constraints is in solved form if it is of the form X_{1} = sexp_{1}, ⋯, X_{n} = sexp_{n} where the X_{i} are distinct variables and the sexp_{i} are set expressions. The problem at hand is to find an explicit representation of the least and greatest models of C, hereafter denoted lm(C) and gm(C) respectively.

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

The main contribution of this section is twofold: first, it deals with the case where C may contain both intersection and projection symbols; second, it deals not only with lm(C), but with gm(C) as well.

4.1 Least Model

We now present an algorithm to find an explicit representation of lm(C). We first construct a set expression grammar which defines lm(C). The bulk of this subsection then deals with the problem of converting this set expression grammar into an equivalent term grammar.

We begin by transforming C into grammar form; this form is defined as a conjunction, each of whose constraints is of the form X ⊇ sexp, where sexp does not contain the union or complement symbol. This is achieved by the following simple algorithm.

replace each X = sexp in C by X ⊇ sexp; while C contains a union symbol do

choose an ocurrence of an expression

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

endwhile

We can show that the conjunction C obtained by this algorithm has essentially the same least model as the original conjunction. The essential benefit of a conjunction being in grammar form is that we can construct a grammar representing its least model as follows.

Proposition 3 Let C be a grammar form conjunction of set constraints and let G be the set expression grammar such that X ⟹ t ∈ G just in case X ⊇ t ∈ C. Then

• sexp ⟹^{⋆} sexp′ implies C ⊧ sexp ⊇ sexp′, and

• I_{G} = lm(C).

From the correctness of the algorithm above and proposition 3, we have

Lemma 1 Let C be a solved form conjunction of set constraints. Then we can construct a set expression grammar G such that I_{G}(X) = (lm(C))(X) for all X ∈ var(C).

We now deal with the problem of converting a set expression grammar into an equivalent term grammar. We do this in three main parts. The first part reduces an arbitrary set expression grammar G into an equivalent one in a restricted form. This reduction will employ the following three transformations:

Transformation 1 (Unfold) If G contains an occurrence of a non-variable expression t nested within the scope of a functor or a projection symbol, then replace the occurrence by a new variable Z, and add the production Z ⟹ t.

Transformation 2 (Substitute) If G contains a production X ⟹ sexp such that sexp contains an occurrence of a variable Y different from X and this occurrence is not nested inside a functor or a projection symbol, then

• let Y ⟹ t_{1} ⋯, Y ⟹ t_{n} be all of the productions for Y and

• let sexp_{1}, ⋯, sexp_{n} denote the result of replacing the occurrence of Y in sexp by t_{1}, ⋯, t_{n} respectively

and replace the production X ⟹ sexp by the productions X ⟹ sexp_{1}, ⋯, X ⟹ sexp_{n}. We say that the transformation \underline{using} Y was applied to G.

Transformation 3 (Cycle-Removal) If G contains a production X ⟹ sexp such that sexp has an occurrence of the variable X which is not nested inside a functor or a projection symbol, then delete this production.

We now present an algorithm called STAN-DARDIZE, and we define that its operation on an input grammar G results in a grammar which is in standardized form. In what follows, the term “exhaustively-apply” means repeated application of a transformation until no change is observed.

exhaustively-apply transf^{n} 1; for each variable X in lhs(G) do exhaustively-apply transf^{n} 3; exhaustively-apply transf^{n} 2 using X;

endfor

delete productions containing ⊥;

delete productions containing a variable ∉ lhs(G);

We remark that the relative order of applying these transformations, as indicated in the algorithm above, is important.

Lemma 2 Let G be a set expression grammar. Then

• the STANDARDIZE terminates on G, yielding a set expression grammar, say G′;

• all productions in G′ are of the form X ⟹ t_{1} ∩ ⋯ ∩ t_{n}, n ≥ 1, such that each t_{i} is of the form η(X_{1}, ⋯, X_{k}) where the X_{j} are variables from lhs(G′) and η is a functor or a projection symbol;

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

We next consider elimination of projection symbols from a set expression grammar G. Toward this aim, we define another transformation. In condition (c) below, we assume that there exists a recursive function ORACLE(G, X) which returns true if and only if X ⟹^{⋆} t for some ground set expression t which (a) has no projection symbols, and (b) [[t]] ≠ ◯̸. We provide an implementation of ORACLE later.

Transformation 4 (Projection-Elimination) If G contains a production R which has a subexpression f_{(i)}^{−1}(Z) and if

(a) G contains a production Z ⟹ f(Y_{1,1}, ⋯, Y_{1,n})∩⋯∩f(Y_{k,1}, ⋯, Y_{k,n}) ∩t_{1} ∩ ⋯ ∩ t_{m} where k ≥ 0, m ≥ 0 and the t_{i} are ⊤;

(b) ORACLE(G, Y_{j,i′}), 1 ≤ j ≤ k, 1 ≤ i′ ≤ n; and (c) G contains the productions

Y_{j,i} ⟹ α_{j} (1 ≤ j ≤ k),

then add to G the production resulting from replacing that subexpression in R by α_{1}∩⋯∩α_{k} (or ⊤ in case k = 0) and any removing duplicate α_{j}’s.

Lemma 3 Let G be a standardized set expression grammar. Then

• the exhaustive application of transformation 4 terminates, yielding G′, and

• I_{G} = I_{G′} = I_{G′′} where G′′ contains just those productions in G′ which do not contain the projection symbol.

Finally, we deal with eliminating intersection symbols. Given two term grammars, we can construct a third whose language is the intersection of the first two [10] [2]. We cannot, however, use this result to eliminate occurrences of the intersection symbol and reduce a set expression grammar into a term grammar. This is because a grammar which has intersection symbols within its productions cannot, in general, be broken into intersection-free parts whose interpretations combine to equal the original interpretation.

As before, we proceed by defining two new transformations on a set expression grammar G.

Transformation 5 (∩-distribution) If (a) G contains a subexpression of the form f(X_{1}, ⋯, X_{n}) ∩ f(Y_{1}, ⋯, Y_{n}), and if (b) there are variables Z_{i} such that I_{G}(Z_{i}) = I_{G}(X_{i} ∩ Y_{i}) for all 1 ≤ i ≤ n, then replace this subexpression by f(Z_{1}, ⋯, Z_{n}).

Transformation 6 (∩-clash) If G contains a production of the form X ⟹ f(⋯) ∩ g(⋯) ∩ sexp where f ≠ g, then delete this production.

It is easy to show that these productions are correct in the sense that the least model is preserved. That these productions are complete, in the sense that one of them is applicable whenever G still contains an intersection symbol, is in fact not true. This is because condition (b) of the ∩- distribution transformation may not be satisfied. To remedy this situation, new variables must be introduced. A special naming scheme is used for these new variables; each introduced variable is of the form V_{{X_{1},···,X_{n}}} where X_{1}, ⋯, X_{n} appear in G at the start of the algorithm. The intention here is that such a variable represents X_{1} ∩ ⋯ ∩ X_{n}. Thus a variable such as V_{{X,Y,Z}} not only represents X ∩ Y ∩ Z, but also expressions such as V_{{X,Y }} ∩ Z and V_{{Y,Z}} ∩ V_{{X,Z}}. The following algorithm details how this is achieved.

rename each variable X in G into V_{{X}};

repeat exhaustively-apply transfn 6 to G; if transfn 5 is applicable to G

that is, G contains a subexpression of form f(V_{S_{1}}, ⋯, V_{S_{n}}) ∩ f(V_{T_{1}}, ⋯, V_{T_{n}})

then replace it by f(V_{S_{1}∪T_{1}}, ⋯, V_{S_{n}∪T_{n}}) for each i : 1 ≤ i ≤ n do

if V_{S_{i}∪T_{i}} is a new variable in G then add to G the collection {V_{S_{i}∪T_{i}} ⟹ u ∩ w :

V_{S_{i}} ⟹ u ∈ G and V_{T_{i}} ⟹ w ∈ G} endif endfor

endif until neither transfn 5 nor 6 is applicable to G; rename each variable V_{{X}}, X ∈ V, back into X;

The following lemma states the correctness and completeness of this algorithm. The proof is mainly in establishing certain properties of the introduced variables.

Lemma 4 Let G be a standardized set expression grammar containing no projection symbols. Then • the algorithm above terminates when input with G, yielding a term grammar G′, and

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

We now return to the problem of showing that the function ORACLE used in transformation 4 is recursive. We recall that ORACLE(G, X) is true iff X ⟹^{⋆} t for some set expression t which (a) has no projection symbols, and (b) [[t]] ≠ ◯̸. Since t does not contain projection symbols, its derivation from X in G cannot involve a production containing a projection symbol. Hence ORACLE(G, X) iff ORACLE(G′, X) where G′ is the subset of productions from G which do not contain the projection symbol. By lemma 4 (which does not use transformation 4), we can reduce G′ to an equivalent term grammar G′′. Since we can determine whether or not I_{G′′}(X) = ◯̸, we are done.

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

• terminates, yielding a term grammar G, and

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

4.2 Greatest Models

We will transform the problem of explicitly representing the greatest model of a solved form conjunction C into the problem of explicitly representing the least model of a conjunction closely related to C. We begin by defining the dual of a set expresson sexp, denoted dual(sexp), as follows: if sexp is:

• a variable, then dual(sexp) is sexp;

• a constant, say c, then dual(sexp) is the expression Ω_{c};

• ⊥ or ⊤, then dual(sexp) is ⊤ or ⊥ respectively;

• f(t_{1}, ⋯, t_{n}), then dual(sexp) is Ω_{f} ∪ f(dual(t_{1}), ⊤, ⋯, ⊤) ∪ f(⊤, dual(t_{2}), ⋯, ⊤) ∪ ⋯ ∪ f(⊤, ⊤, ⋯, dual(t_{n}));

• f_{(i)}^{−1}(t), then dual(sexp) is f_{(i)}^{−1}(dual(t));

• s ∪ t, then dual(sexp) is dual(s) ∩ dual(t);

• s ∩ t, then dual(sexp) is dual(s) ∪ dual(t) where Ω_{f} (f is a functor or constant) denotes the expression ⋃g(⊤, ⋯, ⊤), where g ranges over all functors and constants different from f^{4}. Now let I be an interpretation, sexp be a set expression and C be a solved form conjunction of set constraints. Define dual(C) = {X = dual(sexp) : X = sexp is an equation in C\} and \overline{I}(X) = HU − I(X). Then

Lemma 5 (a) \overline{I}(dual(sexp)) = HU − I(sexp), and (b) I ⊧ C iff \overline{I} ⊧ dual(C).

Combining lemma 5 and the following algorithm, we obtain Theorem 2 below.

construct dual(C) =

{X = dual(sexp) : X = sexp ∈ C}; run the algorithm in theorem 1 on dual(C) to obtain the term grammar G_{1}; construct C_{1} = {X = ⋃s : X ⟹ s ∈ G_{1}}; construct dual(C_{1}) =

{X = dual(sexp) : X = sexp ∈ C_{1}}; run the algorithm in theorem 1 on dual(C_{1})

to obtain G;

Theorem 2 Let C be a solved form conjunction of set constraints. Then

• the algorithm, when input with C, terminates, yielding a term grammar G;

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

5 Definite Set Constraints

We now apply the algorithms developed in section 4 to the the satisfiability problem for set constraints. First we state

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

The following transformation serves to simplify the left-hand-sides of expressions in a conjunction of definite set constraints.

4In this section we assume for convenience that Σ is finite.

This restriction can be easily lifted.

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

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

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

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

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

• if lm(C′) ⊧ C, then lm(C′) = lm(C).

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

Lemma 7 Let C′ be a conjunction of definite set constraints whose left-hand-sides are either variables or constants. Then

• lm(active(C′)) exists;

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

• if lm(active(C′)) ⊧ C′, then lm(active(C′)) = lm(C′).

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

exhaustively-apply the flattening transfn to C

to obtain C′; run the algorithm in theorem 1 on active(C′)

to obtain grammar G; if I_{G} ⊧ C then output G; else output “unsatisfiable”;

Theorem 3 Let C be a conjunction of definite set constraints. Then

• the above algorithm terminates;

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

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

References

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

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

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

[4] N. Heintze and J. Jaffar, “A Finite Presentation Theorem for Approximating Logic Programs”, draft manuscript (abstract appears in Proc. ACM-POPL-90), November 1989, 56 pp.

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

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

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

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

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

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

Appendix: Some Program Approximation Examples

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

Example 1

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

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

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

2. y := car(x);

3. x := cdr(x);

4. }

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

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

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

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

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

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

Example 2

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

p(a).

p(s^{m}(X)) ← p(X).

p(Y) ← p(s^{n}(Y)).

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

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

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