On Dart-Zobel Algorithm for Testing Regular
Type Inclusion

arXiv:cs/9810001v1 [cs.LO] 1 Oct 1998

Lunjin Lu and John G. Cleary
Department of Computer Science
University of Waikato
Hamilton, New Zealand
Phone: +64-838-4627/4378
{lunjin,jcleary}@cs.waikato.ac.nz
Abstract. This paper answers open questions about the correctness
and the completeness of Dart-Zobel algorithm for testing the inclusion
relation between two regular types. We show that the algorithm is incorrect for regular types. We also prove that the algorithm is complete
for regular types as well as correct for tuple distributive regular types.
Also presented is a simplified version of Dart-Zobel algorithm for tuple
distributive regular types.
Keywords: type, regular term language, regular term grammar, tuple
distributivity

1

Introduction

Types are ubiquitous in programming languages [4]. They make programs easier to understand and help detect errors since a large number of errors are type errors. Types have been introduced into logic
programming in the forms of type checking and inference [3, 7, 11,
23, 28] or type analysis [22, 29, 15, 17, 12, 20, 5, 21] or typed languages [14, 19, 25, 27]. Recent logic programming systems allow the
programmer declare types for predicates and type errors are then
detected either at compile time or at run time. Even in early logic
programming systems, built-in predicates are usually typed and type
checking for these predicates are performed at run time. The reader
is referred to [24] for more details on type in logic programming.
A type is a possibly infinite set of ground terms with a finite
representation. An integral part of any type system is its type language that specifies which sets of ground terms are types. To be
useful, types should be closed under intersection, union and complement operations. The decision problems such as the emptiness
of a type, inclusion of a type in another, equivalence of two types
should be decidable. Regular term languages [13, 6], called regular

types, satisfy these constraints and has been used widely used as
types [26, 22, 29, 7, 15, 19, 25, 27, 11, 28, 17, 12, 20, 5, 21].
Most type systems use tuple distributive regular types which are
strictly less powerful than regular types [26, 22, 29, 15, 19, 25, 27,
11, 28, 17, 12, 20, 5, 21]. Tuple distributive regular types are regular
types closed under tuple distributive closure. Intuitively, the tuple
distributive closure of a set of terms is the set of all terms constructed
recursively by permuting each argument position among all terms
that have the same function symbol [28]. Tuple distributive regular
types are discussed in section 5.
To our knowledge, Dart and Zobel’s work [8] is the only one to
present, among others, an inclusion algorithm for regular types with
respect to a given set of type definitions without the tuple distributive restriction. Set-based analysis can also be used to deriving types
based on set constraint solving [2, 1, 18, 16, 10]. However, set constraint solving methods are intended to infer descriptive types [25]
rather than for testing inclusion of a prescriptive type [25] in another.
Therefore, they are useful in different settings from Dart-Zobel algorithm. Dart-Zobel algorithm has been used in type or type related
analyses [7, 9]. However, the completeness and the correctness of the
algorithm are left open. This paper provides answers to these open
questions. We show that the algorithm is incorrect for regular types.
We also prove that the algorithm is complete for regular types in
general as well as correct for tuple distributive regular types. These
results lead to a simplified version of Dart-Zobel algorithm that is
complete and correct for tuple distributive regular types.
The remainder of this paper is organised as follows. Section 2 defines regular types by regular term grammars. Section 3 recalls DartZobel algorithm for testing if a regular type is a subset of another
regular type. Section 4 addresses the completeness and the correctness of their algorithm that have been left open. In section 5, we
show that their algorithm is both complete and correct for tuple
distributive regular types and provides a simplified version of their
algorithm for tuple distributive regular types.

2

Regular types

Several equivalent formalisms such as tree automata [13, 6], regular
term grammars [13, 6], regular unary logic programs [28] have been
used to describe regular types. In [8], Dart and Zobel use regular
term grammars to describe regular types that are sets of ground
terms over a ranked alphabet Σ.
A regular term grammar is a tuple G = hΠ, Σ, ∆i where1
– Σ is a fixed ranked alphabet. Each symbol in Σ is called a function symbol and has a fixed arity. It is assumed that Σ contains
at least one constant that is a function symbol of arity 0.
– Π is a set of symbols called nonterminals. These terminals will
be called type symbols as they represent types. Type symbols are
of arity 0. It is assumed that Π ∩ Σ = ∅.
– ∆ is a set of production rules of the form α → τ with α ∈ Π and
τ ∈ T (Σ ∪ Π) where T (Σ ∪ Π) is the set of all terms over Σ ∪ Π.
Terms in T (Σ ∪ Π) will be called pure type terms.
Example 1. Let Σ = {0, s(), nil, cons(, )} and Π = {Nat, NatList}.
G = hΠ, Σ, ∆i defines natural numbers and lists of natural numbers
where


Nat → 0,






 Nat → s(Nat),

∆=


Natlist → nil,






Natlist → cons(Nat, Natlist)
✷
The above presentation is slightly different from [8] where production rules with the same type symbol on their lefthand sides
are grouped together and called a type rule. For instance, production rules in the above examples are grouped into two type rules
Nat → {Nat, Natlist} and Natlist → {nil, cons(Nat, Natlist)}.
Types denoted by a pure type term is given by a rewrite rule ⇒G
associated with G. t ⇒G s if ∆ contains a rule α → τ , α occurs in
t and s results from replacing an occurrence of α in t by τ . Let ⇒∗G
1

A start symbol is not needed in our setting.

be the reflexive and transitive closure of ⇒G . The type denoted by
a pure type term τ is defined as follows.
def

[τ ]G = {t ∈ T (Σ) | τ ⇒∗G t}
[τ ]G is the set of terms over Σ that can be derived from τ by repeatedly replacing the lefthand side of a rule in ∆ with its righthand
side.
Example 2. Let G be the regular term grammar in example 1. We
have
Natlist ⇒G cons(Nat, Natlist)
⇒G cons(s(Nat), Natlist)
⇒G cons(s(0), Natlist)
⇒G cons(s(0), nil)
Thus, [Natlist]]G contains cons(s(0), nil).
The type represented by a sequence ψ of pure type terms and a
set Ψ of sequences of pure type terms are defined as follows.
def

[ǫ]]G = {ǫ}
def

[hτ i + ψ ′]G = [τ ]G × [ψ ′]G
def [
[Ψ ] G =
[ψ]]G
ψ∈Ψ

where ǫ is the empty sequence, + is the infix sequence concatenation
operator, hτ i is the sequence consisting of the pure type term τ and
× is the Cartesian product operator.
The set Π of nonterminals in Dart and Zobel’s type language also
contains constant type symbols. Constant type symbols are not defined by production rules and they denote constant types. In particular, Π contains µ denoting the set of all terms over Σ and φ denoting
the empty set of terms. We will leave out constant type symbols in
this paper in order to simplify presentation. Re-introducing constant
type symbols will not affect the results of the paper.
Dart-Zobel algorithm works with simplified regular term grammars. A regular term grammar G = hΠ, Σ, ∆i is simplified if [α]]G 6= ∅
for each α ∈ Π and τ 6∈ Π for each (α → τ ) ∈ ∆. Every regular
grammar can be simplified.

3

Dart-Zobel Inclusion Algorithm

This section recalls Dart and Zobel’s inclusion algorithm for regular types. As indicated in section 2, we shall disregard constant
type symbols and simplify their algorithm accordingly. We note that
without constant type symbols, many functions in their algorithm
can be greatly simplified. In place of a type rule, we use the corresponding set of production rules. These superficial changes don’t
change the essence of the algorithm but facilitate the presentation.
We shall assume that G is a simplified regular term grammar and
omit references to G where there is no confusion.
We first describe the ancillary functions used in their algorithm.
Let ψ = τ1 τ2 · · · τn be a non-empty sequence of pure type terms and
def
Ψ be a set of non-empty sequences of pure type terms. head (ψ) = τ1
def
def
and tail (ψ) = τ2 · · · τn . heads and tails are defined as heads(Ψ ) =
def
{head (ψ) | ψ ∈ Ψ } and tails(Ψ ) = {tail (ψ) | ψ ∈ Ψ }. The function
expand rewrites a non-empty sequence into a set of sequences when
necessary.
(

def

expand (ψ) =

def

{ψ}
if head(ψ) 6∈ Π
{hτ i + tail (ψ) | (head (ψ) → τ ) ∈ ∆} if head(ψ) ∈ Π

expands(Ψ ) = ψ∈Ψ expand(ψ).
The function selects(τ, Ψ ) defined below applies when τ is pure
type term and τ 6∈ Π and Ψ is a set of non-empty sequences with
heads(Ψ ) ∩ Π = ∅. The output of selects(τ, Ψ ) is the set of the
sequences in Ψ that have the same principal function symbol as τ .
S

def

selects(f (τ1 , · · · , τn ), Ψ ) = {ψ ∈ Ψ | head (ψ) = f (ω1 , · · · , ωn )}
Note that f (τ1 , · · · , τn ) is a constant when n = 0.
The function open(ψ ′ ) defined below applies when ψ ′ is a nonempty sequence with head (ψ ′ ) 6∈ Π. open(ψ ′ ) replaces the head of
ψ ′ with its arguments.
def

open(f (τ1 , · · · , τn ) + ψ) = τ1 τ2 · · · τn + ψ
When n = 0, open(f (τ1 , · · · , τn ) + ψ) = ψ. Without constant type
symbols, open doesn’t need an extra argument as in [8] that is used
to test membership of a term in a constant type and to indicate the

required number of arguments when the constant type symbol is µ.
def
opens(Ψ ) = {open(ψ) | ψ ∈ Ψ }.
The inclusion algorithm subset(τ1 , τ2 ) takes two pure type terms
τ1 and τ2 and is intended to decide if [τ1]G ⊆ [τ2]G is true or false.
The core part subsetv of the inclusion algorithm takes a sequence ψ
of pure type terms and a set Ψ of sequences of pure type terms that
are of the same length as ψ and is intended to decide if [ψ]]G ⊆ [Ψ ]G .
subsetv takes a third argument C to ensure termination. C is a set
of pairs hβ, Υ i where β ∈ Π is a type symbol and Υ ⊆ T (Σ ∪ Π) is a
set of pure type terms. A pair hβ, Υ i in C can be read as [β]]G ⊆ [Υ ]G .
The functions subset and subsetv are defined in the following.
Where several alternative definitions of subsetv apply, the first is
used.
def

subset(τ1 , τ2 ) = subsetv (hτ1 i, {hτ2 i}, ∅)
def

subsetv (ψ, Ψ, C) =


false
if Ψ = ∅




true
if ψ = ǫ






 subsetv (tail (ψ), tails(Ψ ), C)


if hhead (ψ), Υ i ∈ C and heads(Ψ ) ⊇ Υ
′

∀ψ ∈ expand(ψ).subsetv (ψ ′ , Ψ, C ∪ {hhead (ψ, heads(Ψ )i})





if head(ψ) ∈ Π





 subsetv (open(ψ), opens(selects(head (ψ), expands(Ψ ))), C)


if head(ψ) = f (τ1 , · · · , τn )

The second condition heads(Ψ ) ⊇ Υ for the third alternative is
obviously mistaken to be heads(Ψ ) ⊆ Υ in [8]. The first two alternatives deal with two trivial cases. The third alternative uses pairs
in C to force termination. As we shall see later, this is fine for tuple distributive regular types but is problematic for regular types in
general. The fourth alternative expands ψ into a set of sequences
ψ ′ and compares each of them with Ψ . The fifth alternative applies
when ψ = f (τ1 , · · · , τn ) + ψ ′ . Sequences in Ψ are expanded and the
expanded sequences of the form f (σ1 , · · · , σn ) + ω ′ are selected. ψ
and the set of the selected sequences are then compared after replacing f (τ1 , · · · , τn ) with τ1 · · · τn in ψ and replacing f (σ1 , · · · , σn )
with σ1 · · · σn in each f (σ1 , · · · , σn ) + ω ′.

4

Correctness and Completeness

We now address the correctness and the completeness of Dart-Zobel
algorithm that were left open. We first show that the algorithm is
incorrect for regular types by means of a counterexample. We then
prove that the algorithm is complete for regular types. Thus, the
algorithm provides an approximate solution to the inclusion problem
of regular types in that it returns true if inclusion relation holds
between its two arguments while the reverse is not necessarily true.
4.1

Correctness - a counterexample

The following example shows that Dart-Zobel algorithm is incorrect
for regular types.
Example 3. Let G = hΠ, Σ, ∆i with Π = {α, β, θ, σ, ω},
Σ = {a, b, g(), h(, )} and


α





β




→ g(ω)





→ g(θ) | g(σ)

∆ = θ → a | h(θ, a)






σ → b | h(σ, b)





 ω → a | b | h(ω, a) | h(ω, b) 


where, for instance, θ → a | h(θ, a) is an abbreviation of two rules
θ → a and θ → h(θ, a). Let Σh = Σ \ {h}. We have
[θ]]G = {t ∈ T (Σh ) | t is left-skewed and leaves of t are a’s}
[σ]]G = {t ∈ T (Σh ) | t is left-skewed and leaves of t are b’s}
[ω]]G = {t ∈ T (Σh ) | t is left-skewed}
[α]]G = {g(t) | t ∈ [ω]]G }
[β]]G = {g(t) | t ∈ [θ]]G ∪ [σ]]G }
Let t = g(h(h(a, b), a)). t ∈ [α]]G and t 6∈ [β]]G . Therefore, [α]]G 6⊆
[β]]G . The incorrectness of Dart-Zobel algorithm is illustrated by
showing subset(α, β) = true as follows. Let C0 = {hα, {β}i}. We
have
subset(α, β) = subsetv (hαi, {hβi}, ∅)
by def. of subset
= subsetv (hg(ω)i, {hβi}, C0 ) by 4th def. of subsetv
= subsetv (hωi, {hθi, hσi}, C0) by 5th def. of subsetv

Let C1 = C0 ∪ {hω, {θ, σ}i}. By the fourth definition of subsetv
and the above equation,
subsetv (hai, {hθi, hσi}, C1 )
∧
subsetv (hbi, {hθi, hσi}, C1 ) 



subset(α, β) = 
 ∧ subsetv (hh(ω, a)i, {hθi, hσi}, C1 ) 
∧ subsetv (hh(ω, b)i, {hθi, hσi}, C1 )




(1)

By applying the fifth and then the second definitions of subsetv ,
subsetv (hai, {hθi, hσi}, C1 ) = subsetv (ǫ, {ǫ}, C1 ) = true. In the same
way, we obtain subsetv (hai, {hθi, hσi}, C1 ) = true.
subsetv (hh(ω, a)i, {hθi, hσi}, C1)
= subsetv (hω, ai, {hθ, ai, hσ, bi}, C1) by 5th
= subsetv (hai, {hai, hbi}, C1 )
by 3rd
= subsetv (ǫ, {ǫ}, C1 )
by 5th
= true
by 2nd

def.
def.
def.
def.

of
of
of
of

subsetv
subsetv
subsetv
subsetv

We can show subsetv (hh(ω, a)i, {hθi, hσi}, C1 ) = true in the same
way as above. Therefore, by equation 1, subset(α, β) = true and
subset is incorrect for regular types.
✷
The problem with the algorithm stems from the way the set C is
used in the third definition of subsetv . As the above example indicates, the third definition of subsetv severs the dependency between
the terms in a tuple, i.e., subterms of a term.
In [8], Dart and Zobel show by an example that their algorithm
works for some regular types which are not tuple distributive. We
don’t know what is the largest subclass of the class of regular types
for which the algorithm is correct.
4.2

Completeness

We now prove that Dart-Zobel algorithm is complete for regular
types in the sense that subset(τ1 , τ2 ) = true whenever [τ1]G ⊆ [τ2]G .
Let C be a set of pairs hβ, Υ i with β ∈ Π and Υ ⊆ T (Σ ∪ Π). A
pair hβ, Υ i in C states that the denotation of β is included in that
of Υ , i.e., [β]]G ⊆ [Υ ]G for regular types. Define
def

ΓC,G = ∧hβ,Υ i∈C [β]]G ⊆ [Υ ]G

The completeness of subset follows from the following theorem
which asserts the completeness of subsetv .
Theorem 1. Let ψ be a sequence of pure type terms and Ψ a set of
sequences of pure type terms of the same length as ψ, C a set of pairs
hβ, Υ i with β ∈ Π and Υ ⊆ T (Σ ∪ Π). If ΓC,G |= [ψ]]G ⊆ [Ψ ]G then
subsetv (ψ, Ψ, C) = true.
Proof. Assume subsetv (ψ, Ψ, C) = false. The proof is done by showing ΓC,G 6|= [ψ]]G ⊆ [Ψ ]G . This is accomplished by induction on
hdp(ψ, Ψ, C), lg(ψ)i where lg(ψ) is the length of ψ and dp(ψ, Ψ, C)
is the depth of the computation tree for subsetv (ψ, Ψ, C). Define
def
hk, li < hk ′ , l′ i = (k < k ′ ) ∨ (k = k ′ ) ∧ (l < l′ ).
Basis. dp(ψ, Ψ, C) = 0 and lg(ψ) = 0. ψ = ǫ and Ψ = ∅ since
subsetv (ψ, Ψ, C) = false. Let t = ǫ. t ∈ [ψ]]G and t 6∈ [Ψ ]G . So,
ΓC,G 6|= [ψ]]G ⊆ [Ψ ]G .
Induction. dp(ψ, Ψ, C) 6= 0 or lg(ψ) 6= 0. By the definition of
subsetv ,
(a) Ψ = ∅; or
(b) subsetv (tail (ψ), tails(Ψ ), C) = false and there is Υ ⊆ T (Σ ∪ Π)
such that (hhead(ψ), Υ i ∈ C) ∧ (heads(Ψ ) ⊇ Υ ); or
(c) head (ψ) ∈ Π and ∃.ψ ′ ∈ expand(ψ).subsetv (ψ ′ , Ψ, C ′ ) = false
where C ′ = C ∪ {hhead (ψ), heads(Ψ )i}; or
(d) head (ψ) = f (τ1 , · · · , τn ) and subsetv (ψ ′ , Ψ ′, C) = false where
ψ ′ = open(ψ) and Ψ ′ = opens(selects(head(ψ), expands(Ψ ))).
It remains to prove that ΓC,G 6|= [ψ]]G ⊆ [Ψ ]G in each of the cases
(a)-(d). The case (a) is trivial as G is simplified and hence [ψ]]G 6= ∅.
In the case (b), we have dp(tail (ψ), tails(Ψ ), C) ≤ dp(ψ, Ψ, C) and
lg(tail (ψ)) < lg(ψ). By the induction hypothesis, ΓC,G 6|= [tail (ψ)]]G ⊆
[tails(Ψ )]]G . Thus, ΓC,G |= ∃t′ .(t′ ∈ [tail (ψ)]]G ∧ t′ 6∈ [tails(Ψ )]]G ). Let
t ∈ [head (ψ)]]G and t = hti + t′ . Note that t exists as G is simplified.
We have ΓC,G |= t ∈ [ψ]]G ∧ t 6∈ [Ψ ]G . So, ΓC,G 6|= [ψ]]G ⊆ [Ψ ]G .
In the case (c), dp(ψ ′ , Ψ, C ′) < dp(ψ, Ψ, C). By the induction hypothesis, ΓC ′ G 6|= [ψ ′]G ⊆ [Ψ ]G . Note that ΓC ′ ,G = ΓC,G ∧([[head (ψ)]]G ⊆
[heads(Ψ )]]G ). So, we have ΓC,G |= [ψ]]G 6⊆ [Ψ ]G ∨[[head (ψ)]]G 6⊆ [heads(Ψ )]]G .
Assume ΓC,G = true. Either (i) [ψ]]G 6⊆ [Ψ ]G or (ii) [head (ψ)]]G 6⊆
[heads(Ψ )]]G . In the case (i), ∃.t′ .(t′ ∈ [ψ ′]G ) ∧ (t′ 6∈ [Ψ ]G ). By proposition 5.26 in [8], we have ΓC,G 6|= [ψ]]G ⊆ [Ψ ]G . In the case (ii), ∃t.(t ∈

[head(ψ)]]G ) ∧ (t 6∈ [heads(Ψ )]]G ). Let t′ ∈ [tail (ψ)]]G and t = hti + t′ .
Note that t′ exists as G is simplified. We have t ∈ [ψ]]G ∧ t 6∈ [Ψ ]G .
So, ΓC,G 6|= [ψ]]G ⊆ [Ψ ]G in the case (c).
In the case (d), we have ψ ′ = τ1 · · · τn +tail (ψ) and dp(ψ ′ , Ψ ′ , C) <
dp(ψ, Ψ, C). By the induction hypothesis, ΓC,G 6|= [ψ ′]G ⊆ [Ψ ′]G .
Thus, ΓC,G |= ∃t1 .∃t2 .(lg(t1 ) = n) ∧ ((t1 + t2 ) ∈ [ψ ′]G ) ∧ ((t1 +
t2 ) 6∈ [Ψ ′]G ), which implies ΓC,G |= ∃t1 .∃t2 .(hf (t1 )i + t2 ) ∈ [ψ]]G ) ∧
((hf (t1 )i + t2 ) 6∈ [Ψ ]G ). So, ΓC,G 6|= [ψ]]G ⊆ [Ψ ]G .
✷
The completeness of subset is a corollary of the above theorem.
Corollary 2. Let τ1 and τ2 be pure type terms. If [τ1]G ⊆ [τ2]G then
subset(τ1 , τ2 ) = true.
Proof. subset(τ1 , τ2 ) = subsetv (hτ1 i, {hτ2 i}, ∅) by the definition of
subset. We have Γ∅,G |= [hτ1 i]]G ⊆ [{hτ2 i}]]G since [τ1]G ⊆ [τ2]G . The
corollary now follows from the above theorem as Γ∅,G = true.
✷
5

Tuple Distributive Regular Types

Most type languages in logic programming use tuple distributive
closures of regular term languages as types [26, 22, 29, 15, 19, 25,
27, 11, 28, 17, 12, 20, 5, 21]. The notion of tuple distributivity is
due to Mishra [22]. The following definition of tuple distributivity is
due to Heintze and Jaffar [15]. Each function symbol of arity n is
−1
−1
−1
associated with n projection operators f(1)
, f(2)
, · · · , f(n)
. Let S be a
−1
set of ground terms in T (Σ). f(i) is defined as follows.
def

−1
f(i)
(S) = {ti | f (t1 , · · · , ti , · · · , tn ) ∈ S}

The tuple distributive closure of S is
def

⋆

−1
S ⋆ = {c | c ∈ S ∧ c ∈ Σ0 } ∪ {f (t1 , · · · , tn ) | ti ∈ (f(i)
(S)) }

where Σ0 is the set of constants in Σ.
The following proposition results from the fact that (.)⋆ is a
closure operator and preserves set inclusion, i.e., S1 ⊆ S2 implies
S1⋆ ⊆ S2⋆ .

Proposition 3. Let S1 , S2 ⊆ T (Σ). (S1 ∪ S2 )⋆ = (S1⋆ ∪ S2⋆ )⋆ .
✷
The tuple distributive regular type h τ i G associated with a pure
type term τ is the tuple distributive closure of the regular type [τ ]G
associated with τ [22].
def
h τ i G = [τ ]⋆G
Let ψ be a sequence of pure type terms, Ψ be a set of sequences
of pure type terms of the same length.
def

h ǫiiG = {ǫ}
def

h ψiiG = {hti + t | t ∈ h head(ψ)iiG ∧ t ∈ h tail (ψ)iiG }
def

h Ψ iG = (

[

⋆

h head (ψ)iiG ) × h tails(Ψ )iiG

ψ∈Ψ

The definition of h Ψ i G makes use of tuple distributivity and hence
severs the inter-dependency between components of a sequences of
terms.
5.1

Correctness

We now prove that Dart-Zobel algorithm is correct for tuple distributive regular types in the sense that if subset(τ1 , τ2 ) = true then
h τ1 i G ⊆ h τ2 i G . Let C be a set of pairs hβ, Υ i with β ∈ Π and
Υ ⊆ T (Σ ∪ Π). A pair hβ, Υ i in C represents h βiiG ⊆ h Υ i G for tuple
distributive regular types. Define
def

ΦC,G = ∧hβ,Υ i∈C h βiiG ⊆ h Υ i G
The correctness of subset follows from the following theorem which
asserts the correctness of subsetv for tuple distributive regular types.
Theorem 4. Let ψ be a sequence of pure type terms and Ψ a set of
sequences of pure type terms of the same length as ψ, C a set of pairs
hβ, Υ i with β ∈ Π and Υ ⊆ T (Σ ∪ Π). If subsetv (ψ, Ψ, C) = true
then ΦC,G |= h ψiiG ⊆ h Ψ i G .
Proof. Assume subsetv (ψ, Ψ, C) = true. The proof is done by induction on hdp(ψ, Ψ, C), lg(ψ)i.

Basis. dp(ψ, Ψ, C) = 0 and lg(ψ) = 0. ψ = ǫ and Ψ 6= ∅ by the
second definition of subsetv . So, Ψ = {ǫ} and ΦC,G |= h ψiiG ⊆ h Ψ i G .
Induction. dp(ψ, Ψ, C) 6= 0 or lg(ψ) 6= 0 By the definition of
subsetv ,
(a) subsetv (tail (ψ), tails(Ψ ), C) = true and there is Υ ⊆ T (Σ ∪ Π)
such that (hhead (ψ), Υ i ∈ C) ∧ (heads(Ψ ) ⊇ Υ ); or
(b) head (ψ) ∈ Π and ∀.ψ ′ ∈ expand (ψ).subsetv (ψ ′ , Ψ, C ′ ) = true
where C ′ = C ∪ {hhead (ψ), heads(Ψ )i}; or
(c) head (ψ) = f (τ1 , · · · , τn ) and subsetv (ψ ′ , Ψ ′ , C) = true where ψ ′ =
open(ψ) and Ψ ′ = opens(selects(head(ψ), expands(Ψ ))).
It remains to prove that ΦC,G |= h ψiiG ⊆ h Ψ i G in each of the cases
(a)-(c).
In the case (a), we have dp(tail (ψ), tails(Ψ ), C) ≤ dp(ψ, Ψ, C) and
lg(tail (ψ)) < lg(ψ). By the induction hypothesis, ΦC,G |= h tail (ψ)iiG ⊆
h tails(Ψ )iiG . (hhead (ψ), Υ i ∈ C) and (heads(Ψ ) ⊇ Υ ) imply ΦC,G |=
h head (ψ)iiG ⊆ h heads(Ψ )iiG . Thus, ΦC,G |= h ψiiG ⊆ h Ψ i G by the definitions of h ψiiG and h Ψ i G . Note that tuple distributivity is used in
the definition of h Ψ i G .
In the case (b), dp(ψ ′ , Ψ, C ′) < dp(ψ, Ψ, C). By the induction
hypothesis, ΦC ′ ,G |= h ψ ′ i G ⊆ h Ψ i G . Note that ΦC ′ ,G = ΦC,G ∧
(hhhead (ψ)iiG ⊆ h heads(Ψ )iiG ). So,
ΦC,G |= h ψ ′ i G ⊆ h Ψ i G ∨ h head (ψ)iiG 6⊆ h heads(Ψ )iiG
subsetv (head (ψ), heads(Ψ ), C) = true since subsetv (ψ, Ψ, C) = true.
We have ΦC,G |= h head (ψ)iiG ⊆ h heads(Ψ )iiG by the induction hypothesis since dp(head(ψ), heads(Ψ ), C) < dp(ψ, Ψ, C). So, ΦC,G |=
h ψ ′ i G ⊆ h Ψ i G . ΦC,G |= (hh{ψ ′ | ψ ′ ∈ expand(ψ)}iiG ⊆ h Ψ i G ) since (.)⋆
is a closure operator and hence ΦC,G |= h ψiiG ⊆ h Ψ i G
In the case (c), we have ψ ′ = τ1 · · · τn +tail (ψ) and dp(ψ ′ , Ψ ′ , C) <
dp(ψ, Ψ, C). By the induction hypothesis, ΦC,G |= h ψ ′ i G ⊆ h Ψ ′ i G .
By proposition 5.29 in [8], ΦC,G |= h ψiiG ⊆ h Ψ i G . This completes the
proof of the theorem.
✷
The correctness of subset is a corollary of the above theorem.
Corollary 5. Let τ1 and τ2 be pure type terms. If subset(τ1 , τ2 ) =
true then h τ1 i G ⊆ h τ2 i G .

Proof. Let subset(τ1 , τ2 ) = true. subsetv (hτ1 i, {hτ2 i}, ∅) = true by
the definition of subset. Thus, Φ∅,G |= h hτ1 iiiG ⊆ h {hτ2 i}iiG according
to the above theorem. So, h τ1 i G ⊆ h τ2 i G as Φ∅,G = true.
✷
5.2

Completeness

This section presents the completeness of Dart-Zobel algorithm for
tuple distributive regular types. The following theorem is the counterpart of theorem 1.
Theorem 6. Let ψ be a sequence of pure type terms and Ψ a set of
sequences of pure type terms of the same length as ψ, C a set of pairs
hβ, Υ i with β ∈ Π and Υ ⊆ T (Σ ∪ Π). If ΦC,G |= h ψiiG ⊆ h Ψ i G then
subsetv (ψ, Ψ, C) = true.
Proof. The proof can be obtained from that for theorem 1 by simply
replacing Γ·,· with Φ·,· and [·]]G with h ·iiG .
✷
The following completeness result of Dart-Zobel algorithm for tuple distributive regular types follows from the above theorem.
Corollary 7. Let τ1 and τ2 be pure type terms. If h τ1 i G ⊆ h τ2 i G then
subset(τ1 , τ2 ) = true.
Proof. The proof can be obtained from that for corollary 2 by simply replacing Γ(·,·) with Φ(·,·) , [·]]G with h ·iiG and theorem 1 with theorem 6.
✷
5.3

A Simplified Algorithm

Now that Dart-Zobel algorithm is complete and correct for tuple
distributive regular types but not correct for general regular types.
It is desirable to specialise Dart-Zobel algorithm for tuple distributive regular types which was originally proposed for general regular
types. The following is a simplified version of the algorithm for tuple
distributive regular types.

def

subset ′ (τ1 , τ2 ) = subset ′ (τ1 , {τ2 }, ∅)
def

subset ′ (τ, Υ, C) =

false






 true

if Υ = ∅

if (hτ, Υ ′i ∈ C) ∧ (Υ ⊇ Υ ′)

∀τ ′ ∈ expand ′ (τ ).subset ′ (τ ′ , Υ, C ∪ {hτ, Υ i})
if τ ∈ Π



′
′


subsetv (τ1 · · · τn , {σ1 · · · σn | f (σ1 , · · · , σn ) ∈ expands (Υ )}, C)



if τ = f (τ1 , · · · , τn )



def

subsetv ′ (ǫ, {ǫ}, C) = true
def

subsetv ′ (ψ, Ψ, C) =
subset ′ (head(ψ), heads(Ψ ), C) ∧ subsetv ′ (tail (ψ), tails(Ψ ), C)
(
{τ }
if τ 6∈ Π
def
′
expand (τ ) =
{σ | τ → σ) ∈ ∆} if τ ∈ Π
def

expands ′ (Υ ) =

[

expand ′ (τ )

τ ∈Υ

While Dart-Zobel algorithm mainly deals with sequences of pure
type terms, the simplified algorithm primarily deals with pure type
terms by breaking a sequence of pure type terms into its component
pure type terms. This is allowed because tuple distributive regular
types abstract away inter-dependency between component terms in
a sequence of ground terms. We forgo presenting the correctness and
the completeness of the simplified algorithm because they can be
proved by emulating proofs for theorems 1 and 4.
6

Conclusion

We have provided answers to open questions about the correctness
and the completeness of Dart-Zobel algorithm for testing inclusion
of one regular type in another. The algorithm is complete but incorrect for general regular types. It is both complete and correct for
tuple distributive regular types. It is our hope that the results presented in this paper will help identify the applicability of Dart-Zobel
algorithm. We have also provided a simplified version of Dart-Zobel
algorithm for tuple distributive regular types.

References
[1] A. Aiken and T.K. Lakshman. Directional type checking of logic programs. In
B. Le Charlier, editor, Proceedings of the First International Static Analysis Symposium, pages 43–60. Springer-Verlag, 1994.
[2] A. Aiken and E. Wimmers. Solving systems of set constraints. In Proceedings of
the Seventh IEEE Symposium on Logic in Computer Science, pages 329–340. The
IEEE Computer Society Press, 1992.
[3] C. Beierle. Type inferencing for polymorphic order-sorted logic programs. In
L. Sterling, editor, Proceedings of the Twelfth International Conference on Logic
Programming, pages 765–779. The MIT Press, 1995.
[4] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. ACM computing surveys, 17(4):471–522, 1985.
[5] M. Codish and V. Lagoon. Type dependencies for logic programs using aciunification. In Proceedings of the 1996 Israeli Symposium on Theory of Computing
and Systems, pages 136–145. IEEE Press, June 1996.
[6] H. Comon, M. Dauchet, R. Gilleron, D. Lugiez, S. Tison, and M. Tommasi. Tree
Automata Techniques and Applications. Draft, 1998.
[7] P.W. Dart and J. Zobel. Efficient run-time type checking of typed logic programs.
Journal of Logic Programming, 14(1-2):31–69, 1992.
[8] P.W. Dart and J. Zobel. A regular type language for logic programs. In Frank
Pfenning, editor, Types in Logic Programming, pages 157–189. The MIT Press,
1992.
[9] S. K. Debray, P. López-Garcia, and M. Hermenegildo. Non-failure analysis for
logic programs. In Lee Naish, editor, Logic programming: Proceedings of the fourteenth International Conference on Logic Programming, pages 48–62. The MIT
Press, July 1997.
[10] P. Devienne, J-M. Talbot, and S. Tison. Co-definite set constraints with membership expressions. In J. Jaffar, editor, Proceedings of the 1998 Joint Conference
and Symposium on Logic Programming, pages 25–39. The MIT Press, 1998.
[11] T. Fruhwirth, E. Shapiro, M.Y. Vardi, and E. Yardeni. Logic programs as types
for logic programs. In Proceedings of Sixth Annual IEEE Symposium on Logic in
Computer Science, pages 300–309. The IEEE Computer Society Press, 1991.
[12] J.P. Gallagher and D.A. de Waal. Fast and precise regular approximations of logic
programs. In M. Bruynooghe, editor, Proceedings of the Eleventh International
Conference on Logic Programming, pages 599–613. The MIT Press, 1994.
[13] F. Gécseg and M. Steinby. Tree Automata. Akadémiai Kiadó, 1984.
[14] M. Hanus. Horn clause programs with polymorphic types: semantics and resolution. Theoretical Computer Science, 89(1):63–106, 1991.
[15] N. Heintze and J. Jaffar. A finite presentation theorem for approximating logic
programs. In Proceedings of the seventh Annual ACM Symposium on Principles
of Programming Languages, pages 197–209. The ACM Press, 1990.
[16] N. Heintze and J. Jaffar. A decision procedure for a class of set constraints. Technical Report CMU-CS-91-110, Carnegie-Mellon University, February 1991. (Later
version of a paper in Proc. 5th IEEE Symposium on LICS).
[17] N. Heintze and J. Jaffar. Semantic types for logic programs. In Frank Pfenning,
editor, Types in Logic Programming, pages 141–155. The MIT Press, 1992.
[18] N. Heintze and J. Jaffar. Set constraints and set-based analysis. In Alan Borning,
editor, Principles and Practice of Constraint Programming, volume 874 of Lecture

Notes in Computer Science. Springer, May 1994. (PPCP’94: Second International
Workshop, Orcas Island, Seattle, USA).
[19] D. Jacobs. Type declarations as subtype constraints in logic programming. SIGPLAN Notices, 25(6):165–73, 1990.
[20] L. Lu. Type analysis of logic programs in the presence of type definitions. In
Proceedings of the 1995 ACM SIGPLAN Symposium on Partial Evaluation and
Semantics-Based program manipulation, pages 241–252. The ACM Press, 1995.
[21] L. Lu. A polymorphic type analysis in logic programs by abstract interpretation.
Journal of Logic Programming, 36(1):1–54, 1998.
[22] P. Mishra. Towards a theory of types in Prolog. In Proceedings of the IEEE international Symposium on Logic Programming, pages 289–298. The IEEE Computer
Society Press, 1984.
[23] A. Mycroft and R.A. O’Keefe. A polymorphic type system for Prolog. Artificial
Intelligence, 23:295–307, 1984.
[24] Frank Pfenning, editor. Types in logic programming. The MIT Press, Cambridge,
Massachusetts, 1992.
[25] U.S. Reddy. Types for logic programs. In S. Debray and M. Hermenegildo, editors, Logic Programming. Proceedings of the 1990 North American Conference,
pages 836–40. mit, 1990.
[26] M. Soloman. Type definitions with parameters. In Conference Record of the Fifth
ACM Symposium on Principles of Programming Languages, pages 31–38, 1978.
[27] E. Yardeni, T. Fruehwirth, and E. Shapiro. Polymorphically typed logic programs. In K. Furukawa, editor, Logic Programming. Proceedings of the Eighth
International Conference, pages 379–93. The MIT Press, 1991.
[28] E. Yardeni and E. Shapiro. A type system for logic programs. Journal of Logic
Programming, 10(2):125–153, 1991.
[29] J. Zobel. Derivation of polymorphic types for Prolog programs. In J.-L. Lassez,
editor, Logic Programming: Proceedings of the fourth international conference,
pages 817–838. The MIT Press, 1987.

This article was processed using the LaTEX macro package with LLNCS style

