Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture.

The main observational equivalences of the untyped lambda-calculus have beencharacterized in terms of extensional equalities between B\"ohm trees. It iswell known that the lambda-theory H*, arising by taking as observables the headnormal forms, equates two lambda-terms whenever their B\"ohm trees are equal upto countably many possibly infinite eta-expansions. Similarly, two lambda-termsare equal in Morris's original observational theory H+, generated byconsidering as observable the beta-normal forms, whenever their B\"ohm treesare 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 alongstanding open problem whether the equivalence B-omega obtained by closingthe theory of B\"ohm trees under the omega-rule is strictly included in H+, asconjectured by Sall\'e in the seventies. In this paper we demonstrate that thetwo aforementioned theories actually coincide, thus disproving Sall\'e'sconjecture.

The proof technique we develop for proving the latter inclusion is generalenough to provide as a byproduct a new characterization, based on boundedeta-expansions, of the least extensional equality between B\"ohm trees.Together, these results provide a taxonomy of the different degrees ofextensionality in the theory of B\"ohm trees.