Ohana trees, linear approximation and multi-types for the $\lambda$I-calculus: No variable gets left behind or forgotten!

TL;DR

This paper introduces Ohana trees, a novel evaluation tree concept for the λI-calculus, leading to a new theory that preserves variable information and aligns with Taylor expansion, enhancing the understanding of λI-calculus semantics.

Contribution

It develops a new theory of λI-calculus based on Ohana trees, connecting denotational models, Taylor expansion, and variable tracking, which was previously unexplored.

Findings

Ohana trees encode hidden variables within λI-terms.

The Taylor expansion of a λI-term matches the expansion of its Ohana tree.

The introduced model captures the new equality and variable information.

Abstract

Although the $\lambda$I-calculus is a natural fragment of the $\lambda$-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 $\lambda$I-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the $\lambda$I-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a $\lambda$I-term is an annotated version of its B\"ohm 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 $\lambda$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 $\lambda$-calculus, which is known to yield proper models of the $\lambda$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, (...)