slightly modified version appeared in: Formal Aspects of Computing, Vol. 8(5), pp. 539–564, 1996

Refinement of a typed WAM extension by polymorphic order-sorted types^{∗}

Christoph Beierle^{1} and Egon Börger^{2}

1Fachbereich Informatik, FernUniversität Hagen, D-58084 Hagen, Germany; ^{2}Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56100 Pisa, Italia

Keywords: Constraint logic programming, WAM, types, polymorphism, ordersorted types, correctness proof, evolving algebras

Abstract. We refine the mathematical specification of a WAM extension to typeconstraint logic programming given in [BB96]. We provide a full specification and correctness proof of the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L, by refining the abstract type constraints used in [BB96] to the polymorphic order-sorted types of PROTOS-L. This allows us to develop a detailed and 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.

1. Introduction

In [BR95] a mathematical elaboration of Warren’s Abstract Machine ([War83], [AK91]) for executing Prolog is given, coming in several refinement levels together with correctness proofs, and a correctness proof w.r.t. Börger’s phenomenological Prolog description [Bör90]. In [BB96] we demonstrated how the evolving algebra approach naturally allows for modifications and extensions in the description of both the semantics of programming languages as well as of implementation methods. Extending Börger and Rosenzweig’s WAM description, [BB96] provides a mathematical specification of a WAM extension to type-constraint logic programming and proves its correctness.

Address for correspondence: Christoph Beierle, Fachbereich Informatik, LG Praktische Informatik VIII, FernUniversität Hagen, Bahnhofstr. 48, D-58084 Hagen, Germany; e-mail:

christoph.beierle@fernuni-hagen.de ∗ 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.

The reason that types are dealt with at the abstract machine level is that the extension of logic programming by types requires in general not only static type checking, but types may also be present at run time (see e.g. [MO84], [Han91], [Smo89]). In the presence of types and subtypes, restricting a variable to a subtype represents a constraint in the spirit of constraint logic programming. PROTOS-L [Bei92], 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 [BM94] that is an extension of the WAM by the required polymorphic ordersorted unification. Our aim is to provide here a full specification and correctness proof of the PAM, including extra-logical features and all WAM optimizations (like environment trimming and last call optimization), as well as PAM specific optimizations (like refined variable representation or switch on typed variables).

In [BB96] the notion of type constraints was deliberately kept abstract, in order to be applicable to a range of constraint formalisms such as Prolog III or CLP(R). Consequently, also on the abstract machine level, the type contraint solving parts had to be kept abstract. In this paper we refine these abstract type constraints to the polymorphic order-sorted types of PROTOS-L. We do this again in several refinement steps. This allows us to develop a detailed and mathematically precise account of the PAM’s compiled type constraint representation and solving facilities, and to prove its correctness w.r.t. PROTOS-L.

Section 2 introduces the representation and constraint solving of monomorphic, order-sorted type constraints. Section 3 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 4 gives a detailed account of polymorphic type constraint representation and solving in the PAM. Since this paper is a direct sequel to [BB96], we assume the reader to be familiar with it and refer to it for unexplained definitions and notations and for further references to the literature.

2. PAM algebras with monomorphic type constraints

2.1. Binding

We start with 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 we define

    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.

if OK

Bind-1 (Bind-Direction)

  & 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.

if BIND

Bind-2 (Bind-Var-Var)

  & 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

if BIND

Bind-3 (Bind-Var-Struc)

  & 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 in [BB96], 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).

2.2. Monomorphic, order-sorted types

Before introducing a representation for type terms we introduce some new functions and universes that are related to TYPETERM. Until now we have kept TYPETERM abstract; in this section we come to some more specific type term characteristics such as monomorphic and polymorphic type terms. Going by stepwise refinement, 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 TYPETERM we introduce the three functions

    is top, is monomorphic, 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 [Bei92]). 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 2.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.

2.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 4):

    (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 in [BB96] by replacing the universe TYPETERM by its representing universe TYPEAREA. The codomain of the ref function (from 3.1 in [BB96]) now contains TYPEAREA, and in the integrity constraints of 3.1 in [BB96] 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)

2.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 in [BB96]) (Its

use in the multiple mk unbounds update in get structure will be refined in Section 2.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.^{1}

Similarly, the insertion of polymorphic type terms by insert poly(l,tt) will be handled in Section 4. 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 in [BB96].

Proof. By straightforward case analysis for TOP, monomorphic and polymorphic type restrictions; for the latter the POLYMORPHIC TYPE INSERTION CON-DITION is used.

2.5. Binding of type constrained variables

We refine the binding rules of Section 2.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:

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

then

  trail(arg1)
  arg1 ← <REF,arg2>
  bind success     | occur check(arg1,arg2)
if BIND
  & monomorphic(arg1) OR polymorphic(arg1)
  & top(arg2)

then

will not elaborate this topic in this paper.

Bind-2a (Bind-TOP-Any)

Bind-2b (Bind-Var-TOP)

1 Note 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

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

Bind-2c (Bind-Mono-Mono)

& 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                             |
if BIND

Bind-2d (Bind-Poly-Poly)

& polymorphic(arg1)
& polymorphic(arg2)

then

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

For the still abstract update poly infimum(l_{1},l_{2}) used when binding two polymorphically restricted variables 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 2.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

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-3a (Bind-Mono-Struc)

if BIND

Bind-3b (Bind-Poly-Struc)

  & 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 PROPAGATION CONDITION of 2.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 correctly realize the binding rules of Section 2.1 and thus the binding update of 3.2 in [BB96].

Proof. Following the proof of the BINDING LEMMA in 2.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 in [BB96]). For the monomorphic case we conclude from the last integrity constraint given in Section 2.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 CONDI-TIONS are used.

2.6. Getting of structures

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

if RUN

Get-Structure-2a

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

then

  backtrack
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}))) |

Get-Structure-2b

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 in [BB96], 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 in [BB96] 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 in [BB96] are propagated onto the arguments of the structure.

Whereas we have now 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 Sec-

tion 4.

3. PAM Optimizations

3.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 [BM94]. 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 in [BB96]) 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 in [BB96] 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{cases}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{cases}

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 2.6).

Similarly, the rules for initializing variables (Section 5.2 in [BB96]) 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 polymor-

phic(tt) holds. Likewise, 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.

if RUN

Put-1 (X variable)

& 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
if RUN

Put-2 (Y variable)

&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
if RUN

Get (Variable)

& 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
if RUN

Unify (Read Mode)

& 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
if RUN

Unify (Write Mode)

& 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 2.

Proof. The only type inserting update of 2.4 that is still used is insert poly for which the POLYMORPHIC TYPE INSERTION CONDITION ensures the TYPE INSERTION CONDITION. Inserting TOP and monomorphic type restrictions for variables obviously has the same effect as in 2.4. Trailing still works fine since in 4.2 in [BB96] we trailed the complete val decoration of a data area location - including its tag - and restored it upon backtracking. With these two observations the proof follows by case analysis for the three different kinds of type restrictions. Showing that each variable is initialized properly is straightforward; the correct treatment of the 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).

3.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 in [BB96]) which increases the determinacy detection abilities. Since only monomorphic types can have explicitly defined subtypes there are two switch-on-term instructions. (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, leading to additional parameters in the following instructions.)

if RUN

Switch-on-poly-term

  & 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. Appendix B.7 in [BB96]) 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 [Bei92].

if RUN

Switch-on-mono-term

  & 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:

if RUN

Switch-on-sort

  & 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.

For the correctness proof for the extended switching instructions we must extend the assumptions on the compiler stated in 2.2 in [BB96]. The defintion of chain is changed so that the two cases for switch on term are replaced by

chain(Ptr) =

      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})

…

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.

The special representation of typed variables introduced in this section yield that the type extension in the PAM is 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 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.

4. Polymorphic type constraint solving

In this section polymorphic type constraint handling is refined by re-

fining the three updates insert poly(l,tt), poly infimum(l_{1},l_{2}), and

poly propagate(l_{1},l_{2}) that have been left abstract so far.

4.1. Representation of polymorphic type terms

For the representation of polymorphic type terms we introduce the function

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 in [BB96]) 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

We illustrate these integrity constraints by an example. 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    arity(entry(succ,1))   =1
target sort(entry(cons,2))   =list   arity(entry(cons,2))   =2
target sort(entry(mk pair,2))=pair   arity(entry(mk pair,2))=2
sort arity(nat)  = 0      is monomorphic(nat)           = true
sort arity(list) = 1      is polymorphic(list(list(γ))) = true
sort arity(pair) = 2

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 2.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}

4.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 3) is replaced by

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

For simplicity this list representation abstracts 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) =

     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)). . .))

For any type term tt ∈ TYPETERM we impose the integrity constraint

    decompile type(compile type(tt)) = tt

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 2.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 2.4, i.e. the POLYMORPHIC TYPE INSER-TION 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.

4.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 2.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

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

where X ∈ VARIABLE. Thus, from the conditions on the solution func-

tion in 2.1 we have e.g. inhabited(BOTTOM) = false, inhabited(TOP) =
true, 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 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 for i = 1, 2:

    pargi ≡ p argi(p current)
    ttagi ≡ ttag(pargi)
    trefi ≡ tref(pargi)

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.

if POLY-INF

Polymorphic Infimum 1 (S TOP, S BOTTOM)

  & 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.

if POLY-INF

Polymorphic Infimum 2 (S MONO)

  & p status(p current) = expand
  & ttag1 = S MONO  &  ttag2 = S MONO
  & subsort(tref1,|subsort(tref2,|sort glb(tref1,|sort glb(tref1,
            tref2)|        tref1) |         tref2)|         tref2)

                  |               |  = 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.

if POLY-INF

Polymorphic Infimum 3 (S POLY-1)

  & 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.
if POLY-INF

Polymorphic Infimum 4 (S POLY-2)

  & 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.

if POLY-INF

Polymorphic Infimum 5 (S POLY-3)

  & 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.

if POLY-INF

Polymorphic Infimum 6 (S REF-1)

  & 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.

if POLY-INF

Polymorphic Infimum 7 (S REF-2)

  & 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) = | ttag(res) ≠
                  |                |     S BOTTOM |     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 2.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 2.2). Taking the integrity constraints given for inf, sort glb, and poly inf in 2.1, 2.2, and 4.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 CON-

DITION 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.

4.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 2.5 and in the Get-Structure-2b rule of Section 2.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. [Bei92], [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 4.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 4.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.

if POLY-PROP

Polymorphic Propagation 1

  & 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 4.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&subst(ttop+j-1, nth(j,L), tl)
          ENDFORALL
          ttop := ttop + length(L)

where

     offset&subst(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 2.1).

if POLY-PROP

Polymorphic Propagation 2

  & 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).

if POLY-PROP

Polymorphic Propagation 3

  & 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 in [BB96]).

POLYMORPHIC PROPAGATION LEMMA: The polymorphic propagation rules given above are a correct realization of the poly propagate(l_{1},l_{2}) update of Section 2.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 in [BB96], 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.

4.5. Main Theorem

Putting everything together, we obtain

Correctness Theorem 3: 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.

[BB96] C. Beierle and E. Börger. Specification and correctness proof of a WAM extension with abstract type constraints. Formal Aspects of Computing, 8(4), 1996.

[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.

[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.

[Bör90] E. Börger. A logical operational semantics of full Prolog. Part I. Selection core and control. CSL’89 - 3rd Workshop on Computer Science Logic. LNCS 440, pages 36–64. Springer-Verlag, Berlin, 1990.

[BR95] E. Börger and D. Rosenzweig. The WAM – definition and compiler correctness. In C. Beierle and L. Plümer, editors, Logic Programming: Formal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence, chapter 2, pages 20–90. Elsevier Science B.V./North-Holland, Amsterdam, 1995.

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

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

[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.