Ohana trees, linear approximation and multi-types for the $λ$I-calculus: No variable gets left behind or forgotten!
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910058507403264 |
|---|---|
| author | Cerda, Rémy Manzonetto, Giulio Saurin, Alexis |
| author_facet | Cerda, Rémy Manzonetto, Giulio Saurin, Alexis |
| contents | Although the $λ$I-calculus is a natural fragment of the $λ$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable $λ$I-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the $λ$I-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a $λ$I-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches.
We develop the associated theories of program approximation: the first approach -- more classic -- is based on finite trees and continuity, the second adapts Ehrhard and Regnier's Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a $λ$I-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application.
Subsequently, we introduce a denotational model designed to capture the equality induced by Ohana trees. Although presented as a non-idempotent type system, our model is based on a suitably modified version of the relational semantics of the $λ$-calculus, which is known to yield proper models of the $λ$I-calculus when restricted to non-empty finite multisets. To track variables occurring in subterms that are hidden or pushed to infinity in the evaluation trees, we generalize the system in two ways: first, we reintroduce annotated versions of the empty multiset indexed by sets of variables; second, (...) |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_06193 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Ohana trees, linear approximation and multi-types for the $λ$I-calculus: No variable gets left behind or forgotten! Cerda, Rémy Manzonetto, Giulio Saurin, Alexis Logic in Computer Science Programming Languages F.4.2; F.3.1 Although the $λ$I-calculus is a natural fragment of the $λ$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable $λ$I-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the $λ$I-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a $λ$I-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach -- more classic -- is based on finite trees and continuity, the second adapts Ehrhard and Regnier's Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a $λ$I-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. Subsequently, we introduce a denotational model designed to capture the equality induced by Ohana trees. Although presented as a non-idempotent type system, our model is based on a suitably modified version of the relational semantics of the $λ$-calculus, which is known to yield proper models of the $λ$I-calculus when restricted to non-empty finite multisets. To track variables occurring in subterms that are hidden or pushed to infinity in the evaluation trees, we generalize the system in two ways: first, we reintroduce annotated versions of the empty multiset indexed by sets of variables; second, (...) |
| title | Ohana trees, linear approximation and multi-types for the $λ$I-calculus: No variable gets left behind or forgotten! |
| topic | Logic in Computer Science Programming Languages F.4.2; F.3.1 |
| url | https://arxiv.org/abs/2505.06193 |