We present abstract hyper-normalisation results for strategies. These#R##N#results are then applied to term rewriting systems, both first and#R##N#higher-order. For example, we show hyper-normalisation of the#R##N#left--outer strategy for, what we call, left--outer pattern rewrite#R##N#systems, a class comprising both Combinatory Logic and the#R##N#lambda-calculus but also systems with critical pairs. Our#R##N#results apply to strategies that need not be deterministic but do have#R##N#Newman's random descent property: all reductions to normal form have#R##N#the same length, with Huet and Levy's external strategy being an#R##N#example. Technically, we base our development on supplementing the#R##N#usual notion of commutation diagram with a notion of order, expressing#R##N#that the measure of its right leg does not exceed that of its left#R##N#leg, where measure is an abstraction of the usual notion of length.#R##N#We give an exact characterisation of such global commutation diagrams,#R##N#for pairs of reductions, by means of local ones, for pairs of steps,#R##N#we dub Dyck diagrams.
['Vincent van Oostrom', 'Yoshihito Toyama']
Normalisation by Random Descent