2026-07-20T05:59:45Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3131 2024-03-06T10:33:52Z ddc:004 open_access

Weakening the Axiom of Overlap in Infinitary Lambda Calculus Severi, Paula de Vries, Fer-Jan Infinitary Lambda Calculus Confluence Normalization In this paper we present a set of necessary and sufficient conditions on a set of lambda terms to serve as the set of meaningless terms in an infinitary bottom extension of lambda calculus. So far only a set of sufficient conditions was known for choosing a suitable set of meaningless terms to make this construction produce confluent extensions. The conditions covered the three main known examples of sets of meaningless terms. However, the much later construction of many more examples of sets of meaningless terms satisfying the sufficient conditions renewed the interest in the necessity question and led us to reconsider the old conditions. The key idea in this paper is an alternative solution for solving the overlap between beta reduction and bottom reduction. This allows us to reformulate the Axiom of Overlap, which now determines together with the other conditions a larger class of sets of meaningless terms. We show that the reformulated conditions are not only sufficient but also necessary for obtaining a confluent and normalizing infinitary lambda beta bottom calculus. As an interesting consequence of the necessity proof we obtain for infinitary lambda calculus with beta and bot reduction that confluence implies normalization. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Paula Severi and Fer-Jan de Vries 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.313 urn:nbn:de:0030-drops-31312 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.313 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode