Development Closed Critical Pairs


The class of orthogonal rewriting systems (rewriting systems where rewrite steps cannot depend on one another) is the main class of not-necessarily-terminating rewriting systems for which confluence is known to hold. Huet and Toyama have shown that for left-linear first-order term rewriting systems (TRSs) the orthogonality restriction can be relaxed somewhat by allowing critical pairs (arising from maximally general ways of dependence between steps), but requiring them to be parallel closed. We extend these results by replacing the parallel closed condition by a development closed condition. This also permits to generalise them to higher-order term rewriting, yielding a confluence criterion for Klop's combinatory reduction systems (CRSs), Khasidashvili's expression reduction systems (ERSs), and Nipkow's higher-order pattern rewriting systems (PRSs).