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.