arXiv:cs/0612063v1 [cs.PL] 12 Dec 2006

Under consideration for publication in Theory and Practice of Logic Programming

1

Improving Precision of Type Analysis
Using Non-Discriminative Union
LUNJIN LU
Oakland University, Rochester, MI 48309, USA.
(e-mail: lunjin@acm.org)
submitted 10 February 2005; revised 28 August 2006; accepted 11 December 2006

Abstract
This paper presents a new type analysis for logic programs. The analysis is performed
with a priori type deﬁnitions; and type expressions are formed from a ﬁxed alphabet of
type constructors. Non-discriminative union is used to join type information from diﬀerent sources without loss of precision. An operation that is performed repeatedly during
an analysis is to detect if a ﬁxpoint has been reached. This is reduced to checking the
emptiness of types. Due to the use of non-discriminative union, the fundamental problem
of checking the emptiness of types is more complex in the proposed type analysis than
in other type analyses with a priori type deﬁnitions. The experimental results, however,
show that use of tabling reduces the eﬀect to a small fraction of analysis time on a set of
benchmarks.
KEYWORDS: Type analysis, Non-discriminative union, Abstract interpretation, Tabling

1 Introduction
Types play an important role in programming. They make programs easier to understand and help detect errors. There has been much research into types in logic
programming. A type checker requires the programmer to declare types for each
predicate in the program and verifies if the program is consistent with the declared
types (Aiken and Lakshman 1994; Dart and Zobel 1992a; Fages and Coquery 2001;
Frühwirth et al. 1991; Mycroft and O’Keefe 1984; Reddy 1990; Yardeni et al. 1991;
Yardeni and Shapiro 1991). A type analysis derives types for the predicates or
literals in the program from the text of the program (Gallagher and Puebla 2002;
Charatonik and Podelski 1998; Codish and Lagoon 2000; Gallagher and de Waal
1994; Heintze and Jaffar 1990; Heintze and Jaffar 1992; Lu 1998; Mishra 1984;
Saglam and Gallagher 1995; Zobel 1987).
This paper presents a new type analysis that infers types with a priori type definitions which determine possible types and their meanings. Types are formed from
type constructors from a fixed alphabet. This is in contrast to those type analyses that generate type definitions during analysis. Both kinds of type analysis are
useful. An analysis that generates type definitions may be favored in compile-time

2

Lunjin Lu

optimizations and program transformations whilst an analysis with a priori type
definitions may be preferred in interactive programming tools such as debuggers
because inferred types are easier for the programmer to understand.
A number of factors compromise the precision of previous type analyses with
a priori type definitions. Firstly, they only allow deterministic type definitions. A
function symbol cannot occur more than once in the definition of the same type.
A type then denotes a tree language recognized by a deterministic top-down tree
automaton (Comon et al. 2002) and hence called a deterministic type. The restriction to deterministic type definitions allows fast propagation of type information.
However, it causes loss of precision because of the limited power of deterministic
types. The same restriction also prevents many natural typings. For instance, these
two type rules f loat_ + (integer, f loat) and f loat_ + (f loat, f loat) violate the
restriction. Some previous work even disallows function overloading (Horiuchi and
Kanamori 1988; Kanamori and Horiuchi 1985; Kanamori and Kawamura 1993),
which makes it hard to support built-in types. For instance, Prolog has built-in
type atom that denotes the set of atoms. Without function overloading, atoms such
as [ ] cannot be a member of another type, say list . Secondly, the type languages
in previous type analyses with a priori type definitions do not include set union as
a type constructor. The denotation of the join of two types can be larger than the
set union of their denotations. For instance, the join of list (integer) and list (f loat)
is list (number). Let or be a type constructor that is interpreted as set union. Then
list (number) is a super-type of or(list (integer), list (f loat)) since the list [1, 2.5]
belongs to the former but not the latter. Should non-deterministic type definitions
be allowed, there is also a need to use set intersection as a type constructor as explained in Section 2. Finally, previous type analyses with a priori type definitions
describe a set of substitutions by a single variable typing which maps variables of
interest into types. The least upper bound of two variable typings is performed
point-wise, effectively severing type dependency between variables.
Our type analysis aims to improve precision by eliminating the above mentioned
factors. It supports non-deterministic type definitions, uses a type language that
includes set union and intersection as type constructors and describes a set of substitutions by a set of variable typings. All these help improve analysis precision. On
the other hand, they all incur performance penalty. However, experimental results
with a prototype implementation show that tabling (Warren 1992) reduces the time
increase to a small fraction on a suite of benchmark programs. Our type analysis is
presented as an abstract domain together with a few primitive operations on the domain. The domain is presented for an abstract semantics that is Nilsson’s abstract
semantics (Nilsson 1988) extended to deal with negation and built-in predicates.
The primitive operations on the domain can be easily adapted to work with other
abstract semantics such as (Bruynooghe 1991).
The remainder of the paper is organized as follows. Section 2 provides motivation
behind our work with some examples and Section 3 briefly presents the abstract
semantics along with basic concepts and notations used in the remainder of the
paper. Section 4 is devoted to types — their definitions and denotations. Section 5
presents the abstract domain and Section 6 the abstract operations. In Section 7,

Improving Precision of Type Analysis Using Non-Discriminative Union

3

we present a prototype implementation of our type analysis and some experimental
results. Section 8 compares our type analysis with others and Section 9 concludes.
An appendix contains proofs.

2 Motivation
This section provides motivation behind our type analysis via examples. The primary operations for propagating type information are informally illustrated; and
the need for using set union and intersection as type constructors is highlighted.
Example 2.1
This example demonstrates the use of set union as a type constructor. Consider the
following program and type rules.
p(Z) ←

2

X =a

←

1

p(Z)

list (β)
list (β)

3,Y

6.

= 2.5

4

, Z = cons(X, cons(Y, nil))

5.

% query

_ nil

_ cons(β, list (β))

The two type rules define lists. They state that a term is of type list (β) iff it is either
nil or of the form cons(X, Y ) such that X is of type β and Y of type list (β). Type
rules are formally introduced in Section 4. The program has been annotated with
circled numbers to identify relevant program points for the purpose of exposition.
The type analysis can be thought of as an abstract execution that mimics the
concrete (normal) execution of the program. A program state in the concrete execution is replaced with an abstract one that describes the concrete state. The abstract
states are type constraints.
Suppose that no type information is given at program point 1 — the start point
of the execution. This is described by the type constraint µ1 = true. The execution
reaches program point 2 with the abstract state µ2 = true. The abstract state
at program point 3 is µ3 = (X ∈ atom) which states that X is of type atom.
The abstract state at program point 4 is µ4 = (X ∈ atom) ∧ (Y ∈ float ). The
abstract execution of Z = cons(X, cons(Y, nil)) in µ4 obtains the abstract state
µ5 at program point 5 . The computation of µ5 needs some explanation. The two
terms that are unified have the same type after the unification. Since µ4 does not
constrain Z, there is no type information propagated from Z to either X or Y . The
type for Z in µ5 equals the type of cons(X, cons(Y, nil)) in µ4 which is computed in
a bottom-up manner. To compute the type for nil, we apply the type rule for nil/0.
The type rule states that nil is of type list (β) for any β. Thus, the most precise
type for nil is list (0) where the type 0 denotes the empty set of terms. We omit the
process of computing the type list (float ) for cons(Y, nil) in µ4 since it is similar to
the following. To compute the type for cons(X, cons(Y, nil)), we apply the type rule
for cons/2. The right hand side of the type rule is cons(β, list (β)). We first find the
smallest value for β such that β is greater than or equal to atom — the type for X in

4

Lunjin Lu

µ4 and the smallest value for β such that list (β) is greater than or equal to list (float )
— the type for cons(Y, nil) in µ4 . Those two values are respectively atom and float
and their least upper bound is or(atom, float ). Replacing β with or(atom, float ) in
the left hand side of the type rule gives the most precise type list (or(atom, float ))
for cons(X, cons(Y, nil)) in µ4 . Conjoining Z ∈ list (or(atom, float )) with µ4 results
in µ5 = ((X ∈ atom) ∧ (Y ∈ float ) ∧ (Z ∈ list (or(atom, float )))). The abstract state
at program point 6 is µ6 = (Z ∈ list (or(atom, float ))) which is obtained from µ5
by projecting out type constraints on X and Y .
The existence of the type constructor or helps avoid approximations. Without it,
the least upper bound of atom and float is 1 which denotes the set of all terms.
Note that the collection of type rules is fixed during analysis.
When two or more type rules are associated with a single function symbol, there
is also a need to use set intersection as a type constructor. The following example
illustrates this point.
Example 2.2
Suppose that types are defined by the following four type rules.
list (β)
list (β)
tree(β)
tree(β)

_ nil

_ cons(β, list (β))
_ nil

_ node(tree(β), β, tree(β))

Consider the problem of computing the type for cons(X, nil) in the abstract state
µ = (X ∈ integer ).
There are two type rules for nil/0. The type rule list (β)_nil states that nil
belongs to list (β) for any β. The most precise type for nil that can be inferred
from this rule is list (0). Similarly, the most precise type for nil that can be inferred
from the type rule tree(β)_nil is tree(0). Thus, the most precise type for nil is
and(list (0), tree(0)) where and is a type constructor that denotes set intersection.
To compute the type for cons(X, nil), we apply the type rule for cons/2. Its
right hand side is cons(β, list (β)). We first find the smallest value for β such that
β is greater than or equal to integer — the type for X in µ. The value is integer .
We then find the smallest value for β such that list (β) is greater than or equal
to and(list (0), tree(0)) — the type for nil in µ. This is done by matching list (β)
with list (0) and with tree(0) and intersecting values for β obtained from these
two matches. The first match results in 0. The second match is unsuccessful and
produces 1 since we are computing an upper approximation. The intersection of
these two types is and(0, 1) which is equivalent to 0. The join of the two smallest
values integer and 0 for β is or(integer , 0) which is equivalent to integer. Finally,
the type list (integer ) for cons(X, nil) is obtained by substituting integer for β in
the left hand side of the type rule.
Without and in the type language, a choice must be made between list (0) and
tree(0) as the type for nil. Though these types are equivalent to and(list (0), tree(0)),
the choice made could complicate the ensuing computation. Should tree(0) be chosen, we would need to find the smallest value for β such that list (β) is greater than

Improving Precision of Type Analysis Using Non-Discriminative Union

5

or equal to tree(0). This could only be solved by applying an algorithm for solving
type inclusion constraints. The presence of and allows us to avoid that.
For the purpose of improving the precision of analysis, there is also a need for
disjunction at the level of abstract states. The following example illustrates this
point.
Example 2.3
Consider the following program
p(X) ← q(X, Y ),

1

...

q(1, 2).
q(a, b).
← p(X). % query
When the execution reaches program point 1 , X and Y are both of type integer or
they are both of type atom. This is described by a type constraint ((X ∈ integer ) ∧
(Y ∈ integer )) ∨ ((X ∈ atom) ∧ (Y ∈ atom)). Without disjunction at the level of
abstract states, we would have to replace the type constraint with a less precise
one: ((X ∈ or(integer , atom)) ∧ (Y ∈ or(integer , atom))).
3 Preliminaries
The reader is assumed to be familiar with the terminology of logic programming
(Lloyd 1987) and that of abstract interpretation (Cousot and Cousot 1977). We
consider a subset of Prolog which contains definite logic programs extended with
negation as failure and some built-in predicates.
3.1 Basic Concepts
We sometimes use Church’s lambda notation for functions, so that a function f
defined f (x) = e will be denoted λx.e. Let A and B be sets. Then A 7→ B is
the set of total functions from A to B and A≻→B is the set of partial functions
from A to B. The function composition ◦ is defined f ◦ g = λx.f (g(x)). Let D
be a set. A sequence over D is either ǫ or d • d~ where d ∈ D and d~ is a sequence
over D. The infix operator • associates to the right and prepends an element to
a sequence to form a longer sequence. The set of all sequences over D is denoted
D∗ . Let d~ = d1 • d2 • · · · • dn • ǫ. We will sometimes write d~ as d1 , d2 , · · · , dn . The
~ of d~ is n. Let E ⊆ D and S ⊆ D∗ . The set extension of • is defined
dimension kdk
as E • S = {d • d~ | d ∈ E ∧ d~ ∈ S}.
3.2 Abstract Interpretation
A semantics of a program is given by an interpretation h(C, ⊑C ), Ci where (C, ⊑C )
is a complete lattice and C is a monotone function on (C, ⊑C ). The semantics is
defined as the least fixed point lfp C of C. The concrete semantics of the program

6

Lunjin Lu

is given by the concrete interpretation h(C, ⊑C ), Ci while an abstract semantics
is given by an abstract interpretation h(A, ⊑A ), Ai. The correspondence between
the concrete and the abstract domains is formalized by a Galois connection (α, γ)
between (C, ⊑C ) and (A, ⊑A ). A Galois connection between A and C is a pair of
monotone functions α : C 7→ A and γ : A 7→ C satisfying ∀c ∈ C.(c ⊑C γ ◦ α(c))
and ∀a ∈ A.(α ◦ γ(a) ⊑A a). The function α is called an abstraction function
and the function γ a concretization function. A sufficient condition for lfpA to be
a safe abstraction of lfp C is ∀a ∈ A.(α ◦ C ◦ γ(a) ⊑A A(a)) or equivalently
∀a ∈ A.(C ◦ γ(a) ⊑C γ ◦ A(a)), according to propositions 24 and 25 in (Cousot and
Cousot 1992). The abstraction and concretization functions in a Galois connection
uniquely determine each other; and a complete meet-morphism γ : A 7→ C induces
a Galois connection (α, γ) with α(c) = ⊓A {a | c ⊑C γ(a)}. A function γ : A 7→ C
is a complete meet-morphism iff γ(⊓A X) = ⊓C {γ(x) ∈ X} for any X ⊆ A. Thus,
an analysis can be formalized as a tuple (h(C, ⊑C ), Ci, γ, h(A, ⊑A ), Ai) such that
h(C, ⊑C ), Ci and h(A, ⊑A ), Ai are interpretations, γ is a complete meet-morphism
from (C, ⊑C ) to (A, ⊑A ), and ∀a ∈ A.(C ◦ γ(a) ⊑C γ ◦ A(a)).

3.3 Logic Programs
Let Σ be a set of function symbols, Π a set of predicate symbols and Var a denumerable set of variables. Each function or predicate symbol has an arity which is a nonnegative integer. We write f /n ∈ Σ for an n-ary function symbol f in Σ and p/n ∈ Π
for an n-ary predicate symbol p in Π. Let V ⊆ Var. The set of all terms over Σ and
V , denoted Term(Σ, V ), is the smallest set satisfying: (i) V ⊆ Term(Σ, V ); and (ii) if
{t1 , · · · , tn } ⊆ Term(Σ, V ) and f /n ∈ Σ then f (t1 , · · · , tn ) ∈ Term(Σ, V ). The set of
all atoms that can be constructed from Π and Term(Σ, V ) is denoted Atom(Π, Σ, V );
Atom(Π, Σ, V ) = {p(t1 , · · · , tn ) | (p/n ∈ Π) ∧ ({t1 , · · · , tn } ⊆ Term(Π, Σ, V ))}. Let
Term = Term(Σ, Var) and Atom = Atom(Π, Σ, Var) for abbreviation. The set Term
contains all terms and the set Atom all atoms. The negation of an atom p(t1 , · · · , tn )
is written ¬p(t1 , · · · , tn ). A literal is either an atom or the negation of an atom. The
set of all literals is denoted Literal. Let Bip denote the set of calls to built-in predicates. Note that Bip ⊆ Atom.
A clause C is a formula of the form H ← L1 , · · · , Ln where H ∈ Atom ∪ {✷} and
Li ∈ Literal for 1 ≤ i ≤ n. H is called the head of the clause and L1 , · · · , Ln the
body of the clause. Note that ✷ denotes the empty head and denotes the empty
body. A query is a clause whose head is ✷. A program is a set of clauses of which
one is a query. The query initiates the execution of the program.
Program states which exist during the execution of a logic program are called
substitutions. A substitution θ is a mapping from Var to Term such that dom(θ) =
{x | (x ∈ Var) ∧ (θ(x) 6= x)} is finite. The set dom(θ) is called the domain of θ.
Let dom(θ) = {x1 , · · · , xn }. Then θ is written as {x1 7→ θ(x1 ), · · · , xn 7→ θ(xn )}.
A substitution θ is idempotent if θ ◦ θ = θ. The set of idempotent substitutions
is denoted Sub; and the identity substitution is denoted ǫ. Let Sub fail = Sub ∪
{fail } and extend ◦ by θ ◦ fail = fail and fail ◦ θ = fail for any θ ∈ Sub fail .

Improving Precision of Type Analysis Using Non-Discriminative Union

7

Substitutions are not distinguished from their homomorphic extensions to various
syntactic categories.
An equation is a formula of the form l = r where either l, r ∈ Term or l, r ∈ Atom.
The set of all equations is denoted Eqn. For a set of equations E, mgu : ℘(Eqn) 7→
Sub fail returns either a most general unifier for E if E is unifiable or fail otherwise.
Let mgu(l, r) stand for mgu({l = r}). Define eq(θ) = {x = θ(x) |x ∈ dom(θ)} for
θ ∈ Sub and eq(fail ) = fail .
The set of variables in a syntactic object o is denoted vars(o). A renaming substitution ρ is a substitution such that {ρ(x) | x ∈ Var} is a permutation of Var. The
set of all renaming substitutions is denoted Ren. Define Ren(o1 , o2 ) = {ρ ∈ Ren |
vars(ρ(o1 )) ∩ vars(o2 ) = ∅}.
We assume that there is a function sys : Bip × Sub 7→ ℘(Sub) that models the
behavior of built-in predicates. The set sys(p(t1 , · · · , tn ), θ) consists of all those
substitutions σ ◦ θ such that σ is a computed answer to θ(p(t1 , · · · , tn )).
Let VP be the set of variables in the program and AtomP = Atom(Π, Σ, VP ).
Define uf : AtomP × Sub × AtomP × Sub 7→ Sub fail by
uf (a1 , θ, a2 , ω) = let ρ ∈ Ren(θ(a1 ), ω(a2 )) in mgu(ρ(θ(a1 )), ω(a2 )) ◦ ω
The operation uf (a1 , θ, a2 , ω) models both procedure-call and procedure-exit operations. In a procedure-call operation, a1 and θ are the call and the program state
before the call, a2 is the head of the clause that is used to resolve with the call and
ω the identity substitution ǫ. In a procedure-exit operation, a2 and ω are the call
and the program state before the call, a1 is the head of the clause that was used to
resolve with the call and θ is the program state after the execution of the body of
the clause. A renaming is applied to the call in a procedure-call operation whilst in
a procedure-exit operation it is the head of the clause that is renamed.
3.4 Abstract Semantics
The new type analysis is presented as an abstract domain with four abstract operations. The domain and the operations are designed for an abstract semantics
in (Nilsson 1988) extended with supports for negation-as-failure and built-in predicates. The extended abstract semantics is a special case of an abstract semantics
in (Lu 2003) where a formal presentation can be found. The adaptation of the analysis to other abstract semantics such as (Bruynooghe 1991) is straightforward since
they require abstract operations with similar functionalities.
The abstract semantics is parameterized by an abstract domain hASub ♭ , ⊑♭ i. The
elements in ASub ♭ are called abstract substitutions since they are properties of substitutions. The abstract domain is related to the collecting domain h℘(Sub), ⊆i via
a concretization function γ : ASub ♭ 7→ ℘(Sub). We say that an abstract substitution
π describes a set of substitutions Θ iff Θ ⊆ γ(π). As usual, the abstract domain
and the concretization function are required to satisfy the following conditions.
C1: < ASub ♭ , ⊑♭ > is a complete lattice with least upper bound operation ⊔♭ ;
S
C2: γ(ASub ♭ ) is a Moore family where γ(X) = {γ(x) | x ∈ X}.

8

Lunjin Lu

We informally present the abstract semantics using the following program as a
running example.
diff(X, L, K)
diff(X, L, K)
member(X, [X|L])
member(X, [H|L])

←
←
←
←
←

1
4

member(X, L),
member(X, K),

2
5

¬member(X, K)
¬member(X, L)

3
6

7
8
10

member(X, L) 9
Y = [a, b] 11 Z = [1, 2]

12

diff(X, Y, Z)

13

The intended interpretation for member(X, L) is that X is a member of list L.
The intended interpretation for diff(X, L, K) is that X is in L or K but not
in both. For brevity of exposition, let A = member(X, L); B = member(X, K);
C = member(X, [X|L]); D = member(X, [H|L]); E = diff(X, L, K) and F =
diff(X, Y, Z). The atom in the literal to the right of a program point p is denoted A(p). For instance, A(2) = A(4) = B. Let H(p) denote the head of the clause
with which p is associated. For instance, H(1) = H(2) = E. Let p be the point to
the left of p if p exists. For instance, 2− = 1 whilst 1− is undefined.
The abstract semantics associates each textual program point with an abstract
substitution. The abstract substitution describes all the substitutions that may be
obtained when the execution reaches the program point. The abstract semantics is
the least solution to a system of data flow equations - one for each program point.
The system is derived from the control flow graph of the program whose vertices
are the textual program points. Let Pt be the set of the textual program points.
An edge from vertex p to vertex q in the graph is denoted q ↼ p; and it indicates
that the execution may reach q immediately after it reaches p.
Consider the example program. We have Pt = {1, · · · , 13}. The program point
ι = 10 is called the initial program point since it is where the execution of the
program is initiated. The abstract substitution at ι = 10 is an analysis input,
denoted πι , and it does not change during analysis. Thus, the data flow equation
for program point 10 is X ♭ (10) = πι where X ♭ is a mapping from program points to
abstract substitutions. The data flow equations for other program points are derived
by considering four kinds of control flow that may arise during program execution.
The first kind models the execution of built-in calls. For instance, the control may
flow from program point 10 to program point 11 by executing Y = [a, b]. The data
flow equation for program point 11 is X ♭ (11) = Sys ♭ (Y = [a, b], X ♭(10)) where
the transfer function Sys ♭ : Bip × ASub ♭ 7→ ASub ♭ emulates the execution of a
built-in call. Let Ptbip be the set of all the program points that follow the built-in
calls in the program. We have Ptbip = {11, 12} for the example program. Another
kind of control flow models negation-as-failure. The transfer function for this kind
of control flow is the identity function. For instance, the control may flow from
program point 2 to program point 3 since member(X,K) may fail, which yields this
data flow equation X ♭ (3) = X ♭ (2). Denote by Ptnf the set of all the program points
that follow negative literals. We have Ptnf = {3, 6} for the example program.
The third kind of control flow arises when a procedure-call is performed. For
instance, the control may flow from program point 1 to program point 8. The
description of data that flow from program point 1 to program point 8 is expressed

Improving Precision of Type Analysis Using Non-Discriminative Union

9

as Uf ♭ (A, X ♭ (1), D, Id ♭ ) where Id ♭ is an abstract substitution that describes {ǫ}.
Note that A is the call and D the head of the clause to which program point 8
belongs. The control may also flow to program point 8 from program points 4, 8, 2
and 5. The control flows from program point 5 to program point 8 when the negated
sub-goal member(K,L) is executed. The descriptions of data that flow to program
point 8 from those five source program points are merged together using the least
upper bound operation ⊔♭ on ASub ♭ , yielding the following data flow equation.
X ♭ (8) = Uf ♭ (A, X ♭ (1), D, Id ♭ ) ⊔♭ Uf ♭ (B, X ♭ (4), D, Id ♭ ) ⊔♭ Uf ♭ (A, X ♭ (8), D, Id ♭ )
⊔♭ Uf ♭ (B, X ♭ (2), D, Id ♭ ) ⊔♭ Uf ♭ (A, X ♭ (5), D, Id ♭ )
The transfer function Uf ♭ : AtomP ×ASub ♭ ×AtomP ×ASub ♭ 7→ ASub ♭ approximates
Uf : AtomP × ℘(Sub) × AtomP × ℘(Sub) 7→ ℘(Sub) defined
Uf (a1 , Θ1 , a2 , Θ2 ) = {uf (a1 , θ1 , a2 , θ2 ) 6= fail | θ1 ∈ Θ1 ∧ θ2 ∈ Θ2 }
which is the set extension of uf . Denote by Ptcall the set of program points that are
reached via procedure-calls. We have Ptcall = {1, 4, 7, 8} for the example program.
The fourth kind of control flow arises when a procedure exits. For instance,
the control may flow from program point 3 to program point 13. The description of data that flow from program point 3 to program point 13 is expressed by
Uf ♭ (E, X ♭ (3), F, X ♭ (12)) where E is the head of the clause to which program point
3 belongs and F the call that invoked the clause. The only other control flow to
program point 13 is from program point 6. Thus, the data flow equation for program point 13 is X ♭ (13) = Uf ♭ (E, X ♭ (3), F, X ♭ (12)) ⊔♭ Uf ♭ (E, X ♭ (6), F, X ♭ (12)).
Let Ptret be the set of program points that are reached via procedure-exits. For the
example program, we have Ptret = {2, 5, 9, 13}.
Let Edge = {q ↼ p | q ∈ Pt } where  ∈ {call, ret, nf, bip}. Note that Edge is
the set of control flows that sink in Pt . The data flow equation has the following
general form.

πι
if q = ι



♭
♭

♭
♭

if q ∈ Ptcall
 ⊔ {Uf (A(p), X (p), H(q), Id ) | q ↼ p ∈ Edge}
X ♭ (q) =
⊔♭ {Uf ♭ (H(q), X ♭ (q), A(p ), X ♭ (p )) | q ↼ p ∈ Edge} if q ∈ Ptret



X ♭ (q )
if q ∈ Ptnf



Sys ♭ (A(q ), X ♭ (q ))
if q ∈ Ptbip
where πι is the input abstract substitution. The least solution to the system of data
flow equations is a correct analysis if, in addition to C1 and C2, the following local
safety requirements are met.
C3: {ǫ} ⊆ γ(Id ♭ );
C4: Sys(a, γ(π)) ⊆ γ(Sys ♭ (a, π)) for any a ∈ Bip with vars(a) ⊆ VP and π ∈
ASub ♭ ; and
C5: Uf (a1 , γ(π1 ), a2 , γ(π2 )) ⊆ γ ◦ Uf ♭ (a1 , π1 , a2 , π2 ) for any π1 , π2 ∈ ASub ♭ , any
a1 , a2 ∈ AtomP .
Note that the condition C2 implies that ⊔♭ safely abstracts ∪ with respect to γ. The

10

Lunjin Lu

operation Uf ♭ is called abstract unification since it mimics the normal unification
operation whilst Sys ♭ is called abstract built-in execution operation.
The complete system of data flow equations for the example program is as follows.
X ♭ (1) = Uf ♭ (F, X ♭ (12), E, Id ♭ )
X ♭ (2) = Uf ♭ (C, X ♭ (7), A, X ♭ (1)) ⊔♭ Uf ♭ (D, X ♭ (9), A, X ♭ (1))
X ♭ (3) = X ♭ (2)
X ♭ (4) = Uf ♭ (F, X ♭ (12), E, Id ♭ )
X ♭ (5) = Uf ♭ (C, X ♭ (7), B, X ♭ (4)) ⊔♭ Uf ♭ (D, X ♭ (9), B, X ♭ (4))
X ♭ (6) = X ♭ (5)
X ♭ (7) = Uf ♭ (A, X ♭ (1), C, Id ♭ ) ⊔♭ Uf ♭ (B, X ♭ (4), C, Id ♭ ) ⊔♭
Uf ♭ (A, X ♭ (8), C, Id ♭ ) ⊔♭ Uf ♭ (B, X ♭ (2), C, Id ♭ ) ⊔♭
Uf ♭ (A, X ♭ (5), C, Id ♭ )
X ♭ (8) = Uf ♭ (A, X ♭ (1), D, Id ♭ ) ⊔♭ Uf ♭ (B, X ♭ (4), D, Id ♭ ) ⊔♭
Uf ♭ (A, X ♭ (8), D, Id ♭ ) ⊔♭ Uf ♭ (B, X ♭ (2), D, Id ♭ ) ⊔♭
Uf ♭ (A, X ♭ (5), D, Id ♭ )
X ♭ (9) = Uf ♭ (C, X ♭ (7), A, X ♭ (8)) ⊔♭ Uf ♭ (D, X ♭ (9), A, X ♭ (8))
X ♭ (10) = πι
X ♭ (11) = Sys ♭ (Y = [a, b], X ♭(10))
X ♭ (12) = Sys ♭ (Z = [1, 2], X ♭(11))
X ♭ (13) = Uf ♭ (E, X ♭ (3), F, X ♭ (12)) ⊔♭ Uf ♭ (E, X ♭ (6), F, X ♭ (12))
The remainder of the paper presents our type analysis as an abstract domain and
four abstract operations as required by the above abstract semantics. We begin with
the type language and type definitions.
4 Types
The type language in a type system decides which sets of terms are types. A
type is syntactically a ground term constructed from a ranked alphabet Cons and
{and, or, 1, 0} where and and or are binary and 1 and 0 are nullary. Elements
of Cons ∪ {and, or, 1, 0} are called type constructors. It is assumed that (Cons ∪
{and, or, 1, 0}) ∩ Σ = ∅. The set of types is Type = Term(Cons ∪ {and, or, 1, 0}, ∅).
The denotations of type constructors in Cons are determined by type definitions
whilst and, or, 1 and 0 have fixed denotations.
4.1 Type Rules
Types are defined by type rules. A type parameter is a variable from Para. A type
scheme is either a type parameter or of the form c(β1 , · · · , βm ) where c ∈ Cons and
β1 , · · · , βm are different parameters. Let Schm be the set of all type schemes. A type

Improving Precision of Type Analysis Using Non-Discriminative Union

11

rule is of the form c(β1 , · · · , βm )_f (τ1 , · · · , τn ) where c ∈ Cons, f /n ∈ Σ, β1 , · · · , βm
are different type parameters, and τj is a type scheme with type parameters from
{β1 , · · · , βm }. Note that every type parameter in the right-hand side of a type rule
must occur in the left-hand side. Overloading of function symbols is permitted since
a function symbol can appear in the right-hand sides of two or more type rules.
Let ∆ be the set of all type rules. We assume that each function symbol occurs in
at least one type rule and that each type constructor occurs in at least one type
rule. Type rules are similar to type definitions used in typed logic programming
languages Mercury (Somogyi et al. 1996) and Gödel (Hill and Lloyd 1994).
Example 4.1
Let Σ = {0, s(), [ ], [ | ], void, tr(, , )} and Cons = {nat, even, odd , list (), tree()}. The
following set of type rules will be used in examples throughout the paper.


nat _0,
nat _s(nat ),








even_s(odd ),
 even_0,

∆=
odd _s(even),




 list (β)_[ ],

list (β)_[β|list (β)]




tree(β)_void, tree(β)_tr(β, tree(β), tree(β))

Type rules in ∆ define natural numbers, even numbers, odd numbers, lists and
trees.
4.2 Denotations of Types
A (ground) type substitution is a member of TSub = (Para≻→Type) ∪ {⊤, ⊥}. The
application of a type substitution to a type scheme is defined as follows. ⊤(τ ) = 1
and ⊥(τ ) = 0 for any type scheme τ . Let k ∈ (Para≻→Type). Define k(β) = 0 for
each β 6∈ dom(k) where dom(k) is the domain of k. Then k(τ ) is obtained by replacing each β in τ with k(β). For instance, {β1 7→ list (nat ), β2 7→ nat }(list (β1 )) =
list (list (nat )).
Definition 4.2
The meaning of a type is defined by a function [·]]∆ : Type 7→ ℘(Term).
[1]]∆
[0]]∆
[and(R1 , R2 )]]∆
[or(R1 , R2 )]]∆
[c(R1 , · · · , Rm )]]∆

= Term
= ∅
= [R1]∆ ∩ [R2]∆
= [R1]∆ ∪ [R2]∆
=



let k = {βj 7→ Rj | 1 ≤ j ≤ m}
 in

(c(β1 ,···,βm )_f (τ1 ,···,τn ))∈∆
{f (t1 , · · · , tn ) | ∀1 ≤ i ≤ n.ti ∈ [k(τi )]]∆ }

S

The function [·]]∆ gives fixed denotations to and, or, 1 and 0. Type constructors
and and or are interpreted as set intersection and set union respectively. The type
constructor 1 denotes Term and 0 the empty set. We say that a term t is in a

12

Lunjin Lu

type R iff t ∈ [R]]∆ . Set inclusion and [·]]∆ induce a pre-order ⊑ on types: (R1 ⊑
R2 ) = ([[R1]∆ ⊆ [R2]∆ ) and an equivalence relation ≡ on types: (R1 ≡ R2 ) = (R1 ⊑
R2 ) ∧ (R2 ⊑ R1 ).
Example 4.3
Continuing with Example 4.1, we have
[nat ]∆ = {0, s(0), s(s(0)), · · ·}
[list (0)]]∆ = {[ ]}
[list (1)]]∆ = {[ ], [x|[ ]], · · ·}
where x ∈ Var. Observe that or(list (even), list (odd )) 6≡ list (nat ) since [0, s(0)] ∈
[list (nat )]]∆ and [0, s(0)] 6∈ [list (even)]]∆ and [0, s(0)] 6∈ [list (odd )]]∆ .
The type constructors and and or will sometimes be written as infix operators,
i.e., and(R1 , R2 ) is written as (R1 and R2 ) and or(R1 , R2 ) as (R1 or R2 ). A type
is atomic if its main constructor is neither and nor or. A type is conjunctive if
it is of the form and1≤i≤k Ai where each Ai is atomic. By an obvious analogy to
propositional logic, for any type R, there is a type of the form or1≤i≤m Ci such
that each Ci is conjunctive and R ≡ or1≤i≤m Ci . We call or1≤i≤m Ci a disjunctive
normal form of R.
A term in a type may contain variables. This lemma states that types are closed
under instantiation.
Lemma 4.4
Let R ∈ Type and t ∈ Term. If t ∈ [R]]∆ then σ(t) ∈ [R]]∆ for any σ ∈ Sub.
Type rules in ∆ are production rules for a context-free tree grammar (Comon
et al. 2002; Gécseg and Steinby 1984). The complement of the denotation of a
type is not necessarily closed under instantiation. For an instance, let ∆ be defined
as in Example 4.1, x ∈ Var and σ = {x 7→ s(0)}. Observe that x 6∈ [nat ]∆ and
σ(x) ∈ [nat ]∆ . Since x ∈ Term \ [nat]]∆ and σ(x) 6∈ Term \ [nat]]∆ , Term \ [nat]]∆ is not
closed under instantiation and cannot be denoted by a type in Type. The example
shows that the family of types is not closed under complement. This explains why
set complement is not a type constructor.
Types have also been defined using tree automata (Gécseg and Steinby 1984;
Comon et al. 2002), regular term grammars (Dart and Zobel 1992b; Smaus 2001;
Lagoon and Stuckey 2001), and regular unary logic programs (Yardeni and Shapiro
1991). A type defined in such a formalism denotes a regular set of ground terms. The
meaning function [·]]∆ interprets a type as a set of possible non-ground terms; in particular, it interprets 1 as the set of all terms. Type rules are used to propagate type
information during analysis. Let x be of type nat and y of type list (atom). Then the
type rule list (β)_[β|list (β)] is used to infer that [x|y] is of type list (or(nat , atom)).
The type parameter β is not only used as a placeholder but also used in folding
heterogeneous types precisely via non-discriminated union operator.

Improving Precision of Type Analysis Using Non-Discriminative Union

13

4.3 Type Sequences
During propagation of type information, it is necessary to work with type sequences.
A type sequence expression is an expression consisting of type sequences of the
same dimension and constructors and and or. Note that constructors and and or are
overloaded. The dimension of the type sequence expression is defined to be that of
~ ∈ Type∗ and E1 and E2 be type sequence
a type sequence in it. Let R ∈ Type, R
expressions. We extend [·]]∆ to type sequence expressions as follows.
[ǫ]]∆
~]
[R • R]
∆

=

{ǫ}

~]
= [R]]∆ • [R]
∆

[E1 and E2]∆

= [E1]∆ ∩ [E2]∆

[E1 or E2]∆

= [E1]∆ ∪ [E2]∆

The relations ⊑ and ≡ on types carry over naturally to type sequence expressions.
An occurrence of ~0 (respectively ~1) stands for the type sequence of 0’s (respectively
1’s) with a dimension appropriate for the occurrence.
5 Abstract Domain
Abstract substitutions in our type analysis are type constraints represented as a set
of variable typings which are mappings from variables to types. A variable typing
represents the conjunction of primitive type constraints of the form x ∈ R. For
instance, the variable typing {x 7→ nat , y 7→ even} represents the type constraint
(x ∈ nat) ∧ (y ∈ even). The restriction of a variable typing µ to a set V of variables
is defined as
µ ↑ V = λx.(if x ∈ V then µ(x) else 1)
The denotation of a variable typing is given by γVT : (VP 7→ Type) 7→ ℘(Sub)
defined
γVT (µ) = {θ | ∀x ∈ VP .(θ(x) ∈ [µ(x)]]∆ )}
For instance, γVT ({x 7→ nat , y →
7
list (nat )}) = {θ | θ(x) ∈ [nat ]∆ ∧ θ(y) ∈
[list (nat )]]∆ }. The denotation of a set of variable typings is the set union of the
denotations of its elements.
Example 5.1
For instance, letting S = {{x 7→ nat , y 7→ list (nat )}, {x 7→ list (nat ), y 7→ nat}}, S
denotes {θ | θ(x) ∈ [nat ]∆ ∧ θ(y) ∈ [list (nat )]]∆ } ∪ {θ | θ(x) ∈ [list (nat )]]∆ ∧ θ(y) ∈
[nat ]∆ }.
There may be many sets of variable typings that denote the same set of substitutions. Firstly, two different type expressions in Type may denote the same set of
terms. For instance, [nat and list (1)]]∆ = [0]]∆ using ∆ in Example 4.1. Secondly, an
element of a set of variable typings may have a smaller denotation than another.
For an example, let S = {{x 7→ list (1)}, {x 7→ list (nat )}}. Then S has the same denotation as one of its proper subset S ′ = {{x 7→ list (1)}}. Those abstract elements
that have the same denotation are identified. Let 4 on ℘(VP 7→ Type) be defined

14

Lunjin Lu

S
S
as S1 4 S2 = ( µ∈S1 γVT (µ)) ⊆ ( ν∈S2 γVT (ν)). It is a pre-order and induces an
equivalence relation ≈ on ℘(VP 7→ Type): (S1 ≈ S2 ) = (S1 4 S2 ) ∧ (S2 4 S1 ). The
equivalence classes with respect to ≈ are abstract substitutions. Thus, the abstract
domain is hASub ♭ , ⊑♭ i where
ASub ♭

=

℘(VP 7→ Type)/≈

♭

=

4/≈

⊑

hASub ♭ , ⊑♭ i is a complete lattice. Its join and meet operators are respectively
[S1 ]≈ ⊔♭ [S2 ]≈ = [S1 ∪ S2 ]≈ and [S1 ]≈ ⊓♭ [S2 ]≈ = [S1↓ ∩ S2↓ ]≈ where Si↓ = {µ ∈
(VP 7→ Type) | ∃ν ∈ Si .(γVT (µ) ⊆ γVT (ν))}. The infimum is [∅]≈ and the supremum
[{x 7→ 1 | x ∈ VP }]≈ . The concretization function γ : ASub ♭ 7→ ℘(Sub) is defined
[
γ([S]≈ ) =
γVT (µ)
µ∈S

The following lemma states that γ satisfies the safety requirement C2.
Lemma 5.2
γ(ASub ♭ ) is a Moore family.
The definition of ⊓♭ is not constructive since the downward closure of a set of
variable typings S can be infinite. For instance, letting S = {{x 7→ list (1)}},
{x 7→ list k (nat)} is in S ↓ for any k ≥ 1. The following operator ⊗ : ℘(VP 7→
Type) × ℘(VP 7→ Type) 7→ ℘(VP 7→ Type) computes effectively the meet of abstract
substitutions.
S1 ⊗ S2 = {{x 7→ (µ(x) and ν(x)) | x ∈ VP } | µ ∈ S1 ∧ ν ∈ S2 }
If S1 and S2 are finite representatives of two abstract substitutions then S1 ⊗ S2
is a finite representative of the meet of the abstract substitutions, which is stated
in this lemma.
Lemma 5.3
γ([S1 ⊗ S2 ]≈ ) = γ([S1 ]≈ ⊓♭ [S2 ]≈ ).
We will use a fixed renaming substitution Ψ such that VP ∩ Ψ(VP ) = ∅ and define
VP′ = VP ∪ Ψ(VP ). The relation ≈, the functions γVT and γ and the operator ⊗
extend naturally to sets of variable typings over VP′ . Let µ be a variable typing, S a
set of variable typings and θ a substitution. We say that θ satisfies µ if θ ∈ γVT (µ);
and we say that θ satisfies S if θ ∈ γ([S]≈ ).
The conditions C1 and C2 are satisfied. C1 holds because hASub ♭ , ⊑♭ , ⊔♭ i is a
complete lattice. C2 is implied by Lemma 5.2.
6 Abstract Operations
The design of our type analysis is completed with four abstract operations required
by the abstract semantics given in Section 3. One operation is ⊔♭ which is the
least upper bound on hASub ♭ , ⊑♭ i. Let Id ♭ = [{λx ∈ VP .1}]≈ . The operation Id ♭
obviously satisfies the condition C3 and thus safely abstracts {ǫ} with respect to γ.

Improving Precision of Type Analysis Using Non-Discriminative Union

15

Since abstract built-in execution operation Sys ♭ makes use of ancillary operations
for abstract unification operation Uf ♭ , we present Uf ♭ before Sys ♭ .
6.1 Outline of Abstract Unification
The abstract unification operator Uf ♭ takes two atoms and two abstract substitutions and computes an abstract substitution. The computation is reduced to solving
a constraint that consists of a set of equations in solved form E and a set of variable
typings Si . The solution to the constraint is a set of variable typings So . In order
to ensure that Uf ♭ safely abstracts Uf , So is required to describe the set of all
those substitutions that satisfy both E and Si . Let E = {x1 = t1 , · · · , xn = tn }.
The set So is computed in two steps. In the first step, type information about xi is
used to derive more type information about the variables in ti . This is a downward
propagation since type information is propagated from a term to its sub-terms. The
second step propagates type information in the opposite direction. It derives more
type information about xi from type information about the variables in ti .
For an illustration, let E = {x = [w], y = [w]} and Si = {µ} where µ =
{w 7→ 1, x 7→ list (atom or float ), y 7→ list (atom or integer )}. During the downward
propagation step, more type information for w is derived from type information
for both x and y. Since µ(x) = list (atom or float ) and x = [w], [w] is of type
list (atom or float ). Since there is only one type rule for [·|·]: list (β)_[β|list (β)],
we deduce that w is of type (atom or float ). Similarly, we deduce that w is of
type (atom or integer ) since µ(y) = list (atom or integer ) and y = [w]. So, w is
of type ((atom or float ) and (atom or integer )) that is equivalent to atom. The
derived type atom for w is used to strengthen µ into ν = {w 7→ atom, x 7→
list (atom or float ), y 7→ list (atom or integer )}. During the upward propagation
step, more type information for both x and y is derived type information for w.
Note that [w] is an abbreviation for [w|[ ]]. By applying the type rule list (β)_[ ],
we infer that [ ] is of type list (0). Since ν(w) = atom, we derive that [w] is of type
list (atom) by applying the type rule list (β)_[β|list (β)]. We deduce that both x
and y are of type list (atom) since x = [w] and y = [w]. The derived type list (atom)
for x and y is used to strengthen ν, resulting in this singleton set of variable typing
So = {{w 7→ atom, x 7→ list (atom), y 7→ list (atom)}}. Both the downward and upward propagation steps in the preceding example produce a single output variable
typing from an input variable typing. In more general cases, both steps may yield
multiple output variable typings from an input variable typing. We now present in
details these two steps.
6.2 Downward Propagation
Downward propagation requires propagating a type R downwards (the structure of)
a term t ∈ Term(Σ, VP′ ). Let Θ = {θ | θ(t) ∈ [R]]∆ }. Propagation of R downwards t
calculates a set of variable typings S (computed as vts(R, t)) such that Θ ⊆ γ([S]≈ ),
that is, S describes the set of all those substitutions that instantiate t to a term of
type R. This is done by a case analysis. If R = 1 then Θ = Sub since θ(t) is in R for

16

Lunjin Lu

any θ ∈ Sub. Put S = {λy ∈ VP′ .1}. Then S satisfies the condition that Θ ⊆ γ([S]≈ ).
If t ∈ VP′ then S = {λy ∈ VP′ .(if y = t then R else 1)} satisfies the condition that
Θ ⊆ γ([S]≈ ). Consider the case R = (R1 or R2 ). We have Θ = Θ1 ∪ Θ2 where
Θ1 = {θ1 | θ1 (t) ∈ [R]]∆ } and Θ2 = {θ2 | θ2 (t) ∈ [R2]∆ }. We propagate the types R1
and R2 downwards t separately, obtaining two sets of variable typings S1 and S2
such that Θ1 ⊆ γ([S1 ]≈ ) and Θ2 ⊆ γ([S2 ]≈ ). Put S = S1 ∪ S2 . Then the condition
that Θ ⊆ γ([S]≈ ) is satisfied. For the case R = R1 and R2 , S = S1 ⊗ S2 satisfies the
condition that Θ ⊆ γ([S]≈ ) where S1 and S2 are obtained as above. Consider the
remaining case R = c(R1 , · · · , R2 ) and t = f (t1 , · · · , tn ). Assume that there are k
j
type rules Υ1 , · · · , Υk for c/m and f /n and Υj is c(β1j , · · · , βm
)_f (τ1j , · · · , τnj ). By
S
the definition of [·]]∆ , Θ = 1≤j≤k Θj where
Θj

= {θ | θ(f (t1 , · · · , tn )) ∈ {f (s1 , · · · , sn ) | ∀1 ≤ i ≤ n.(si ∈ [κj (τij ))]]∆ }}

= {θ | f (θ(t1 ), · · · , θ(tn )) ∈ {f (s1 , · · · , sn ) | ∀1 ≤ i ≤ n.(si ∈ [κj (τij ))]]∆ }}
= {θ | ∀1 ≤ i ≤ n.(θ(ti ) ∈ [κj (τij ))]]∆
= Θj1 ∩ Θj2 ∩ · · · ∩ Θjn
j
and κj = {β1j 7→ R1 , · · · , βm
7→ Rm } and Θji = {θ | θ(ti ) ∈ [κj (τij )]]∆ }. We obtain
S as follows. We first propagate type κj (τij ) downwards term ti , obtaining a set of
variable typings Sij . We have that Θji ⊆ γ([Sij ]≈ ). We then calculate S j = S1j ⊗
· · · ⊗ Snj for the type rule Υj . The set S j satisfies the condition that Θj ⊆ γ([S j ]≈ ).
S
Finally, we compute S = S 1 ∪ · · · ∪ S k . Since Θj ⊆ γ([S j ]≈ ) and Θ = 1≤j≤k Θj ,
S satisfies the condition that Θ ⊆ γ([S]≈ ). In summary, S = vts(R, t) where vts :
Type × Term(Σ, VP′ ) 7→ ℘(VP′ 7→ Type) is defined

= {λy ∈ VP′ .1}
= {λy ∈ VP′ .(if y = x then R else 1)}
= vts(R1 , t) ⊗ vts(R2 , t)
= vts(R1 , t) ∪ vts(R2 , t)
=


let k = {βj 7→ Rj | 1 ≤ j ≤ m}
S
 in

(c(β1 ,···,βm )_f (τ1 ,···,τn ))∈∆
N
1≤i≤n vts(k(τi ), ti )

vts(1, t)
vts(R, x)
vts((R1 and R2 ), t)
vts((R1 or R2 ), t)
vts(c(R1 , · · · , Rm ), f (t1 , · · · , tn ))

where x ∈ VP′ , f /n ∈ Σ and c/m ∈ Cons. The first one applies when there are
multiple applicable alternatives.
The following lemma states that vts(R, t) describes all the substitutions that
instantiate t to a term of type R.
Lemma 6.1
For any R ∈ Type and t ∈ Term(Σ, VP′ ), {θ | θ(t) ∈ [R]]∆ } ⊆ γ([vts(R, t)]≈ ).
We now consider the overall downward propagation given a set of variable typings
S and a set of equations in solved form E = {x1 = t1 , · · · , xn = tn }. Each variable
typing µ in S is processed separately as follows. We first propagate the type µ(xi )
downwards ti . This results in a set of variable typings vts(µ(xi ), ti ) which describes
all the substitutions that instantiate ti to a term of type µ(xi ). We then calculate

Improving Precision of Type Analysis Using Non-Discriminative Union

17

Sµ = vts(µ(x1 ), t1 ) ⊗ · · · ⊗ vts(µ(xn ), tn ). The set Sµ describes all the substitutions
that instantiate ti to a term of type µ(xi ) for all 1 ≤ i ≤ n. We finally conjoin Sµ
with {µ}, obtaining {µ}⊗Sµ which describes all the substitutions that satisfy both µ
and E. After each variable typing in S is processed, results from different variable
typings are joined together using set union. The overall downward propagation
function down : ℘(Eqn) × ℘(VP′ 7→ Type) 7→ ℘(VP′ 7→ Type) is defined
down (E, S) =

[

µ∈S

({µ} ⊗

O

vts(µ(x), t))

(1)

(x=t)∈E

Example 6.2
Let VP′ = {x, y}, S = {{x 7→ 1, y 7→ (list (nat ) or nat)}} and ∆ be that in Example 4.1. We have vts(list (nat ), [x|[ ]]) = {{x 7→ nat , y 7→ 1}} and vts(nat , [x|[ ]]) = ∅.
So,
vts(list (nat ) or nat , [x|[ ]]) = {{x 7→ nat, y 7→ 1}}
and
down({y = [x|[ ]]}, S)
=

{{x 7→ 1, y 7→ (list (nat ) or nat)}} ⊗ {{x 7→ nat, y 7→ 1}}

=

{µ}

where µ = {x 7→ nat , y 7→ (list (nat ) or nat )}.
The following lemma states the correctness of downward propagation.
Lemma 6.3
Let S ′ = down(E, S). Then mgu(θ(E)) ◦ θ ∈ γ([S ′ ]≈ ) for all θ ∈ γ([S]≈ ).
6.3 Upward Propagation
We now consider upward propagation of type information. The key step in upward propagation is to compute a type for a term from those of its variables.
We first consider how a type rule τ _f (τ1 , · · · , τn ) can be applied to compute a
type of f (t1 , · · · , tn ) from types of its top-level sub-terms t1 , · · · , tn . Let Ri be
the type of ti . A simplistic approach would compute a type substitution k such
that hR1 , · · · , Rn i ⊑ k(hτ1 , · · · , τn i) and then return k(τ ) as the type of t. However, this leads to loss of precision. Consider the term [x|y] and the type rule
list(β)_[β|list (β)]. Let the types of x and y be (even or odd ) and list (0). Then
the minimal type substitution k such that heven or odd , list (0)i ⊑ k(hβ, list (β)i) is
k = {β 7→ (even or odd )}. We would obtain k(list (β)) = list (even or odd ) as a type
of [x|y]. A more precise type of [x|y] is (list (even) or list (odd )). We first compute a
set of type substitutions K such that hR1 , · · · , Rn i ⊑ ork∈K k(hτ1 , · · · , τn i) and then
return ork∈K k(τ ) as a type of f (t1 , · · · , tn ). Continue with the above example. Let
K = {{β 7→ even}, {β 7→ odd }}. Then heven or odd , list (0)i ⊑ ork∈K k(hβ, list (β)i).
We obtain (list (even) or list (odd )) as a type of [x|y].

18

Lunjin Lu

Definition 6.4
~ ∈ Type∗ and K ∈ ℘(TSub). We say that K
Let τ ∈ Schm, ~τ ∈ Schm∗ , R ∈ Type, R
~ and ~τ iff
is a cover for R and τ iff R ⊑ ork∈K k(τ ). We say that K is a cover for R
~ ⊑ ork∈K k(~τ ).
R
Calculating a cover for a type and a type scheme is a key task in upward propagation of type information. Before defining a function that does the computation,
we need some operations on type substitutions.
6.3.1 Operations on Type Substitutions
We first introduce an operation for calculating an upper bound of two type substitutions. It is the point-wise extension of or when both of its operands are mappings
from type parameters to types. Define g : TSub × TSub 7→ TSub as follows.

⊤,
if (k1 = ⊤) ∨ (k2 = ⊤);



k2 ,
else if (k1 = ⊥);
k1 g k2 =
k
,
else
if (k2 = ⊥);

1


{β 7→ (k1 (β) or k2 (β)) | β ∈ dom(k1 ) ∪ dom(k2 )},
otherwise.

An operation f : TSub × TSub 7→ TSub that calculates a lower bound of type
substitutions is defined dually:

⊥,
if (k1 = ⊥) ∨ (k2 = ⊥);



k2 ,
else if (k1 = ⊤);
k1 f k2 =

k
,
else if (k2 = ⊤);

 1
{β 7→ (k1 (β) and k2 (β)) | β ∈ dom(k1 ) ∩ dom(k2 )},
otherwise.
The following lemma states that the operations g and f indeed compute upper
and lower bounds of two type substitutions respectively.
Lemma 6.5
For any τ ∈ Schm and any k1 , k2 ∈ TSub,
(a) (k1 (τ ) or k2 (τ )) ⊑ (k1 g k2 )(τ ); and
(b) (k1 (τ ) and k2 (τ )) ≡ (k1 f k2 )(τ ).

While the type substitution operation is a meet homomorphism according to
Lemma 6.5.(b), it is not a join homomorphism. For an instance, let τ = list (β), k1 =
{β 7→ nat } and k2 = {β 7→ list (nat )}. Then k1 g k2 = {β 7→ (nat or list (nat ))},
(k1 gk2 )(τ ) = list (nat or list (nat )), and k1 (τ ) or k2 (τ ) = list (nat ) or list (list (nat )).
Observe that (k1 (τ ) or k2 (τ )) 6≡ (k1 gk2 )(τ ) since the term [0, [0]] has type list(nat or
list(nat)) but it does not have type (list (nat ) or list (list (nat ))).
Let K1 and K2 be sets of type substitutions. We say that K1 and K2 are equivalent, denoted as K1 ∼
= K2 , iff (ork∈K1 k(τ )) ≡ (ork∈K2 k(τ )) for any type scheme
b c
τ . Define , : ℘(TSub) × ℘(TSub) 7→ ℘(TSub) as the set extensions of g and f
respectively:

Improving Precision of Type Analysis Using Non-Discriminative Union

K1

j

K2

= {k1 g k2 | k1 ∈ K1 ∧ k2 ∈ K2 }

K1

k

K2

= {k1 f k2 | k1 ∈ K1 ∧ k2 ∈ K2 }

19

Example 6.6
Let K1 = {{β1 7→ tree(nat), β2 7→ nat}, {β1 7→ list (nat ), β2 7→ nat }} and K2 =
{{β1 7→ list (even), β2 7→ even}}. Since even ⊑ nat and list (even) ⊑ list (nat ), we
have


j
{β1 7→ tree(nat ) or list (even), β2 7→ nat or even},
K1
K2 =
{β1 7→ list (nat) or list (even), β2 7→ nat or even}


{β1 7→ tree(nat ) or list (even), β2 7→ nat },
∼
=
{β1 7→ list (nat ), β2 7→ nat }
We also have


k
{β1 7→ (tree(nat ) and list (even)), β2 7→ (nat and even)},
K1 K2 =
{β1 7→ (list (nat ) and list (even)), β2 7→ (nat and even)}


{β1 7→ (tree(nat ) and list (even)), β2 7→ even},
∼
=
{β1 7→ list (even), β2 7→ even}
∼
= {{β1 7→ list (even), β2 7→ even}}
since (tree(nat ) and list (even)) ≡ 0.
A cover for a type sequence and a type scheme sequence can be computed compositionally according to the following lemma.
Lemma 6.7
~ ∈ Type∗ and ~τ ∈ Schm∗ such
Let K1 , K2 ∈ ℘(TSub), R ∈ Type, τ ∈ Schm, R
~ ⊑
~ ⊑ ork2 ∈K2 k2 (~τ ) then R • R
~ = k~τ k. If R ⊑ ork1 ∈K1 k1 (τ ) and R
that kRk
b
ork∈(K1 K2 ) k(τ • ~τ ).
6.3.2 Calculating a Cover
We now consider how to compute a cover K for a type R and a type scheme τ .
In the case R = 1, K = {⊤} is a cover since ⊤(τ ) = 1; and K = {⊥} is a
cover in the case R = 0 since ⊥(τ ) = 0. Consider the case R = (R1 or R2 ), a
cover Kj can be recursively computed for Rj and τ for j = 1, 2. We have that
Rj ⊑ ork∈Kj k(τ ) and hence that (R1 or R2 ) ⊑ ork∈(K1 ∪K2 ) k(τ ). So, the union of
K1 and K2 is a cover for R and τ . Consider the case R = (R1 and R2 ). A cover
c
Kj can be recursively computed for Rj and τ for j = 1, 2. Let K = K1 K2 =
{k1 f k2 | k1 ∈ K1 ∧ k2 ∈ K2 }. Then ork∈K (τ ) = ork1 ∈K1 ∧k2 ∈K2 (k1 f k2 )(τ ). By
Lemma 6.5.(b), ork∈K (τ ) = ork1 ∈K1 ∧k2 ∈K2 (k1 (τ ) and k2 (τ )) and hence ork∈K (τ ) =
c
(ork1 ∈K1 k1 (τ )) and (ork2 ∈K2 k2 (τ )). So, K = K1 K2 is a cover for R and τ . In the
case R is atomic and τ is a type parameter, K = {{τ 7→ R}} is a cover for R and
τ . In the remaining case, R = c(R1 , · · · , Rm ) and τ = d(β1 , · · · , βk )). If c/m = d/k

20

Lunjin Lu

then {{βj 7→ Rj | 1 ≤ j ≤ m}} is a cover. Otherwise {⊤} is a cover. In summary,
the function that computes a cover is cover : Type × Schm 7→ ℘(TSub) defined
cover (1, τ )
cover (0, τ )
cover ((R1 or R2 ), τ )
cover ((R1 and R2 ), τ )
cover (R, β)
cover (c(R1 , · · · , Rm ), d(β1 , · · · , βk ))

if (c/m) = (d/k)
else {⊤}

= {⊤}
= {⊥}
= cover (R1 , τ ) ∪ cover (R2 , τ )
c
= cover (R1 , τ ) cover (R2 , τ )
= {{β 7→ R}}
=
then {{βj 7→ Rj | 1 ≤ j ≤ m}}

Example 6.8
Let Cons be given in Example 4.1. Then,
cover ((list (nat ) and tree(even)), list (β))
k
= cover (list (nat ), list (β)) cover (tree(even), list (β))
k
∼
= {{β 7→ nat}} {⊤}
= {{β 7→ nat}}

The following lemma states that cover (R, τ ) is a cover for R and τ .
Lemma 6.9
Let τ ∈ Schm, R ∈ Type and K = cover (R, τ ). Then R ⊑ ork∈K k(τ ).
6.3.3 Computing a Type
The type of a term t is computed from those of its variables in a bottom-up manner.
The types of the variables are given by a variable typing µ. For a compound term
t = f (t1 , · · · , tn ), a type Ri is first computed from ti and µ for each 1 ≤ i ≤ n. Each
type rule for f /n is applied to compute a type of t. Types resulting from all type
rules for f /n are conjoined using and. The result is a type of t since conjunctions of
two or more types of t is also a type of t. For a type rule τ _f (τ1 , · · · , τn ), a cover Ki
for Ri and τi is computed for each 1 ≤ i ≤ n. Joining covers for 1 ≤ i ≤ n obtains
a cover K for hR1 , · · · , Rn i and hτ1 , · · · , τn i. The type that is computed from the
type rule is ork∈K k(τ ). Define type : Term(Σ, VP′ ) × (VP′ 7→ Type) 7→ Type by
type(x, µ)
type(f (t1 , · · · , tn ), µ)

= µ(x)
= andτ _f (τ1 ,···,τn )∈∆ (ork∈(b1≤i≤n cover(type(ti ,µ),τi )) k(τ ))

Example 6.10
Let µ = {x 7→ nat , y 7→ (list (nat ) or nat )}, k1 = {β 7→ nat } and k2 = {β 7→ 0}. By
the definition of cover , cover (nat , β) = {k1 } and cover (list (0), list (β)) = {k2 }. By
the definition of type, type(x, µ) = nat and type([ ], µ) = list (0). So, type([x|[ ]], µ) =
(k1 g k2 )(list (β)) = list (nat ).

Improving Precision of Type Analysis Using Non-Discriminative Union

21

The following lemma says that type(t, µ) is a type that contains all the instances
of t under the substitutions described by µ.
Lemma 6.11
Let t ∈ Term(Σ, VP′ ) and µ ∈ (VP′ 7→ Type). Then θ(t) ∈ [type(t, µ)]]∆ for all
θ ∈ γVT (µ).
6.3.4 Upward Propagation
We are now ready to present the overall upward propagation. For a set S of variable
typings and a set E of equations in solved form, upward propagation strengthens
each variable typing µ in S as follows. For each equation x = t in E, type(t, µ) is
a type of x if variables occurring in t satisfy µ. The overall upward propagation is
performed by a function up : ℘(Eqn) × ℘(VP′ 7→ Type) 7→ ℘(VP′ 7→ Type) defined



if ∃t.(x = t) ∈ E

[
up(E, S) =
λx ∈ VP′ .  then (µ(x) and type(t, µ)) 


µ∈S
else µ(x)
Example 6.12
Continue with Example 6.10. We have
up({y = [x|[ ]]}, {µ}) =
≈

{µ[y 7→ ((list (nat ) or nat ) and list (nat ))]}
{{x 7→ nat, y 7→ list (nat )}}

The correctness of upward propagation is ensured by this lemma.
Lemma 6.13
Let S ∈ ℘(VP′ 7→ Type) and E ∈ ℘(Eqn). Then mgu(θ(E)) ◦ θ ∈ γ([up(E, S)]≈ ) for
all θ ∈ γ([S]≈ ).
6.4 Abstract Unification
Algorithm 6.14 defines the abstract unification operation Uf ♭ . Given two atoms
a1 , a2 ∈ AtomP and two abstract substitutions [S1 ]≈ , [S2 ]≈ ∈ ASub ♭ , it first applies
the renaming substitution Ψ to a1 and S1 and computes E0 = eq ◦ mgu(Ψ(a1 ), a2 ).
If E0 = fail , it returns [∅]≈ – the smallest abstract substitution which describes
U
the empty set of substitutions. Otherwise, it calculates S0′ = Ψ(S1 ) S2 where
U
: (Ψ(VP ) 7→ Type) × (VP 7→ Type) 7→ (VP′ 7→ Type). A variable typing represents
a conjunctive type constraint. If µ and ν have disjoint domains then µ∪ν represents
U
the conjunction of µ and ν. The first operand of is a set of variable typings over
Ψ(VP ) and the second operand a set of variable typings over VP . The result of
U
describes the set of all the substitutions that satisfy both of its two operands.
Thus S0′ describes the set of all the substitutions that satisfy both Ψ(S1 ) and S2 .
Note that S0′ ∈ ℘(VP′ 7→ Type). The abstract unification operation then calls a
function solve : Eqn × ℘(VP′ 7→ Type) 7→ ℘(VP′ 7→ Type) to perform downward

22

Lunjin Lu

and upward propagations. The result S1′ is solve(E0 , S0′ ) which describes the set
of all the substitutions that satisfy both E0 and S0′ . Finally, it calls a function
rest : ℘(VP′ 7→ Type) 7→ ℘(VP 7→ Type) to restrict each variable typing in S1′ to VP .
Algorithm 6.14

Uf ♭ (a1 , [S1 ]≈ , a2 , [S2 ]≈ )

=

U
S1 S2
rest(S)
solve(E, S)

=
=
=


let E0 = eq ◦ mgu(Ψ(a1 ), a2 ) in



if
E0 6= fail
U

then
[rest ◦ solve(E0 , Ψ(S1 ) S2 )]≈


else [∅]≈
{µ ∪ ν | µ ∈ S1 ∧ ν ∈ S2 }
{µ ↑ VP | µ ∈ S ∧ ∀x ∈ VP′ .(µ(x) 6≡ 0)}
up(E, down (E, S))

The function rest removes those variable typings that denote the empty set of
substitutions and projects the remaining variable typings onto VP .
Example 6.15
Let VP = {x}, Ψ(x) = y, a1 = p(x), a2 = p([x|[ ]]), S1 = {{x 7→ (list (nat ) or nat )}},
U
and S2 = {{x 7→ 1}}. Then E0 = {y = [x|[ ]]} and Ψ(S1 ) S2 = S with S being
that in Example 6.2. By Examples 6.2 and 6.12,
solve(E0 , S)

=

up(E0 , down(E0 , S)) = up(E0 , {µ})

=

{{x 7→ nat , y 7→ list (nat )}}

with µ given in Example 6.12.
The following theorem states that Uf ♭ safely abstracts Uf with respect to γ.
Theorem 6.16
For any [S1 ]≈ , [S2 ]≈ ∈ ASub ♭ and any a1 , a2 ∈ AtomP ,
Uf (a1 , γ([S1 ]≈ ), a2 , γ([S2 ]≈ )) ⊆

γ(Uf ♭ (a1 , [S1 ]≈ , a2 , [S2 ]≈ ))

6.5 Abstract Built-in Execution Operation
For each built-in, it is necessary to specify an operation that transforms an input
abstract substitution to an output abstract substitution. These operations are given
in Table 1 where abstract substitutions are displayed as sets of variable typings. The
primitive types integer, f loat, number, string, atom and atomic have their usual
denotations in Prolog. Observe that number = (integer or f loat) and atomic =
(number or atom).
Unification t1 =t2 is modeled by λS.solve(mgu(t1 , t2 ), S). Let θ be the program
state before the execution of t1 =t2 and assume that θ satisfies S. The program state
after the execution of t1 =t2 is mgu(θ(t1 ), θ(t2 ))◦θ and satisfies solve(mgu(t1 , t2 ), S).
Built-ins such as </2 succeed only if their arguments satisfy certain type constraints.
Such type constraints are conjoined with the input abstract substitution to obtain
the output abstract substitution. For instance, the execution of t1 <t2 in an input

Improving Precision of Type Analysis Using Non-Discriminative Union

23

program state θ succeeds only if θ instantiates both t1 and t2 to numbers. So, the
abstract operation for t1 <t2 is f3 = λS.(S ⊗vts(number, t1 )⊗vts(number, t2 )) where
vts defined in Section 6.2 is extended to deal with built-in types. The extension is
straightforward and omitted. For another instance, f ormat(t1 ) succeeds only if t
is an atom, or a list of character codes or a string in its input program state.
The above type constraint is obtained as vts(atom or list (integer) or string, t1 ).
The type list (integer) describes lists of character codes since character codes are
integers. The type checking built-ins such as atom/1 are modeled in the same way.
Built-ins such as @</2 do not instantiate their arguments or check types of their
arguments. They are modeled by the identity function λS.S. The built-in f ail/0
never succeeds and hence is modeled by the constant function that always returns
∅.
Consider a built-in to which a call p(t1 , · · · , tn ) will definitely instantiate ti to a
term of type Ri upon success. The type Ri can be propagated downwards ti , resulting in a set of variable typings. The input abstract substitution can be strengthened by this set of variable typings to give the output abstract substitution. For
an instance, consider name(t1 , t2 ). Upon success, t1 is either an atom or an integer
and t2 is a string. So, name(t1 , t2 ) is modeled by λS.(S ⊗ vts(atom or integer, t1) ⊗
vts(string, t2 )). The built-ins length(t1 , t2 ) and compare(t1 , t2 , t3 ) fall into this category.
Consider the built-in var(t). The execution of var(t) succeeds in a program state
θ iff θ(t) is a variable. All types that contains variables are equivalent to 1. Thus, the
built-in var(t) is modeled by λS.{µ | µ ∈ S ∧ type(t, µ) ≡ 1}. The output abstract
substitution contains only those variable typings in which t has no type smaller
than 1. The built-in nonvar(t) is modeled by the identity function λS.S since a
term being a non-variable does not provide any information about its type unless
non-freeness is defined as a type. So is the built-in ground(t) since a term being
ground says nothing about its type unless groundness is defined as a type. The
operation for the built-in compound(t) makes use of the property that a compound
term is not atomic. It removes from the input abstract substitution any variable
typing in which t is atomic.
7 Implementation
We have implemented a prototype of our type analysis in SWI-Prolog. The prototype is a meta-interpreter using ground representations for program variables. The
prototype supports the primitive types integer, f loat, number, string, atom and
atomic with their usual denotations in Prolog.
7.1 Examples
Example 7.1
The following is the intersect program that computes the intersection of two lists
and its analysis result. Lists are defined in Example 4.1. Abstract substitutions are
displayed as comments. The abstract substitution associated with the entry point

24

Lunjin Lu

Predicate
abort, f ail, f alse
!,
t1 @<t2 ,
t1 @>t2 ,
t1 =<@t2 ,
t1 @>=t2 ,
t1 \==t2 , t1 \=t2 , display(t1 ), ground(t1 ),
listing,
listing(t1 ),
nl,
nonvar(t1 ),
portray clause(t1 ),
print(t1 ),
read(t1 ),
repeat, true, write(t1 ), writeq(t1 )
compound(t)
atom(t)
atomic(t)
f loat(t)
erase(t), integer(t), tab(t)
number(t)
put(t)
string(t)
var(t)
t1 =t2 , t1 ==t2
f ormat(t1 ), f ormat(t1 , t2 ), f ormat(t0 , t1 , t2 )
t1 <t2 , t1 > t2 , t1 =<t2 , t1 >=t2 , t1 =:=t2 ,
t1 =\=t2 , is(t1 , t2 )
length(t1 , t2 )
compare(t1, t2 , t3 )
name(t1 , t2 )

Operation
λS.∅
λS.S

λS.({µ | µ ∈ S ∧ type(t, µ) 6⊑ atomic})
λS.(S ⊗ vts(atom, t))
λS.(S ⊗ vts(atomic, t))
λS.(S ⊗ vts(f loat, t))
λS.(S ⊗ vts(integer, t))
λS.(S ⊗ vts(number, t))
λS.(S ⊗ vts(atom or integer, t))
λS.(S ⊗ vts (string, t))
λS.{µ | µ ∈ S ∧ type(t, µ) ≡ 1}
λS.solve(mgu(t1 , t2 ), S)
f4
f3
f1
λS.(S ⊗ vts(atom, t1 ))
f2

Table 1. Abstract operations for built-ins where f1 = λS.(S ⊗ vts(list (1), t1 ) ⊗
vts(integer, t2 )), f2 = λS.(S ⊗ vts(atom or integer, t1 ) ⊗ vts(string, t2 )),
f3 = λS.(S ⊗ vts(number, t1 ) ⊗ vts(number, t2 )), and f4 = λS.(S ⊗
vts(atom or list (integer) or string, t1 )).
of the query is an analysis input whilst all other abstract substitutions are analysis
outputs. Sets are displayed as lists. A binding V 7→ T is written as V /T , or as or
and and as and . The code for the predicate member/2 is omitted.
:- %[[X/list(atom or float),Y/list(atom or integer)]]
intersect(X,Y,Z).
%[[X/list(atom or float),Y/list(atom or integer),Z/list(atom)]]
intersect([],L,[]).
%[[L/list(atom or integer)]]
intersect([X|Xs],Ys,[X|Zs]) :%[[X/atom,Xs/list(atom or float),Ys/list(atom or integer)],
% [X/float,Xs/list(atom or float),Ys/list(atom or integer)]]
member(X,Ys),
%[[X/atom,Xs/list(atom or float),Ys/list(atom or integer)]]
intersect(Xs,Ys,Zs).
%[[X/atom,Xs/list(atom or float),Ys/list(atom or integer),
% Zs/list(atom)]]
intersect([X|Xs],Ys,Zs) :%[[X/atom,Xs/list(atom or float),Ys/list(atom or integer)],

Improving Precision of Type Analysis Using Non-Discriminative Union

25

% [X/float,Xs/list(atom or float),Ys/list(atom or integer)]]
\+ member(X,Ys),
%[[X/float,Xs/list(atom or float),Ys/list(atom or integer)],
% [X/atom,Xs/list(atom or float),Ys/list(atom or integer)]]
intersect(Xs,Ys,Zs).
%[[X/float,Xs/list(atom or float),Ys/list(atom or integer),
% Zs/list(atom)],
% [X/atom,Xs/list(atom or float),Ys/list(atom or integer),
% Zs/list(atom)]]
The result shows that the intersection of a list containing atoms and float numbers
and another list containing atoms and integer numbers is a list of atoms. This is
precise because the type ((atom or f loat) and (atom or integer)) is equivalent to the
type atom. Without the set operators and and or in their type languages, previous
type analyses with a priori type definitions cannot produce a result as precise as
the above.
Example 7.2
The following is a program p/1. The analysis result is displayed with the typing
binding x 7→ 1 omitted for any variable x.
p([]). % [[]]
p([X|Y]) :% [[]]
integer(X),
% [[X/integer]]
p(Y).
% [[X/integer, Y/list(or(atom, integer))]]
p([X|Y]) :% [[]]
atom(X),
% [[X/atom]]
p(Y).
% [[X/atom, Y/list(or(atom, integer))]]
:-

% [[]]
p(U).
% [[U/list(or(atom, integer))]]

The result captures precisely type information in the success set of the program,
that is, U is a list consisting of integers and atoms upon success of p(U).1

1

This example was provided by an anonymous referee of a previous version of this paper.

26

Lunjin Lu

During analysis of a program, the analyzer repeatedly checks if two sets of variable
typings are equivalent and if a set of variable typings contains redundant elements.
Both of these decision problems are reduced to checking if a given type denotes the
empty set of terms.
7.2 Emptiness of Types
Type rules in ∆ are production rules for a context-free tree grammar in restricted
form (Gécseg and Steinby 1984). According to (Lu and Cleary 1998), if 1 denotes
the set of all ground terms instead of all terms then each type denotes a regular
tree language. We now show how an algorithm in (Lu and Cleary 1998) can be
used for checking the emptiness of types. We first extend the type language with
the complement operator ∼ and define eType = Term(Cons ∪ {∼, and, or, 1, 0}, ∅).
Observe that Type ⊂ eType and that [·]]∆ is not defined for elements in eType \
Type. Since the algorithm in (Lu and Cleary 1998) was developed for checking
the emptiness of types that denote sets of ground terms, we need to justify its
application by closing the gap between the two different semantics of types. This
is achieved by extending the signature Σ with an extra constant ̺ (̺ ∈ Σ) that is
used to encode variables in terms. Use of extended signatures in analysis of logic
programs can be traced to (Gallagher et al. 1995) where extra constants are used to
encode non-ground terms. In fact, by introducing an infinite set of extra constants
one can obtain an isomorphism between the set of all terms in the original signature
and the set of the ground terms in the extended signature.
Definition 7.3
The meaning of a type in eType is given by a function hh·ii∆ : eType 7→ ℘(Term(Σ ∪
{̺}, ∅).
hh1ii∆
hh0ii∆
hh∼Rii∆
hhand(R1 , R2 )ii∆
hhor(R1 , R2 )ii∆
hhc(R1 , · · · , Rm )ii∆

=
=
=
=
=
=

Term(Σ ∪ {̺}, ∅)
∅
hh1ii∆ \ hhRii∆
hhR1 ii∆ ∩ hhR2 ii∆
hhR1 ii∆ ∪ hhR2 ii∆



let k = {βj 7→ Rj | 1 ≤ j ≤ m}
S
 in

(c(β1 ,···,βm )_f (τ1 ,···,τn ))∈∆
{f (t1 , · · · , tn ) | ∀1 ≤ i ≤ n.ti ∈ hhk(τi )ii∆ }

There are two differences between hh·ii∆ and [·]]∆ . Firstly, ∼ is interpreted as set
complement under hh·ii∆ whilst it has no denotation under [·]]∆ . Type constructor
∼ can be interpreted as set complement by hh·ii∆ because hhRii∆ is a regular tree
language for any R ∈ eType (Lu and Cleary 1998). It cannot be interpreted as set
complement by [·]]∆ because the complement of [R]]∆ is not closed under instantiation. Secondly, the universal type 1 denotes Term(Σ, Var) in [·]]∆ whilst it denotes
Term(Σ∪{̺}, ∅) in hh·ii∆ . An implication is that a type denotes a set of terms closed
under instantiation under [·]]∆ whilst it denotes a set of ground terms under hh·ii∆ .

Improving Precision of Type Analysis Using Non-Discriminative Union

27

Let χ : Term(Σ, Var) 7→ Term(Σ ∪ {̺}, ∅) be defined χ(x) = ̺ for all x ∈ Var and
χ(f (t1 , · · · , tn )) = f (χ(t1 ), · · · , χ(tn )). The function χ(·) transforms a term into a
ground term by replacing all variables in the term with the same constant ̺. The
following theorem states that, given a term t and a type R, the membership of t in
[R]]∆ is equivalent to that of χ(t) in hhRii∆ .
Theorem 7.4
For any term t in Term(Σ, Var) and any type R in Type, t ∈ [R]]∆ iff χ(t) ∈ hhRii∆ .
As a consequence, checking the emptiness of a type under [·]]∆ can be reduced to
checking the emptiness of the type under hh·ii∆ , and vice versa. Therefore, whether
[R]]∆ = ∅ can be decided by employing the algorithm developed in (Lu and Cleary
1998) that checks if hhRii∆ = ∅. The following corollary of the theorem allows us to
reduce a type inclusion test under [·]]∆ to a type inclusion test under hh·ii∆ .
Corollary 7.5
For any R1 , R2 ∈ Type, [R1]∆ ⊆ [R2]∆ iff hhR1 ii∆ ⊆ hhR2 ii∆ .
In order to reduce the decision problems to the emptiness of types, we need to
extend the syntax for type sequence expressions with the operator ∼ and hh·ii∆ to
type sequences. The expression ∼E is a type sequence expression whenever E is a
~ a type sequence in eType∗ ,
type sequence expression. Let R be a type in eType, R
~
E1 and E2 be type sequence expressions. Define hhǫii∆ = {ǫ}, hhR • Rii
∆ = hhRii∆ •
~
hhRii∆ , hhE1 and E2 ii∆ = hhE1 ii∆ ∩ hhE2 ii∆ , hhE1 or E2 ii∆ = hhE1 ii∆ ∪ hhE2 ii∆ and
hh∼ Eii∆ = hh~1ii∆ −hhEii∆ . It can be shown that both Theorem 7.4 and Corollary 7.5
carry over to type sequence expressions that do not contain ∼.
Set inclusion and hh·ii∆ induces an equivalence between types and type sequence
.
.
expressions. Let R1 = R2 iff hhR1 ii∆ = hhR2 ii∆ and E1 = E2 iff hhE1 ii∆ = hhE2 ii∆ .
The following function eliminates the complement operator ∼ over type sequence
expressions.
push(∼(ori∈I Ei ))
push(∼(andi∈I Ei ))
push(∼(R1 , R2 , · · · , Rk ))

= andi∈I push(∼Ei )
= ori∈I push(∼Ei )
= or1≤l≤k (1, · · · , 1, ∼Rl , 1, · · · , 1)
| {z }
| {z }
l−1

for k ≥ 1

k−l

.
It follows from De Morgan’s law and the definition of hh·ii∆ that push(∼E) =
∼E. Note that the complement operator ∼ does not apply to any type sequence
expression in push(∼E); it only applies to type expressions. Let R ∈ eType and
.
define etype(R) = (hhRii∆ = ∅). The formula etype(R) is true iff R = 0 is true. By
Theorem 7.4, if R ∈ Type then etype(R) is true iff R ≡ 0 is true.
7.3 Equivalence between Sets of Variable Typings
An indispensable operation in a static analyzer is to check if a fixpoint has been
reached. This operation reduces to checking if two sets of variable typings denote

28

Lunjin Lu

the same set of concrete substitutions. This equivalence test is reduced to checking
emptiness of types as follows. Let VP = {x1 , · · · , xk } and S1 , S2 ∈ ℘(VP 7→ Type).
S
S
S
By definition, S1 ≈ S2 iff µ∈S1 γVT (µ) ⊆ ν∈S2 γVT (ν) and ν∈S2 γVT (ν) ⊆
S
µ∈S1 γVT (µ). Suppose S1 = {µ1 , µ2 , · · · , µm } and S2 = {ν1 , ν2 , · · · , νn }. We con~ 1, R
~ 2, · · · , R
~ m and T~1 , T~2 , · · · , T~n as follows. R
~ i = hµi (x1 ), µi (x2 ), · · · , µi (xk )i
struct R
S
S
and T~j = hνj (x1 ), νj (x2 ), · · · , νj (xk )i. Then µ∈S1 γVT (µ) ⊆ ν∈S2 γVT (ν) is true
~ i ⊑ or1≤j T~j is true iff
~ i ⊑ or1≤j T~j is true. By Corollary 7.5, or1≤i R
iff or1≤i R
. ~
~
~
(or1≤i Ri ) and ∼(or1≤j Tj ) = 0 is true. The latter can be reduced to emptiness
of types as shown in (Lu and Cleary 1998).
Example 7.6
Let ∆ be given as in Example 4.1, VP = {x, y}, S1 = {µ1 , µ2 } and S2 = {µ3 } where
µ1

= {x 7→ list (even), y 7→ list (nat)}

µ2

= {x 7→ list (odd ), y 7→ list (nat)}

µ3

= {x 7→ list (even) or list (odd ), y 7→ list (nat )}

The truth value of (γVT (µ1 ) ∪ γVT (µ2 )) ⊆ γVT (µ3 ) is decided by testing emptiness
of types as follows. Let
~1
R
~2
R

=

hlist (even), list (nat )i

=

hlist (odd ), list (nat )i

T~1

=

hlist (even) or list (odd ), list (nat )i
. ~
~ 1 or R
~ 2 ) and ∼T~1 =
0 which, by replacing
Then (γVT (µ1 )∪γVT (µ2 )) ⊆ γVT (µ3 ) iff (R
∼T~1 with push(∼T~1 ) and distributing and over or, is equivalent to the conjunction
of the following formulas.
.
hlist (even), list (nat )i and h1, ∼list (nat )i = ~0
.
hlist (odd ), list (nat )i and h1, ∼list (nat )i = ~0
.
hlist (even), list (nat )i and h∼list (even) and ∼list (odd ), 1i = ~0
.
hlist (odd ), list (nat )i and h∼list (even) and ∼list (odd ), 1i = ~0
.
.
The first of the above holds iff either list (even) = 0 or list (nat ) and ∼list (nat ) = 0,
.
both of which are emptiness tests on types. Since list (nat ) and ∼list (nat ) = 0, the
first formula is decided to be true. The other three can be decided to be true
similarly. Therefore, (γVT (µ1 ) ∪ γVT (µ2 )) ⊆ γVT (µ3 ) holds. In a similar way, we can
show that γVT (µ3 ) ⊆ (γVT (µ1 ) ∪ γVT (µ2 )) holds. So, S1 ≈ S2 .
7.4 Redundancy Removal
For the sake of an efficient implementation, an abstract substitution [S]≈ should
be represented by a set of variable typings that does not contain redundancy. A
set of variable typings can be redundant in two ways. Firstly, a variable typing µ
in S may denote the empty set of substitutions i.e., µ(x) ≡ 0 for some x ∈ VP .

Improving Precision of Type Analysis Using Non-Discriminative Union

29

Secondly, a variable typing µ in S can be subsumed by other variable typings in
S
that γVT (µ) ⊆ ν∈S∧ν6=µ γVT (ν). In both cases, S \ {µ} and S denote the same
set of substitutions and µ can be removed from S. Suppose VP = {x1 , · · · , xk }.
The detection of γVT (µ) = ∅ reduces to etype(µ(x1 )) ∨ · · · ∨ etype(µ(xk )) while the
S
detection of γVT (µ) ⊆ ν∈S∧ν6=µ γVT (ν) can be reduced to checking emptiness of
types as in Section 7.3.
Example 7.7
Let ∆ be given Example 4.1, VP = {x, y}, S = {µ1 , µ2 , µ3 } where
µ1

=

{x 7→ list (even), y 7→ list (nat )}

µ2

=

{x 7→ list (odd ), y 7→ list (nat )}

µ3

=

{x 7→ list (nat ), y 7→ list (nat )}

We now show how µ1 is decided to be redundant in S. Let
~1
R
~2
R

=

hlist (even), list (nat )i

=

hlist (odd ), list (nat)i

~3
R

=

hlist (nat ), list (nat )i

. ~
~ 1 and ∼(R
~ 2 or R
~ 3) =
Then γVT (µ1 ) ⊆ γVT (µ2 ) ∪ γVT (µ3 ) holds iff R
0 holds iff
.
~
~ 3 with
~
~
~
~
R1 and ∼R2 and ∼R3 = 0 holds. The latter, after replacing ∼R2 and ∼R
~
~
push(∼R2 ) and push(∼R3 ) respectively and distributing and over or, is equivalent
to the conjunction of the following formulas.
.
hlist (even), list (nat )i and h1, ∼list (nat )i and h1, ∼list (nat )i = ~0
.
hlist (even), list (nat )i and h1, ∼list (nat )i and h∼list (nat ), 1i = ~0
.
hlist (even), list (nat )i and h∼list (odd ), 1i and h1, ∼list (nat )i = ~0
. ~
hlist (even), list (nat )i and h∼list (odd ), 1i and h∼list (nat ), 1i = 0

Each of the above can be decided to be true by testing emptiness of types as in
Example 7.6. Therefore, µ1 is redundant in S. In a similar way, µ2 is decided to
be redundant in S \ {µ1 }. So, S ≈ {µ3 }. That µ3 is not redundant in S is decided
similarly.
7.5 Tabling
The operations in our type analysis are complex because of non-deterministic type
definitions and non-discriminative union at both the level of types and the level
of abstract substitutions. The equality of two abstract substitutions in an analysis
without these features can be done in linear time (Horiuchi and Kanamori 1988;
Kanamori and Horiuchi 1985; Kanamori and Kawamura 1993; Lu 1995). The same
operation is exponential in our type analysis because deciding the emptiness of a
type is exponential. This indicates that our type analysis could be much more time
consuming.
As shown later, there is a high degree of repetition in emptiness checks during

30

Lunjin Lu
Table 2. Time Performance
Program
browse
cs r
disj r
dnf
kalah
life
meta
neural
nbody
press
serialize
zebra

Program Points
103
277
132
77
228
100
89
341
375
318
37
43
Sum = 2120

Goal
q
pgenconﬁg(C)
top(K)
go
play(G, R)
life(MR, MC, LC, SFG)
interpret(G)
go
go(M, G)
test press(X, Y)
go(S)
zebra(E, S, J, U, N, Z, W)

Time
110
661
171
200
590
89
50
250
281
161
80
40
Sum = 2683

the analysis of a program. Making use of this observation, we have reduced time
increase to 15% on average using a simple tabling technique. We memoize each call
to etype(R) and its success or failure by asserting a fact $etype tabled(R, Ans).
The fact $etype tabled(R, yes) (resp. $etype tabled(R, no)) indicates that etype(R)
has been called before and etype(R) succeeded (resp. failed). The tabled version of
etype(R) is etype tabled(R). It first checks if a fact $etype tabled(R, Ans) exists.
If so, the call etype tabled(R) succeeds or fails immediately. Otherwise, it calls
etype(R) and memoizes its success or failure.
We now present some experimental results with the prototype analyzer. The
experiments were done with a Pentium (R) 4 CPU 2.26 GHz running GNU/Linux
and SWI-Prolog-5.2.13.
7.5.1 Time Performance
Table 2 shows analysis time on a suite of benchmark programs. Each row except
the last one corresponds to a test case. The first three columns contain the name,
the size of the program in terms of the number of program points and the top-level
goal. The top abstract substitution which contains no type information is used as
the input abstract substitution for each test case. These test cases will be used
in subsequent tables where only the program names are given. The fourth column
gives analysis time in milliseconds. The time is obtained by running the analyzer ten
times on the test case and averaging analysis time from these runs. Timing data in
other tables are also obtained in this way. The table shows that the analyzer takes
an average of 1.27 milliseconds per program point.
7.5.2 Repetition of Emptiness Checks
Table 3 shows that there is a high degree of repetition in emptiness checks during
analysis. Each test case corresponds to a row of the table. The first column of the
row is the name of the program, the second is the total number of emptiness checks
that occur during analysis. The third column gives the number of different types

Improving Precision of Type Analysis Using Non-Discriminative Union

31

Table 3. Repetition of Emptiness Checks
Program
browse
cs r
disj r
dnf
kalah
life
meta
neural
nbody
press
serialize
zebra

Total
Checks
3050
23846
4500
6290
31182
3277
468
7985
8567
1734
2019
947

Diﬀerent
Checks
64
53
37
9
86
24
13
131
39
23
37
22

Degree of
Repetition
47.65
449.92
121.62
698.88
362.58
136.54
36.00
60.95
219.66
75.39
54.56
43.04
Ave.=192.23

that are checked for emptiness. The fourth column gives the average repetition of
emptiness checks, which is the ratio of the second and the third columns. While
the total number of emptiness checks can be very large for a test case, the number
of different emptiness checks is small, exhibiting a high degree of repetition in
emptiness checks. The repetition of the emptiness checks ranges from 36.00 to
698.88. The weighted repetition average is about 192.23. This motivated the use of
tabling to reduce the time spent on emptiness checks.

7.5.3 Effect of Tabulation
Table 4 illustrates the effect of tabling. Statistics are obtained by running the
analyzer with and without tabling. For both experiments, we measured analysis
time and time spent on emptiness checks. The table shows that tabling reduces
1
. The table also gives the proportion of analysis time that is
analysis time to 2.6
spent on emptiness checks. An average of 53% of analysis time is spent on emptiness
checks without tabling while only a negligible portion of analysis time is spent on
emptiness checks with tabling.

7.6 Cost and Effect of Precision Improvement Features
The precision improvement features in our type analysis all incur some performance
penalty. In order to evaluate the effect of these features, we also implemented a simplified type analysis. The simplified analysis is obtained by removing the precision
improvement features from the full-fledged analysis. In the simplified analysis, type
expressions do not contain the constructors or or and; an abstract substitution
is simply a variable typing; and non-deterministic type definitions are disallowed.
Function overloading is still allowed. Abstract operations are simplified accordingly.
For instance, since (list (list (nat )) or list (nat )) is not in the type language of the
simplified analysis, the least upper bound of list (list (nat )) and list (nat) is list (1).

32

Lunjin Lu
Table 4. Effect of Tabulation
Program
browse
cs r
disj r
dnf
kalah
life
meta
neural
nbody
press
serialize
zebra

With Tabling
Analysis Check
Time
Time Proportion
110
10
0.09
661
0
0
171
0
0
200
0
0
590
0
0
89
0
0
50
0
0
250
30
0.12
281
0
0
161
0
0
80
0
0
40
0
0
Sum=2683
Ave.=0.01

Without Tabling
Analysis Check
Time
Time Proportion
269
129
0.47
1700
891
0.52
359
157
0.43
581
363
0.62
1939
1124
0.57
210
117
0.55
60
21
0.35
731
469
0.64
620
314
0.50
250
29
0.11
179
82
0.45
70
31
0.44
Sum=6968
Ave.=0.53

Table 5. Cost and Effect of Precision Improvement Features
Program

browse
cs r
disj r
dnf
kalah
life
meta
neural
nbody
press
serialize
zebra

Simpliﬁed
Analysis
Time
100.00
589.00
151.00
190.00
420.00
89.00
40.00
200.00
231.00
159.00
80.00
40.00

Full-ﬂedged
Analysis
Time
110.00
661.00
171.00
200.00
590.00
89.00
50.00
250.00
281.00
161.00
80.00
40.00

Time
Ratio

Precision
Ratio

0.90
0.89
0.88
0.95
0.71
1.00
0.80
0.80
0.82
0.98
1.00
1.00
Ave. =0.85

0.74
0.77
0.73
0.00
0.49
0.35
0.05
0.49
0.23
0.95
0.83
0.35
Ave. =0.54

The least upper bound operation on abstract substitutions is the point-wise extension of the least upper bound operation on types.
Table 5 compares two type analyses. The two analyses are performed on each
test case with the same input type information. The input abstract substitution for
the full-fledged analysis is a singleton set of a variable typing. The corresponding
abstract substitution for the simplified analysis is the variable typing. For each test
case, the table gives analysis times by the two analyzers and their ratio. The relative
performance of the two analyzers varies with the test case. On average, the simplified
analysis takes 85 percent of the analysis time of the full-fledged type analysis. This
illustrates that the precision improvement features does not substantially increase
analysis time.
The fifth column in Table 5 gives information about the effect of the precision
improvement features. For each program, it lists the ratio of the number of the pro-

Improving Precision of Type Analysis Using Non-Discriminative Union

33

gram points at which the full-fledged analysis derives more precise type information
than the simplified analysis over the number of all program points. Whether or not
these features improve analysis precision depends on the program that is analysed.
For some programs like dnf and meta, there is little or no improvement. For some
other programs like press and serialize, there is a substantial improvement. On average, the full-fledged analysis derives more precise type information at 54% of
the program points in a program. This indicates that the precision improvement
features is cost effective.
7.7 Termination
The abstract domain of our type analysis contains chains of infinite length, which
may lead to non-termination of the analysis of a program.
Example 7.8
Let the program consist of a single clause p(x) :- ⊛ p([x]) where ⊛ is a label of
a program point. Let the query be of the form :- p(u) with u being of type nat.
Then x is a term of type list i (nat ) at the ith time the execution reaches the program
point ⊛. Thus, the chain of the abstract substitutions at the program point ⊛ is
{{x 7→ list (nat)}}
{{x 7→ list (nat)}, {x 7→ list (list (nat ))}}
..
.
{{x 7→ list j (nat)} | 0 < j ≤ k}
..
.
which is infinite. The program is an instance of polymorphic recursion (Kahrs 1996)
which is prohibited in ML.
The analyzer uses a canonical representation of types and a depth abstraction
to ensure termination. A conjunctive type is compact if it contains no duplicated
type atoms. A type in disjunctive normal form is compact if it contains no duplicated conjuncts and all of its conjuncts are compact. A type is canonical if it is
in disjunctive normal form, it is compact and all arguments of its type atoms are
canonical. For every type R, a canonical equivalent of R – a canonical type Rc such
that Rc ≡ R – can be obtained as follows. A disjunctive normal form R ′ of R is
first computed. Each argument of each type atom in R ′ is then replaced with its
canonical equivalent, resulting in a type R ′′ . Finally, Rc is obtained by deleting
duplicate type atoms in each conjunct of R ′′ and then deleting duplicate conjuncts.
Let cn(R) denote the canonical equivalent of R obtained by the above procedure.
For instance, cn(tree(tree(list (1) or list (1)))) = tree(tree(list (1))).
Let R be a type. An atomic sub-term A of R is both a sub-term of R and a type
atom. The depth of A in R is the number of the occurrences of type constructors
in Cons on the path from the root of R to but excluding the root of A. Thus, the
depth of the only occurrence of list (nat ) in tree(tree(list (even) or list (list (nat ))))
is 3 and the depth of the only occurrence of list (even) in the same type is 2. Note

34

Lunjin Lu

that type constructors and and or are ignored in determining the depth of A in R.
If the depth of A in R is k then A is called an atomic sub-term of R at depth k. The
depth of R is defined as the maximum of the depths of all its atomic sub-terms.
Definition 7.9
Let R be a type and k a positive integer. The depth k abstraction of R, denoted
as dk (R), is the result of replacing each argument of any atomic sub-term of R at
depth k by 1.
For instance,
d2 (tree(tree(list (even) or list (list (nat )))))
= tree(tree(list (1) or list (1)))
During analysis, the abstract substitution for a program point is initialized to
the empty set of variable typings. It is updated by adding new variable typings and
removing redundant ones. The analyzer ensures termination as follows. For each
program point, the analyzer determines a depth k the first time a non-empty set
of variable typings S0 is added. The depth k is the maximum of the depths of the
types occurring in S0 plus some fixed constant k0 with k0 ≥ 0. After that, each
time a set of variable typings S is added, each type R occurring in S is replaced
by cn(dk (cn(R))). The above abstraction preserves analysis correctness because
R ′ ⊑ dk (R ′ ) and cn(R) ≡ R. The number of depth k abstractions of the canonical
types occurring in the abstract substitution is bounded and so is the number of
variable typings in the abstract substitution. This ensures termination.
Example 7.10
Continue Example 7.8 and let k0 = 1. We have S0 = {{x 7→ list (nat )}} and hence
k = 2 since the depth of the only type list (nat ) in S0 is 1. The chain of the abstract
substitutions for the program point ⊛ is
{{x 7→ list (nat )}}
{{x 7→ list (nat )}, {x 7→ list (list (nat))}}
{{x 7→ list (nat )}, {x 7→ list (list (nat))}, {x 7→ list (list (list (1)))}}
The last in the chain is the final abstract substitution for the program point ⊛.
8 Related Work
There is a rich literature on type inference analysis for logic programs. Type analyses in (Frühwirth et al. 1991; Gallagher and de Waal 1994; Gallagher and Puebla
2002; Mishra 1984; Zobel 1987) are performed without a priori type definitions.
They generate regular tree grammars, or type graphs (Van Hentenryck et al. 1995;
Janssens and Bruynooghe 1992) or set constraints (Heintze and Jaffar 1990; Heintze
and Jaffar 1992) as type definitions. These different formalisms for expressing type
definitions are equivalent. A type graph is equivalent to a regular tree grammar
such that a production rule in the grammar corresponds to a subgraph that is composed of a node and its successors in the graph. For a system of set constraints,

Improving Precision of Type Analysis Using Non-Discriminative Union

35

there is a regular tree grammar that generates the least solution to the system of
set constraints, and vice versa (Cousot and Cousot 1995). The production rules in
a regular tree grammar are similar to type rules used in our analysis but are not
parameterized. This kind of analysis is useful for compiler-time optimizations and
transformations but inferred type definitions can be difficult for the programmer to
interpret. Like those in (Horiuchi and Kanamori 1988; Kanamori and Horiuchi 1985;
Barbuti and Giacobazzi 1992; Kanamori and Kawamura 1993; Codish and Demoen
1994; Lu 1995; Saglam and Gallagher 1995; Codish and Lagoon 2000; Lu 1998; Hill
and Spoto 2002), our type analysis is performed with a priori type definitions. The
type expressions it infers are formed of given type constructors. Since the meaning
of a type constructor is given by a priori type definitions that are well understood
to the programmer, the inferred types are easier for the programmer to interpret
and thus they are more useful in an interactive programming environment.
The type analyses with a priori type definitions in (Horiuchi and Kanamori 1988;
Kanamori and Horiuchi 1985; Kanamori and Kawamura 1993; Lu 1995) are based
on top-down abstract interpretation frameworks. They are performed with a type
description of possible queries as an input and are thus goal-dependent. They infer
for each program point a type description of all the program states that might be
obtained when the execution of the program reaches that program point. These are
also characteristics of our analysis. However, these analyses do not support nondeterministic type definitions or non-discriminative union at the levels of types and
abstract substitutions. The analysis in (Lu 1998) traces non-discriminative union
at the level of abstract substitutions but not at the level of types. In addition, it
does not allow non-determinism in type definitions. The above mentioned top-down
type analyses with a priori type definitions approximate non-discriminative union
of two types by their least upper bound. The least upper bound may have a strictly
larger denotation than the set union of the denotations of the two types since set
union is not a type constructor. Thus, our type analysis is strictly more precise
than (Horiuchi and Kanamori 1988; Kanamori and Horiuchi 1985; Kanamori and
Kawamura 1993; Lu 1995; Lu 1998).
The type analyses with a priori type definitions in (Barbuti and Giacobazzi
1992; Codish and Demoen 1994; Saglam and Gallagher 1995; Codish and Lagoon
2000; Hill and Spoto 2002) are based on bottom-up abstract interpretaion frameworks. They infer a type description of the success set of the program. The inferred type description is a set of type atoms each of which is a predicate symbol applied to a tuple of types. Some general remarks can be made about the
differences between our analysis and these analyses. Firstly, our analysis is goaldependent while these analyses are goal-independent. Secondly, our analysis allows
non-deterministic type definitions that are disallowed by these analyses. Consequently, more natual typings are allowed by our type analysis than by these analyses. However, non-deterministic type definitions also make abstract operations in
our analysis more complex than in these analyses. Thirdly, like our analysis, these
analyses can express non-discriminative union at the level of predicates. For example, the two type atoms p(list (integer)) and p(tree(integer)) express the same
information as hp(x), x ∈ (list (integer) or tree(integer))i in our type analysis. How-

36

Lunjin Lu

ever, these analyses except an informal proposal in (Barbuti and Giacobazzi 1992)
cannot trace non-discriminative union at the level of arguments, which leads to
imprecise analysis results. For instance, the inferred type for the concrete atom
p([1, [1]]) is p(list (1)) according to (Codish and Demoen 1994; Saglam and Gallagher 1995; Codish and Lagoon 2000; Hill and Spoto 2002) and the main proposal
in (Barbuti and Giacobazzi 1992). The inferred type p(list (1)) is less precise than
hp(x), x ∈ list (integer or list (integer))i which is inferred by our type analysis.
Lastly, as a minor note, set intersection is not used as a type constructor in these
type analyses except (Hill and Spoto 2002). The two type clauses x(list (β)) ← and
x(tree(β)) ← in an abstract substitution of (Hill and Spoto 2002) indicates that
x is both a list and a tree. Some comparisons on other aspects between our type
analysis and these bottom-up analyses are in order.
Barbuti and Giacobazzi (1992) infer polymorphic types of Horn clause logic programs using a bottom-up abstract interpretation framework (Barbuti et al. 1993).
The type description of the success set of a Horn logic program is computed as the
least fixed-point of an abstract immediate consequence operator associated with
the program. The abstract immediate consequence operator is defined in terms of
abstract unification and abstract application. Abstract unification computes an abstract substitution given a term and a type. Abstract application computes a type
given an abstract substitution and a term. Both computations are derivations of
a Prolog program that is derived from a priori type definitions. The inferred type
description describes only part of the success set of the program though abstract
operations can be modified so that the type description approximates the whole
success set. Ill-typed atoms are not described by the type description. Nor are
those well-typed atoms that possess only ill-typed SLD resolutions. An SLD resolution is ill-typed if any of its selected atoms is ill-typed. Their type definitions are
slightly different form ours. For instance, they define the type of the empty list [ ] as
[ ] → list (⊥) which is equivalent to list (0)_[ ] in our notation whilst the empty list
[ ] is typed by list (β)_[ ] in our analysis. Barbuti and Giacobazzi also informally
introduced and exemplified an associative, commutative and idempotent operator
∪ that expresses non-deterministic union at the level of types. However, abstract
unification and abstract application operations for this modified domain of types
are not given. In addition, it requires changing type definitions, for instance, from
cons(β, list (β)) → list (β) to cons(α, list (β)) → list (α∪β). Barbuti and Giacobazzi’s
analysis captures more type dependency than ours. This is achieved through type
parameters. For instance, the type description for the program {p(X, [X]) ←} is
{p(α, list (α))}. Abstract unification of the query p(X, Y ) with the only type atom
in the type description yields the abstract substitution {X 7→ α, Y 7→ list (α)}, This
kind of type dependency will be lost in our analysis. The use of type parameters
and the use of non-discriminative union are orthogonal to each other and it is an
interesting topic for future research to combine them for more analysis precision.
Codish and Demoen (1994) apply abstract compilation (Hermenegildo et al. 1992)
to infer type dependencies by associating each type with an incarnation of the abstract domain Prop (Marriott and Søndergaard 1989). The incarnations of Prop
define meanings of types and capture interactions between types. The type depen-

Improving Precision of Type Analysis Using Non-Discriminative Union

37

dencies of a logic program is similar to the type description of the program inferred
by the type analysis of Barbuti and Giacobazzi (1992) except that the type dependencies describe the whole success set of the program. Codish and Lagoon (2000)
improve (Codish and Demoen 1994) by augmenting abstract compilation with ACIunification. An associative, commutative and idempotent operator ⊕ is introduced
to form the type of a term from the types of its sub-terms. It has the flavor of set
union. Nevertheless, it does not denote the set union. For an example, the term
[1, [1]] has type list (integer) ⊕ list (list (integer)) according to (Codish and Lagoon
2000) while it has type list (integer or list (integer)) in our type analysis. Like (Barbuti and Giacobazzi 1992), type analyses in (Codish and Demoen 1994; Codish and
Lagoon 2000) capture type dependency via type parameters. In addition, they have
the desired property of condensing which our analysis does not have.
Hill and Spoto (2002) provide a method that enriches an abstract domain with
type dependency information. The enriched domain contain elements like (x ∈
nat) → (y ∈ list (nat )) meaning if x has type nat then y has type list (nat). Each
element in the enriched domain is represented as a logic program. Type analysis is
performed by abstract compilation. Their approach to improving precision of type
analysis is different from ours. Their domain can express type dependencies that
ours cannot whilst our domain can express non-discriminative union at the level
of types but theirs cannot. Hill and Spoto do not take subtyping into account in
their design of abstract operations possibly because subtyping is outside the focus
of their work.
Gallagher and de Waal (1994) approximates the success set of the program by a
unary regular logic program (Yardeni and Shapiro 1991). This analysis infers both
type definitions and types and is incorporated into the Ciao System (Hermenegildo
et al. 1999). Saglam and Gallagher (1995) extend (Gallagher and de Waal 1994) by
allowing the programmer to supply deterministic type definitions for some function
symbols. The supplied type definitions are used to transform the program and the
transformed program is analyzed as in (Gallagher and de Waal 1994). An interesting
topic for further study is to integrate non-deterministic type definitions and nondiscriminative union into (Saglam and Gallagher 1995) and evaluate their impact
on analysis precision and analysis cost.
Finally, it is also worthy mentioning work on directional types (Bronsard et al.
1992; Aiken and Lakshman 1994; Boye and Malúszynski 1996; Charatonik and
Podelski 1998; Rychlikowski and Truderung 2001). Aiken and Lakshman (1994)
present an algorithm for automatic checking directional types of logic programs.
Directional types describe both the structure of terms and the directionality of
predicates. A directional type for a predicate p/n is of the form τI → τO . Type
τI is called an input type and type τO an output type. They are type tuples of
dimension n. The directional type expresses two requirements. Firstly, if p/n is
called with an argument of type τI then the argument has type τO upon its success.
Secondly, each predicate q/m invoked by p is called with an argument that has the
input type of a directional type for q/m. A program is well-typed with respect to
a collection of directional types if each directional type in the collection is verified.
The type checking problem is reduced to a decision problem on systems of inclusion

38

Lunjin Lu

constraints over set expressions. The algorithm is sound and complete for discriminative directional types. Charatonik and Podelski (1998) provide an algorithm for
inferring directional types with respect to which the program is well-typed.

9 Conclusion
We have presented a type analysis. The type analysis supports non-deterministic
type definitions, allows set operators in type expressions, and uses a set of variable
typings to describe type information in a set of substitutions. The analysis is presented as an abstract domain and four abstract operations for Nilsson’s abstract
semantics (Nilsson 1988) extended to deal with negation and built-in predicates.
These operations are defined in detail and their local correctness proved. The abstract unification involves propagation of type information downwards and upwards
the structure of a term. Given a set of equations in solved form and an abstract
substitution, abstract unification is accomplished in two steps. In the first step,
more type information for variables occurring on the right-hand side of each equation is derived from type information for the variable on the left-hand side. The
second step derives more type information for the variable on the left-hand side
of each equation from type information for the variables on the right-hand side.
The abstract built-in execution operation approximates the execution of built-in
predicates. Each built-in is modeled as a function of abstract substitutions.
Detection of the least fixpoint and elimination of redundancy in a set of variable
typings are both reduced to checking the emptiness of types. Though types denote
sets of possibly non-ground terms and are not closed under set complement, checking the emptiness of types can be done by using an algorithm that checks for the
emptiness of the types that denote sets of ground terms. An experimental study
shows that due to a large repetition of emptiness checks, with tabling, the precision
improvement measures incurs only a small increase in analysis time.
Acknowledgments: The work is supported in part by the National Science Foundation under grants CCR-0131862 and INT-0327760. A preliminary version of this
article appeared, under the title “A Precise Type Analysis of Logic Programs”, in
Proceedings of the Second International ACM SIGPLAN Conference on Principles
and Practice of Declarative Programming, Montreal, Canada, 2000. We would like
to thank anonymous reviewers for insightful comments on previous drafts of this
report.

Appendix A Proofs
Let N denote the set of natural numbers. Define h : Term(Σ, Var) 7→ N as follows.
h(x) = 0 for all x ∈ Var and h(f (t1 , · · · , tn )) = 1 + max{h(ti ) | 1 ≤ i ≤ n}.
Define h : Type 7→ N in the same way. Note h(R) ≥ 1 for any R ∈ Type. Let
hx1 , y 1 i ≺ hx2 , y 2 i = (x1 < x2 ) ∨ ((x1 = x2 ) ∧ (y 1 < y 2 )).

Improving Precision of Type Analysis Using Non-Discriminative Union

39

Lemma 4.4. Let R ∈ Type and t ∈ Term. If t ∈ [R]]∆ then σ(t) ∈ [R]]∆ for any
σ ∈ Sub.
Proof
The proof is done by induction on hh(t), h(R)i. Let σ ∈ Sub be an arbitrary substitution.
Basis. We have that h(t) = 0 and that h(R) = 1. So, t ∈ Var which implies R = 1
since t ∈ [R]]∆ and h(R) = 1. Thus, [R]]∆ = Term and σ(t) ∈ [R]]∆ .
Induction. Either that h(t) = 0 or that h(t) > 0. Consider the case where h(t) = 0
first. Then t ∈ Var. Either (i) R = 1; (ii) R = R1 or R2 ; or (iii) R = R1 and R2 . The
case (i) is a special case of the base case. Consider the case (ii). We have either that
t ∈ [R1]∆ or that t ∈ [R2]∆ . If t ∈ [Rj ]∆ then, by induction hypothesis, σ(t) ∈ [Rj ]∆
for j = 1, 2 since h(Rj ) < h(R). So, σ(t) ∈ [R]]∆ by the definition of [·]]∆ . The case
(iii) is symmetric to the case (ii). Thus, σ(t) ∈ [R]]∆ .
Now consider the case where h(t) > 0. Then t = f (t1 , · · · , tn ). Either (i) R = 1;
(ii) R = R1 or R2 ; (iii) R = R1 and R2 ; or (iv) R = c(R1 , · · · , Rm ). The proof
for that σ(t) ∈ [R]]∆ in the cases (i), (ii) and (iii) is the same as in the previous paragraph. Consider the case (iv). Since t ∈ [R]]∆ , there is a type rule
c(β1 , · · · , βm )_f (τ1 , · · · , τn ) such that tj ∈ [k(τj )]]∆ where k = {β1 7→ R1 , · · · , βm 7→
Rm }. We have that h(k(τj )) ≤ h(R) and that h(tj ) < h(t). By the induction hypothesis, σ(tj ) ∈ [k(τj )]]∆ , which together with the definition for [·]]∆ , implies that
σ(t) ∈ [R]]∆ .
Lemma 5.2. γ(ASub ♭ ) is a Moore family.
Proof
Since, γ([{x 7→ 1 | x ∈ VP }]≈ ) = Sub and Sub is the supremum on ℘(Sub), γ(ASub ♭ )
contains the supremum on ℘(Sub). Let [S1 ]≈ , [S2 ]≈ ∈ ASub ♭ . Then [S1 ]≈ ⊓♭ [S2 ]≈ ∈
ASub ♭ . Furthermore,
γ([S1 ]≈ ⊓♭ [S2 ]≈ )

= γ([S1↓ ∩ S2↓ ]≈ )
[
[
γVT (ν))
γVT (µ)) ∩ (
= (
ν∈S2↓

µ∈S1↓

= (

[

γVT (µ)) ∩ (

µ∈S1

[

γVT (ν))

ν∈S2

= γ([S1 ]≈ ) ∩ γ([S2 ]≈ )
♭

Thus, γ(ASub ) is closed under ∩ – the meet on ℘(Sub). So, γ(ASub ♭ ) is a Moore
family.
Lemma 5.3. γ([S1 ⊗ S2 ]≈ ) = γ([S1 ]≈ ⊓♭ [S2 ]≈ ).
Proof
We first prove that γ([S1 ⊗ S2 ]≈ ) ⊆ γ([S1 ]≈ ⊓♭ [S2 ]≈ ). Let θ ∈ γ([S1 ⊗ S2 ]≈ ). Then
there is ρ in (S1 ⊗ S2 ) such that θ ∈ γVT (ρ). This implies that there are µ in S1
and ν ∈ S2 such that ρ = λx ∈ VP .(µ(x) and ν(x)). We have γVT (ρ) ⊆ γVT (µ) and

40

Lunjin Lu

γVT (ρ) ⊆ γVT (ν), implying ρ ∈ S1↓ and ρ ∈ S2↓ . Therefore, ρ ∈ (S1↓ ∩ S2↓ ). Since
θ ∈ γVT (ρ), we have that θ ∈ γ([S1↓ ∩ S2↓ ]≈ ) and θ ∈ γ([S1 ]≈ ⊓♭ [S2 ]≈ ).
We now prove that γ([S1 ⊗ S2 ]≈ ) ⊇ γ([S1 ]≈ ⊓♭ [S2 ]≈ ). Let θ ∈ γ([S1 ]≈ ⊓♭ [S2 ]≈ ).
Then θ ∈ γVT (ρ) for some ρ ∈ (S1↓ ∩S2↓ ) by the definition of ⊓♭ . There are µ ∈ S1 and
ν ∈ S2 such that γVT (ρ) ⊆ γVT (µ) and γVT (ρ) ⊆ γVT (ν), implying ∀x ∈ VP .(θ(x) ∈
[µ(x) and ν(x)]]∆ ). Thus, θ ∈ γ([S1 ⊗ S2 ]≈ ) by the definition of ⊗.
Lemma 6.1. For any R ∈ Type and t ∈ Term(Σ, VP′ ), {θ | θ(t) ∈ [R]]∆ } ⊆
γ([vts(R, t)]≈ ).
Proof
The proof is done by induction on hh(t), h(R)i.
Basis. hh(t), h(R)i = h0, 1i. Then t ∈ VP′ and
vts(R, t) = {λx ∈ VP′ .(if x = t then R else 1)}
The lemma holds since {θ | θ(t) ∈ [R]]∆ } = γ([vts(R, t)]≈ ).
Induction. Assume that the lemma holds for all R ′ ∈ Type and t′ ∈ Term(Σ, VP′ )
such that hh(t′ ), h(R ′ )i ≺ hh(t), h(R)i. Either (1) h(R) > 1 or (2) h(R) = 1.
Consider the case (1). Either (i) R = R1 and R2 or (ii) R = R1 or R2 or (iii)
R = c(R1 , · · · , Rm ) for some m ≥ 1. The cases (i) and (ii) are immediate. Consider
the case (iii). By the definition of [·]]∆ , θ(f (t1 , · · · , tn )) ∈ [R]]∆ implies that there
is a type rule c(β1 , · · · , βm )_f (τ1 , · · · , τn ) in ∆ such that θ(ti ) ∈ [k(τi )]]∆ where
k = {βj 7→ Rj | 1 ≤ j ≤ m}. We have h(ti ) < h(f (t1 , · · · , tn )). By the induction
hypothesis,
θ ∈ γ([vts(k(τi ), ti )]≈ )
for all 1 ≤ i ≤ n. By Lemmas 5.2 and 5.3,


O
θ ∈ γ(
vts(k(τi ), ti ) )
1≤i≤n

≈

By the definition of vts, we have
θ ∈ γ([vts(c(R1 , · · · , Rm ), f (t1 , · · · , tn ))]≈ )
Thus, the lemma holds for the case (1).
Now consider the case (2). We have that t = f (t1 , · · · , tn ). The proof is the same
as that for the case (1).(iii).
Lemma 6.3. Let S ′ = down(E, S). Then mgu(θ(E)) ◦ θ ∈ γ([S ′ ]≈ ) for all θ ∈
γ([S]≈ ).
Proof
N
Let Sµ = {µ} ⊗ (x=t)∈E vts(µ(x), t). It suffices to prove that mgu(σ(E)) ◦ σ ∈
γ([Sµ ]≈ ) for all σ ∈ γVT (µ). mgu(σ(E)) ◦ σ ∈ γVT (µ) as the denotation of any type
in Type is closed under substitution. By Lemma 6.1, we have mgu(σ(E)) ◦ σ ∈
γ([vts(µ(x), t)]≈ ) for any (x = t) in E. So, mgu(σ(E)) ◦ σ ∈ γ([Sµ ]≈ ).

Improving Precision of Type Analysis Using Non-Discriminative Union

41

Lemma 6.5. For any τ ∈ Schm and any k1 , k2 ∈ TSub,
(a) (k1 (τ ) or k2 (τ )) ⊑ (k1 g k2 )(τ ); and
(b) (k1 (τ ) and k2 (τ )) ≡ (k1 f k2 )(τ ).
Proof
We prove only (a) since the proof for (b) is similar to that for (a). Let t ∈
[k1 (τ ) or k2 (τ )]]∆ . Either (1) t ∈ [k1 (τ )]]∆ or (2) t ∈ [k2 (τ )]]∆ . Without loss of generality, we assume (1). We prove t ∈ [(k1 g k2 )(τ )]]∆ by induction on hh(τ ), h(t)i.
Basis. h(τ ) = 0. Then τ ∈ Para and (a) holds since (k1 (τ ) or k2 (τ )) ≡ (k1 g k2 )(τ )
by definition of g.
Induction. h(τ ) 6= 0 implies that τ = c(τ1 , · · · , τm ). If t ∈ Var then k1 (τ ) ≡ 1
and hence (k1 g k2 )(τ ) ≡ 1 and t ∈ [(k1 g k2 )(τ )]]∆ . Otherwise, t = f (t1 , · · · , tn ).
Since t ∈ [k1 (τ )]]∆ , there is a type rule τ _f (τ1 , · · · , τn ) such that ti ∈ [k1 (τi )]]∆ for
1 ≤ i ≤ n. We have h(τi ) ≤ h(τ ) and h(ti ) < h(t). Thus, ti ∈ [(k1 g k2 )(τi )]]∆ by
the induction hypothesis and hence t ∈ [(k1 g k2 )(τ )]]∆ by the definition [·]]∆ .
~ ∈ Type∗ and ~τ ∈
Lemma 6.7. Let K1 , K2 ∈ ℘(TSub), R ∈ Type, τ ∈ Schm, R
∗
~ ⊑ ork2 ∈K2 k2 (~τ ) then
~ = k~τ k. If R ⊑ ork1 ∈K1 k1 (τ ) and R
Schm such that kRk
b
~
R • R ⊑ ork∈(K1 K2 ) k(τ • ~τ ).
Proof
~ ] . Then t ∈ [R]] and ~t ∈ [R]
~ ] . By assumption, there are k1 ∈ K1
Let t • ~t ∈ [R • R]
∆
∆
∆
such that t ∈ [k1 (τ )]]∆ and k2 ∈ K2 such that ~t ∈ [k2 (~τ )]]∆ . Let k = k1 g k2 . We have
b
b
k ∈ (K1 K2 ) by the definition of and t ∈ [k(τ )]]∆ and ~t ∈ [k(~τ )]]∆ by Lemma 6.5.
Thus, t • ~t ∈ [k(τ • ~τ )]]∆ by the definition of [·]]∆ .
Lemma 6.9. Let τ ∈ Schm, R ∈ Type and K = cover (R, τ ). Then R ⊑ ork∈K k(τ ).
Proof
The proof is done by induction on the structure of R.
Basis. R is atomic. R = 1 or R = 0 or R = c(R1 , · · · , Rm ) for some c/m ∈ Cons
and R1 , · · · , Rm ∈ Type. If R = 1 or R = 0 then the lemma holds by the definitions
of ⊤, ⊥ and [·]]∆ . Let R = c(R1 , · · · , Rm ). Either (a) τ ∈ Para or (b) τ = d(β1 , · · · , βk )
with β1 , · · · , βk being different type parameters in Para. In the case (a), we have
K = {k} with k = {τ 7→ R}. The lemma holds because k(τ ) = R. Consider the case
(b), if c/m = d/k then K = {k} with k = {βj 7→ Rj | 1 ≤ j ≤ m} by the definition
of cover and we have k(τ ) = R. Otherwise, K = {k} with k = ⊤ by the definition
of cover and k(τ ) = 1 by the definition of ⊤. So, the lemma holds in the case (b).
Induction. Either (1) R = R1 or R2 or (2) R = R1 and R2 . In the case (1),
S
let K1 = cover (R1 , τ ) and K2 = cover (R2 , τ ). We have [Ri]∆ ⊆ k∈Ki [k(τ )]]∆ for
1 ≤ i ≤ 2 by the induction hypothesis. Therefore,
[R1 or R2]∆

= [R1]∆ ∪ [R2]∆
[
[
⊆
[k(τ )]]∆ ∪
[k(τ )]]∆
k∈K1

k∈K2

42
=

Lunjin Lu
[

[k(τ )]]∆

k∈(K1 ∪K2 )

[

=

[k(τ )]]∆

k∈cover(R,τ )

So the lemma holds for the case (1). Consider the case (2). Let K1 = cover (R1 , τ )
S
and K2 = cover (R2 , τ ). We have [Ri]∆ ⊆ k∈Ki [k(τ )]]∆ for 1 ≤ i ≤ 2 by the
induction hypothesis. So,
[R1 and R2]∆

= [R1]∆ ∩ [R2]∆
[
[
⊆
[k(τ )]]∆ ∩
[k(τ )]]∆
k∈K1

k∈K2

[

=

k∈(K1

c

[k(τ )]]∆ by Lemma 6.5.(b)
K2 )

[

=

[k(τ )]]∆

k∈cover(R,τ )

Thus, the lemma holds for the case (2).
Lemma 6.11. Let t ∈ Term(Σ, VP′ ) and µ ∈ (VP′ 7→ Type). Then θ(t) ∈ [type(t, µ)]]∆
for all θ ∈ γVT (µ).
Proof
The proof is done by induction on h(t).
Basis. h(t) = 0. Then t ∈ VP′ and type(t, µ) = µ(t). The lemma holds.
Induction. h(t) > 0. Let t = f (t1 , · · · , tn ) and Ri = type(ti , µ) for i ∈ {1, · · · , n}
and θ ∈ γVT (µ). By the induction hypothesis, we have θ(ti ) ∈ [Ri]∆ for all 1 ≤ i ≤ n.
Let τ _f (τ1 , · · · , τi ) be a type rule in ∆ and Ki = cover (Ri , τi ). By Lemma 6.9,
S
S
[k(hτ1 , · · · , τn i)]]∆
[Ri]∆ ⊆ k∈Ki [k(τi )]]∆ . Thus, [hR1 , · · · , Rn i]]∆ ⊆ k∈(b
1≤i≤n Ki )
S
b
by Lemma 6.7, which implies θ(t) ∈ k∈(
[k(τ )]]∆ by the definition of [·]]∆ .
1≤i≤n Ki )
This is true of each type rule for f /n. Therefore, θ(t) ∈ [type(t, µ)]]∆ .
Lemma 6.13. Let S ∈ ℘(VP′ 7→ Type) and E ∈ ℘(Eqn). Then mgu(θ(E)) ◦ θ ∈
γ([up(E, S)]≈ ) for all θ ∈ γ([S]≈ ).
Proof
Let



if ∃t.(x = t) ∈ E
µ′ = λx ∈ VP′ .  then µ(x) and type(t, µ) 
else µ(x)

It suffices to prove that mgu(σ(E))◦σ ∈ γVT (µ′ ) for all σ ∈ γVT (µ). By Lemma 6.11,
σ(t) ∈ [type(t, µ)]]∆ . We have (mgu(σ(E)) ◦ σ)(x) ∈ [type(t, µ)]]∆ for all x and t such
that (x = t) ∈ E. Therefore, (mgu(σ(E)) ◦ σ) ∈ γVT (µ′ ).
Theorem 6.16. For any [S1 ]≈ , [S2 ]≈ ∈ ASub ♭ and any a1 , a2 ∈ AtomP ,
Uf (a1 , γ([S1 ]≈ ), a2 , γ([S2 ]≈ )) ⊆

γ(Uf ♭ (a1 , [S1 ]≈ , a2 , [S2 ]≈ ))

Improving Precision of Type Analysis Using Non-Discriminative Union

43

Proof
We first prove a preliminary result on substitution and unification. Let η, θ ∈ Sub
and E, E1 , E2 ∈ ℘(Eqn) and assume that θ = mgu(η(E)) ◦ η 6= fail . Recall that
mgu(E1 ∪ E2 ) = mgu(E1 ∪ eq(mgu(E2 ))) and mgu(η(E)) = mgu(eq(η) ∪ E) (Eder
1985). Then
mgu(θ(E)) ◦ θ

=

mgu(mgu(η(E)) ◦ η(E)) ◦ mgu(η(E)) ◦ η

=

mgu(mgu(η(E))(η(E))) ◦ mgu(η(E)) ◦ η

=

mgu(eq(mgu(η(E))) ∪ eq(η) ∪ E) ◦ mgu(η(E)) ◦ η

=

mgu(eq(mgu(eq(η) ∪ E)) ∪ eq(η) ∪ E) ◦ mgu(η(E)) ◦ η

=

mgu(eq(η) ∪ E ∪ eq(η) ∪ E) ◦ mgu(η(E)) ◦ η

=

mgu(eq(η) ∪ E) ◦ mgu(η(E)) ◦ η

=

mgu(η(E)) ◦ mgu(η(E)) ◦ η

=

mgu(η(E)) ◦ η

=

θ

We are now ready to prove the theorem. Let θ1 ∈ γ([S1 ]≈ ), θ2 ∈ γ([S2 ]≈ ) and
E0 = eq ◦ mgu(Ψ(a1 ), a2 ). Assume that uf (a1 , θ1 , a2 , θ2 ) 6= fail . It is equivalent
to prove uf (a1 , θ1 , a2 , θ2 ) ∈ γ(Uf ♭ (a1 , [S1 ]≈ , a2 , [S2 ]≈ )). By the definition of γ and
rest, if ζ ∈ γ([S]≈ ) then ζ ∈ γ([rest (S)]≈ ) for any substitution ζ and any set
of variable typings over VP′ . Thus, it suffices to prove that uf (a1 , θ1 , a2 , θ2 ) ∈
U
γ([up(E0 , down(E0 , Ψ(S1 ) S2 ))]≈ ) by the definitions for Uf ♭ and solve. Without loss of generality, assume that Ψ renames θ1 (a1 ) apart from θ2 (a2 ). Let η =
θ2 ∪ Ψ(θ1 ) and θ = mgu(η(E0 )) ◦ η. Then
]
uf (a1 , θ1 , a2 , θ2 ) ∈ γ([up(E0 , down(E0 , Ψ(S1 ) S2 ))] )
≈
]
↔ mgu((Ψ(θ1 ))(Ψ(a1 )), θ2 (a2 )) ◦ θ2 ∈ γ([up(E0 , down(E0 , Ψ(S1 ) S2 ))] )
≈
]
↔ mgu(η(E0 )) ◦ η ∈ γ([up(E0 , down(E0 , Ψ(S1 ) S2 ))] )
≈
]
↔ θ ∈ γ([up(E0 , down(E0 , Ψ(S1 ) S2 ))] )
≈
U
Thus, it remains to prove θ ∈ γ([up(E0 , down(E0 , Ψ(S1 ) S2 ))]≈ ). Since η ∈
U
U
γ(Ψ(S1 ) S2 ) and θ = mgu(η(E0 ))◦η, it holds that θ ∈ γ([down(E0 , Ψ(S1 ) S2 )]≈ )
according to Lemma 6.3. According to Lemma 6.13, we have mgu(θ(E)) ◦ θ ∈
U
γ([up(E0 , down(E0 , Ψ(S1 ) S2 ))]≈ ). Note that mgu(θ(E)) ◦ θ = θ. Thus, θ ∈
U
γ([up(E0 , down(E0 , Ψ(S1 ) S2 ))]≈ ).
Theorem 7.4. For any term t in Term(Σ, Var) and any type R in Type, t ∈ [R]]∆
iff χ(t) ∈ hhRii∆ .
Proof
We first prove necessity. Assume that t ∈ [R]]∆ . We prove that χ(t) ∈ hhRii∆ by
induction on hh(t), h(R)i.
Basis. h(t) = 0 and h(R) = 1. We have that t ∈ Var and that R = 1 by the
definition of [·]]∆ . Thus, χ(t) = ̺ ∈ hhRii∆ .

44

Lunjin Lu

Induction. Either h(t) = 0 and h(R) > 1 or h(t) > 0 and h(R) ≥ 1. Consider first
the case where h(t) = 0 and h(R) > 1. Then t ∈ Var and either (i) R = (R1 or R2 );
or (ii) R = (R1 and R2 ). We only prove the case (i) since the case (ii) is dual
to the case (i). Since t ∈ [R]]∆ , either t ∈ [R1]∆ or t ∈ [R2]∆ . So, we have either
χ(t) ∈ hhR1 ii∆ or χ(t) ∈ hhR2 ii∆ by the induction hypothesis. Thus, χ(t) ∈ hhRii∆ .
Now consider the case h(t) > 0 and h(R) ≥ 1. Then t = f (t1 , · · · , tn ). Either (i)
R = (R1 or R2 ); (ii) R = (R1 and R2 ); (iii) R = 1 or (iv) R = c(R1 , · · · , Rm ). The
proof for that χ(t) ∈ hhRii∆ in cases (i) and (ii) are the same as in the previous
paragraph. The case (iii) is vacuous. Consider the case (iv). Since t ∈ [R]]∆ , by the
definition of [·]]∆ , there is a type rule c(β1 , · · · , βm )_f (τ1 , · · · , τn ) in ∆ such that
ti ∈ [k(τi )]]∆ for all 1 ≤ i ≤ n where k = {β1 7→ R1 , · · · , βm 7→ Rm }. Observe that
h(ti ) < h(t) and h(k(τi )) ≤ h(R). By induction hypothesis, χ(ti ) ∈ hhk(τi )ii∆ . By
the definition of hh·ii∆ , t ∈ hhRii∆ .
We now prove sufficiency. Assume that χ(t) ∈ hhRii∆ . We prove that t ∈ [R]]∆ by
induction on hh(t), h(R)i.
Basis. h(t) = 0 and h(R) = 1. Then t ∈ Var and χ(t) = ̺. We have that R = 1
by the definition of hh·ii∆ . Thus, t ∈ [R]]∆ .
Induction. Either h(t) = 0 and h(R) > 1 or h(t) > 0 and h(R) ≥ 1. Consider first
the case where h(t) = 0 and h(R) > 1. Then t ∈ Var and either (i) R = (R1 or R2 );
or (ii) R = (R1 and R2 ). We only prove the case (i) since the case (ii) is dual to the
case (i). Since χ(t) ∈ hhRii∆ , either χ(t) ∈ hhR1 ii∆ or χ(t) ∈ hhR2 ii∆ . So, we have
either t ∈ [R1]∆ or t ∈ [R2]∆ by the induction hypothesis. Thus, t ∈ [R]]∆ .
Now consider the case h(t) > 0 and h(R) ≥ 1. Then t = f (t1 , · · · , tn ). Either
(i) R = (R1 or R2 ); (ii) R = (R1 and R2 ); (iii) R = 1 or (iv) R = c(R1 , · · · , Rm ).
The proof for that t ∈ [R]]∆ in cases (i) and (ii) are the same as in the previous
paragraph. The case (iii) is vacuous. Consider the case (iv). Since χ(t) ∈ hhRii∆ ,
by the definition of hh·ii∆ , there is a type rule c(β1 , · · · , βm )_f (τ1 , · · · , τn ) in ∆
such that χ(ti ) ∈ hhk(τi )ii∆ for all 1 ≤ i ≤ n where k = {β1 7→ R1 , · · · , βm 7→
Rm }. Observe that h(ti ) < h(t) and h(k(τi )) ≤ h(R). By induction hypothesis,
ti ∈ [k(τi )]]∆ . By the definition of [·]]∆ , χ(t) ∈ [R]]∆ .

Corollary 7.5. For any R1 , R2 ∈ Type, [R1]∆ ⊆ [R2]∆ iff hhR1 ii∆ ⊆ hhR2 ii∆ .
Proof
Both sufficiency and necessity are proved by contradiction. We first consider sufficiency. Assume that hhR1 ii∆ ⊆ hhR2 ii∆ but [R1]∆ 6⊆ [R2]∆ . Then there is a term t
such that t ∈ [R1]∆ and t 6∈ [R2]∆ . By Theorem 7.4, we have that χ(t) ∈ hhR1 ii∆ . By
the assumption, χ(t) ∈ hhR2 ii∆ . By Theorem 7.4, t ∈ [R2]∆ that contradicts with
that t 6∈ [R2]∆ .
We now prove necessity. Assume that [R1]∆ ⊆ [R2]∆ but hhR1 ii∆ 6⊆ hhR2 ii∆ . Then
there is a term t such that t ∈ hhR1 ii∆ and t 6∈ hhR2 ii∆ . By Theorem 7.4, there is
a term t′ such that χ(t′ ) = t and t′ ∈ [R1]∆ . By the assumption, t′ ∈ [R2]∆ . By
Theorem 7.4, t ∈ hhR2 ii∆ that contradicts with that t 6∈ hhR2 ii∆ .

Improving Precision of Type Analysis Using Non-Discriminative Union

45

References
Aiken, A. and Lakshman, T. 1994. Directional type checking of logic programs. In
Proceedings of the First International Static Analysis Symposium, B. Le Charlier, Ed.
Lecture Notes in Computer Science, vol. 864. Springer, 43–60.
Barbuti, R. and Giacobazzi, R. 1992. A bottom-up polymorphic type inference in logic
programming. Science of Computer Programming 19, 3, 133–181.
Barbuti, R., Giacobazzi, R., and Levi, G. 1993. A general framework for semanticsbased bottom-up abstract interpretation of logic programs. ACM Transactions on Programming Languages and Systems 15, 1, 133–181.
Boye, J. and Malúszynski, J. 1996. Two aspects of directional types. In Proceedings of
the Twelfth International Conference on Logic Programming. The MIT Press, 747–761.
Bronsard, F., Lakshman, T. K., and Reddy, U. S. 1992. A framework of directionality
for proving termination of logic programs. In Proceedings of the Joint International
Conference and Symposium on Logic Programming, K. Apt, Ed. The MIT Press, 321–
335.
Bruynooghe, M. 1991. A practical framework for the abstract interpretation of logic
progams. Journal of Logic Programming 10, 2, 91–124.
Charatonik, W. and Podelski, A. 1998. Directional type inference for logic programs.
In Proceedings of the Fifth International Symposium on Static Analysis, G. Levi, Ed.
Lecture Notes in Computer Science, vol. 1503. Springer, 278–294.
Codish, M. and Demoen, B. 1994. Deriving polymorphic type dependencies for logic
programs using multiple incarnations of Prop. In Proceedings of the First International
Static Analysis Symposium, B. Le Charlier, Ed. Lecture Notes in Computer Science,
vol. 864. Springer, 281–297.
Codish, M. and Lagoon, V. 2000. Type dependencies for logic programs using ACIuniﬁcation. Theoretical Computer Science 238, 1–2, 131–159.
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., and Tommasi, M. 2002. Tree automata techniques and applications.
http://www.grappa.univ-lille3.fr/tata.
Cousot, P. and Cousot, R. 1977. Abstract interpretation: a uniﬁed framework for
static analysis of programs by construction or approximation of ﬁxpoints. In Principles
of Programming Languages. The ACM Press, 238–252.
Cousot, P. and Cousot, R. 1992. Abstract interpretation and application to logic
programs. Journal of Logic Programming 13, 1–4, 103–179.
Cousot, P. and Cousot, R. 1995. Formal language, grammar and set-constraint-based
program analysis by abstract interpretation. In Proceedings of the Seventh ACM Conference on Functional Programming Languages and Computer Architecture. The ACM
Press, 170–181.
Dart, P. and Zobel, J. 1992a. Eﬃcient runtime type checking of typed logic programs.
Journal of Logic Programming 14, 1-2, 31–69.
Dart, P. and Zobel, J. 1992b. A regular type language for logic programs. In Types in
Logic Programming, F. Pfenning, Ed. The MIT Press, 157–189.
Eder, E. 1985. Properties of substitutions and uniﬁcations. Journal of Symbolic Computation 1, 1, 31–46.
Fages, F. and Coquery, E. 2001. Typing constraint logic programs. Theory and Practice
of Logic Programming 1, 6, 751–777.
Frühwirth, T., Shapiro, E., Vardi, M., and Yardeni, E. 1991. Logic programs as
types for logic programs. In Proceedings of the Sixth Annual IEEE Symposium on Logic
in Computer Science. The IEEE Computer Society Press, 300–309.

46

Lunjin Lu

Gallagher, J. and de Waal, D. 1994. Fast and precise regular approximations of logic
programs. In Proceedings of the Eleventh International Conference on Logic Programming, M. Bruynooghe, Ed. The MIT Press, 599–613.
Gallagher, J. P., Boulanger, D., and Saglam, H. 1995. Practical model-based
static analysis for deﬁnite logic programs. In Proceedings of the Fifteenth International
Symposium on Logic Programming, J. W. Lloyd, Ed. The MIT Press, 351–368.
Gallagher, J. P. and Puebla, G. 2002. Abstract interpretation over non-deterministic
ﬁnite tree automata for set-based analysis of logic programs. In Proceedings of the
Fourth International Symposium on Practical Aspects of Declarative Languages, S. Krishnamurthi and C. R. Ramakrishnan, Eds. Lecture Notes in Computer Science, vol.
2257. Springer, 243–261.
Gécseg, F. and Steinby, M. 1984. Tree Automata. Akadémiai Kiadó.
Heintze, N. and Jaffar, J. 1990. A ﬁnite presentation theorem for approximating logic
programs. In Principles of Programming Languages. The ACM Press, 197–209.
Heintze, N. and Jaffar, J. 1992. Semantic types for logic programs. In Types in Logic
Programming, F. Pfenning, Ed. The MIT Press, 141–155.
Hermenegildo, M., Warren, R., and Debray, S. 1992. Global ﬂow analysis as a
practical compilation tool. Journal of Logic Programming 13, 1–4, 349–366.
Hermenegildo, M. V., Bueno, F., Puebla, G., and López, P. 1999. Program analysis,
debugging, and optimization using the Ciao system preprocessor. In Proceedings of the
1999 International Conference on Logic Programming. The MIT Press, 52–65.
Hill, P. and Lloyd, J. 1994. The Gödel Programming Language. The MIT Press.
Hill, P. M. and Spoto, F. 2002. Generalising Def and Pos to type analysis. Journal
of Logic and Computation 12, 3, 497–542.
Horiuchi, K. and Kanamori, T. 1988. Polymorphic type inference in Prolog by abstract interpretation. In Proceedings of the Sixth Conference on Logic Programming,
K. Furukawa, H. Tanaka, and T. Fujisaki, Eds. Lecture Notes in Computer Science, vol.
315. Springer, 195–214.
Janssens, G. and Bruynooghe, M. 1992. Deriving descriptions of possible values of
program variables by means of abstract interpretation. Journal of Logic Programming 13, 1–4, 205–258.
Kahrs, S. 1996. Limits of ML-deﬁnability. In Proceedings of the Eighth International Symposium on Programming Languages: Implementation, Logic and Programs, H. Kuchen
and S. D. Swierstra, Eds. Lecture Notes in Computer Science, vol. 1140. Springer, 17–31.
Kanamori, T. and Horiuchi, K. 1985. Type inference in Prolog and its application.
In Proceedings of the Ninth International Joint Conference on Artificial Intelligence,
A. Joshi, Ed. Morgan Kaufmann, 704–707.
Kanamori, T. and Kawamura, T. 1993. Abstract interpretation based on OLDT resolution. Journal of Logic Programming 15, 1 & 2, 1–30.
Lagoon, V. and Stuckey, P. J. 2001. A framework for analysis of typed logic programs. In Proceedings of the Fifth International Symposium on Functional and Logic
Programming, H. Kuchen and K. Ueda, Eds. Lecture Notes in Computer Science, vol.
2024. Springer, 296–310.
Lloyd, J. 1987. Foundations of Logic Programming. Springer-Verlag.
Lu, L. 1995. Type analysis of logic programs in the presence of type deﬁnitions. In Proceedings of the 1995 ACM SIGPLAN Symposium on Partial Evaluation and SemanticsBased Program Manipulation. The ACM Press, 241–252.
Lu, L. 1998. A polymorphic type analysis in logic programs by abstract interpretation.
Journal of Logic Programming 36, 1, 1–54.

Improving Precision of Type Analysis Using Non-Discriminative Union

47

Lu, L. 2003. Path dependent analysis of logic programs. Higher-Order and Symbolic
Computation 16, 341–377.
Lu, L. and Cleary, J. 1998. An emptiness algorithm for regular types with set operators. Technical report, Department of Computer Science, The University of Waikato.
http://xxx.lanl.gov/abs/cs.LO/9811015.
Marriott, K. and Søndergaard, H. 1989. Semantics-based dataﬂow analysis of logic
programs. In Information Processing 89, Proceedings of the Eleventh IFIP World Computer Congress, G. Ritter, Ed. North-Holland, 601–606.
Mishra, P. 1984. Towards a theory of types in Prolog. In Proceedings of the IEEE
International Symposium on Logic Programming. The IEEE Computer Society Press,
289–298.
Mycroft, A. and O’Keefe, R. 1984. A polymorphic type system for Prolog. Artificial
Intelligence 23, 3, 295–307.
Nilsson, U. 1988. Towards a framework for abstract interpretation of logic programs.
In Proceedings of the First International Workshop on Programming Language Implementation and Logic Programming, P. Deransart, B. Lorho, and J. Maluszynski, Eds.
Lecture Notes in Computer Science, vol. 348. Springer, 68–82.
Reddy, U. 1990. Types for logic programs. In Proceedings of the 1990 North American
Conference on Logic Programming. The MIT Press, 836–40.
Rychlikowski, P. and Truderung, T. 2001. Polymorphic directional types for logic
programming. In Proceedings of the Third ACM SIGPLAN International Conference
on Principles and Practice of Declarative Programming. The ACM Press, 61–72.
Saglam, H. and Gallagher, J. 1995. Approximating constraint logic programs using
polymorphic types and regular descriptions. Technical report CSTR-95-017, Department of Computer Science, University of Bristol.
Smaus, J.-G. 2001. Analysis of polymorphically typed logic programs using ACIuniﬁcation. In Proceedings of the Eighth International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Lecture Notes in Artiﬁcial Intelligence, vol.
2250. Springer, 282–298.
Somogyi, Z., Henderson, F., and Conway, T. 1996. The execution algorithm of Mercury: An eﬃcient purely declarative logic programming language. Journal of Logic
Programming 29, 1–3, 19–64.
Van Hentenryck, P., Cortesi, A., and Le Charlier, B. 1995. Type analysis of Prolog
using type graphs. Journal of Logic Programming 22, 3, 179–208.
Warren, D. S. 1992. Memoing for logic programs. Communications of the ACM 35, 3,
93–111.
Yardeni, E., Frühwirth, T., and Shapiro, E. 1991. Polymorphically typed logic programs. In Proceedings of the Eighth International Conference on Logic Programming,
K. Furukawa, Ed. The MIT Press, 379–93.
Yardeni, E. and Shapiro, E. 1991. A type system for logic programs. Journal of Logic
Programming 10, 2, 125–153.
Zobel, J. 1987. Derivation of polymorphic types for Prolog programs. In Proceedings of
the Fourth International Conference on Logic Programming, J. Lassez, Ed. The MIT
Press, 817–838.

