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.
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.
