Severi, Paula ;
de Vries, FerJan
Weakening the Axiom of Overlap in Infinitary Lambda Calculus
Abstract
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.
BibTeX  Entry
@InProceedings{severi_et_al:LIPIcs:2011:3131,
author = {Paula Severi and FerJan de Vries},
title = {{Weakening the Axiom of Overlap in Infinitary Lambda Calculus}},
booktitle = {22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
pages = {313328},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897309 },
ISSN = {18688969},
year = {2011},
volume = {10},
editor = {Manfred SchmidtSchau{\ss}},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2011/3131},
URN = {urn:nbn:de:0030drops31312},
doi = {http://dx.doi.org/10.4230/LIPIcs.RTA.2011.313},
annote = {Keywords: Infinitary Lambda Calculus, Confluence, Normalization}
}
2011
Keywords: 

Infinitary Lambda Calculus, Confluence, Normalization 
Seminar: 

22nd International Conference on Rewriting Techniques and Applications (RTA'11)

Issue date: 

2011 
Date of publication: 

2011 