Degrees of extensionality in the theory of Böhm trees and sallé’s conjecture

The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between Bohm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal forms, equates two A-terms whenever their Bohm trees are equal up to countably many possibly infinite eta-expansions. Similarly, two lambda-terms are equal in Morris's original observational theory H+, generated by considering as observable the beta-normal forms, whenever their Bohm trees are equal up to countably many finite eta-expansions.The lambda-calculus also possesses a strong notion of extensionality called the omega-rule, which has been the subject of many investigations. It is a longstanding open problem whether the equivalence B omega obtained by closing the theory of Bohm trees under the u-rule is strictly included in H+, as conjectured by Salle in the seventies. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallc's conjecture.The inclusion B omega subset of H+ is a consequence of the fact that the lambda-theory H+ satisfies the omega-rule. This result follows from a weak form of separability enjoyed by lambda-terms whose Bohm trees only differ because of some infinite eta-expansions, a property which is proved through a refined version of the famous Bohm-out technique.The inclusion H+ subset of B omega follows from the fact that whenever two A-terms are observationally equivalent in H+ their Bohm trees have a common "beta-supremum" that can be A-defined starting from a stream (infinite sequence) of eta-expansions of the identity. It turns out that in B omega such a stream is equal to the stream containing infinitely many copies of the identity, a peculiar property that actually makes the two theories collapse.The proof technique we develop for proving the latter inclusion is general enough to provide as a byproduct a new characterization, based on bounded eta-expansions, of the least extensional equality between Bohm trees. Together, these results provide a taxonomy of the different degrees of extensionality in the theory of Bohm trees.