Summary: 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 interpreted 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.
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.
For the entire collection see [Zbl 0768.00012].