English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The main observational equivalences of the untyped lambda-calculus have beencharacterized in terms of extensional equalities between B\"ohm trees. It iswell known that the lambda-theory H*, arising by taking as observables the headnormal forms, equates two lambda-terms whenever their B\"ohm trees are equal upto countably many possibly infinite eta-expansions. Similarly, two lambda-termsare equal in Morris's original observational theory H+, generated byconsidering as observable the beta-normal forms, whenever their B\"ohm treesare 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 alongstanding open problem whether the equivalence B-omega obtained by closingthe theory of B\"ohm trees under the omega-rule is strictly included in H+, asconjectured by Sall\'e in the seventies. In this paper we demonstrate that thetwo aforementioned theories actually coincide, thus disproving Sall\'e'sconjecture.  The proof technique we develop for proving the latter inclusion is generalenough to provide as a byproduct a new characterization, based on boundedeta-expansions, of the least extensional equality between B\"ohm trees.Together, these results provide a taxonomy of the different degrees ofextensionality in the theory of B\"ohm trees.

Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture