Delimiting Diagrams


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 F-infinity for the lambda-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 F-infinity for the lambda-x-calculus. As far was we know, this is the first time that a strategy has been proven maximal for a lambda-calculus with explicit substitutions.