## 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 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).

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).

Originalsprog | Engelsk |
---|---|

Titel | 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) |

Antal sider | 16 |

Forlag | Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH |

Publikationsdato | jul. 2018 |

Sider | 8:1-8:16 |

Artikelnummer | 8 |

DOI | |

Status | Udgivet - jul. 2018 |

Begivenhed | International Conference on Formal Structures for Computation and Deduction - Oxford, Storbritannien Varighed: 9 jul. 2018 → 12 jul. 2018 Konferencens nummer: 3 http://www.cs.le.ac.uk/events/fscd2018/ |

### Konference

Konference | International Conference on Formal Structures for Computation and Deduction |
---|---|

Nummer | 3 |

Land/Område | Storbritannien |

By | Oxford |

Periode | 09/07/2018 → 12/07/2018 |

Internetadresse |