Confluence for Abstract and Higher-Order Rewriting


In the first part the confluence by decreasing diagrams method is presented (see below). In the second part the higher-order rewriting systems (HORS) framework, developed in cooperation with Femke van Raamsdonk, is introduced. HORS rewriting is rewriting modulo some substitution calculus (SC). Some (7) axioms on an SC are presented which suffice to reduce the finiteness of developments theorem for a HORS to termination of the SC. This has the finiteness of developments theorem for higher-order term rewriting (= rewriting modulo simply typed lambda calculus) as a consequence, and implies confluence for all orthogonal higher-order term rewriting systems. Moreover, one extra axiom (cubicity, expressing that every triple of pairwise independent redexes is independent), is shown to suffice to conclude confluence of weakly orthogonal (all critical pairs are trivial, e.g. lambda beta eta calculus) systems. This implies modularity of confluence for left-linear systems such that critical pairs among the systems are trivial. We conclude by combining the two methods (confluence by decreasing diagrams and confluence by orthogonality) to show confluence for a list-extension of lambda calculus due to Revesz.