Refutation of Sallé’s Longstanding Conjecture

Carte non disponible

Date/heure
Date(s) - 15/02/2018
11 h 00 min - 12 h 30 min

Catégories


The lambda-calculus 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 obtained by closing the theory of Böhm trees under the omega-rule 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 omega-rule. 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 eta-expansions, of the least extensional equality between Böhm trees.

http://www-lipn.univ-paris13.fr/~gmanzonetto/

Olivier CHABROL
Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange