A First-Order Theory of Types and Polymorphism in Logic Programming ^{∗}

Michael Kifer Department of Computer Science SUNY at Stony Brook Stony Brook, NY 11794 kifer@cs.sunysb.edu

James Wu Department of Computer Science SUNY at Stony Brook Stony Brook, NY 11794 wujwo@cs.sunysb.edu

Technical Report #90/23 July 1990 Department of Computer Science SUNY at Stony Brook

Abstract

We describe a new logic called typed predicate calculus (T PC) that gives declarative meaning to logic programs with type declarations and type inference. T PC supports all popular types of polymorphism, such as parametric, inclusion, and ad hoc polymorphism. The proper interaction between parametric and inclusion varieties of polymorphism is achieved through a new construct, called type dependency, which is analogous to implication types of [PR89] but yields more natural and succinct specifications. Unlike other proposals where typing has extra-logical status, in T PC the notion of type-correctness has precise model-theoretic meaning that is independent of any specific type-checking or type-inference procedure. Moreover, many different approaches to typing that were proposed in the past can be studied and compared within the framework of our logic. As an illustration, we apply T PC to interpret and compare the results reported in [MO84, Smo88, HT90, Mis84, XW88]. Another novel feature of T PC is its reflexivity with respect to type declarations; namely, in T PC these declarations can be queried the same way as any other data. This should be contrasted with other proposals where typing is part of meta-specifications about the program, inaccessible from within the program. Type reflexivity is useful for browsing knowledge bases and, potentially, for debugging logic programs.

∗Work supported in part by the NSF grant IRI-8903507

1 Introduction

Classical logic programming lacks the notion of typing and thus cannot protect predicates from taking semantically meaningless arguments. As a result, subgoals that are formed in this way—often referred to as type errors—are indistinguishable from the regular failing subgoals, which makes logic programs hard to debug. Typing information can also suggest various ways to optimize programs, and this opportunity is missed out in classical logic programming.

Several researchers have addressed this problem by attempting to enrich logic programming with various typing disciplines. These efforts can be classified into declaration-based and inference-based (also known as reconstruction-based or descriptive) approaches. Bruynooghe [Bru82] proposed a declarationbased type system, that requires the user to augment logic programs with type information, thereby enabling the system to detect type errors at compile time. Mycroft and O’Keefe [MO84] extended [Bru82] to support parametric polymorphism. Recently, Dietrich and Hagl [DH88] and Jacobs [Jac90] further extended [MO84] to handle inclusion polymorphism. Another approach to polymorphic type checking, based on HiLog [CKW89a, CKW89b], is discussed in [Fru89, YFS90].

Other researchers argued that declaration-based typing may severely impact the simplicity and flexibility of logic programming, since it requires every predicate symbol to be annotated with a type. Mishra [Mis84] was the first one to show that the idea of type inference that is widely used in functional languages is applicable to logic programs as well. This work was then followed by [MR85, KH85, Zob87, Azz88, Fru88, PR89], where various inference-based approaches were studied. The idea of type inference is to let the compiler infer the types of predicates automatically, with little or no declarations supplied by the user. With type inference, the compiler normally cannot detect type errors, since types are inferred from the syntactic structure of untyped programs. Nevertheless, the types inferred by the system can be presented to the user who—upon inspection—will decide whether the typing is consistent with the user’s intentions.

A drawback of many of the aforementioned approaches is that the notion of type errors and typecorrectness lacks model-theoretic semantics. This creates a disparity between the semantics of classical (untyped) programs and their typed counterparts. Furthermore, correctness of type checking or inference algorithms cannot be independently verified and thus many of these studies bear a significant ad hoc component.

In an attempt to close the semantic gap between programs and types, Xu and Warren [XW88, Xu89, XW90] developed a model theory for type-inference based on the notion of partial interpretations. They convincingly argued that in practice both paradigms, declaration-based and inference-based, are useful. They proposed an algorithm that takes into account user-supplied type declarations and then infers types for the rest of the predicates. Unfortunately, this approach does not work well in the presence of inclusion polymorphism, as discussed in Section 9.3.

In this paper, we propose a framework that unifies many of the above works. Section 9 presents a case-study of several representative approaches [MO84, Smo88, HT90, Mis84, XW88, XW90]. Our results shed new light on these works, and allow to compare them in a single framework.

We start with the classical first-order predicate calculus (abbr., PC) and extend it into a new logic, called typed predicate calculus (abbr., T PC), that supports all major types of polymorphism: inclusion, parametric, and ad hoc.

The notoriously hard problem in regard with polymorphism in logic systems is the accommodation of parametric types and type hierarchy. In T PC, this is achieved, in part, through the novel notion of type dependency. Polymorphic types are treated as first-class citizens and are represented as ordinary terms.^{1} The relationship among types and their instances is defined by the user, via logic formulae that correspond to type declarations of [MO84, YS87, XW88, Jac90], but are more general.

It should be noted that, despite its name, T PC is not a typed language. Instead, the type of a predicate is declared via logical formulas, called signatures, and types are enforced by semantics, modeltheoretic means (as opposed to the syntactic means, such as many-sorted algebras [Smo88, HT90]). Thus, unlike other approaches, type declarations in T PC are formulae in the object language of the logic, rather than syntactic expressions in a meta-language. This bridges the gap between the calculi of types and data and enables the user to query type declarations in quite sophisticated ways (see (2) of Section 5.3), which is useful for browsing the structure of knowledge bases and, potentially, also for debugging logic programs.

In T PC, type-correctness and type errors have precise model-theoretic meaning that is independent of any specific type checking algorithm. Likewise, the semantics of inferred types is independent of the inference algorithm. Therefore, various such algorithms can be formally studied and compared in our framework. Last but not least, as in [Xu89, XW90], type inference under partial type declarations has a natural semantics in T PC.

2 Typed Predicate Calculus

In this section, we introduce our new logic, Typed Predicate Calculus, that extends classical first-order predicate calculus both syntactically and semantically.

2.1 Syntax

The alphabet of a language L of T PC consists of (1) a set F of function symbols, (2) a set P of predicate symbols, and (3) a set V of variables, as in classical PC. Each function and predicate symbol has an arity—a nonnegative integer denoting the number of arguments that the symbol can take. A 0-ary function symbol is called a constant.

As in classical PC, a term is a constant, a variable, or a statement of the form f(t_{1}, ..., t_{n}), where f is a function symbol of arity n > 0 and the t_{i}’s are terms. In T PC, ground (i.e., variable-free) terms denote individual objects (as in PC) as well as classes (or types) of objects.^{2}

So as not to overwhelm the reader with too many new concepts, we first describe a 1-sorted version of our logic, which does not distinguish between individuals and classes. In particular, we will use just one sort of variables that range over the names of types as well as over the names of individuals populating these types. Section 7 presents a simple 2-sorted extension of T PC that allows us to distinguish between types and individuals and yet preserve the reflexivity of T PC, i.e., the ability to manipulate types the same way as data. In our formalism, typing is defined via the notion of a class of entities (or objects), and to foster this intuition we will be using the terms class and type interchangeably.

Atomic formulae of classical predicate calculus are called data atoms in T PC, in order to distinguish them from is-a and signature atoms introduced below.

1Jacobs [Jac90] uses a similar (but less general) term-based representation of types. His overall approach is not semantic, though, and the notion of type-correctness is algorithm-dependent. In a different context, term-based representation of types also appears in [KL89].

2The view of types as classes comes from object-oriented logics [KL89, KLW90].

To enable modeling the inclusion polymorphism, T PClets one organize terms in an is-a hierarchy via a new kind of atomic formulae, called is-a atoms. An is-a atom S : T, where S and T are terms, states that S is of the type T or, more precisely, S belongs to the class of things denoted by the term T. The notion of is-a atoms is the primary tool for representing polymorphic types. As will be seen later, the class denoted by T includes T itself (as a “typical” element) and thus is-a atoms denote non-strict subclass relationship. In particular, if S = T holds in all semantic structures then so do S : T and T : S.

Type constraints are imposed on predicates by means of another kind of atomic formulae, called signature atoms.^{3} A signature atom (abbr., signature), p⟨T_{1}, ..., T_{n}/α_{1} → β_{1}; ...; α_{k} → β_{k}⟩, for an n-ary predicate symbol p consists of a tuple of types represented as terms T_{1}, ..., T_{n} and a (possibly empty) set { α_{j} → β_{j} }_{j=1}^{k} of type-dependencies for p. A type-dependency α → β (abbr., T D) for a predicate symbol p is a statement of the form α → β, where α and β are sets of argument positions of p.

We shall see shortly that TDs behave similarly to functional dependencies of the database theory (although, by themselves, they do not enforce any functional dependency on predicates). Type dependencies generalize modes in Prolog literature [War77, DW86, DH88]. Intuitively, TDs represent the flow of control between predicate arguments. Section 5.2 (see after Example 5.5) shows that, in the presence of inclusion polymorphism, mode declarations alone are incapable of capturing certain subtleties of interaction between the types assigned to predicate arguments. TDs are also related to implicational types of [Red88], which serve similar purpose.

Informally, a signature such as p⟨u, v, w/{1, 2} → {3}; {3} → {1}⟩ states that for every data atom p(a, b, c), if a and b are of the types u and v, respectively, then c must be of the type w. Likewise, if c is of the type w then a is of the type u. For notational simplicity, we will often omit braces in signature atoms; e.g., we will write p⟨u, v, w/1, 2 → 3; 3 → 1⟩ instead of the above.

Signature atoms allow us to express parametric polymorphic type constraints. For example, the signature same type⟨T, T/1 → 2; 2 → 1⟩ means that the second argument of same type must conform to the type of the first and, at the same time, the first argument must conform to the type of the second one. Similarly, a type constraint for append can be defined by a signature append⟨list(T), list(T), list(T)/1, 2 → 3; 3 → 1, 2⟩, which requires that for all t, if the first two arguments of append have the type list(t) then so does the third argument, and vice-versa.

Given a TD α → β, the argument positions in the sets α and (β − α) are called domain and range positions, respectively (β − α denotes the ordinary set-difference). We note that either α, or β, or both may be empty, e.g., husband⟨man, woman/1, 2 → ∅⟩ or parent⟨person, person/∅ → 1, 2⟩. Likewise, α ∩ β may be non-empty. The meaning of such TDs will become apparent shortly. To shorten the notation, the set that contains all argument positions of a predicate is denoted by “ω” (the predicate in question will be always clear from the context). For example, we can write husband⟨man, woman/∅ → ω⟩ instead of husband⟨man, woman/∅ → 1, 2⟩. In summary, the language of T PC consists of the following three kinds of atomic formulae:

• data atoms p(T_{1}, ..., T_{n}), where p is an n-ary predicate symbol and T_{1}, ..., T_{n} are terms;

• is-a atoms S : T, where S and T are terms;

• signature atoms p⟨T_{1}, ..., T_{n}/α_{1} → β_{1}; ...; α_{k} → β_{k}⟩, where p is an n-ary predicate symbol, T_{1}, ..., T_{n} are terms, and α_{j} → β_{j}, 1 ≤ j ≤ k, are TDs of p.

3By analogy with functional programming languages, these can be viewed as signatures of the respective predicates.

The well-formed formulae of T PC are constructed from the atomic formulae by means of the connectives ¬, ∧, ∨ and the quantifiers ∃ and ∀, in the usual way.

Let α be a sequence of argument positions of an n-ary predicate. Given an n-tuple t⃗, we will write t⃗[α] to denote the projection of that tuple on the positions of α (e.g., if t⃗ = ⟨a, b, c⟩ then t⃗[2, 1, 1] = ⟨b, a, a⟩). In particular, if α is the empty set then t⃗[α] is the empty tuple. Likewise, if R is a relation of an appropriate arity, then R[α] denotes the relation obtained by projecting every tuple of R on α.

2.2 Semantics

Given a language L of T PC, a semantic structure I is a tuple ⟨U, ≺_{U}, I_{F}, I_{P}, I_{T} ⟩. Here U is the domain of I, partially ordered by ≺_{U}. As usual, we write a ⪯_{U} b whenever a ≺_{U} b or a = b. The ordering ≺_{U} defines the subclass relationship among the elements of U. Intuitively, a ≺_{U} b says that a is a subclass (or a subtype) of b. We extend ⪯_{U} to tuples over U in the usual way: for u⃗, v⃗ ∈ U^{n}, u⃗ ⪯_{U} v⃗ if this relation holds component-wise.

Function symbols are interpreted using the mapping I_{F} that assigns to each constant an element in U and to each n-ary (n > 0) function symbol f ∈ F a function I_{F}(f) : U^{n} → U.

Predicates too are interpreted exactly as in classical PC. For each n-ary predicate symbol p, I_{P}(p) is a subset of U^{n}, i.e., each n-ary predicate is interpreted via an n-ary relation. The equality predicate is interpreted in the standard way: I_{P}(=) =^{def} {⟨u, u⟩|u ∈ U}. Occasionally, we will refer to the tuples of I_{P}(p) as data-tuples and to I_{P}(p) itself as the data-relation assigned to p by I, to distinguish them from tuples and relations of the typing constraints associated with p (see next).

The typing constraints on predicates are defined via the mapping I_{T} that assigns to each n-ary predicate symbol p a relation I_{T} (p) ⊆ U^{n}×T D^{(n)}, where T D^{(n)} denotes the set of all type-dependencies on n-ary predicates. Each tuple ⟨t⃗, α → β⟩ in I_{T} (p) represents a typing constraint; such a constraint is satisfied by a data-tuple u⃗ in I_{P}(p), if whenever u⃗ conforms to the type t⃗ over the positions α, then u⃗ also conforms to the type t⃗ over the positions β. Formally, u⃗ satisfies Γ = ⟨t⃗, α → β⟩ if and only if

• u⃗ [α] ⪯_{U} t⃗[α] implies u⃗ [β] ⪯_{U} t⃗[β].

Observe that u⃗ satisfies ⟨t⃗, α → β⟩ if and only if it satisfies ⟨t⃗, α → (β − α)⟩, i.e., repeating some or all of the argument-positions of α in β does not change the meaning of the TD α → β. Also, if α = ∅ then u⃗ [β] ⪯_{U} t⃗[β] holds unconditionally and if β ⊆ α (in particular, if β = ∅) then ⟨t⃗, α → β⟩ constrains nothing.

We require each I_{T} (p) to be closed with respect to the implication of TDs as well as the supertyping relationship: TD Implication:

Let Γ, Γ_{1}, ..., Γ_{k} be type dependencies in T D^{(n)}. We say that {Γ_{1}, ..., Γ_{k}} logically implies Γ, denoted {Γ_{1}, ..., Γ_{k}} ⊧_{T D} Γ, if

• for all domains ⟨V, ≺_{V} ⟩ and for all tuples u⃗, t⃗ ∈ V^{n}, if u⃗ satisfies all of ⟨t⃗, Γ_{1}⟩ ,...,

⟨t⃗, Γ_{k}⟩ then it also satisfies ⟨t⃗, Γ⟩.

(E.g., 1, 2 → 3 and 3 → 4, 5 imply 1, 2 → 4, 5; inference rules for TDs appear in Section 4.)

Supertyping:

Let t⃗ and s⃗ be tuples of the same arity and τ_{1} = ⟨t⃗, α → β⟩, τ_{2} = ⟨s⃗, α → β⟩ be a pair of typing constraints tagged with the same TD. We say that τ_{1} is a supertyping of τ_{2} (or that τ_{1} is a typing weaker than τ_{2}), denoted τ_{1} ⪯_{T} τ_{2}, if

1. t⃗[ω − (α ∪ β)] = s⃗ [ω − (α ∪ β)], where ω denotes the set of all component-places of t⃗ (and s⃗);

2. t⃗[α] ⪯_{U} s⃗ [α]; and

3. s⃗ [β − α] ⪯_{U} t⃗[β − α].

Condition (2) above requires t⃗ to be a subtype of s⃗ in the domain-positions of the TD, while condition (3) says that t⃗ must be a supertype of s⃗ in the range-positions. Clearly, a data-tuple that satisfies τ_{2} also satisfies its supertyping, τ_{1}. If we view predicates as set-valued functions from the domain positions to the range positions, these conditions become identical to the usual statements about functional types.

A relation I_{T} (p) is closed with respect to the implication of TDs (⊧_{T D}) and the supertyping relationship (⪯_{T}) if and only if the following two conditions hold:

1. If ⟨t⃗, Γ_{1}⟩, ..., ⟨t⃗, Γ_{k}⟩ ∈ I_{T} (p), and {Γ_{1}, ..., Γ_{k}} ⊧_{T D} Γ, then ⟨t⃗, Γ⟩ ∈ I_{T} (p); and

2. If τ ∈ I_{T} (p) and τ′ ⪯_{T} τ then also τ′ ∈ I_{T} (p).

In a semantic structure I, the data-relation associated to a predicate symbol, p, must satisfy the typing constraints associated with p. Formally, this means that the relationship between I_{P} and I_{T} is governed by the following rules that glue together the semantics of predicates with that of their signatures.

The Well-Typing Conditions: For every predicate p in P, and every data-tuple s⃗ ∈ I_{P}(p):

1. s⃗ satisfies every typing constraint in I_{T} (p);

2. there is a typing constraint ⟨t⃗, α → β⟩ in I_{T} (p), such that s⃗ ⪯_{U} t⃗.

Condition (2) here requires that every data-tuple s must conform to at least one tuple of types, t⃗, in I_{T} (p).

A variable-assignment, ν, is a mapping from variables, V, to the domain U. It is extended to terms in the usual way: ν(f(t_{1}, ..., t_{n})) = I_{F}(f)(ν(t_{1}), ..., ν(t_{n})). Let I be a semantic structure and ν a variable-assignment. Satisfaction of an atom A under a semantic structure I and a variable-assignment ν, denoted I ⊧_{ν} A, is defined as follows:

1. For an is-a atom S : T, I ⊧_{ν} S : T if and only if

• ν(S) ⪯_{U} ν(T).

2. For a signature atom A = p⟨T_{1}, ..., T_{n}/α_{1} → β_{1}; ...; α_{k} → β_{k}⟩, I ⊧_{ν} A if and only if

• When k ≥ 1: ⟨ν(T_{1}), ..., ν(T_{n}), α_{i} → β_{i}⟩ ∈ I_{T} (p), for i = 1, ..., k;

• When k = 0: ⟨ν(T_{1}), ..., ν(T_{n}), ∅ → ∅⟩ ∈ I_{T} (p).

3. For a data atom A = p(T_{1}, ..., T_{n}), I ⊧_{ν} A if and only if

• ⟨ν(T_{1}), ..., ν(T_{n})⟩ ∈ I_{P}(p).

The meaning of the formulae ϕ ∨ ψ, ϕ ∧ ψ, and ¬ϕ is defined in the standard way: I ⊧_{ν} ϕ ∨ ψ (or I ⊧_{ν} ϕ ∧ ψ, or I ⊧_{ν} ¬ϕ) if and only if I ⊧_{ν} ϕ or I ⊧_{ν} ψ (resp., I ⊧_{ν} ϕ and I ⊧_{ν} ψ, resp., I |̸=_{ν} ϕ). The meaning of quantifiers is also standard: I ⊧_{ν} ψ, where ψ = (∀X)ϕ (or ψ = (∃X)ϕ) if for every (resp., some) μ that agrees with ν everywhere, except possibly on X, I ⊧_{μ} ϕ.

Clearly, for a closed formula, ψ, its meaning is independent of a variable-assignment, and we can thus write I ⊧ ψ, when ψ is closed. A semantic structure I is a model of ψ if I ⊧ ψ. If S is a set of formulae and ψ is a formula, we write S ⊧ ψ (ψ is logically implied or entailed by S) if and only if ψ is true in every model of S.

2.3 Untyped Semantic Structures

In order to distinguish the well-typed T PC programs from the ill-typed ones, we introduce the notion of untyped semantic structures and models.

Untyped semantic structures for a T PC language L are defined similarly to ordinary T PC semantic structures, except that the former are not required to satisfy the well-typing conditions of the previous subsection. From now on, the semantic structures introduced in the previous subsection will be called typed semantic structures.

The notion of formula satisfaction by untyped structures goes unchanged. We use the same notation I ⊧_{ν} ψ (I ⊧ ψ, for closed formulae) to denote the fact that I satisfies ψ. An untyped semantic structure I is an untyped model of a closed formula ψ if I ⊧ ψ.

It is easy to see that every typed semantic structure (or model) is also an untyped structure (resp., model) and that any untyped model that is also a typed semantic structure is a typed model.

Although the notion of untyped logical entailment between formulae is immediate, we are not going to use it in the future. Therefore, if S is a set of formulae then S ⊧ ψ will always stand for the typed entailment defined in Section 2.2.

In the sequel, unqualified references to semantic structures (or models) will refer to the typed versions of these concepts. However, we shall often explicitly add the qualifier “typed,” for the contrast. On the other hand, when untyped semantic structures are meant, the qualifier “untyped” will always be present.

3 Skolem and Herbrand’s Theorems

Since quantification in PC and T PC is similar, Skolemization is similar too. For instance, a Skolem normal form for ∀X∃Y (p⟨X, Y ⟩∨q(Y) ) would be ∀X(p⟨X, f(X)⟩∨q(f(X)) ), where f is a new function symbol.

Theorem 3.1 (cf. Skolem Theorem) Let ϕ be a formula (that may contain data, is-a, and signature atoms) and ϕ′ be its Skolemization. Then ϕ is unsatisfiable if and only if so is ϕ′.

Given a language L, its Herbrand universe, denoted U(L), is the set of all ground (i.e., variablefree) terms in the language. The Herbrand base of L, denoted H(L), is the set of all ground atomic formulae in the language, including is-a, signature, and data atoms. A Herbrand interpretation, H, is a semantic structure with the domain U(L) and the standard interpretation I_{F}^{H} of function symbols: if f is a k-ary function symbol then I_{F}^{H}(f)(t_{1}, ..., t_{k}) = f(t_{1}, ..., t_{k}). Equivalently, Herbrand interpretations can be defined as subsets of H(L) that are closed under the logical implication “⊧”. The closure requirement is convenient here since ground atoms may imply other atoms in a non-trivial way, e.g. {p⟨a, b, c/1 → 2⟩, p⟨a, b, c/1 → 3⟩} ⊧ p⟨a, b, c/1 → 2, 3⟩. This is similar to predicate calculus with equality, where sets of ground atoms may imply other atoms.

Proposition 3.1 Let S be a set of clauses. Then S is unsatisfiable if and only if S has no Herbrand model.

Proof: The proof is similar to that in PC. □

Proposition 3.2 Let L be an arbitrary language of T PC. There is a corresponding language L′ of PC and a pair of transformations

Φ : T PC-formulae of L ⟼ PC-formulae of L′

Ψ : T PC-semantic structures for L ⟼ PC-semantic structures for L′

such that for every T PC-formula ϕ in L and a T PC-semantic structure M, M ⊧_{T PC} ϕ if and only if Ψ(M) ⊧_{PC} Φ(ϕ) ( ⊧_{T PC} and ⊧_{PC} denote logical implication in T PC and PC, respectively).

Proof: In constructing these mappings, one needs to introduce the “signature-version” for each predicate p (i.e., a new predicate name p^{sig}) and then use formulae of predicate calculus to encode the unique features of T PC-semantic structures, including the is-a relationship, the well-typing conditions, the closure requirements of TDs, and the supertyping relationship. □

Theorem 3.2 (cf. Herbrand’s Theorem) A set of clauses S is unsatisfiable if and only if so is some finite subset of ground instances of clauses in S.

Proof: The result follows from Proposition 3.2 and Herbrand’s theorem for PC. □

As in PC, Herbrand’s theorem for T PC is in the basis of the completeness proof for the resolutionbased proof procedure that is presented in the next section.

4 Proof Theory

The existence of some proof theory for T PC is not at all surprising in view of Proposition 3.2. What is remarkable though is the existence of a complete proof theory that combines ordinary resolution with type-inference rules commonly found in the works on typing of functional programs.

In view of Skolem theorem, we can restrict our attention to formulas in the clausal form, i.e., universally quantified disjunctions of literals, where literal is either an atomic formula or negation of an atomic formula.

A substitution, σ, is a mapping {Variables of L} ⟶ {Terms of L} that is an identity almost everywhere but on a finite number of variables. The notion of unifiers in T PC is the same as in PC: Given a set L_{1}, ..., L_{n} of literals of the same kind (is-a, data, or signature), a substitution σ is a unifier if σ(L_{1}) = ... = σ(L_{n}). A unifier σ is most general if for every other unifier, γ, there is a substitution θ such that γ = θ ∘ σ.

Consider a set S = {p⟨T⃗/Γ_{1}⟩, ..., p⟨T⃗/Γ_{k}⟩} of signature-atoms that differ only in the TD-part. It is easy to check that S logically entails every atom p⟨T⃗/Γ⟩ such that each member of Γ is ⊧_{T D}-entailed by the union of Γ_{1}, ..., Γ_{k}. For instance, since {1 → 2, 3} ⊧_{T D} 1 → 2 and {1 → 2, 3} ⊧_{T D} 1 → 3, we have {p⟨a, b, c/1 → 2, 3⟩} ⊧ p⟨a, b, c/1 → 2; 1 → 3⟩. To account for the derivations of this kind, we need to characterize the logical implication among sets of TDs. The following inference rules are sound and complete for TDs. Incidentally, these rules coincide with the well-known Armstrong’s axioms for functional dependencies [Ull88]. Let Γ be a set of TDs for n-ary predicates, and let ω_{n} = {1, ..., n}.

Reflexivity : If β ⊆ α ⊆ ω_{n}, then Γ ⊢_{T D} α → β.

Augmentation : If Γ ⊢_{T D} α → β then Γ ⊢_{T D} (α ∪ δ) → (β ∪ δ), for some δ ⊆ ω_{n}.

Transitivity : If Γ ⊢_{T D} α → β and Γ ⊢_{T D} β → γ then Γ ⊢_{T D} α → γ.

A derivation of a TD γ from Γ is a sequence γ_{1}, ..., γ_{m} such that γ_{m} = γ and each γ_{i} is either in Γ or is derived from γ_{1}, ..., γ_{i−1} by one of the above rules. We write Γ ⊢_{T D} Γ′, where Γ′ is a set of TDs, if every member of Γ′ can be derived from Γ using a derivation sequence from Γ. The question of whether or not Γ ⊢_{T D} γ, can be decided in linear time in the sizes of Γ and γ [BB79].

Proposition 4.1 The inference rules for TDs are sound and complete, that is,

Γ ⊧_{T D} γ if and only if Γ ⊢_{T D} γ.

Proof: Similar to the corresponding proof for functional dependencies [Ull88]. □

It follows from the above rules for TDs that ∅ → ∅, ω → ∅ and, in fact, any TD α → β, where β ⊆ α, is a tautology. Thus, for instance, p⟨t⃗/ω → ∅⟩ is logically equivalent to p⟨t⃗/∅ → ∅ ⟩ and to p⟨t⃗/ ⟩. Tautological TDs will be called trivial in the sequel.

Figure 1 lists the inference rules for T PC. In this figure, if S⃗ and T⃗ are tuples of terms of the same arity n then mgu(T⃗, S⃗) denotes the most general simultaneous unifier of T⃗ [i] and S⃗ [i] (i = 1, ..., n). In the paramodulation rule, L[T] denotes a literal that contains T as a term; L[S′] denotes the same literal with one occurrence of T replaced by S′. A derivation of a clause C from a set of clauses P is a sequence C_{0}, ..., C_{n}, where C_{n} = C and each C_{i} is either in P or is derived from C_{0}, ..., C_{i−1} using one of the derivation rules of Figure 1. Existence of such a derivation, is denoted by P ⊢ C. A refutation of P is a derivation of an empty clause from P.

Theorem 4.1 (Soundness) If P ⊢ C then P ⊧ C.

Theorem 4.2 (Completeness) If a set of clauses P is unsatisfiable then there is a refutation of P.

5 Well-Typed Logic Programs

T PC is much too general than what we actually might need in order to write programs. Apart from the usual restrictions on the form of rules in logic programs, we will dissect T PC programs into the following three disjoint components:

1. class-hierarchy (or is-a hierarchy) declaration;

2. type declaration; and

3. data definition.

Core Inference Rules

1. Resolution:  ¬A ∨ C_{1}, A′ ∨ C_{2}, θ = mgu(A, A′) ⊢ θ(C_{1} ∨ C_{2})
2. Factorization:  L ∨ L′ ∨ C, θ = mgu(L, L′) ⊢ θ(L ∨ C)
3. Paramodulation: L[T] ∨ C_{1}, T′ = S′ ∨ C_{2}, θ = mgu(T, T′) ⊢ θ(L[S′] ∨ C_{1} ∨ C_{2})

Inference Rules for ISA

4. ISA-reflexivity:  ⊢ T : T
5. ISA-transitivity: S : R ∨ C_{1}, R′ : T ∨ C_{2}, θ = mgu(R, R′) ⊢ θ(S : T ∨ C_{1} ∨ C_{2})
6. ISA-acyclicity:  S : T ∨ C_{1}, T′ : S′ ∨ C_{2}, θ = mgu(⟨S, T ⟩, ⟨S′, T′⟩) ⊢ θ(S = T ∨ C_{1} ∨ C_{2})

Inference Rules for Typing

7. TD-derivation:  p⟨T⃗/Γ⟩ ∨ C_{1}, p⟨T⃗′/Γ′⟩ ∨ C_{2}, Γ ∪ Γ′ ⊢_{T D} Γ′′, θ = mgu(T⃗, T⃗′)

⊢ θ(p⟨T⃗/Γ′′⟩ ∨ C_{1} ∨ C_{2})

8. Supertyping #1: p⟨T_{1}, ..., T_{n}/Γ⟩ ∨ C_{1}, S : T′ ∨ C_{2}, α → β ∈ Γ, i ∈ α,

θ = mgu(T_{i}, T′) ⊢ θ(p⟨T_{1}, ..., T_{i−1}, S, T_{i+1}, ..., T_{n}/α → β⟩ ∨ C_{1} ∨ C_{2})

9. Supertyping #2: p⟨T_{1}, ..., T_{n}/Γ⟩ ∨ C_{1}, T′ : S ∨ C_{2}, α → β ∈ Γ, j ∈ β − α,

θ = mgu(T_{j}, T′) ⊢ θ(p⟨T_{1}, ..., T_{j−1}, S, T_{j+1}, ..., T_{n}/α → β⟩ ∨ C_{1} ∨ C_{2})

Inference Rules for Type Checking

10. Well-typing #1: p(S⃗) ∨ C_{1}, p⟨T⃗/Γ⟩ ∨ C_{2}, α → β ∈ Γ, θ = mgu(S⃗ [α], T⃗ [α]),

⊢ θ(S⃗ [j] : T⃗ [j] ∨ C_{1} ∨ C_{2}), for all j ∈ β − α

11. Well-typing #2: p(S⃗) ∨ C ⊢ p⟨S⃗/∅ → ∅ ⟩ ∨ C

Figure 1: T PC Inference Rules

Strictly speaking, this separation is not necessary for our theory to work. However, this seems to be a common practice so far in the works on types in logic programming and we do not intend to break the tradition in this paper. We note that object-oriented logic languages [KLW90] may require additional flexibility of being able to define classes that contain all objects with certain typing or internal state. In such a case, the above three components might not be independent.

The following subsections discuss the aforesaid program components separately. As we shall see, the monotonic semantics of Section 2.2 is not strong enough to capture all aspects of typing. We then define a nonmonotonic semantics of logic programs on top of the logical entailment relation “⊧” of Section 2.2 and argue that this gives an adequate semantics to the notion of type-correctness.

5.1 Class-Hierarchy Declaration

Class or is-a hierarchies are specified via sets of definite Horn clauses that involve is-a and equality atoms only. Such a declaration, Isa, says what is a subclass (or a subtype) of what, i.e., if Isa ⊧ p : q, then p is a subclass of q. It also specifies which types can be referred to via different names. For instance, if Isa ⊧ (human = person) then human and person denote the same type. In the following, we will use the terms class/subclass and type/subtype interchangeably.

Unfortunately, as given, class declarations are too weak since definite Horn clauses cannot tell what is not a subclass of another class. The solution is to use the Closed World Assumption (abbr., CWA)— a standard technique for nonmonotonic reasoning that allows to infer negative information from Horn clause programs; it states that whenever Isa |̸= p : q then one can nonmonotonically derive ¬p : q. As is well known, for definite Horn clauses, CWA is tantamount to restricting logical entailment to minimal models only.

The minimality order on untyped semantic structures is defined as follows: Let İ and Ï be a pair of semantic structures. Then İ ≪^{min} Ï if and only if for every ground atom ϕ, İ ⊧ ϕ implies Ï ⊧ ϕ.

The class hierarchy defined by P is the set of all ground is-a atoms satisfied by some minimal model of P. Note that since Isa is a set of definite Horn clauses and is-a atoms do not depend on the rest of P, it does not matter which minimal model is chosen here, even if other components of P are non-Horn.

Example 5.1 Consider the following class-hierarchy declaration:

{man : person \atop woman : person}  john : man ; bob : man ; peter : man  mary : woman ; ann : woman ; sue : woman.

This declaration states not only that john is a man, but also that john is not a woman. The former is defined explicitly, while the latter is derived nonmonotonically by CWA, since john : woman is not logically entailed by the declaration.

The first pair of clauses above define the subtype relationship among man, woman, and person; subtype relationship is a key ingredient in the notion of inclusion polymorphism. □

Example 5.2 The type of all objects, all, and the type of natural numbers, nat, can be defined thus:

X : all  (1)
zero : nat
succ(X) : nat ⟵ X : nat.

The first clause says that every thing is of the type all (including the constant all itself). From now on, the symbol all will be reserved to denote the type of all things, whenever it is defined (note: (1) may not be part of Isa and thus all may not be defined). The last pair of clauses recursively defines the instances of nat: zero, succ(zero), succ(succ(zero)), and so on. □

In T PC, types are denoted by terms, so they may contain variables. This gives us the flexibility needed to support parametric polymorphism.

Example 5.3 The following pair of clauses defines a parametric type list(T):

\begin{matrix}nil : list(T) \\ cons(X, Y) : list(T) ⟵ X : T & Y : list(T). \end{matrix}

Let nat denote the type of natural numbers. Then list(nat) is the type of all lists of natural numbers, containing elements such as nil, cons(zero, nil), cons(zero, cons(succ(zero), nil)), and so on. □

Observe that we do not require types to be tuple-distributive in the sense of [Mis84]. However, usually they will come out that way, if the semantic of a specific type calls for this feature (cf. list(T) above). Likewise, in T PC, type constructors do not have to be monotonic. For instance, the definition of list(T) in Example 5.3 does not guarantee that list(nat) : list(int) holds, even if nat : int is known to hold. It is true, however, that if a : list(nat) holds for some term a, then so does a : list(int), as expected. If monotonicity is desired, it can be declared explicitly, e.g.,

list(T) : list(S) ⟵ T : S.

5.2 Type Declaration

A type declaration is a set of definite Horn clauses with signature atoms in the head and signature or is-a atoms in the body. The purpose of type declarations is to impose type constraints on the arguments of predicates.

Unfortunately, as in the case of class hierarchies, the monotonic semantics of T PC is not (and cannot be) strong enough to capture the idea of typing. For instance, plus⟨int, int, int/1, 2 → 3⟩ and plus(“a”,“b”,“c”) are consistent with each other: an appropriate model could be the one where ⟨“a”, “b”, “c”, {1, 2} → {3}⟩ belongs to I_{T} (plus).

Luckily, CWA rescues the situation once again. It is clear that in order to eliminate the “wrong” models where plus(“a”,“b”,“c”) is true, we need to ensure that I_{T} contains no “accidental” tuples, like ⟨“a”, “b”, “c”⟩, i.e., tuples that are not logically mandated by the given type declarations. This can be achieved by minimizing semantic structures with respect to signature-atoms that they satisfy, and the minimal model semantics discussed in the previous section can be used once again. Intuitively, we want the typing of a program P to be the set of all ground signature-atoms satisfied by some minimal model of P. Again, the specifics of the minimal model do not matter, even when P is non-Horn, because Type and Isa are Horn and is-a and signature-atoms do not depend on the rest of P. (As noted earlier, this independence of Isa and Type from the rest of the program does not really matter, but it is traditional and simplifies the discussion somewhat.)

Example 5.4 A possible type declaration for husband, parent, and play relations is:

{husband⟨man, woman/∅ → ∅⟩ \atop parent⟨person, person/∅ → ∅⟩}  {play⟨team, team/1 → 2; 2 → 1⟩ \atop play⟨jr team, jr team/1 → 2; 2 → 1⟩.}

We assume that man : person, woman : person, and jr team : team hold and these classes are suitably defined. The typing constraint imposed by the first signature requires husband to be a relation between instances of the classes man and woman. The second signature requires parent to be a relation between persons. The typing for play says that, in general, teams play against teams, but junior teams (jr team) play against junior teams.

For instance, if P =^{def} Isa ∪ Type ∪ Data is a program and Isa ⊧ giants : team ∧ yankees : team then play(giants, yankees) is well-typed. However, if Isa ⊧ pee wee : jr team but Isa |̸= giants : jr team then play(giants, pee wee) is ill-typed in the sense that P has no typed minimal model, i.e., none of its untyped minimal models satisfies the well-typing conditions of Section 2.2. □

Each TD represents a particular type-enforcement pattern. One can therefore expect that signatures tagged with different TDs will result in different typing constraints.

Example 5.5 Consider the following pair of type declarations:

T_{1} : {p⟨student, student/∅ → ∅⟩ \atop p⟨employee, employee/∅ → ∅⟩} T_{2} : {p⟨student, student/∅ → ω⟩ \atop p⟨employee, employee/∅ → ω⟩.}

Here, T_{1} says that every tuple of p must be either a student-student pair or an employee-employee pair, and nothing else. In contrast, the signatures in T_{2} require each tuple in p to be both a student-student pair and an employee-employee pair. It is instructive to consult the definitions in Section 2.2 to see why this is indeed the case.

Another interesting observation is that T_{1} and T_{2} are examples of so called ad hoc polymorphism: normally student and employee are incomparable in the class hierarchy and therefore the set of tuples in p may be heterogeneous. □

The above examples illustrate the importance of TDs for specifying the typing of predicate symbols. It follows from the definitions that whenever a predicate symbol, p, has at most one ground signature-atom associated with it, then the specifics of TDs that tag this atom are immaterial. For instance, in Example 5.4, the TDs associated with the signature of husband or parent do not matter much: husband⟨man, woman/∅ → ω⟩ would yield the same semantics. Indeed, according to the definitions in Section 2.2 and the notion of well-typedness given below (in Section 5.4), both signatures mean the same: an atom husband(a, b) is consistent with any of the above signatures for husband if and only if Isa ⊧ a : man ∧ b : woman. (It is important to understand, however, that even though husband⟨man, woman/∅ → ω⟩ and husband⟨man, woman/∅ → ∅⟩ result in the same typing for husband, these two signatures are logically inequivalent.)

The difference in tagging shows up in the presence of multiple signatures for the same predicate in the presence of the subtype relationship. One example to this effect is given in Example 5.5. Similarly, the typing of play in Example 5.4 would have had a different meaning if we changed the TDs, e.g., play⟨jr team, jr team/∅ → ∅⟩. Such tagging would have made play(giants, pee wee) type-compatible with the signatures for play. Even more subtle cases arise when parametric types interact with subtyping. For instance, suppose that int : real and the signature for append is append⟨list(T), list(T), list(T)/∅ → ∅ ⟩. Then append([1], [2, 3], [2.3, 1.4]) will be consistent with this signature, namely with its instance append⟨list(real), list(real), list(real)/∅ → ∅ ⟩. Even the more intuitive typing append⟨list(T), list(T), list(T)/1, 2 → 3⟩ is not completely adequate, since it permits atoms such as append([0.5], [1, 3.2], [3, 4]), i.e., appending a pair of lists of non-integers that yields a list of integers. This does not contradict the signature since int is a real, according to our assumption. A better signature would be append⟨list(T), list(T), list(T)/1, 2 → 3; 3 → 1, 2⟩. For example, the atom append([0.5], [1, 3.2], [3, 4]) is not consistent with this signature, since the TD {3} → {1, 2} requires the first two arguments of append to be of the type list(int), whenever so is the third argument.

Observe that, in contrast to our approach, predicate modes for append [DH88] can express only what amounts to a single TD {1, 2} → {3}, and therefore the anomaly exhibited above is inevitable. This shows that several subtleties of the interplay between argument types elude the mode declaration idea.

5.3 Data Definition

A data definition, Data, is a set of rules where data-atoms are in the head, while the rule-bodies may consist of arbitrary, possibly negated, literals (is-a, data, or signature). The purpose of data definitions is to define the meaning of predicates. We call Data the “data definition” because it defines the objectlevel data, such as parent(tom, john) or play(giants, yankees); in contrast, class-hierarchy and type declarations specify what can be viewed as “meta” or “higher-order” data.

It is easy to see that every data definition that consists of definite Horn rules has a unique least Herbrand model, which can be taken as its semantics. With negative literals in rule-bodies, there is a number of different competing semantics [GRS88, GL88, Van89, AV88, KP88], each of which can easily be adapted to T PC. All of these semantics have in common that the logical entailment is defined with respect to some subset of models, called canonic models (which may be different for different proposals).

We can thus assume that there is a subclass of canonic models among all the T PC-models and that untyped canonic models of P = Data ∪ Isa ∪ Type are precisely the canonic models within the class of all untyped models of P. (It is essential here that we talk about models of P and not just of Data.) A typed canonic model is any typed semantic structure that is also an untyped canonic model.

Since all our examples employ definite Horn clauses only, the reader can handily think that canonic models coincide with ≪^{min} -minimal models defined in Section 5.1. Precise definitions of canonic models in T PC according to the prefect [Prz88], well-founded [GRS88, Van89], or stable model semantics [GL88] can be given along the lines of the corresponding developments in PC and are beyond the scope of this paper. We just note that in the case of well-founded models the glue conditions of Section 2.2 need to be modified to account for the fact that well-founded models are 3-valued.

It follows from the definition that signature-atoms are allowed to appear in the body of the rules in data definitions. This makes T PC a reflexive theory where programs can examine and reason about the typing of predicates via the same mechanism as the one used for querying data. For instance, the query

?− play⟨X, Y/∅ → ∅⟩ & play(V, W) & V : X & W : Y  (2)

would return all the typings for play such that this predicate actually has a data-tuple that conforms to this typing. The latter condition is not a trivial one, since it is quite possible for a polymorphic predicate not to have any data-tuple conforming to some of its legal typings. For instance, if in Example 5.4 play had no data about junior teams, this query would have returned the answer X = Y = team (since play⟨team, team/∅ → ∅⟩ is a logical consequence of the clause play⟨team, team/1 → 2; 2 → 1⟩ in Example 5.4), leaving the other candidate answer, X = Y = jr team, out.

Notice that in (2) the result depends on the available object-level data as well as type declarations. We envision that queries against type declarations of T PC logic programs will be quite useful for debugging. In [KLW90] such queries are shown to be useful for browsing knowledge bases.

5.4 The Semantics of Well-Typedness

We now pull together the various pieces discussed so far and define a semantics for T PC programs.

Example 5.6 The following is a complete definition for append, which includes a class-hierarchy declaration, a type declaration, and a data definition:

nil : list(T)  % Class-hierarchy declaration
cons(X, L) : list(T) ⟵ X : T & L : list(T)
append⟨list(T), list(T), list(T)/1, 2 → 3; 3 → 1, 2⟩ % Type declaration
append(nil, L, L) ⟵ L : list(T)  % Data definition
append(cons(X, L), M, cons(X, N))
⟵ append(L, M, N) & X : T & N : list(T).

□

Semantics of logic programs is now defined with respect to the class of typed canonic models. Since this is only a subset of all models of P, the corresponding logical entailment is nonmonotonic and is denoted by “|≈”: Given a logic program P, we write P |≈ ψ if and only if for all typed canonic models M of P, M ⊧ ψ.

Now we can formally define type errors and well-typed programs. A logic program has a type-error if it has no typed canonic models but does have untyped ones. A program is well-typed (or typecorrect) if and only if it has no type error. This model-theoretic notion of type error is unique to T PC; it separates programs that have no models due to some intrinsic logical inconsistency in the data from programs that lack models because of type-incompatibility.

Note that in Example 5.6 the program may not be well-typed without the last two conjuncts in the body of the last clause. that—perhaps unexpectedly—this program may be ill-typed. Indeed, suppose our type system contains only int and string, which do not have a common supertype. Then, because of the unrestricted variable X in the head of the last clause for append, the data definition may produce a fact of the form append([1], [“abc”], [1, “abc”]). Since int and string have no common supertype, every untyped canonic model for append must be such that I_{T} (append) has no type-constraint that covers ⟨[1], [“abc”], [1, “abc”]⟩ and hence the second well-typing condition in Section 2.2 cannot be satisfied. On the other hand, if Isa had the “type of all things” (see (1) of Section 5.1), then the program in Example 5.6 would have been well-typed.

In general, in the presence of polymorphic types the programmer must be careful with variables that are not restricted by positive literals in the rule body, and it might be a good programming practice to explicitly indicate which types are allowed for such variables.

5.5 Discussion

Various approaches to types in logic programming can be classified as syntactic or semantic. Syntactic approaches, usually found in the works on type checking (e.g., [MO84, DH88, Smo88, Fru89, YFS90, Jac90, HT90]), see the notion of type-correctness as a syntactic concept. Their notion of well-typing is defined by a set of “well-formedness rules” that are imposed directly on the syntactic structure of logic programs. In contrast, semantic approaches, where T PC and most of the works on type inference (e.g., [Mis84, YS87, Xu89]) belong, define the concept of type-correctness in model-theoretic or set-theoretic terms. For instance, in T PC, a program is regarded as well-typed if and only if the intended model of the program satisfies the well-typing conditions of Section 2.2.

As a rule, the criteria for well-typedness in syntactic approaches are stricter than in semantic approaches. For instance, a program may be ill-typed according to Mycroft and O’Keefe [MO84] but not in T PC. As an example, let P have an is-a hierarchy declaration Isa such that Isa |̸= a : int and let the rest of P include

\begin{matrix}p⟨int/ ⟩ \\ q⟨all/ ⟩ \\ p(a) ⟵ false \end{matrix}  (3)

where false is a propositional constant such that P |̸= false. This program is well-typed in T PC, for p(a) is never derived. In Mycroft-O’Keefe’s type system [MO84] this program is clearly ill-typed because p(a) is ill-formed regardless of whether it can be derived or not.

One advantage of syntactic approaches is that the type-checking problem is (usually) decidable, since only finitely many program components need be examined. In semantic approaches, however, type checking is undecidable, in general. The following lemma shows that this is also the case in T PC.

Lemma 5.1 The class of the well-typed Horn programs in T PC is not recursively enumerable.

Proof: The proof is by a reduction from the query emptiness problem. Query emptiness is a problem of whether the set of solutions to a logical query ?− q(...) defined by a program P is empty. The class of all empty queries is known to be nonrecursively enumerable. (For instance, in the proof of Theorem 2-6, Manna [Man74, pages 105-106] shows that for every Post system S there is a Horn program P and a query ?− p(Z, Z) such that this query has no answers if and only if S has no solution.)

The reduction from query emptiness to type-correctness is carried out as follows. Let P be a program and q be a query predicate (it suffices to consider only atomic queries). We can also assume that q appears only in the heads of the rules in P, which can be ensured by a simple program transformation. We now construct a signature Σ for P so that for every predicate p in P, except q, Σ contains the signature atom p⟨X_{1}, ..., X_{k}/∅ → ∅⟩. However, Σ does not contain any signature for q. Clearly, the T PC program P ∪ Σ is well-typed if and only if ?− q(X_{1}, ..., X_{n}) has no answers. □

Another advantage of syntactic approaches is that they go farther (than semantic approaches) towards capturing the notion of ill-typed atoms in rule bodies, i.e., atoms that are instantiated with type-incompatible arguments. The importance of capturing type inconsistency in rule bodies lies in the fact that this leads to the notion of useless clauses [YS87], i.e., clauses that do not affect the meaning of a program. Let the program P be:

\begin{matrix}r⟨string/ ⟩ & r(X) ⟵ p(X) & q(X). \\ p⟨string/ ⟩ \\ q⟨int/ ⟩ \end{matrix}  (4)

Suppose int and string have no common subtypes and elements. Then any type assignment for X makes either p(X) or q(X) ill-typed because string and int do not share common subtype or instances. As a consequence, P would be regarded as ill-typed by syntactic approaches, such as Mycroft-O’Keefe’s [MO84]. In contrast, the notion of well-typedness in T PC given earlier does not capture the above intuition and is too weak to classify P as ill-typed.

There are deficiencies in syntactic approaches, too. Many such approaches insist that well-typed programs should not “go wrong” [Mil78, MO84]. Although this requirement causes problems even without subtyping, the latter makes it unavoidable to think of better criteria for syntactic well-typedness. For instance, the not-going-wrong requirement makes it illegal to ask for the intersection of a pair of predicates that define heterogeneous sets. Suppose p is true of a term whenever it belongs to the class employee and q is true of and only student objects. Then the query ?− p(X) & q(X) is likely to “go wrong” whenever p(X) is instantiated to an employee-nonstudent fact or when q(X) is instantiated to a student-nonemployee fact.

Another problem is in applying syntactic well-typedness to programs with negation. Consider the following example:

r⟨all/ ⟩  r(X) ⟵ p(X) & ¬q(X).
p⟨all/ ⟩
q⟨int/ ⟩

The intention of the last clause is to compute the set difference of p and q. Here, the variable X should be given the type all to cover the type of p. However, under this type assignment X becomes type-incompatible with q and, say, Mycroft-O’Keefe’s well-typing rules would label this program as ill-typed.

None of these problems arise in T PC, which considers the above two programs as type-correct, since they do not entail ill-typed atoms. Actually, these can also be rendered type-correct due to the syntactic approaches if we replace p and q by p′ and q′, declared as p⟨all/ ⟩ and q⟨all/ ⟩, and define p′(X) ⟵ p(X) and q′(X) ⟵ q(X). However, this way of circumventing type-checking is hardly an elegant solution to the problem of heterogeneous set intersection and set difference.

With all the merits and demerits of the two major points of view discussed above, it is intriguing to see if there exists a reasonable notion of type-correctness that combines the benefits of both approaches. Some of the problems with the notion of type correctness in T PC, such as the one with (3), can be easily rectified; other deficiencies are harder to eliminate, e.g., the problem in (4).

6 Semantics of Type Inference

Type inference is a procedure that determines the “most appropriate” type declaration for a program. Compared to type checking, which works only when complete type information is given, type inference is more widely applicable since it can be used to extract typing from programs with partial type information or none at all. In logic programming, type inference can be used as a debugging tool as follows: Once the typing is inferred, the programmer can examine it and see if this is what was intended. If unwanted types are detected, the programmer may suspect a program error. For instance, consider the following defective program that is supposed to sum up elements of a list:

\begin{matrix}sum(cons(X, nil), X) ⟵ X : int \\ sum(cons(X, L), Z′) ⟵ sum(Z, L) & plus(X, Z, Z′). \end{matrix}

The mistake here appears to be in the second rule, where the arguments in sum(Z, L) are misplaced. Assuming that only the trivial TDs are associated with sum, the programmer would expect the following signature: { sum⟨list(int), int/∅ → ∅⟩ }. However, the inferred typing can only be { sum⟨all, int/∅ → ∅⟩ }, because in the rule-body L is bound to arguments of type int instead of list(int) and therefore cons(X, L) is not of the type list(int) (all is the type of everything, defined in (1) ). This discrepancy may alert the programmer to the mistake in the second rule.

Type inference can also be used for query optimization, e.g., to detect that certain goals are bound to fail. For instance, suppose the set of signatures inferred from a program is { husband⟨man, woman/∅ → ∅⟩ }. The system could then immediately reject queries such as ?− husband(mary, X) and inform the user that the first argument of husband is expected to be a man (assuming mary : man does not logically follow from the program).

Type inference algorithms usually need the following input: a class-hierarchy declaration, Isa, a data definition, Data, and a type-dependency declaration, Td. A type-dependencies declaration (abbr., a TD-declaration) is a mapping that assigns to each predicate that occurs in Data a set of TDs. The objective of type inference is to infer a set of signatures Type for predicates appearing in Data, such that P =^{def} Isa ∪ Data ∪ Type is a well-typed program, where every signature in Type is of the form p⟨t⃗/Td(p)⟩ (i.e., the TDs in each such signature must be precisely the ones that are associated to p via Td). Furthermore, Type must be the strongest type declaration for which P is well-typed. The latter requirement is important, for otherwise signatures like sum⟨all, all/∅ → ∅⟩ will always do the job.

Given a pair of type declarations T and T′, we say that T is stronger than T′ modulo a classhierarchy Isa, denoted T ≥ T′ mod Isa, if and only if:

• For every data definition Data, whenever Isa ∪ Data ∪ T is well-typed, Isa ∪ Data ∪ T′ is also well-typed.

A type declaration T is nonredundant (with respect to Isa)if there is no T′ such that T′ ⊂ T and T and T′ are equally strong (i.e., T ≥ T′ mod Isa and T′ ≥ T mod Isa).

Example 6.1 TDs play a crucial role in determining the condition T ≥ T′, as shown next. Let

T : {p⟨student, student/∅ → ∅⟩, \atop p⟨employee, employee/∅ → ∅⟩} T′ : p⟨student, student/∅ → ∅⟩

T′′ : {p⟨student, student/∅ → ω⟩, \atop p⟨employee, employee/∅ → ω⟩} T′′′ : p⟨student, student/∅ → ω⟩.

Suppose that the Isa-part is empty here. Then every data tuple that is type-compatible with T′ is also compatible with T and thus T′ ≥ T. However, with different TDs the situation may reverse itself. For instance, the tuples that are compatible with T′′ are now also compatible with T′′′, hence T′′ ≥ T′′′. □

The following lemma gives a sufficient condition for one signature to be stronger than another:

Lemma 6.1 Let T_{1} and T_{2} be collections of signatures that associate each predicate (occurring in these signatures) with exactly one TD (the TD may be different for different predicates, though). Then T_{1} ≥ T_{2} mod Isa if the following conditions hold:

1. For every ground instance p⟨t_{1}, ..., t_{n}/α → β⟩ of a signature in T_{1}, there is a ground instance p⟨t′_{1}, ..., t′_{n}/α → β⟩ of some signature in T_{2}, such that Isa ⊧ t_{i} : t′_{i}, for i = 1, ..., n; and

2. For every ground instance p⟨t′_{1}, ..., t′_{n}/α → β⟩ of a signature in T_{2}, if β − α is non-empty then there is a ground instance p⟨t_{1}, ..., t_{n}/α → β⟩ of a signature in T_{1}, such that Isa ⊧ t′_{i} : t_{i}, for all i ∈ α, and Isa ⊧ t_{j} : t′_{j}, for all j ∈ β − α.

Proof: It easily follows from the definitions that for every ground data atom A, if Isa ∪ {A} ∪ T_{1} is well-typed, then Isa ∪ {A} ∪ T_{2} is also well-typed. Hence T_{1} ≥ T_{2} mod Isa. □

It should be noted that the user does not always have to supply the type-dependency declaration Td. In extreme cases, the system can assume all TDs to be trivial (e.g., ∅ → ∅, ω → ∅) or, alternatively, the strongest ones (i.e., ∅ → ω). For instance, Mishra [Mis84] and Xu and Warren [XW88, Xu89, XW90] implicitly assume all type dependencies to be trivial. User-supplied TDs may improve the accuracy of type inference algorithms, for in case of trivial TDs too many signatures may be inferred, leading to information glut. In contrast, if only the strongest TDs ∅ → ω are considered, too general signatures are likely to be inferred, which may not be informative enough.

The user can further control type inference by supplying a set of ground terms as a type base. The type inference procedure will then look only for those signatures whose type-names are drawn from the type base. There are two reasons to supply user-defined type base. One is to guide type inference towards returning more informative answers. The other is to improve the speed of type inference by considering a relatively small type base.

The semantics of type inference can be understood as a form of abductive reasoning. Given a quadruple ⟨Isa, Data, Td, Base⟩, where Isa is a class declaration, Data is a data definition, Td is a TD-declaration, and Base is a type base, an ideal inferred type declaration is a type declaration Type such that

• Isa ∪ Data ∪ Type is a well-typed program; • Type is a set of signatures that mention only the type-names appearing in Base;

• For each signature p⟨T_{1}, ..., T_{n}/Γ⟩ in Type, Γ is the set of signatures associated with p via Td;

• Type is a strongest (modulo Isa) nonredundant type declaration satisfying the above conditions.

Despite its name, an ideal inferred type declaration may not be unique. For instance, suppose Isa consists of the following rules:

\begin{matrix}X : c ⟵ X : a & X : b & X ≠ a & X ≠ b & X : a ⟵ X : c & X : d & X ≠ c & X ≠ d \\ X : d ⟵ X : a & X : b & X ≠ a & X ≠ b & X : b ⟵ X : c & X : d & X ≠ c & X ≠ d. \end{matrix}

This means that intersection of the extensions of classes a and b coincides with that of the extensions of c and d. It is easy to see that the sets of signatures S_{1} = {p⟨a/∅ → ω⟩, p⟨b/∅ → ω⟩} and S_{2} = {p⟨c/∅ → ω⟩, p⟨d/∅ → ω⟩} are equally strong modulo Isa and none of them is redundant. Therefore, if S_{1} is an ideal inferred type for some program then so is S_{2}, provided that Base contains a, b, c, and d.

Let Data be a data definition. A naive type inference algorithm for ⟨Isa, Data, Td, Base⟩, where Td assigns a trivial TD to every predicate, works as follows:

1. [Evaluate]: Use the bottom-up evaluation method to compute the canonic model W of Data.

2. [Transform]: For each data atom p(s_{1}, ..., s_{n}) in W, find a minimal supertype t_{i} of s_{i} in Base, i = 1, ..., n; set V := V ∪ {p⟨t_{1}, ..., t_{n}/∅ → ∅⟩}.

3. [Postprocess]: Remove redundancies in V. Return V as the inferred type declaration.

Unfortunately, this algorithm may not stop if W is infinite. However, we can approximate W using a particular group of type bases with finite domains. For instance, for the type bases Π_{n} in [XW88] that contain terms up to a certain depth, the termination of the algorithm is guaranteed. We will discuss the type bases Π_{n} and the type inference algorithm of [XW88] in Section 9.3.

The above type inference can be combined with partial type declarations, which works like this: The user declares signatures for some of the predicates (possibly none, if “pure” type inference is desired). Then the system checks types of the predicates whose signatures are declared in the partial type declaration, and infers signatures for predicates whose signatures are not mentioned.

More specificly, let Type_{init} be a partial type declaration for a program P. For every predicate p that appears in P but not in Type_{init}, a signature p⟨all, ..., all/∅ → ∅⟩ is added to Type_{init}, where all is the largest type, defined by the clause X : all. Such signatures impose no restriction on p. Then the system uses a type-checking procedure to decide whether the program P is well-typed under the augmented type declaration. If P is well-typed, then the predicates in Type_{init} satisfy the partial type declaration. At the last stage, a type-inference procedure is applied to the program, as in pure type-inference. Finally, signatures for the predicates that are not mentioned in Type_{init} are reported to the user.

7 Separating Individuals from Classes

So far, T PC did not distinguish between classes and individuals, and any individual (e.g., john) was also regarded as a class that contains at least itself as an instance (since, e.g., john : john is a tautology). However, it is often useful to distinguish classes from individuals.

First, users do not expect class names to appear among answers to the “ordinary” queries. Second, separating class names from individuals is even more important for the typing; otherwise certain parametric signatures may become too strong. Consider the following signature:

same type⟨X, X/1 → 2; 2 → 1⟩,  (5)

that declares both arguments of same type to have precisely the same type or, equivalently, to be instances of the same set of classes. However, if individuals are also classes then this would be clearly too strong a condition. For instance, same type(1, 2) is not well-typed relatively to the above signature, since the variable X will range over 1 and 2 as well, and hence 1 would have to belong to the class 2 and vice versa. This implies that 1 = 2 in all untyped models. Since in the standard interpretation of integers 1 ≠ 2, same type(1, 2) would be incompatible with (5). In fact, it is easy to see that only the atoms of the form same type(t, t), where t is a term, are compatible with (5).

There are several different ways to deal with this problem. In our opinion, the most elegant solution consists in splitting the set of T PC terms into two different sorts: classes and individuals. Formally, this is done as follows. All variables and function symbols (and constants as a special case) can be split into three categories: those whose range of values is the sort of individuals, the sort of classes, and those whose range is the universal sort (the union of the first two sorts). There is no need to impose sorts on the arguments of function and predicate symbols. Syntacticly, we can distinguish the class-valued symbols by attaching to them the prefix “♯”, e.g., ♯X, ♯union; the individuals-valued symbols can be prefixed with “!”, e.g., !Y, !cons; and the symbols whose range is universal will begin with a letter. Then, we postulate that a term belongs to a class-sort, the sort of individuals, or the universal sort if and only if its outermost symbol (a function symbol, a constant, or a variable) is prefixed with “♯”, “!”, or starts with a letter, respectively.

The next step would be to restrict the language in such a way that

• The terms in the signature atoms must be class-terms (i.e., their outermost symbol must be prefixed with a “♯”-sign);

• For an is-a term, Cl : SupCl, we may require SupCl to be a class-term (i.e., it should really be ♯SupCl).

These restrictions ensure that individuals will not be used as classes and that signatures do not meddle with individuals. For instance, (5) above will not be a syntacticly correct formula; in the sorted version of T PC, a correct signature corresponding to (5) would be

same type⟨♯X, ♯X/1 → 2; 2 → 1⟩,

which imposes the desired typing constraint.

Semantics of the sorted version of T PC is a simple modification of the model theory given in Section 2.2. In a nutshell, domains of semantic structures now become disjoint unions of the subdomains for classes and individuals, respectively: U = ♯U ⊎ !U, where ⊎ denotes the operator of disjoint union of sets. Function symbols of the form ♯f (or !f) are now interpreted by the maps U^{k} ⟼ ♯U (resp., U^{k} ⟼!U). Symbols starting with a letter are interpreted by functions U^{k} ⟼ U. Notice that since arguments of function symbols are not sorted, the domain of these functions is U^{k}, not ♯U^{k} or !U^{k}. Another change involves the definition of variable-assignments. An assignment ν now maps variables of the form ♯X into ♯U and those of the form !X to !U. The details are straightforward and are left to the reader.

The proof theory does not require many changes either, except that the definition of substitutions must be modified to preserve sorts, i.e., substitutions should map the “♯”-variables (or “!”-variables) to “♯”-terms (resp., “!”-terms) only; unrestricted variables can be mapped into any term.

8 Evaluation

Query evaluation in T PC is based on the proof theory of Section 4. First, note that in terms of the proof theory, the purpose of type checking is precisely that of the elimination (or, at least, reducing) of the need in applying the well-typing inference rules of Figure 1. Indeed, once the user has type-checked his program using one of the schemes discussed earlier (pure type-checking, pure type-inference, or type inference under partial type declarations), the use of the well-typing rules is redundant, since all atomic formulae entailed by this program will be guaranteed to conform to the declared (or inferred) typing.

For type-correct programs it can be shown that a T PC analogue of the SLD-resolution [Llo87] is sound and complete for Horn programs. Similarly, SLDNF-resolution can be defined and the corresponding classical results carry over to T PC programs.

9 Case Study

9.1 Syntactic Approaches to Type Checking

Majority of the approaches to type checking in logic programming (e.g., [MO84, DH88, Smo88, Fru89, YFS90, Jac90, HT90]) can be classified as syntactic. The notion of type-correctness is established via a set of well-typing rules, defined inductively on the syntactic structure of formulae. Consider first Mycroft-O’Keefe’s type checking system [MO84]. Their well-typing rules are derived from the slogan that “well-typed programs do not go wrong”, coined in by Milner [Mil78]. By “not going wrong” in [MO84] is meant that subgoals are not called with bindings that disagree with the declared typing of the corresponding predicates. Although this principle may be appropriate in functional programming, it cannot be fully applied to logic programs since, in fact, logic programs never go wrong in the logical sense. Even if a subgoal with “wrong” arguments is generated, it is discarded later because of the subsequent mismatch with the database. This is different from functional programming where illtyped input may cause run-time errors because functions are usually undefined outside their declared argument-types. Consider a variation on the program (3) in Section 5.5 that does not involve subtyping and therefore can be represented in Mycroft-O’Keefe’s system:

\begin{matrix}p⟨string/∅ → ∅⟩ & p(“abc”) \\ p⟨int/∅ → ∅⟩ & p(1) \\ q⟨int/∅ → ∅⟩ & q(1). \end{matrix}  (6)

The typing for p says that its arguments are either of the type string or int; q’s arguments are integers only. According to the “not-going-wrong” condition, the query ?− p(Z) & q(Z) is ill-typed since it leads to an ill-typed subgoal ?− q(“abc”). On the other hand, during the course of the top-down evaluation, the subgoal ?− q(“abc”) is discarded immediately, and only the well-typed answer Z = 1 is returned. What this effectively means is that an innocent query that asks for the intersection of two heterogeneous sets (like p and q above) is illegitimate according to [MO84]. Dietrich and Hagl [DH88] and Jacobs [Jac90] have a similar problem if p is typed as p⟨all/∅ → ∅⟩. Hence, the well-typing conditions in [MO84, DH88, Jac90] are too restrictive. It is easy to see that in T PC the above program is well-typed.

Furthermore, the original approach in [MO84] has no model-theoretic semantics. As a result, some confusion may arise if the typed logic programs are interpreted naively. For instance, the program

\begin{matrix}p⟨int/∅ → ∅⟩ \\ p(X) \end{matrix}  (7)

is well-typed according to [MO84] because for any well-typed query, its top-down evaluation generates only well-typed subgoals. However, this program logically entails ill-typed atoms, such as p(“abc”) (assuming “abc” occurs somewhere else in the program), which suggests that (7) is going to misbehave under bottom-up evaluation.

The recent work by Reddy [Red91] rectifies the problem by reconstructing Mycroft-O’Keefe’s approach on the basis of the many-sorted algebra [GTW78]. In particular, predicate p in (7) would have the sort int and so will the variable X. As a result, p(X) would no longer generate ill-typed atoms and (7) becomes equivalent to the following well-typed T PC program:

\begin{matrix}p⟨int/∅ → ∅⟩ \\ p(X) ⟵ X : int \end{matrix}  (8)

The program (8) is called the one-sorted form of (7). There is a standard procedure to convert sorted programs into the one-sorted form (see [End72, page 279]). The following theorem establishes a correspondence between the well-typed programs of [MO84] (in Reddy’s reconstruction) and those of T PC.

Theorem 9.1 Let P be a well-typed program with respect to a type assignment Σ in the sense of Mycroft-O’Keefe-Reddy. Let P^{∗} be the one-sorted version of P. Then there is an is-a hierarchy declaration Isa and a type declaration Type corresponding to Σ, such that Isa ∪ Type ∪ P^{∗} is welltyped in T PC.

Mycroft-O’Keefe’s type system can be extended to support inclusion polymorphism using the idea of parametric order-sorted logic. Such extensions are described in [Smo88] and [HT90]. Results similar to Theorem 9.1 also hold about the relationship of these extensions to T PC.

9.2 Mishra’s Type Inference System

Mishra [Mis84] proposed an inference-based type system for Prolog, based on the idea of automatic type inference in ML. This type system is able to infer typings for all predicates in any logic program without explicit type declarations. The inferred type declarations are represented as regular trees and satisfy the well-typing principle according to which the inferred typing must cover all atoms that can be successfully derived from the program. This principle is widely accepted in the logic programming community, and several other researchers [Zob87, Azz88, PR89] further extended Mishra’s work by proposing different type inference algorithms. In this subsection we explain how T PC captures the notion of Mishra’s regular trees and show that his well-typing principle is consistent with the notion of type-correctness in T PC. In particular, this means that the type-inference algorithms developed in [Mis84, Zob87, Azz88, PR89] can be used in T PC, provided that the type-base is restricted to regular trees.

Example 9.1 Consider the standard Prolog program for append:

\begin{matrix}append(nil, K, K) \\ append(cons(X, L), M, cons(X, N)) ⟵ append(L, M, N). \end{matrix}

The typing computed by Mishra’s algorithm would be

T (append) = T_{1}♯T_{2}♯T_{3}, where T_{1} = Z! nil + cons(X, Z)
T_{2} = Y
T_{3} = Z! Y + cons(X, Z).

Here, T_{1}, T_{2}, and T_{3} are regular trees that describe the types of each of the three arguments of append; “♯” is the argument separator. Regular trees are extensions of the first-order terms with the addition of the union operator “+” and the fixpoint operator “!”. The former is used to construct unions of types, while the latter is a means of creation of recursive types. Each regular tree T is associated with a set of ground terms, called instances of T. For example, Z! nil + cons(int, Z) is associated with the terms nil, cons(1, nil), cons(2, cons(1, nil)), and so on.

The typing for append, T_{1}♯T_{2}♯T_{3}, is the Cartesian product of the sets denoted by T_{1}, T_{2} and T_{3}. It covers all append-tuples that can be successfully derived from the program. That is, if append(s_{1}, s_{2}, s_{3}) is derived then the tuple ⟨s_{1}, s_{2}, s_{3}⟩ must be an instance of T_{1}♯T_{2}♯T_{3}. □

Regular trees can be represented in T PC as follows. First, we transform each regular tree t into a first-order term, tr(t). New function symbols—union, fixpt, and seed—are used to express the union and the fixpoint operators.

• For a constant c, tr(c) =^{def} c.

• For a regular tree f(t_{1}, ..., t_{n}), tr(f(t_{1}, ..., t_{n})) =^{def} f(tr(t_{1}), ..., tr(t_{n})), where f is a function symbol.

• For a union-expression r + s, tr(r + s) =^{def} union(tr(r), tr(s)).

• For a fixpoint-expression τ of the form Z! p + q(Z), where q(Z) is a regular tree involving a variable Z, tr(τ) =^{def} fixpt(tr(p), tr(q(seed)).

The instances of regular trees can be defined using class-hierarchy declarations. Given a set of regular trees T, the class-hierarchy declaration corresponding to T consists of the following rules:

(1) For every function symbol f:

f(X_{1}, ..., X_{n}) : f(Y_{1}, ..., Y_{n}) ⟵ X_{1} : Y_{1} & … & X_{n} : Y_{n}.

(2) For the union operator:

{X : union(X, Y) \atop Y : union(X, Y).}

(3) For every fixpoint expression Z! p + q(Z) in T:

{tr(p) : fixpt(tr(p), tr(q(seed))) \atop tr(q(Z)) : fixpt(tr(p), tr(q(seed))) ⟵ Z : fixpt(tr(p) & tr(q(seed))).}

Rule (1) here says that every function symbol is monotone with respect to types. The second rule says that for every a and b, union(a, b) contains (in the least model) precisely the instances of the classes a and b. The last rule defines instances of the class tr(τ), the translation of the fixpoint expression, by mimicing Mishra’s semantics for such expressions.

With the above translation, we can transplant Mishra’s type inference on T PC. Let P be a data definition in question. For every predicate p in P, if the typing inferred by Mishra’s algorithm is τ_{1}♯ ⋯ ♯τ_{n}, then let Isa_{P} contain the class-hierarchy declaration that corresponds to τ_{1}, ..., τ_{n} and let Type_{P} contain the signature p⟨tr(τ_{1}), ..., tr(τ_{n})/∅ → ∅⟩. Then Isa_{P} and Type_{P} define the typing for p in T PC that corresponds to the typing generated by Mishra’s algorithm.

Example 9.2 Consider the logic program of Example 9.1. The signature for append generated by Mishra’s algorithm (in the T PC notation) would be

append⟨fixpt(nil, cons(X, seed)), Y, fixpt(Y, cons(X, seed))/∅ → ∅⟩.  (9)

The corresponding class-hierarchy declaration Isa_{P} in T PC is

cons(X_{1}, X_{2}) : cons(Y_{1}, Y_{2}) ⟵ X_{1} : Y_{1} & X_{2} : Y_{2}
Y : fixpt(Y, cons(X, seed))
cons(Y, Z) : fixpt(Y, cons(X, seed)) ⟵ Z : fixpt(Y, cons(X, seed)).

It is worth comparing (9) with a much more natural typing append⟨list(T), list(T), list(T)/1, 2 → 3; 3 → 1, 2⟩ of Example 5.6 or even with append⟨list(all), list(all), list(all)/∅ → ∅⟩ that would have been derived by the naive algorithm described in Section 6. □

Theorem 9.2 Consider a logic program P such that Isa_{P} and Type_{P} are constructed as explained above. Then Isa_{P} ∪ Type_{P} ∪ P is a well-typed program in T PC.

It should be noted, however, that although the typing Type_{P} produced by Mishra’s algorithm is a legal inferred typing for P in T PC, it is not the strongest one. For instance, for append, the typing append⟨list(all), list(all), list(all)/∅ → ∅⟩ is stronger than (9).

9.3 Xu-Warren’s Type Inference [XW88, Xu89]

In [XW88], the typing of a program is defined via typed interpretations. Given a type base Π, a typed interpretation A under Π is a semantic structure where terms are interpreted by the types of Π, and predicates are interpreted as relations over Π. Given a Horn clause program P, the typing of P is defined as the minimum typed model of P under Π.

The type-inference algorithm of [XW88] correctly (relatively to their semantics) finds the minimum typed model of any Horn clause program. Unfortunately, no such algorithm can terminate in all cases. As a practical solution, Xu and Warren consider a particular group of type bases, Π_{n}, for which their type inference algorithm always terminates. Given a natural number n, Π_{n} consists of a finite set of truncated terms, where for every function symbol f truncation occurs below each n-th repeated nested occurrence of f. Subterms that are removed by truncation are replaced by the special symbol “∗”. For instance, if the language L has one constant a, a unary functor f, and a 2-ary functor g, then the type base Π_{1} would be

a, f(a), f(f(∗)),
f(g(a, a)), f(g(a, f(∗))), f(g(a, g(∗, ∗))),
f(g(f(∗), a)), f(g(g(∗, ∗), a)),
. . . . . . . . .

A truncated term, say, f(g(a, f(∗))) represents the set {f(g(a, f(t)))| for all ground terms t of L}. It is shown in [XW88] that their type inference algorithm terminates for every type base Π_{n}. As an example, consider the following program P that subtracts 1 from its first argument:

\begin{matrix}sub1(succ(zero), zero) \\ sub1(succ(X), succ(Y)) ⟵ sub1(X, Y). \end{matrix}

Let the type base be Π_{1}. The type declaration inferred by the algorithm in [XW88] (represented in the T PC-notation) is:

\begin{matrix}sub1⟨succ(zero), zero/∅ → ∅⟩ \\ sub1⟨succ(succ(all)), succ(succ(all))/∅ → ∅⟩, \end{matrix}

where “all” is the class of all things defined in (1).

For each truncated term t of [XW88], its T PC counterpart is obtained from t by replacing each occurrence of “∗” by all. The class-hierarchy declaration corresponding to Π_{n} consists of the declaration for all as the class of all things (X : all) and of the monotonicity condition

f(X_{1},…, X_{k}) : f(Y_{1},…, Y_{k}) ⟵ X_{1} : Y_{1} & … & X_{k} : Y_{k}

per each k-ary function symbol f, k > 0. The type-dependency declaration corresponding to the formalism of [XW88] is the simplest possible one: every signature is tagged with a trivial TD.

Theorem 9.3 Let P be a program and Type be the type declaration for P generated by Xu-Warren’s type inference algorithm. Let Isa be the class-hierarchy declaration obtained from Π_{n} as explained above. Then Isa ∪ Type ∪ P is a well-typed T PC-program.

In [XW90], Xu and Warren extended the framework of [XW88] and introduced type declarations, making it possible to do type checking together with type inference, as in Section 6. Unfortunately, in the presence of inclusion polymorphism the extended theory is not completely adequate, for it is not sufficiently strong and lets certain ill-typed programs to slip through:

p(X) ⇝ man(X)  p(X) ⟵ q(X)
q(X) ⇝ person(X)  q(mary)
q(john).

Here, the first pair of clauses declares p to be a set of men while q is a set of persons. Intuitively, this program is ill-typed because the query ?− p(Y) returns mary as one of the answers. This contradicts the declaration of p as a set of men (assuming mary is not a man). It is not clear whether an adequate solution to the problem of type declarations can be found within the framework of partial interpretations developed in [XW88, XW90].

10 Conclusion

We presented a new logic, typed predicate calculus (T PC), that provides a natural framework for representing logic programs with type declaration and for reasoning about type-correctness of these programs. The logic naturally supports inclusion, parametric, and ad hoc polymorphism. Type declarations in T PC are more expressive than in [MO84, Xu89, Jac90] and other works, since multiple signatures and functional-style type-enforcement patterns, can be used to capture polymorphic types.

We combined the benefits of declaration-based and inference-based approaches, and showed how type inference under partial type declarations fits in our framework. Most importantly, we gave precise model-theoretic meaning to the notion of type-correctness, independent of any specific type-checking or type-inference procedure. This enables us to accommodate many different type-checking and typeinference algorithms that suit in different situations. As an illustration, we showed how the formalisms of [MO84, Smo88, HT90, Mis84, XW88, Xu89] can be accounted for in our framework. Finally, we note that all results in this paper can be easily extended to typing HiLog [CKW89a, CKW89b]—a recently proposed higher-order logic programming language. Acknowledgements: We thank Catriel Beeri, Thom Fruehwirth, Dean Jacobs, Prateek Mishra, Uday Reddy, David Warren and Jiyang Xu for their valuable suggestions and illuminating discussions.

References

[AV88] S. Abiteboul and V. Vianu. Procedural and declarative database update languages. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 240–250, 1988.

[Azz88] H. Azzoune. Type inference in Prolog. In Proceedings of International Conference on Automated Deduction, pages 258–277, 1988.

[BB79] C. Beeri and P.A. Bernstein. Computational problems related to the design of normal form relational schemes. ACM Transactions on Database Systems, 4(1):30–59, March 1979.

[Bru82] M. Bruynooghe. Adding redundancy to obtain more reliable and more readable Prolog programs. In Proceedings of the First International Logic Programming Conference, pages 129–133, Marseille, France, 1982.

[CKW89a] W. Chen, M. Kifer, and D.S. Warren. HiLog: A first-order semantics for higher-order logic programming constructs. In Proceedings of the North American Conference on Logic Programming, October 1989.

[CKW89b] W. Chen, M. Kifer, and D.S. Warren. HiLog as a platform for database programming languages (or why predicate calculus is not enough). In R. Hull, R. Morrison, and D. Stemple, editors, Database Programming Languages, pages 315–329, Morgan-Kaufmann, June 1989.

[DH88] R. Dietrich and F. Hagl. A polymorphic type system with subtypes for Prolog. In Proceedings of the 2-nd European Symp. on Programming, Lecture Notes in Computer Science 300, pages 79–93, Springer Verlag, 1988.

[DW86] S.K. Debray and D.S. Warren. Automatic mode inference for Prolog programs. In IEEE Symposium on Logic Programming, 1986.

[End72] H.B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.

[Fru88] T. Fruehwirth. Type inference by program transformation and partial evaluation. In IEEE Intl. Conf. on Computer Languages, pages 347–355, Miami Beach, FL, 1988.

[Fru89] T. Fruehwirth. Polymorphic type checking for Prolog in HiLog. In 6th Israel Conference on Artificial Intelligence and Computer Vision, Tel Aviv, Israel, 1989.

[GL88] M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In Logic Programming: Proceedings of the Fifth Conference and Symposium, pages 1070–1080, 1988.

[GRS88] A. Van Gelder, K.A. Ross, and J.S. Schlipf. The well-founded semantics for general logic programs. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 221–230, 1988.

[GTW78] J.A. Goguen, J.W. Thatcher, and E.W. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In R.T. Yeh, editor, Current Trends in Programming Methodology, pages 80–149, Prentice-Hall, 1978.

[HT90] P. Hill and R. Topor. A semantics for typed logic programs. 1990. manuscript.

[Jac90] D. Jacobs. Type declarations as subtype constraints in logic programming. In Proceedings of the ACM SIGPLAN-90 Conference on Programming Language Design and Implementation, pages 165–173, June 1990.

[KH85] T. Kanamori and K. Horiuchi. Type inference in Prolog and its application. In Intl. Joint Conference on Artificial Intelligence, pages 704–707, 1985.

[KL89] M. Kifer and G. Lausen. F-logic: A higher-order language for reasoning about objects, inheritance and schema. In Proceedings of the ACM SIGMOD Conference on Management of Data, pages 134–146, 1989.

[KLW90] M. Kifer, G. Lausen, and J. Wu. Logical Foundations of Object-Oriented and Frame-Based Languages. Technical Report 90/14, Department of Computer Science, SUNY at Stony Brook, July 1990.

[KP88] P.G. Kolaitis and C.H. Papadimitriou. Why not negation by fixpoint. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 231–239, 1988.

[Llo87] J.W. Lloyd. Foundations of Logic Programming (Second Edition). Springer Verlag, 1987.

[Man74] Z. Manna. Mathematical Theory of Computation. McGraw-Hill Book Co., 1974.

[Mil78] R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348–375, 1978.

[Mis84] P. Mishra. Towards a theory of types in Prolog. In IEEE Symposium on Logic Programming, pages 289–298, 1984.

[MO84] A. Mycroft and R.A. O’Keefe. A polymorphic type system for Prolog. Artificial Intelligence, 23:295–307, 1984.

[MR85] P. Mishra and U.S. Reddy. Declaration-free type checking. In ACM Symposium on Principles of Programming Languages, pages 7–21, 1985.

[PR89] C. Pyo and U.S. Reddy. Inference of polymorphic types for logic programs. In Proceedings of the North American Conference on Logic Programming, pages 1115–1132, 1989.

[Prz88] T.C. Przymusinski. On the declarative semantics of deductive databases and logic programs. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 193–216, Morgan Kaufmann, Los Altos, CA, 1988.

[Red88] U.S. Reddy. Notions of polymorphism for predicate logic programs. In Intl. Conference on Logic Programming, pages (addendum, distributed at conference) 17–34, MIT Press, August 1988. also to appear in J. Logic Programming.

[Red91] U. Reddy. A perspective on types for logic programs. In F. Pfenning, editor, Types in Logic Programming, MIT Press, 1991. to appear.

[Smo88] G. Smolka. Logic Programming with Polymorphically Order-Sorted Types. Technical Report ILOG Report 55, IBM Deutchland GmbH, 1988.

[Ull88] J.F. Ullman. Principles of Database and Knowledge-Base Systems, Volume 1. Computer Science Press, 1988.

[Van89] A. Van Gelder. The alternating fixpoint of logic programs with negation. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of database Systems, pages 1–10, 1989.

[War77] D.H.D. Warren. Implementing Prolog – Compiling Predicate Logic Programs. Technical Report 39 and 40, Dept. of Artificial Intelligence, University of Edinburgh, 1977.

[Xu89] J. Xu. A Theory of Types and Type Inference in Logic Programming Languages. PhD thesis, SUNY at Stony Brook, 1989.

[XW88] J. Xu and D.S. Warren. A type inference system for Prolog. In Intl. Conference on Logic Programming, pages 604–619, 1988.

[XW90] J. Xu and D.S. Warren. Semantics of types in logic programming. 1990. manuscript.

[YFS90] E. Yardeni, T. Fruehwirth, and E. Shapiro. Polymorphically typed logic programs. 1990. manuscript.

[YS87] E. Yardeni and E. Shapiro. A type system for logic programs. In E. Shapiro, editor, Concurrent Prolog, MIT Press, 1987.

[Zob87] J. Zobel. Derivation of polymorphic types for Prolog programs. In Proceedings of the Fourth International Logic Programming Conference, Australia, 1987.