Strict Ideal Completions of the Lambda Calculus

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

View graph of relations

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 res- ulting infinitary calculi exhibit different notions of strictness. To obtain infinitary normalisation and infinitary confluence properties for these calculi, Kennaway et al. extend β-reduction with infinitely many ‘⊥-rules’, which contract meaningless terms directly to ⊥. 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 ex- tends 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 cor- responding metric-based calculi. Our calculi dispense with the infinitely many ⊥-rules of the metric-based calculi. The fully non-strict calculus (called 111) consists of only β-reduction, while the other two calculi (called 001 and 101) require two additional rules that precisely state their strictness properties: λx.⊥ → ⊥ (for 001) and ⊥ M → ⊥ (for 001 and 101).
Original languageEnglish
Title of host publication3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Number of pages16
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH
Publication dateJul 2018
Article number8
Publication statusPublished - Jul 2018
EventInternational Conference on Formal Structures for Computation and Deduction - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018
Conference number: 3


ConferenceInternational Conference on Formal Structures for Computation and Deduction
LandUnited Kingdom

    Research areas

  • lambda calculus, infinitary rewriting, Böhm trees, meaningless terms, confluence

ID: 83193562