### Normalisation by Random Descent

Vincent van Oostrom and Yoshihito ToyamaProceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Leibniz International Proceedings in Informatics 52, pp. 32:1 – 32:18, 2016.

### Abstract

We present abstract hyper-normalisation results for strategies. These

results are then applied to term rewriting systems, both first and

higher-order. For example, we show hyper-normalisation of the

left—outer strategy for, what we call, left—outer pattern rewrite

systems, a class comprising both Combinatory Logic and the

lambda-calculus but also systems with critical pairs. Our results apply

to strategies that need not be deterministic but do have Newman’s random

descent property: all reductions to normal form have the same length,

with Huet and Lévy’s external strategy being an example. Technically, we

base our development on supplementing the usual notion of commutation

diagram with a notion of order, expressing that the measure of its right

leg does not exceed that of its left leg, where measure is an

abstraction of the usual notion of length. We give an exact

characterisation of such global commutation diagrams, for pairs of

reductions, by means of local ones, for pairs of steps, we dub Dyck

diagrams.

### BibTeX

@inproceedings{VvOYT-FSCD16, author = "Vincent van Oostrom and Yoshihito Toyama", title = "Normalisation by Random Descent", booktitle = "Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)", pages = "32:1-32:18", series = "Leibniz International Proceedings in Informatics (LIPIcs)", volume = 52, editor = "Delia Kesner and Brigitte Pientka", publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik", year = 2016 }

Creative Commons License CC-BY