A Bottom-up Polymorphic Type Inference in Logic Programming

Roberto Barbuti , Roberto Giacobazzi Dipartimento di Informatica Università di Pisa Corso Italia 40, 56125 Pisa

{barbuti,giaco}@di.unipi.it

May 10, 1995

Abstract We present a type inference system for Horn Clause Logic programs, based on a bottomup abstract interpretation technique. Through the definition of suitable abstract operators, we obtain an abstract immediate consequence operator map associated with the program to analyze. The least fixpoint of such an operator gives an approximated description, by means of types, of the success set of the program. By changing the abstract domain of types, we easily obtain different type inference systems. This is useful to make the inference appropriate for different purposes. Due to the semantic basis, the system declaratively handles type union and parametric polymorphism.

1 Introduction

Logic programming has been introduced as an untyped language, without any discipline on types. Such flexibility is often paid in terms of difficult debugging and not efficient computations. On the other hand, a strong type discipline as in Pascal precludes the flexibility which is a key point of the logic programming style. Given the importance of the topic, many studies were devoted to type schemes for logic programming. The proposed approaches can be partitioned in two main classes, type checking and type inference. Type checking consists in verifying whether the use of types in a program is consistent with some type declarations. On the other hand, type inference is the process of determining the type of program units, given a program with incomplete type declarations. Type inference was first studied within the functional paradigm [23, 28]. Its application to logic programming has been done with a conceptually different meaning. In functional programming, all the rules (or branches) defining a function must be potentially applicable to values in the same domain. Thus, if a function is defined by rules involving different (comparable) types, the overall type is the greatest lower bound of them. On the other hand, type inference in logic programming respects the untyped nature of the paradigm. If the clauses defining a predicate generate results with different types, the inferred type is simply the union of them, without imposing restrictions. Thus, type inference in logic programming results in the approximated description, by means of types, of the success set. This result can be used as a powerful tool for debugging logic programs.

A number of different semantics for logic programs are possible as a basis for abstract interpretation. The distinction between top-down and bottom-up data-flow analyses in imperative and functional languages helps also in logic programming to distinguish between two different classes of analyses [25]. Top-down analyses propagate the information in the same direction as an SLD-refutation, whereas bottom-up analyses propagate information in the opposite direction, thus returning an approximation of the whole success set. A number of studies have been devoted to show the equivalence of the two approaches in logic programming [3, 7]. However, since the bottom-up one returns an approximation of the success set of the program, it is more adequate for goal independent type inference.

The aim of this paper is to show how polymorphic type inference can be seen as an instance of bottom-up abstract interpretation. Moreover different type inferences can be obtained as instances of the framework with different abstract domains. This approach can be used to study the relationships among various type inference systems.

Logic programming is not extended with complex type structures, but types are only used to describe approximations of success sets in a concise way. We show how polymorphic typing can be handled in a very natural way by abstracting an underlying (concrete) semantics defined in terms of non-ground semantics objects. The advantages of this approach come from the use of a new declarative semantics for logic programs via a bottom-up abstract interpretation, namely:

• the correctness proof can be carried out in a standard way,

• the inference process is goal independent (we generate a success set on the domain of “polymorphic types” with respect to which any goal can be analyzed),

• type inference can be easily enriched simply by changing the domain of types.

The above features characterize this approach with respect to the ones in the literature.

The paper is organized as follows. Section 2 discusses other approaches to the problem. Section 3 briefly reviews the notion of abstract interpretation, the semantics basis of our approach and a bottom-up abstract interpretation scheme. Section 4 presents a type inference system, together with some examples. In Section 5, different definitions of the abstract domain and operators lead to a discussion about the role of bottom-up abstract interpretation for type inference in logic programming. Finally, Section 6 concludes.

2 Related Works

In this section we discuss works about the introduction of type information in logic programming. Such studies are conceptually partitioned in three classes: type checking, type inference and abstract interpretation based type inference. One of the first contribution on a polymorphic type system in logic programming is that of Mycroft and O’Keefe [30], inspired by the type system of ML [28]. Polymorphism results from the possibility to have type variables in the type structures. In this type system for Prolog, the programmer has to declare types for predicates and functions. The approach is to consider type specifications as restrictions on the arguments of predicates and terms, and a static type checker is devoted to check that these restrictions are respected. In [15], Gang and Zhiliang give a type system for Prolog with type declarations. It is mainly intended to gain efficiencies at compile-time and run-time. In [17], Hanus describes a type system for HCL, where predicates and functions are declared with polymorphic types. The obtained polymorphic type system is an extension of the one in [30]. A model theoretic and an operational semantics are given. A specialized unification algorithm extends the refutation method to a typed world. One of the first works about type inference is presented by Mishra in [29]. The type of a predicate describes all terms for which the predicate may succeed, a predicate p has type τ if p(t) fails for all t “outside” τ. The inferred types are symbolic descriptions of terms by means of ground regular trees (only monomorphic types are inferred). Type inference is performed by a set of inference rules on a restricted class of Prolog predicates. The extension to a polymorphic type scheme presents some problem due to difficulties in handling parameterized regular trees. Zobel [36] presents an approach similar to the previous one. A syntactic type inference based on a specialisation of the classical unification algorithm is presented. It does not require any type declaration: The inference process returns a set of type rules: α ← {f(β)} for each predicate in the program. The type of a predicate has the form p(η_{1}, ..., η_{n}) together with a set of type rules S = {α_{j} ← ω_{j}}, in which each η_{i} may be defined. For the sake of finiteness, the clauses are explored only once, thus recursive clauses can give rise to highly incomplete type information. Pyo and Reddy follow this line by presenting a type inference algorithm based on the notion of type as a set of values [31]. An approach based on a top-down abstract interpretation technique can be found in Bruynooghe et al. [6]. To obtain a finite lattice of types (the abstract domain), a normalized type graph (rational tree) is associated with each type. The meaning of a graph is the set of ground terms which can be folded onto it. The presence of restrictions ensures that all type graphs are finite and that only a finite number of such graphs can be constructed from a given finite set of functor symbols. Type inference is performed by specializing the abstract interpretation scheme, which generate an AND/OR graph associated with the refutation process for a given goal. The main problem in this approach is the strong approximation induced by the restrictions on type graphs: for example, to limit the depth of the graph, any acyclic path is not allowed to contain the same functor symbol twice. An extension of this approach is given in [5]. Kluz̀niak [21] uses top-down abstract interpretation to derive a description of the solutions of a ground Prolog goal, starting from mode declarations. The above approaches do not use type names, types are described by different representations of set of values. The following two works are closer to our approach. The Herbrand Universe is partitioned in classes, and each class is described by a type term. Then, for each predicate an approximation of its success set is inferred and its representation by means of type terms is given. In [19], Kanomori and Horiuchi present a type inference based on an abstract interpretation technique. The polymorphic inference derives from a variation (at the abstract level) of the OLDT-resolution by Sato and Tamaki (this is an hybrid interpretation for logic programs, based on both a top-down and a bottom-up analysis of the program itself). Since the algorithm might generate an infinite number of solutions, a depth-k cutting prevents the analysis from infinite loops [32]. Our type structure and inference is similar to this one. One of the main differences is the use of variables in our type patterns (instead of the any value), thus preserving the connection among arguments of polymorphic types. Moreover, the use of bottom-up abstract semantics allow us to give a view of predicate types in the whole program (not only those involved in a specific goal). In [34], a paper by Xu and Warren, the typing is a consequence of a partition of the Herbrand universe based on type declarations. The inference procedure is performed by a program transformation which returns a type inference logic program, and then by querying this new program. A call to P ROV E (the type inference procedure) is performed for each predicate defined in the original program. The answer obtained by P ROV E, which represents the associated type pattern, can contain uninstantiated variables. These variables are considered as globally quantified on types, thus handling polymorphism. By groundness, the treatment of parametric polymorphism does not, in the Herbrand universe, result uniform with respect to the monomorphic case. The semantic foundation of polymorphism cannot be given in a declarative style, through the notion of Herbrand model. The same problem is present in [35] where types are seen as regular sets of terms. In this paper type inference and type checking are studied using abstract interpretation. However, the approach does not allow to infer parametric types. Moreover the type of a predicate is considered to be unique.

We define a polymorphic type inference system for logic programs, based on a bottom-up abstract interpretation scheme. This approach overcome the problems of the previous ones, mainly for two points: i) the use of bottom-up abstract interpretation allows a goal independent analysis, and ii) the use of a suitable semantics gives a natural (semantics-based) treatment of polymorphism. Through the definition of a suitable set of abstract operators we obtain the abstract (finitely convergent) counterpart of the immediate consequence operator T_{P}. The least fixpoint of it is the approximation of the success set of the program by means of type patterns describing the well-typed atoms in it.

3 Preliminaries

In this section we present the bottom-up abstract interpretation framework together with a T_{P} - based concrete semantics for logic programs. Any concept not formally defined can be found in [2, 3, 11, 12].

3.1 Abstract interpretation

We formalize the notion of abstract interpretation according to the ideas given by Cousot and Cousot [9]. An introduction to the subject of abstract interpretation in the field of logic and functional languages can be found in [1]. Let us consider a concrete domain D_{P} (a set of computational state representations associated with the generic program P) which is a complete lattice with respect to a partial order relation ≤_{D_{P}}, and a state transition function E_{P}, defined on D_{P}. Let us assume the program computational behavior being fully characterized by a solution of the recursive equation x = E_{P} (x). Thus we can state that (D_{P} , ≤_{D_{P}} , E_{P}) defines a standard fixpoint semantics for the program P. Since computations can be infinite, the above definition cannot be used for static program analysis. Therefore we define a non-standard fixpoint semantics based on an abstract (usually finite or even Noetherian) domain D_{P}, called abstract semantics (D_{P} , ≤_{D_{P}} , E_{P}) to guarantee the effectiveness of the analysis. Obviously, this kind of analysis is less precise than the one given by the complete semantics definition.

The relation between the standard and the abstract semantics was established in [9] by defining a pair of functions α and γ (abstraction and concretization), which form a Galois insertion between (D_{P} , ≤_{D_{P}}) and (D_{P} , ≤_{D_{P}}) [9, 27]. This notion allows us to formally handle the correctness condition on the abstract interpretation framework. Formally, an abstract interpretation scheme [9, 25] is a tuple ⟨(D_{P} , ≤_{D_{P}}) , E_{P} , (D_{P} , ≤_{D_{P}}) , E_{P} , α , γ⟩ such that

1. (D_{P} , ≤_{D_{P}}) and (D_{P} , ≤_{D_{P}}) are complete lattices,

2. E_{P} : D_{P} → D_{P} and E_{P} : D_{P} → D_{P} are monotonic functions,

3. α : D_{P} → D_{P} (abstraction) and γ : D_{P} → D_{P} (concretization) are monotonic functions,

4. ∀ d^{α} ∈ D_{P} , α(γ(d^{α})) = d^{α},

5. ∀ d ∈ D_{P} , d ≤_{D_{P}} γ(α(d)).

The last three conditions define a Galois insertion between the abstract domain and the concrete one. Galois insertions give us the formal framework to prove correctness of an abstract interpretation. They define a strong relationship between the concrete domain of computations and the abstract, usually simpler, domain associated with the analysis. Their usefulness was outlined in [9, 10] as a base to develop soundness conditions for semantics-based analysis of flowchart programs. They also ensure that the domain D_{P} (the abstract domain of computation) does not contain redundant elements. According to conditions 4 and 5, the concretization cannot cause any loss of information, while the abstraction of a concrete object may cause some loss of information [9]. Given a Galois insertion ⟨α, γ⟩ on the lattices (D_{P} , ≤_{D_{P}}) and (D_{P} , ≤_{D_{P}}), the following statements hold [10, 27]:

• abstraction and concretization uniquely determine each other,

• γ preserves arbitrary meets, that is ∀ B ⊆ D_{P} , glb_{≤_{D_{P}}} { γ(d^{α}) | d^{α} ∈ B } = γ(glb_{≤_{D_{P}}} B),

• α preserves arbitrary joins (i.e. α is additive), that is ∀ B ⊆ D_{P} , lub_{≤_{D_{P}}} { α(d) | d ∈ B } = α(lub_{≤_{D_{P}}} B).

The program analysis is done by computing a (finite) Kleene sequence {E_{P}^{n}(⊥_{D_{P}})}_{n∈{1,...,k}} of finitely computable approximations of the semantic solution of the recursive equation x = E_{P} (x). The correctness of such an approximation can be given by conditions relating E_{P} with E_{P}: for example ∀ d ∈ D_{P} : α(E_{P} (d)) ≤_{D_{P}} E_{P} (α(d)) [9, 10]. In our case, we will consider a weaker notion of correctness (see Theorem 4.23).

In the following sections we introduce a declarative semantics for logic programs adequate for semantics-based program analyses and the main ideas of a framework for bottom-up logic program analysis based on such a semantics.

3.2 Bottom-up semantics of logic programs

The following results about the semantics of logic programs are defined in [11, 12]. This semantic definition is closer than the one in [24, 33] to the operational behavior of logic programs, which was shown to require a more complex and appropriate notion of model, in general different from the minimal Herbrand model. The model theoretic and fixpoint semantics in [12] capture possibly non-ground computed answer substitutions. Such a semantic definition is then the right one in order to develop a bottom-up abstract interpretation framework, without requiring to extend the standard semantics with a somewhat artificial collecting semantics. A standard semantics able to characterize the operational behavior of logic languages can therefore be found inside the first order logic semantics (model-theoretic and fixpoint), by considering possibly non-initial models, having a richer information structure, like those giving a representation (usually finite by means of variables) of infinite sets of ground atoms. We have to consider a different notion of program equivalence, rich enough to model the useful information for program analysis, i.e. the observable properties of the operational semantics.

We consider an extended Herbrand Universe containing also non-ground terms. Thus, it is possible to define a non-ground success set and to declaratively characterize the ability of logic programs to compute answer substitutions (which are non-ground in general).

Let us consider the set Σ of constructors, with typical elements a, b, c, ... (constructors with 0 arguments Σ_{0}), and f, g, h, ... (constructors with one or more arguments Σ_{n}, n > 0), and a denumerable set V ar of variables. The free Σ-algebra on V ar, T_{Σ}(V ar), is inductively defined as the least family such that:

• ∀c ∈ Σ_{0}, c ∈ T_{Σ}(V ar);

• ∀v ∈ V ar, v ∈ T_{Σ}(V ar);

• ∀t_{1} ∈ T_{Σ}(V ar), ..., ∀t_{n} ∈ T_{Σ}(V ar), ∀d ∈ Σ_{n}, d(t_{1}, ..., t_{n}) ∈ T_{Σ}(V ar).

Notice that the standard Herbrand Universe is defined as T_{Σ}(∅), that is the set of all ground terms in the language. In the following, we denote by ≡ the syntactic equivalence of objects.

The set of substitutions, with typical elements σ, ϑ, ... consists of all the mappings ϑ from V ar into T_{Σ}(V ar), such that {x ∈ V ar | ϑ(x) ≠ x} is finite. ε denotes the empty substitution.

The application of a substitution ϑ to a term t (denoted tϑ) is defined as the term obtained by replacing each variable x in t by ϑ(x). The composition ϑσ of ϑ and σ is defined as function composition. We recall that the composition is associative and for each term t, t(ϑσ) ≡ (tϑ)σ. A renaming is a variable bijection. A substitution ϑ′ is more general than ϑ (ϑ ≤ ϑ′), iff there exists σ such that ϑ = ϑ′σ. The notion of unification can be given with respect to a set of equations. An equation is an expression of the form t = u, where t, u ∈ T_{Σ}(V ar). Given a set E of equations, E is unifiable iff there exists ϑ such that ∀(t = u) ∈ E, (tϑ) ≡ (uϑ). We denote by Unif(E) the (possibly empty) set of unifiers of E. We denote by mgu(E) the set {ϑ ∈ Unif(E) | ∀ϑ′ ∈ Unif(E) : ϑ ≤ ϑ′}. It is well known that all the most general unifiers of a set E are equivalent [22].

Consider a program P and the set Σ_{P} of constructors of the first order language underlying P. The extended Herbrand Universe U_{P} is defined as T_{Σ_{P}} (V ar)/ ∼, i.e. the set of equivalence classes with respect to the variance relation ∼ (t_{1} ∼ t_{2} iff ∃ ϑ_{1}, ϑ_{2} such that t_{1}ϑ_{1} = t_{2} ∧ t_{2}ϑ_{2} = t_{1}). Together with an added least element, it is a complete lattice with respect to the usual preorder on terms ≤ , such that t_{1} ≤ t_{2} iff ∃ϑ | t_{1} = t_{2}ϑ.

Let Π_{P} be the set of predicate symbols in the program P. An atom is an object of the form p(t_{1}, ..., t_{n}) where t_{1}, ..., t_{n} ∈ T_{Σ_{P}} (V ar) and p is an n-ary predicate symbol (i.e. p ∈Π^{n}_{P}). We denote the set of atoms as Atoms. In the following, given two atoms A = p(t_{1}, ..., t_{n}) and A′ = p(t′_{1}, ..., t′_{n}), we denote by mgu(A, A′) an element in mgu({t_{i} = t′_{i} | i = 1, ..., n}). We extend this notation to any tuple of atoms.

A clause is a formula of the form H : − B_{1}, ..., B_{n} with n ≥ 0 where H (the head) and B_{1}, ..., B_{n} (the body) are atoms and : − and “,” denote logic implication and conjunction respectively. The variables are assumed to be universally quantified. If the body is empty, the clause is a unit clause. A goal is a formula B_{1}, ..., B_{n} (denoted by : −B_{1}, ..., B_{n}), where each B_{i} are atoms. A logic program is a finite set of clauses.

Given a term t ∈ T_{Σ}(V ar), the set of variables occurring in t is denoted by vars(t) (in the following, with abuse of notation, we apply the vars operator to atoms and clauses as well). We extend also the notion of variance ∼ to any syntactic object (i.e. terms, atoms, clauses, etc.). For a syntactic object s and a set of equivalence classes modulo renaming of objects I, we denote by ⟨c_{1}, …, c_{n}⟩ <<_{s} I that c_{1}, …, c_{n} are representatives of elements of I renamed apart from s and from each other. Namely, that [c_{i}]_{∼} ∈ I, vars(c_{i}) ∩ vars(s) = ∅ (i = 1..n); and that for i ≠ j, vars(c_{i}) ∩ vars(c_{j}) = ∅ (i = 1..n, j = 1..n). The powerset of a set X is denoted by ℘(X). If X is a set, the corresponding set of n-tuples of elements in X is denoted X^{n}.

In the following, an extended notion of interpretation is given [13, 14]. The extended interpretations are more expressive than Herbrand interpretations because of the use of more syntactic objects (like variables) in the semantic domains.

Analogously to the standard semantics, the Base of interpretations B_{P} is defined as Atoms/ ∼. An extended interpretation (interpretation) I is a subset of B_{P} (it represents the set of atoms which are true in I).

Definition 3.1 [13] An interpretation I is a model for the logic program P iff every clause of P is true in the Herbrand interpretation G(I) (i.e. G(I) is a Herbrand model for P), where G(I) represents the set of ground instances of atoms in I.

In positive logic programs, the operational semantics is a set of possibly non-ground atoms. The notion of model is general enough to capture the observable operational behavior of a logic program as a model. Moreover, every Herbrand model is still a model in the extended context.

We introduce now an immediate consequences operator T_{P} on interpretations whose least fixpoint is an extended model (model) which is able to capture computed answer substitutions.

Definition 3.2 (immediate consequences operator) [11, 12] Given a logic program P, the operator T_{P} on the set of interpretations associated with P is defined as follows

T_{P} (I) = \{ A′ ∈ B_{P} | \begin{matrix}C ≡ A : −B_{1}, ..., B_{n} ∈ P \\ ⟨B′_{1}, ..., B′_{n}⟩ <<_{C} I \\ ϑ = mgu((B_{1}, ..., B_{n}), (B′_{1}, ..., B′_{n})) \\ and A′ = Aϑ \end{matrix} \} .

This definition is different with respect to the standard ground T_{P} operator [33]. It derives possibly non-ground atoms by means of a bottom-up inference rule which is based on unification, as in the top-down SLD resolution. As usual, T_{P} is a continuous function on the complete lattice of interpretations ordered by set-inclusion [12]. In the following we use T_{P} ↑ α as a notation for ∪_{n∈α} T_{P}^{n}(∅), where α is a set of finite ordinals and ω denotes the set of all the finite ordinals. A fixpoint characterization of the program semantics is lfp(T_{P}) = T_{P} ↑ ω. We observe that each interpretation I such that T_{P} (I) ⊆ I is a model for P thus, lfp(T_{P}) is a model as well.

The two most important results which characterize the relation between the new fixpoint semantics and the operational one (the equivalence between fixpoint and operational semantics) are the strong soundness and the strong completeness theorems given below. They show that lfp(T_{P}) is the fully abstract semantics with respect to computed answer substitutions. Previous attempts of defining bottom-up abstract interpretations failed on non-trivial analyses (like mode analysis and polymorphic type inference) since they were based on an immediate consequence operator leading to a fixpoint semantics which did not model computed answer substitutions.

In the following G →_{P}^{∗}^{ϑ} □ denotes a refutation for a given goal G in P, with answer substitution ϑ, while ϑ_{|G} is the restriction of the substitution ϑ to the variables occurring in G, extended as an identity for each variable x ∈ vars(G) such that ϑ(x) is undefined. We extend the notation ϑ_{|s} to any syntactic objects s.

Theorem 3.3 (Strong Soundness) [11, 12] Let P be a logic program and let G be a goal : −B_{1}, ..., B_{n}. Assume that G →_{P}^{∗}^{ϑ} □, then ∃ ⟨B′_{1}, ..., B′_{n}⟩ <<_{G} lfp(T_{P}) and ∃ ϑ′ = mgu((B_{1}, ..., B_{n}), (B′_{1}, ..., B′_{n})) such that ϑ′_{|G} = ϑ_{|G}.

Theorem 3.4 (Strong Completeness) [11, 12] Let P be a logic program and let G be a goal : −B_{1}, ..., B_{n}. If ∃ ⟨B′_{1}, ..., B′_{n}⟩ <<_{G} lfp(T_{P}) and

∃ ϑ′ = mgu((B_{1}, ..., B_{n}), (B′_{1}, ..., B′_{n})), then ∃ ϑ such that G →_{P}^{∗}^{ϑ} □ and ϑ′_{|G} = ϑ_{|G}.

This semantics, due to its relation with the operational one, has been used in some bottomup abstract interpretations frameworks [3, 7, 20]. Since we wil introduce the notion of well-typed derivation for a goal, the correctness of our analysis will be proved with respect to a variant of the previous concrete semantics.

3.3 Bottom-up abstract interpretation

In the following we recall some of the basic concepts developed in [3]. This framework is particulary suitable for semantics-based polymorphic type inference in logic programming, due to the use of possibly non-ground semantics objects.

The basic idea is to abstract the concrete immediate consequence operator T_{P} to obtain an abstract operator whose fixpoint is finitely computable and is a correct approximation of the concrete bottom-up semantics of the program. This is achieved by defining an abstract domain of interpretations, based on the notion of abstract atom. The construction of the domain of abstract interpretations follows a step-by-step approach. The main problem is what we want to observe from the concrete data behaviour and how the resulting abstract data objects are represented in order to have an efficient (concise) data-flow analysis. In order to suitably define an abstract domain for a given program analysis, three abstraction levels are presented, each one related with a different data-property. In the first one, the abstraction is performed on terms in order to summarize all and only those properties which are useful for the “term analysis”. The second step deals with how abstract terms are collected together (in abstract atoms) and which properties of their union the analysis is interested in. Finally, in the third step, the notion of abstract interpretation is introduced. It corresponds to choosing which properties we want to observe, collecting together different abstract atoms [3].

In type infrence the first abstraction level will correspond to abstract a given term returning its type. A corresponding domain of abstract atoms will be considered for the second one. As for the third abstraction level, we will consider abstract interpretations as sets of abstract atoms. In the following we will consider a simplified instance of the framework in [3], which is general enough to define our type inference system.

Let H be a domain of abstract terms and B_{P} the set of (abstract) atoms defined on H. Let (℘(B_{P}), ⊆) be the resulting abstract domain of interpretations, specified by means of a Galois insertion (α, γ) of (℘(B_{P}), ⊆) into (℘(B_{P}), ⊆). We assume that (℘(B_{P}), ⊆) is a finite lattice.

The definition of an abstract immediate consequence operator T_{P} : B_{P} → B_{P} abstracting T_{P} is given in terms of a set of abstract operators, namely:

• abstract unification, α-mgu : B_{P}^{n} × B_{P}^{n} ⟶ (V ar → H): it plays the fundamental role of passing the information from the abstract to the concrete context, by returning an abstract substitution (i.e. a binding of concrete variables to abstract terms) defined on the set on variables of the concrete atoms.

• abstract substitution application, α-apply : B_{P} × (V ar → H) ⟶ B_{P}: which applies an abstract substitution to a concrete atom returning an abstract atom.

The abstract immediate consequence operator is then:

T_{P} (I^{α}) = \{ α − apply(A, ϑ^{α}) | \begin{matrix}C ≡ A : −B_{1}, ..., B_{n} ∈ P \\ ⟨B_{1}^{α}, ..., B_{n}^{α}⟩ <<_{C} I^{α} \\ ϑ^{α} = α − mgu((B_{1}, ..., B_{n}), (B_{1}^{α}, ..., B_{n}^{α})) \\ ϑ^{α} ≠ F ail \end{matrix} \} .

where I^{α} ∈ ℘(B_{P}) and << extends in the obvious way on abstract variables (if any) as well as concrete ones.

4 Type Inference

In this section we present a polymorphic type inference based on the above abstract interpretation scheme. In the first subsection we introduce type declarations. In the second one we present the domain of types. In the third subsection we present an approximation of the domain of types. The fourth subsection introduces a set of abstract operators which can be used to define a correct abstract immediate consequence operator for polymorphic type inference. The proofs of the basic properties of the abstract semantics are in the Appendix. Finally, in the last subsection we show some examples.

4.1 Type declarations

In order to build the domain of types we use type declarations to reduce each term to its type. The choice of having type declarations is motivated both by the need to have a concise description of the success set (as stressed in [34]) and by the advantages given by type variables [28]. Unlike other approaches, multiple occurrences of the same type variable allow to specify that the type of components, although not specified, must be the same. A type declaration is a set of rules grouped in two possible constructs, simple type declaration and parametric type declaration:

Simple type declaration:

type tname :
c → tname
.....................
f(τ_{1}, ..., τ_{m}) → tname

end Parametric type declaration:

type tname(ζ_{1}, ..., ζ_{n}) :

c → tname(⊥_{τ} , ..., ⊥_{τ})

.....................

f(τ_{1}, ..., τ_{m}) → tname(ζ_{1}, ..., ζ_{n}) end

Each type declaration begins with the type name it defines; a parametric type is a type name applied to variables (ζ_{i}) ranging on types.

The left part of each rule is either a constant or the application of a function symbol to types τ_{i}. A type is a simple type name, a variable or a parametric type name applied to types. A parametric type declaration cannot consist of constants only.

The right part of each rule defining a simple type is the type name itself, while the right part of a rule defining a parametric type is the application of the type name either to a sequence of variables or to a sequence of ⊥_{τ}. ⊥_{τ} stands for the undefined type, and tname(⊥_{τ} , ..., ⊥_{τ}) denotes the type associated with any constant in a parametric type declaration. Intuitively, the meaning of tname(⊥_{τ} , ..., ⊥_{τ}) is that the type associated with a constant of a parametric type is partially undefined: it will be completely known only when used in a more structured object. The reason of this choice will be clear in the following, let us only mention that a similar choice is adopted in [19] (∅ replaces ⊥ ) although with a different underlying intuition.

Type declarations can be used as a set of reduction rules to reduce terms to types. In order to assign only one type to a term, there are no two rules with unifiable left parts.

Reduction rules induce a set of equivalence classes on the universe of terms: two terms belong to the same class if and only if they are reducible to the same type or they are (both) not reducible to a type (i.e. they are not well-typed).

Finally, to be useful, type declarations must be complete for the logic program we want to study: i.e. each constant or function symbol occurring in the program must occurr in a rule left part.

Example 1 As an example consider the definition of the type nat and the type list, a simple and a parametric type declaration respectively:

type nat :  type list(α) :
0 → nat  nil → list(⊥_{τ})
s(nat) → nat  cons(α, list(α)) → list(α)
end  end

Type declarations are defined on a set of type constructors denoted Ω and on a denumerable set of type variables V ar_{τ} such that V ar ∩ V ar_{τ} = ∅. Let T_{Ω}(V ar_{τ}) denotes the set of type terms inductively defined on Ω and V ar_{τ}. In the following we denote (also inside programs) variables ranging on types (in V ar_{τ}) by greek letters α, β, ζ, ... and arbitrary types (in T_{Ω}(V ar_{τ})) by τ, τ′, τ′′, ... . Moreover, we denote by RR^{τ} the set of reduction rules of simple and parametric type declarations: RR^{τ} = RR_{simple}^{τ} ∪ RR_{parametric}^{τ}.

4.2 The domain of types

Starting from type declarations, we define a standard methodology to construct the domains of types for a type inference system. The domain of types is built by typing the terms of the concrete one. Usually typing is performed by means of inference rules; in our case this role is played by the reduction rules obtained from type declarations. Thus, the domain of types is obtained by reducing terms to types by means of RR^{τ}. An important point is that our system, given the presence of ⊥_{τ} and type variables, can infer different types for terms which are supposed to have the same type structure. The following two examples clarify the problem:

• consider the term cons(0, nil). The reduction process leads to cons(nat, list(⊥_{τ})) which is not furtherly reducible. To force the reduction we normalize two different types to the most descriptive of them when possible. In this case since nat is more descriptive then ⊥_{τ}, cons(nat, list(⊥_{τ})) is forced to cons(nat, list(nat)) and then reduced.

• Consider now cons(0, cons(X, Y)). This term can be reduced to cons(nat, list(α)) and furtherly reduced to list(nat) by substituting α with nat. This means that a type name is more descriptive than a variable, or, in different words that we can know the type of a list by knowing the type of at least one element (a discussion on this assumption is presented in Section 5).

These examples show that typing is performed by both a reduction and a normalization process. These two processes can be performed by means of a simple deterministic program. Since the application of reduction rules needs unification, we use a Prolog program P^{τ} to perform reductions. This program derives directly from type declarations and type descriptivity and it is defined on the universe of terms extended with types terms. The definition is given by two predicates: T ype, which is responsible of the reduction of terms to types, and Norm, which normalize two types to the most descriptive, when possible. Notice that only type correct terms can be reduced to their types. Let P^{τ} denote the following Prolog program:

{T ype(X, X) : −V ar(X),!. } ∪

{ T ype(type, type) : −!. | type is a simple or parametrictype } ∪

{ T ype(c, tname). | c → tname ∈ RR_{simple}^{τ} } ∪

\{ \begin{matrix}T ype(f(X_{1}, ..., X_{m}), tname) : −T ype(X_{1}, τ_{1}), ..., T ype(X_{m}, τ_{m}). \\ where f(τ_{1}, ..., τ_{m}) → tname ∈ RR_{simple}^{τ} \end{matrix} \} ∪

{ T ype(c, tname(⊥_{τ} , ..., ⊥_{τ})). | for each c → tname(⊥_{τ} , ..., ⊥_{τ}) ∈ RR_{parametric}^{τ} } ∪

\{ \begin{matrix}T ype(f(X_{1}, ..., X_{m}), tname(ζ_{1}, ..., ζ_{n})) : −T ype(X_{1}, τ′_{1}), ..., T ype(X_{m}, τ′_{m}), ..., \\ Norm(W_{1_{i}}, W_{2_{i}}, Z_{1_{i}}), ..., Norm(Z_{k_{i}−1}, W_{k_{i}}, ζ_{i}), .... \end{matrix} \}

where f(τ_{1}, ..., τ_{m}) → tname(ζ_{1}, ..., ζ_{n}) ∈ RR_{parametric}^{τ}, and the

terms τ′_{1}..τ′_{m} are obtained from τ_{1}..τ_{m} by replacing all the k_{i} occurrences of each variable ζ_{i} by k_{i} fresh variables W_{s}, s = 1, .., k_{i}.

The first two sets of program clauses handle type variables and declared types (the type is given by themselves). The clauses associated with simple type declarations either give type to constants or recursively apply the predicate T ype to the components of a term. The clauses associated with parametric type declaration do the same, the only difference is that in a clause corresponding to a rule f(τ_{1}, ..., τ_{m}) → tname(ζ_{1}, ..., ζ_{n}), all the occurrences of a type variable ζ_{i} (i = 1, ..., m) in τ_{1}, ..., τ_{m} are replaced by fresh variables (W). The predicate Norm returns the most descriptive type among the answers computed for the W ’s (that is among the ones computed for the same variable ζ_{i}). The definition of the predicate Norm, computing in its third argument the most descriptive type between the first two, is given as follows:

{Norm(X, X, X) : −V ar(X),!.} ∪

{Norm(X, Y, X) : −Y == ⊥_{τ} ,!.} ∪

{Norm(Y, X, X) : −Y == ⊥_{τ} ,!.} ∪

\{ \begin{matrix}Norm(tname(ζ_{1_{1}}, ..., ζ_{1_{n}}), tname(ζ_{2_{1}}, ..., ζ_{2_{n}}), tname(ζ_{3_{1}}, ..., ζ_{3_{n}})) : − \\ Norm(ζ_{1_{1}}, ζ_{2_{1}}, ζ_{3_{1}}), ..., Norm(ζ_{1_{n}}, ζ_{2_{n}}, ζ_{3_{n}}),!. \\ where tname(ζ_{1}, ..., ζ_{n}) is a parametric type. \end{matrix} \} ∪

{Norm(X, X, X).}

The first clause says that the most descriptive type between two variables is a variable, while the next two state that ⊥_{τ} is less descriptive than any other type. A recursive definition of Norm is associated with each parametric declared type name. In this case the computation is recursively performed on the type structure. The last clause states that the most descriptive type between a type name and a variable is the type name itself, and that two different type names have not a most descriptive type.

Example 2 Let us consider the type declarations given in Example 1. The associated logic program P^{τ} is:

\begin{matrix}T ype(X, X) : −V ar(X),!. \\ T ype(nat, nat) : −!. \\ T ype(list(X), list(X)) : −!. \\ T ype(0, nat). \\ T ype(s(X), nat) : −T ype(X, nat). \\ T ype(nil, list(⊥_{τ})). \\ T ype(cons(X, Y), list(W)) : −T ype(X, Z), T ype(Y, list(T)), Norm(Z, T, W). \end{matrix} \begin{matrix}Norm(X, X, X) : −V ar(X),!. \\ Norm(X, Y, X) : −Y == ⊥_{τ} ,!. \\ Norm(Y, X, X) : −Y == ⊥_{τ} ,!. \\ Norm(list(X), list(Y), list(Z)) : −Norm(X, Y, Z),!. \\ Norm(X, X, X). \end{matrix}

Using P^{τ} the type of the term cons(nil, cons(s(0), nil)) can be obtained as the computed answer substitution for the goal : −T ype(cons(nil, cons(cons(s(0), nil), nil)), X) that is {list(list(nat))/_{X}}.

Thus, the Prolog program P^{τ}, associated with a set of type declarations for a logic program P, gives a procedural method to compute the type for any term belonging to the universe of terms of P.

As in the concrete case, the notion of “equivalence up renaming” ∼ can be also applied to type terms.

Definition 4.1 A term t ∈ T_{Σ}(V ar) is reducible to the type τ (t has type τ) iff

: −T ype(t, X) →_{P^{τ}}^{∗}^{ϑ} □ and ϑ(X) ∼ τ. If : −T ype(t, X) →_{P^{τ}}^{∗} F ail, then t has type ERR.

Thus, given a term t belonging to the universe of terms associated with the program P, if t is reducible by means of P^{τ} to the type symbol τ, the term is well-typed and its type is denoted by τ. Note also that if the given term is not reducible to any type name, its type is denoted by ERR. In the following we denote T_{Ω}(V ar_{τ}) ∪ {ERR} as T_{Ω}(V ar_{τ}).

Theorem 4.2 Consider a goal of the form : −T ype(t, t′) and the Prolog program P^{τ}. The computation of the goal terminates and, in case of success, it gives a unique computer answer substitution.

Proof. It comes from the definition of P^{τ}. □

Thus, P^{τ} completely characterizes the type of terms. Let us consider the equivalence relation ≈_{τ} over the universe T_{Σ}(V ar) induced by the program P^{τ}, such that ∀t_{1}, t_{2} ∈ T_{Σ}(V ar), t_{1} ≈_{τ} t_{2} iff

• : −T ype(t_{1}, α_{1}) →_{P^{τ}}^{∗}^{ϑ} □ ∧ : −T ype(t_{2}, α_{2}) →_{P^{τ}}^{∗}^{σ} □ : ϑ_{|α_{1}} ∼ σ_{|α_{2}}, or

• : −T ype(t_{1}, α_{1}) →_{P^{τ}}^{∗} F ail ∧ : −T ype(t_{2}, α_{2}) →_{P^{τ}}^{∗} F ail.

The quotient set T_{Σ}(V ar)_{/≈_{τ}} represents the set of all equivalence classes each of them containing terms having the same type (in the following the equivalence class of a term t (the type of t) will be denoted by [t]_{≈_{τ}}).

Definition 4.3 A type substitution (denoted by ϑ^{τ}) is a mapping from a finite set of type variables to T_{Ω}(V ar_{τ}).

Definition 4.4 A ⊥_{τ} substitution (denoted by η^{⊥_{τ}}) is a set of subterm descriptions {d_{1}^{τ}, ..., d_{n}^{τ}}. Each subterm description is a finite sequence of naturals numbers identifying a specific subterm.

For example the sequence ⟨3, 2⟩ means “ the subterm which is the second argument of the third argument” of the original term.

Definition 4.5 The application of a ⊥_{τ} substitution η^{⊥_{τ}} to a type term τ results in a term τ′ in which all the subterms described in η^{⊥_{τ}} (and occurring in τ) are replaced by ⊥_{τ}.

For example the application of η^{⊥_{τ}} = {⟨1, 1⟩} to the type term list(list(list(nat))) results in list(list(⊥_{τ})).

Definition 4.6 (preordering relation among type terms) Given two type terms τ_{1} and τ_{2}, τ_{1} ⪯_{τ} τ_{2} iff either τ_{2} = ERR or there exist ϑ_{τ} (type substitution) and η^{⊥_{τ}} (substitution of ⊥_{τ} for terms) such that τ_{1} ∼ (τ_{2}ϑ_{τ})η^{⊥_{τ}}.

For example the type term τ_{1} = list(⊥_{τ}) is smaller than τ_{2} = list(list(nat)) because there exist ϑ^{τ} = {} and η^{⊥_{τ}} = {⟨1⟩} such that (τ_{2}ϑ^{τ})η^{⊥_{τ}} = list(⊥_{τ}). In the following, with abuse of notation, we use ⪯_{τ} as an ordering relation on T_{Ω}(V ar_{τ}). We denote by ∼_{τ} the equivalence relation induced by the symmetric closure of ⪯_{τ}. Notice that τ_{1} ∼_{τ} τ_{2} iff τ_{1} ∼ τ_{2}. The least upper bound with respect to ⪯_{τ} is denoted ⊔_{τ}.

Theorem 4.7 There exists D ⊆ T_{Ω}(V ar_{τ}) such that D/_{∼_{τ}} and T_{Σ}(V ar)/_{≈_{τ}} are isomorphic.

Proof. It follows by defining D/_{∼_{τ}} as:

\{ [τ]_{∼} | \begin{matrix}t ∈ T_{Σ}(V ar) \\ : −T ype(t, τ) →_{P^{τ}}^{∗} □ \end{matrix} \} ∪ \{ERR\}

The mapping from T_{Σ}(V ar)/_{≈_{τ}} to D/_{∼}, given by the program, is injective by Theorem 4.2 and by definition of ≈_{τ}. Surjectivity follows by definition. □

Thus, any equivalence class [t]_{≈_{τ}} can be represented as a term in T_{Ω}(V ar_{τ})/_{∼}, denoting the type of the term. ERR denotes the equivalence class of terms with a wrong type structure with respect to the type declarations. Since all the definitions we consider are independent on any particular choice of the elements in the equivalence classes modulo ∼, we will denote by τ the equivalence class [τ]_{∼}.

Theorem 4.8 For each τ_{1}, τ_{2} ∈ D/_{∼}, τ_{1} ⊔_{τ} τ_{2} ∈ D/_{∼}.

Proof. We need the following recursive definition of terms corresponding to a type τ in a term t: denoted {t}_{τ}.

• {t}_{τ} = {t} if [t]_{≈_{τ}} = τ (t has type τ);

• {t}_{τ} = ∅ if t has simple type τ′ and τ′ ≠ τ or t has type ϕ( ¯⊥) and τ ≠ ϕ( ¯⊥);

• {f(t_{1}, ..., t_{m})}_{τ} = ∪_{i=1}^{m} {t_{i}}_{τ} otherwise

The theorem is proved by constructing a term t with type τ = τ_{1} ⊔_{τ} τ_{2}.

By definition let i = 1, 2 and ϑ_{i}^{τ}, η_{i}^{⊥_{τ}} such that τ_{1} = (τϑ_{1}^{τ})η_{1}^{⊥_{τ}} and τ_{2} = (τϑ_{2}^{τ})η_{2}^{⊥_{τ}}. Let us consider the terms t̃_{1} and t̃_{2} obtained by substituting each term in {t_{i}}τ̃_{j} with a fresh variable X, where {τ̃_{j}/_{α}} ∈ ϑ_{i}^{τ}. Each η_{i}^{⊥_{τ}} identifies a class of subtypes in τ, such that the corresponding type in τ_{i} is a constant in a parametric type definition: tname( ¯⊥_{τ}). The term t is constructed by taking either t̃_{1} or t̃_{2} (consider t̃_{1}) and by substituting each term in {t̃_{i}}_{tname( ¯⊥_{τ})} with a term such that the type of the resulting term is τ. These terms exist since t̃_{2} does contain them by l.u.b. definition.

□

Definition 4.9 (type patterns) A n-type pattern is a n-tuple (τ_{1}, ..., τ_{n}) of type terms.

The previous notions of type reduction and ordering extend naturally on any tuples of (concrete) terms and on type patterns respectively. With abuse of notation, the domain of n-type patterns D^{n}/_{∼} is denoted D^{n} and by ⊥_{τ}^{n} we denote the n-type pattern (⊥_{τ} , ..., ⊥_{τ}).

Proposition 4.10 Let n be a finite natural number. D^{n} ∪ {⊥_{τ}^{n}} is an infinite complete lattice with respect to the ⪯_{τ} ordering relation.

Proof. It is a straigthforward consequence of the previous theorem. □

Example 3 Let us consider the type definitions given in Example 1, the complete lattice of types is given in Figure 1.

[figure: ⊥_{τ}; list(⊥_{τ}); list(list(α)); list(nat); list(α); nat; ERR; α...; .......]

Figure 1. The lattice of types: D.

4.3 Abstract domain

The above domain of type patterns is characterized by an infinite number of elements. In order to obtain an abstract domain usable in abstract interpretation, we have to define a finite approximation of this infinite lattice of types. Let us consider a recursive function depth : T_{Ω}(V ar_{τ}) → ω such that ∀τ ∈ T_{Ω}(V ar_{τ}):

1. depth(τ) = 0 iff τ is a type variable, ⊥_{τ} or a simple (non parametric) type,

2. depth(τ) = 1 + max{depth(τ_{1}), ..., depth(τ_{n})} iff τ = ϕ(τ_{1}, ..., τ_{n}), where ϕ is a parametric type name.

A finite domain of type patterns is obtainable by extending the depth notion on type patterns and by cutting at depth-k the corresponding infinite lattice of types. Thus, given a positive integer k, let us define D_{k}^{n} ⊆ D^{n} as follows:

Definition 4.11 D_{k}^{n} = Cut_{k}(D^{n}), where Cut_{k}((τ_{1}, ..., τ_{n})) is the set of type patterns (τ_{1}^{k}, ..., τ_{n}^{k}) such that τ_{i}^{k} is obtained by substituting with a fresh variable each subtype τ′ in τ such that, depth(τ) − depth(τ′) = k.

Proposition 4.12 D_{k}^{n} is a finite complete lattice with respect to ⪯_{τ} ordering relation.

Example 4 The finite complete lattice of types corresponding to the previous infinite one, with n = 1 and k = 3, is given in Figure 2.

[figure: ⊥_{τ}; list(⊥_{τ}); list(list(⊥_{τ})); list(list(list(α))); list(list(nat)); list(list(α)); list(nat); list(α); nat; α...; ERR]

Figure 2. The approximated lattice of types for k = 3: D_{3}^{1}

We can now consider the approximated lattice of type patterns as the basis to construct abstract atoms.

Definition 4.13 α_{τ} : T_{Σ}(V ar)^{n} → D_{k}^{n} is such that ∀t̄∈ T_{Σ}(V ar)^{n}: α_{τ} (t̄) = Cut_{k}([t̄]_{≈_{τ}}).

The domain of abstract τ-interpretations is composed by atoms defined on type patterns. The abstract base B_{P}^{k} is defined as follows:

Definition 4.14 (base of abstract τ-interpretations)

B_{P}^{k} = \{ p(τ_{1}, ..., τ_{n}) | \begin{matrix}p ∈Π^{n}_{P} \\ (τ_{1}, ..., τ_{n}) ∈ D_{k}^{n} \end{matrix} \} .

Thus an abstract atom is a predicate symbol in the language applied to a type pattern.

A well-typed atom is an abstract atom having no ERR types in the corresponding pattern. The notion of well-typed atoms extends naturally to any syntactic object.

Definition 4.15 An abstract τ-interpretation I^{τ} for the polymorphic type inference is any subset of the abstract base.

Proposition 4.16 (℘(B_{P}^{k}), ⊆) is a finite lattice.

The relation between the concrete (infinite) lattice of (standard) interpretations, (℘(B_{P}), ⊆) and (℘(B_{P}^{k}), ⊆) is established by a Galois insertion. Let

• α : (℘(B_{P}), ⊆) → (℘(B_{P}^{k}), ⊆) such that:

α(I) = \{ p(Ψ) | \begin{matrix}p(t_{1}, ..., t_{n}) ∈ I \\ Ψ = α_{τ} (t_{1}, ..., t_{n}) \end{matrix} \};

• γ : (℘(B_{P}^{k}), ⊆) → (℘(B_{P}), ⊆) such that

γ(I^{τ}) = ∪ { I | α(I) ⊆ I^{τ} } .

Theorem 4.17 The pair (α, γ) is a Galois insertion of (℘(B_{P}^{k}), ⊆) into (℘(B_{P}), ⊆).

Proof. Notice that α is additive: let D ⊆ ℘(B_{P}) be a possibly denumerable collection of concrete interpretations {I_{1}, ..., I_{n}, ..}. p(Ψ) ∈ α(∪D) iff ∃p(t_{1}, ..., t_{n}) ∈ ∪D ∧ Ψ = α_{τ} (t_{1}, ..., t_{n}) iff

∃I ∈ D such that p(t_{1}, ..., t_{n}) ∈ ∪D ∧ Ψ = α_{τ} (t_{1}, ..., t_{n}) iff p(Ψ) ∈ ∪_{I∈D} α(I).

• α and γ monotonicity follows by definition.

• By α additivity:

α(γ(I^{τ})) = α(∪ { I | α(I) ⊆ I^{τ} }) = I^{τ}

• γ(α(I)) ⊇ I follows by definition.

□

4.4 Abstract interpretation and type inference

In this section we analyze the abstract operators involved in the definition of the associated abstract interpretation. Following the framework in [3], we define an abstract unification operator and a type substitution application. These operators allow to define an abstract immediate consequence operator whose least fixpoint is a correct approximation of the concrete success set.

Definition 4.18 (abstract unification) Let p(t_{1}, ..., t_{n}) and p(τ_{1}, ..., τ_{n}), be respectively a concrete and an abstract atom. We define the goal:

G^{τ} = {: −T ype(t_{1}, τ_{1}), ..., T ype(t_{n}, τ_{n})}.

The abstract unification is defined as follows:

α − mgu(p(t_{1}, ..., t_{n}), p(τ_{1}, ..., τ_{n})) = \{ \begin{matrix}ϑ^{τ} & G^{τ} →_{P^{τ}}^{∗}^{ϑ} □ ∧ ϑ^{τ} = ϑ_{|(t_{1},...,t_{n})} \\ F ail & otherwise \end{matrix}

α-mgu returns a type substitution defined on the set of variable symbols belonging to the concrete atom. It is easy to extend the previous definition to any number of concrete and abstract atoms to unify.

Let us consider now the α-apply operator which “applies” a type substitution ϑ^{τ} to a concrete atom p(t_{1}, ..., t_{n}). By considering the logic program associated with the type definition section, we can give a procedural method to compute the operator.

Definition 4.19 (type substitution application) Given a concrete atom p(t_{1}, ..., t_{n}) and a type substitution ϑ^{τ},

α − apply(p(t_{1}, ..., t_{n}), ϑ^{τ}) = {p(Cut_{k}((τ_{1}, ..., τ_{n})))}

where {τ_{1}/_{ζ_{1}}, ..., τ_{n}/_{ζ_{n}}} is the answer substitution computed in P^{τ} by the goal

{: −T ype(t_{1}ϑ^{τ} , ζ_{1}), ..., T ype(t_{n}ϑ^{τ} , ζ_{n})}

If the computation fails, α-apply returns a type pattern having the extra type symbol ERR for each subgoal which fails (this actually requires a proof procedure quite different from the standard one, but it is easy to define a meta interpreter to do it).

The computation of α-apply is always finite. The result is the type configuration of the predicate arguments. Moreover α-apply reports any type-error occurring during the substitution application.

According to the bottom-up abstract interpretation framework in [3], we can specialize the general abstract transformation map associated with any logic program.

Definition 4.20 The mapping T_{P}^{τ} : ℘(B_{P}^{k}) → ℘(B_{P}^{k}) is defined as follows:

T_{P}^{τ} (I^{τ}) = \{ α − apply(H, ϑ^{τ}) | \begin{matrix}C = H ← B_{1}, ..., B_{n} ∈ P \\ ⟨B_{1}^{τ} , ..., B_{n}^{τ}⟩ <<_{C} I^{τ} \\ ϑ^{τ} = α − mgu((B_{1}, ..., B_{n}), (B_{1}^{τ} , ..., B_{n}^{τ})) \\ ϑ^{τ} ≠ F ail \end{matrix} \} .

Where << extends naturally on type variables as well as concrete variables and selects only the well-typed atoms in I^{τ}.

Theorem 4.21 T_{P}^{τ} is monotonic on (℘(B_{P}^{k}), ⊆).

Proof. Let I_{1}^{τ} ⊆ I_{2}^{τ}. With an abuse of notation let us denote by

α − mgu((B_{1}, ..., B_{n}), I) = \{ ϑ^{τ} | \begin{matrix}⟨B_{1}^{τ} , ..., B_{n}^{τ}⟩ <<_{C} I \\ ϑ^{τ} = α − mgu((B_{1}, ..., B_{n}), (B_{1}^{τ} , ..., B_{n}^{τ})) \\ ϑ^{τ} ≠ F ail \end{matrix} \} .

Thus: α−mgu((B_{1}, ..., B_{n}), I_{1}) ⊆ α−mgu((B_{1}, ..., B_{n}), I_{2}). The thesis follows by α-apply definition. □

Corollary 4.22 Under the previous hypothesis, there exists a positive integer h such that lfp(T_{P}) = T_{P} ↑ h.

Let us denote SS_{P}^{τ} the lfp(T_{P}^{τ}). The meaning of our type system is more formally given by the following theorem, which establishes the connection between (concrete) successful derivations and the abstract success set SS_{P}^{τ}.

Let us denote as G ⇝_{P}^{∗}^{ϑ} □ a well-typed successful derivation, namely a sequence of goals G_{1}, ..., G_{m} containing only well-typed atoms.

Theorem 4.23 (Soundness) Let P be a logic program and let G be a goal : −B_{1}, ..., B_{n}. If G ⇝_{P}^{∗}^{ϑ} □, then there exist ⟨B_{1}^{τ} , ..., B_{n}^{τ}⟩ <<_{G} SS_{P}^{τ} such that α-mgu((B_{1}, ..., B_{n})θ, (B_{1}^{τ} , ..., B_{n}^{τ})) ≠ F ail.

Proof. The proof is in the Appendix. □

SS_{P}^{τ} contains polymorphic type patterns for each predicate symbol. It provides a description of the success set in terms of well-typed terms. It is easy to observe that greater is the description limit k, greater results the type information associated with the abstract interpretation. A good choice of the description limit k may be k > max { pdepth(A) | A is an atom defined in P }, where, given an atom p(t_{1}, ..., t_{n}): pdepth(p(t_{1}, ..., t_{n})) = max{depth(t_{i})}_{i∈{1,...,n}}.

4.5 Examples

In this section we analyze some examples of type inference in HCL. In our T_{P}^{τ} -based analysis, all the types of success patterns are generated.

Example 5 Let us consider the following logic program:

        append(nil,X,X).
        append(cons(X,Y),Z,cons(X,U)):-append(Y,Z,U).

whose domain of types is built starting from the following type declarations:

type nat :  type list(a)
0 → nat  nil → list(⊥_{τ})
s(nat) → nat  cons(α, list(α)) → list(α)
end  end

Using the definition (with k = 2) we compute the abstract success set in two steps

1. T_{P}^{τ} (∅) = {append(list(⊥_{τ}), β, β)};

2. T_{P}^{τ} (T_{P}^{τ} (∅)) = {append(list(⊥_{τ}), β, β), append(list(ζ), list(ζ), list(ζ))}.

3. T_{P}^{τ} (T_{P}^{τ} (T_{P}^{τ} (∅))) = T_{P}^{τ} (T_{P}^{τ} (∅)). (fixpoint)

In fact, from the first clause in the program we have T_{P}^{τ} (∅). To compute T_{P}^{τ} (T_{P}^{τ} (∅)) we have to consider that

α − mgu(append(y, z, u), append(list(⊥_{τ}), β, β)) = {list(⊥_{τ})/_{y}, β/_{z}, β/_{u}}.

and

α − apply(append(cons(x, y), z, cons(x, u)), {list(⊥_{τ})/_{y}, β/_{z}, β/_{u}}) =
{append(list(ζ), list(ζ), list(ζ))}.

The abstract success set gives the type structure of the predicate append, i.e. all the well-typed solutions of goals are instances of these type patterns. This example points out also a problem in this definition of append: there are possible solutions which are instances of the pattern append(list(⊥_{τ}), β, β). In fact the goal append(nil,s(0),s(0)) is provable in contrast to the intuition. The following definition of append overcomes this problem.

    append(nil,nil,nil).
    append(nil,cons(X,Y),cons(X,Y)):-append(nil,Y,Y).
    append(cons(X,Y),Z,cons(X,U)):-append(Y,Z,U).

The abstract success sets is

SS_{P}^{τ} = \{ \begin{matrix}append(list(⊥_{τ}), list(⊥_{τ}), list(⊥_{τ})) \\ append(list(⊥_{τ}), list(α), list(α)) \\ append(list(α), list(⊥_{τ}), list(α)) \\ append(list(α), list(α), list(α)) \end{matrix} \} .

This example shows that type inference can be used as a tool for verifying the relations between the implementation and the intuition about a program.

The following example shows the approximation level introduced by depth-k abstraction.

Example 6 Let us consider the logic program:

    iszero(0).
    p(cons(X,Y)):-iszero(X).
    p(cons(cons(X,Y),Z)):-p(cons(X,Y)).

with the previous type definitions. Given a finite positive integer k, we obtain in k + 1 steps the following sequence:

T_{P}^{τ} ↑ 1 = {iszero(nat)};

T_{P}^{τ} ↑ 2 = {iszero(nat), p(list(nat))}

T_{P}^{τ} ↑ 3 = {iszero(nat), p(list(nat)), p(list(list(nat)))};

........

T_{P}^{τ} ↑ (k + 1) = {iszero(nat), p(list(nat)), p(list(list(nat))), ..., p(list^{k}(α))};

T_{P}^{τ} ↑ (k + 2) = T_{P}^{τ} ↑ (k + 1) (fixpoint)

The approximation of the cut at depth-k is introduced because the type of predicate p is the infinite set {nat, list(nat), list(list(nat)), ...}, which is not computable in a finite number of steps.

Example 7 Let us consider a program (studied in [19]), still based on the previous type declarations:

    map-plus(nil,X,nil).
    map-plus(cons(X,Y),z,cons(U,W)):-plus(X,Z,U),map-plus(Y,Z,W).
    plus(0,X,X).
    plus(s(X),Y,s(Z)):-plus(X,Y,Z).

The abstract success set for the program is computed as follows

T_{P}^{τ} ↑ 1 = {map − plus(list(⊥_{τ}), β, list(⊥_{τ})), plus(nat, δ, δ)};

T_{P}^{τ} ↑ 2 = \{ \begin{matrix}map − plus(list(⊥_{τ}), β, list(⊥_{τ})) \\ map − plus(list(nat), ζ, list(ζ)) \\ plus(nat, δ, δ) \\ plus(nat, nat, nat) \end{matrix} \}.

T_{P}^{τ} ↑ 3 = \{ \begin{matrix}map − plus(list(⊥_{τ}), β, list(⊥_{τ})) \\ map − plus(list(nat), ζ, list(ζ)) \\ map − plus(list(nat), nat, list(nat)) \\ plus(nat, δ, δ) \\ plus(nat, nat, nat) \end{matrix} \}.

T_{P}^{τ} ↑ 4 = T_{P}^{τ} ↑ 3 (fixpoint)

The abstract success set shows that in any refutation for predicate map-plus, if the second argument has type α, the third one has result of type list(α), and viceversa, while there is a successful computation with any term as second argument if both the first and the third are nil.

The difference with [19] is that, by using bottom-up abstract interpretation, we obtain goalindependent information: given any goal, the type of the possible type-correct solutions is obtained by abstractly unifying it with atoms in SS_{P}^{τ}, as proved in Theorem 4.23. Thus, given the goal :-

map-plus(X,s(0),Y):

α-mgu(map-plus(X, s(0), Y), map-plus(list(nat), ζ, list(ζ))) = {list(nat)/_{X}, list(nat)/_{Y} }, α-mgu(map-plus(X, s(0), Y), map-plus(list(nat), nat, list(nat))) = {list(nat)/_{X}, list(nat)/_{Y} }, α-mgu(map-plus(X, s(0), Y), map-plus(list(⊥), ζ, list(⊥))) = {list(⊥)/_{X}, list(⊥)/_{Y} }, we obtain that list(nat) and list(⊥) are the type informations associated with the variables X and Y, in the success hypothesis.

The following example shows the treatment of type-errors in our approach and introduces some problems related with the use of our type system. In the following section we will discuss the possibility, given by the abstract interpretation framework, to extend the type inference system to overcome these problems.

Example 8 Consider the following simple program:

  p(cons(a,nil)).
  p(cons(0,X)) :- p(X).

with the type declarations

type nat :  type list(α)  type char
0 → nat  nil → list(⊥_{τ})  a → char
s(nat) → nat  cons(α, list(α)) → list(α)  ...
end  end  z → char

end

The type inference system returns the following abstract success set:

SS_{P}^{τ} = {p(list(char)), p(ERR)}.

The atom p(ERR) comes from the second clause in which the argument of the head should be a list containing both characters and natural numbers. The type of this list cannot be approximated by list(α). In our system the type list(α) represents the class of lists with elements of any type, but homogeneous. Thus list(α) indicates the lists of natural numbers and the lists of characters but not the lists of naturals and characters.

The type inference does not capture the possibility of computing heterogeneous (from a type viewpoint) structures. All the heterogeneous structures are mapped into the ERR class.

5 Modifying the Type Inference

In this section we discuss possible changes of the type inference system. Due to the underlying abstract interpretation framework, such changes are achieved by modifying the domain of types. The first extension deals with the problem of decomposing the ERR class into different, more descriptive, subclasses. The second change provides a description of the whole success set and allows a stronger notion of soundness.

5.1 Decomposing the ERR class

Example 8 of the previous section shows that the result of type inference could be improved: the ERR class is too comprehensive. In order to have a more precise approximation of the success set, the type inference scheme can be extended to capture the type of heterogeneous data structures.

Such a type inference may be defined by allowing type union in the domain of types. The idea is to define a new domain of types in which the most descriptive type between two uncomparable types is not ERR but the type union of them. Thus, in the new domain, types are seen as sets, although, abusing the notation we omit the {} parentheses for singletons. In Example 8 the most descriptive type between list(char) and list(nat) should be list(char ∪ nat), which describes heterogeneous lists with both character and natural numbers as elements. It is conceptually easy to extend the Prolog program P^{τ} to cope with ∪. We omit such a definition here because the program is very long inspite of its conceptual simplicity. Let us denote, with abuse of notation, as T_{Ω}(V ar_{τ}) the domain of type terms extended with the ∪ (idempotent, commutative and associative) binary type constructor. According to this view, the new preordering relation on types is: ∀τ_{1}, τ_{2} ∈ T_{Ω}(V ar_{τ}), τ_{1} ⪯_{∪} τ_{2} iff one of the following conditions hold:

• there exist ϑ^{τ} and η^{⊥_{τ}} such that τ_{1} ∼ (τ_{2}ϑ^{τ})η^{⊥_{τ}},

• τ_{1} = f(τ′_{1}, ..., τ′_{n}), τ_{2} = f(τ′′_{1}, ..., τ′′_{n}) and τ′_{i} ⪯_{∪} τ′′_{i} ∀i ∈ {1, ..., n},

• ∀τ′_{1} ∈ τ_{1}, ∃τ′_{2} ∈ τ_{2} such that τ′_{1} ⪯_{∪} τ′_{2}.

The previous ordering extends naturally on type patterns. The domain of type patterns (D^{n}) is a subset of T_{Ω}(V ar_{τ})^{n}/_{∼_{∪}}, isomorphic to T_{Σ}(V ar)^{n}/_{≈_{τ}}, where

∀τ_{1}, τ_{2} ∈ T_{Ω}(V ar_{τ})^{n}, τ_{1} ∼_{∪} τ_{2} iff τ_{1} ⪯_{∪} τ_{2} and τ_{2} ⪯_{∪} τ_{1}.

As an example, in the domain D, the types τ_{1} = list(α) ∪ list(nat) and τ_{2} = list(α) are identified because τ_{1} ∼_{∪} τ_{2}. The same holds for τ_{1} = list(nat) and τ_{2} = list(nat ∪ ⊥_{τ}). The depth-k approximation is exactly the same as in the previous case. Note that we have an ERR equivalence class which is smaller then the previous one because we obtain a set of equivalence classes associated with each heterogeneous type structure.

Example 9 Let us consider the type declarations

type nat :  type list(α) :
0 → nat  nil → list(⊥_{τ})
s(nat) → nat  cons(α, list(β)) → list(α ∪ β)
end  end

Given k = 3, the corresponding abstract domain of types is shown in Figure 3.

[figure: ⊥_{τ}; list(⊥_{τ}); list(list(⊥_{τ})); nat; nat ∪ list(⊥_{τ}); list(list(nat)); list(list(list(α))); list(list(α)); list(nat ∪ list(α)); list(nat); list(α); nat ∪ list(list(α)); ERR; nat ∪ list(nat); nat ∪ list(α); α...]

Figure 3. The modified finite lattice of types: D_{3}^{1}

By considering this new domain we have that the term cons(0, cons(cons(0, nil), nil), nil) has type list(nat ∪ list(nat)) while the term cons(0, 0) has type ERR. Example 10 Consider the following program, where 1 means s(0), 2 means s(s(0)) and so on:

plus(0,X,X).
plus(s(X),Y,s(Z)) :- plus(X,Y,Z).

char_weight(a,1).
char_weight(b,2).
...
char_weight(z,26).
word_weight(nil,0).
word_weight(cons(X,Y),W) :-   char_weight(X,S),
                              word_weight(Y, V),
                              plus(S,V,W).
map_weight(nil,nil).
map_weight(cons(X,Z),cons(X,cons(Y,W))) :-   word_weight(X,Y),
                                             map_weight(Z,W).

with the type declarations

type nat :  type list(α)  type char
0 → nat  nil → list(⊥_{τ})  a → char
s(nat) → nat  cons(α, list(β)) → list(α ∪ β)  ...
end  end  z → char

end

The predicate map weight is intended to build (given a list of words) a new list in which every word is followed by its weight (the sum of the weights of its characters). Using the new domain of types the approximated success set for the program is:

SS_{P}^{τ} = \{ \begin{matrix}plus(nat, δ, δ) \\ plus(nat, nat, nat) \\ char weight(char, nat) \\ word weight(list(⊥_{τ}), nat) \\ word weight(list(char)), nat) \\ map weight(list(⊥_{τ}), list(⊥_{τ})) \\ map weight(list(list(⊥_{τ})), list(list(⊥_{τ}) ∪ nat)) \\ map weight(list(list(char)), list(list(char) ∪ nat)) \end{matrix} \} .

Frm the type inference we can deduce that the solutions of goals for the predicate map weight have the following three possible forms:

1. if the first argument is a nil value, then the second is a nil value; or 2. if the first argument is a list of nil values, then the second argument results in a list in which

the elements are either nil values or natural numbers; or

3. if the first argument is a list of words (lists of characters), then the second argument results in a list of words and natural numbers.

It is important to remark that with the domain of types for homogeneous data-structures, the type of map weight would be

\{ \begin{matrix}map weight(list(⊥_{τ}), list(⊥_{τ})) \\ map weight(list(list(⊥_{τ})), ERR) \\ map weight(list(list(char)), ERR) \end{matrix} \} .

5.2 Capturing the whole success set

The approximated description of the success set provided by the type inference for heterogeneous data-structures, does not capture the possibility of type-wrong solutions. Consider the program composed by the only clause p(cons(0,Y)) in the world of homogeneous lists. Its approximated success set is SS_{P}^{τ} = {p(list(nat))}. Consider now the goal :- p(cons(X,cons(a,Z))) which is not abstractly unifyable with p(list(nat)), but, despite of this, it is refutable. Its refutation leads to the answer substitution {0/_{X}} which, applied to the goal, makes it not well-typed. The origin of this behaviour is considering more descriptive a type name than a variable. In fact, the reduction of p(cons(0, X)) leads p(cons(nat, list(α))) which is reduced to p(list(nat)). This reduction is based on the idea of homogeneity of lists: if one element is a natural number, the others must have the same type. The reduction is also based on the idea that, in the term cons(0, X), X must be a list. To obtain an approximation of the whole success set (thus providing a stronger notion of correctness) we have to change completely the point of view. We have to consider descriptivity as comprehensivity. Following this view, lists are heterogeneous and a variable represents terms of any type, and not only the ones leading to type-correct solutions. For the previous one-clause program, p(cons(0, X)) can be reduced to p(cons(nat, α)); and, because α can be any type, the atom has to be reduced to the types cons(nat, α). SS_{P}^{τ} is now {p(list(α)), p(list(nat)), p(ERR)} which means that the solutions for p are heterogeneous lists, list of naturals or type-wrong solutions. However, this SS_{P}^{τ} does not give the idea that type-wrong solutions are obtained only by starting with typewrong goals. Although this type inference captures the whole success set, we still consider that the abstract scheme we presented in Section 4 is more useful to understand and to reason about programs. Goals not abstractly unifyable with atoms in the abstract success have no solutions or only type-wrong solutions. In a sense, these goals “do not correspond to the philosophy of the program”.

These two informally described extensions give the idea of the flexibility of the approach. Due to the bottom-up abstract interpretation scheme, modifications of the type inference can be achieved by modifying the abstract domain.

6 Concluding Remarks

In this paper we have presented a polymorphic type inference scheme for logic programs. It can handle both parametric polymorphism and type union, which denote essential aspects in the logic programming style. The approach is based on a bottom-up abstract interpretation technique which is able to collect information on the whole success set of the program independently from the possible goals submitted to the refutation process. Moreover, by allowing non-ground terms into the semantics, we obtain an approach to the polymorphism with a clear declarative foundation. We have considered a depth-k abstraction technique [32] to get finite domains. Different techniques can be used for this purpose, like the widening/narrowing-based approach in [9] to ensure the termination of the abstract interpretation on the infinite lattice of (all) types. By considering a different (compositional) underlying semantics [4], our type inference can be adapted to deal with program modules, thus allowing more powerful analysis like compositional type inference of logic programs and inter-modules type checking, as recently proposed in [8].

There are several directions for further research. It is be possible to extend our type inference scheme to meta predicates. New type constructors should be included in the domain of types, like predn(α_{1}, ..., α_{n}), denoting the type of n-ary predicates. Moreover we should extend the type declarations to predicates too.

Our type inference, together with a suitable type declaration for predicates, may be usefully used in program debugging and in compiler optimizations. In particular, since it returns an abstract type version of the success set of the program, we observe the applicability of the inferred type information to statically handle (at compile time) AND-parallelism in logic programming, as in determining errors between consumer and producer interchange [16]. Another interesting application of the derivation of polymorphic types in HCL is about the interconnection between first order logic and discrete programming [18]. To limit the potentially exponential growth in these methods, in fact, we can usefully use the concept of type for predicate variables and constants. This technique is widely-used for curtailing instantiations of the first order logic into the propositional one. Thus, it restricts the number of possible instantiation of predicates, in order to apply quantitative methods (e.g. mathematical programming) instead of the usual inefficient symbolic calculation.

Appendix

We prove a weak notion of soundness for the abstract interpretation (Theorem 4.23) with respect to the following T_{P} -based semantics capturing “well-typed” derivations.

Definition 6.1 (T_{P}^{wt} operator) Let us consider I ∈ ℘(B_{P}):

T_{P}^{wt}(I) = \{ Aϑσ | \begin{matrix}C : A : −B_{1}, ..., B_{n} ∈ P, ⟨B′_{1}, ..., B′_{n}⟩ <<_{C} I \\ (B_{1}, ..., B_{n})ϑ = B′_{1}, ..., B′_{n} \\ (B_{1}, ..., B_{n})ϑ is well-typed \\ dom(σ) ⊆ vars(A) − vars(B_{1}, ..., B_{n}) \\ A well-typed ⇒ Aσ well-typed \end{matrix} \}

Proposition 6.2 T_{P}^{wt} is continuous on (℘(B_{P}), ⊆).

Proof. The proof is standard [12]. □

The fixpoint of T_{P}^{wt} is the set of atoms (ground or non-ground) with successful well-typed derivations. The following theorem specifies the soundness of T_{P}^{wt}-based semantics with respect to the semantics of well-typed derivations.

Theorem 6.3 Let P be a logic program. If p(t̄) ⇝_{P}^{∗}^{ϑ} □ then p(t̄)ϑ ∈ T_{P}^{wt} ↑ ω.

Proof. By induction on the lenght n of the derivation (⇝^{n}):

• base case: p(t̄) ⇝_{P}^{ϑ} □ then p(t̄)ϑ is a well-typed instance of a unit clause in P. Thus p(t̄)ϑ ∈ T_{P}^{wt} ↑ ω;

• inductive case: p(t̄) ⇝_{P}^{n+1}^{ϑ} □, then there exists a clause C : p(t̄′) : −B_{1}, ..., B_{n} ∈ P such that

p(t̄) ⇝_{P}^{ϑ′} B_{1}, ..., B_{n} ⇝_{P}^{n}^{ϑ′′} □

where p(t̄)ϑ′ = p(t̄′)ϑ′ and ϑ = ϑ′ϑ′′. For each i = 1..n: B_{i}ϑ′ϑ′′ ⇝_{P}^{n_{i}}^{ε} □ and n_{i} ≤ n (see [12]). By the inductive hypothesis, (B_{1}, ..., B_{n})ϑ ∈ T_{P}^{wt} ↑ ω and is well-typed. By T_{P}^{wt} definition, we have p(t̄′)ϑ ∈ T_{P}^{wt} ↑ ω.

□

The proof of the Theorem 4.23 is based on the following Lemma:

Lemma 6.4 ∀n ∈ ω, ∀p(t̄) ∈ T_{P}^{wt} ↑ n, ∃p(τ̄) ∈ T_{P}^{τ} ↑ n such that α-mgu(p(t̄), p(τ̄)) ≠ F ail.

Proof. By induction on n:

• base case: straightforward.

• inductive case: let p(t̄)ϑσ ∈ T_{P}^{wt} ↑ (n + 1) = T_{P}^{wt}(T_{P}^{wt} ↑ n). By definition:

C : p(t̄) : −B_{1}, ..., B_{n} ∈ P, ⟨B′_{1}, ..., B′_{n}⟩ <<_{C} T_{P}^{wt} ↑ n (B_{1}, ..., B_{n})ϑ = B′_{1}, ..., B′_{n}, (B_{1}, ..., B_{n})ϑ is well-typed dom(σ) ⊆ vars(t̄) − vars(B_{1}, ..., B_{n}), p(t̄) well-typed ⇒ p(t̄)σ well-typed

By the inductive hypothesis B_{1}^{τ} , ..., B_{n}^{τ} ∈ T_{P}^{τ} ↑ n and

α − mgu((B′_{1}, ..., B′_{n}), (B_{1}^{τ} , ..., B_{n}^{τ})) ≠ F ail.

Then: α − mgu((B_{1}, ..., B_{n})ϑ, (B_{1}^{τ} , ..., B_{n}^{τ})) ≠ F ail. Since (B_{1}, ..., B_{n})ϑ is well-typed, then:

α − mgu((B_{1}, ..., B_{n}), (B_{1}^{τ} , ..., B_{n}^{τ})) = ϑ^{τ} ∧ ϑ^{τ} ≠ F ail.

Thus: α-apply(p(t̄), ϑ^{τ}) ∈ T_{P}^{τ} ↑ (n + 1). We prove that: α − mgu(p(t̄)ϑσ, α − apply(p(t̄), ϑ^{τ})) ≠ F ail. This is equivalent to prove that ^{1} α − mgu(p(t̄)ϑ, α − apply(p(t̄), ϑ^{τ})) ≠ F ail. Assume that α − mgu(p(t̄)ϑ, α − apply(p(t̄), ϑ^{τ})) = F ail, then there exist t/_{x} ∈ ϑ_{|(t̄)} and τ/_{x} ∈ ϑ^{τ} such that x ∈ vars(B_{1}, ..., B_{n}) and

: −T ype(t, τ) ⇝_{P^{τ}}^{∗} F ail.

Thus α − mgu((B_{1}, ..., B_{n})ϑ, (B_{1}^{τ} , ..., B_{n}^{τ})) must fail, leading to a contradiction.

□

Theorem 4.23 (Soundness) Let P be a logic program and let G be a goal : −B_{1}, ..., B_{n}. If G ⇝_{P}^{∗}^{ϑ} □, then there exists ⟨B_{1}^{τ} , ..., B_{n}^{τ}⟩ <<_{G} SS_{P}^{τ} such that α-mgu((B_{1}, ..., B_{n})θ, (B_{1}^{τ} , ..., B_{n}^{τ})) ≠ F ail. Proof.

It follows by Theorem 6.3, T_{P}^{wt} continuity and Lemma 6.4. □

1Notice that if a well-typed term t has type τ, any well-typed instance tμ has type τ′ and there exists a type substitution μ^{τ} such that τμ^{τ} = τ′.

References

[1] S. Abramsky and C. Hankin. An Introduction to Abstract Interpretation. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 9–31. Ellis Horwood Ltd, 1987.

[2] R. Barbuti, R. Giacobazzi, and G. Levi. A Declarative Abstract Semantics for Logic Programs. In A. Bertoni, C. Böhm, and P. Miglioli, editors, Proc. of the Third Italian Conference on Theoretical Computer Science, pages 84–96. World Scientific, 1989.

[3] R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs. Technical Report TR 12/91, Dipartimento di Informatica, Università di Pisa, 1991. To appear in ACM Transactions on Programming Languages and Systems.

[4] A. Bossi, M. Gabbrielli, G. Levi, and M. C. Meo. Contributions to the Semantics of Open Logic Programs. Technical Report TR 17/91, Dipartimento di Informatica, Università di Pisa, 1991. To appear in Proc. FGCS ’92.

[5] M. Bruynooghe and G. Janssens. An Instance of Abstract Interpretation Integrating Type and Mode Inferencing. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 669–683. The MIT Press, Cambridge, Mass., 1988.

[6] M. Bruynooghe, G. Janssens, B. Demoen, and A. Callebaut. Abstract Interpretation: Towards the Global Optimization of Prolog Programs. In Proc. Fourth IEEE Int’l Symp. on Logic Programming, pages 192–204. IEEE Comp. Soc. Press, 1987.

[7] M. Codish, D. Dams, and E. Yardeni. Bottom-up Abstract Interpretation of Logic Programs. Technical report, Dept. of Computer Science, The Weizmann Institute, Rehovot, 1990. To appear in Theoretical Computer Science.

[8] M. Codish, S. Debray, and R. Giacobazzi. Compositional Analysis of Modular Logic Programs. Technical Report, Dipartimento di Informatica, Università di Pisa, 1992.

[9] P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. Fourth ACM Symp. Principles of Programming Languages, pages 238–252, 1977.

[10] P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. Sixth ACM Symp. Principles of Programming Languages, pages 269–282, 1979.

[11] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. A new Declarative Semantics for Logic Languages. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 993– 1005. The MIT Press, Cambridge, Mass., 1988.

[12] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative Modeling of the Operational Behavior of Logic Languages. Theoretical Computer Science, 69(3):289–318, 1989.

[13] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. A Model-Theoretic Reconstruction of the Operational Semantics of Logic Programs. Technical Report TR 32/89, Dipartimento di Informatica, Università di Pisa, 1989. To appear in Information and Computation.

[14] M. Gabbrielli and G. Levi. On the Semantics of Logic Programs. In J. Leach Albert, B. Monien, and M. Rodriguez-Artalejo, editors, Automata, Languages and Programming, 18th International Colloquium, volume 510 of Lecture Notes in Computer Science, pages 1–19. Springer-Verlag, Berlin, 1991.

[15] Y. Gang and X. Zhiliang. An Efficient Type System for Prolog. In Proc. IFIP Congress 86, pages 355–359, 1986.

[16] R. Giacobazzi and L. Ricci. Pipeline Optimizations in AND-Parallelism by Abstract Interpretation. In D. H. D. Warren and P. Szeredi, editors, Proc. Seventh Int’l Conf. on Logic Programming, pages 291–305. The MIT Press, Cambridge, Mass., 1990.

[17] M. Hanus. Horn Clause Programs with Polymorphic Types: Semantics and Resolution. In Proc. of TAPSOFT 89, volume 351 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1989.

[18] R. Jeroslow. Computation-oriented Reduction of Predicate to Propositional Logic. Technical report, Georgia Institute of Technology - Atlanta, 1985.

[19] T. Kanomori and K. Horiuchi. Polymorphic Type Inference in Prolog by Abstract Interpretation. In Logic Programming 87- Tokyo, volume 315 of Lecture Notes in Computer Science, pages 195–214. Springer-Verlag, Berlin, 1988.

[20] R. Kemp and G. Ringwood. An Algebraic Framework for the Abstract Interpretation of Logic Programs. In S. Debray and M. Hermenegildo, editors, Proc. North American Conf. on Logic Programming’90, pages 506–520. The MIT Press, Cambridge, Mass., 1990.

[21] F. Kluźniak. Type Synthesis for Ground Prolog. In J.-L. Lassez, editor, Proc. Fourth Int’l Conf. on Logic Programming, pages 788–816. The MIT Press, Cambridge, Mass., 1988.

[22] J.-L. Lassez, M. J. Maher, and K. Marriott. Unification Revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Los Altos, Ca., 1988.

[23] D. Leivant. Polymorphic Type Inference. In Proc. Tenth ACM Symp. Principles of Programming Languages, pages 88–98, 1983.

[24] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.

[25] K. Marriott and H. Søndergaard. Bottom-up Abstract Interpretation of Logic Programs. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 733–748. The MIT Press, Cambridge, Mass., 1988.

[26] K. Marriott and H. Søndergaard. On Describing Success Patterns of Logic Programs. Technical Report 12, The University of Melbourne, 1988.

[27] A. Melton, D.A. Schmidt, and G.E. Strecker. Galois Connections and Computer Science Applications. In D. Pitt et al., editor, Category Theory and Computer Programming, volume 240 of Lecture Notes in Computer Science, pages 299–312. Springer-Verlag, Berlin, 1986.

[28] R. Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and Systems Sciences, 17-3:348–375, 1978.

[29] P. Mishra. Towards a Theory of Types in Prolog. In Proc. 1st IEEE Symp. Logic Programming, pages 289–298, 1984.

[30] A. Mycroft and R.A. O’Keefe. A Polymorphic Type System for Prolog. Artificial Intelligence, 23:295– 307, 1984.

[31] C. Pyo and U.S. Reddy. Inference of Polymorphic Types for Logic Programming. In E. Lusk and R. Overbeck, editors, Proc. North American Conf. on Logic Programming’89, pages 1115–1132. The MIT Press, Cambridge, Mass., 1989.

[32] T. Sato and H. Tamaki. Enumeration of Success Patterns in Logic Programs. Theoretical Computer Science, 34:227–240, 1984.

[33] M. H. van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. Journal of the ACM, 23(4):733–742, 1976.

[34] J. Xu and D.S. Warren. A Type Inference System for Prolog. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 604–619. The MIT Press, Cambridge, Mass., 1988.

[35] E. Yardeni and E. Shapiro. A Type System for Logic Programs. Journal of Logic Programming, 10:125–135, 1991.

[36] J. Zobel. Derivation of Polymorphic Types for Prolog Programs. In J.-L. Lassez, editor, Proc. Fourth Int’l Conf. on Logic Programming, pages 817–838. The MIT Press, Cambridge, Mass., 1988.