A Logical Operational Semantics of Full Prolog: Part III. Built-In Predicates for Files, Terms, Arithmetic and Input-Output

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, unnatural or machine-dependent, is simple, natural and abstract and in particular supports the process oriented understanding of programs by programmers. In spite of its abstractness, our semantics is machine executable. It is designed for extensibility and as a result of the inherent extensibility of dynamic algebra semantics, we are able to proceed by stepwise refinement.

We give this semantics for the full language of Prolog including all the usual non-logical built-in predicates. We hope to contribute in this way to reducing the “mismatch between theory and practice… that much of the theory of logic programming only apply 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 logical framework in which standards can be defined rigorously and in which different implementations may be compared and judged. This work is in applied logic and suggests several interesting new classes of problems in model theory.

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. In Part II the database built-in predicates are treated. In the present Part III we deal with the remaining built-in predicates for manipulation of files, terms, input/output and arithmetic.