Delimiting diagrams

Abstract

We introduce the unifying notion of delimiting diagram. Hitherto unrelated results such as: Minimality of the internal needed strategy for orthogonal first-order term rewriting systems, maximality of the limit strategy for orthogonal higher-order pattern rewrite systems (with maximality of the strategy Foo for the λ-calculus as a special case), and uniform normalisation of balanced weak Church–Rosser abstract rewriting systems, all are seen to follow from the property that any pair of diverging steps can be completed into a delimiting diagram. Apart from yielding simple uniform proofs of those results, the same methodology yields a proof of maximality of the strategy Foo for the λx--calculus. As far was we know, this is the first time that a strategy has been proven maximal for a λ-calculus with explicit substitutions.