Comparative semantics for prolog with cut
type: Item
instance of: scholarly article
title: Comparative semantics for prolog with cut
zbMATH Open document ID: 0708.68034
DOI: 10.1016/0167-6423(90)90072-L
author: Erik de Vink
published in: Science of Computer Programming
publication date: 1990-01-01T00:00:00Z
review text: 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 substitut…
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68N17
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 4164146
zbMATH Keywords: metric domain
zbMATH Keywords: denotational semantics
zbMATH Keywords: Prolog
zbMATH Keywords: Cut
zbMATH Keywords: flow-of-control
zbMATH Keywords: operational semantics
zbMATH Keywords: equivalence
reviewed by: Peter van Emde Boas
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 4164146