On the equivalence of deferred substitution and immediate substitution semantics for Logic Programs

Abstract

The paper considers a deferred substitution semantics for Logic Programs, in which both the composition of computed substitutions and their application to atoms in the current goal are deferred. This kind of semantics occurs in several interpreter optimization contexts:

• Prolog implementation optimization.

• Concurrent Logic Programs with committed choice.

• Distributed Logic Programs.

However, in none of the specific applications of this kind of optimization, was any theoretical justification given, by formally relating this optimization to the standard operational semantics, based on SLD-resolution.

In this paper we prove the equivalence of these two kinds of semantics for a natural class of selection rules, including the standard leftmost selection rule applied by Prolog interpreters. Thus, we provide the missing justification of this known optimization.

The paper considers also in more detail the implications of this semantics to Distributed Logic Programs, which seems to be a new application. For the sequential case, an abstract implementation via meta-interpretation is described.