Benedetto Intrigila ; Giulio Manzonetto ; Andrew Polonsky - Degrees of extensionality in the theory of Böhm trees and Sallé's conjecture

lmcs:4305 - Logical Methods in Computer Science, January 29, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:6)2019
Degrees of extensionality in the theory of Böhm trees and Sallé's conjectureArticle

Authors: Benedetto Intrigila ; Giulio Manzonetto ; Andrew Polonsky

    The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between Böhm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal forms, equates two lambda-terms whenever their Böhm 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 Böhm 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 Böhm trees under the omega-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öhm trees. Together, these results provide a taxonomy of the different degrees of extensionality in the theory of Böhm trees.


    Volume: Volume 15, Issue 1
    Published on: January 29, 2019
    Accepted on: December 13, 2018
    Submitted on: February 22, 2018
    Keywords: Computer Science - Logic in Computer Science

    1 Document citing this article

    Consultation statistics

    This page has been seen 1164 times.
    This article's PDF has been downloaded 343 times.