2026-07-23T06:52:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7723 2024-03-06T10:41:03Z ddc:004 open_access

Refutation of Sallé's Longstanding Conjecture Intrigila, Benedetto Manzonetto, Giulio Polonsky, Andrew lambda calculus observational equivalence Böhm trees omega-rule 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. In a recent work, Breuvart et al. have shown that Morris's theory satisfies the omega-rule. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Benedetto Intrigila and Giulio Manzonetto and Andrew Polonsky 2017 Is Part Of LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2017.20 urn:nbn:de:0030-drops-77236 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.20 eng https://creativecommons.org/licenses/by/3.0/legalcode