Is there an axiomatic semantics for standard pure Prolog? (Q805224): Difference between revisions

A well known problem with the semantics of pure prolog programs arises from the differences between the intended declarative meaning and the operational semantics which results from the use of a particular selection rule in the process of SLD resolution. Differences which would not arise if all SLD resolution trees would be finite. The infinite computations, however, create a gap between the succeeding SLD trees and the finitely failed ones. Several authors have attempted to present axiomatic descriptions for the semantics of pure prolog by the way of syntactic transformations of the input program. The syntactic translation strengthens the meaning in such a way that the intended least Herbrand model of the input program becomes the unique model of the transformed program without having to invoke higher order principles. Again these translations in general work only for clean evaluation strategies (fair use of a breath first strategy). This leaves open the problem of defining transformations which capture the operational semantics for the case that real life SLD trees are used, since these are generated by an unfair depth-first search method. The author presents a pair of alternative semantics for pure prolog programs: the finite standard semantics, which is independent of clause ordering and the finite invariant operational semantics which is independent both of ordering of clauses and subgoals within a clause. These two semantics are subsequently axiomalized by a syntactic transformation of the input program. These axiomatics are subfrequently shown to be complete for the corresponding semantics.