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.2017.8
URN: urn:nbn:de:0030-drops-77275
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7727/
Go to the corresponding LIPIcs Volume Portal

Bahr, Patrick

Böhm Reduction in Infinitary Term Graph Rewriting Systems

pdf-format:
LIPIcs-FSCD-2017-8.pdf (0.5 MB)

Abstract

The confluence properties of lambda calculus and orthogonal term rewriting do not generalise to the corresponding infinitary calculi. In order to recover the confluence property in a meaningful way, Kennaway et al. introduced Böhm reduction, which extends the ordinary reduction relation so that "meaningless terms" can be contracted to a fresh constant "bottom". In previous work, we have established that Böhm reduction can be instead characterised by a different mode of convergences of transfinite reductions that is based on a partial order structure instead of a metric space.

In this paper, we develop a corresponding theory of Böhm reduction for term graphs. Our main result is that partial order convergence in a term graph rewriting system can be truthfully and faithfully simulated by metric convergence in the Böhm extension of the system. To prove this result we generalise the notion of residuals and projections to the setting of infinitary term graph rewriting. As ancillary results we prove the infinitary strip lemma and the compression property, both for partial order and metric convergence.

BibTeX - Entry

@InProceedings{bahr:LIPIcs:2017:7727,
  author =	{Patrick Bahr},
  title =	{{B{\"o}hm Reduction in Infinitary Term Graph Rewriting Systems}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7727},
  URN =		{urn:nbn:de:0030-drops-77275},
  doi =		{10.4230/LIPIcs.FSCD.2017.8},
  annote =	{Keywords: infinitary rewriting, term graphs, B{\"o}hm trees}
}

Keywords: infinitary rewriting, term graphs, Böhm trees
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

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