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 identi ed as the responsibles of most of the problems occurring in modularity, and the concept of well-behaved (from the modularity point of view) reduction, said neat reduction, is introduced. Neating consists of two steps: the rst 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 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.

• Type: Journal
• Year: 1998
• Where: TCS
• Authors: Massimo Marchiori
• Keywords: Left-linear Term, Neat Reductions, TCS 1998, Term Rewriting Systems, Theoretical Computer Science