Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture
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\"...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-01-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4305/pdf |
| _version_ | 1797268553876897792 |
|---|---|
| author | Benedetto Intrigila Giulio Manzonetto Andrew Polonsky |
| author_facet | Benedetto Intrigila Giulio Manzonetto Andrew Polonsky |
| author_sort | Benedetto Intrigila |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:19Z |
| format | Article |
| id | doaj.art-420b00724d084f548817bec7f5d21f2f |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:19Z |
| publishDate | 2019-01-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-420b00724d084f548817bec7f5d21f2f2024-03-08T10:27:56ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-01-01Volume 15, Issue 110.23638/LMCS-15(1:6)20194305Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjectureBenedetto IntrigilaGiulio ManzonettoAndrew PolonskyThe 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.https://lmcs.episciences.org/4305/pdfcomputer science - logic in computer science |
| spellingShingle | Benedetto Intrigila Giulio Manzonetto Andrew Polonsky Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture Logical Methods in Computer Science computer science - logic in computer science |
| title | Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture |
| title_full | Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture |
| title_fullStr | Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture |
| title_full_unstemmed | Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture |
| title_short | Degrees of extensionality in the theory of B\"ohm trees and Sall\'e's conjecture |
| title_sort | degrees of extensionality in the theory of b ohm trees and sall e s conjecture |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/4305/pdf |
| work_keys_str_mv | AT benedettointrigila degreesofextensionalityinthetheoryofbohmtreesandsallesconjecture AT giuliomanzonetto degreesofextensionalityinthetheoryofbohmtreesandsallesconjecture AT andrewpolonsky degreesofextensionalityinthetheoryofbohmtreesandsallesconjecture |