@article{graphsimple-extended,
  Title = {Convergence in Infinitary Term Graph Rewriting Systems is Simple},
  Author = {Patrick Bahr},
  journal = {Mathematical Structures in Computer Science},
  publisher = {Cambridge University Press},
  pages = {1–52},
  Month = aug,
  Date = {2018-08-09},
  Year = {2018},
  doi = {10.1017/S0960129518000166},
  Abstract = {Term graph rewriting provides a formalism for implementing term
  rewriting in an efficient manner by emulating duplication via
  sharing. Infinitary term rewriting has been introduced to study
  infinite term reduction sequences. Such infinite reductions can be
  used to model \emph{non-strict evaluation}. In this paper, we unify
  term graph rewriting and infinitary term rewriting thereby
  addressing both components of \emph{lazy evaluation}: non-strictness
  and sharing.

  In contrast to previous attempts to formalise infinitary term graph
  rewriting, our approach is based on a simple and natural
  generalisation of the modes of convergence of infinitary term
  rewriting. We show that this new approach is better suited for
  infinitary term graph rewriting as it is simpler and more
  general. The latter is demonstrated by the fact that our notions of
  convergence give rise to two independent canonical and exhaustive
  constructions of infinite term graphs from finite term graphs via
  metric and ideal completion.  In addition, we show that our notions
  of convergence on term graphs are sound w.r.t.\ the ones employed in
  infinitary term rewriting in the sense that convergence is preserved
  by unravelling term graphs to terms. Moreover, the resulting
  infinitary term graph calculi provide a unified framework for both
  infinitary term rewriting and term graph rewriting, which makes it
  possible to study the correspondences between these two worlds more
  closely.}
}