BUBBLES IN MODULARITY

We provide a global technique, called neatening, for the study of modu larity of left-linear term rewriting systems. Objects called bubbles a re identified as the responsibles of most of the problems occurring in modularity, and the concept of well-behaved (from the modularity poin t 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 gene ric reduction so to obtain a neat one, thus showing that restricting t o neat reductions is not limitative. This general technique is used to provide a unique, uniform method able to elegantly prove all the exis ting results on the modularity of every basic property of left-linear term rewriting systems, and also to provide new results on the modular ity of termination.