[To appear in: L. Sterling (ed): Proceedings of the Twelfth International Conference on Logic Programming - ICLP’95, Tokyo, Japan. MIT Press, 1995.]

Type inferencing for polymorphic order-sorted logic programs

Christoph Beierle FernUniversität Hagen Fachbereich Informatik Bahnhofstr. 48 D-58084 Hagen, Germany

christoph.beierle@fernuni-hagen.de

Abstract

The purpose of this paper is to study the problem of complete type inferencing for polymorphic order-sorted logic programs. We show that previous approaches are incomplete even if one does not employ the full power of the used type systems. We present a complete type inferencing algorithm that covers the polymorphic order-sorted types in PROTOS-L, a logic programming language that allows for polymorphism as in ML and for hierarchically structured monomorphic types.

1 Introduction

It has often been argued that the lack of types in logic programming is a disadvantage from a software engineering point of view. There are now many different approaches for introducing types in logic programming, for an overview see [11]. In this paper we consider polymorphic types combined with order-sorted types, i.e. types which are hierarchically ordered. Polymorphism for logic programming was first suggested in [10]; for extensions of this approach to order-sorted types see [4], [6], [13], [8], [3].

In all of these approaches, a precondition for the well-definedness of the semantics of a typed logic program is that the program is well-typed. Thus, (static) type checking of programs is a precondition for the semantics to work properly, and usually type checking comes with the type inferencing done automatically to at least some degree. The purpose of this paper is to study the problem of complete type inferencing for polymorphic ordersorted logic programs. However, among the different approaches to type inferencing in logic programming (e.g. [9, 15, 14, 13, 8]) there are only a few dealing with type inferencing in an polymorphic order-sorted setting. Of the cited work, only [13] and [8] explicitly address this topic. However, there are problems with both approaches. As is already pointed out in [12, 13] the type inferencing algorithm presented there is incomplete. We will show in this paper that the type inferencing algorithm in [8] is also incomplete. Moreover, both problems still remain even if we consider only typed programs that do not exploit the full power of the respective typing systems. Whereas TEL [12, 13] allows explicit subtype relationships between polymorphic types having different arities (e.g. list(α) ≤ my type(α, β)), in [8] subtype relationships between polymorphic type are allowed only between type constructors of the same arity. The type system of PROTOS-L [3, 1] was derived form TEL by disallowing any explicit subtype relationship between polymorphic type constructors. The type inferencing algorithms of both [12, 13] and [8] are also incomplete for the PROTOS-L type system.

The type inferencing algorithm we present here covers the type system of PROTOS-L and can easily be extended to the type system of [8].

The paper is organized as follows: In the following section, we illustrate the special difficulties arising in type inferencing for polymorphic ordersorted logic programs and show the problems with previous approaches. In Section 3, polymorphic order-sorted types and the notion of well-typed programs are precisely defined as a basis for the type inferencing algorithm T I presented in Section 4, while Section 5 contains the corresponding correctness and completeness results.

2 Motivation and related work

The combination of order-sortedness and polymorphism causes some special difficulties. Having already derived different types for different occurrences of the same variable within a clause, the type inferencer must then “typeunify” these different types in order to get a consistent typing for the clause. If this involves the instantiation of a type variable there may be different choices from hierarchically ordered types.

Example 1 As an example, consider the type hierarchy

[figure: negint; int; nat]

and the usual polymorphic type constructors list(α) and pair(α, β). From a polymorphic predicate declaration p : list(α) and the subgoals

      ...  X = 1 ∧ p([X|L]) ...

we might derive the simultaneous type requirements

      X:nat    X:α  L:list(α)

since 1:nat, and the type inferencer could (prematurely) instantiate α to nat. However, for the extended subgoal sequence

      ...  X = 1 ∧ p([X|L]) ∧ Y = -1 ∧ p([Y|L]) ...

this type substitution is not possible. The derived type requirements

      X:nat    X:α  L:list(α)    Y:negint    Y:α

are not consistent with the type instantiation α = nat, whereas α could still be instantiated to int. □

Typed logic programming with polymorphically order-sorted types as studied in [13] provides the theoretical foundations for TEL [12]. Given declarations for all predicates and functors, TEL’s type inferencing component infers the types for the variables occurring in a clause. However, as already pointed out in [13], it is incomplete in the sense that it may fail on a clause involving polymorphic predicates although the clause could be well-typed, or that it computes a variable typing that is not most general. Whereas [13] gives examples where another ordering of the literals leads to a successful typing, the following example shows that for no ordering of the literals TEL’s type inferencing algorithm succeeds although there is a well-typing.

Example 2 Consider the types as in Example 1 and a predicate with declaration

      member3:  negint × α × list(α) × β × list(β)

For the goal

      member3(X,2,[X|L],2,[Y|M]) ∧ member3(Y,2,[X|L],2,[Y|M])

as well as for the rearranged goal

      member3(Y,2,[X|L],2,[Y|M]) ∧ member3(X,2,[X|L],2,[Y|M])

TEL’s type inferencing algorithm fails to generate a variable typing. However, there is a most general variable typing

      {X:negint, Y:negint, L:list(int), M:list(int)}

under which both goals are well-typed. □

Another approach to type inferencing for polymorphic order-sorted types is presented in [8]. Its central component is the “most general type unifier” (mgtu) algorithm defined in Theorem 1.1.2 of [8], which is, however, incomplete as the following example shows.

Example 3 Consider the type hierarchy as in Example 1 and a predicate declaration q : pair(α,α). The subgoals

      q(X) ∧ X = mk pair(1,-1)

imply the simultaneous type requirements

      X:pair(α, α)    X:pair(nat,negint)

Then applying the mgtu algorithm to the resulting set of types

      S = {pair(α,α), pair(nat,negint)}

returns a failure although {α/int} is a most general type unifier for S. □

Note that the mgtu algorithm of Theorem 1.1.2 is of central importance for the further development in [8]. Thus, the situation might be repaired by replacing the proof of Theorem 1.1.2 in [8] with a correct version of the mgtu algorithm. Unfortunately, however, no such algorithm exists since there are finite sets of unifiable types that do not have a “most general solution” in the sense of [8]. This is in contrast to Lemma 1.1.10 of [8] which is falsified by the following counter-example.

Example 4 Let the type hierarchy of Example 1 be extended to

[figure: index; expr; negint; int; nat]

For the set of types S = {pair(α,α), pair(nat,negint)} generated by the two type requirements of Example 3 there are 3 different type unifiers ({α/int}, {α/index}, {α/expr}), but none of them is a most general type unifier (in the sense of [8]). □

Since all of the examples above do not use use any subtype relationships between polymorphic types, the type inferencing components of the cited approaches are still incomplete w.r.t. type systems that do not support explicit subtype relationships between polymorphic types. In the following, we will present a complete type inferencing algorithm for such polymorphic order-sorted type systems which is thus applicable to PROTOS-L and which can be extended to the type system of [8].

3 Typed logic programs

3.1 Types

A type alphabet T is a finite set of type symbols each of which comes with an arity ≥ 0. Type symbols with arity 0 are called monomorphic, type symbols with arity strictly greater than 0 are called polymorphic. T_{mono} (resp. T_{poly}) is the set of all monomorphic (resp. polymorphic) type symbols. T_{mono} comes with a partial order ≤; we will assume that (T_{mono}, ≤) has a greatest lower bound glb(s_{1}, s_{2}) for any two elements s_{1} and s_{2} having a lower bound at all (this ensures unitary unification; we will, however, do not deal with unification in this paper). Thus, since T_{mono} is finite also the least upper bound lub(s_{1}, s_{2}) exists provided s_{1} and s_{2} have an upper bound at all.

V_{type} is a set of type variables. T ype is the set of types which are exactly the terms freely generated by the type symbols T over V_{type} in the usual way, i.e.

• every type variable α is a type

• every monomorphic type symbol s (also called type constant) is a type

• if η is a polymorphic type symbol with arity n ≥ 1 and τ_{1}, …, τ_{n} are types, then η(τ_{1}, …, τ_{n}) is a type.

The partial order (T_{mono}, ≤) is extended to a partial order (T ype, ≤) on the set T ype of all types as follows:

• for any type variable α we have α ≤ α

• for any types η(τ_{1}, …, τ_{n}) and η(τ′_{1}, …, τ′_{n}) with n ≥ 1 we have

η(τ_{1}, …, τ_{n}) ≤ η(τ′_{1}, …, τ′_{n})

iff τ_{i} ≤ τ′_{i} for any i ∈ {1, …, n}

Thus, α ≰ β for any α ≠ β and η(…) ≰ η′(…) for any η ≠ η′.

Since types are defined as terms, we can define a type substitution as an ordinary substitution on terms, i.e. as a morphism

ϑ : T ype → T ype

on the set of all type terms whose restriction to the set of type variables is the identity almost everywhere. We will represent type substitutions by

ϑ = {α_{1} ≐ τ_{1}, …, α_{n} ≐ τ_{n}}

where {α_{1}, …, α_{m}} is the domain of ϑ.

\underline{Notation:} In the rest of this paper we assume a fixed, but arbitrary type alphabet. We will use the following (possibly subscripted and dashed) symbols for denoting elements taken from the respective sets:

s  monomorphic type symbol
η  polymorphic type symbol
ξ  monomorphic or polymorphic type symbol
τ  type from T ype
α, β  type variable
ϑ, ρ, σ type substitution

3.2 Polymorphic order-sorted signature

A polymorphic order-sorted signature (over the set T ype of types) is a pair (Func, Pred) with:

• Func is a set of function declarations of the form

f : τ_{1} × … × τ_{n} → τ_{0} with τ_{i} ∈ T ype, n ≥ 0; τ_{o} is of the form ξ(α_{1}, …, α_{m}) with m ≥ 0 and pairwise distinct variables α_{j}, and for any i ∈ {1, …, n} all variables of τ_{i} are contained in {α_{1}, …, α_{m}}.

• Pred is a set of predicate declarations of the form

p : τ_{1} × … × τ_{n} with τ_{i} ∈ T ype , for i ∈ {1, …, n}.

Since we do not consider overloading we require that Func and Pred contain exactly one declaration for every function resp. predicate symbol. Moreover, in order to avoid the “empty set” problem [5] we assume that for any type there is a ground term of that type.

Let Var be an infinite set of variables. When considering from the type declaration of function and predicate symbols just their number of arguments, (untyped) first-order terms, literals, and formulas are freely generated by Func and Pred over Var in the usual way.

3.3 Well-typed Logic Programs

A (type) prefix P (or a variable typing) is a finite set of the form

P = {x_{1} : τ_{1}, …, x_{n} : τ_{n}}

with pairwise distinct variables x_{i}. The set dom(P) = {x_{1}, …, x_{n}} is called the domain of P. For a type substitution ϑ we let ϑ(P) denote the prefix

{x_{1} : ϑ(τ_{1}), …, x_{n} : ϑ(τ_{n})}.

In the following, we use the notation:

P type prefix
x variable from Var
t first order term built in the usual way over Func and Var

A well-typed term of type τ w.r.t. a type prefix P is defined by:

1. If x : τ is in P, then x is a well-typed term of type τ w.r.t. P.

2. If f : τ_{1} ×…×τ_{n} → τ_{o} is the declaration for f, σ is a type substitution, t_{i} is a well-typed term of type τ′_{i} ≤ σ(τ_{i}) w.r.t. P for i ∈ {1, …, n}, then f(t_{1}, …, t_{n}) is a well-typed term of type τ w.r.t. P for τ = σ(τ_{o}).

Likewise, we define well-typed clauses w.r.t. a prefix P:

1. If p : τ_{1} × … × τ_{n} is the declaration for p, σ is a type substitution, t_{i} is a well-typed term of type τ′_{i} ≤ σ(τ_{i}) w.r.t. P for i ∈ {1, …, n}, then p(t_{1}, …, t_{n}) is a well-typed atomic formula w.r.t. P.

2. If F, F_{1}, …, F_{n} are well-typed atomic formulas w.r.t. P then

F ← F_{1} ∧ … ∧ F_{n}.

is a well-typed clause w.r.t. P.

As usual, a logic program Prog is a set of clauses. Prog is well-typed if each of its clauses is well-typed, and a clause is well-typed if it is well-typed w.r.t. some prefix. ^{1}

The problem of type inferencing for logic programs can thus be stated precisely as follows:

1Note that this notion of well-typedness does not ensure the head-condition (the head of a clause must belong to a type that is a variant - rather than an instance - of the head predicate’s declaration). However, only some of the approaches to polymorphic ordersorted logic programming require the head condition (e.g. [10], [13], [8]), but not all of them (e.g. [7]). Once one has established a (most general) well-typing for a clause it is easy to check whether the head condition is satisfied.

• Given a program Prog decide whether Prog is well-typed, i.e. for any of its clauses Cl find a prefix P such that Cl is well-typed w.r.t. P.

As argued in Section 2, there are clauses that do not have a most general well-typing in the sense that any other well-typing can be obtained from it by further instantiation. Therefore, the type inferencing algorithm T I presented in the next section produces a (representation of a) set of welltypings. T I is correct and complete in the following sense: It identifies exactly all clauses that can not be well-typed, and for any well-typing prefix P for a clause Cl it derives a well-typing prefix P′ such that P′ is more general than P, i.e. there is a type substitution ρ such that ρ(P′) = P.

4 Type inferencing

Given a clause

Cl = L_{o} ← L_{1} ∧ … ∧ L_{n}

we must find a prefix P such that for any i = {0, …, n}, L_{i} is a well-typed atomic formula w.r.t. P. The type inferencing procedure T I to be presented in this section will use the following notion of type constraint.

Definition 5 (type constraint) A type constraint is one of the following:

a subtype constraint:  τ ≤^{ı} τ′
a monomorphic set constraint: α :: M

where M ⊆ T_{mono}. A subtype constraint is called basic if it is of the form α ≤^{ı} s, s ≤^{ı} α, or α ≤^{ı} β. A type substitution ϑ satisfies the type constraint

\begin{matrix}τ ≤^{ı} τ′ & if & ϑ(τ) ≤ ϑ(τ′) \\ α :: M & if & ϑ(α) ∈ M \end{matrix}  □

With this definition, the type inferencing procedure T I consists of the following 5 steps:

1. Transform Cl into a set R of type constraints.

2. From R infer a set R′ of basic type constraints and a corresponding type substitution ϑ.

3. Split R′ into polymorphic and monomorphic type constraints, yielding R_{poly} and R_{mono}.

4. Solve R_{poly} by extending ϑ, yielding ϑ′.

5. Solve R_{mono} by

5.1 constraint propagation, yielding R′_{mono},

5.2 choosing solutions for R′_{mono} by extending ϑ′, yielding ϑ′′.

If these steps are carried out successfully, Cl is well-typed w.r.t. the prefix

(1) \frac{p(t_{1}, …, t_{n}) & M, R}{t_{1} : τ & … & t_{n} : τ_{n} & M, R} if p : τ_{1} × … × τ_{n} is a variant of the declaration of p

(2) \frac{f(t_{1}, …, t_{n}) : τ & M, R}{t_{1} : τ_{1} & … & t_{n} : τ_{n} & M, τ_{o} ≤^{ı} τ & R} if f : τ_{1} × … × τ_{n} → τ_{o} is a variant of the declaration of f

(3)

\frac{x : τ & M, R}{M, α_{x} ≤^{ı} τ & R}

where α_{x} is a unique type variable associated to x

Figure 1: Computing type constraints from terms and literals

P = { x : ϑ′′(α_{x}) | x is a variable in Cl }

where α_{x} is a unique type variable associated to x.

In the following five subsections, we will give precise definitions of these five steps. Each step will be defined by a terminating set of transformation rules that are applied exhaustively to the respective input configuration.

4.1 Computation of subtype constraints

In order to ease our notation we will use & as an associative, commutative, and idempotent operator for sets. The pair (M, ∅) with M = L_{o} & … & L_{n} is our starting configuration to which the transformation rules of Figure 1 are applied.

Rule (1) introduces for every argument t of a literal a type membership requirement of the form t:τ. The idea is that a prefix P satisfies such a requirement if it renders t to be of a subtype of an instance of τ, i.e. if there is ϑ and τ′ with τ′ ≤^{ı} ϑ(τ) such that t is a well-typed term of type τ′ w.r.t. P. (c.f. the definition of well-typed atomic formula is Section 3.3).

These type membership requirements are decomposed by rule (2) into type membership requirements for the subterms and a subtype constraint for the type of the term according to the definition of well-typed term. Rule (3) finally transforms the remaining type membership requirements for the variables into corresponding subtype constraints where for every variable x a unique associated type variable α_{x} is introduced.

It is easy to show that the rules of Figure 1 terminate, thereby eliminating M and yielding the pair

∅, R

where R is a set of subtype constraints.

4.2 Inferring basic subtype constraints

Input to our second set of transformation rules given in Figure 2 is the pair

(1)  \frac{α ≤^{ı} α & R, ϑ}{R, ϑ}

(2) \frac{τ_{1} ≤^{ı} τ_{2} & τ_{2} ≤^{ı} τ_{3} & R, ϑ}{τ_{1} ≤^{ı} τ_{2} & τ_{2} ≤^{ı} τ_{3} & τ_{1} ≤^{ı} τ_{3} & R, ϑ} if τ_{1} ≤^{ı} τ_{3} ∉ R

(3)

\frac{α ≤^{ı} τ & τ ≤^{ı} α & R, ϑ}{ρ(R), ρ ∘ ϑ} if α does not occur in τ and where ρ is the type substitution {α ≐ τ}

(4)  \frac{s_{1} ≤^{ı} s_{2} & R, ϑ}{R, ϑ}  if s_{1} ≤ s_{2}

(5)  \frac{s_{1} ≤^{ı} α & s_{2} ≤^{ı} α & R, ϑ}{s ≤^{ı} α & R, ϑ}  if s = lub(s_{1}, s_{2})

(6)  \frac{α ≤^{ı} s_{1} & α ≤^{ı} s_{2} & R, ϑ}{α ≤^{ı} s & R, ϑ}  if s = glb(s_{1}, s_{2})

(7)  \frac{η(τ_{1}, …, τ_{n}) ≤^{ı} η(τ′_{1}, …, τ′_{n}) & R, ϑ}{τ_{1} ≤^{ı} τ′_{1} & … & τ_{n} ≤^{ı} τ′_{n} & R, ϑ}

(8) \frac{η(τ_{1}, …, τ_{n}) ≤^{ı} α & R, ϑ}{τ_{1} ≤^{ı} α_{1} & … & τ_{n} ≤^{ı} α_{n} & ρ(R), ρ ∘ ϑ}

if α does not occur in τ_{1}, …, τ_{n} and where α_{1}, …, α_{n} are new, pairwise distinct variables and ρ is the type substitution {α ≐ η(α_{1}, …, α_{n})}

(9) \frac{α ≤^{ı} η(τ_{1}, …, τ_{n}) & R, ϑ}{α_{1} ≤^{ı} τ_{1} & … & α_{n} ≤^{ı} τ_{n} & ρ(R), ρ ∘ ϑ}

if α does not occur in τ_{1}, …, τ_{n} and where α_{1}, …, α_{n} are new, pairwise distinct variables and ρ is the type substitution {α ≐ η(α_{1}, …, α_{n})}

Figure 2: Transformation and simplification of type requirements

R, id

with id denoting the identity type substitution.

Rule (1) eliminates trivial constraints. Rule (2) computes the transitive closure of ≤^{ı} . Rule (3) exploits the fact that ≤^{ı} obviously is antisymmetric w.r.t. to any solution. Rule (4) eliminates subtype constraints between monomorphic types that hold trivially. Rule (5) and (6) replace a common monomorphic upper bounds (resp. lower bound) by the least upper bound (resp. greatest lower bound). Rule (7) decomposes a subtype constraint between complex types. Rules (8) and (9) replace a subtype constraint between a type variable α and a complex type τ by an instantiation α and a set of simplified subtype constraints involving the arguments of τ.

Let the pair

R′, ϑ

be the result of applying the rules (1) - (9) exhaustively to (R, id). A failure condition in R′ is:

s_{1} ≤^{ı} s_{2}  if s_{1} ≰ s_{2}
s_{1} ≤^{ı} α & s_{2} ≤^{ı} α  if lub(s_{1}, s_{2}) does not exist
α ≤^{ı} s_{1} & α ≤^{ı} s_{2}  if glb(s_{1}, s_{2}) doest not exist
η(τ_{1}, …, τ_{n}) ≤^{ı} η′(τ′_{1}, …, τ′_{m}) if η ≠ η′
η(τ_{1}, …, τ_{n}) ≤^{ı} α  if α occurs in τ_{1}, …, τ_{n}
α ≤^{ı} η(τ_{1}, …, τ_{n})  if α occurs in τ_{1}, …, τ_{n}

Proposition 6 If R′ contains a failure condition, then there is no prefix P such that Cl is well-typed w.r.t. P. If R′ does not contain any of the above conditions, then R′ contains only basic type constraints and is said to be in solved form. □

4.3 Distinguishing polymorphic and monomorphic constraints

From the basic subtype constraints in R′ we can now easily determine which type variables must be instantiated to a monomorphic type constant. This is obviously the case for α ≤^{ı} s or s ≤^{ı} α, but also for every α′ with a (direct or indirect) subtype constraint w.r.t. α. Thus, we split R′ into two dispoint subsets R_{mono} and R_{poly}:

• R_{mono} is the smallest subset of R′ with

α ≤^{ı} s ∈ R_{mono} if α ≤^{ı} s ∈ R′
s ≤^{ı} α ∈ R_{mono} if s ≤^{ı} α ∈ R′
α ≤^{ı} α′ ∈ R_{mono} if α ≤^{ı} α′ ∈ R′ and
α or α′ occurs in R_{mono}

• R_{poly} := R′\R_{mono}

Proposition 7 Any well-typing for Cl must instantiate every variable occurring in R_{mono} to a monomorphic type constant, whereas any variable occurring in R_{poly} may remain a type variable. □

4.4 Solving polymorphic subtype constraints

We can sharpen the previous proposition with regard to the variables in R_{poly}. In fact, in any well-typing that is “most general” (in the sense that as few as possible type variables are instantiated to type terms that are as

(1) \frac{α ≤^{ı} β & R_{poly}, ϑ}{ρ(R_{poly}), ρ ∘ ϑ} where ρ is the type substitution {α ≐ β}

(2)  \frac{α ≤^{ı} α & R_{poly}, ϑ}{R_{poly}, ϑ}

Figure 3: Solving polymorphic type constraints

“small as possible”, see Section 5) every variable α in R_{poly} will indeed remain a variable, only identified with another type variable β if there is a subtype relationship between α and β in R_{poly}. Thus, the subtype requirements in R_{poly} are solved by applying the rules of Figure 3 to the pair

(R_{poly}, ϑ)

Since R_{poly} contains only basic type constraints between type variables we can prove that this will always resolve all elements in R_{poly}, leading to a pair (∅, ϑ′).

4.5 Solving monomorphic subtype constraints

We are now left with the pair (R_{mono}, ϑ′) where for each variable in R_{mono} a monomorphic type constant from T_{mono} must be found such that the constraints in R_{mono} are satisfied. This process is carried out in two steps. First the monomorphic set constraints in R_{mono} are propagated to all variables as far as possible (4.5.1). Whereas so far all steps have been carried out deterministically, the final step nondeterministically chooses monomorphic type instantiations from the remaining possibilities (4.5.2).

4.5.1 Propagating monomorphic set constraints

For any variable α in R_{mono} we can safely add the initialization constraint α :: T_{mono}. Therefore, the rules of Figure 4 are applied to

R_{mono} ∪ {α :: T_{mono} | α occurs in R_{mono}} (*)

Rules (1) and (2) evaluate a subtype restriction between a type variable and a monomorphic constant. Two monomorphic set constraints for the same type variable can be simplified to a single one by taking the respective intersection (rule (3)). Rule (4) allows to sharpen the monomorphic set constraints of two variables that must be instantiated to subtypes of each other: If α ≤^{ı} α′ then the set M of possible type constants for α can be restricted to those elements for which there is some supertype in the set M′ of possible type constants for α′. More formally, the set descriptions used in rule (4) are defined by

(1)  \frac{α ≤^{ı} s & R}{α :: \{s′ ∈ T_{mono} | s′ ≤ s\} & R}

(2)  \frac{s ≤^{ı} α & R}{α :: \{s′ ∈ T_{mono} | s ≤ s′\} & R}

(3)  \frac{α :: M & α :: M′ & R}{α :: (M ∩ M′) & R}

(4)  \frac{α :: M & α′ :: M′ & α ≤^{ı} α′ & R}{α :: M_{|≤M′} & α′ :: M′_{|≥M} & α ≤^{ı} α′ & R}  {if M ≠ M_{|≤M′} or \atop M′ ≠ M′_{|≥M}}

Figure 4: Propagating monomorphic set constraints

\begin{matrix}M_{|≤M′} := \{s ∈ M | ∃s′ ∈ M′.s ≤ s′\} \\ M_{|≥M′} := \{s ∈ M | ∃s′ ∈ M′.s ≥ s′\} \end{matrix}

Let R′_{mono} be the result of applying these rules exhaustively to (*). A failure condition in R′_{mono} is of the form

α :: ∅

since there is no possible instantiation for α.

Proposition 8 If R′_{mono} contains a failure condition, then there is no prefix P such that Cl is well-typed w.r.t. P. □

Therefore, for the last step let us assume that R′_{mono} does not contain a failure condition.

4.5.2 Choosing monomorphic types

We have now obtained the pair (R′_{mono}, ϑ′) where R′_{mono} contains a monomorphic set restriction α :: M for every variable α occurring in it, together with subtype constraints of the form α_{1} ≤^{ı} α_{2}. This pair (R′_{mono}, ϑ′) represents a set of solutions to our type inferencing problem: Instantiating any such α by an element of its associated set M such that the subtype constraints are satisfied yields a well-typing prefix for Cl. Moreover, this pair is a minimal representation of all (most general) well-typings of Cl in the following sense: For any such α :: M we can select any s ∈ M and still yield a well-typing under this selection.

Therefore, whereas all previous steps of T I were carried out deterministically, the final inferencing step non-deterministically chooses a type variable together with a possible monomorphic type constant by applying the rule of Figure 5 successively to the pair

(1) \frac{α :: \{s_{1}, …, s_{n}\} & R_{mono}, ϑ}{R′_{mono}, ρ ∘ ϑ}

where ρ is the type substitution {α ≐ s}, s is any of monomorphic types s_{1}, …, s_{n}, and R′_{mono} results from ρ(R_{mono}) by exhaustively applying the rules of Figure 4

Figure 5: Choosing monomorphic type instantiations

R′_{mono}, ϑ′

Exhaustively applying the propagation rules of Figure 4 after each selection ensure that no failure condition will be generated.

Proposition 9 During the propagation of constraints initiated by the selection rule in Figure 5 no failure condition of the form α :: ∅ will be generated. □

Thus, applying the selection rule terminates with a pair (∅, ϑ′′). ϑ′′ is said to be a type substitution generated by the type inferencing algorithm T I, and

P_{ϑ′′} := { x : ϑ′′(α_{x}) | x is a variable in Cl }

is a prefix inferred by T I.

Example 10 For the goal in Example 2, T I infers the type prefix

      {X:negint, Y:negint, L:list(int), M:list(int)}

□

Example 11 Consider the situation of Example 4. After execution of step 5.1 in T I the set R′_{mono} contains

      α :: {int, index, expr}

and thus each of {X:int}, {X:index}, and {X:expr} is a prefix inferred by T I. □

5 Correctness and completeness of type inferencing

We will now precisely state our correctness and completeness results for the type inferencing procedure T I. Due to lack of space the complete proofs can not be given here, but are given in the full version of this paper [2]. The proofs use the propositions given in the previous section; the termination proof is by induction on the involved terms.

We assume the notation of the previous section; in particular for Cl, R, R′, R_{poly}, R_{mono}, ϑ, ϑ′ and ϑ′′.

Theorem 12 (Correctness of successful derivations) If no failure condition occurs, then Cl is well-typed w.r.t. to the prefix P_{ϑ′′}.

Theorem 13 (Correctness of derivation failures) If a failure condition occurs, then there is no prefix P such that Cl is well-typed w.r.t. P.

Theorem 14 (Termination/Completeness of type inferencing) The type inferencing algorithm always terminates, i.e. each of the steps 1 to 5 terminates if all preceding steps have been carried out successfully.

The three theorems above imply the correctness and completeness of T I. However, we can even prove a stronger completeness result. The completeness result above says that whenever there is a well-typing prefix P then T I will derive a type substitution and thus some well-typing prefix P′. The strong completeness of T I ensures that for any such P T I derives a well-typing prefix P′ such that P′ is more general than P.

Theorem 15 (strong completeness) If there is a prefix P such that Cl is well-typed w.r.t. P then T I derives a type substitution ϑ_{P} such that Cl is well-typed w.r.t. P_{ϑ_{P}} and there is a type substitution ρ such that ρ(P_{ϑ_{P}}) = P.

6 Conclusions and further work

In this paper we have studied automatic type inferencing for polymorphic order-sorted logic programs. After pointing out the difficulties with previous approaches we have presented a complete type inferencing algorithm for this problem. Whereas we addressed the correctness and completeness issues, we did not deal with efficiency or complexity matters in this paper. For instance, in an implementation of T I one would look for an efficient representation of the monomorphic set constraints α :: M. An obvious choice for the representation of M would be the representation by its lower and upper bounds. Another aspect not yet studied in this paper that needs further investigation is the relationship of our approach to the work on polymorphic type inference done for functional programming languages.

Acknowledgements

I would like to thank Gregor Meyer for his comments on previous versions of this paper as well as the anonymous referees for their valuable hints.

References

[1] C. Beierle. Concepts, implementation, and applications of a typed logic programming language. In C. Beierle and L. Plümer, editors, Logic Programming: Formal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence, chapter 5, pages 139–167. Elsevier Science B.V./North-Holland, Amsterdam, Holland, 1995.

[2] C. Beierle. Type inferencing for logic programming with polymorphic order-sorted types. Informatik-Bericht, FB Informatik, FernUniversität Hagen, 1995. (to appear).

[3] C. Beierle and G. Meyer. Run-time type computations in the Warren Abstract Machine. Journal of Logic Programming, 18(2):123–148, February 1994.

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

[5] J.A. Goguen and J. Meseguer. Remarks on Remarks on Many-Sorted Equational Logic. In Bulletin of the EATCS , number 30, 1986.

[6] M. Hanus. Horn clause programs with polymorphic types: Semantics and resolution. In Proceedings TAPSOFT’89. Springer-Verlag, 1989.

[7] M. Hanus. Logic programming with type specifications. In F. Pfenning, editor, Types in Logic Programming. MIT Press, 1992.

[8] P. M. Hill and R. W. Topor. A semantics for typed logic programs. In F. Pfenning, editor, Types in Logic Programming. MIT Press, 1992.

[9] P. Mishra. Towards a theory of types in Prolog. In Proceedings of the 1984 Symposium on Logic Programming, pages 289–298, Atlantic City, New Jersey, 1984.

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

[11] F. Pfenning. Types in Logic Programming. MIT Press, Cambridge, MA, 1992.

[12] G. Smolka. TEL (Version 0.9), Report and User Manual. SEKI-Report SR 87-17, FB Informatik, Universität Kaiserslautern, 1988.

[13] G. Smolka. Logic Programming over Polymorphically Order-Sorted Types. PhD thesis, FB Informatik, Univ. Kaiserslautern, 1989.

[14] J. Xu and D. S. Warren. A type inference system for Prolog. In K. A. Bowen and R. A. Kowalski, editors, Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 604– 619, Seattle, Washington, August 1988. MIT PRESS.

[15] J. Zobel. Derivation of polymorphic types for Prolog programs. In J.-L. Lassez, editor, Proceedings of the Fourth International Conference on Logic Programming, pages 817–838, Melbourne, May 1987. MIT PRESS.