Correctness proof for the WAM with types

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. In this 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. Starting from type-constraint Prolog algebras that are derived from Börger’s standard Prolog algebras, the specification of the type-constraint WAM extension is given by a sequence of evolving algebras, each representing a refinement level. 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 and for every compiler satisfying the specified conditions, the WAM extension with an abstract notion of types is correct w.r.t. L. This is a first step towards our aim 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.