The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between Bohm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal forms, equates two A-terms whenever their Bohm 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 Bohm 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 Bohm trees under the u-rule is strictly included in H+, as conjectured by Salle in the seventies. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallc's conjecture.The inclusion B omega subset of H+ is a consequence of the fact that the lambda-theory H+ satisfies the omega-rule. This result follows from a weak form of separability enjoyed by lambda-terms whose Bohm trees only differ because of some infinite eta-expansions, a property which is proved through a refined version of the famous Bohm-out technique.The inclusion H+ subset of B omega follows from the fact that whenever two A-terms are observationally equivalent in H+ their Bohm trees have a common "beta-supremum" that can be A-defined starting from a stream (infinite sequence) of eta-expansions of the identity. It turns out that in B omega such a stream is equal to the stream containing infinitely many copies of the identity, a peculiar property that actually makes the two theories collapse.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 Bohm trees. Together, these results provide a taxonomy of the different degrees of extensionality in the theory of Bohm trees.

Intrigila, B., Manzonetto, G., Polonsky, A. (2019). Degrees of extensionality in the theory of Böhm trees and sallé’s conjecture. LOGICAL METHODS IN COMPUTER SCIENCE, 15(1), 6:3-6:36 [10.23638/LMCS-15(1:6)2019].

Degrees of extensionality in the theory of Böhm trees and sallé’s conjecture

Intrigila B.;
2019-01-29

Abstract

The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between Bohm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal forms, equates two A-terms whenever their Bohm 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 Bohm 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 Bohm trees under the u-rule is strictly included in H+, as conjectured by Salle in the seventies. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallc's conjecture.The inclusion B omega subset of H+ is a consequence of the fact that the lambda-theory H+ satisfies the omega-rule. This result follows from a weak form of separability enjoyed by lambda-terms whose Bohm trees only differ because of some infinite eta-expansions, a property which is proved through a refined version of the famous Bohm-out technique.The inclusion H+ subset of B omega follows from the fact that whenever two A-terms are observationally equivalent in H+ their Bohm trees have a common "beta-supremum" that can be A-defined starting from a stream (infinite sequence) of eta-expansions of the identity. It turns out that in B omega such a stream is equal to the stream containing infinitely many copies of the identity, a peculiar property that actually makes the two theories collapse.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 Bohm trees. Together, these results provide a taxonomy of the different degrees of extensionality in the theory of Bohm trees.
29-gen-2019
Pubblicato
Rilevanza internazionale
Articolo
Esperti anonimi
Settore INF/01 - INFORMATICA
English
lambda-calculus; lambda-theories; observational equivalences; Bohm trees; omega-rule; Sallc's conjecture; Bohm-out technique
Intrigila, B., Manzonetto, G., Polonsky, A. (2019). Degrees of extensionality in the theory of Böhm trees and sallé’s conjecture. LOGICAL METHODS IN COMPUTER SCIENCE, 15(1), 6:3-6:36 [10.23638/LMCS-15(1:6)2019].
Intrigila, B; Manzonetto, G; Polonsky, A
Articolo su rivista
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2108/234758
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact