Chapter 1

Semantic Types for Logic Programs

by Nevin Heintze and Joxan Jaffar

A semantic type represents an approximation to the meaning of a logic program. This paper deals with the relationship between two main formalisms used to define such types. In the first, a set formula is constructed from the program and a type is a distinguished model of this formula. In the second, an adaptation of the immediate consequence operator T_{P} is defined, and a type is some fixpoint of this operator. In this paper, we use variations of these formalisms to obtain a number of different definitions of type. Our main result is that the formalisms are essentially equivalent: a definition of type in one formalism has its counterpart in the other formalism.

1.1 Background

A type is a formalism for describing an approximation of certain aspects of a program. In logic programming, one can distinguish between two kinds of type: that which pertains to the program’s operational model, and that which pertains to the program’s declarative semantics. We characterize the first kind as those which describe properties in terms of program derivations. We characterize the second kind, call them the semantic types, as the types which describe properties in terms of successful program derivations. We now elaborate.

In the former kind of type system, the essential property that is captured is that a derivation step from a well-typed subgoal (that is, a subgoal consistent with the type at hand) can only result in another subgoal which is also well-typed. An example of such a system is [10] where, starting with a definition of type as an annotation of the alphabet, rules were established for constructing well-typed programs and goals. It was then shown that for any such program, type consistency is preserved by a derivation step. A different approach is based directly on program derivations, rather than program syntax. Starting with a distinguished goal, flow analysis or abstract interpretation techniques may be employed to obtain a conservative approximation of the set of possible subgoals that may arise; see [7], [1] for example. Thus, by construction, this approximation has the property that the goals it describes are closed under derivation steps.

A semantic type describes an approximation to the program’s meaning. Typically, this approximation is a conservative approximation to a programs success set. That is, it describes a superset of the (ground) atoms which may succeed. An important property captured by such a type is that any atom which falls outside the type is guaranteed not to have a successful derivation. A central issue with semantic types is the trade-off between two requirements: that a type be a recursive structure and that a type give an accurate approximation.

In the literature, three main approaches have been used to obtain semantic types. The first approach obtains from a program a collection of formulas which describes set-theoretic relationships between the atoms appearing in the program. A type is then defined to be a distinguished model of the formulas. The paper [9] introduced this approach, and gave partial algorithms for extracting a type from the formulas. The second approach uses an adaptation of the definition of the immediate consequence operator T_{P} associated with the program P. This adaptation typically introduces an approximation which ignores argument and/or variable value dependencies. A type is then defined as a fixpoint (or a pre-fixpoint or post-fixpoint) of the resulting function. [14] is an example. The third approach uses flow analysis to infer a semantic type from a program. The algorithms employed are typically based on an abstraction of the underlying domain and an appropriate adaptation of a logic programming operational model. Some examples are [6], [13] and [1].

The relative merits of these three approaches are essentially the following. The first approach presents the type in a closed-form; thus the problem of reasoning about a type can be solved by a decision procedure for the corresponding formulas. The second approach is more declarative in the sense that relationships between the type and the program’s meaning (for example, that the approximation given by the type is indeed conservative) are easier to establish. The third approach has lead to practical algorithms based on iterative fixpoint computations. However, to ensure that these algorithms terminate, the abstract domains employed must be restricted; this in turn imposes a fundamental limitation on accuracy.

The primary concern of this paper is the relationship between the set formula and immediate consequence operator approaches for semantic types^{1}. We do not consider the flow analysis approach essentially because the exact properties of the types inferred are usually dependent on algorithmic details. Thus these types are difficult to characterize in any way other than their algorithmic definition. Consequently, they are generally incomparable with the types from the fixpoint or set formula approaches. In many cases, however, flow analysis approaches employ, in addition to an abstraction of the underlying domain, an approximation which ignores dependencies between arguments. The motivation for this is usually efficiency. In such cases, the set formula and fixpoint approaches can be viewed as an upper bound on the accuracy of the flow analysis approach.

1We do not consider (parametric) polymorphism. Although polymorphic type systems have been developed using variations of the set formula approach [11], a corresponding approach based on an immediate consequence operator appears to be problematic.

In this paper we consider the class of definite logic programs. We first discuss a uniform methodology for obtaining, given a program, a collection of set formulas representing the desired type. From here, we obtain a number of different ways of obtaining such formulas which, in turn, give rise to a number of different types. These types coincide with those appearing in the literature. We then present an alternative framework for obtaining a number of different adaptations of T_{P}. The main theorem proves that the various notions of type obtained via set formulas are respectively equivalent to the various notions of type obtained via adaptations of T_{P}. Formal proofs of the various results are somewhat lengthy and are omitted.

1.2 Preliminaries

We refer to [8] for standard terminology and definitions about pure logic programs P. We assume, with no loss of generality, that no two rules in P have the same variable. Given P, we write Π_{P} and Σ_{P} to respectively denote the finite sets of predicate and function symbols in P. Let HU_{P} and HB_{P} respectively denote the Herbrand universe and base arising from Π_{P} and Σ_{P}. Let P |_{p} denote the rules in P defining the relation p. Where S ⊆ HB_{P}, let S|_{p} denote the subset of S involving the predicate p. A body-only (head-only) variable within a rule is one which does not appear in the head (body) of the rule.

Where e is any expression, var(e) denotes its collection of variables. An atom or term is linear if it contains at most one occurrence of each distinct variable. The symbol ∼ is used to group expressions into a possibly empty sequence or set, this choice being dictated by an obvious context. For example A ← B̃ denotes a rule R whose body atoms are represented by B̃. Writing B̃ ⊆ S, on the other hand, means that each atom in B̃ appears in the set S.

A set expression (s.e.) over an alphabet Δ of functors is either

• a variable in VAR;

• a constant from Δ or one of the special constants ⊥ or ⊤;

• f(t_{1}, ... , t_{n}) where f ∈ Δ is n-ary, n ≥ 1, and t_{1}, ... , t_{n} are s.e.’s • f_{(i)}^{−1}(s) where f ∈ Δ is n-ary, 1 ≤ i ≤ n, and s is a s.e.

• s̄ where s is a s.e.;

• u ⊎ s, u ∪ s, or u ∩ s where u and s are s.e.’s.

A set constraint is of the form s ⊆ t where s and t are set expressions.

Let τ(Δ) denote the set of all (ground) terms over Δ. Let S, S_{1}, ⋯, S_{n} be subsets of τ(Δ) and let f be an n-ary functor, n ≥ 1. Then f(S_{1}, ⋯, S_{n}) denotes the set

{f(s_{1}, ⋯ s_{n}) : s_{1} ∈ S_{1}, ⋯, s_{n} ∈ S_{n}}.

Define the ith projection of f, call it f_{(i)}^{−1}, by

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

The following defines a tuple closure operation ⋆ on sets of ground terms:

S^{⋆} =^{def} {c : c is a constant in S} ∪ ⋃_{f} f ((f_{(1)}^{−1}(S))^{⋆}, ⋯, (f_{(arity(f))}^{−1}(S))^{⋆})

where f ranges over the symbols whose arity, denoted arity(f), is non-zero.

An interpretation I is a mapping from each variable in VAR into a subset of τ(Δ). An interpretation can be uniquely extended to map from set expressions to subsets of τ(Δ) as follows. If t is:

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

• a constant symbol c, then I(t) is {c};

• a special constant ⊥ or ⊤, then I(t) is ∅ or τ(Δ) respectively;

• f(t_{1}, ... , t_{n}) where n ≥ 1, then I(t) is f(I(t_{1}), ... , I(t_{n}));

• f_{(i)}^{−1}(s), then I(t) is f_{(i)}^{−1}(I(s));

• s̄, then I(t) is τ(Δ) − I(s);

• u ⊎ s or u ∪ s, then I(t) is (I(u) ∪ I(s))^{⋆} or I(u) ∪ I(s) respectively;

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

A model of a collection C of set constraints is an interpretation of C which evaluates to true. Where I_{1} and I_{2} are interpretations, I_{1} ⊆ I_{2} denotes that I_{1}(X) ⊆ I_{2}(X) for all variables X. We use lm(C) and gm(C) to respectively denote the least and greatest models of C (ordered according to ⊆).

1.3 Set Formulas

The use of set formulas to model program behavior dates back to at least [12] which infers data structure definitions for a lisp-like language. In logic programming, set formulas were used in [9] to obtain an approximation of the success set of a program. We begin this section with an outline of the method for constructing such formulas corresponding to a program. We then introduce refinements to this basic method.

The set formulas constructed below are intended to describe the success set of a program P. To begin, we introduce a distinguished set of variables called type variables which have the form Υ_{p} where p is a predicate symbol in P. By construction, any model of these formulas will map each type variable Υ_{p} into a set of ground atoms. Consequently, a model of the set formulas defines an interpretation of a program P as the union of the sets corresponding to the type variables, that is:

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

In what follows, we will sometimes identify a model of set formulas with a subset of HB_{P} in the sense just described. We now proceed with the construction of a set formula corresponding to P.

First obtain, for each predicate symbol p in Π_{P}, a head-formula of the form

Υ_{p} ⊆ H_{p,1} ⊎ H_{p,2} ⊎ ⋯ ⊎ H_{p,n_{p}}

where H_{p,1}, ⋯, H_{p,n_{p}} denote the head-atoms in P |_{p}. Then obtain, for each body atom q(t̃) in P, a body-formula of the form

q(t̃) ⊆ Υ_{q}.

An interpretation and model for such set formulas is essentially the same as those given for set constraints in the previous section. Note, however, that each type variable is assigned a subset of HB_{P} while each program variable is assigned a subset of HU_{P}. Consider an example program P:

                          {p(a). \atop p(f(X)) :- p(X).}

The set formula constructed from P is

\begin{aligned}Υ_{p} & ⊆ & p(a) ⊎ p(f(X)) \\ p(X) & ⊆ & Υ_{p}. \end{aligned}

The greatest model of the above formula gives Υ_{p} = {p(f^{n}(a)) : n ≥ 0}, and happens to capture exactly the meaning of the program. The least model, on the other hand, is the trivial model which maps all variables into ∅. (This is true in general for the formulas constructed above; the least model of these formulas is therefore not useful for defining program approximations).

The formulas in [9] were essentially constructed as indicated above, and the distinguished model sought was the greatest model. This choice is not always appropriate, as the following example shows. Consider augmenting the above program with the rule p(Z) :- p(Z). The corresponding set formula now becomes

\begin{aligned}Υ_{p} & ⊆ & p(a) ⊎ p(f(X)) ⊎ p(Z) \\ p(X) & ⊆ & Υ_{p} \\ p(Z) & ⊆ & Υ_{p}. \end{aligned}

While the meaning the program has not changed with the addition of the extra rule, the greatest model of the set formula now assigns HB_{P} to Υ_{p}. That is, the greatest model gives no useful information about the program.

We now present a refinement to the scheme above by considering a change not in the choice of model, but in the set formulas themselves. Specifically, we replace set inclusion by set equality and appropriately modify the right-hand-sides of the bodyformulas. Let P be a program with N ≥ 1 rules. First define that HEADONLY_{P} is the set of equations

{Z = ⊤ : Z is a head-only variable in P }

and define that HEAD_{P} (p), is

Υ_{p} = H_{p,1} ⊎ ⋯ ⊎ H_{p,n_{p}}

where H_{p,1}, ⋯, H_{p,n_{p}} denote the head atoms in P |_{p}^{2}. Now, for any 1 ≤ i ≤ N, let the variables in the i^{th} rule be X_{1}, X_{2}, ⋯, X_{k} where k ≥ 0, and let the body of this rule be the sequence of atoms p_{1}(t̃_{1}), ⋯, p_{n}(t̃_{n}) where n ≥ 0. Then, where x_{1}, ⋯, x_{k} is a sequence of distinct new variables, obtain a new sequence p_{1}(t̃_{1}′), ⋯, p_{n}(t̃_{n}′) by replacing each variable X_{i} by the corresponding new variable x_{i}. Now define that BODY_{P} (i), 1 ≤ i ≤ N, is the conjunction of the following equations:

X_{j} = {x_{j} : ∃x_{1} ⋯ x_{j−1}x_{j+1} ⋯ x_{k} ( p_{1}(t̃_{1}′) ∈ Υ_{p_{1}} ; p_{2}(t̃_{2}′) ∈ Υ_{p_{2}} ; ⋮ ; p_{n}(t̃_{n}′) ∈ Υ_{p_{n}} )} , 1 ≤ j ≤ k.

2When P |_{p} is the empty set, HEAD_{P} (p) is defined to be Υ_{p} =⊥.

We are now in a position to define that the set formula SF_{P} corresponding to a given program P is the conjunction of the following equations:

HEADONLY_{P} ∪ ( ⋃_{p∈Π_{P}} HEAD_{P} (p)) ∪ ( ⋃_{1≤i≤N} BODY_{P} (i)) .

Using the previous example program P

                          p(a).
                          p(f(X)) :- p(X).
                          p(Z) :- p(Z).

the set formula SF_{P} is

\begin{aligned}Υ_{p} & = & p(a) ⊎ p(f(X)) ⊎ p(Z), \\ X & = & \{x : p(x) ∈ Υ_{p}\}, \\ Z & = & \{z : p(z) ∈ Υ_{p}\}. \end{aligned}

The definition of an interpretation and model for such set formulas is obtained by extending the definition given previously in an obvious way. Note, however, that the symbol ⊤ is always interpreted as HU_{P}.

Given any program P, it can be proved that all models of SF_{P} define conservative approximations to the meaning of P. It is therefore appropriate to choose the least model lm(SF_{P}) (which always exists) as our distinguished model. In the above example, lm(SF_{P}) describes the exact meaning of P, {p(f^{n}(a)) : n ≥ 0}. We remark that the greatest models of SF_{P} correspond to the greatest models of the formulas used in [9] which are described in the first part of this section.

A variation to the construction of SF_{P} described above is obtained by replacing all occurrences of the symbol ⊎ by the symbol ∪. To distinguish between these two variations of SF_{P}, we now introduce the notations SF_{P} (⊎) and SF_{P} (∪). One immediate observation is that the least model of SF_{P} (∪) is a better approximation to the meaning of P than SF_{P} (⊎). Consider, for example, the program consisting of just the two facts p(a, b) and p(b, a). Here SF_{P} (⊎) and SF_{P} (∪) would respectively be

Υ_{p} = p(a, b) ⊎ p(b, a) and Υ_{p} = p(a, b) ∪ p(b, a),

giving the least models

Υ_{p} = {p(a, b), p(b, a), p(a, a), p(b, b)} and Υ_{p} = {p(a, b), p(b, a)}

respectively. We now define yet another variation on the construction methods for SF_{P} (⊎) and SF_{P} (∪). We proceed first by example: let P be the program

                          p(a, b).
                          p(b, a).
                          q(X) :- p(X, X).

The new set formula is:

\begin{aligned}Υ_{p} & = & p(a, b) ∪ p(b, a), \\ Υ_{q} & = & q(X), \\ X & = & \{x : ∃x′p(x, x′) ∈ Υ_{p}\} ∩ \{x : ∃x′p(x′, x) ∈ Υ_{p}\}. \end{aligned}

Consider the difference between this formula and SF_{P} (∪), that is, consider the third equation above. In SF_{P} (∪), this equation appears as X = {x : p(x, x) ∈ Υ_{p}}, whereas in the new formula, a set is constructed for each occurrence of the variable X. The final set for X is then determined by the intersection of the values corresponding to the various occurrences. Note that the least model of the formula above gives Υ_{q} = {q(a), q(b)}, whereas the least model of SF_{P} (∪) gives Υ_{q} = ∅.

We now extend our notation SF_{P} (⊎) and SF_{P} (∪) to SF_{P} (⊎, var), SF_{P} (⊎, occ), SF_{P} (∪, var) and SF_{P} (∪, occ) to distinguish (a) the use of ⊎ or ∪ in the headformulas, and (b) the treatment of each variable as one entity or in an occurrencebased way. We now formally define SF_{P} (⊎, occ); the definition of SF_{P} (∪, occ) will then be obtained by simply replacing each occurrence of ⊎ by ∪.

Fix i: 1 ≤ i ≤ N. Let the i^{th} rule of P be H ← p_{1}(t̃_{1}), ⋯, p_{n}(t̃_{n}) where n ≥ 0 and let B̃ denote p_{1}(t̃_{1}), ⋯, p_{n}(t̃_{n}). Fix on some variable X appearing in B̃, and let m denote the number of occurrences of X in B̃. Let the remaining variables in B̃ be Y_{1}, ⋯, Y_{k} and let ỹ = y_{1}, ⋯, y_{k} be a corresponding sequence of distinct new variables. Then, obtain a new sequence p_{1}(t̃_{1}′), ⋯, p_{n}(t̃_{n}′) by replacing each occurrence of a variable in p_{1}(t̃_{1}), ⋯, p_{n}(t̃_{n}) as follows:

1. replace the jth occurrence of X, 1 ≤ j ≤ m, by a new variable x_{j}, and

2. replace every occurrence of Y_{l}, 1 ≤ l ≤ k, by the corresponding variable y_{l}.

Now define BODY_{P}^{occ}(i)|_{X} to be the equation:

X = \begin{aligned}& \{x_{1} : ∃x_{2}x_{3} ⋯ x_{m}∃ỹ( p_{1}(t̃_{1}′) ∈ Υ_{p_{1}} ; ⋮ ; p_{n}(t̃_{n}′) ∈ Υ_{p_{n}} )\} \\ ∩ & \{x_{2} : ∃x_{1}x_{3} ⋯ x_{m}∃ỹ( p_{1}(t̃_{1}′) ∈ Υ_{p_{1}} ; ⋮ ; p_{n}(t̃_{n}′) ∈ Υ_{p_{n}} )\} \\ ∩ & ⋯ \\ ∩ & \{x_{m} : ∃x_{1} ⋯ x_{m−1}∃ỹ( p_{1}(t̃_{1}′) ∈ Υ_{p_{1}} ; ⋮ ; p_{n}(t̃_{n}′) ∈ Υ_{p_{n}} )\} \end{aligned}

Next define that BODY_{P}^{occ}(i) is the conjunction of the equations BODY_{P}^{occ}(i)|_{X} over the variables X in B̃. Finally, define that SF_{P} (⊎, occ) is the conjunction of the following equations:

HEADONLY_{P} ∪ ( ⋃_{p∈Π_{P}} HEAD_{P} (p)) ∪ ( ⋃_{1≤i≤N} BODY_{P}^{occ}(i))

where HEADONLY_{P} and HEAD_{P} (p) are as defined before.

In summary for this section, we have defined four different ways to construct, given a logic program P, a set formula whose least model represents the type of P. The resulting four classes of set formulas: SF_{P} (⊎, var), SF_{P} (⊎, occ), SF_{P} (∪, var) and SF_{P} (∪, occ), differed only in whether or not set-union was augmented with a tuple-closure operation, and in whether or not program variables were treated in an occurrence-based way. Informally, these formulas are intended to be natural closed-form representations of conservative approximations to the program’s meaning. Formally, we have

Lemma 1 For any logic program P,

T_{P} ↑ω ⊆ lm(SF_{P} (∪, var))
⊆ lm(SF_{P} (∪, occ))
⊆ lm(SF_{P} (⊎, var))
= lm(SF_{P} (⊎, occ)).

1.4 Fixpoint Operators

We give three different adaptations of the immediate consequence function T_{P} associated with a program P. These, in turn, define three different kinds of types. We begin by recalling the standard T_{P} operator:

T_{P} (I) =^{def} {Hθ : H ← B̃ ∈ P, and B̃θ ⊆ I} .

Observe that this definition consists of three main components: (i) the collection of unifiers (for example, the collection of θ’s above) corresponding to the body atoms of a rule, (ii) the application of these unifiers to the head of a rule, and (iii) the joining of the resulting sets, one from each rule head. The adaptations of T_{P} considered in this section shall be obtained by replacing some of these components by approximate counterparts.

First consider the fixpoint operator defined in [14]. This function, call it Y_{P}, is defined to be the tuple closure of the T_{P} function. That is:

Y_{P} (I) =^{def} (T_{P} (I))⋆ .

Thus components (i) and (ii) of the definition of T_{P} remain unchanged in Y_{P}. Component (iii), the joining of head atoms, is now augmented with a tuple closure operation. For example, if P were

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

then T_{P} ↑ω is {p(f(a, b)), p(f(b, a)), s(f(a, b)), s(f(b, a))}, whereas Y_{P} ↑ω is the larger set

\{ \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} \} .

Note that in the construction of Y_{P} ↑ω the approximation operator ⋆ is applied after each application of T_{P}. Thus, for example, it is generally not the case that Y_{P} ↑ω = (T_{P} ↑ω)⋆.

Recently, in [4], a more accurate approximate consequence operator was studied. This operator, call it τ_{P}, was obtained by first defining an approximation operator A which is applied to a collection of unifiers to obtain a set substitution. Such a substitution is a mapping from terms into sets of ground terms, and it can be defined as the natural extension of a mapping from variables into sets of ground terms. Thus, for example, if α were the set substitution given by the mapping {[X ↦ {a, c}, Y ↦ {b, d}]}, then p(X, Y)α denotes the set {p(a, b), p(a, d), p(c, b), p(c, d)}.

Now let Θ be a collection of ground substitutions over variables X̃. Define that AX̃(Θ) is the single set substitution which maps each variable X_{i} ∈ X̃ into the set {X_{i}θ : θ ∈ Θ}, and it is undefined on all other variables^{3}. The operator τ_{P} can now be defined as follows:

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

Intuitively, τ_{P} first collects together the ground substitutions for a rule which instantiate the body atoms into elements in I. From these substitutions, it collects all the possible values that each variable may be instantiated to, ignoring relationships between these variables. A set substitution is then defined as the mapping from each variable into the corresponding collected set of values, and finally, this set substitution is applied to the head of the rule.

3AX̃(∅) is a special set-substitution which maps every term into ∅. If however Θ ≠ ∅ and X̃ is empty, AX̃(Θ) is the set-substitution which maps every ground term t into {t}.

Note that the type of closure used here is different from the tuple closure operation used to define Y_{P}. In Y_{P}, the closure occurred at the level of arguments of predicate and function symbols so that, for example, tuple closure augments the set {p(a, b), p(c, d)} with the elements p(a, d) and p(c, b). In τ_{P}, closure occurs at the level of variables, so that, the unifiers {[X ↦ a, Y ↦ b], [X ↦ c, Y ↦ d]}, for example, are approximated by the set substitution {[X ↦ {a, c}, Y ↦ {b, d}]}.

Returning to the previous example program P, τ_{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} \} .

An alternative definition of an approximate consequence operator is obtained by using substitutions which are defined to be mappings from each occurrence of a variable, as opposed to mappings from each variable. Toward this end, define a occurrence-based substitution to be of the form

{X_{j_{1}}^{(i_{1})}/t_{1}, X_{j_{2}}^{(i_{2})}/t_{2}, ⋯ X_{j_{n}}^{(i_{n})}/t_{n}}

where n ≥ 1, the t_{1}, ⋯, t_{n} are terms, X̃ = X_{j_{1}}, ⋯ X_{j_{n}} is a sequence of not necessarily distinct variables, and {i_{1}, ⋯, i_{n}} is a collection of positive numbers such that i_{k} identifies a specific occurrence, the i_{k}^{th} one, of the variable X_{j_{k}}. Application of a occurrence-based substitution on a sequence of terms or atoms is defined in the obvious way. For example p(X), q(X, Y){X^{(1)}/a, X^{(2)}/b, X^{(3)}/c, Y^{(1)}/d, Y^{(2})/e} is p(a), q(b, d). An occurrence-based substitution θ is ground on a sequence of terms or atoms D̃ if θ grounds all variable occurrences in occ(D̃), the set of variable occurrences in D̃. We can now adapt the A approximation operator defined above so that it maps collections of ground occurrence-based substitutions with respect to D̃ as follows: A_{occ(D̃)}(Θ) maps each variable X in var(D̃) into the set:

{ ⋂_{X^{(i)}∈occ(D̃)}{X^{(i)}θ : θ ∈ Θ}}

and is undefined if X does not appear in D̃. We now define yet another operator Z_{P} in a similar way as τ_{P}, except that occurrence-based substitutions θ are now used instead of normal substitutions, as follows:

Z_{P} (I) =^{def} \left\{{a : a ∈ Hα where H ⟵ B̃ ∈ P, and \atop α = A_{occ(B̃,H)}(\{θ : B̃θ ⊆ I\})}\right\}

where θ ranges over the ground occurrence-based substitutions on the sequence B̃, H. Using the above program P once again, Z_{P} ↑ω is

\{ \begin{matrix}p(f(a, b)), p(f(b, a)) \\ r(a), r(b) \\ s(f(a, a)), s(f(a, b)), s(f(b, a)), s(f(b, b)) \end{matrix} \} .

The relative accuracies of the three operators indicated by this example program are true in general. That is, Z_{P} gives rise to an approximate meaning of a program which is, in general, more accurate than Y_{P} but less accurate than τ_{P}. The following lemma is easy to verify.

Lemma 2 For any logic program P,

T_{P} ↑ω ⊆ τ_{P} ↑ω
⊆ Z_{P} ↑ω
⊆ Y_{P} ↑ω.

1.5 Main Results

We now prove that the formulation of types via set formulas is essentially equivalent to the formulation of types using fixpoint operators. Specifically, the desired result is that for any program P,

• a model of SF_{P} (⊎, var) is a fixpoint of Y_{P}, and vice versa;

• a model of SF_{P} (∪, occ) is a fixpoint of Z_{P}, and vice versa;

• a model of SF_{P} (∪, var) is a fixpoint of τ_{P}, and vice versa.

However, the simple program p(a) :- p(b). is a counter-example. A closer observation reveals that the falsity of the desired result can be isolated to programs which have very specific properties^{4}. We deal with these special properties now.

Let I be a Herbrand interpretation. A rule R is redundant w.r.t. I if T_{{R}}(I) = ∅. A program P is redundant if it contains a rule which is redundant w.r.t. T_{P} ↑ω. A rule is degenerate if its head atom is ground. A program is degenerate if it contains a degenerate rule.

Theorem 1 Let P be a program which is \underline{either} non-redundant or non-degenerate, and let I ⊆ HB_{P}. Then

• I models SF_{P} (∪, var) iff I is a fixpoint of τ_{P};

• I models SF_{P} (∪, occ) iff I is a fixpoint of Z_{P}; • I models SF_{P} (⊎, var) iff I is a fixpoint of Y_{P};

4We could modify the definitions of the various set formulas so that their models correspond to fixpoints over arbitrary programs. This would, however, make the construction of a set formula corresponding to a program slightly more complex.

• I models SF_{P} (⊎, occ) iff I is a fixpoint of Y_{P}.

One important application of this theorem is that fixpoint types can be computed using algorithms for the corresponding set formulas. Even though the theorem is stated conditionally in terms degeneracy and redundancy, it is in fact applicable for all programs. Specifically, suppose that an algorithm computes a representation of SF(∪, var) given an arbitrary program P. We assume that one can determine whether or not a sequence of atoms B̃ has a ground instance in the representation. We can now apply the above theorem showing how to obtain a representation of τ_{P} ↑ω.

If P is non-degenerate (and this is an easily tested syntactic condition), then the theorem implies that the representation we have is in fact the representation we seek. If P were degenerate, then we can apply the following algorithm.

Set P_{1} to the subset of P containing just the non-degenerate rules. Compute a representation of SF_{P_{1}}(∪, var). Now, for each degenerate rule in P − P_{1}, determine if its body atoms have a ground instance in the representation. If so, add the rule to P_{1}. Let P_{2} denote the resultant set of rules, and repeat this process to obtain P_{3}, P_{4}, etc. In other words, to compute P_{i}, i ≥ 2, use a representation of SF_{P_{i−1}}(∪, var), and construct P_{i} from P_{i−1} by adding those rules in P which have a ground instance in SF_{P_{i−1}}(∪, var). Clearly the process can be terminated when P_{i} is the same as P_{i−1} for some i, and the resulting representation is indeed that of τ_{P} ↑ω.

An alternative approach is to rewrite each rule R in P as follows. Let Z be a new variable, then add an extra argument, filled with the variable Z, to each atom in R. For example p(a) :- p(b). would be rewritten to p(a, Z) :- p(b, Z). The resulting program, call it P′, is non-degenerate, and, by systematically ignoring the extra argument, it can be shown that P′ is essentially equivalent to P with respect to fixpoint and set formula constructions. Therefore, to compute a representation of SF_{P} (∪, var), it suffices to compute a representation of SF_{P′}(∪, var), and then delete the extra argument from this representation.

In summary, our theorem proves that the formulation of types via set formulas is equivalent to the formulation of types using using fixpoint operators in the context of programs P which were either non-degenerate or non-redundant. The theorem, however, is essentially applicable over arbitrary programs because it is straightforward to augment any algorithm which computes a representation of the least model of a given set formula so that it computes a representation of the least fixpoint of the corresponding fixpoint operator.

1.6 Concluding Discussion

We have established an equivalence between two formalisms for defining semantic types, and three specific types were studied. An additional way to study the relative properties of these three types is obtained by program transformation. Given a program P, two kinds of transformation are possible. We briefly describe their properties here, but omit the full details.

• We may obtain a program P′ such that Z_{P′}↑ω and τ_{P′}↑ω coincide and such that Z is preserved, that is, Z_{P} ↑ω = Z_{P′}↑ω = τ_{P′}↑ω. This transformation is essentially the exhaustive application of the replacement steps such as: if H ← A, p(X, X), B is a rule, then replace this rule by H ← A, p(X, X_{1}), p(X_{2}, X), B where X_{1} and X_{2} are new variables. Note also that SF_{P} (∪, occ) is equivalent to SF_{P′}(∪, var), and so this program transformation can be used to obtain an alternative definition for SF_{P} (∪, occ).

• We may obtain a program P′ such that τ_{P′}↑ω and T_{P′}↑ω coincide and such that τ is preserved, that is, τ_{P} ↑ω = τ_{P′}↑ω = T_{P′}↑ω. This transformation is essentially the exhaustive application of the replacement steps such as: if q(X, Y) ← p(X, Y) is a rule, then replace this rule by p(X, Y) ← p(X, Z_{1}), p(Z_{2}, Y), where Z_{1} and Z_{2} are new variables.

Transformations are also possible on set formulas. In fact, it is possible to transform both SF(∪, occ) and SF(⊎, var) so that they become just set constraints (that is, it is possible to eliminate the quantifiers). This process, called “flattening”, is useful for two reasons. First, it leads to constraints of a simpler and more intuitive structure. Second, it reduces the problem of reasoning about set formulas to the simpler problem of reasoning about set constraints.

We now conclude with a brief summary of the three kinds of semantic type we have described.

• τ_{P} ↑ω or lm(SF_{P} (∪, var)):

This is the most accurate type of the three. It has been shown to be a recursive set [4], and further, there are algorithms to compute a representation of the type in the form of a regular tree grammar (in the sense of nondeterministic tree automata; see e.g. [2]). Also, it is possible to transform P to a program P′ such that τ_{P} ↑ω = T_{P′}↑ω. However, it is not in general possible to apply flattening to the set formula SF_{P} (∪, var) to reduce it to set constraints.

• Z_{P} ↑ω or lm(SF_{P} (∪, occ)):

This is the type of intermediate accuracy. That these types are recursive can be shown using transformations on either the program, or the corresponding set formulas. First, it is possible to transform P to a program P′ such that Z_{P} ↑ω = τ_{P′}↑ω. Hence we can use the algorithm for τ_{P} ↑ω. Alternatively, the flattening procedure can be applied to SF_{P} (∪, occ) to reduce these set formulas to set constraints, and these constraints can be solved by an algorithm from [5]. Thus these types can also be represented by regular tree grammars.

• Y_{P} ↑ω or lm(SF_{P} (⊎, var)) or lm(SF_{P} (⊎, occ)): This is the least accurate type of the three. The question of whether this type is recursive is still open. Although it is possible to apply the flattening procedure to SF_{P} (⊎, var) to reduce these set formulas to set constraints, algorithms do not exist for the resulting constraints. It is conjectured that these types can be represented by the subclass of regular tree grammars corresponding to deterministic root-to-frontier tree automata. This type has, however, been shown to useful in a type-checking system [14].

Finally, we remark that the definitions of set formulas may be weakened so as to obtain different kinds of types. Specifically, we can replace = with ⊇ or ⊆ in the head equations, to obtain post- and pre-fixpoints of the corresponding operators. An earlier manuscript [3] used this variation to define types for notions such as specializing a program’s meaning, and run-time type consistency.

1.7 Acknowledgements

We thank Michael Maher for his comments.

16 CHAPTER 1. SEMANTIC TYPES FOR LOGIC PROGRAMS

Bibliography

[1] M. Bruynooghe, G. Janssens, A. Callebaut and B. Demoen, “Abstract Interpretation: Towards the Global Optimisation of PROLOG Programs”, Proceedings 4^{th} IEEE Symposium on Logic Programming, pp 192 - 204, September 1987.

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

[3] “Elementary Logic Programming Types”, draft manuscript, July 1987.

[4] N. Heintze and J. Jaffar, “A Finite Presentation Theorem for Approximating Logic Programs”, IBM Research Report RC 16089 (#71415), 6 Sept. 90. (An extended abstract appears in Proc. ACM-POPL-90.)

[5] N. Heintze and J. Jaffar, “A Decision Procedure for a Class of Set Constraints”, forthcoming CMU techical report, February 1991. (An extended abstract appears in Proc. IEEE LICS-90.)

[6] T. Kanamori and K. Horiuchi, “Type Inference in PROLOG and its Applications”, Proc. 9^{th} Intl. Joint Conf. on Artificial Intelligence, Vol. 2, pp 704 - 707, 1985.

[7] F. Kluzniak, “Type Synthesis for Ground PROLOG”, Proceedings 4^{th} Intl. Conf. on Logic Programming, MIT Press, pp 788 - 816, July 1987.

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

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

[10] A. Mycroft and R.A. O’Keefe, “A Polymorphic Type System for PROLOG”, Artificial Intelligence 23, pp 295 - 307, 1985.

[11] C. Pyo and U.S. Reddy, “Inference of Polymorphic Types for Logic Programs” Logic Programming, Proceedings of the North American Conference, 1989, MIT Press, pp 1115 - 1134, October, 1989.

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

18 BIBLIOGRAPHY

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