Operational and denotational semantics of rewrite programs

In this paper we present a new operational and denotational semantics for rewrite systems as logic programs. The main feature of our rewrite programs is that they allow us to define predicates not only by implications as in Prolog, but also by equivalences. We give a few examples showing how rewrite programs may turn out to be more effective than Prolog programs in capturing the user's intended semantics, because of this additional feature. Rewrite programs are interpreted by linear completion. Our definition of linear completion differs from the previous ones, because we allow simplification of goals by their ancestors. If simplification is allowed, programs given by equivalences and programs given by implications show a different behaviour. In the second part of the paper we give a fixpoint characterization of rewrite programs and we show that it captures both the proof theoretic and the model theoretic semantics. Rewrite programs and Prolog programs for the same predicates have the same fixpoint, i.e. the same set of ground true facts, although a rewrite program may give fewer answers. We show that this happens because if predicates are defined by equivalences, distinct Prolog answers turn out to be equivalent with respect to the rewrite program. However, for every Prolog answer there is an equivalent answer given by the rewrite program. This explains why a smaller set of answers covers the same set of ground true facts.