One of the key results in the field of modularity for Term Rewriting Systems is the modularity of completeness for left-linear TRSs established by Toyama, Klop and Barendregt in [TKB89]. The proof, however, is quite long and involved. In this paper, a new proof of this basic result is given which is both short and easy, employing the powerful technique of "pile and delete" already used with success in proving the modularity of UN->. Moreover, the same proof is shown to extend the result in [TKB89] proving modularity of termination for left-linear and consistent with respect to reduction TRSs.

Modularity of Completeness Revisited

MARCHIORI, MASSIMO
1995

Abstract

One of the key results in the field of modularity for Term Rewriting Systems is the modularity of completeness for left-linear TRSs established by Toyama, Klop and Barendregt in [TKB89]. The proof, however, is quite long and involved. In this paper, a new proof of this basic result is given which is both short and easy, employing the powerful technique of "pile and delete" already used with success in proving the modularity of UN->. Moreover, the same proof is shown to extend the result in [TKB89] proving modularity of termination for left-linear and consistent with respect to reduction TRSs.
1995
Rewriting Techniques and Applications
9783540592006
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/2523481
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? ND
social impact