Document Open Access Logo

Böhm Reduction in Infinitary Term Graph Rewriting Systems

Author Patrick Bahr

Thumbnail PDF


  • Filesize: 0.53 MB
  • 20 pages

Document Identifiers

Author Details

Patrick Bahr

Cite AsGet BibTex

Patrick Bahr. Böhm Reduction in Infinitary Term Graph Rewriting Systems. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 8:1-8:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)


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.
  • infinitary rewriting
  • term graphs
  • Böhm trees


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. P. Bahr. Abstract models of transfinite reductions. In C. Lynch, editor, RTA 10, volume 6 of LIPIcs, pages 49-66, 2010. URL:
  2. P. Bahr. Partial order infinitary term rewriting and Böhm trees. In C. Lynch, editor, RTA, volume 6 of LIPIcs, pages 67-84, 2010. URL:
  3. P. Bahr. Infinitary term graph rewriting is simple, sound and complete. In A. Tiwari, editor, RTA, volume 15 of LIPIcs, pages 69-84, 2012. URL:
  4. P. Bahr. Convergence in infinitary term graph rewriting systems is simple. Unpublished manuscript, available from the author’s website, 2013. Google Scholar
  5. P. Bahr. Böhm reduction in infinitary term graph rewriting systems. Companion report, available from the author’s website, 2017. Google Scholar
  6. Henk P. Barendregt. Representing`undefined' in the lambda calculus. Journal of Functional Programming, 2:367-374, 1992. Google Scholar
  7. H. P. Barendregt, M. C. J. D. van Eekelen, J. R. W. Glauert, R. Kennaway, M. J. Plasmeijer, and M. R. Sleep. Term graph rewriting. In PARLE, pages 141-158, 1987. Google Scholar
  8. R. Kennaway and F.-J. de Vries. Infinitary rewriting. In Terese, editor, Term Rewriting Systems, chapter 12, pages 668-711. Cambridge University Press, 2003. Google Scholar
  9. R. Kennaway, J. W. Klop, M. R. Sleep, and F.-J. de Vries. Transfinite reductions in orthogonal term rewriting systems. Inf. Comput., 119(1):18-38, 1995. URL: 10.1006/inco.1995.1075.
  10. R. Kennaway, V. van Oostrom, and F.-J. de Vries. Meaningless terms in rewriting. J. Funct. Logic Programming, 1999(1):1-35, February 1999. Google Scholar
  11. Richard Kennaway, Jan Willem Klop, M. R. Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. Theoretical Computer Science, 175(1):93-125, 1997. URL:
  12. J. Ketema. Böhm-Like Trees for Rewriting. PhD thesis, Vrije Universiteit Amsterdam, 2006. URL:
  13. D. Plump. Term graph rewriting. In H. Ehrig, G. Engels, H.-J. Kreowski, and G. Rozenberg, editors, Handbook of Graph Grammars and Computing by Graph Transformation, volume 2, pages 3-61. World Scientific Publishing Co., Inc., 1999. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail