Rewrite programs are logic programs represented as rewrite rules, whose execution mechanism usually employs some version of Knuth-Bendix type completion. Rewrite programs allow one to express mutually exclusively defined predicates as well as those which are not. In this paper we demonstrate that rewrite programs, although denotationally equivalent to Prolog on the ground level, may produce fewer answers in general. Consequently, a rewrite program may halt with finitely many answers while the corresponding Prolog program goes into an infinite loop. In order to explain these observations, we present a precise operational semantics for rewrite programs, define their denotational (fixpoint) semantics, prove the equivalence of operational, model theoretic and denotational semantics, and clarify the relationship between rewrite programs and Prolog. Comparisons between the pruning effects of simplification and those of subsumption based loop checking mechanisms for Prolog are also included.
On rewrite programs: semantics and relationship with Prolog
BONACINA, Maria Paola
;
1992-01-01
Abstract
Rewrite programs are logic programs represented as rewrite rules, whose execution mechanism usually employs some version of Knuth-Bendix type completion. Rewrite programs allow one to express mutually exclusively defined predicates as well as those which are not. In this paper we demonstrate that rewrite programs, although denotationally equivalent to Prolog on the ground level, may produce fewer answers in general. Consequently, a rewrite program may halt with finitely many answers while the corresponding Prolog program goes into an infinite loop. In order to explain these observations, we present a precise operational semantics for rewrite programs, define their denotational (fixpoint) semantics, prove the equivalence of operational, model theoretic and denotational semantics, and clarify the relationship between rewrite programs and Prolog. Comparisons between the pruning effects of simplification and those of subsumption based loop checking mechanisms for Prolog are also included.File | Dimensione | Formato | |
---|---|---|---|
JLP1992rewprograms.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
374.19 kB
Formato
Adobe PDF
|
374.19 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.