License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.32
URN: urn:nbn:de:0030-drops-59862
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5986/
Go to the corresponding LIPIcs Volume Portal

van Oostrom, Vincent ; Toyama, Yoshihito

Normalisation by Random Descent

pdf-format:
LIPIcs-FSCD-2016-32.pdf (0.7 MB)

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 - Entry

@InProceedings{vanoostrom_et_al:LIPIcs:2016:5986,
  author =	{Vincent van Oostrom and Yoshihito Toyama},
  title =	{{Normalisation by Random Descent}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{32:1--32:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5986},
  URN =		{urn:nbn:de:0030-drops-59862},
  doi =		{10.4230/LIPIcs.FSCD.2016.32},
  annote =	{Keywords: strategy,  hyper-normalisation, commutation, random descent}
}

Keywords: strategy, hyper-normalisation, commutation, random descent
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI