|
Abstract : |
The last open problem regarding the modularity of the fundamental properties of Term Rewriting Systems concerns the property of uniqueness of normal forms w.r.t. reduction (UN). In this article we solve this open problem,showing that UN is modular for leftlinear Term Rewriting Systems. The novel `pile and delete ' technique here introduced allows for quite a short proof, and is of independent interest in the study of modular properties. Moreover, we also study the modularity of consistency w.r.t. reduction (CON, |