AUGMENTED PROLOG — AN EVOLUTIONARY APPROACH

KARL STROETMANN AND THOMAS GLAß

Siemens AG, Corporate Research and Development, D–81730 Munich^{∗}

Abstract. Prolog has been marketed as a declarative programming language. In practical programming, however, this pretension is seldom justified. There are many reasons for the gap between the theory of logic programming and the practice of Prolog, the most important being the lack of a type system and the fact that the hitherto developed declarative semantics for Prolog makes no attempt to capture the meaning of the cut operator. This paper shows a way of equipping Prolog with a declarative semantics that takes the effects of the cut operator into consideration. This approach offers a possibility of reconciling Prolog and logic programming.

1. Introduction

Fifteen years ago, when the Japanese fifth generation computer project started, many of the augurs prophesied that Prolog would soon oust conventional imperative languages. Today, these prophecies have turned out to be wrong. Prolog is by far not as well accepted as imperative programming languages. There are many reasons that have led to this situation. However, the most important ones are the following:

1. Prolog is not suitable for large industrial applications since current Prolog compilers offer less support to detect errors than compilers for more conventional languages. This is due to the lack of types in Prolog. It precludes the use of Prolog in certain fields of applications where, for safety reasons, the use of strongly typed languages is mandatory.

2. Commercially available programming environments for Prolog are not as sophisticated as, e.g. environments for C.

3. Contrary to the claims sometimes heard in the logic programming community, Prolog is not a declarative language. This can be mainly attributed to three reasons:

(a) The lack of types.

(b) The completion semantics is too complicated to be supported effectively by tools for program verification.

(c) The cut operator is not dealt with satisfactorily in the theory of logic programming. The above mentioned problems have been known for several years and have given rise to a bewildering multitude of new logic programming languages. To name but a few there is Mercury [SHC94], Gödel [HL94], Protos–L [Bei95], etc. On the technical side, these new proposals for a logic programming language address the problems stated above. Unfortunately, each of these proposals solves a different subset of the problems mentioned above and none of them solves all. But even if there were a proposal that would solve all the problems in a satisfactory manner, then it would still be doubtful whether any of these proposals could have commercial success in the near future. There are two reasons for this assessment. First, in an industrial context it is at least difficult, if not impossible, to use software that is not commercially supported. Secondly, a number of fields of applications, particularly those with a safety–critical context, require the use of standardized programming languages. It does not seem likely that a standard for a Prolog successor will be available in the near future. After all, it has taken more than five years to arrive at an ISO–standard for Prolog. But then, what is the solution? We do not want to discourage research groups to carry on developing their “pet” successor of Prolog. However, in an industrial context we should stay with Prolog for some time. In order to solve the problems with existing Prolog implementations we recommend the following solution.

∗ E-mail: Karl.Stroetmann@zfe.siemens.de.

1. Augment Prolog programs with mode and type information. Nearly all of the proposals for a successor to Prolog have identified the lack of a type system as a serious problem of Prolog. However, we do not need to invent a new language to add a type system to logic programming. Our approach is to add type information as special comments so that a conventional Prolog interpreter will ignore them. Then a special type checker can be used as a preprocessor to check the type correctness of the programs annotated this way.

There are two conflicting requirements for a type system. First, a type system should be expressive. Secondly, it should be computationally feasible to check whether a program is well–typed. Obviously, the question whether a program is well–typed gets more complicated as the type language gets more expressive. Concerning the expressiveness of a type system, we consider the following features a necessity for a type system to be useful in practice:

• parametric polymorphism,

• inclusion polymorphism,

• support of types containing non–ground terms.

2. In order to develop sophisticated tools capable of analyzing Prolog programs and spotting many more errors than just type error, it is useful to restrict the use of Prolog. Backtracking is a useful feature and the concept of a Prolog variable is very powerful. However, when these features are used arbitrarily the resulting programs become both incomprehensible and unmaintainable. Therefore it is a good advise to use a functional programming style whenever this is suitable. Predicates that are functional should be declared as functional. This offers the possibility of a tool checking various properties of functional predicates, e.g. it is possible to check functional predicates for the property of being completely defined and for termination.^{1}

3. Furthermore, using a functional programming style offers the possibility of developing a suitable declarative semantics for Prolog that takes care of the cut operator. Fortunately, it turns out that, when used with a certain discipline, cut operators give rise to a declarative semantics that is simpler than the completion semantics! The reason is that a large number of Prolog predicates are really functional, i.e. most predicates return exactly one result for every type correct instantiation of their input arguments. This behaviour is usually achieved by equipping each Prolog clause implementing a functional predicate with a cut operator. Then, if certain other conditions are satisfied, the cut gives rise to a local semantics. This semantics is local because every clause is translated into a single formula. Note that this is not the case with the completion semantics. With completion semantics, the set of all clauses implementing a predicate is taken together to arrive at the declarative semantics. The details of our new declarative semantics are presented in [SG95]. The basic idea is as follows. A (propositional) clause

p ← q_{1}, ⋯, q_{m},!, r_{1}, ⋯, r_{n}

is interpreted as the formula

q_{1} ∧ ⋯ ∧ q_{m} ⇒ (p ↔ r_{1} ∧ ⋯ ∧ r_{n}).

The semantics sketched above is only correct if the underlying program is subject to certain conditions outlined in [SG95], but then this is also true for the completion semantics.

In the rest of this paper we will describe the new declarative semantics sketched above in more detail. Our declarative semantics builds upon the type system described in [Apt93]. We introduce the necessary notions and notations together with this type system in the next section. The declarative semantics will then be introduced in the third section. The fourth section discusses an implementation of our system. In the final section we compare our approach with similar approaches recently discussed in the literature and suggest directions for future work.

1Of course, these properties are undecidable in general. However, when a certain programming style is adhered to it is well possible to check these properties in most interesting cases. Compare, e.g. the work of Gröger and Plümer [GP92] or, more recently, Müller [Mül95].

2. Preliminaries

All notions and notations not defined in this paper are assumed to be the same as in Apt [Apt90]. We will only deviate in a small number of points from [Apt90], the most important being that we use modes and types which will be defined below. Another deviation is the fact that we do not use goals but rather find it more convenient to work with queries. A query is taken to be a list of literals separated by commas. If L_{1}, ⋯, L_{m} is a query, then it will be interpreted as the conjunction L_{1} ∧ ⋯ ∧ L_{m}. Furthermore, we will use the following meta rule for denoting sequences of items: If the items from a class are denoted by a fixed group of letters, then sequences of these items will be denoted by the same letters in boldface. For example, since s and t denote terms, s and t will be used to denote sequences of terms.

2.1. Modes and Types. As already noted by others, compare e. g. [Apt93], in order to develop a declarative semantics for Prolog one has to introduce the concept of modes [DM85] and types [MO84]. We find it convenient to use the notion of a well–typed program as given in Apt and Etalle [AE93]. This paper is itself based on the paper by Bronsard, Lakshman and Reddy [BLR92]. However, in contrast to [BLR92] we use only types that denote sets of ground terms. We plan to extend our approach to the general case.

We start with the notion of a mode used to define input and output positions of a relation.

Definition 1 (mode). A mode for an n–ary relation symbol p is a function m_{p} from the set {1, ⋯, n} to the set {+, −}. If m_{p}(i) = “+”, we call i an input position of p and if m_{p}(i) = “−”, we call i an output position of p. A moding is a collection of modes, each for a different relation symbol. □

We proceed to define types. Since we do not intend to present a new type system here, the only assumption we make is that a type is a decidable set of ground Prolog terms. The set of all types will be denoted by 𝔗. Individual types will be written as σ and τ.

Definition 2 (type). A type for an n–ary relation symbol p is a function t_{p} from the set {1, ⋯, n} to the set 𝔗. If t_{p}(i) = τ, we call τ the type associated with the position i of p. A typing is a collection of types, each for a different relation symbol. □

The mode and the type of a relation are the components of the signature of the relation.

Definition 3 (signature). A signature for an n–ary relation symbol p is a function s_{p} from the set {1, ⋯, n} to the set {+, −} × 𝔗 such that s_{p}(i) is the pair ⟨m_{p}(i), t_{p}(i)⟩, where m_{p} and t_{p} are the mode and the type of the relation p. Instead of the clumsy ⟨m_{p}(i), t_{p}(i)⟩ we will write s_{p}(i) as the string m_{p}(i)t_{p}(i). A signature for a Prolog program ℙ is a collection of signatures for the relation symbols of ℙ. □

If p is an n–ary relation with mode m_{p} and type t_{p}, the signature of p will be written as

p( m_{p}(1) t_{p}(1), ⋯, m_{p}(n) t_{p}(n) ).

A typed term is a construct of the form s: σ where s is a term and σ is a type. Given a sequence s_{1} :σ_{1}, ⋯, s_{n}:σ_{n} of typed terms we write s ∈ σ where s abbreviates s_{1}, ⋯, s_{n} and σ abbreviates σ_{1}, ⋯, σ_{n} iff for all i = 1, ⋯, n we have s_{i} ∈ σ_{i}. A type judgment is a statement of the form s:σ ⇒ t:τ. It is considered to be true (notation ⊧ s:σ ⇒ t:τ) iff for all substitutions ϑ, sϑ ∈ σ implies tϑ ∈ τ.

In the definition below we will write l to denote either a predicate symbol p or a negated predicate symbol ¬p. We will assume that if a relation p is used negatively, i.e. as ¬p(s), then p has only input positions, i.e. its signature is given by

p( +σ ).

Definition 4 (well–signed). In the following, assume that for i = 0, 1, ⋯, n the signature of the relation symbol p_{i} is given by

p_{i}( +σ_{i}, −τ_{i} ).

• A clause p_{0}(t_{0}, s_{n+1}) ← l_{1}(s_{1}, t_{1}), ⋯, l_{n}(s_{n}, t_{n}) is well–signed iff the following conditions are satisfied for all i ∈ {1, ⋯, n + 1}:

1. FV(s_{i}) ⊆ ⋃_{j=0}^{i−1} FV(t_{j}).

2. ⊧ t_{0} :τ_{0}, ⋯, t_{i−1} :τ_{i−1} ⇒ s_{i}:σ_{i}.

• A query l_{1}(s_{1}, t_{1}), ⋯, l_{n}(s_{n}, t_{n}) is well–signed iff the clause

true ← l_{1}(s_{1}, t_{1}), ⋯, l_{n}(s_{n}, t_{n})

is well–signed.

• Finally, a program is called well–signed if every clause of it is. □

The concept of well–signedness can best be understood in terms of the notion of earlier positions. Intuitively, the position of a term s is earlier than the position of a term t in a query Q if during the computation of an answer for Q the variables in s will be instantiated earlier than the variables appearing in t. To define this notion formally, let us assume that for i = 0, 1, ⋯, n the signatures of the relation symbols p_{i} are given by

p_{i}( +σ_{i}, −τ_{i} ).

Then, if either Q is a query of the form l_{1}(s_{1}, t_{1}), ⋯, l_{n}(s_{n}, t_{n}), or if C is a clause of the form p_{0}(t_{0}, s_{n+1}) ← l_{1}(s_{1}, t_{1}), ⋯, l_{n}(s_{n}, t_{n}), then for all i = 1, ⋯, n we have the following:

• The positions of the terms in t_{0} are earlier than the positions of the terms in s_{i}, t_{i}, and s_{n+1}.

• The positions of the terms in t_{0}, s_{i}, and t_{i} are earlier than the positions of the terms in s_{n+1}.

• The positions of the terms in s_{i} are earlier than the positions of the terms in t_{i}.

• If j < i the positions of the terms in s_{j} and t_{j} are earlier than the positions of the terms in

s_{i} and t_{i}. Furthermore, if we have a query of the form l_{1}(s_{1}, t_{1}), ⋯, l_{n}(s_{n}, t_{n}), or a clause of the form p_{0}(t_{0}, s_{n+1}) ← l_{1}(s_{1}, t_{1}), ⋯, l_{n}(s_{n}, t_{n}), let us define the positions in the terms s_{i} as input positions and the positions in the terms t_{i} as output positions. Then it is easy to see that a clause or a query is well–signed iff the following two conditions are satisfied:

1. If s is a term appearing at an input position and X is a variable in FV(s), then there has to exist a term t at an earlier output position such that X is in FV(t).

2. If s is a term appearing at an input position with associated type σ, then we have to be able to show s: σ from the assumption that all terms appearing at earlier output positions have the types associated with these positions.

For the next subsection we will need the notion of simply–moded queries and clauses. This notion is due to Apt and Etalle [AE93]. A well–signed query or clause is called simply–moded iff the terms appearing at output positions are distinct variables that have not occurred at earlier positions. Variables of this type will also be called fresh variables. A program is called simply–moded iff all of its clauses are simply–moded.

2.2. Clean Programs. The declarative semantics to be developed in the next section requires the programs to adhere to a certain standard. Since this standard precludes arbitrary backtracking it is not possible for the implementation of every predicate to adhere to this standard. Therefore we classify the predicates of a program as functional and backtrackable. Basically, we classify all those functions as functional that are not backtrackable. The declarative semantics to be developed can only be used for functional predicates.

We will need a condition that ensures certain recursive definitions to be well–defined. To this end we assume that there is a function

level : Σ → ℕ

mapping the predicate symbols to the non–negative integers. This function is extended to literals in the obvious way. We call a clause of the form

P ← L_{1}, ⋯, L_{m},!, H_{1}, ⋯, H_{n}

nicely–stratified iff the following conditions hold:

1. The predicates occurring in L_{i} and H_{j} are classified as functional for all i = 1, ⋯, m and j = 1, ⋯, n.

2. The clause contains exactly one occurrence of the cut operator, i.e. none of the L_{i} or H_{j} is a cut.

3. level(L_{i}) < level(P) for all i = 1, ⋯, m.

4. level(H_{j}) ≤ level(P) for all j = 1, ⋯, n. If ℙ is a program, then ℙ_{n} denotes the subset of all clauses from ℙ that implement a predicate symbol of level less or equal to n. We call ℙ nicely–stratified iff every clause from ℙ that implements a functional predicate is nicely–stratified.

We proceed to give the definition of a clean program.

Definition 5 (clean program). A program ℙ is called clean iff the following conditions hold: • ℙ is well–signed.

• ℙ is simply–moded.

• ℙ is nicely–stratified.

• No clause that implements a backtrackable predicate contains a cut operator.

• Only functional predicates may be negated. Furthermore, we require ℙ to be terminating on every well–signed query.

In the following we make the assumption that all programs encountered are clean.

3. A Declarative Semantics for Clean Programs

Assume a predicate p with signature

p(+σ_{1}, ⋯, +σ_{m}, −τ_{1}, ⋯, −τ_{n}).

is given. Since we view predicates as representing the graph of partial functions we introduce n new function symbols p_{i}, for i = 1, ⋯, n and a new predicate symbol p_{def}. The signatures of these symbols are given as

p_{i} : σ_{1} × ⋯ × σ_{m} → τ_{i} for i = 1, ⋯, n;

p_{def} : σ_{1} × ⋯ × σ_{m}.

The relation between the predicate p and the symbols p_{def} and p_{i} is given by p(x_{1}, ⋯, x_{m}, y_{1}, ⋯, y_{n}) ↔ p_{def}(x_{1}, ⋯, x_{m}) ∧ p_{1}(x_{1}, ⋯, x_{m}) = y_{1} ∧ ⋯ ∧ p_{n}(x_{1}, ⋯, x_{m}) = y_{n} Since this formula is rather unreadable we will write it as

p(x, y) ↔ p_{def}(x) ∧ p(x) = y (1)

i.e. we use bold face notation to denote tuples.

We have two different types of function symbols: First, there are the function symbols that are used as Prolog term constructors. We will refer to them as constructor symbols. Secondly, there are the defined function symbols which are introduced when translating predicates according to (1). It is important to realize that the axioms of Clarks equational theory do only hold for the constructor symbols.

To proceed, let us assume that a clause of the form

p(s, x) ← l^{(1)}(t_{1}, y_{1}), ⋯, l^{(m)}(t_{m}, y_{m}), !, h^{(1)}(r_{1}, z_{1}), ⋯, h^{(n)}(r_{n}, z_{n}). (2)

is given, where the l^{(i)} and h^{(j)} denote either predicate symbols or negated predicate symbols. Furthermore, using the above notation we tacitly assume the first tuple of arguments to be placed at the input positions while the second tuple of arguments is placed at the output positions, e.g. in writing p(s, x) we assume that the components of the tuple s are placed at the input positions of p, while the components of x are placed at the output positions. Using this notation the understanding is, of course, that if l^{(i)} is a negated predicate symbols, then y_{i} is the empty string. A similar remark holds true for the h^{(j)}.

In order to translate (2) into a formula we define substitutions φ_{i} for i = 1, ⋯, m, ϑ_{j} for j = 1, ⋯, n and ϱ by induction. We will use the following notation: If q(u, v) is a predicate with m input positions and n output positions, then we write {v/q(u)} to denote the substitution {v_{1}/q_{1}(u), ⋯, v_{n}/q_{n}(u)}. The definition runs now as follows:

1. φ_{1} = {y_{1}/l^{(1)}(t_{1})}.

2. φ_{i+1} = φ_{i} ∪ {y_{i+1}/l^{(i+1)}(t_{i+1}φ_{i})} for i = 1, ⋯, m − 1.

3. ϑ_{1} = φ_{m} ∪ {z_{1}/h^{(1)}(r_{1}φ_{m})}.

4. ϑ_{j+1} = ϑ_{j} ∪ {z_{j+1}/h^{(j+1)}(r_{j+1}ϑ_{j})}. for j = 1, ⋯, n − 1.

5. ϱ = ϑ_{n}

Using these substitutions the clause (2) is translated into the formulas

l_{def}^{(1)}(t_{1}ϱ) ∧ ⋯ ∧ l_{def}^{(m)}(t_{m}ϱ) → (p_{def}(s) ↔ h_{def}^{(1)}(r_{1}ϱ) ∧ ⋯ ∧ h_{def}^{(n)}(r_{n}ϱ)) (3)

and

p_{def}(s) ∧ l_{def}^{(1)}(t_{1}ϱ) ∧ ⋯ ∧ l_{def}^{(m)}(t_{m}ϱ) → p(s) = xϱ (4)

In these formulas l_{def}^{(i)}(t_{i}ϱ) denotes q_{def}^{(i)}(t_{i}ϱ) if l^{(i)} is the predicate symbol q^{(i)} or, if l^{(i)} ≡ ¬q^{(i)},

then l_{def}^{(i)}(t_{i}ϱ) denotes the formula ¬q_{def}^{(i)}(t_{i}ϱ). We will refer to formula (3) as the definedness condition of p corresponding to the clause (2).

Observe that (4) can be regarded as a set of k conditional equations, where k is the number of output positions of p. Furthermore, if the symbol “↔” in formula (3) is interpreted as an equality symbol for Booleans, then formula (3) can be regarded as a conditional equation, too. If ℙ is a clean Prolog program, then we arrive at the declarative semantics decl(ℙ) of ℙ by transforming every clause of ℙ that implements a predicate classified as functional according to the procedure given above. Furthermore, by decl(ℙ_{n}) we denote the set of formulas resulting from transforming all those clauses that implement predicates of level less or equal to n.

In order for the transformation of clauses into formulas given above to be correct, the predicate symbols are required to be completely defined over their input types. This notion will be explained now: If the predicate symbol p with signature

p(+σ, −τ) and level(p) = n + 1

is implemented by k clauses and if the definedness condition resulting from clause number i is given as

B_{i} → (p_{def}(l_{i}) ↔ K_{i}),

then for every tuple of terms s of type σ we have to demonstrate an i ∈ {1, ⋯, k} and a substitution ϑ such that s ≡ l_{i}ϑ holds and, furthermore, we have to prove

decl(ℙ_{n}) ⊧ B_{i}ϑ.

Here the formula decl(ℙ_{n}) ⊧ B_{i}ϑ expresses the fact that we are able to prove B_{i}ϑ using the formulas of decl(ℙ_{n}) as assumptions.

The definedness condition guarantees that every case is dealt with. For the declarative semantics to be correct we also have to guarantee that all cases are dealt with consistently, i.e. we have to guarantee that the defined functions we have introduced are single valued. This gives rise to a consistency condition similar to the completeness condition just given. However, due to lack of space we will not discuss this condition here.

3.1. An Example. We close this section by presenting an example for the declarative semantics developed so far. Let us consider the familiar quick sort example. The signature of the predicate

quick sort is given by
  %# function: quick_sort( +int_list, -int_list ) never_fails.

where the type int list denotes the set of lists of integers. (The meaning of the attribute never fails will be explained in the next section.) If the type of integers is given by int then the type int list can be defined via the following recursive equation

  %# int_list := [] + [ int | int_list ].

In order to define quick sort we will need two auxiliary predicates, split and the well–known append. Their signatures are given as:

  %# function: split( +int, +int_list, -int_list, -int_list ) never_fails.
  %# function: append( +int_list, +int_list, -int_list ) never_fails.

The predicate split splits its input list into two lists, the first of which contains all elements less or equal than the integer argument of split while the second list contains the remaining arguments. The predicate split is implemented by the following clauses:

  split( X, [ Y | Ys ], [ Y | Small ], Big ) :-
            Y =< X,
            !,
            split( X, Ys, Small, Big ).
  split( X, [ Y | Ys ], Small, [ Y | Big ] ) :-
            not Y =< X,
            !,
            split( X, Ys, Small, Big ).
  split( X, [], [], [] ) :- !.

We have written this predicate in a way that it is invariant under permutation of the clauses. This forced us to introduce the redundant test “not Y =< X” in the second clause. This test is needed to make our declarative semantics consistent.

The clauses above are translated into the following conditional equations:

        split_{def}(X,[Y|Ys]) ∧ Y =< X → split_{1}(X,[Y|Ys]) = [ Y | split_{1}(X,Ys) ].

        split_{def}(X,[Y|Ys]) ∧ Y =< X → split_{2}(X,[Y|Ys]) = split_{2}(X,Ys).
     split_{def}(X,[Y|Ys]) ∧ ¬ Y =< X → split_{1}(X,[Y|Ys]) = split_{1}(X,Ys).
     split_{def}(X,[Y|Ys]) ∧ ¬ Y =< X → split_{2}(X,[Y|Ys]) = [Y|split_{2}(X,Ys)].
        split_{def}(X,[]) → split_{1}(X,[]) = [].
        split_{def}(X,[]) → split_{2}(X,[]) = [].

Furthermore, we give the definedness conditions for split. These are as follows:

        Y =< X → (split_{def}(X,[Y|Ys]) ↔ split_{def}(X,Ys)).

     ¬ Y =< X → (split_{def}(X,[Y|Ys]) ↔ split_{def}(X,Ys)).

split_{def}(X,[]).

Inspecting these conditions it is easily seen that split is defined for all its inputs, i.e. we have

split_{def}(X,Xs) = true for all X, Xs.

To complete this example we transform the clauses defining the predicate quick sort. The clauses implementing quick sort are:

          quick_sort( [ X | Xs ], Sorted ) :-
                    !,
                    split( X, Xs, Small, Big ),
                    quick_sort( Small, L1 ),
                    quick_sort( Big, L2 ),
                    append( L1, [ X | L2 ], Sorted ).
          quick_sort( [], [] ) :- !.

The declarative semantics of these clauses is:

quick sort_{1}( [X|Xs] ) = quick sort_{1}(split_{1}(X,Xs)) ∗ [ X | quick sort_{1}(split_{2}(X,Xs)) ]. quick sort_{1}( [] ) = [].

In the formula above we have taken the liberty of writing “∗” instead of “append_{1}” and using an infix notation for this function. Furthermore, we have dropped the definedness condition since the predicate quick sort trivially implements a total function. Finally, the formulas corresponding to the classical implementation of append are the following:

        [ X | Xs ] ∗ Ys = [ X | Xs ∗ Ys ].
        [] ∗ Ys = Ys.

3.2. A Refinement of the Declarative Semantics. In this section we have given the declarative semantics for clean programs. The condition that all clauses should be simply–moded which is a precondition for a program being clean precludes any form of unification. Since this is quite restrictive we have extended our semantics in a way such that this condition can be dropped. In order to do this we have given a declarative semantics to the process of unification. The basic idea is to interpret unifications either as tests for equality or as substitutions or, in the general case, as a mixture of both. Unfortunately, space does not permit us to give the details.

4. Implementation

In this section we describe the Prolog Analyzer (Pan for short) that we have built. Furthermore, we compare our approach with similar systems described in the literature. We will put special emphasis on a comparison with Mercury since we have found that this approach is quite similar to ours, the most notable exception being that the team developing Mercury had the freedom to design a new language while the necessities arising from our industrial context confined us to build our system around Prolog.

Pan is designed as a preprocessor. Its sole purpose is to spot errors. This is in contrast to systems like Mercury that use the type and mode information as a basis for various optimizations of the code generated by the Mercury compiler. The advantage of our approach is that we do not force our type system upon a user of our Prolog system: Anybody who wants to write quick–and–dirty prototypes is still able to do this without being bothered to give either mode or type information. The disadvantage of our approach is that, since the compiler has no access to the mode or type information, it is not possible to exploit this knowledge for the purpose of generating more efficient code.

In summary, Pan is able to check the following properties of programs:

1. type and mode correctness,

2. completeness of definitions, and

3. termination. Due to lack of space we will only discuss the first two points, the algorithm for checking the termination of a program is given in [Mül95].

4.1. Type and Mode Correctness. We have found it desirable to have a type system admitting both inclusion polymorphism and parametric polymorphism. This is not possible with the type system of Mycroft and O’Keefe [MO84] which is the basis of the type system implemented in Gödel and Mercury. With our type system which is based on Bronsard, Lakshman, and Reddy [BLR92] types can be defined in one of two ways. The first is exemplified by the definition of the polymorphic type list(T) that is given below:

  %# list(T) := [] + [ T | list(T) ].

Except for the syntax, this is the same as a definition of lists in either Gödel or Mercury and therefore need not be commented. The second way to define a type is exemplified by the definition of the type regexp (regular expressions) which runs as follows:

  %# regexp extends char by
  %#                cat(regexp,regexp) + or(regexp,regexp) + star(regexp).

This definition amounts to the following inductive definition of terms of type regexp: 1. Every character is a regular expression.

2. If R_{1} and R_{2} are terms of type regexp, then cat(R_{1},R_{2}), or(R_{1},R_{2}), and star(R_{1}) are

terms of type regexp. The definition of regexp turns the type char into a subtype of regexp. Therefore, a character can be used at every place where a term of type regexp is required.

As long as the type system admits only parametric polymorphism the type system and the mode system can easily be separated. This is no longer true when inclusion polymorphism enters the picture. The reason is that with inclusion polymorphism it is no longer possible to assign every variable of a clause a unique type. Rather, successive calls of predicates will delineate the type of a variable more and more. This is the reason that the type system is tightly coupled with the mode system in our approach, compare Definition 4. Therefore, in order to prevent the implementation of the resulting system from getting to complex, we have chosen a mode system that distinguishes only between input and output parameters. We plan to extend this system for future versions along the lines of the mode system implemented in Mercury.

Sometimes the type correctness of a program is not a local property. To see this, consider the following implementation of the predicate pp regexp/1 that could be used to pretty–print terms of the type regexp described earlier.

  %# predicate: pp_regexp( + regexp ).

  pp_regexp( cat( R1, R2 ) ) :-
      !,
      pp_regexp( R1 ),
      pp_regexp( R2 ).
  pp_regexp( or( R1, R2 ) ) :-
      !,
      write( '(' ),
      pp_regexp( R1 ),
      write( '|' ),
      pp_regexp( R2 ),
      write( ')' ).
  pp_regexp( star( R ) ) :-
      !,
      pp_regexp( R ),
      write( '*' ).
  pp_regexp( Char ) :-
      !,
      put_char( Char ).

Here the predicate put char/1 is a predicate with signature

  %# predicate: put_char( + char ).

The fact that the last clause of pp regexp/1 is type correct can not be seen locally. It rather follows from the fact that all the other cases are dealt with in the preceding clauses and that the predicate is deterministic. As it stands, the last clause would produce the error message

  error.pro:16: type mismatch: put_char/1, argno: 1, variable Char
  error.pro:16: expected char/0, found regexp/0

when analyzed with Pan. To prevent this error message we can change the last clause to the following:

  pp_regexp( Char ) :-
  %# Char :: char,
     !,
     put_char( Char ).

With the current implementation of Pan the type annotation “%# Char :: char” is not checked by the system. Instead, its correctness lies at the full responsibility of the user. Obviously, this is a weak point of our system. There are also other situations where an explicit type annotation is needed. These occur when second order predicates like findall/3, assertz/1, call/1 etc. are used in conjunction with the univ–operator =../2.

Mercury does not have an escape mechanism of the above kind. It does not need to have one, since all those constructs that do not fit into a declarative setting have been eliminated from the language. We are planning to extend our system in a way such that

• Most type annotations can be checked statically.

• Those type annotations that can not be established as true are replaced by a call to a predicate performing the type check at run time.

4.2. Completeness. We have integrated a small theorem prover into Pan that can be used to check the completeness condition given in Section 3. This theorem prover employs methods similar to those described in [BR91]. A complete description of this theorem prover will be given in a forthcoming paper.

On the surface, checking the completeness condition is akin to the checking of determinism in the Mercury compiler. With Mercury, predicates can be classified according to the categories det, semidet, multidet, and nondet corresponding to the fact that a predicate produces exactly one, at most one, at least one, or at least zero solutions. Mercury also has the determinism category erroneous corresponding to predicates whose computation does not terminate and failure for predicates that always fail. Up to now, we have only found it necessary to implement the first four of these categories. With our system, predicates can be classified as never fails, is complete, and as functional or backtrackable. Predicates need not be classified at all. These predicates correspond to predicates defined as nondet in Mercury.

With Pan, functional predicates are those that succeed at most once. If a functional predicate is given the attribute never fails, then we furthermore assert that the predicate will succeed exactly once, if it is attributed as is complete it may fail as well. Backtrackable predicates can produce an arbitrary number of solutions. However, if they are attributed as never fails they must produce at least one solution.

For functional predicates, the attribute never fails therefore resembles the attribute det of the Mercury compiler, for backtrackable predicates it resembles multidet. Similarly, for functional predicates, the attribute is complete resembles semidet, while for backtrackable predicates it resembles the nondet of Mercury.

For a predicate to be declared as is complete we have to check the completeness condition given in Section 3. This condition guarantees that every case is dealt with explicitly. In order for this condition to be true we have to include explicit failure clauses, i.e. the correctness of our implementation may not rely on the negation as failure semantics. For example, an implementation of the predicate member chk/2 checking for membership in a list would take the following form:

  %# test: member_chk( + list( T ), + T ) is_complete.
  member_chk( [ X | Xs ], Y ) :-
     X == Y,
     !.
  member_chk( [ X | Xs ], Y ) :-
     X \== Y,
     !,
     member_chk( Xs, Y ).
  member_chk( [], _) :-
     !,
     fail.

We had to add the last clause in order to justify the attribute is complete. Although writing programs in this spirit makes the resulting programs somewhat longer, we conclude from the experience gained so far that there is ample reward for this extra effort, especially when it comes to maintaining programs. The reason is that when changing some data type by adding an additional constructor, Pan readily spots all those predicates whose definitions have to be changed in turn. Another interesting observation made in this context is that as soon as the complexity of data types used exceeds a certain limit, programmers do tend to forget cases. Often, this does not result in an error on simple test examples since the same cases that were overlooked in the program will be overlooked when designing the examples. When we finished the first prototype of Pan we were quite surprised when Pan spotted missing cases in programs that had already been running for some time without showing any errors and whose correctness therefore had been taken for granted.

Furthermore, we have noticed that adding clauses providing negative information significantly increases the readability of the resulting programs.

When compared with the checking of determinism in Mercury [HSC95] our checking of the is complete attribute seems to be considerably stronger in recognizing the fact that a predicate is indeed completely defined. The reason is that, while the analysis performed by the Mercury compiler is purely syntactical, we use a simple albeit powerful theorem prover for recognizing the completeness of a predicate. Consider, for example, the following alternative version of the predicate split/4 described in Section 3.

          split( X, [ Y | Ys ], [ Y | Small ], Big ) :-
                    Y < X,
                    !,
                    split( X, Ys, Small, Big ).
          split( X, [ Y | Ys ], Small, Big ) :-
                    X == Y,
                    !,
                    split( X, Ys, Small, Big ).

          split( X, [ Y | Ys ], Small, [ Y | Big ] ) :-
                    Y > X,
                    !,
                    split( X, Ys, Small, Big ).
          split( X, [], [], [] ) :- !.

(This predicate would be used in a version of the quick sort algorithm that eliminates multiple occurrences of elements in a list.) Pan is able to establish the completeness of this definition since its theorem prover is able to recognize the formula x < y ∨ x = y ∨ x > y as valid. If the same predicate would have to be coded for the Mercury compiler it would be necessary to combine the first three clauses into a single clause using a nested if–then–else construction. We think that our version of the predicate is easier to read than the coding using a nested if–then–else construction. The reason is that with the above implementation every clause can be read separately, therefore the information is better localized than in the version using the if–then–else construction.

Furthermore, while an if–then–else construction is trivially complete, this is not the case with the programming style exhibited above since there every clause is guarded by the condition consisting of the conjunction of the predicates called before the cut is encountered. This gives Pan the possibility to spot errors that are quite subtle. This ability could be increased by checking not only the completeness but also the consistency of definitions. The latter would amount to checking that different clauses of a definition of a predicate do not overlap.

5. Conclusion

We have found that even a type system alone significantly increases the productivity of software development in Prolog. However, once Prolog programs are typed there is a lot more that can be done than mere type checking. Using the declarative semantics given in this paper we have developed a tool that is not only able to type check Prolog programs, but is also capable of checking functional predicates for being completely defined and terminating. Of course, these properties are, in general, undecidable. Nevertheless, this seems to be no problem in practice. In those (few) cases where either the termination or the completeness of a predicate can not be proven automatically the user can simply switch off the checking of these predicates.

The experience gained so far clearly shows that by checking automatically for completeness and termination of programs a lot of errors can be spotted automatically. This results in an increased productivity and leads to programs of a high quality. Especially when maintaining large Prolog programs this proves to be invaluable. This has been made possible by a declarative semantics capable of describing the effects of the cut operator. Although a lot of work has been going on in order to give a declarative semantics to the cut operator, compare e.g. [Bör89, PS95], previous approaches were only concerned with the operational semantics. Most probably the fact that previous authors confined themselves to an investigation of the operational semantics of the cut has its origin in the fact that a declarative semantics for an unrestricted use of the cut operator would be of prohibitive complexity. But the solution is not to abandon a declarative semantics altogether, one rather has to find sufficient conditions that enable the cut operator to be interpreted declaratively. We view the semantics suggested in the present paper as a promising step in this direction.

For the future, we plan to exploit the new declarative semantics of Prolog even more by building a system that can be used to verify Prolog programs. The reason we believe this to be possible is the fact that, with our declarative interpretation of Prolog programs, every clause is translated into a conditional equation. Now the work of Bouhoula et. al. [BR95] clearly shows that at least for specifications written as conditional equations computer aided verification is feasible.

Acknowledgments. The authors would like to thank Prof. Helmut Schwichtenberg and Andrea Engelhardt for carefully reading earlier versions of this paper. Furthermore, thanks go to Martin Müller for designing and implementing that part of Pan responsible for checking the termination of predicates.

References

[AE93] Krzysztof R. Apt and Sandro Etalle. On the unification free Prolog programs. In S. Sokolowski, editor, Proceedings of the Conference on Mathematical Foundations of Computer Science (MFCS ‘93), Lecture Notes in Computer Science. Springer Verlag, 1993. This paper is identical to report CS-R9331 of the CWI

in Amsterdam, the Netherlands. URL: http://www.cwi.nl/cwi/publications/index.html.

[Apt90] Krzysztof R. Apt. Logic programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, chapter 10, pages 495–574. Elsevier, 1990.

[Apt92] Krzysztof R. Apt, editor. Logic Programming. The MIT Press, 1992.

[Apt93] Krzysztof R. Apt. Declarative programming in Prolog. In D. Miller, editor, Proceedings of International Logic Programming Symposium (ILPS ‘93), Cambridge, Mass./London, 1993. The MIT Press. This paper is identical to report CS-R9353 of the CWI in Amsterdam, the Netherlands. URL:

http://www.cwi.nl/cwi/publications/index.html.

[Bei95] C. Beierle. Concepts, implementation, and applications of a typed logic programming language. In Beierle and Plümer [BP95], chapter 5, pages 139–167.

[BLR92] François Bronsard, T. K. Lakshman, and Uday S. Reddy. A framework of directionality for proving termination of logic programs. In Apt [Apt92], pages 321–335.

[Bör89] E. Börger. A logical operational semantics of full Prolog, part I: Selection core and control. In E. Börger, H. Kleine Büning, and M. M. Richter, editors, Computer Science Logic CSL ’89, pages 36–64. Springer-Verlag, Lecture Notes in Computer Science 440, 1989.

[BP95] C. Beierle and L. Plümer, editors. Logic Programming: Formal Methods and Practical Applications. Studies in Computer Science and Artificial Intelligence. Elsevier Science B.V./North-Holland, Amsterdam, Holland, 1995.

[BR91] Wadoud Bousdira and Jean-Luc Rémy. On sufficient completeness of conditional specifications. In Stéphane Kaplan and Mitsuhiro Okada, editors, Conditional and Typed Rewriting Systems, 2nd International Workshop, LNCS 516, pages 272–286. Springer-Verlag, 1991.

[BR95] Adel Bouhoula and Michaël Rusinowitch. Implicit induction in conditional theories. Journal of Automated Reasoning, 1995.

[DM85] P. Dembinski and J. Maluszynski. And–parallelism with intelligent backtracking for annotated logic programs. In Proceedings of the International Symposium on Logic Programming, 1985.

[GP92] Gerhard Gröger and Lutz Plümer. Handling of mutual recursion in automatic termination proofs for logic programs. In Apt [Apt92], pages 336–350.

[HL94] P.M. Hill and J.W. Lloyd. The Gödel Programming Language. MIT Press, 1994.

[HSC95] Fergus Henderson, Zoltan Somogyi, and Thomas Conway. Determinism analysis in the mercury compiler. Submitted for publication, 1995.

[MO84] Alan Mycroft and Richard A. O’Keefe. A polymorphic type system for Prolog. Artif. Intell., 23:295–307, 1984.

[Mül95] Martin Müller. Automatisierbare Terminierungsnachweise von Prolog–Programmen. Master’s thesis, Uni-

versität Marburg, 1995.

[PS95] Andreas Podelski and Gert Smolka. Operational semantics of constraint logic programs with coroutining. In Leon Sterling, editor, Proceedings of the 1995 International Conference on Logic Programming, pages 449–463, Kanagawa, Japan, 13–18 June 1995. The MIT Press.

[SG95] Karl Stroetmann and Thomas Glaß. A declarative semantics for Prolog. Technical report, Siemens AG, ZFE T SE 1, 81730 München, Germany, 1995. This paper is a draft in statu nascendi.

[SHC94] Zoltan Somogyi, Fergus Henderson, and Thomas Conway. The implementation of mercury: an efficient purely declarative logic programming language. In Proceedings of the ILPS ’94 Postconference Workshop on Implementation Techniques for Logic Programming Languages, 1994.