2026-07-20T07:17:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5986 2024-03-06T10:37:27Z ddc:004 open_access

Normalisation by Random Descent van Oostrom, Vincent Toyama, Yoshihito strategy hyper-normalisation commutation random descent 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Vincent van Oostrom and Yoshihito Toyama 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.32 urn:nbn:de:0030-drops-59862 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.32 eng https://creativecommons.org/licenses/by/3.0/legalcode