ORACLE SEMANTICS FOR PROLOG

This paper proposes to specify semantic definitions for logic programm ing languages such as Prolog in terms of an oracle which specifies the control strategy and identifies which clauses are to be applied to re solve a given goal. The approach is quite general. It can be applied t o Prolog to specify both operational and declarative semantics as well as other logic programming languages. Previous semantic definitions f or Prolog typically encode the sequential depth-first search of the la nguage into various mathematical frameworks, Such semantics mimic a Pr olog interpreter in the sense that following the ''leftmost'' infinite path in the computation tree excludes computation to the right of thi s 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 g iven 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 conci se semantic definitions which are more useful for arguing the correctn ess of program transformations and providing the basis for abstract in terpretations than previous proposals. (C) 1995 Academic Press, Inc.