一句话：证明 B-ω 与 Morris 理论 H+ 相等，推翻 Sallé 猜想，并给出 Böhm 树外延性等价的分类。
本文研究无类型 λ 演算中基于 Böhm 树的观察等价。已知 H* 对应 Böhm 树在可数多个可能无穷 η-展开下的相等，Morris 的 H+ 对应可数多个有限 η-展开下的相等；B-ω 则将 Böhm 树理论对 ω-规则封闭。Sallé 曾猜想 B-ω 严格包含于 H+。作者证明 B-ω 与 H+ 实际重合，从而否定该猜想。其证明技术还具有一般性，可推出以有界 η-展开刻画 Böhm 树间最小外延等价的新结果，并据此给出不同外延性程度的分类。
The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between B\"ohm 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\"ohm 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\"ohm 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\"ohm trees under the omega-rule is strictly included in H+, as conjectured by Sall\'e in the seventies. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sall\'e'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\"ohm trees. Together, these results provide a taxonomy of the different degrees of extensionality in the theory of B\"ohm trees.
@article{paperbot835,
title = {Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture},
author = {Benedetto Intrigila and Giulio Manzonetto and Andrew Polonsky},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:6)2019}
}