Bubbles in modularity

We provide a global technique, called neatening, for the study of modularity of left-linear term rewriting systems. Objects called bubbles are identified as the responsibles of most of the problems occurring in modularity, and the concept of well-behaved (from the modularity point of view) reduction, called neat reduction, is introduced. Neatening consists of two steps: the first is proving a property is modular when only neat reductions are considered; the second is to ‘neaten’ a generic reduction so to obtain a neat one, thus showing that restricting to neat reductions is not limitative. This general technique is used to provide a unique, uniform method able to elegantly prove all the existing results on the modularity of every basic property of left-linear term rewriting systems, and also to provide new results on the modularity of termination.