LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Seminar
Degrees of extensionality in the theory of Boehm trees
- Date
- 14.01.2020, 11:00
- Place
- Pavillon des Jardins
- Speaker
- Giulio Manzonetto (LIPN)
The main observational equivalences of the untyped λ-calculus have been characterized in terms of extensional equalities between Böhm trees. It is well known that the λ-theory H*, arising by taking as observables the head normal forms, equates two λ-terms whenever their Böhm trees are equal up to countably many possibly infinite eta-expansions. Similarly, two λ-terms are equal in Morris's original observational theory H+, generated by considering as observable the beta-normal forms, whenever their Böhm trees are equal up to countably many finite eta-expansions. The λ-calculus also possesses a strong notion of extensionality called the ω-rule, which has been the subject of many investigations. It is a longstanding open problem whether the equivalence Bω obtained by closing the theory of Böhm trees under the ω-rule is strictly included in H+, as conjectured by Sallé in the seventies. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture. 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 Böhmtrees. Together, these results provide a taxonomy of the different degrees of extensionality in the theory of Böhm trees.