Strict Ideal Completions of the Lambda Calculus

Author Patrick Bahr



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.8.pdf
  • Filesize: 492 kB
  • 16 pages

Document Identifiers

Author Details

Patrick Bahr
  • IT University of Copenhagen, Denmark

Cite AsGet BibTex

Patrick Bahr. Strict Ideal Completions of the Lambda Calculus. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.8

Abstract

The infinitary lambda calculi pioneered by Kennaway et al. extend the basic lambda calculus by metric completion to infinite terms and reductions. Depending on the chosen metric, the resulting infinitary calculi exhibit different notions of strictness. To obtain infinitary normalisation and infinitary confluence properties for these calculi, Kennaway et al. extend beta-reduction with infinitely many `bot-rules', which contract meaningless terms directly to bot. Three of the resulting Böhm reduction calculi have unique infinitary normal forms corresponding to Böhm-like trees. In this paper we develop a corresponding theory of infinitary lambda calculi based on ideal completion instead of metric completion. We show that each of our calculi conservatively extends the corresponding metric-based calculus. Three of our calculi are infinitarily normalising and confluent; their unique infinitary normal forms are exactly the Böhm-like trees of the corresponding metric-based calculi. Our calculi dispense with the infinitely many bot-rules of the metric-based calculi. The fully non-strict calculus (called 111) consists of only beta-reduction, while the other two calculi (called 001 and 101) require two additional rules that precisely state their strictness properties: lambda x.bot -> bot (for 001) and bot M -> bot (for 001 and 101).

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
Keywords
  • lambda calculus
  • infinitary rewriting
  • Böhm trees
  • meaningless terms
  • confluence

Metrics

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

References

  1. André Arnold and Maurice Nivat. The metric space of infinite trees. algebraic and topological properties. Fundamenta Informaticae, 3(4):445-476, 1980. Google Scholar
  2. Patrick Bahr. Abstract Models of Transfinite Reductions. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 49-66, Dagstuhl, Germany, 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2010.49.
  3. Patrick Bahr. Partial order infinitary term rewriting and Böhm trees. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 67-84, Dagstuhl, Germany, 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2010.67.
  4. Patrick Bahr. Infinitary term graph rewriting is simple, sound and complete. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12), volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), pages 69-84, Dagstuhl, Germany, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2012.69.
  5. Patrick Bahr. Ideal completions of the lambda calculus. Companion report, available from the author’s web site, 2018. Google Scholar
  6. Henk P Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathemantics. Elsevier Science, revised edition, 1984. Google Scholar
  7. Alessandro Berarducci. Infinite λ-calculus and non-sensible models. In A Ursini and P Aglianó, editors, Logic and algebra, number 180 in Lecture Notes in Pure and Applied Mathematics, pages 339-378. CRC Press, 1996. Google Scholar
  8. Stefan Blom. Term Graph Rewriting-Syntax and Semantics. PhD thesis, Vrije Universiteit te Amsterdam, 2001. Google Scholar
  9. Stefan Blom. An approximation based approach to infinitary lambda calculi. In Vincent van Oostrom, editor, Rewriting Techniques and Applications, volume 3091 of Lecture Notes in Computer Science, pages 221-232. Springer Berlin / Heidelberg, 2004. URL: http://dx.doi.org/10.1007/b98160.
  10. 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: https://doi.org/10.1016/S0304-3975(96)00171-5.
  11. Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries. Meaningless terms in rewriting. Journal of Functional and Logic Programming, 1999(1):1-35, 1999. Google Scholar
  12. Jeroen Ketema. Böhm-Like Trees for Rewriting. PhD thesis, Vrije Universiteit Amsterdam, 2006. URL: http://dare.ubvu.vu.nl/handle/1871/9203.
  13. Jean-Jacques Lévy. An algebraic interpretation of the λβ K-calculus; and an application of a labelled λ-calculus. Theoretical Computer Science, 2(1):97-114, 1976. URL: http://dx.doi.org/10.1016/0304-3975(76)90009-8.
  14. Jean-Jacques Lévy. Réductions Correctes et Optimales dans le Lambda-Calcul. PhD thesis, Université Paris VII, 1978. Google Scholar
  15. Giuseppe Longo. Set-theoretical models of λ-calculus: theories, expansions, isomorphisms. Annals of pure and applied logic, 24(2):153-188, 1983. Google Scholar
  16. Mila E Majster-Cederbaum and Christel Baier. Metric completion versus ideal completion. Theoretical Computer Science, 170(1-2):145-171, 1996. URL: https://doi.org/10.1016/S0304-3975(96)80705-5.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail