Oracle Semantics for Prolog
By: R. Barbuti, M. Codish, R. Giacobazzi and M. Maher
Roberto
Giacobazzi
Dip. di Informatica
Univ. di Pisa
Corso
Italia 40, 56125 Pisa
(Italy)
giaco@di.unipi.it
Abstract:
This paper proposes to
specify semantic definitions for logic programming languages such as
Prolog in terms of an oracle which specifies the control strategy and
identifies which clauses are to be applied to resolve a given
goal. The approach is quite general. It is applicable to Prolog to
specify both operational and declarative semantics as well as other
logic programming languages. Previous semantic definitions for Prolog
typically encode the sequential depth-first search of the language
into various mathematical frameworks. Such semantics mimic a Prolog
interpreter in the sense that following the ``leftmost'' infinite path
in the computation tree excludes computation to the right of this path
from being considered by the semantics. The basic idea in this paper
is to abstract away from the sequential control of Prolog and to
provide a declarative characterization of the clauses to apply to a
given goal. The decision whether or not to apply a clause is viewed
as a query to an oracle which is specified from within the semantics
and reasoned about from outside. This approach results in simple and
concise semantic definitions which are more useful for arguing the
correctness of program transformations and providing the basis for
abstract interpretations than previous proposals.
Available:
DVI,
PostScript,
BibTeX Entry.
giaco@di.unipi.it