@InProceedings{bohmgraphs,
  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 = aug,
  Date = {2017-08-30},
  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}
}