Séminaire, 15 février 2018
Exposés
 11:00: Giulio Manzonetto (LIPN, Paris 13), Refutation of Sallé's Longstanding Conjecture

The lambdacalculus possesses a strong notion of extensionality, called "the omegarule", which has been the subject of many investigations. It is a longstanding open problem whether the equivalence obtained by closing the theory of Böhm trees under the omegarule is strictly included in Morris's original observational theory, as conjectured by Sallé in the seventies. We will first show that Morris's theory satisfies the omegarule. We will then demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture. The proof technique we develop is general enough to provide as a byproduct a new characterization, based on bounded etaexpansions, of the least extensional equality between Böhm trees.