Finite Family Developments


Associate to a rewrite system R having rules l -> r its labelled version R(N) having rules l(n+1) -> r[n] for any natural number n in N. These rules roughly express that a left-hand side l carrying labels all larger than n can be replaced by its right-hand side r carrying labels all smaller than or equal to n. A rewrite system R enjoys finite family developments (FFD) if R(N) is terminating. We show that the class of higher order pattern rewrite systems enjoys FFD, extending earlier results for the lambda calculus and first order term rewrite systems.