@InProceedings{bahr17fscd,
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},
Month = sep,
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
⊥. 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.},
Keywords = {term graphs, confluence, infinitary rewriting, graph rewriting, Böhm trees}
}