Comparative semantics for prolog with cut (Q920622)

The paper describes an operational and a denotational semantics for Prolog with Cut, and presents a proof of their equivalence. In achieving this goal the paper is not the first to do so, but the improvements over its predecessors are numerous. Earlier authors either had to provide a far more complicated semantics and equivalence proof, or failed to formally prove the equivalence at all. Clarity is achieved by factoring out the problem in two steps. Step one deals with the flow-of-control aspects of Prolog. A special purpose abstract language B is introduced which represents the control of Prolog while disregarding the Horn-clause logic aspects. The operational semantics of this language B is described using a Plotkin style transition system. A denotational semantics is based on least fixed point solutions of semantic equations over a metric domain of streams. As such these two semantics are still inappropriate for proving their equivalence. The discrepancy has to do with the cut operator which was rather easy to express in terms of the transition system but which required a visible marker in the denotational semantics in order to make the latter semantics compositional. In order to bridge this gap the author introduces an intermediate semantics, where a corresponding cut- marker is introduced in the transition system. The connection between the new and the earlier transition system consists of the hiding of the cut marker in the generated set of traces. On the other hand the new operational semantics can be shown to be equivalent with the denotational one by establishing the termwise equivalence between two sequences of approximations, each converging in the limit to the relevant semantics. This equivalence proof forms the main body of the paper - by the end of this proof the reader has consumed about 80\% of the text. In the last section the two semantics are refined in order to deal with the logic part of Prolog. By specialising states to become sets of substitutions and by letting the atomic actions be represented by calculating the required most general unifications the abstract semantics turns into a semantics for Prolog, the impact of the cut operator having been dealt with in the previous part. Still the question of full abstractness of the semantics remains as an open problem - the involvement of the cut marker prohibits the semantics from being fully abstract.