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.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
H. Aït-Kaci. Warren's Abstract Machine: A Tutorial Reconstruction. MIT Press, Cambridge, MA, 1991.
C. Beierle. Types, modules and databases in the logic programming language PROTOSL. In K. H. Bläsius, U. Hedtstück, and C.-R. Rollinger, editors, Sorts and Types for Artificial Intelligence. LNAI 418, Springer-Verlag, Berlin, Heidelberg, New York, 1990.
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.
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 Programing: Proceedings of the 1991 International Symposium, pages 272–286, MIT Press, Cambridge, MA, 1991.
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, Heidelberg, New York, 1990.
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, Springer-Verlag, Berlin, Heidelberg, New York, 1990.
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, Heidelberg, New York, 1991.
E. Börger and D. Rosenzweig. WAM algebras-a mathematical study of implementation, Part II. In Russian Conference on Logic Programming '91. LNCS, Springer-Verlag, 1992. (to appear). Preliminary version in: Technical Report CSE-TR-88-91, The University of Michigan, Department of Electrical Engineering and Computer Science, Ann Arbor, Michigan.
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, Heidelberg, New York, 1991.
Y. Gurevich. Evolving algebras. A tutorial introduction. EATCS Bulletin, 43, February 1991.
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.
D. M. Russinoff. A Verified Prolog Compiler for the Warren Abstract Machine. Technical Report ACT-ST-292-89, MCC, Austin, Texas, 1989. (To appear in Journal of Logic Programming).
H. Semle. Extension of an Abstract Machine for Order-Sorted Prolog to Polymorphism. Diplomarbeit Nr. 583, Universität Stuttgart und IBM Deutschland GmbH, Stuttgart, April 1989. (in German).
G. Smolka. Logic Programming over Polymorphically Order-Sorted Types. PhD thesis, FB Informatik, Univ. Kaiserslautern, 1989.
G. Smolka. TEL (Version 0.9), Report and User Manual SEKI-Report SR 87-17, FB Informatik, Universität Kaiserslautern, 1988.
D. Warren. An Abstract PROLOG Instruction Set. Technical Report 309, SRI, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beierle, C., Börger, E. (1992). Correctness proof for the WAM with types. In: Börger, E., Jäger, G., Kleine Büning, H., Richter, M.M. (eds) Computer Science Logic. CSL 1991. Lecture Notes in Computer Science, vol 626. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023755
Download citation
DOI: https://doi.org/10.1007/BFb0023755
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55789-0
Online ISBN: 978-3-540-47285-8
eBook Packages: Springer Book Archive