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 betareduction with infinitely many `botrules', which contract meaningless terms directly to bot. Three of the resulting Böhm reduction calculi have unique infinitary normal forms corresponding to Böhmlike 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 metricbased calculus. Three of our calculi are infinitarily normalising and confluent; their unique infinitary normal forms are exactly the Böhmlike trees of the corresponding metricbased calculi. Our calculi dispense with the infinitely many botrules of the metricbased calculi. The fully nonstrict calculus (called 111) consists of only betareduction, 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).
BibTeX  Entry
@InProceedings{bahr:LIPIcs:2018:9178,
author = {Patrick Bahr},
title = {{Strict Ideal Completions of the Lambda Calculus}},
booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
pages = {8:18:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770774},
ISSN = {18688969},
year = {2018},
volume = {108},
editor = {H{\'e}l{\`e}ne Kirchner},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9178},
URN = {urn:nbn:de:0030drops91787},
doi = {10.4230/LIPIcs.FSCD.2018.8},
annote = {Keywords: lambda calculus, infinitary rewriting, B{\"o}hm trees, meaningless terms, confluence}
}
Keywords: 

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

3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) 
Issue Date: 

2018 
Date of publication: 

04.07.2018 