A logical operational semantics of full prolog: Part I. selection core and control

Abstract

Y. Gurevich recently proposed a framework for semantics of programming concepts which directly reflects the dynamic and resource-bounded aspects of computation. This approach is based on (essentially first-order) structures that evolve over time and are finite in the same way as real computers are (so-called “dynamic algebras”). We use dynamic algebras to give an operational semantics for Prolog which, far from being hopelessly complicated or too machine-dependent, is both simple and abstract and supports the process oriented understanding of programs by programmers. In spite of its abstractness, our semantics can easily be made machine executable. It is designed for extensibility. We give this semantics for the full language of Prolog including all the usual non-logical built-in predicates for arithmetic, input/output and manipulation of terms, files and databases. We hope to contribute in this way to reducing the “mismatch between theory and practice… that much of the theory of logic programming only applies to pure subsets of Prolog, whereas the extra-logical facilities of the language appear essential for it to be practical” (Lloyd 1989). Our specific aim is to provide a mathematically precise but simple framework in which standards can be defined rigorously and in which different implementations may be compared and judged. Part I' deals with the core of Prolog which governs the selection mechanism of clauses for goal satisfaction including backtracking and cut and closely related built-in control predicates including call. In parts II and III the remaining classes of built-in predicates are treated. As a result of the inherent extensibility of dynamic algebra semantics, we are able to proceed by stepwise refinement.