Developing Developments


In the absence of termination, confluence of rewriting systems is often hard to establish. The class of orthogonal rewriting systems is the main class of not-necessarily-terminating, but confluent rewriting systems. The reason why confluence holds in orthogonal rewriting systems is the absence of so-called critical pairs, making that rewrite steps never interfere (in a destructive way) with one another. We discuss some ways to adapt the confluence by orthogonality proofmethod to rewriting systems having `innocent' critical pairs. Confluence results are obtained for lambda calculus with beta, eta and Omega rules, lambda calculi with restricted expansion rules and for (first- and higher-order) term rewriting systems for which all critical pairs are development closed.