[To appear in: Formal Aspects of Computing, Springer-Verlag.]

Specification and correctness proof

of a WAM extension for

type-constraint logic programming

Christoph Beierle  Egon Börger
Fachbereich Informatik  Dipartimento di Informatica
FernUniversität Hagen  Università di Pisa
Bahnhofstr. 48  Corso Italia 40
D-58084 Hagen, Germany  I-56100 Pisa, Italia
beierle@fernuni-hagen.de  boerger@di.unipi.it

February 11, 1993; revised July 10, 1995

Abstract: We provide a mathematical specification of an extension of Warren’s Abstract Machine for executing Prolog to type-constraint logic programming and prove its correctness. Our aim is to provide a full specification and correctness proof of a concrete system, the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L.

In the first part of the paper, we keep the notion of types and dynamic type constraints rather abstract to allow applications to different constraint formalisms like Prolog III or CLP(R). This generality permits us to introduce modular extensions of Börger’s and Rosenzweig’s formal derivation of the WAM. Since the type constraint handling is orthogonal to the compilation of predicates and clauses, we start from type-constraint Prolog algebras with compiled AND/OR structure that are derived from Börger’s and Rosenzweig’s corresponding compiled standard Prolog algebras. The specification of the type-constraint WAM extension is then given by a sequence of evolving algebras, each representing a refinement level, and for each refinement step a correctness proof is given. Thus, we obtain the theorem that for every such abstract type-constraint logic programming system L, every compiler to the WAM extension with an abstract notion of types which satisfies the specified conditions, is correct.

In the second part of the paper, we refine the type constraints to the polymorphic order-sorted types of PROTOS-L. This allows us to develop a detailed, yet due to the use of evolving algebras, mathematically precise account of the PAM’s compiled type constraint representation and solving facilities, and to extend the correctness theorem to compilation on the fully specified PAM.

Acknowledgements: The first author was partially funded by the German Ministry for Research and Technology (BMFT) in the framework of the WISPRO Project (Grant 01 IW 206). He would also like to thank the Scientific Center of IBM Germany where the work reported here was started.

Contents

1 Introduction 1

PART I: Adding types constraints to Prolog and the WAM  5

2 PROTOS-L Algebras with compiled AND / OR structure 5 2.1 An abstract notion of type constraints . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.3 Choicepoints and Environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.4 Initial State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.5 Transition rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

3 Term representation 11 3.1 Universes and Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.3 Putting of terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.4 Getting of terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.5 Putting of Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

4 PAM Algebras 18 4.1 Environment and Choicepoint Representation . . . . . . . . . . . . . . . . . . . . . 18 4.2 Trailing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 4.3 Pure PROTOS-L theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

5 Additional WAM optimizations in the PAM 22 5.1 Environment Trimming and Last Call Optimization . . . . . . . . . . . . . . . . . 22 5.2 Initializing Temporary and Permanent Variables . . . . . . . . . . . . . . . . . . . 22 5.3 Switching instructions and the Cut . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.4 Main Theorem of Part I . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

PART II: Polymorphic, order-sorted type constraints  25

6 PAM algebras with monomorphic type constraints 25 6.1 Binding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6.2 Monomorphic, order-sorted types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 6.3 Representation of types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 6.4 Initialization of type constrained variables . . . . . . . . . . . . . . . . . . . . . . . 29 6.5 Binding of type constrained variables . . . . . . . . . . . . . . . . . . . . . . . . . . 29 6.6 Getting of structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

7 PAM Optimizations 33 7.1 Special representation for typed variables . . . . . . . . . . . . . . . . . . . . . . . 33 7.2 Switch on Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 8 Polymorphic type constraint solving 38

8.1 Representation of polymorphic type terms . . . . . . . . . . . . . . . . . . . . . . . 38 8.2 Creation of polymorphic type terms . . . . . . . . . . . . . . . . . . . . . . . . . . 39 8.3 Polymorphic infimum . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 8.4 Propagation of polymorphic type restrictions . . . . . . . . . . . . . . . . . . . . . 45 8.5 Main Theorem of Part II . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48

References 49

A Transition rules for compiled And/Or structure 51

B Transition rules for the PAM with abstract type terms of Part I 53 B.1 Low level unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 B.2 Putting and Getting Code . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 B.3 Putting of terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 B.4 Getting of terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 B.5 Unify instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 B.6 Environment and Choicepoint Representation . . . . . . . . . . . . . . . . . . . . . 57 B.7 Indexing and Switching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

1 Introduction

Recently, Gurevich’s evolving algebra approach ([Gur88]) has not only been used for the description of the (operational) semantics of various programming languages (Modula-2, Occam, Prolog, Prolog III, Smalltalk, Parlog, C; see [Gur91]), but also for the description and analysis of implementation methods: Börger and Rosenzweig ([BR91, BR92b, BR92a]) provide a mathematical elaboration of Warren’s Abstract Machine ([War83], [AK91]) for executing Prolog. The description consists of several refinement levels together with correctness proofs, and a correctness proof w.r.t. Börger’s phenomenological Prolog description ([Bör90a, Bör90b].

In this paper we demonstrate how the evolving algebra approach naturally allows for modifications and extensions in the description of both the semantics of programming languages as well as in the description of implementation methods. Based on Börger and Rosenzweig’s WAM description we provide a mathematical specification of a WAM extension to type-constraint logic programming and prove its correctness. Note that thereby our treatment can be easily extended to cover also all extra-logical features (like the Prolog cut) whereas the WAM correctness proof of [Rus92] deals merely with SLD resolution for Horn clauses.

The extension of logic programming by types requires in general not only static type checking, but types are also present at run time (see e.g. [MO84], [GM86], [NM88], [Han88], [Han91], [Smo89]). For instance, if there are types and subtypes, restricting a variable to a subtype represents a constraint in the spirit of constraint logic programming. PROTOS-L ([Bei92], [BBM91]) is a logic programming language that has a polymorphic, order-sorted type concept (similar to the slightly more general type concept of TEL [Smo88]) and a complete abstract machine implementation, called PAM ([BMS91], [BM94]) that is an extension of the WAM by the required polymorphic order-sorted unification. Our aim is to provide a full specification and correctness proof of the concrete PAM system.

In the first part of this paper, we keep the notion of types and dynamic type constraints rather abstract to allow applications to different constraint formalisms. Since the type constraint handling is orthogonal to the compilation of predicates and clauses, we start from type-constraint Prolog algebras with compiled AND/OR structure that are derived from Börger’s and Rosenzweig’s corresponding compiled standard Prolog algebras. The specification of the type-constraint WAM extension is then given by a sequence of evolving algebras, each representing a refinement level. For each refinement step a correctness proof is given. As final result of Part I of this paper we obtain the theorem: For every such abstract type-constraint logic programming system L and for every compiler satisfying the specified conditions, compilation from L to the the WAM extension with an abstract notion of types is correct.

Although our description in Part I is oriented towards type constraints, it is modular in the sense that it can be extended to other constraint formalisms, like Prolog III [Col90] or CLP(R) [JL87], [JMSY90], as well. For instance, in [BS95] a specification of the CLAM, an abstract machine for CLP(R), is given along these lines, together with a correctness proof for CLP(R) compilation. [Bei94] extends the work reported here by studying a general implementation scheme for CLP(X) and designing a generic extension WAM(X) of the WAM. Nevertheless, in order to avoid proliferation of different classes of evolving algebras, we will already speak here in Part I in terms of PROTOS-L and PAM algebras (instead of type-constraint Prolog and type-constraint WAM algebras).

In Part II we refine the type constraints to the polymorphic order-sorted types of PROTOS-L, again in several refinement steps. This allows us to develop a detailed, yet due to the use of the evolving algebras, mathematically precise account of the PAM’s compiled type constraint representation and solving facilities, and to prove its correctness w.r.t. PROTOS-L which we obtain as the final correctness theorem.

This paper was written in 1992/93 and revises and extends our work presented in [BB91] and [BB92]. It is organized as follows: Part I consists of Sections 2 - 5. Section 2 introduces an abstract notion of (type) constraints and defines PROTOS-L algebras with compiled AND/OR structure, the starting point of our development. This already includes the treatment of indexing and switching instructions which on this level of abstraction carry over from the WAM to the PAM. Section 3 introduces the representation of terms. The stack representation of environments and choicepoints is given in Section 4 which also contains the “Pure PROTOS-L” theorem stating the correctness of the PAM algebras developed so far w.r.t. the PROTOS-L algebras of Section 2. Various WAM optimizations that are also present in the PAM (environment trimming, last call optimization, initialization “on the fly” of temporary and permanent variables) are described in Section 5. The notions of type constraint and constraint solving have been kept abstract through all refinement levels so far; thus, the development carried out in Part I applies to any type system satisfying the given abstract conditions.

Part II consists of the Sections 6 - 8. Section 6 introduces the representation and constraint solving of monomorphic, order-sorted type constraints. Section 7 contains some type-specific optimizations of the PAM, which yields a situation where the WAM comes out as a special case of the PAM for any program not exploiting the advantages of dynamic type constraints. Section 8 gives a detailed account of polymorphic type constraint representation and solving in the PAM.

Notation and prerequisites

In this section we first list those definitions which are necessary to the reader who is interested only in analysis of the PAM, reading our rules as ‘pseudocode over abstract data’, and not in checking the correctness proof (for which we rely more explicitely on the underlying methodology of evolving algebras; for background and a definition of this notion which is due to Y. Gurevich see [Gur91]).

The abstract data comes as elements of (not further analysed) sets (domains, universes). The operations allowed on universes will be represented by partial functions.

We shall allow the setup to evolve in time, by executing function updates of the form

         f(t_{1},. . .,t_{n}) := t

whose execution is to be understood as changing (or defining, if there was none) the value of function f at given arguments.

We shall also allow some of the universes (typically initially empty) to grow in time, by executing updates of form

extend A by t_{1},…,t_{n} with updates endextend

where updates may (and should) depend on the t_{i}’s, setting the values of some functions on newly created elements t_{i} of A.

The precise way our ‘abstract machines’ may evolve in time will be determined by a finite set of rules of the form

         if condition
         then updates

where condition or guard is a boolean, the truth of which triggers simultaneous execution of all updates listed in updates. Simultaneous execution helps us avoid coding to, say, interchange two values.

If at every moment at most one rule is applicable (which will in this paper always be the case), we shall talk about determinism - otherwise we might think of a daemon freely choosing the rule to fire. The forms obviously reducible to the above basic syntax, which we shall freely use as abbreviations, are let and if then else. The transition rule notation

         if condition_{1} | . . . | condition_{n}
         then updates_{1} | . . . | updates_{n}

with pairwise incompatible conditions condition_{i} stands for the obvious set of n transition rules

if condition_{1}
then updates_{1}
if condition_{2}
then updates_{2}

…

if condition_{n}
then updates_{n}

We will also use the |-notation to separate alternative parts within more complex rule conditions and the corresponding update parts. For instance, the rule notation

if OK
  & code(p) = call(BIP)
  & BIP =
     true | fail      | cut

then

  succeed | backtrack | b := ct'(e)
          |           | succeed

deals with the built-in predicates true, fail, and cut and stands for the three rules

if OK
  & code(p) = call(BIP)
  & BIP = true

then

  succeed
if OK
  & code(p) = call(BIP)
  & BIP = fail

then

  backtrack
if OK
  & code(p) = call(BIP)
  & BIP = cut

then

  b := ct'(e)
  succeed

Also, we will often introduce abbreviations of the form a ≡ term. For instance, in the rules just given we used the three abbreviations

succeed ≡ p := p + 1
OK ≡ stop = 0

                                   backtrack ≡ if b = nil
                                                then stop := -1
                                                else p := p(b)

We shall assume that we have the standard mathematical universes of booleans, integers, lists of whatever etc. (as well as the standard operations on them) at our disposal without further mention. We use usual notations, in particular Prolog notation for lists.

Here are some more remarks on the formal background for the reader who is interested to follow our proofs.

Definition. An evolving algebra is a pair (A, R) where A is a first-order heterogeneous algebra with partial functions and possibly empty domains, and R is a finite system of transition rules. The transition rules are of form

if condition then updates

where condition is a boolean expression of the signature of A and updates is a finite sequence of updates of one of the following three forms:

function update : f(t_{1}, …, t_{n}) := t where f is a function of A and t_{1}, …, t_{n}, t are terms in the signature of A.

universe extension : extend A by t_{1}, …, t_{n} with updates endextend where t_{1}, …, t_{n} are variables possibly occurring in function updates updates (standing for elements of A).

update schema : FORALL i = t_{1}, …, t_{2} DO updates(i) ENDFORALL where t_{1} and t_{2} are numerical terms and updates(i) are updates (with parameter i).

The meaning of rules and updates execution is as explained above. We intend an update schema to denote an algebra update obtained by first evaluating t_{1} and t_{2} to numbers n_{1} and n_{2} and then executing updates(i) for all i ∈ {n_{1},…,n_{2}} in parallel. This construct, which does not appear in Gurevich’s original definition in [Gur91] is obviously reducible to rules with function updates.

Every evolving algebra (A, R) determines a class of structures called algebras or states of (A, R). Within such classes we will have a notion of initial and terminal algebras, expressing initial resp. final states of the target system. We are essentially interested only in those states which are reachable from inital states by R. In our refinement steps we typically construct a more concrete evolving algebra (B, S) out of a given more abstract evolving algebra (A, R) and relate them by a (partial) proof map F mapping states B of (B, S) to states F(B) of (A, R), and rule sequences R of R to rule sequences F(R) of S, so that the following diagram commutes:

[figure: F(B); F(R); F(B′); F; B; B′; F; R]

In accordance to terminology used in abstract data type theory [EM89] we call F also an abstraction function.

We shall consider such a proof map to establish correctness of (B, S) with respect to (A, R) if F preserves initiality, success and failure (indicated by the value of a special 0-ary function stop) of states, since in that case we may view successful (failing) concrete computations as implementing successful (failing) abstract computations.

We can consider such a proof map to establish completeness of (B, S) with respect to (A, R) if every terminating computation in (A, R) is image under F of a terminating computation in (B, S), since in that case we may view every successful (failing) abstract computation as implemented by a successful (failing) concrete computation.

In case we establish, in the above sense, both correctness (as we will do explicitly on every of our refinement steps) as well as completeness (which follows from all our refinement steps by straightforward observations) we may speak of operational equivalence of evolving algebras.

PART I: Adding type constraints to Prolog and the WAM

2 PROTOS-L Algebras with compiled AND / OR structure

2.1 An abstract notion of type constraints

The basic universes and functions in PROTOS-L algebras dealing with terms and substitutions can be taken directly from the standard Prolog algebras ([Bör90a], [Bör90b]). In particular, we have the universes TERM and SUBST of terms and substitutions with a function

subres: TERM × SUBST → TERM

yielding subres(t,s), the result of applying s to t.

To be able to talk about (type constraints of) variables involved in substitutions we introduce a new universe

VARIABLE ⊆ TERM

Since in PROTOS-L unification on terms is subject to type constraints on the involved variables, we have to distinguish between equating terms and satisfying type constraints for them. For this purpose we introduce a universe

EQUATION ⊆ TERM × TERM

whose elements are written as t_{1} ≐ t_{2}. Substitutions are then supposed to be (represented by) finite sets of equations of the form {X_{1} ≐ t_{1}, …, X_{n} ≐ t_{n}} with pairwise distinct variables X_{i}. The domain of such a substitution is the set of variables occurring on the left hand sides. (Note: If you want to have the logically correct notion of substitution - with occur check -, you should add the condition that no X_{i} occurs in any of the t_{j}.)

For a formalization of type constraints for terms - in the spirit of constraint logic programming - we introduce a new abstract universe TYPETERM, disjoint from TERM and containing all typeterms, of which we only assume that it comes with a special constant TOP ∈ TYPETERM. Type constraints are given by the universe

TYPECONS ⊆ TERM × TYPETERM

whose elements are written as t : tt. A set P ⊆ TYPECONS is called a prefix if it contains only type constraints of the form X : tt where X ∈ VARIABLE and at most one such pair for every variable is contained in P. The domain of P is the set of all variables X such that X : tt is in P for some tt. We denote by TYPEPREFIX the universe of all type prefixes.

Constraints are then defined as equations or type constraints, i.e.

CONSTRAINT ⊆ EQUATION ∪ TYPECONS

Let CSS denote the set of all sets of constraints together with nil ∈ CSS denoting an inconsistent constraint system.

The unifiability notion of ordinary Prolog is now replaced by a more general (for the moment abstract) constraint solving function:

         solvable: CSS → BOOL

telling us whether the given constraint system is solvable or not. Every (solution of a) solvable constraint system can be represented by a pair consisting of a substitution and a type prefix. Thus, we introduce a function

solution: CSS → SUBST × TYPEPREFIX ∪ {nil}

where solution(CS) = nil iff solvable(CS) = false. For the trivially solvable empty constraint system we have

         solution(∅) = (∅,∅)

and the functions

         subst part: CSS → SUBST

prefix part: CSS → TYPEPREFIX

are the two obvious projections of solution. As an integrity constraint we assume

         solution({t : TOP}) = (∅,∅)

i.e., TOP is used to represent a trivially solvable type constraint.

These are the only assumptions we make about the universe TYPETERM until we introduce a special representation for it in Section 6. Thus, the complete development up to Section 5 (i.e. Part I of this paper) applies to any concept of (type) constraints that exhibits the minimal requirements stated so far.

Having refined the notions of unifiability and substitution to constraint solvability and (solvable) constraint system, respectively, we can now also refine the related notion of substitution result to terms with type constrained variables. The latter involves three arguments:

1. a term t to be instantiated,

2. type constraints for the variables of t given by a prefix Pt, and

3. a constraint system CS to be applied.

Since a CS-solution consists of an ordinary substitution sCS together with variable type constraints PCS via solution(CS) = (sCS, PCS), the result of the constraint application can be introduced by

         conres(t, Pt, CS) = (t_{1}, P_{1})

as a pair consisting of the instantiated term t_{1} and type constraints P_{1} for the variables of t_{1}. For this function

conres: TERM × TYPEPREFIX × CSS → TERM × TYPEPREFIX ∪ {nil}

we impose the following integrity constraints:

∀ t ∈ TERM, Pt ∈ TYPEPREFIX, CS ∈ CSS .

         if solvable(Pt ∪ CS) then
                                    conres(t, Pt, CS) = (t_{1}, P_{1})

where:

                                    t_{1} = subres(t, subst part(CS))
                                    P_{1} = prefix part(Pt ∪ CS)_{|var(t_{1})}

else

                                    conres(t, Pt, CS) = nil

where P′_{|var(t′)} is obtained from P′ by eliminating the type constraints for all variables not occurring in t′.

P\X will be an abbreviation for P_{|domain(P)\{X}}, the prefix obtained from P by eliminating (if present) the constraint for X.

Thus, the condition that a constraint system CS “can be applied” to a term t with its variables constrained by Pt means that Pt is compatible with CS, i.e. solvable(CS ∪ Pt) = true.

2.2 Compilation

As already mentioned, our starting point in this paper are PROTOS-L algebras with compiled AND/OR structure. This is motivated by the fact that the type constraint mechanism is orthogonal both to the compilation of the predicate structure (OR structure) as well as to the compilation of the clause structure (AND structure). Leaving the notion of terms and substitutions as abstract as in 2.1, we can use the compiled AND/OR structure development for Prolog in [BR91], [BR92b] also for PROTOS-L: Essentially we just have to replace substitutions by the more general constraint systems, and have to take care of a clause constraint when resolving a goal.

In a PROTOS-L algebra a program is a pair consisting of a definition context and a sequence of clauses

PROGRAM ⊆ DEFCONTEXT × CLAUSE^{∗}

The definition context contains declarations of types, type constructors, etc. and will be refined in Part II. For prog = (defc,db) ∈ PROGRAM we will write x ∈ prog for both x ∈ defc and x ∈ db when it is clear from the context whether x is e.g. a type declaration or a list of clauses. A clause, depicted as

         {P} H <-- G_{1} & . . . & G_{n}.

is an ordinary Prolog clause together with a set P of type constraints for (all and only) the variables occurring in the clause head and body. As in [BS91] we use three obvious projection functions

clhead: CLAUSE → LIT clbody: CLAUSE → LIT^{∗} clconstraint: CLAUSE → TYPEPREFIX

where LIT is the universe of literals. Literals as used in ordinary logic programming are (nonnegated) atomic first-order formulas. An element of the universe GOAL also comes with a type prefix and is written as

{P} G_{1} & … & G_{n}.

We assume a universe INSTR of instructions containing

         {unify(H), add constraint(P), call(G),
          allocate, deallocate, proceed, true, fail, cut,
          try me else(N), try(L), retry me else(N), retry(L), trust me, trust(L),
          switch on term(i,Lv,Ls), switch on structure(i,T) |

i ∈ NAT, H, G ∈ TERM, P ∈ TYPEPREFIX,

N, L, Lv, Ls ∈ CODEAREA, T ∈ (ATOM × NAT × CODEAREA)^{∗}}

Here, add constraint is a new instruction not occurring in the WAM that adds a clause constraint to the current set of constraints accumulated so far. The universe ATOM contains the constant and function symbols; elements of ATOM are used in the switch on structure instruction in order to allow indexing over the top-level function symbol of an argument. Later on, further instructions will be added to INSTR.^{1}

For the compilation of clauses we have a function compile: CLAUSE → INSTR^{∗}

         compile({P} H <-- G_{1} & . . . & G_{n}) =
                     [allocate, add constraint(P), unify(H),
                      call(G_{1}),

…

                      call(G_{n}),
                      deallocate, proceed]

1Note that in this paper we do not consider a special representation for constants or lists. These are present in the PAM, and could be added to our formal treatment without difficulty. For instance, switch on term would get an additional argument for the constant case.

Compiled programs are “stored” in a universe CODEAREA which comes with functions

+,-: CODEAREA → CODEAREA

code: CODEAREA → INSTR

where + and its inverse - yield a linear structure on CODEAREA and code(l) gives the instruction “stored” in l. The function

unload: CODEAREA → INSTR^{∗}

         unload(Ptr) = if code(Ptr) = proceed
                        then [proceed]
                        else [code(Ptr)|unload(Ptr+)]

is an auxiliary function. We say that Ptr ∈ CODEAREA points to code for a clause Cl if

         unload(Ptr) = compile(Cl)

The function

procdef: LIT × CSS × PROGRAM → CODEAREA

yields a pointer Ptr = procdef(G,Cs,Prog) that points to a chain chain(Ptr) of clauses containing all candidate clauses for resolving G in Prog under the constraint system Cs, i.e.:

         ∀ Cl ∈ Prog .
         ((∀ P ∈ chain(procdef(G,Cs,Prog)) . P does not point to code for Cl)

⇒

             solvable({g≐ rename(clhead(Cl),i)} ∪ Cs
                      ∪ rename(clconstraint(Cl),i)) = false)

where i ∈ NAT is chosen such that rename(GC,i) renames all variables in a goal or constraint GC to new variables. For the auxiliary function chain

chain: CODEAREA → CODEAREA^{∗}

we assume for an activator literal act

 chain(Ptr) = \{ \begin{matrix}chain(Lv) & if code(Ptr) = switch on term(i,Lv,Ls) \\ & and is var(X_{i}) \\ chain(Ls) & if code(Ptr) = switch on term(i,Lv,Ls) \\ & and is struct(X_{i}) \\ chain(select(T,f,a)) & if code(Ptr) = switch on structure(i,T) \\ & and f = functor(X_{i}) and a = arity(X_{i}) \\ chain_{1}(Ptr) & otherwise \end{matrix}

chain_{1}(Ptr) = \{ \begin{matrix}flatten[chain_{1}(Ptr),chain_{1}(N)] & if code(Ptr) = try me else(N) \\ & or code(Ptr) = retry me else(N) \\ flatten[chain_{1}(C),chain_{1}(Ptr+)] & if code(Ptr) = try(C) \\ & or code(Ptr) = retry(C) \\ chain_{1}(Ptr+) & if code(Ptr) = trust me \\ chain_{1}(C) & if code(Ptr) = trust(C) \\ [Ptr] & otherwise \end{matrix}

where X_{i} = arg(act,i), functor, arity, and arg are the term analyzing functions, and is var and is struct are true for variables and compound terms, respectively. Furthermore, the switch on structure parameter T could be thought of as a hash table, with select(T,f,a)

= pt if (f,a,pt) ∈ T.

2.3 Choicepoints and Environments

Executing AND/OR compiled PROTOS-L programs requires two stacks where w.r.t. the Prolog case we replace the substitution part by a constraint system. STATE is a universe to store the choicepoints and comes with functions

nil: → STATE cs: STATE → CSS accumulated constraint system p: STATE → CODEAREA program pointer cp: STATE → CODEAREA continuation pointer

e:  STATE → ENV  environment
b:  STATE → STATE  backtracking point

vi: STATE → NAT renaming index for variables ct: STATE → STATE cut point

The universe ENV of environments comes with functions

nil: → ENV

ce: ENV → ENV continuation environment cp': ENV → CODEAREA continuation pointer ct': ENV → STATE cut point vi': ENV → NAT renaming index for variables

As in the WAM, STATE and ENV are embedded into a single STACK STATE, ENV ⊆ STACK -: STACK → STACK

with a common bottom element nil. tos(b,e) denotes the top of the stack which will always be the maximum of b and e.

2.4 Initial State

To hold the current status of the machine there are some 0-ary functions which correspond to their unary counterparts above. Given the PROTOS-L goal {P} G_{1} & … & G_{n} we have the following initial values:

cs ∈ CSS cs = ∅

p ∈ CODEAREA  unload(p) = [add constraint(P),
                                        call(G_{1}),. . .,call(G_{n}),
                                        proceed]

cp ∈ CODEAREA cp = p++

e ∈ ENV  vi'(e)=0, ct'(e)=nil, ce(e)=nil

b ∈ STATE b = nil

vi ∈ NAT  vi = 0
ct ∈ STATE  ct = nil

The literals of the initial PROTOS-L goal, as well as all intermediate goals that will be constructed during program executing, can be recovered via the continuation pointer. For code(cp-) = call(G) (which will always be the case as long as there is still something to do) we have in particular

act ≡ subres(rename(G,vi'(e)),subst part(cs))

which is called the current activator.

The 0-ary function prog ∈ PROGRAM holds all declarations and clauses of the program (which in this paper will always be constant since we do not consider database operations like assert or retract). Finally, stop ∈ {-1,0,1} indicates whether the machine has stopped with failure, is still running, or has stopped with success.

2.5 Transition rules

The transition rules are as in the Prolog case with the substitution component being replaced by a constraint system, and with the following extension to the unify rule and the new add constraint instruction:

unify

if OK
  & code(p) = unify(H)

then

  if solvable(cs ∪ {act≐ rename(H,vi)})
  then cs := cs ∪ {act≐ rename(H,vi)}
        vi := vi + 1
        succeed
  else backtrack

add constraint

                                          if OK
                                            & code(p) = add constraint(P)

then

                                            if solvable(cs ∪ rename(P,vi))
                                            then cs := cs ∪ rename(P,vi)
                                                 succeed
                                            else backtrack

The condition OK is an abbreviation for stop = 0, i.e., the machine is operating in normal mode and no stop condition has been encountered. All abbreviations as well as the complete set of transition rules are given in Appendix A.

3 Term representation

The representation of terms and substitutions in the WAM can be introduced in several steps. Following the development in [BR92b] we first introduce the treatment of the low-level run-time unification (but leaving the details of type constraint solving as an abstract update to be refined later), followed by the term constructing and analyzing put and get instructions. In particular, the WAM-specific optimizations of environment trimming, last call optimization, or the initialization of temporary and permanent variables are postponed until we have established the correctness of the first refinement level with respect to the PROTOS-L algebras with compiled AND/OR structure in Section 2. The major derivation from the real PAM code in Sections 3 and 4 will be our simplifying assumption that all variables are permanent and are initialized on allocation to free unconstrained variables. Under this assumption the variables receive their initial type restrictions, derived statically by the compiler, immediately after allocation. This is achieved by a new (auxiliary) put constraint instruction which will be dropped again later (in Section 5).

3.1 Universes and Functions

For the representation of terms we use the pointer algebra

         (DATAAREA; +, -; val)

with DATAAREA ⊆ MEMORY, where

+, - : DATAAREA → DATAAREA

connect the locations in DATAAREA and are inverse to each other. In the codomain of the function

val: DATAAREA → PO + MEMORY + SYMBOLTABLE

we use the universe SYMBOLTABLE in order to connect a function symbol to its arity and type. It comes with functions

atom: SYMBOLTABLE → ATOM arity: SYMBOLTABLE → NAT entry: ATOM × NAT → SYMBOLTABLE

of which we assume entry(atom(s),arity(s)) = s for any s ∈ SYMBOLTABLE and

atom(entry(f,n)) = f, arity(entry(f,n)) = n for any atom f with arity n.

The functions tag and ref are defined on the universe PO of “PROTOS-L objects”

tag: PO → TAGS

ref: PO → DATAAREA + TYPETERM

where, because of the type constraint treatment, a new tag VAR for indicating free variables is introduced into the universe

         TAGS = {REF, STRUC, VAR}

Special tags for representing constants, lists, built-in integers, etc. are also present in the PAM, but in this paper we consider them as optimizations that can be added later on without any difficulties. The tag FUNC from [BR92b] is not included since it is not needed.

The codomain of ref contains the universe TYPETERM since we will keep the type term representation abstract here; it will be refined later (see Section 6).

As in [BR92b] we use some abbreviations for dealing with locations l ∈ DATAAREA:

         tag(l)  ≡ tag(val(l))
         ref(l)  ≡ ref(val(l))
         l_{1} ← l_{2} ≡ val(l_{1}) := val(l_{2})

         l ← <t,r> ≡ tag(l) := t
                       ref(l) := r
         unbound(l) ≡ tag(l) = VAR
         mk unbound(l)  ≡ mk unbound(l,TOP)
         mk unbound(l,tt) ≡ tag(l) := VAR
                              insert type(l,tt)
         insert type(l,tt) ≡ ref(l) := tt

where the last four abbreviations deal with the typed variable representation and where tt ∈ TYPETERM. Note that an unconstrained free variable gets the trivial type restriction TOP, representing no restriction at all (c.f. Section 2.1).

In addition to the (partial) dereferencing and term reconstructing functions from the WAM case we now also assume a function that recovers the type constraints for all variables occurring in a term. Of these functions

deref: DATAAREA → DATAAREA

term: DATAAREA → TERM

type prefix: DATAAREA → TYPEPREFIX

we assume for l ∈ DATAAREA:

          deref(l) = \{ \begin{matrix}deref(ref(l)) & if tag(l) = REF \\ l & otherwise \end{matrix}

           term(l) = \{ \begin{matrix}mk var(l) & if unbound(l) \\ term(deref(l)) & if tag(l) = REF \\ f(a_{1},. . .,a_{n}) & if tag(l) = STRUC and \\ & f = atom(val(ref(l))) \\ & n = arity(val(ref(l))) \\ & a_{i} = term(ref(l)+i) \end{matrix}

    type prefix(l) = \{ \begin{matrix}mk var(l) : ref(l) & if unbound(l) \\ type prefix(deref(l)) & if tag(l) = REF \\ P_{1} ∪ . . . ∪ P_{n} & if tag(l) = STRUC and \\ & n = arity(val(ref(l))) \\ & P_{i} = type prefix(ref(l)+i) \end{matrix}

where make var(l) ∈ VARIABLE is a unique variable assigned to l. Note that the condition term(l) ∈ TERM now implies various consistency properties like:

         if unbound(l)  then ref(l) ∈ TYPETERM
         if tag(l) ∈ {REF, STRUC} then ref(l) ∈ DATAAREA
                                        term(l) ∈ TERM
                                        typeprefix(l) ∈ TYPEPREFIX
         if tag(l) = STRUC  then val(ref(l)) ∈ SYMBOLTABLE
                                        term(ref(l)+i) ∈ TERM
                                        type prefix(ref(l)+i) ∈ TYPEPREFIX
with i ∈ {1,. . .,arity(val(ref(l)))}.

3.2 Unification

Lowlevel unification in the PAM can be carried out as in the WAM (see [AK91]) if we refine the bind operation into one that takes into account also the type constraints of the variables ([BMS91], [BM94]). The bind operation may thus also fail and initiate backtracking if the type constraints are not satisfied. Thus, we can use the treatment of unification as described in [BR92b], while leaving the bind operation abstract for the moment, not only in order to postpone the discussion of occur check and trailing but also to stress the fact that the bind operation will take care of the type constraints for the variables.

To be more precise, the DATAAREA subalgebra

         (PDL; pdl, nil; +, -; ref')

with pdl, nil ∈ PDL and ref': PDL→ DATAAREA

is the push down list used for lowlevel unification, containing all pairs of (addresses of) terms still to be unified, with

         left ≡ ref'(pdl)           right ≡ ref'(pdl-)

being the current pair of terms. Unification is triggered by the update

         unify(l_{1},l_{2}) ≡ ref'(nil++) := l_{1}
                         ref'(nil+) := l_{2}
                         pdl := nil++
                         what to do := Unify

The 0-ary function

         what to do ∈ {Unify, Run}

will be used in the guard of all following rules in the form of conditions like

         UNIF ≡ OK & what to do = Unify
         RUN ≡ OK & what to do = Run

Unification is carried out by unification rules as in [BR92b] (see appendix B.1) where for the abstract bind update we impose the following modified

BINDING CONDITION 1: For any l_{1}, l_{2}, l ∈ DATAARRA, with term resp. term' values of term(l) and with prefix resp. prefix' values of type prefix(l) before resp. after execution of bind(l_{1},l_{2}), we have if unbound(l_{1}) holds:

         LET CS = {mk var(l_{1}) = term(l_{2})} ∪ type prefix(l_{1})
                                           ∪ type prefix(l_{2})
         If solvable(CS) = true
         then (term', prefix') = conres(term, prefix, CS)

else backtrack update will be executed.

With this generalized binding assumption we obtain the following modified

UNIFICATION LEMMA: If pdl-- = nil, term(left), term(right) ∈ TERM, and
type prefix(left), type prefix(right) ∈ TYPEPREFIX, the effect of setting what to do

to Unify, for any l ∈ DATAAREA such that term(l) ∈ TERM and type prefix(l) ∈ TYPEPREFIX is as follows:

Let term resp. term' be the values of term(l) and prefix resp. prefix' be the values of type prefix(l) when setting what to do to Unify and when what to do has been set back to Run again, respectively. Then we have:

         LET CS = {term(left) = term(right)} ∪ type prefix(left)
                                              ∪ type prefix(right)
         If solvable(CS) = true
         then (term', prefix') = conres(term, prefix, CS)

else backtrack update will be executed.

Proof: The proof of the Unification Lemma is by induction on the size of the terms to be unified, relying on our generalized Binding Condition.

3.3 Putting of terms

As in the WAM, run time structures are created in the subalgebra of DATAAREA

         (HEAP; h, boh; +, -; val)

where h, boh ∈ HEAP represent the top resp. the bottom element of the heap. We use nextarg ∈ HEAP to point to the next argument when anyalyzing a structure on the heap. Furthermore, we now assume

DATAAREA + CODEAREA ⊆ MEMORY

where CODEAREA is as in Section 2.2 but where INSTR now contains

         put value(y_{n},x_{j})
         put structure(f,x_{i})
         get value(y_{n},x_{j})
         get structure(f,x_{i})
         unify value(y_{n})
         unify variable(x_{n})
         put constraint(y_{n},tt)

with n,j,i ∈ NAT, f ∈ SYMBOLTABLE, tt ∈ TYPETERM, y_{n} ∈ DATAAREA, x_{i} ≡ x(i), where x: NAT → AREGS and AREGS ⊆ DATAAREA. Note that put constraint(y_{n},tt) is a new instruction used for inserting a type restriction into a heap location. Instead of having a pair (fn,a) ∈ ATOM × NAT we use f = entry(fn,a) in the code.

The code developed in Section 1.2 of [BR92b] for constructing terms in body goals uses put instructions which assume that, for all variables Y_{i} of the term t to be built on the heap, there is already a term denoting y_{i} ∈ DATAAREA available. Since this means in particular that no variables are created during this process, we can use (with the obvious modification mentioned above) the same put instructions (i.e. put value, unify value in Write mode, put structure) for the compilation of a body goal (see Appendix B.2 and B.3). Furthermore, we may assume that for the variables Y_{i} we have no type constraints to formalize here because they have already been associated to the corresponding location y_{i} (i.e. the variable term(y_{i}) which is - up to renaming - equal to Y_{i}. This gives us the following

PUTTING LEMMA: If all variables occurring in a term t ∈ TERM are among {Y_{1},…,Y_{l}}, and if for n ∈ {1, …, l}, y_{n} ∈ DATAAREA with

         term(y_{n}) ∈ TERM
         type prefix(y_{n}) ∈ TYPEPREFIX

and X_{i} is a fresh variable, and CS is the constraint system consisting of the substitution associating every Y_{n} with term(y_{n}) and of the union of the type constraints type prefix(y_{n}), i.e.

         CS = ⋃_{n} {Y_{n} ≐ term(y_{n})} ∪ type prefix(y_{n})

then the effect of setting p to

         load(append(put code(X_{i} = t), More))

with subsequent fresh indices generated by the term normal form function nf_{s} (Appendix B.2) being non-top level, is that the pair

         (term(x_{i}), type prefix(x_{i}))

at the moment of passing to More, gets value of

         conres(t, ∅, CS)

Proof: The proof follows by induction over the size of the involved terms, observing that no type related actions like variable creation or variable binding is involved here.

3.4 Getting of terms

Unlike putting of terms that does not involve unification, the getting of terms does involve unification where parts of it are compiled into the getting instructions (like get structure followed by a sequence of unify instructions) and the remaining unification tasks are handled by the lowlevel unify procedure.

The get value, unify value, and unify variable instructions are as in the WAM case (see Appendix B.4 and B.5). Note that we need unify variable both in Read and Write mode which is controlled by the 0-ary function mode ∈ {Read, Write}. In [BR92b] unify variable in Write mode is introduced only as an optimization for variable initialization “on the fly”, but when the machine enters Write mode in get structure, unify variable will be executed for the auxiliary substructure descriptors X_{i} generated by the term normal form function nf_{a} (Appendix B.2). Since we do not have to consider type contraints for such X_{i}, it suffices to initialize them to a free variable without any type restriction. Thus, for the generation of a heap variable in Write mode

of unify variable we use
         mk heap var(l) ≡ mk unbound(h)
                          bind(l,h)
                          h := h+

When unify variable will be used for “on the fly” initialization of typed variables, we will have to consider an additional type initialization parameter (c.f. Section 5).

The first get structure rule for PROTOS-L is as in the WAM case, covering the situation where x_{i} in get structure(f,x_{i}) is bound to a non-variable term (Appendix B.4). When x_{i} is unbound, it must be bound to a newly created term with top-level symbol f. Whereas in the WAM this will always succeed, in the PAM case the type constraint of x_{i} must be taken into account. Indeed, what is happening here is the binding of a variable X with a type constraint, say tt, to a term t starting with f. In abstract terms this amounts to solving the constraint system

         {X≐ t, X : tt}

We still want to leave the details of variable binding abstract here; what is of interest for this special case occurring in get structure is which type constraints stemming from tt and (the declaration of) f must be propagated onto the argument terms of t = f(…). Therefore, we introduce the function

propagate list: SYMBOLTABLE × TYPETERM → TYPETERM^{∗} ∪ {nil}

yielding for arguments entry(f,n) and tt the list of type terms the arguments of f must satisfy. To be more precise, we have the following integrity constraint:

         propagate list(entry(f,n),tt) = (tt_{1},. . .,tt_{n})

iff

         prefix-part({f(X_{1},. . .,X_{n}) : tt}) = {Xi_{1} : tti_{1},. . ., Xi_{k} : tti_{k}}

where {i_{1},…,i_{k}} ⊆ {1,…,n}, and for j ∈ {1,…,n}\{i_{1},…,i_{k}} we have tt_{j} = TOP.

If the constraint system {f(X_{1},…,X_{n}) : tt} is not solvable, no propagation is possible, and if it reduces to the trivially solvable empty constraint system, propagate list yields a list containing only TOP. Thus we introduce the abbreviations

   can propagate(entry(f,n),tt)  ≡ solution({f(X_{1},. . .,X_{n}) : tt}) ≠ nil
   trivially propagates(entry(f,n),tt) ≡ solution({f(X_{1},. . .,X_{n}) : tt}) = ∅

Get-Structure-2

if RUN
  & code(p) = get structure(f,x_{i})

  & unbound(deref(x_{i}))
  & can propagate(f,ref(deref(x_{i})))
              = true                      | = false
  & trivially propagates(f,ref(deref(x_{i}))) |
      = true    | = false                 |

then

  h ← <STRUC,h+>                          | backtrack
  bind(deref(x_{i}),h)                        |
  val(h+) := f                            |
  h := h++                                |
  mode := Write | nextarg := h++          |
                 | mk unbounds(h+,propagate list(f,ref(deref(x_{i}))) |
                 | mode := Read            |
  succeed                                 |

For l ∈ DATAAREA and tt_{1},…,t_{n} ∈ TYPETERM, the update

         mk unbounds(l,(tt_{1},. . .,tt_{n})) ≡ FORALL i = 1,. . .,n DO

                                           mk unbound(l+i,tt_{i})
                                        ENDFORALL

puts n type restricted variables at the locations l+1,…,l+n on the heap. When this update is executed in the rule above the machine continues in read mode so that the subsequent n unify instructions take into account these type restrictions.

GETTING LEMMA: If all variables occurring in a term t ∈ TERM are among {Y_{1},…,Y_{l}}, and if for n ∈ {1,…,l}, y_{n} ∈ DATAAREA with

         unbound(y_{n})

ref(y_{n}) ∈ TYPETERM

and X_{i} is a fresh variable with x_{i} ∈ DATAAREA and

         term(x_{i}) ∈ TERM
         type prefix(x_{i}) ∈ TYPEREFIX

and CS is the constraint system consisting of the equation t≐ term(x_{i}) together with type prefix(x_{i}) and the union of the type constraints type prefix(y_{n}), i.e.

         CS = {t≐ term(x_{i})} ∪ type prefix(x_{i}) ∪ ⋃_{n} type prefix(y_{n})

then the effect of setting p to

         load(append(get code(X_{i} = t), More))
for any l ∈DATAAREA with term = term(l) ∈ TERM and typeprefix = type prefix(l)

∈ TYPEPREFIX being the values before execution, is as follows:

If solvable(CS) = true then p reaches More without backtracking and the pair

         (term(l), type prefix(l))

at the moment of passing to More, gets value of

         conres(term, typeprefix, CS)

else backtracking will occur before p reaches More. Proof: The proof follows by induction on the size of the involved terms. Observe that similar to the Putting Lemma no real variable creation occurs: When an auxiliary variable X_{k} (generated by nf_{a}) is created on the heap via unify variable in Write mode, its <VAR,TOP> initialization will be overwritten by a subsequent get structure instruction corresponding to the subterm represented by X_{k}. Note also that if CS is solvable, then conres(term, typeprefix, CS) ≠ nil because CS ∪ typeprefix is also solvable since the intersection between typeprefix and any type prefix(y_{n}) is already contained in CS.

In order to uphold the

HEAP VARIABLES CONSTRAINT: No heap variable points outside the heap, i.e. for any

l ∈ HEAP with boh ≤ l < h and tag(l) = REF, we have boh ≤ ref(l) < h.

the instruction unify local value in Write mode creates a new heap variable for a so-called local variable (cf. B.5):

         local(l) ≡ unbound(l) & l ∈ HEAP & NOT(boh ≤ l < h)

For a discussion of local variables see [AK91] or [BR92b]. In the PROTOS-L case the type restriction of the local variable must be taken into account which is done by the binding update in our mk heap variable abbreviation. Thus, the HEAP VARIABLES CONSTRAINT as well as the

HEAP VARIABLES LEMMA: If the put code and get code functions generate unify local value instead of unify value for all occurrences of local variables, then the execution of put seq and get seq preserve the HEAP VARIABLES CONSTRAINT [BR92b].

carries over to the PROTOS-L case, provided we ensure

BINDING CONDITION 2: The bind update preserves the HEAP VARIABLES CON-STRAINT.

3.5 Putting of Constraints

In this section we will still keep the type constraint representation abstract, while specifying the conditions about the constraint handling code (for realization of add constraint of Section 2) in order to prove a theorem corresponding to the Pure Prolog Theorem of [BR92b] (see 4).

The compile function will be refined using

         put constraint seq({Y_{1} : tt_{1},. . .,Y_{r}: tt_{r}}) = [put constraint(y_{1},tt_{1}),

…,

                                                   put constraint(y_{r},tt_{r})]

for which we use the new instruction put constraint(y_{n},tt) (where tt ∈ TYPETERM) and the following rule:

Put-Constraint

if RUN
  & code(p) = put constraint(l,tt)

then

  insert type(l,tt)
  succeed

The update for inserting a type restriction has still the straightforward definition given in 3.1 (i.e. ref(l) := tt), but will be refined later when we introduce a representation of type terms. In any case it must satisfy the following

TYPE INSERTING CONDITION: For any l_{1}, l ∈ DATAARRA, with term resp. term' values of term(l) and with prefix resp. prefix' values of type prefix(l) before resp. after execution of insert type(l_{1},tt) we have if unbound(l_{1}) holds:

         (term', prefix') = conres(term, prefix\{mk var(l_{1})}, {mk var(l_{1}) : tt})

For the definition given above the type inserting condition is obviously satisfied.

4 PAM Algebras

4.1 Environment and Choicepoint Representation

The stack of states and environments of PROTOS-L algebras with compiled AND/ OR structure of Section 2 are now represented by a subalgebra of DATAAREA

         (STACK; bos; +, -; val)

with bos ∈ STACK representing the bottom element corresponding to nil in Section 2. The concrete memory layout can be done as in the WAM [BR92b] (see Appendix B.6) since the only type-related action is in the allocation of n free variable cells in the rule for Allocate: This situation is covered by our modified mk unbound abbreviation that assigns the trivial TOP type restriction to each such initialized variable:

allocate

if OK
  & code(p) = allocate(n)

then

  e := tos(b,e)
  val(ce(tos(b,e))) := e
  val(cp(tos(b,e))) := cp
  FORALL i = 1,. . .,n DO
     mk unbound(y_{i}(tos(b,e)))
  ENDFORALL
  succeed

deallocate

                                          if OK
                                            & code(p) = deallocate

then

                                            e := val(ce(e))
                                            cp := val(cp(e))
                                            succeed

4.2 Trailing

As is standard practice in the WAM, we assume that HEAP < STACK < AREGS and the WAM binding discipline:

BINDING CONDITION 3: If unbound(l_{1}) and unbound(l_{2}) and bind(l_{1},l_{2}) does not initiate backtracking, then after executing bind(l_{1},l_{2}) the higher location will be bound to the lower one.

Together, these conditions imply BINDING CONDITION 2 and also the

STACK VARIABLES PROPERTY: Every stack variable l points either to the heap or to a lower location of the stack, i.e. ref(l) ∈ HEAP with boh ≤ l < h, or ref(l) ∈ STACK with

bos ≤ l ≤ tos(b,e).

Whereas BINDING CONDITION 3 and the STACK VARIABLES PROPERTY are exactly as in the WAM case [BR92b], for trailing variable bindings also the type restrictions must be taken into account in the PAM. Since variables in the PAM carry a type restriction represented in the ref value of a location - which is updated when binding the variable -, the type restriction must be saved upon binding and recovered upon backtracking. Strictly speaking, it would be sufficient to save only the ref value of a location; however, for use in a later refinement -when we will introduce different tags for free variables - we also trail the tag of a location. Therefore, in the DATAAREA subalgebra

         (TRAIL, tr, botr; +, -; ref¨ )

with tr, botr ∈ TRAIL being the top and bottom elements, the codomain of the function

ref¨ : TRAIL → DATAAREA × PO

records also the complete val decoration. The trail update, to be executed when changing the value of a location l during binding is then:

         trail(l) ≡ ref¨ (tr) := (l, val(l))
                     tr := tr+

Note that this is a non-optimized version of the trailing operation; we could have also used a conditional trailing governed by the condition boh ≤ l < h & l < hb OR bos ≤ l ≤ tos(b,e)

& l < b.

For t ∈ TRAIL with ref¨ (t) = (l, v) we use the following abbreviation for the two obvious projections on ref¨ (t):

         location(t) ≡ l         value(t) ≡ v

Upon backtracking we must now unwind the trail

         backtrack ≡ p := val(p(b))
                         unwind trail
         unwind trail ≡ FORALL t = tr-,. . .,tr(b) DO
                            location(t) ← value(t)
                         ENDFORALL

where value(t) retrieves the previous tag and type restriction of location(t). We still leave the binding update abstract, but pose the following

TRAILING CONDITION: Let l_{1}, l_{2}, l ∈ DATAAREA. If val(l) before execution of bind(l_{1},l_{2}) is different from val(l) after successful execution of bind(l_{1},l_{2}), then the location l has been trailed with trail(l).

Note that due to the update on the type restrictions of a variable the trailing of both locations l_{1} and l_{2} may be triggered by bind(l_{1},l_{2}); moreover, if e.g. l_{2} denotes a polymorphic term containing variables these variables also have to be trailed if they get another type restriction in the binding process (see Sections 6.1 and 6.5).

4.3 Pure PROTOS-L theorem

In order to establish a correctness proof of compilation to PAM algebras developed so far from PROTOS-L algebras with compiled AND/OR structure of Section 2, we can generalize the ”Pure Prolog Theorem” of [BR92b] to our case. We will thus construct a function F (c.f. Section 1) from the PROTOS-L algebras to the PAM algebras. We will also first ignore cutpoints (ct, ct') which are not needed for pure PROTOS-L, as well as variable renaming indices (vi, vi') since as in the WAM case the renaming is ensured by the offsets in the stack and the heap. Further, all names of universes and functions on Section 2 will get an index 1. For the function compile dealing with the term representing algebras we have

         compile({P} H <-- G_{1} & . . . & G_{n}) =

                     flatten([allocate(r), put constraint seq(P), get seq(H),
                              call seq(G_{1}),

…

                              call seq(G_{1}),
                              deallocate, proceed])

The abstraction function F maps PAM rules to PROTOS-L rules in the obvious way. It is defined via a mapping between instruction sequences (which directly correspond to rule sequences). For instance, with respect to unification and type constraint solving we have

call seq(G)  ↦ call(G)
get seq(H)  ↦ unify(H)
put constraint seq(P) ↦ add constraint(P)

This correspondence also defines a (partial) function

codepointer: CODEAREA × CODEAREA_{1}

by mapping e.g. the beginning of get seq(H) to the location labelled with unify(H). Furthermore, we establish the functions

css: TRAIL → CSS_{1} subst: TRAIL → SUBST_{1}

choicepoint: STACK → STATE_{1}

env: STACK → ENV_{1} term: DATAAREA × TRAIL → TERM_{1} typeprefix: DATAAREA × TRAIL → TYPEPREFIX_{1}

where we have added - w.r.t. the WAM case in [BR92b] - the functions css and typeprefix in order to construct the correspondence between the constraint representations. Viewing an element of STATE_{1} (resp. ENV_{1}) as a tuple of its cs, p, cp, e, b (resp. cp’, ce) values, these functions are defined by:

term(l,l_{t}) yields the value term(l) would take after having unwound

the trail down to l_{t}

typeprefix(l,l_{t}) yields the value type prefix(l) would take after having

unwound the trail down to l_{t}

css(l_{t})  = ⋃_{botr≤l<tr} {mk var(location(l))≐ term(location(l),l_{t})}
                             ∪ typeprefix(location(l),l_{t})
subst(l_{t})  = subst part(css(l_{t}))
choicepoint(lb) = ⟨ css(val(tr(lb))),
                     codepointer(val(p(lb))),
                     codepointer(val(cp(lb))),
                     env(val(e(lb))),
                     choicepoint(val(b(lb))) ⟩
env(le)  = ⟨ codepointer(val(cp(le))),
                     env(val(ce(le))) ⟩

The 0-ary functions are defined by

cs_{1} = css(tr)
p_{1} = codepointer(p)
cp_{1} = codepointer(cp)
e_{1} = env(e)
b_{1} = choicepoint(b)

Furthermore, for the current activator act_{1} of 2.4 we have for code(cp-) = call(g,m,r) the correspondence

act_{1} = g(term(x_{1}),. . .,term(x_{m}))

Correctness Theorem 1 (PURE PROTOS-L THEOREM): Compilation from the PROTOS-L algebras with compiled AND/OR structure (of Section 2) to the PAM algebras developed so far (and thus satisfying all the conditions explicitely stated above) is correct. Proof: For the proof it suffices to show that for any PAM algebra A and any transition rule sequence R such that F(A) and F(R) is defined, the diagram

                       [figure: F(A); F(R); F(A'); F; A; A'; F; R]

commutes. This follows by case analysis, relying on the conditions and lemmas established so far. In particular, w.r.t. type constraints we observe the fact that allocate allocates a new variable location (with TOP restriction) for every variable occurring in the clause. These locations are used by the put constraint instructions, so that the preconditions for the TYPE INSERTING CONDITION hold.

5 Additional WAM optimizations in the PAM

5.1 Environment Trimming and Last Call Optimization

Environment trimming and last call optimization (LCO) are among the most prominent optimizations in the WAM; for a discussion we refer to [AK91] and [BR92b]. The necessary ARGUMENT REGISTERS PROPERTY as formulated in [BR92b] can be ensured by the compiler by generating a put unsafe value(y_{n},x_{j}) instruction instead of put value(y_{n},x_{j}) for each unsafe occurrence of Y_{n}. This instruction is executed by the rule:

Put-Unsafe-Value

if RUN
  & code(p) = put unsafe value(y_{n},x_{j})
  & deref(y_{n}) ≤ e  | deref(y_{n}) > e

then

  x_{j} ← deref(y_{n})  | mk heap var(deref(y_{n}))
                   | x_{j} ← <REF,h>
  succeed

Note that the condition deref(y_{n}) > e implies unbound(deref(y_{n})). Thus, in case of y_{n} being unsafe, a new variable is created on the heap, referenced by both y_{n} and x_{j}. Unlike in Prolog, in PROTOS-L the type restriction of y_{i} must be copied to the new heap variable - this is already taken into account by the bind update in our mk heap var abbreviation introduced in Section 3.4. Therefore, following the argumentation in [BR92b], we can savely assume that the compiler enforces environment trimming and also last call optimization (LCO). Thus, every call instruction gets an additional parameter n where n is the number of variables that are still needed in the environment. LCO then means that the instruction sequence

                     Call(g,a,0), Deallocate, Proceed

is replaced by

                     Deallocate, Execute(g,a)

which disregards the current environment before calling the last subgoal of a clause.

5.2 Initializing Temporary and Permanent Variables

Up to now, when allocating an environment, we have allocated r value cells in that environment, where r is the number of variables occurring in the clause. A sequence of r corresponding put constraint(y_{j},tt_{j}) instructions initialized the type restriction on the variables y_{j} to tt_{j} found in the clause’s type prefix.

However, as explained in [BMS91], the first occurrence of a variable in a PROTOS-L clause is sufficient to consider the statically available type restriction. (The specialized instructions of [BMS91, BM94] for variables with monomorphic, polymorphic, or with no type restriction will be introduced as an optimization in Section 7.) Both temporary and permanent variables can be initialized “on the fly”; for a discussion of the classification of variables into temporary and permanent ones which was introduced by [War83] we refer to [AK91] and [BR92b]. Thus, we modify our compile function such that for a temporary variable, Y_{n}, y_{n} is replaced by fresh X_{i}, x_{i}, and such that

         get variable
         put variable
         unify variable

instructions are generated for the first occurrence of a variable, replacing the so-far used get value, put value (resp. put unsafe value), and unify value instructions, respectively.

Put-1 (X variable)

if RUN
  & code(p) = put variable(x_{i},x_{j},tt)

then

  mk unbound(h,tt)
  x_{i} ← <REF,h>
  x_{j} ← <REF,h>
  succeed

Put-2 (Y variable)

                                          if RUN
                                            & code(p) = put variable(y_{n},x_{j},tt)

then

                                            mk unbound(y_{n},tt)
                                            x_{j} ← <REF,y_{n}>
                                            succeed

When initializing a temporary variable with put variable, a new heap cell must be allocated, which is not the case when initializing a permanent variable, provided that put unsafe variable and unify local value instructions are used properly. This, however, has already been verified (see Section 5.1). In both cases, the mk unbound(l,tt) update corresponds to the mk unbound(l) update for that variable carried out previously during allocation, and the insert type(l,tt) update carried out by the put constraint instruction immediately after allocation (c.f. 3.5). Therefore, since the put variable instruction corresponds to the first occurrence of the variable X_{i} resp. Y_{n}, we can savely drop its initialization during allocation and its complete put constraint instruction.

get variable

if RUN
  & code(p) = get variable(l,x_{j},tt)

then

  mk unbound(l,tt)
  bind(l,x_{j})
  succeed

Whereas in the WAM case the get variable instruction always succeeds, in the PROTOS-L case we have to check that the clause’s type restriction tt for x_{j} is satisfied. This is achieved by setting l to an unbound variable, inserting the type term tt as its type restriction, and binding l and x_{j}. The latter is sufficient as the binding update will do the binding only if the type restrictions are satisfied; otherwise it will fail and initiate backtracking (c.f. the BINDING CONDITION of Section 3.2).

unify variable

if RUN
  & code(p) = unify variable(l,tt)
  & mode = Read      | mode = Write

then

  mk unbound(l,tt)   | mk unbound(h,tt)
  bind(l,nextarg)    | l ← <REF,h>
  nextarg := nextarg+| h := h+
  succeed

The instruction unify variable in Read mode has to make sure that the incoming argument satisfies the type restriction, which - as in get variable - is achieved by a bind update. In Write mode, the type restriction has just to be inserted into a new heap cell.

As argued above for put variable, the initialization of a free value cell during allocation as well as the put constraint instruction can also be dropped for all variables initialized by get variable or unify variable, which leads us to the INITIALIZATION LEMMA: Given l > e, the instruction put variable(l,x_{j},tt)

(get variable(l,x_{j},tt), unify variable(l,tt), resp.) is equivalent to initializing l

to unbound with mk unbound(l), executing put constraint(l,tt), and then executing

put unsafe value(l,x_{j}) (get value(l,x_{j}), unify local value(l), resp.). For a permanent

variable Y_{n}, the instruction put variable(y_{n},x_{j},tt) is equivalent to initializing y_{n} to unbound

with mk unbound(y_{n}), executing put constraint(y_{n},tt), and then executing put value(y_{n},x_{j}).

Thus, the rule for allocate looses its initialization update, and the compile function is modified such that no put constraint instruction is generated any more. Moreover, the argumentation of Section3.2 and 3.2 of [BR92b] can be applied to our modified setting, implying also the correctness of special compilation of facts and chain rules where no environment needs to be allocated at all.

5.3 Switching instructions and the Cut

The PAM contains all switching instructions known from the WAM, and since no type specific considerations have to be taken into account, their treatment in the evolving algebra approach in [BR92b] carries over to the PAM as well. Thus, compared to the compiled AND/OR structure (Sect. 2 and Appendix A) the indexing and choicepoint handling rules now also get the predicate arity n as an additional parameter, and the choicepoint information is not attached to a newly created stack element, but by reusing and “overwriting” elements on the stack (see B.7). However, in PROTOS-L additionally a switch on the type restriction of a variable is possible (see Section 7.2).

For the establishment of the Pure PROTOS-L Theorem we had deliberately left out the builtin predicate cut. Since there is no interdependence between cut and the type constraints of PROTOS-L, the cut treatment of Prolog carries over to our case as well [BR92a]: We could either extend every environment by a cutpointer, to be set and restored just as in Section 2, or we could allocate an extra (permanent) variable in those environments containig a so-called deep cut. This extra variable would then be set immediately after allocation, and its value would be assigned to the backtracking pointer b when a cut is encountered (see also [AK91]).

5.4 Main Theorem of Part I

Putting everything together developed so far, we obtain

Correctness Theorem 2 (Main Theorem of Part I): Compilation from PROTOS-L algebras to the PAM algebras developed so far is correct. Thus, since we kept the notion of types abstract, for every such type-constraint logic programming system L and for every compiler satisfying the specified conditions, compilation to the WAM extension with this abstract notion of types is correct.

Thus, any type system satisfying the minimal preconditions on the solution function stated in Section 2.1 is covered by the development above.

PART II: Polymorphic, order-sorted type constraints

6 PAM algebras with monomorphic type constraints

6.1 Binding

We are now ready for a first refinement of the binding update which will take into account the bind direction, occur check, and trailing, while the type constraints still remain abstract. We introduce two new 0-ary functions arg1, arg2 ∈ DATAAREA which will hold the locations given to the binding update, and extend the values of what to do by {Bind direction, Bind} indicating that we have to choose the direction of the binding resp. do the binding itself. The new 0-ary function return from bind will take values of the domain of what to do, indicating where to return when the binding is finished. (Remember that the binding update is used in different places, e.g. in the unify update or in the creation of a new heap variable).

For l_{1},l_{2} ∈ DATAAREA the binding update and some new abbreviations are defined by

         bind(l_{1},l_{2}) ≡ arg1 := l_{1}

                         arg2 := l_{2}
                         return from bind := what to do
                         what to do := Bind direction
         bind success ≡ what to do := return from bind
         BIND  ≡ OK & what to do = Bind
         trail(l_{1},l_{2}) ≡ ref¨ (tr) := (l_{1}, val(l_{1}))
                         ref¨ (tr+):= (l_{2}, val(l_{2}))
                         tr := tr++

In order to reset also the constant what to do upon backtracking, we refine the backtrack update to

         backtrack ≡ p := val(p(b))
                      unwind trail
                      what to do := Run

For unbound(l_{1}) there are two alternative conditions on the update occur check(l_{1},l_{2}), depending on whether the unification should perform the occur check (which is required for being logically correct) or not (which is done in most Prolog implementations for efficiency reasons):

OCCUR CHECK CONDITION: If no occur check should take place then the update occur check(l_{1},l_{2}) is empty; otherwise it has the following effect: If mk var(l_{1}) is among the variables of term(l_{2}) then the backtrack update will be executed.

We will leave the occur check update abstract, and all correctness proofs are thus implicitly parameterized by the decision whether it actually performs the occur check or not.

Bind-1 (Bind-Direction)

if OK
  & what to do = Bind direction
  & unbound(arg1)
  & (NOT (unbound(arg2)) |  unbound(arg2)
       or                | &
     arg2 < arg1)        |  arg2 > arg1      | arg1 = arg2

then

  what to do := Bind      | what to do := Bind | bind success
                         | arg1 := arg2      |
                         | arg2 := arg1      |

When binding two unbound variables their type constraints must be ‘joined’. For this purpose we introduce the function

inf: TYPETERM × TYPETERM → TYPETERM

which yields the infimum of two type terms, which may also be BOTTOM ∈ TYPETERM. TOP and BOTTOM can be thought of as ‘maximal’ and ‘minimal’ type terms. As integrity constraints we have

         inf(TOP,tt) = inf(tt,TOP) = tt
         inf(BOTTOM,tt) = inf(tt,BOTTOM) = BOTTOM
         solution({t : BOTTOM}) = nil
         solution({X : tt_{1}, X : tt_{2}}) = solution({X : inf(tt_{1},tt_{2})})

for any t ∈ TERM and tt_{i} ∈ TYPETERM.

Bind-2 (Bind-Var-Var)

if BIND
  & unbound(arg2)
  & LET inf = inf(ref(arg1),ref(arg2))
  & inf ≠ BOTTOM                           | inf = BOTTOM
  & inf ≠ ref(arg2)      | inf = ref(arg2)|

then

  trail(arg1,arg2)       | trail(arg1)     | backtrack
  insert type(arg2,inf)  |                 |
  arg1 ← <REF,arg2>                       |
  bind success                             |

When binding an unbound variable to a non-variable term, the type restriction of the variable must be propagated to the variables occurring in the term. As a special case this situation already occured in get structure(f,x_{i}) when the dereferenced value of x_{i} is a type-restricted variable. In that situation where the term was still to be built upon the heap, we ensured the propagation by writing arity(f) free value cells on the heap with appropriate type restrictions and continuing in read mode; the actual propagation was then achieved by the immediately following sequence of unify instructions. In the general case occurring in the binding rules, the arguments of the term are not just variables but arbitrary terms. However, as we will not go into the details of type constraint solving here, we assume an abstract propagate update satisfying the following:

PROPAGATION CONDITION: For any l_{1}, l_{2}, l ∈ DATAARRA, with term resp. term' values of term(l), with prefix resp. prefix' values of type prefix(l), and with val resp. val' values of val(l), before resp. after execution of propagate(l_{1},l_{2}) we have if unbound(l_{1}),

ref(l_{1}) ∈ TYPETERM, tag(l_{2}) = STRUC, and term(l_{2}) ∈ TERM:
         LET CS = {term(l_{2}) : ref(l_{1})}
         if solvable(CS) = true
         then (a) (term', prefix') = conres(term, prefix, CS)

(b) if val ≠ val' then the location l will be trailed else backtrack update will be executed

With this update at hand the third binding rule is

Bind-3 (Bind-Var-Struc)

if BIND
  & NOT (unbound(arg2))

then

  trail(arg1)
  arg1 ← <REF,arg2>
  occur check(arg1,arg2)
  propagate(arg1,arg2)

BINDING LEMMA 1: The bind rules are a correct realization of the binding update of Section 3.2, i.e. the BINDING CONDITIONS 1 and 3 (and thus also 2), the TRAILING CONDITION as well as the STACK VARIABLES PROPERTY are preserved. Proof: The proof for the update bind(l_{1},l_{2}) is by case analysis and induction on the size of term(l_{2}), relying on the integrity conditions for the infimum function on type terms when binding one type-restricted variable to another one (Bind-2), resp. on the Propagation Condition when binding a variable to a non-variable term (Bind-3).

6.2 Monomorphic, order-sorted types

Before introducing a representation for type terms we introduce some new functions and universes that are related to TYPETERM. Note that until now we have kept TYPETERM indeed abstract; it is only in this section that we come to some more specific type term characteristics such as monomorphic and polymorphic type terms. However, following our principle of stepwise refinement of the PAM development, we first deal only with monomorphic type constraints solving, while the details of polymorphic type constraint handling will still be kept abstract in this section.

On the universes TYPETERM and SYMBOLTABLE we introduce the functions

is top: TYPETERM → BOOL

         is monomorphic: TYPETERM → BOOL
         is polymorphic: TYPETERM → BOOL

with their obvious meaning. The function

target sort: SYMBOLTABLE → SORT

yields the target sort of a constructor, where SORT is a new universe, representing sort names. It comes with a function

subsort: SORT × SORT → BOOL

defining the order relation on the monomorphic sorts (and being undefined on the polymorhic sorts [Bei90]), respectively. For the refinement of type constraint handling we assume two functions

sort glb: SORT × SORT → SORT

poly inf: TYPETERM × TYPETERM → TYPETERM

that refine the inf function (from 6.1) in the sense that for any tt_{1}, tt_{2} ∈ TYPETERM

         inf(tt_{1},tt_{2}) = \{ \begin{matrix}sort glb(tt_{1}, tt_{2}) & if is monomorphic(tt_{1}) \\ & and is monomorphic(tt_{2}) \\ poly inf(tt_{1}, tt_{2}) & if is polymorphic(tt_{1}) \\ & and is polymorphic(tt_{2}) \end{matrix}

For constraint solving involving a monomorphic type term s and t = f(…) ∈ TERM we have the integrity constraint

             solution(\{t : s\}) = \{ \begin{matrix}∅ & if subsort(target sort(f),s) \\ nil & otherwise \end{matrix}

i.e. the solvability of a monomorphic type constraint depends solely on the subsort relationship between the required sort and the target sort of the top-level constructor of the term. It will turn out that this suffices for the refinement of monomorphic type constraint handling.

6.3 Representation of types

For the PAM representation of typeterms we introduce a pointer algebra, similar to DATAAREA, which will be used for the representation of both monomorphic types and polymorphic type terms (for the latter see Section 8):

         (TYPEAREA; ttop, tbottom, TOP; +, -; tval)
         ttop, tbottom, TOP: → TYPEAREA

+, -: TYPEAREA → TYPEAREA

tval: TYPEAREA → TO

The functions ttag and tref are defined on the universe of “type objects” TO

ttag: TO → TTAGS

tref: TO → SORT + TYPEAREA

with the tags for type terms given by (to be extended later)

         { S TOP, S MONO, S POLY } ⊆ TTAGS

Similar as done before, we abbreviate ttag(tval(l)) and tref(tval(l)) by ttag(l) and tref(l). As integrity constraints we have

         if ttag(l) = S MONO then tref(l) ∈ SORT
                                    is monomorphic(tref(l))
         if ttag(l) = S POLY then is polymorphic(tref(l))

where the auxiliary function

typeterm: TYPEAREA → TYPETERM

satisfies the constraints

         typeterm(l) = TOP  if ttag(l) = S TOP
         typeterm(l) = tref(l)  if ttag(l) = S MONO

We refine the PAM algebras of Section 5 by replacing the universe TYPETERM by its representing universe TYPEAREA. The codomain of the ref function (from 3.1) now contains TYPEAREA, and in the integrity constraints of 3.1 as well as in the definition of type prefix the case for unbound(l) now contains typeterm(ref(l)) instead of ref(l). The three abstract functions is top, is monomorphic, and is polymorphic defined on TYPETERM are defined on TYPEAREA by just looking at the type tag; for l ∈ DATAAREA we therefore use the following abbreviations:

         top(l)  ≡ tag(l) = VAR & ttag(ref(l)) = S TOP
         monomorphic(l) ≡ tag(l) = VAR & ttag(ref(l)) = S MONO
         polymorphic(l) ≡ tag(l) = VAR & ttag(ref(l)) = S POLY
         sort(l)  ≡ typeterm(ref(l))  if monomorphic(l)

6.4 Initialization of type constrained variables

In the PAM algebras developed so far the update insert type(l,t) is used - as part of the mk unbound update - in the variable initialization instructions get variable, put variable, and unify variable (Section 5.2). (Its use in the multiple mk unbounds update in get structure will be refined in Section 6.6 below). This update is now refined by

         insert type(l,tt) ≡ if is top(tt)
                                then insert top(l)
                                else if is monomorphic(tt)
                                    then insert mono(l,tt)
                                    else insert poly(l,tt)
         insert top(l)  ≡ ref(l) := ttop
                              ttag(ttop) := S TOP
                              ttop := ttop+
         insert mono(l,s) ≡ ref(l) := ttop
                              ttag(ttop) := S MONO
                              tref(ttop) := s
                              ttop := ttop+

where we use a new type area location when inserting a monomorphic sort s (resp. TOP) as restriction for location l ∈ DATAAREA. ^{2}

Similarly, the insertion of polymorphic type terms by insert poly(l,tt) will be handled in Section 8. As we want to leave the details of polymorphic type constraint solving still abstract here, we pose the following

POLYMORPHIC TYPE INSERTION CONDITION: For any l_{1}, l ∈ DATAARRA,

with term resp. term' values of term(l) and with prefix resp. prefix' values of type prefix(l)

before resp. after execution of insert poly(l_{1},tt), we have if unbound(l_{1}) and tt ∈

TYPETERM with is polymorphic(tt):
         (term', prefix') = conres(term, prefix\mk var(l_{1}), {mk var(l_{1}) : tt})

TYPE INSERTION LEMMA: The refinement of the insert type update satisfies the TYPE INSERTING CONDITION of 3.5. Proof: By straightforward case analysis for TOP, monomorphic and polymorphic type restrictions; for the latter the POLYMORPHIC TYPE INSERTION CONDITION is used.

6.5 Binding of type constrained variables

We refine the binding rules of Section 6.1 according to the type term representation. Rule Bind-1 remains unchanged, whereas the rule Bind-2 for binding two variables is replaced by the following four rules:

Bind-2a (Bind-TOP-Any)

if BIND
  & top(arg1)
  & unbound(arg2)) | NOT (unbound(arg2))

2Note that deliberately we have left out the re-use of type area locations. For trailing, we have to preserve old type restrictions to be recovered upon backtracking. However, locations that will not be reached any more by backtracking can be re-used, just as e.g. memory on the local stack or on the heap is freed for re-use upon backtracking. In the current PAM implementation the type area is embedded into the heap so that the same mechanism for allocating and deallocating can be used. However, other realizations are also possible, and we will not elaborate this topic in this paper.

then

trail(arg1)
arg1 ← <REF,arg2>
bind success     | occur check(arg1,arg2)

Bind-2b (Bind-Var-TOP)

if BIND
& monomorphic(arg1) OR polymorphic(arg1)
& top(arg2)

then

trail(arg1,arg2)
arg1 ← <REF,arg2>
arg2 ← arg1
bind success

Bind-2c (Bind-Mono-Mono)

if BIND
& monomorphic(arg1)
& monomorphic(arg2)
& LET glb = sort glb(sort(arg1),sort(arg2))
& glb ≠ BOTTOM                           | glb = BOTTOM
& glb ≠ sort(arg2)    | glb = sort(arg2)|

then

trail(arg1,arg2)      | trail(arg1)      | backtrack
insert type(arg2,glb) |                  |
arg1 ← <REF,arg2>                       |
bind success                             |

Bind-2d (Bind-Poly-Poly)

if BIND
& polymorphic(arg1)
& polymorphic(arg2)

then

trail(arg1)
arg1 ← <REF,arg2>
poly infimum(arg1,arg2)

The only still abstract update in these rules is the poly infimum(l_{1},l_{2}) update used when binding two polymorphically restricted variables, for which we require the following

POLYMORPHIC INFIMUM CONDITION: For any l_{1}, l_{2}, l ∈ DATAAREA, with

term resp. term' values of term(l), with prefix resp. prefix' values of type prefix(l), and

with val resp. val' values of val(l), before resp. after execution of poly infimum(l_{1},l_{2}) we

have if for i = 1,2 unbound(l_{i}), polymorphic(l_{i}), and typeterm(ref(l_{i})) ∈ TYPETERM:
       LET CS = {mk var(l_{2}) : poly inf(typeterm(l_{1}),typeterm(l_{2}))}
       if solvable(CS) = true
       then (a) (term', prefix') = conres(term, prefix, CS)

(b) if val ≠ val' then the location l will be trailed else backtrack update will be executed

Rule Bind-3 of Section 6.1 for binding a variable to a non-variable structure is replaced by the rules Bind-2a above (which already covers the case that the variable has no type restriction, denoted by TOP) and the two new rules

Bind-3a (Bind-Mono-Struc)

if BIND
  & monomorphic(arg1)
  & NOT (unbound(arg2))
  & subsort(target sort(ref(arg2)),sort(arg1))
       = true           |  = false

then

  trail(arg1)           | backtrack
  arg1 ← <REF,arg2>     |
  occur check(arg1,arg2) |

Bind-3b (Bind-Poly-Struc)

if BIND
  & polymorphic(arg1)
  & NOT (unbound(arg2))

then

  trail(arg1)
  arg1 ← <REF,arg2>
  occur check(arg1,arg2)
  poly propagate(arg1,arg2)

The abstract update poly propagate(l_{1},l_{2}) must satisfy the

POLYMORPHIC PROPAGATION CONDITION which is obtained from the PROPA-GATION CONDITION of 6.1 by adding is polymorphic(l_{1}) as an additional precondition and

replacing ref(l_{1}) by typeterm(ref(l_{1})).

BINDING LEMMA 2: The refined binding rules are a correct realization of the binding rules of Section 6.1 and thus also of the binding update of 3.2. Proof: Following the proof of the BINDING LEMMA in 6.1 we have to show that the rules Bind-2a - Bind-2d and Bind-3a - Bind-3b are correct realizations of the inf function used in Bind-2 and of the propagate update used in Bind-3. This follows by straightforward case analysis for TOP, monomorphic, and polymorphic type restrictions: For TOP, we use its property that it is ‘maximal’ w.r.t. inf and that the propagate update can not have any effect since any TOP restriction trivially holds (Section 2.1). For the monomorphic case we conclude from the last integrity constraint given in Section 6.2 that the propagate update is either empty or fails immediately due to the subsort test, implying that the different cases correctly simulate this situation. For the polymorphic case the POLYMORPHIC INFIMUM and POLYMORPHIC PROPAGATION CONDITIONS are used.

6.6 Getting of structures

We refine the get struture rules of Section 3.4 according to the type term representation. Rule Get-Structure-1 remains unchanged, whereas the rule Get-Structure-2 for the case that x_{i} is an unbound variable is replaced by the following two rules:

Get-Structure-2a

if RUN
  & code(p) = get structure(f,x_{i})
  & monomorphic(deref(x_{i}))
  & NOT ( subsort(target sort(f),sort(deref(x_{i}))) )

then

  backtrack

Get-Structure-2b

if RUN
  & code(p) = get structure(f,x_{i})
  & top(deref(x_{i}))            | polymorphic(deref(x_{i}))
         OR                   |
    (monomorphic(deref(x_{i})) & |
     subsort(target sort(f),  |
             sort(deref(x_{i}))) |

then

  h ← <STRUC,h+>
  bind(deref(x_{i}),h)
  val(h+) := f
  h := h++                    | h := h + arity(f) + 2
  mode := Write               | nextarg := h++
                              | mode := Read
                              | FORALL i = 1,. . .,arity(f) DO
                              |    mk unbound(h+i)
                              | ENDFORALL
                              | poly propagate(h+,deref(x_{i}))
  succeed

Thus, the only remaining abstract update is in the case when x_{i} is a polymorphically restricted variable; this case in Get-Structure-2b is reduced to the more general update poly propagate already introduced in the previous subsection.

CORRECTNESS OF GET-STRUCTURE REFINEMENT: The refined Get-Structure rules are a correct realization of the rules of Section 3.4, i.e. the GETTING LEMMA stills holds for the refined type term representation. Proof: As in the proof of the BINDING LEMMA 2 in the previous subsection we can apply a straightforward case analysis for TOP, monomorphic, and polymorphic type restrictions: For TOP, we

observe that always both conditions can propagate(f,TOP) and trivially propagates(f,TOP)

used in the Get-Structure rule of 3.4 hold. For monomorphic type restrictions, the propagation reduces again to the subsort test. For the polymorphic case the POLYMORPHIC PROPAGATION CONDITION ensures that exactly the type restrictions given by the propagate list function used in 3.4 are propagated onto the arguments of the structure.

Whereas we have now introduced a representation for type terms and rules for monomorphic type constraint solving, some details of polymorphic type constraint solving are still abstract, namely the three updates insert poly(l,tt), poly infimum(l_{1},l_{2}), and poly propagate(l_{1},l_{2}) which will be refined in Section 8.

7 PAM Optimizations

7.1 Special representation for typed variables

Many of the type related rules introduced above - in particular the get-structure and the binding rules - apply only if the involved variable has no type restriction at all (i.e. TOP), or a monomorphic, or a polymorphic type restriction, respectively. In the spirit of the WAM’s tagged architecture it is thus sensible to distinguish these three different cases efficiently by special tags [BMS91]. The tag VAR is therefore replaced by the three tags FREE, FREE M, FREE P.

Moreover, in the representation of monomorphic sorts one can also easily save a type area location by letting the ref value of a data area location point directly to SORT. Therefore, we extend the codomain of the function ref (see 3.1) to include also SORT. Let l ∈ DATAAREA; instead of

val(l) = <VAR,t>  and  tval(t) = <S MONO,s>

we will just have

val(l) = <FREE M,s>

and instead of

val(l) = <VAR,t>  and  ttag(t) = S TOP

we will just have

tag(l) = FREE

This motivates the following modified abbreviations:

mk unbound(l)  ≡ tag(l) := FREE
mk unbound mono(l,s) ≡ tag(l) := FREE M
                        ref(l) := s
mk unbound poly(l,tt) ≡ tag(l) := FREE P
                        insert poly(l,tt)
mk unbound(l,tt)  ≡ if is top(tt)
                          then mk unbound(l)
                          elseif is monomorphic(tt)
                                then mk unbound mono(l,tt)
                                else mk unbound poly(l,tt)
unbound(l)  ≡ tag(l) ∈ {FREE, FREE M, FREE P}
top(l)  ≡ tag(l) = FREE
monomorphic(l) ≡ tag(l) = FREE M
polymorphic(l) ≡ tag(l) = FREE P
sort(l)  ≡ ref(l)  if monomorphic(l)

The integrity constraint for the case unbound(l) of Section 3.1 is replaced by

if tag(l) = FREE M then ref(l) ∈ SORT
if tag(l) = FREE P then ref(l) ∈ TYPEAREA
                          typeterm(ref(l)) ∈ TYPETERM
                          is polymorphic(typeterm(ref(l)))

and in the definition of type prefix the case for unbound(l) is refined to

type prefix(l) = \{ \begin{matrix}mk var(l) : TOP & if tag(l) = FREE \\ mk var(l) : ref(l) & if tag(l) = FREE M \\ mk var(l) : typeterm(ref(l)) & if tag(l) = FREE P \\ . . . \end{matrix}

Every time a new variable is created, this refined representation of variables will be taken into account by one of the specialized mk unbound updates introduced above; for instance in the Get-Structure-2b rule (Section 6.6).

Similarly, the rules for initializing variables (Section 5.2) are modified as explained in the following. In order to take advantage of the refined variable representation we modify the compile function such that each instruction of the form

         get variable(l,x_{j},tt)

is replaced by one of the three new instructions

         get free(l,x_{j})
         get mono(l,x_{j},tt)
         get poly(l,x_{j},tt)
depending on whether is top(tt), is monomorphic(tt), or is polymorphic(tt) holds. Like-

wise, all put variable and unify variable instructions are replaced by the instructions

         put free(l,x_{j})           unify free(l)
         put mono(l,x_{j},tt)        unify mono(l,tt)
         put poly(l,x_{j},tt)        unify poly(l,tt)

respectively. Note that these new instructions always correspond to the first occurrence of a variable in a clause and are thus responsible for the correct type initialization of that variable.

Put-1 (X variable)

if RUN
  & code(p) =
      put free(x_{i},x_{j}) | put mono(x_{i},x_{j},s)    | put poly(x_{i},x_{j},tt)

then

  mk unbound(h)      | mk unbound mono(h,s) | mk unbound poly(h,tt)
  x_{i} ← <REF,h>
  x_{j} ← <REF,h>
  h := h+
  succeed

Put-2 (Y variable)

if RUN
  & code(p) =
      put free(y_{n},x_{j}) | put mono(y_{n},x_{j},s)    | put poly(y_{n},x_{j},tt)

then

  mk unbound(y_{n})      | mk unbound mono(y_{n},s)| mk unbound poly(y_{n},tt)
  x_{j} ← <REF,y_{n}>
  succeed

Get (Variable)

if RUN
  & code(p) =
      get free(l,x_{j}) | get mono(l,x_{j},s)    | get poly(l,x_{j},tt)

then

  l ← x_{j}  | mk unbound mono(l,s)| mk unbound poly(l,tt)
                     | bind(l,x_{j})          | bind(l,x_{j})
  succeed

Unify (Read Mode)

if RUN
  & code(p) =
      unify free(l)  | unify mono(l,s)     | unify poly(l,tt)
  & mode = Read

then

  l ← <REF,nextarg> | mk unbound mono(l,s)| mk unbound poly(l,tt)
                     | bind(l,nextarg)     | bind(l,nextarg)
  nextarg := nextarg+
  succeed

Unify (Write Mode)

if RUN
  & code(p) =
      unify free(l) | unify mono(l,s)     | unify poly(l,tt)
  & mode = Write

then

  mk unbound(h)     | mk unbound mono(h,s)| mk unbound poly(h,tt)
  l ← <REF,h>
  h := h+
  succeed

CORRECTNESS OF REFINED VARIABLE REPRESENTATION: The PAM algebras with the refined variable representation are correct with respect to the PAM algebras constructed in Section 6. Proof: The only type inserting update of 6.4 that is still used is insert poly for which the POLY-MORPHIC TYPE INSERTION CONDITION ensures the TYPE INSERTION CONDITION. Inserting TOP and monomorphic type restrictions for variables obviously has the same effect as in 6.4. Trailing still works fine since in 4.2 we trailed the complete val decoration of a data area location - including its tag - and restored it upon backtracking. With these two main observations the proof follows by case analysis for the three different kinds of type restrictions. Showing that each variable is initialized properly is straightforward, and the correct treatment of the thus refined variable representation in all relevant rules (in particular the binding rules) is ensured directly by our modified abbreviations that refer to a variable’s representation, like monomorphic(l) or

sort(l).

7.2 Switch on Types

As opposed to the WAM, in the PAM also a switch on the subtype restriction of a variable is possible (c.f. 5.3) which increases the determinancy detection abilities. Since only monomorphic types can have explicitly defined subtypes there are two switch-on-term instructions. (Note that in this paper we did not introduce special representations for constants, lists, or built-in integers; they are, however, present in the PAM and could be added to our treatment without difficulties, which would lead to additional parameters in the following instructions.)

Switch-on-poly-term

if RUN
  & code(p) = switch on poly term(i,Lfree,Lstruc)
  & tag(deref(x_{i})) ∈ {FREE, FREE P} | tag(deref(x_{i})) = STRUC

then

  p := Lfree                        | p := Lstruc

The switch on poly term instruction is as the WAM switch on term instruction (c.f. B.7) except that the variable may carry a polymorphic type restriction, which however does not lead to the exclusion of any clauses, since in PROTOS-L no explicit subtype relationships are allowed between polymorphic types [Bei90].

Switch-on-mono-term

if RUN
  & code(p) = switch on mono term(i,Lfree,Lfree m,Lstruc)
  & tag(deref(x_{i})) =
       FREE   | FREE M       | STRUC

then

  p := Lfree  | p := Lfree m | p := Lstruc

In the switch on mono term instruction we distinguish the two cases for a FREE variable and a FREE M variable. In the first case again no clauses can be excluded form further consideration, but in the second case only those clauses that are compatible with x_{i}’s subtype restriction have to be taken into account. The latter is achieved by setting the program counter p to a label where a switch on sort instruction will exploit x_{i}’s subtype restriction:

Switch-on-sort

if RUN
  & code(p) = switch on sort(i,Table)

then

  p:=select_{sort}(Table,sort(deref(x_{i})))

where Table is a list of pairs of the form SORT × CODEAREA, and select_{sort}(Table,s) yields the location c such that (s,c) is in Table.

In order to establish a correctness proof for the extended switching instructions we must extend the assumptions on the compiler stated in 2.2. The defintion of chain is changed so that the two cases for switch on term are replaced by

chain(Ptr) = \{ \begin{matrix}chain(Lf) & if code(Ptr) = switch on poly term(i,Lf,Ls) \\ and is top(X_{i}) or is polymorphic(X_{i}) \\ chain(Ls) & if code(Ptr) = switch on poly term(i,Lf,Ls) \\ and is struct(X_{i}) \\ chain(Lf) & if code(Ptr) = switch on mono term(i,Lf,Lfm,Ls) \\ and is top(X_{i}) \\ chain(Lfm) & if code(Ptr) = switch on mono term(i,Lf,Lfm,Ls) \\ and is monomorphic(X_{i}) \\ chain(Ls) & if code(Ptr) = switch on mono term(i,Lf,Lfm,Ls) \\ and is struct(X_{i}) \\ chain(select_{sort}(T,s)) & if code(Ptr) = switch on sort(i,T) \\ and s = sort(X_{i}) \\ . . . \end{matrix}

SWITCHING LEMMA: Switching extended to types preserves correctness. Proof: By case analysis using the extended chain definition, and relying on the correctness of the other building blocks of the determinancy detection mechanism (like try, retry, trust, etc.) which remain unchanged.

Note that the special representation of typed variables introduced in this section lead to the situation that the type extension in the PAM is indeed orthogonal to the WAM. Any untyped program is carried out in the PAM with the same efficiency as in the WAM: Adding the trivial one-sorted type information to such a program reveals that the PAM code will contain only the FREE-case for variables. Apart form the minor difference of representing a free (unconstrained) variable not by a selfreference (as in the WAM) but by a special tag, the generated and executed code is thus exactly the same for both the WAM and the PAM. On the other hand, any typed program exploiting e.g. the possibilities of computing with subtypes can take advantage of the type constraint handling facilities in the PAM which would have to be simulated by additional explicit program clauses in an untyped version.

8 Polymorphic type constraint solving

In this section polymorphic type constraint handling is refined by refining the three updates

insert poly(l,tt), poly infimum(l_{1},l_{2}), and poly propagate(l_{1},l_{2}) that have been left ab-

stract so far.

8.1 Representation of polymorphic type terms

For the representation of polymorphic type terms we introduce an additional function on SORT

sort arity: SORT → NAT

yielding the arity of a polymorphic sort (which must be 0 in the case of a monomorphic sort). The relationship between the declaration part of the program prog (see 2.1 and 2.4) and the functions on SORT is regulated by the following integrity constraints: For each function declaration of the form

f: d_{1} … d_{m} → s(α_{1},…,α_{n})

with m, n ≥ 0, pairwise distinct (type) variables α_{i} that occur in d_{1},…,d_{m}, and each tt = s(…) ∈ TYPETERM the following holds:

target sort(entry(f, m)) = s
arity(entry(f, m)) = m
sort arity(s) = n
is monomorphic(tt) = true  iff  n = 0
is polymorphic(tt) = true  iff  n > 0

Let use illustrate these integrity constraints by some examples. Consider the three function declarations

succ:    nat → nat
cons:  α × list(α) → list(α)
mk pair: α × β → pair(α, β)

Then we have e.g. the following relationships:

target sort(entry(succ,1))    = nat
target sort(entry(cons,2))    = list
target sort(entry(mk pair,2)) = pair
arity(entry(succ,1))   = 1
arity(entry(cons,2))   = 2
arity(entry(mk pair,2) = 2
sort arity(nat)  = 0
sort arity(list) = 1
sort arity(pair) = 2
is monomorphic(nat)           = true
is polymorphic(list(list(γ))) = true

Since the type terms required at run time are represented in TYPEAREA, we add two new tags S REF and S BOTTOM to the set of type tags, yielding

TTAGS = { S TOP, S BOTTOM, S MONO, S REF, S POLY }

where S REF corresponds to the subterm reference STRUC used in DATAAREA for ordinary terms. Together with the additional integrity constraints

         if tag(l) = S REF  then tref(l) ∈ TYPEAREA
                                   ttag(tref(l)) = S POLY
         if tag(l) = S POLY then tref(l) ∈ SORT
                                   is polymorphic(typeterm(l))

the function

typeterm: TYPEAREA → TYPETERM

introduced in Section 6.3 is now completely defined by

        typeterm(l) = \{ \begin{matrix}TOP & if ttag(l) = S TOP \\ BOTTOM & if ttag(l) = S BOTTOM \\ tref(l) & if ttag(l) = S MONO \\ typeterm(tref(l)) & if ttag(l) = S REF \\ s(a_{1},. . .,a_{n}) & if ttag(l) = S POLY and \\ & s = tref(l) \\ & n = sort arity(tref(l)) \\ & a_{i} = typeterm(tref(l)+i) \end{matrix}

8.2 Creation of polymorphic type terms

We introduce a representation of polymorphic type terms occurring as arguments of the instructions in CODEAREA such that they can easily be loaded into TYPEAREA. For this purpose, we extend the compile function such that every polymorphic type term tt occurring in any of the generated PAM instructions introduced so far (i.e. put , get , unify variable, respectively their refinements put free, put mono etc., see Section 7) is replaced by

         compile type(tt) ∈ (TTAG × (SORT + NAT))^{∗}

Note that just for simplicity reasons this list representation abstracts away from the actual representation used in the PAM where the tagged type term representation occurring in the code is embedded into CODEAREA, mapping the list structure to the +-structure of CODEAREA. The function inverse to compile type is defined by

decompile type(L) = \{ \begin{matrix}TOP & if head(L) = <S TOP,.> \\ BOTTOM & if head(L) = <S BOTTOM,.> \\ s & if head(L) = <S MONO,s> \\ decompile type(\underbrace{tail(. . . (tail}_{m−times}(L)). . .)) & if head(L) = <S REF,m> \\ s(a_{1},. . .,a_{n}) & if head(L) = <S POLY,s> and \\ n = sort arity(tref(l)) \\ a_{i} = decompile type(\underbrace{tail(. . . (tail}_{i−times}(L)). . .)) \end{matrix}

and the integrity constraint we impose is

         decompile type(compile type(tt)) = tt

for any type term tt ∈ TYPETERM.

Using compile type(tt) instead of tt itself passes this refined argument to the update mk unbound. Since the update mk unbound is defined in terms of insert type which in turn is defined in terms of insert poly for the polymorphic case, we only have to adapt the - until now - abstract update insert poly (Section 6.4). It is now defined by

         insert poly(l,L) ≡ ref(l) := ttop
                             FORALL j = 1,. . .,length(L) DO
                                tval(ttop+j-1) := offset(ttop+j-1,nth(j,L))
                             ENDFORALL
                             ttop := ttop + length(L)

where

              offset(tl, <tag,k>) = \{ \begin{matrix}<tag, tl+k> & if tag = S REF \\ <tag, k> & otherwise \end{matrix}

POLYMORPHIC TYPE INSERTION LEMMA: The representation of type terms and the update defined above are a correct realization of the insert poly update of Section 6.4, i.e. the POLYMORPHIC TYPE INSERTION CONDITION is satisfied. Proof: The list representation generated by the function compile type reflects exactly the structure of the representation of type terms in TYPEAREA, the only difference being that a sub- (type-)term pointer in TYPEAREA (with tag S REF) is realized by an integer offset in the list representation. This representation difference is taken into account in the definition of insert poly given above by adding the offset to the current TYPEAREA location in the S REF case.

8.3 Polymorphic infimum

In order to refine the still abtract update poly infimum(l_{1},l_{2}) used in the Bind-2d rule of Section 6.5 to the infimum computation of polymorphic type terms as they occur in PROTOS-L, we need to know whether a type term is empty or not. For instance, given the standard notions of list(α_{1}) and pair(α_{1},α_{2}), list(BOTTOM) is not empty since it can be instantiated to the empty list nil, while pair(BOTTOM,INTEGER) is empty since there is no pair without a first component. The property that a type tt is not empty is formalized by the abbreviation

         inhabited(tt) ≡ solution({X : tt}) ≠ nil

where X ∈ VARIABLE. Thus, from the conditions on the solution function in 6.1

we have e.g. inhabited(BOTTOM) = false, inhabited(TOP) = true, and furthermore
inhabited(list(BOTTOM)) = true, inhabited(pair(BOTTOM,INTEGER)) = false.

We pose three additional integrity conditions. The first one requires that there are no ‘empty’ (monomorphic) sorts:

         is monomorphic(s) ⇒ inhabited(s)

The second integrity constraint says that the infimum of polymorphic type terms is computed from the infimum of the argument types, and that it is always BOTTOM if we have different polymorphic types:

poly inf(s(tt_{1},. . .,tt_{n}),s'(tt_{1}',. . .,tt_{n}')

= \{ \begin{matrix}s(poly inf(tt_{1},tt_{1}'),. . .,(poly inf(tt_{n},tt_{n}')) & if s = s' \\ and \\ inhabited(s(poly inf(tt_{1},tt_{1}'),. . .,poly inf(tt_{n},tt_{n}'))) \\ BOTTOM & otherwise \end{matrix}

For the third integrity constraint we introduce a new abstract function inst modus: SORT × BOOL^{∗} → BOOL

which tells whether terms of a given sort can be instantiated, depending only on the emptiness of the argument types, but not on the arguments themselves. This function specifies the ‘instantiation modi’ for a polymorphic sort, i.e. which type arguments of s may be BOTTOM so that s can still be instantiated. For instance, we have

         inst modus(list, [false]) = true
         inst modus(pair, [false, true]) = false

since

         solution({X : list(BOTTOM)}) ≠ nil
         solution({X : pair(BOTTOM,INTEGER)}) = nil

and thus

         inhabited(list(BOTTOM)) = true
         inhabited(pair(BOTTOM,INTEGER)) = false.

The general condition on inst modus is

         inst modus(s,[b_{1},. . .,b_{n}]) = true

              ⇒ ( (∀ i ∈ {1,. . .,n} .  b_{i} = true ⇒ inhabited(tt_{i}) )
                     ⇒ inhabited(s(tt_{1},. . .,tt_{n})) )

For the realization of the poly inf function in the PAM we introduce a new universe P NODE that comes with a tree structure realized by the functions

         p root, p current: P NODE

p father: P NODE → P NODE p sons: P NODE → P NODE^{∗}

where p current is used to navigate through the tree. Each node in the P NODE tree represents an infimum computation task for two type terms given as arguments, and it will be eventually be marked with the result. Thus, we have the three labelling functions

p arg1, p arg2: P NODE → TYPEAREA p result: P NODE → TYPEAREA

When a P NODE element p represents the computation of the infimum of two polymorphic type

terms typeterm(p arg1(p)) = s(tt_{1},. . .,tt_{n}) and typeterm(p arg2(p)) = s(tt_{1}',. . .,tt_{n}'),

then the n required computations of the infimum of the tt_{i} and tt_{i}' will correspond to the n nodes in the list p sons(p). The P NODE label

         p status:  P NODE → {expand, expanded}

indicates for each node whether the son nodes for it have still to be generated or not. The until now abtract update poly infimum(l_{1},l_{2}) for l_{1}, l_{2} ∈ DATAAREA is then defined by

         poly infimum(l_{1},l_{2}) ≡ p arg1(p root) := ref(l_{1})
                               p arg2(p root) := ref(l_{2})
                               p status(p root) := expand
                               p current := p root
                               p return arg := l_{2}
                               ll what to do := polymorphic infimum

It initializes the P NODE tree containing just the root node. Additionally, it sets the new 0-ary function

         p return arg : DATAAREA

which holds the location where the result of the polymorphic infimum computation will be written to when it has been finished.

         ll what to do ∈ {none, polymorphic infiumum, polymorphic propagation}

is also a new 0-ary function that is added to the initial PAM algebras. Its initial value is none, indicating that no specific low-level actions have to be performed. All rules introduced so far get ll what to do = none as an additional precondition; thus the definition of the poly infimum(l_{1},l_{2}) update just given blocks the applicability of all previous rules, until ll what to do has been set back again to the value none by one of the rules to be introduced below. These new rules in turn will be guarded by the precondition

         POLY-INF ≡ OK & ll what to do = polymorphic infimum

(Note that such a scheme has been used before with the 0-ary function what to do, separating e.g. the binding and unification rules from all other rules.) Resetting of ll what to do is done by means of the following abbreviation that holds for tl ∈ TYPEAREA and that is also used for the returning of values in intermediate stages of the polymorphic infimum computation:

         p return(tl) ≡ if p current ≠ p root
                         thenp result(p current) := tl
                             p current := p father(p current)
                         else ll what to do := none
                             if ttag(tl) = S BOTTOM
                             then backtrack
                             else bind success
                                  if ref(p return arg) ≠ tl
                                     then trail(p return arg)
                                          ref(p return arg) := tl

Note that the last if-then conditional is an optimization over the unconditional updates in the then-part since in case the return argument location p return arg already contains the required value we neither have to update nor to trail it. Additionally, the following abbreviations will be used:

         parg1 ≡ p arg1(p current)
         parg2 ≡ p arg2(p current)
         ttag1 ≡ ttag(parg1)
         ttag2 ≡ ttag(parg2)
         tref1 ≡ tref(parg1)
         tref2 ≡ tref(parg2)

If either of the two type term arguments of p current is TOP or BOTTOM, no son nodes have to be created and the result can be determined immediately since it is given by one of the two arguments.

Polymorphic Infimum 1 (S TOP, S BOTTOM)

if POLY-INF
  & p status(p current) = expand
  & (ttag1 = S TOP              | (ttag1 = S BOTTOM
        OR                      |     OR
     ttag2 = S BOTTOM)          |  ttag2 = S TOP)

then

  p status(p current) := expanded
  p return(parg2)               | p return(parg1)

Also in the case of monomorphic types no son nodes have to be created.

Polymorphic Infimum 2 (S MONO)

if POLY-INF
  & p status(p current) = expand
  & ttag1 = S MONO  &  ttag2 = S MONO
  & subsort(tref1, | subsort(tref2, | sort glb(tref1,tref2) | sort glb(tref1,tref2)
            tref2) |         tref1) |  = BOTTOM          |  ≠ BOTTOM

then

  p status(p current) := expanded
  p return(parg1)  | p return(parg2)| make s bottom         | make s mono(
                   |                |                       | sort glb(tref1,tref2))
                   |                | p return(ttop)        | p return(ttop)

where for s ∈ SORT the allocation of new type locations in TYPEAREA is achieved by

         make s mono(s) ≡ ttag(ttop) := S MONO
                          tref(ttop) := s
                          ttop := ttop+
         make s bottom ≡ ttag(ttop) := S BOTTOM
                          ttop := ttop+

If p current points to a node with S POLY tagged arguments for the first time (i.e. its status is expand), sort arity(tref(p arg1(p current))) new son nodes are created and labelled accordingly (c.f. the integrity condition on poly inf given above). p current is set to the first of the new sons, and the new function

p rest calls: P NODE → P NODE^{∗}

is set to the remaining son nodes, indicating that these nodes still have to be visited by p current.

Polymorphic Infimum 3 (S POLY-1)

if POLY-INF
  & p status(p current) = expand
  & ttag1 = S POLY  &  ttag2 = S POLY

then

  p status(p current) := expanded
  LET n = sort arity(tref1)
  extend P NODE by temp(1),...,temp(n)
     where p arg1(temp(i)) := parg1 + i
            p arg2(temp(i)) := parg2 + i
            p father(temp(i)) := p current
            p sons(p current) := [temp(1),. . .,temp(n)]
            p status(temp(i)) := expand
            p current := temp(1)
            p rest calls(p current) := [temp(2),. . .,temp(n)]

endextend

When p current points to a node with S POLY tagged arguments for the second or a later time (i.e. its status is expanded) and there are still sons to be visited (i.e. p rest calls(p current)) ≠ []), then p current is set to the next son.

Polymorphic Infimum 4 (S POLY-2)

if POLY-INF
  & p status(p current) = expanded
  & ttag1 = S POLY  &  ttag2 = S POLY
  & p rest calls(p current) ≠ []

then

  p current := head(p rest calls(p current))
  p rest calls(p current) := tail(p rest calls(p current))

When p current points to a node with S POLY tagged arguments for the second or a later time and all sons have already been visited (i.e. p rest calls(p current)) = []), then all sub-computations for this node have been completed and the result is returned.

Polymorphic Infimum 5 (S POLY-3)

if POLY-INF
  & p status(p current) = expanded
  & ttag1 = S POLY  &  ttag2 = S POLY

  & p rest calls(p current) = []
  & subtype(1)    | subtype(2)     | NOT (is inhabited) | is inhabited

then

  p return(parg1) | p return(parg2)| make s bottom      | write poly term
                  |                | p return(ttop)     | p return(ttop)

The three new abbreviations in the last rule are given by

     subtype(i)  ≡ FOR ALL k = 1,. . .,sort arity(tref1) .
                          pargi + k = p result(nth(k,p sons(p current)))
     write poly term ≡ tval(ttop) := tval(parg1)
                       FOR ALL k = 1,. . .,sort arity(tref1) DO
                          tval(ttop + k) := tval(p result(nth(k,p sons(p current))))
                       ENDFORALL
                       ttop := ttop + sort arity(tref1) + 1
     is inhabited ≡ inst modus(tref1,[tb_{1},. . .,tb_{n}])

where in the last abbreviation n = sort arity(tref1), and for k = 1,...,n

         tb_{k} ≡ ttag(p result(nth(k,p sons(p current)))) ≠ S BOTTOM

The subtype conditions in the above rule represent an optimization analogously to the subsort optimization in the S MONO case (rule Polymorphic Infimum 2): only if the result differs from one of the two input arguments a new TYPEAREA location has to be returnd.

If p current points to a node with S REF tagged arguments for the first time (i.e. its status is expand), a single new son node labelled with the respective referenced type area locations is created.

Polymorphic Infimum 6 (S REF-1)

if POLY-INF
  & p status(p current) = expand
  & ttag1 = S REF  &  ttag2 = S REF

then

  p status(p current) := expanded

extend P NODE by temp

     where p arg1(temp) := tref1
            p arg2(temp) := tref2
            p father(temp) := p current
            p sons(p current) := [temp]
            p status(temp) := expand
            p current := temp

endextend

When p current points to a node with S REF tagged arguments for the second time (i.e. its status is expanded), then the sub-computations for its single son node has been completed and the result is returned.

Polymorphic Infimum 7 (S REF-2)

if POLY-INF
  & p status(p current) = expanded
  & ttag1 = S REF  &  ttag2 = S REF
  & LET res = p result(head(p sons(p current)))
  & res = tref1  | res = tref2    | ttag(res) = S BOTTOM | ttag(res) ≠ S BOTTOM

then

  p return(parg1) | p return(parg2) | p return(res)        | make s ref(res)
                  |                |                      | p return(ttop)

where for tl ∈ TYPEAREA the new abbreviation in the last rule is given by

         make s ref(tl) ≡ ttag(ttop) := S REF
                          tref(ttop) := tl
                          ttop := ttop+

POLYMORPHIC INFIMUM LEMMA: The polymorphic infimum rules given above are a correct realization of the poly infimum(l_{1},l_{2}) update of Section 6.5. Proof: We have to show that the polymorphic infimum rules represent a correct realization of the poly inf function on TYPETERM that is used in PROTOS-L (and which was introduced as an abtract function in Section 6.2). Taking the integrity constraints given for inf, sort glb, and poly inf in 6.1, 6.2, and 8.1 the proof follows by case analysis and induction on the sizes of typeterm(ref(l_{1})) and typeterm(ref(l_{2})). Note that the TRAILING CONDITION is also satisfied since in p return(tl) the location p return arg (which had been set to l_{2}) is trailed if its value is to be changed.

8.4 Propagation of polymorphic type restrictions

The still abtract update poly propagate(l_{1},l_{2}) is used in the Bind-3b rule of Section 6.5 and in the Get-Structure-2b rule of Section 6.6. We refine this update to the propagation of polymorphic type constraints as they occur in PROTOS-L.

Let us start with an example. Consider the polymorphic declaration for list(α) with constructors

         nil: → list(α)
         cons: α × list(α) → list(α)

and assume monomorphic types NAT and INTEGER with subsort(NAT,INTEGER) = true. Then solving the unification (or binding) constraint

         X≐ cons(Y,L)

in the presence of the type prefix

         {X : list(NAT), Y : INTEGER, L : list(INTEGER)}

generates the type constraint

         cons(Y,L) : list(NAT)

under the same type prefix. Thus, the update poly propagate(l_{1},l_{2}) would be called with

term(l_{2}) = cons(Y,L) and typeterm(ref(l_{1})) = list(NAT).

More generally, the arguments of the term referenced by l_{2} (in the example Y : INTEGER and L : list(INTEGER)) must be restricted to the respective argument domains of the top-level functor f of term(l_{2}) (here: cons) where each type variable in an argument domain in the declaration of f (here: cons: α × list(α) → list(α)) is replaced by the respective argument of typeterm(ref(l_{1})) (here: replacing α by NAT, which yields cons: NAT × list(NAT) →

list(NAT)).

This can be achieved in two steps: First, a new term f(X_{1},…,X_{m}) (in the example: cons(X_{1},X_{2})) is created with appropriately type-restricted new variables X_{i} (here: X_{1} : NAT and X_{2} : list(NAT)), and second, this new term is unified with term(l_{2}). Thus, in the example the type constraint cons(Y,L) : list(NAT) represented by poly propagate(l_{1},l_{2}) would be reduced to the unification problem

         cons(X_{1},X_{2})≐ cons(Y,L)

with type-constrained new variables X_{1} and X_{2}. (In fact, this is a slight simplification of the representation over the actual PAM implementation where the top-level functor (here: cons) would not be generated since it is not needed; instead, the binding of the n argument variables of the new term can be called directly.)

For the general refinement of the polymorphic porpagation we assume as an integrity condition

  solution({f(t_{1},. . .,t_{m}) : s(tt_{1},. . .,tt_{n})}) = solution({f(t_{1},. . .,t_{m})≐ f(X_{1},. . .,X_{m}),
                                                      X_{1} : subres(d_{1},subst), . . .,

                                                      X_{m}: subres(d_{m},subst)})

where the X_{i} are new variables, f has declaration f: d_{1} … d_{m} → s(α_{1},…,α_{n}) ∈ prog

and subst is the substitution (on type terms)

subst = ⋃_{k∈{1,...,n}} {α_{k} ≐ tt_{k}}

(c.f. [Bei90], [BMS91], [BM94]). Note that since s(tt_{1},…,tt_{n}) can not contain any type variables, also in subres(d_{j},subst) all type variables will have been replaced by ground type terms.

For the SYMBOLTABLE representation of the argument domains d_{j} in a function declaration of the form given above we assume a compiled form similar to the representation of type terms in CODEAREA used in 8.2. We assume that the compiler numbers the variables in s(α_{1},…,α_{n}) from left to right, and use the additional tag S VAR such that <S VAR,k> represents the k-th variable α_{k}. Thus, the de-compilation of type terms in 8.2 is extended by

         decompile type(L) = α_{k}  if head(L) = <S VAR,k>

The function

constr arg: SYMBOLTABLE × NAT → ((TTAG + {S VAR}) × (SORT + NAT))^{∗}

returns the argument domains d_{j} for a constructor. For instance, given the above list(α) declaration, we have

         constr arg(entry(cons,2),1) = [<S VAR,1>]
         constr arg(entry(cons,2),2) = [<S POLY,list>, <S VAR,1>]

More generally, for j ∈ {1,…,m} we impose the integrity constraint

         decompile type(constr arg(entry(f,n),j)) = d_{j}

For the refinement of poly propagate we add three new 0-ary functions to our initial PAM algebras: pp t ∈ DATAAREA, representing a reference to the term t to be retricted, pp tt ∈ TYPEAREA, a reference to the type term tt of the restriction, and pp i ∈ NAT, an index for the argument positions {1,…,m}. The update

         poly propagate(l_{1},l_{2}) ≡ pp t := l_{2}
                                   pp tt := ref(l_{1})
                                   pp i := 1
                                   h ← <STRUC,h+>
                                   val(h+) := ref(l_{2})
                                   h := h++
                                   ll what to do := polymorphic propagate

sets the three new 0-ary functions to their initial value, starts the generation of the new term by writing the top level functor on the heap, and blocks the applicability of all previous rules by updating ll what to do. The following three polymorphic propagation rules are guarded by the condition POLY-PROP and use the abbreviations hi (for the heap location of the i-th argument of the term to be generated) and pp f (for its top-level functor):

         POLY-PROP ≡ OK & ll what to do = polymorphic propagate
         hi  ≡ h + pp i - 1
         pp f  ≡ ref(pp t)

The first two propagation rules generate the argument variables X_{1},…,X_{m}. If there is still a variable to be generated (pp i ≤ arity(pp f)) and the (pp i)th argument domain in the declaration of pp f is not a type variable, then a variable with the respective type restriction is generated.

Polymorphic Propagation 1

if POLY-PROP
  & pp i ≤ arity(pp f)
  & head(constr arg(pp f,pp i)) =
       <S TOP, .>  |   <S MONO, s>     |   <S POLY, .>

then

  tag(hi) := FREE  | tag(hi) := FREE M | tag(hi) := FREE P
                   | ref(hi) := s      | insert poly(hi,
                   |                   |             constr arg(pp f,pp i),
                   |                   |             pp tt)
  pp i := pp i + 1

The update insert poly(l,L,tl) is derived from its 2-argument counterpart in 8.2 by additionally substituting the (representation of the) type variable α_{k} by the (representation of the) k-th argument of typeterm(tl):

  insert poly(l,L,tl) ≡ ref(l) := ttop
                        FORALL j = 1,. . .,length(L) DO
                          tval(ttop+j-1) := offset&substitute(ttop+j-1, nth(j,L), tl)
                        ENDFORALL
                        ttop := ttop + length(L)

where

     offset&substitute(tl', <tag,k>, tl) = \{ \begin{matrix}<tag, tl'+k> & if tag = S REF \\ tval(tl+k) & if tag = S VAR \\ <tag, k> & otherwise \end{matrix}

If there is still a variable to be generated (pp i ≤ arity(pp f)) and the (pp i)th argument domain in the declaration of pp f is a type variable (say, α_{k}), then the variable to be written on the heap must get the k-th type argument of typeterm(pp tt) as its type restriction (i.e. tref(pp tt + k)). If the latter is BOTTOM, backtrack update is executed since α_{k}: BOTTOM is an inconsistent type constraint (see 6.1).

Polymorphic Propagation 2

if POLY-PROP
  & pp i ≤ arity(pp f)
  & head(constr arg(pp f,pp i)) = <S VAR, k>
  & ttag(pp tt + k) =
      S TOP       | S MONO            | S POLY            | S BOTTOM

then

  tag(hi) := FREE | tag(hi) := FREE M | tag(hi) := FREE P | backtrack
                  |     ref(hi) := tref(pp tt + k)        |
  pp i := pp i + 1                                        |

The third propagation rule is applied when all argument variables have been written on the heap (pp i > arity(pp f)). It is responsible for the unification of the term to be restricted (pp t) with the newly generated term (referenced by h).

Polymorphic Propagation 3

if POLY-PROP
  & pp i > arity(pp f)

then

  h := h + arity(pp f)
  ll what to do := none
  propagate unify(h,pp t)

with the abbreviations

         propagate unify(l_{1},l_{2})  ≡ if still unifying
                                        then push on unify stack(l_{1},l_{2})
                                        else unify(l_{1},l_{2})
         still unifying  ≡ what to do = Bind & return from bind = Unify
         push on unify stack(l_{1},l_{2}) ≡ ref'(pdl++) := l_{1}
                                      ref'(pdl+) := l_{2}
                                      pdl := pdl++
                                      what to do := Unify

Thus, if the machine is still in unifying mode, the update propagate unify(l_{1},l_{2}) just pushes the two locations to be unified onto the push down list PDL used for unification; otherwise the update unify(l_{1},l_{2}) initializing unification is executed (see 3.2).

POLYMORPHIC PROPAGATION LEMMA: The polymorphic propagation rules given above are a correct realization of the poly propagate(l_{1},l_{2}) update of Section 6.5. Proof: By induction on the number of arguments in typeterm(l_{2}) we can show that, from the time when ll what to do is set to polymorphic propagate to the time when the rule Polymorphic Propagation 3 is being executed, a term of the form f(X_{1},…,X_{m}) is created on the heap. The rules Polymorphic Propagation 1 and 2 as well as the update insert poly(l,L,tt) ensure that the proper type restrictions for X_{i} are inserted, i.e. - using the notation of the solution integrity constraint given in the beginning of this subsection - X_{i}: subres(d_{i},subst). Note that if subres(d_{i},subst) = BOTTOM, rule Polymorphic Propagation 2 carries out the backtrack update

since solution({t : BOTTOM}) = nil for any term t.

Thus, we are left to show that also the equation part f(t_{1},…,t_{m}) ≐ f(X_{1},…,X_{m}) is taken properly into account. This exactly is ensured by the updates of rule Polymorphic Propagation 3: By induction on the number of times the unification of the two terms to be unified will again cause a polymorphic propagation invocation, and using the UNIFICATION LEMMA of Section 3.2, we can show that at the time when the unification initiated by the update propagate unify(h, pp t) has been carried out (either with success or with failure) the post-conditions of the POLYMORPHIC PROPAGATION CONDITION are satisfied.

8.5 Main Theorem of Part II

Putting everything together, we obtain

Correctness Theorem 3 (Main Theorem of Part II): Compilation from PROTOS-L algebras to the PAM algebras with polymorphic, order-sorted type constraint handling is correct.

References

[AK91] H. Aït-Kaci. Warren’s Abstract Machine: A Tutorial Reconstruction. MIT Press, Cambridge, MA, 1991.

[BB91] C. Beierle and E. Börger. A WAM extension for type-constraint logic programming: Specification and correctness proof. IWBS Report 200, IBM Germany, Scientific Center, Inst. for Knowledge Based Systems, Stuttgart, 1991.

[BB92] C. Beierle and E. Börger. Correctness proof for the WAM with types. In E. Börger, H. Kleine Büning, G. Jäger, and M. M. Richter, editors, Computer Science Logic - CSL’91. LNCS 626. Springer-Verlag, Berlin, 1992.

[BBM91] C. Beierle, S. Böttcher, and G. Meyer. Draft report of the logic programming language PROTOS-L. IWBS Report 175, IBM Germany, Stuttgart, 1991. Revised version: Working Paper 4, IBM Germany, Scientific Center, Institute for Logics and Linguistics, Heidelberg, July 1994.

[Bei90] C. Beierle. Types, modules and databases in the logic programming language PROTOS-L. In K. H. Bläsius, U. Hedtstück, and C.-R. Rollinger, editors, Sorts and Types for Artificial Intelligence. LNAI 418. Springer-Verlag, Berlin, 1990.

[Bei92] C. Beierle. Logic programming with typed unification and its realization on an abstract machine. IBM Journal of Research and Development, 36(3):375–390, May 1992.

[Bei94] C. Beierle. Formal design of an abstract machine for constraint logic programming. In B. Pehrson and I. Simon, editors, Technology and Foundations - Proceedings of the IFIP Congress 94, volume 1, pages 377–382. Elsevier / North Holland, Amsterdam, 1994.

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

[BMS91] C. Beierle, G. Meyer, and H. Semle. Extending the Warren Abstract Machine to polymorphic order-sorted resolution. In V. Saraswat and K. Ueda, editors, Logic Programming: Proceedings of the 1991 International Symposium, pages 272–286, Cambridge, MA, 1991. MIT Press.

[Bör90a] 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, CSL’89 - 3rd Workshop on Computer Science Logic. LNCS 440, pages 36–64. Springer-Verlag, Berlin, 1990.

[Bör90b] E. Börger. A logical operational semantics of full Prolog. Part II. Built-in predicates for database manipulations. In B. Rovan, editor, MFCS’90 - Mathematical Foundations of Computer Science. LNCS 452, pages 1–14, Berlin, 1990. Springer-Verlag.

[BR91] E. Börger and D. Rosenzweig. From Prolog algebras towards WAM - a mathematical study of implementation. In E. Börger, H. Kleine Büning, M. M. Richter, and W. Schönfeld, editors, Computer Science Logic. LNCS 533, pages 31–66. Springer-Verlag, Berlin, 1991.

[BR92a] E. Börger and D. Rosenzweig. The WAM - definition and compiler correctness. TR-14/92, Dipartimento di Informatica, Università di Pisa, 1992. (Revised version in: C. Beierle, L. Plümer (Eds.), Logic Programming: Formal Methods and Practical Applications, North-Holland, 1995).

[BR92b] E. Börger and D. Rosenzweig. WAM algebras - a mathematical study of implementation, Part II. In A. Voronkov, editor, Logic Programming. LNAI 592, pages 35–54, Berlin, 1992. Springer-Verlag.

[BS91] E. Börger and P. H. Schmitt. A formal operational semantics for languages of type Prolog III. In E. Börger, H. Kleine Büning, M. M. Richter, and W. Schönfeld, editors, Computer Science Logic. LNCS 533, pages 67–79. Springer-Verlag, Berlin, 1991.

[BS95] E. Börger and R. Salamone. CLAM specification for provably correct compilation of CLP(R) programs. In E. Börger, editor, Specification and Validation Methods, pages 97–130. Oxford University Press, 1995.

[Col90] A. Colmerauer. An introduction to Prolog-III. Communications of the ACM, 33(7):69– 906, July 1990.

[EM89] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2. EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1989.

[GM86] J. A. Goguen and J. Meseguer. Eqlog: Equality, types, and generic modules for logic programming. In D. DeGroot and G. Lindstrom, editors, Logic Programming, Functions, Relations, and Equations, pages 295–363. Prentice Hall, 1986.

[Gur88] Y. Gurevich. Logic and the challenge of computer science. In E. Börger, editor, Trends in Theoretical Computer Science, pages 1–57. Computer Science Press, 1988.

[Gur91] Y. Gurevich. Evolving algebras. A tutorial introduction. EATCS Bulletin, 43, February 1991.

[Han88] M. Hanus. Horn Clause Specifications with Polymorphic Types. PhD thesis, FB Informatik, Universität Dortmund, 1988.

[Han91] M. Hanus. Horn clause programs with polymorphic types: Semantics and resolution. Theoretical Computer Science, 89:63–106, 1991.

[JL87] J. Jaffar and J.-L. Lassez. Constraint logic programming. In Proceedings of the 14th ACM Symposium on Principles of Programming Languages, pages 111–119. ACM, January 1987.

[JMSY90] J. Jaffar, S. Michaylov, P. Stuckey, and R. Yap. The CLP(R) language and system. Technical Report RC 16292, IBM Research Devision, 1990.

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

[NM88] G. Nadathur and D. Miller. An overview of λProlog. In K. Bowen and R. Kowalski, editors, Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 810–827, Cambridge, MA, 1988. MIT Press.

[Rus92] D. M. Russinoff. A verified Prolog compiler for the Warren Abstract Machine. Journal of Logic Programming, 13:367–412, 1992.

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

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

[War83] D. H. D. Warren. An Abstract PROLOG Instruction Set. Technical Report 309, SRI, 1983.

A Transition rules for compiled And/Or structure

allocate

if OK
& code(p) = allocate

then

PUSH ENV temp IN
   cp'(temp) := cp
   vi'(temp) := vi
   ct'(temp) := ct
ENDPUSH
succeed

deallocate

                                        if OK
                                          & code(p) = deallocate

then

                                          POP ENV
                                          cp := cp'(e)
                                          succeed

call

if OK
& code(p) = call(G)
& is user defined(G)

then

let p1 = procdef(act,cs,prog)
if code(p1) = fail
then backtrack
else p := p1
     ct := b
     cp := p+

unify

                                        if OK
                                          & code(p) = unify(H)

then

                                          if solvable(cs ∪ {act≐ rename(H,vi)})
                                          then cs := cs ∪ {act≐ rename(H,vi)}
                                               vi := vi + 1
                                               succeed
                                          else backtrack

true/fail/cut

if OK
& code(p) = call(BIP)
& BIP =
   true | fail      | cut

then

succeed | backtrack | b := ct'(e)
        |           | succeed

add constraint

                                        if OK
                                          & code(p) = add constraint(P)

then

                                          if solvable(cs ∪ rename(P,vi))
                                          then cs := cs ∪ rename(P,vi)
                                               succeed
                                          else backtrack

try me else/try

if OK
& code(p) =
   try me else(N) | try(L)

then

PUSH STATE temp IN
   store state in(temp)
   p(temp) := N  | p(temp) := p+
   p:= p+        | p := L
ENDPUSH

trust me/trust

                                        if OK
                                          & code(p) =
                                             trust me | trust(L)

then

                                          fetch state from(b)
                                          POP STATE
                                          p:= p+      | p := L

retry me else/retry

if OK
  & code(p) =
     retry me else(N) | retry(L)

then

  fetch state from(b)
  p(b) := N          | p(b) := p+
  p:= p+             | p := L

proceed

                                          if OK
                                            & code(p) = proceed
                                            & code(cp)
                                               = proceed | ≠ proceed

then

                                            stop := 1    | p := cp

switch on structure

if OK
  & code(p) = switch on structure(i,T)

then

  let x_{i} = arg(act,i)
  p := select(T,func(x_{i}),arity(x_{i}))

switch on term

                                          if OK
                                            & code(p) = switch on term(i,Lv,Ls)
                                            & let x_{i} = arg(act,i)
                                              is var(x_{i}) | is struct(x_{i})

then

                                              p := Lv   | p := Ls

Abbreviations:

   succeed ≡ p := p + 1
   OK ≡ stop = 0

                                             backtrack ≡ if b = nil
                                                         then stop := -1
                                                         else p := p(b)

PUSH STATE temp IN updates ENDPUSH
  ≡ EXTEND STATE BY temp WITH

b := temp

       b(temp) := b
       temp- := tos(b,e)

updates

    ENDEXTEND

                                          PUSH ENV temp IN updates ENDPUSH
                                            ≡ EXTEND ENV BY temp WITH

e := temp

                                                 ce(temp) := e
                                                 temp- := tos(b,e)

updates

                                              ENDEXTEND

POP STATE ≡ b := b(b)                     POP ENV ≡ e := ce(e)

fetch state from(b) ≡ cs := cs(b)
                      cp := cp(b)
                      e  := e(b)

                                          store state in(temp) ≡ cs(temp) := cs
                                                                 cp(temp) := cp
                                                                 e(temp)  := e

B Transition rules for the PAM with abstract type terms of Part I

B.1 Low level unification

Unify-1 (success)

if OK & what to do = Unify
& pdl = nil

then

what to do := Run

Unify-2 (Unify-Var-Any)

if UNIF
& unbound(dl) | NOT(unbound(dl))
              | & unbound(dr))

then

bind(dl,dr) | bind(dr,dl)
pdl := pdl--

Unify-3 (Unify-Struc-Struc)

if UNIF
& NOT( unbound(dl) or unbound(dr) )
& val(ref(dl)) = val(ref(dr))

then

FORALL i = 1,...,arity(val(ref(dl))) DO
 ref'(pdl+2*arity(val(ref(dl)))-2*i) := ref(dl)+i
 ref'(pdl+2*arity(val(ref(dl)))-2*i-1) := ref(dr)+i
ENDFORALL
pdl := pdl+2*arity(val(ref(dl)))-2

Unify-4 (Unify-Struc-Struc)

if UNIF
& NOT( unbound(dl) or unbound(dr) )
& NOT( val(ref(dl)) = val(ref(dr)) )

then

backtrack
what to do := Run

Abbreviations:

dr ≡ deref(right)
dl ≡ deref(left)
UNIF ≡ OK & what to do = Unify
RUN ≡ OK & what to do = Run

B.2 Putting and Getting Code

The code for putting (resp. getting) instructions corresponding to a body goal (resp. the clause head) is defined using the term normal form of first order logic. Its two froms nf_{s} (resp. nf_{a}) correspond to the synthesis (resp. analysis) of terms:

nf(X_{i}=Y_{n}) = [X_{i}=Y_{n}]

                nf(Y_{i}=Y_{n}) = [ ]
     nf_{s}(X_{i}=f(s_{1},. . .,s_{m})) = flatten([nf_{s}(Z_{1}=s_{1}),. . .,nf_{s}(Z_{m}=s_{m}), X_{i}=f(Z_{1},. . .,Z_{m})])
     nf_{a}(X_{i}=f(s_{1},. . .,s_{m})) = flatten([X_{i}=f(Z_{1},. . .,Z_{m}), nf_{a}(Z_{1}=s_{1}),. . .,nf_{a}(Z_{m}=s_{m})])

The function put instr (resp. get instr) of a normalized equation is defined by the following table, where j stands for an arbitrary ‘top level’ index (corresponding to the input X_{i}=t for term normalization) and k for a ‘non top level’ index (corresponding to an auxiliary variable introduced by normalization itself):

              X_{j}=Y_{n} → [xxx value(y_{n},x_{j}]
              X_{k}=Y_{n} → [unify value(y_{n})]
     X_{i}=f(Z_{1},. . .,Z_{a}) → [xxx structure(entry(f,a),x_{i}), unify_{xxx} (z_{1}),. . .,unify_{xxx} (z_{a})]

where xxx stands for put (resp. get), y_{i} ∈ DATAAREA, x_{i} ∈ AREGS, and with

        unify_{xxx} (z_{i}) = \{ \begin{matrix}unify value(Y_{n}) & if Z_{i} = Y_{n} and xxx = put \\ unify value(X_{k}) & if Z_{i} = X_{k} and xxx = put \\ unify value(y_{n}) & if Z_{i} = Y_{n} and xxx = get \\ unify variable(X_{k}) & if Z_{i} = X_{k} and xxx = get \end{matrix}

The function put code (resp. get code) is defined by flattening the result of mapping put instr (resp. get instr) along nf_{a}(X_{i}=t) (resp. nf_{s}(X_{i}=t)). The function put seq (resp. get seq) specifies how a body goal (resp. clause head) of the form g(s_{1},…,s_{m}) is compiled:

    xxx seq(g(s_{1},. . .,s_{m})) = flatten([xxx code(X_{1}=s_{1}),. . .,xxx code(X_{m}=s_{m})])

with ‘top level’ j = 1,…,m.

Additionally, for the HEAP VARIABLES LEMMA and the proof of the “Pure PROTOS-L theorem” in 4 we assume that the put code and get code functions generate unify local value instead of unify value for all occurrences of local variables, and that

     call seq(g(s_{1},. . .,s_{k})) = flatten([put seq(g(s_{1},. . .,s_{k})),call(g,k,r)])

with {Y_{1},…,Y_{r}} being all variables occurring in the clause.

Additional compiler assumptions are given in Section 5 for the optimizations introduced there (environment trimming, LCO, variable initialization “on the fly”, etc.).

B.3 Putting of terms

put value

if RUN
& code(p) = put value(l,x_{j})

then

x_{j} ← l
succeed

Put-Unsafe-Value

if RUN
& code(p) = put unsafe value(y_{n},x_{j})
& deref(y_{n}) ≤ e  | deref(y_{n}) > e

then

x_{j} ← deref(y_{n})  | mk heap var(deref(y_{n}))
                 | x_{j} ← <REF,h>
succeed

put structure

                                         if RUN
                                           & code(p) = put structure(f,x_{i})

then

                                           h ← <STRUC,h+>
                                           x_{i} ← <STRUC,h+>
                                           val(h+) := f
                                           h := h++
                                           mode := write
                                           succeed

“On the fly” initialization (Sec. 5.2):

Put-1 (X variable)

if RUN
& code(p) = put variable(x_{i},x_{j},tt)

then

mk unbound(h,tt)
x_{i} ← <REF,h>
x_{j} ← <REF,h>
succeed

Put-2 (Y variable)

                                        if RUN
                                          & code(p) = put variable(y_{n},x_{j},tt)

then

                                          mk unbound(y_{n},tt)
                                          x_{j} ← <REF,y_{n}>
                                          succeed

B.4 Getting of terms

get value

if RUN
& code(p) = get value(l,x_{j})

then

unify(l,x_{j})
succeed

Get-Structure-1

if RUN
& code(p) = get structure(f,x_{i})
& tag(deref(x_{i})) = STRUC
& val(ref(deref(x_{i}))) = f  | val(ref(deref(x_{i}))) ≠ f

then

nextarg := ref(deref(x_{i}))+ | backtrack
mode := Read               |
succeed                    |

Get-Structure-2

if RUN
& code(p) = get structure(f,x_{i})
& unbound(deref(x_{i}))
& can propagate(f,ref(deref(x_{i})))
            = true                      | = false
& trivially propagates(f,ref(deref(x_{i}))) |
    = true    | = false                 |

then

h ← <STRUC,h+>                          | backtrack
bind(deref(x_{i}),h)                        |
val(h+) := f                            |
h := h++                                |
mode := Write | nextarg := h++          |
              | mk unbounds(h+,propagate list(f,ref(deref(x_{i}))) |
              | mode := Read            |
succeed                                 |

“On the fly” initialization (Sec. 5.2):

get variable

if RUN
& code(p) = get variable(l,x_{j},tt)

then

mk unbound(l,tt)
bind(l,x_{j})
succeed

B.5 Unify instructions

Unify Variable

if RUN
& code(p) = unify variable(l)
& mode = Read      | mode = Write

then

mk unbound(l)      | mk unbound(h)
bind(l,nextarg)    | l ← <REF,h>
nextarg := nextarg+| h := h+
succeed

Unify Value

if RUN
& code(p) = unify value(l)
& mode = Read      | mode = Write

then

unify(l,nextarg)   | h ← l
nextarg := nextarg+| h := h+
succeed

Unify Local Value

if RUN
& code(p) = unify local value(l)
& mode = Read      | mode = Write
            | & NOT(local(deref(l))) | local(deref(l))

then

unify(l,nextarg)   | h ← deref(l)          | mk heap var(deref(l))
nextarg := nextarg+| h := h+                |
succeed

“On the fly” initialization (Sec. 5.2):

unify variable

if RUN
& code(p) = unify variable(l,tt)
& mode = Read      | mode = Write

then

mk unbound(l,tt)   | mk unbound(h,tt)
bind(l,nextarg)    | l ← <REF,h>
nextarg := nextarg+| h := h+
succeed

B.6 Environment and Choicepoint Representation

The entries of the environment frame are stored in STACK at fixed offsets from the environment pointer e (ignoring cut points at this stage, but see 5.3). In particular, the environment also contains the variables y_{1},…,y_{n} where n is the second parameter of the last call being executed (which is accessible via cp-):

ce(l)  ≡ l + 1
cp'(l)  ≡ l + 2
y_{i}  ≡ e + 2 + i      ( 1 ≤ i ≤ stack offset(cp) )
y_{i}(l)  ≡ l + 2 + i      ( 1 ≤ i ≤ stack offset(val(cp'(l))) )
stack offset(l) ≡ n  if code(l-) = call(g,a,n)
tos(b,e)  ≡ if b ≤ e
                     then e + 2 + stack offset(cp)
                     else b

Similarly, the choicepoint information is stored in STACK at fixed offsets from the backtracking pointer b. The choicpoint also contains the argument registers x_{1},…,x_{i} of the current goal:

h(l) ≡ l
tr(l) ≡ l - 1
p(l) ≡ l - 2
b(l) ≡ l - 3
cp(l) ≡ l - 4
e(l) ≡ l - 5
x_{i}  ≡ l - 5 - i
hb(l) ≡ val(h(b))

B.7 Indexing and Switching

try me else/try

if RUN
& code(p) =
   try me else(N,n)|try(L,n)

then

LET new b = tos(b,e) + n + 6
b := new b
val(b(new b)) := b
store state in(new b,n)
val(p(new b)) := N |val(p(new b)):=p+
p:= p+             |p := L

trust me else/trust

if RUN
& code(p) =
   trust me(n) | trust(L,n)

then

fetch state from(b,n)
b := val(b(b))
p:= p+         | p := L

retry me else/retry

                                        if RUN
                                          & code(p) =
                                             retry me else(N,n) | retry(L,n)

then

                                          fetch state from(b,n)
                                          val(p(b)) := N       | val(p(b)) := p+
                                          p:= p+               | p := L

switch on term

                                        if RUN
                                          & code(p) = switch on term(i,Lv,Ls)
                                          & tag(deref(x_{i})) =
                                               VAR   |    = STRUC

then

                                            p := Lv  | p := Ls

switch on structure

                                        if RUN
                                          & code(p) = switch on structure(i,T)

then

                                          p := select(T,val(ref(deref(x_{i}))))

Abbreviations:

store state in(t,n) ≡ FORALL i = 1,. . .,n
                     val(x_{i}(t) := x_{i}
                   ENDFORALL
                   val(e(t)) := e
                   val(cp(t)) := cp
                   val(tr(t)) := tr
                   val(h(t)) := h

                                        fetch state from(t,n) ≡ FORALL i = 1,. . .,n
                                                                 x_{i} := val(x_{i}(t))
                                                               ENDFORALL
                                                               e  := val(e(t))
                                                               cp := val(cp(t))
                                                               tr := val(tr(t))
                                                               h  := val(h(t))