In this paper a new approach to divergence in Knuth-Bendix completion is presented. Given a term rewriting system R, whose completion diverges, a strategy can be defined to simulate the application of the (infinite) rewrite rules derived from critical pairs, without attempting any completion. This is done by applying some of the rules in R also as expansion rules.
On dealing with divergent rewrite systems
1992
Abstract
In this paper a new approach to divergence in Knuth-Bendix completion is presented. Given a term rewriting system R, whose completion diverges, a strategy can be defined to simulate the application of the (infinite) rewrite rules derived from critical pairs, without attempting any completion. This is done by applying some of the rules in R also as expansion rules.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_453775-doc_174519.pdf
accesso aperto
Descrizione: On dealing with divergent rewrite systems
Dimensione
986.23 kB
Formato
Adobe PDF
|
986.23 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
