On the Modularity of Normal Forms in Rewriting

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 left-linear 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→), showing its modularity for left-linear Term Rewriting Systems.