Oracle Semantics for Prolog

This paper proposes to specify semantic definitions for Prolog in terms of an oracle which provides information on which clauses are to be applied to resolve a given goal. The approach is quite general. It is applicable to pure Prolog to define both operational and declarative semantics; and can be viewed as a basis for both sequential and parallel implementations. Previous semantic definitions for Prolog typically attempt to encode the sequential depth-first search of the language into various mathematical frameworks. A clause is applied in such semantics only if it is chosen under the search strategy. We prefer instead to specify in a more declarative way the condition upon which a clause is to be applied. The decision whether or not to apply a clause may be viewed as a query to an oracle which may be specified from within the semantics or 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.