Although the $λ$I-calculus is a natural fragment of the $λ$-calculus, obtained by forbidding the erasure, 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, (...)

翻译：尽管$λ$I-演算是$λ$-演算的一个自然片段（通过禁止擦除操作获得），但其等式理论并未受到足够关注。原因在于文献中研究的所有真值指称模型都将所有不可规范化的$λ$I-项视为等价，导致相关理论缺乏信息量。本文的目标是引入一种先前未知的$λ$I-演算理论，该理论由我们称为“Ohana树”的求值树概念所诱导。$λ$I-项的Ohana树是其Böhm树的注释版本，能记录所有隐藏在其无意义子树中或沿无限分支被推至无穷远处的自由变量。我们发展了相应的程序逼近理论：第一种方法（更经典）基于有限树和连续性，第二种方法则适配了Ehrhard与Regnier的泰勒展开。随后我们证明了一个交换定理，表明$λ$I-项的泰勒展开的规范形式与其Ohana树的泰勒展开一致。作为推论，我们得到Ohana树诱导的等式对抽象和应用操作具有兼容性。接着，我们引入一个专门设计用于捕捉Ohana树诱导等式的指称模型。虽然以非幂等类型系统形式呈现，但该模型基于适当修改的$λ$-演算关系语义版本（已知当限制为非空有限多重集时能产生$λ$I-演算的真值模型）。为了追踪在求值树中被隐藏或推至无穷远的子项中出现的变量，我们通过两种方式推广该系统：首先，重新引入由变量集索引的空多重集的注释版本；其次，（……）