Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!

Cerda, Rémy; Manzonetto, Giulio; Saurin, Alexis

doi:10.4230/LIPIcs.FSCD.2025.12

Ohana Trees and Taylor Expansion
for the λI-Calculus

Rémy Cerda

Université Paris Cité, CNRS, IRIF, F-75013, Paris, France Giulio Manzonetto

Université Paris Cité, CNRS, IRIF, F-75013, Paris, France Alexis Saurin Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
INRIA

\pi^{3}

, Paris, France

Abstract

Although the $\lambda{\sf I}$ -calculus is a natural fragment of the $\lambda$ -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 $\lambda{\sf 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{\sf I}$ -calculus, induced by a notion of evaluation trees that we call “Ohana trees”. The Ohana tree of a $\lambda{\sf 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 $\lambda{\sf 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. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full $\lambda$ -calculus.

Keywords and phrases:

\lambda

-calculus, program approximation, Taylor expansion, λI-calculus, persistent free variables, Böhm trees, Ohana trees

Funding:

Rémy Cerda: Partially funded by the ANR project RECIPROG ANR-21-CE48-019.

Alexis Saurin: Partially funded by the ANR project RECIPROG ANR-21-CE48-019.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Rewrite systems ; Theory of computation

\rightarrow

Lambda calculus ; Theory of computation

\rightarrow

Denotational semantics

Related Version:

Version hosted on arXiv, with additional proofs in an appendix: https://arxiv.org/abs/2505.06193 [11]

Acknowledgements:

We wish to thank Thomas Ehrhard, Paul-André Melliès, Lorenzo Tortora de Falco and Lionel Vaux Auclair for interesting discussions. We also thank the anonymous reviewers for the many valuable corrections they suggested.

DOI:

10.4230/LIPIcs.FSCD.2025.12

Event:

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Editors:

Maribel Fernández

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

In the pioneering article “The calculi of lambda-conversion” [13] Alonzo Church introduced the $\lambda$ -calculus together with its fragment without weakening, called the $\lambda{\sf I}$ -calculus, where each abstraction must bind at least one occurrence of a variable. Historically, the $\lambda{\sf I}$ -calculus has proven to be a useful framework for establishing results such as the finiteness of developments and standardization, which were successfully proven for the full $\lambda$ -calculus only decades later. Despite that, in the last forty years there are no groundbreaking advances in its study.

The study of models and theories of $\lambda$ -calculus flourished in the 1970s [4] and remained central in theoretical computer science for decades [5]. Although the equational theories of $\lambda$ -calculus, called $\lambda$ -theories, form a complete lattice of cardinality $2^{\aleph_{0}}$ [33], only a handful are of interest to computer scientists. Most articles focus on $\lambda$ -theories generated through some notion of “evaluation tree” of a $\lambda$ -term, which means that two $\lambda$ -terms are equated in the theory exactly when their evaluation trees coincide. The definitions of evaluation trees present in the literature follow the same pattern: they collect in a possibly infinite tree all stable portions of the output coming out from the computation, and replace the subterms that are considered meaningless by a constant $\bot$ , representing the lack of information. By modifying the notions of “stable” and “meaningless”, one obtains Böhm trees [3], possibly endowed with some form of extensionality [42, 27], Lévy-Longo trees [31, 32] and Berarducci trees [7]. In the modern language of infinitary term rewriting systems, these trees can be seen as the transfinite normal forms of infinitary $\lambda$ -calculi [22, 14]. Another popular method for defining $\lambda$ -theories is via observational equivalences [37]: two $\lambda$ -terms are equivalent if they display the same behaviour whenever plugged in any context. For instance, the theory of Scott’s $\mathcal{D}_{\infty}$ model [41] captures the maximal consistent observational equivalence [26, 47].

Since the $\lambda$ -calculus is a conservative extension of the $\lambda{\sf I}$ -calculus, every theory of the former is also a theory of the latter, namely a $\lambda{\sf I}$ -theory, while the converse does not hold. A typical example is the $\lambda{\sf I}$ -theory $\mathcal{H}_{{\sf I}}$ generated by equating all $\lambda{\sf I}$ -terms that are not $\beta$ -normalizing. The maximal consistent observational equivalence $\mathcal{H}_{{\sf I}}^{\eta}$ is similar, except for the fact that it is extensional. Note that equating all $\lambda$ -terms without a $\beta$ -normal form gives rise to an inconsistent $\lambda$ -theory, but in the context of $\lambda{\sf I}$ -calculus it is consistent and arises naturally: all “proper” denotational models of the $\lambda{\sf I}$ -calculus induce either $\mathcal{H}_{{\sf I}}$ or $\mathcal{H}_{{\sf I}}^{\eta}$ [25]. This is somewhat disappointing, since models and theories are most valuable when they capture non-trivial operational properties of programs, and normalization is relatively elementary in this setting. In this paper we are going to introduce a new (proper) $\lambda{\sf I}$ -theory, induced by a notion of evaluation trees inspired by Böhm trees, but explicitly designed for $\lambda{\sf I}$ -terms.

Böhm trees and Taylor expansion for the $\lambda{\sf I}$ -calculus

An important feature of Böhm trees is that, because of their coinductive nature, they are capable of pushing some subterms into infinity. Consider for instance a $\lambda{\sf I}$ -term $M$ satisfying

Mxf\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}f(Mxf)% \mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}f(f(Mxf))% \mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}f(f(f(Mxf)))% \mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}f^{n}(Mxf)% \mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}\cdots

then the Böhm tree of $M x f$ is the “limit” of this infinite reduction: $f^{\omega}=f(f(f(\cdots)))$ . Observe that $x$ is “persistent” in the sense that it is never erased along any finite reduction, but is forgotten at the limit. We say that $x$ is pushed into infinity in the Böhm tree of $M x f$ . To some extent, also the variable $f$ is pushed into infinity, but it occurs infinitely often in $f^{\omega}$ . The variable $x$ can also disappear because it is hidden behind a meaningless term like ${\sf\Omega}$ . For instance, the Böhm tree of the $\lambda{\sf I}$ -term $N={\sf\Omega}x$ is just $\bot$ and we say that $x$ is left behind.

As a consequence there are $\lambda{\sf I}$ -terms, like $\lambda xf.M$ and $\lambda xy.y({\sf\Omega}x)$ , whose Böhm tree is not a $\lambda{\sf I}$ -tree [4, Def. 10.1.26] since the variable $x$ is abstracted, but does not appear in the tree. This shows that Böhm trees are not well-suited for the $\lambda{\sf I}$ -calculus, and the question of whether other notions of trees can model $\lambda{\sf I}$ -terms in a more faithful way naturally arises.

In this paper we introduce a notion of Böhm trees keeping tracks of the variables persistently occurring along each possibly infinite path, or left behind a meaningless subterm. We call them Ohana trees as they remember all the variables present in the terms generating them, even if these variables are never actually used in their evaluations. This is obtained by simply annotating such variables on the branches of the Böhm tree, and on its $\bot$ -nodes, but bares interesting consequences: since Ohana trees are invariant under $\beta$ -conversion, showing that two terms have distinct Ohana trees becomes a way of separating them modulo $=_{\beta}$ .

Once the coinductive definition of Ohana trees is given (Definition 10), we develop the corresponding theory of program approximation based on finite trees. Perhaps surprisingly, in the finite approximants, the only variable annotations that are actually required are those on the constant $\bot$ , as all other labels can be reconstructed when taking their supremum. Our main result in this setting is the Approximation Theorem 20 stating that the Ohana tree of a $\lambda{\sf I}$ -term is uniquely determined by the (directed) set of all its finite approximants.

Inspired by quantitative semantics of linear logics, Ehrhard and Regnier proposed a theory of program approximation for regular $\lambda$ -terms based on Taylor expansion [19, 21]. A $\lambda$ -term is approximated by a possibly infinite power-series of programs living in a completely linear resource calculus, where no resource can be duplicated or erased along the computation. This theory is linked to Böhm trees by a Commutation Theorem [20] stating that the normal form of the Taylor expansion of a $\lambda$ -term is equal to the Taylor expansion of its Böhm tree.

The second part of our paper is devoted to explore the question of whether it is possible to define a Taylor expansion for the $\lambda{\sf I}$ -calculus capturing the Ohana tree equality. In Section 4 we design a $\lambda{\sf I}$ -resource calculus with memory, mixing linear and non-linear features. Our terms are either applied to non-empty bags (finite multiset) of non-duplicable resources, or to an empty bag $1_{X}$ annotated with a set $X$ of variables (the non-linear parts of the terms). The reduction of a resource term $t$ preserves its free variables $\mathrm{fv}(t)$ : if the reduction is valid then $t$ consumes all its linear resources and each variable is recorded in some labels, otherwise an exception is thrown and $t$ reduces to an empty program $\mathbf{0}_{X}$ , where $X=\mathrm{fv}(t)$ .

First we prove that the resource calculus so-obtained is confluent and strongly normalizing, then we use it as the target language of a Taylor expansion with memory, capable of approximating both $\lambda{\sf I}$ -terms and Ohana trees. Our main result is that the Commutation Theorem from [20] extends to this setting: the normal form of the Taylor expansion with memory of a $\lambda{\sf I}$ -term always exists and is equal to the Taylor expansion with memory of its Ohana tree (Theorem 38). As consequences (Corollaries 44 and 45), we obtain that: 1) The equality induced on $\lambda{\sf I}$ -terms by Ohana trees coincides with the equality induced by the normalized Taylor expansion with memory; 2) The equality induced by Ohana trees is compatible with application and abstraction, in the sense of the $\lambda{\sf I}$ -calculus, and it is therefore a $\lambda{\sf I}$ -theory. We consider this work a first step in a broader line of research, which we discuss further in the conclusion of the paper. In particular, we aim to extend our formalism to the full $\lambda$ -calculus and explore its applicability to other kinds of trees.

Related works

On the syntactic side, the $\lambda{\sf I}$ -calculus can be translated into MELL proofnets without weakening studied in [15, 16]. Our Ohana trees can be presented as labelled Böhm trees, and therefore share similarities with Melliès”s (infinitary) $\lambda$ -terms “with boundaries”, whose branches are annotated by booleans [36]. However, our labels are describing additional points occurring at transfinite positions, a phenomenon reminiscent of the non-monotonic pre-fixed point construction defined in [6]. They can also be seen as an instances of the transfinite terms considered in [30], but simpler, because no reduction is performed at transfinite positions. Thus, Ohana trees should correspond to normal forms of an infinitary labelled $\lambda{\sf I}$ -calculus, just like Böhm trees are the normal forms of the infinitary $\lambda$ -calculus [29]. We wonder whether a clever translation of the $\lambda{\sf I}$ -calculus into the process calculus in [17] would allow us to retrieve the Ohana trees and the associated Taylor expansion, in which case our Commutation Theorem might become an instance of their general construction.

Concerning denotational semantics, certain relevant intersection type systems [44, 24, 1] can be used to represent models of the $\lambda{\sf I}$ -calculus, as they describe reflexive objects in the smcc of cpos and strict functions [28]. In [25], the authors show that the model introduced in [18] is fully abstract for the $\lambda{\sf I}$ -theory $\mathcal{H}_{{\sf I}}^{\eta}$ . The results in [16] suggest that the relational semantics, endowed with the comonad of finite non-empty multisets, contains models whose theory is either $\mathcal{H}_{{\sf I}}$ or $\mathcal{H}_{{\sf I}}^{\eta}$ . No filter model or relational graph model can induce the Ohana tree equality, since they equate all $\lambda$ -terms having the same Böhm tree [40, 8]. However, the relational model $\mathcal{E}$ defined in [9] using the comonad of finite multisets with possibly infinite coefficients, gives hope since it separates $M x f$ from $M y f$ , and ${\sf\Omega}x$ from ${\sf\Omega}y$ , when $x\neq y$ . This category appears to be the most promising for finding models capturing Ohana trees.

2 Preliminaries

We recall some basic notions and results concerning the $\lambda$ -calculus, and its fragment without weakening known as the $\lambda{\sf I}$ -calculus. For more information, we refer to Barendregt’s book [4].

2.1 The $\lambda$ -calculus, in a nutshell

Let us fix an infinite set $\mathcal{V}$ of variables. The set $\Lambda$ of $\lambda$ -terms is defined by induction

\Lambda\quad\ni\quad M,N\mathrel{\Coloneqq}x\mid\lambda x.M\mid MN\quad(\text{% for $x\in\mathcal{V}$})

We use parentheses when needed. We assume that application associates on the left, and has higher precedence than abstraction. E.g., $\lambda x.\lambda y.\lambda z.xyz$ stands for $\lambda x.(\lambda y.(\lambda z.(xy)z))$ . We write $\lambda x_{1}\ldots x_{n}.M$ or even $\lambda\vec{x}.M$ for $\lambda x_{1}.\ldots\lambda x_{n}.M$ , and $N^{n}(M)$ for $N(N(\cdots N(M)\cdots))$ , where $N$ occurs $n$ times. In particular, when $n=0$ , we get $\lambda\vec{x}.M=N^{n}(M)=M$ .

The set $\mathrm{fv}(M)$ of free variables of $M$ is defined as usual, and we say that $M$ is closed whenever $\mathrm{fv}(M)=\varnothing$ . Hereafter, $\lambda$ -terms are considered modulo $\alpha$ -conversion (see [4, §2.1]).

Example 1.

The $\lambda$ -terms below are used throughout the paper to construct examples:

{\sf I}\coloneqq\lambda x.x,\quad{\sf K}\coloneqq\lambda xy.x,\quad{\sf F}% \coloneqq\lambda xy.y,\quad{\sf B}\coloneqq\lambda fgx.f(g(x)),\quad{\sf D}% \coloneqq\lambda x.xx,\quad{\sf\Omega}\coloneqq{\sf DD}.

The $\lambda$ -term ${\sf I}$ is the identity, ${\sf K,F}$ are the projections, ${\sf B}$ is the composition, ${\sf D}$ is the diagonal and ${\sf\Omega}$ a looping term. The pairing of $M, N$ is encoded as $[M,N]\coloneqq\lambda x.xMN$ , for $x$ fresh.

The $\beta$ -reduction $\to_{\beta}$ is generated by the rule $(\lambda x.M)N\to M[N/x]$ , where $(\lambda x.M)N$ is called a $\beta$ -redex and $M[N/x]$ stands for the capture-free substitution of $N$ for all free occurrences of $x$ in $M$ . We let $\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}$ (resp. $=_{\beta}$ ) be the reflexive-transitive (and symmetric) closure of $\to_{\beta}$ . We say that $M$ is in $\beta$ -normal form ( $\beta$ -nf) if $M$ does not contain any $\beta$ -redex, and that $M$ has a $\beta$ -nf if $M\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}N$ , for some $N$ in $\beta$ -nf. Since $\rightarrow_{\beta}$ is confluent, such $N$ must be unique.

$\blacktriangleright$ Remark 2.

Any $\lambda$ -term $M$ can be written in one of the following forms: either $M=\lambda\vec{x}.yM_{1}\cdots M_{k}$ , in which case $M$ is called a head normal form (hnf) and $y$ its head variable; or $M=\lambda\vec{x}.(\lambda y.P)QM_{1}\cdots M_{k}$ , where $(\lambda y.P)Q$ is referred to as its head redex.

The head reduction $\rightarrow_{h}$ is the restriction of $\rightarrow_{\beta}$ obtained by contracting the head redex.

Definition 3.

A $\lambda$ -term $Y$ is a fixed-point combinator (fpc) if it satisfies $Yx=_{\beta}x(Yx)$ .

Notice that we do not require that fixed-point combinators are closed $\lambda$ -terms. We recall Curry’s combinator ${\sf Y}$ and define, for all $l\in\mathcal{V}$ , Polonsky’s $\Theta_{l}$ and Klop’s $\text{\scalebox{0.8}{\faBible}}_{\,l}$ [35]:

{\sf D}_{f}\coloneqq\lambda x.f(xx),\quad{\sf Y}\coloneqq\lambda f.{\sf D}_{f}% {\sf D}_{f},\quad{\sf V}\coloneqq\lambda vlf.f(vvlf),\quad\Theta_{l}\coloneqq{% \sf VV}l,\quad\text{\scalebox{0.8}{\faBible}}_{\,l}\coloneqq\lambda e.{\sf BYB% }el.

(1)

It is easy to check that ${\sf Y}$ and $\Theta_{l}$ are fpcs. Regarding the Bible $\text{\scalebox{0.8}{\faBible}}_{\,l}$ , which owes its name to its distinctive spelling, we get $\text{\scalebox{0.8}{\faBible}}_{\,l}x=_{\beta}{\sf BYB}xl=_{\beta}{\sf Y}({% \sf B}x)l=_{\beta}{\sf B}x({\sf Y}({\sf B}x))l=_{\beta}x({\sf Y}({\sf B}x)l)=_% {\beta}x(\text{\scalebox{0.8}{\faBible}}_{\,l}x)$ . Note that the variable $l$ remains in a passive position along the reduction of $\text{\scalebox{0.8}{\faBible}}_{\,l}$ (and of $\Theta_{l}$ ), therefore $\text{\scalebox{0.8}{\faBible}}_{\,N}:=\text{\scalebox{0.8}{\faBible}}_{\,l}[N% /l]$ (resp. $\Theta_{N}:=\Theta_{l}[N/l]$ ) remains a fpc, for all $N\in\Lambda$ .

Although fpcs $Y$ are not $\beta$ -normalizable, they differ from ${\sf\Omega}$ since they produce increasing stable amounts of information along reduction: $Y\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}\lambda f.fY_{% 1}\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}\lambda f.f^{% n}(Y_{n})\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}\cdots$ . Barendregt introduced a notion of “evaluation tree” to capture this infinitary behaviour [3].

Definition 4.

The Böhm tree $\mathrm{BT}(M)$ of a $\lambda$ -term $M$ is coinductively defined as follows.

1.

If $M$ has a hnf, that is $M\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{h}\lambda x_{1}\dots x% _{n}.yM_{1}\cdots M_{k}$ , then
2.

$\mathrm{BT}(M)\coloneqq\bot$ , otherwise. The constant $\bot$ represents the absolute lack of information.

Example 5.

Using the terms from Example 1 and (1), let us construct some Böhm trees.

(i)

If $M$ has a $\beta$ -normal form $N$ then, up to isomorphism, $\mathrm{BT}(M)=N$ . E.g., $\mathrm{BT}({\sf DI})={\sf I}$ .
(ii)

Since ${\sf\Omega}$ and ${\sf YK}$ have no hnf, we get $\mathrm{BT}({\sf\Omega})=\mathrm{BT}({\sf YK})=\bot$ .
(iii)

If $Y$ is an fpc, then $\mathrm{BT}(Y)=\lambda f.f(f(f(\cdots)))$ . Thus, $\mathrm{BT}({\sf Y})=\mathrm{BT}(\text{\scalebox{0.8}{\faBible}}_{\,l})=% \mathrm{BT}(\Theta_{l})$ .
(iv)

Using the fpc ${\sf Y}$ , one can define $\lambda$ -terms ${\sf E}_{x},{\sf O}_{x}$ satisfying ${\sf E}_{x}=_{\beta}{[}{\sf\Omega},[{\sf\Omega}x,{\sf E}_{x}]]$ and ${\sf O}_{x}=_{\beta}{[}{\sf\Omega}x,[{\sf\Omega},{\sf O}_{x}]]$ . These two $\lambda$ -terms both construct a “stream” $[M_{1},[M_{2},[M_{3},[\cdots]]]]$ , but the former places ${\sf\Omega}x$ at even positions and ${\sf\Omega}$ at odd ones, while the latter does the converse. This difference is however forgotten in their Böhm trees:

$\mathrm{BT}({\sf E}_{x})=\mathrm{BT}({\sf O}_{x})=[\bot,[\bot,[\bot,[\bot,[\,% \cdots]]]]]\hfill\textrm{ (inline depiction of a tree)}$
(v)

Check that, given ${\sf R}=\lambda ylx.x(y(xl))$ , we have $\mathrm{BT}({\sf YR}l)=\lambda x_{0}.x_{0}(\lambda x_{1}.x_{1}(\lambda x_{2}.x% _{2}(\cdots)))$ .

The Böhm tree equality induces an equivalence on $\lambda$ -terms: $M=_{\mathcal{B}}N$ iff $\mathrm{BT}(M)=\mathrm{BT}(N)$ . As shown in [31, 48], $\mathcal{B}$ is a $\lambda$ -theory because it contains $=_{\beta}$ and is compatible with abstraction and application: $M=_{\mathcal{B}}M^{\prime}$ entails $\lambda x.M=_{\mathcal{B}}\lambda x.M^{\prime}$ , $MN=_{\mathcal{B}}M^{\prime}N$ and $NM=_{\mathcal{B}}NM^{\prime}$ .

2.2 The $\lambda{\sf I}$ -calculus

The set $\Lambda_{\sf I}$ of $\lambda{\sf I}$ -terms is the subset of $\Lambda$ consisting of those $\lambda$ -terms in which every abstraction binds at least one occurrence of the abstracted variable. Note that $\rightarrow_{\beta}$ induces a reduction on $\Lambda_{\sf I}$ since $M\in\Lambda_{\sf I}$ and $M\rightarrow_{\beta}N$ entail $N\in\Lambda_{\sf I}$ . In other words, the property of being a $\lambda{\sf I}$ -term is preserved by $\rightarrow_{\beta}$ . Similarly, the $\lambda{\sf I}$ -calculus inherits from $\lambda$ -calculus all the notions previously defined like head reduction, Böhm trees, etc. For convenience, we consider an alternative definition of $\Lambda_{\sf I}$ simultaneously defining $\lambda{\sf I}$ -terms and their sets of free variables.

Definition 6.

(i)

For all $X\subseteq\mathcal{V}$ , $\Lambda_{\sf I}(X)$ is defined as the smallest subset of $\Lambda$ such that:

$x\in\Lambda_{\sf I}(\{x\})\qquad\lambda x.M\in\Lambda_{\sf I}(X-\{x\})M\in% \Lambda_{\sf I}(X)\quad x\in X\qquad MN\in\Lambda_{\sf I}(X\cup Y)% \lx@proof@logical@and M\in\Lambda_{\sf I}(X)N\in\Lambda_{\sf I}(Y)$
(ii)

Finally, the set of all $\lambda{\sf I}$ -terms is given by the disjoint union $\Lambda_{\sf I}=\coprod_{X\subseteq\mathcal{V}}\Lambda_{\sf I}(X)$ .

$\blacktriangleright$ Remark 7.

(i)

Note that $M\in\Lambda_{\sf I}(X)$ means that $M$ is a $\lambda{\sf I}$ -term such that $\mathrm{fv}{(M)}=X$ . As a consequence, if $M\in\Lambda_{\sf I}(X)$ then the set $X$ must be finite.
(ii)

Each set $\Lambda_{\sf I}(X)$ is closed under $\beta$ -conversion.
(iii)

Our examples ${\sf I},{\sf B},{\sf D},{\sf\Omega},{\sf Y},\text{\scalebox{0.8}{\faBible}}_{% \,l},\Theta_{l},{\sf E}_{x},{\sf O}_{x},{\sf YR}l$ are $\lambda{\sf I}$ -terms, while ${\sf K},{\sf F},{\sf YK}\notin\Lambda_{\sf I}$ .

Definition 8.

A $\lambda{\sf I}$ -theory $\mathcal{T}$ is given by an equivalence $\mathord{=_{\mathcal{T}}}\subseteq\Lambda_{\sf I}^{2}$ containing $\beta$ -conversion and compatible with application and abstraction. In the context of $\lambda{\sf I}$ -calculus, the compatibility with abstraction becomes: $M=_{\mathcal{T}}M^{\prime}$ and $x\in\mathrm{fv}(M)\cap\mathrm{fv}(M^{\prime})$ imply $\lambda x.M=_{\mathcal{T}}\lambda x.M^{\prime}$ .

The only subtlety in the definition above stands in the side condition on the compatibility with abstraction. However, this small difference has significant consequences: e.g., the theory axiomatized by equating all terms without a $\beta$ -nf is consistent as a $\lambda{\sf I}$ -theory, but inconsistent as a $\lambda$ -theory. The following theorem collects the main properties of the $\lambda{\sf I}$ -calculus.

Theorem 9.

(i)

Every computable numerical function is $\lambda{\sf I}$ -definable [4, Thm. 9.2.16].
(ii)

Strong and weak $\beta$ -normalization coincide for the $\lambda{\sf I}$ -calculus [4, Thm. 11.3.4].
(iii)

Every $\lambda$ -theory is also a $\lambda{\sf I}$ -theory, while the converse does not hold.

By (iii), Böhm trees induce a $\lambda{\sf I}$ -theory, but we argue that this theory does not respect the spirit of $\Lambda_{\sf I}$ . E.g., the variable $l$ is never erased along the reduction of, say, $\text{\scalebox{0.8}{\faBible}}_{\,l}$ , but it disappears in its Böhm tree. Using the terminology of [4], one says that $l$ is pushed to infinity in $\mathrm{BT}(\text{\scalebox{0.8}{\faBible}}_{\,l})$ . This shows that the Böhm tree of the $\lambda{\sf I}$ -term $\lambda l.\text{\scalebox{0.8}{\faBible}}_{\,l}\in\Lambda_{\sf I}$ is not a $\lambda{\sf I}$ -tree: the outer $\lambda$ -abstraction “ $\lambda l$ ” does not bind any free occurrence of $l$ in $\mathrm{BT}(\text{\scalebox{0.8}{\faBible}}_{\,l})=\lambda f.f(f(f(\,\cdots)))$ .

3 Ohana trees

Figure 1: Examples of Ohana trees of

\lambda{\sf I}

-terms.

We have seen that Böhm trees are not well-suited for representing $\lambda{\sf I}$ -terms faithfully, because variables that are never erased along the reduction are forgotten (i.e., pushed into infinity). We now introduce a notion of evaluation tree that records all variables that are pushed along each path, ensuring that none are forgotten, whether they remain in passive position or not.

3.1 The coinductive definition

For every finite set $X\subseteq\mathcal{V}$ , written $X\subseteq_{\mathrm{f}}\mathcal{V}$ , we introduce a constant $\bot_{X}$ representing any looping $M\in\Lambda_{\sf I}(X)$ . Intuitively, the Ohana tree of a $\lambda{\sf I}$ -term $M$ is obtained from $\mathrm{BT}(M)$ by annotating each subtree (also $\bot$ ) with the free variables of the $\lambda$ -term that generated it.

Definition 10.

The Ohana tree of a term $M\in\Lambda_{\sf I}(X)$ is coinductively defined as follows:

(i)

If $M\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{h}\lambda x_{1}\dots x% _{n}.yM_{1}\cdots M_{k}$ with $y\in X\cup\{\vec{x}\}$ , $M_{i}\in\Lambda_{\sf I}(X_{i})$ (for $1\leq i\leq k$ ), then
(ii)

$\mathrm{OT}(M)\coloneqq\bot_{X}$ , otherwise. Recall that $X=\mathrm{fv}(M)$ , since $M\in\Lambda_{\sf I}(X)$ .

We sometimes use an inline presentation of Ohana trees, by introducing application symbols annotated with the sets $X_{i}$ , as in $\lambda x_{1}\ldots x_{n}.y\cdot^{X_{1}}T_{1}\cdots^{X_{k}}T_{k}$ .

Example 11.

(i)

$\mathrm{OT}({\sf I})=\lambda x.x$ , $\mathrm{OT}({\sf D})=\lambda x.x\cdot^{\{x\}}x$ , $\mathrm{OT}({\sf B})=\lambda fgx.f\cdot^{\{g,x\}}(g\cdot^{\{x\}}x)$ .
(ii)

$\mathrm{OT}({\sf\Omega})=\mathrm{OT}(\lambda y.{\sf\Omega}y)=\bot_{\varnothing}$ , $\mathrm{OT}({\sf\Omega}x)=\bot_{\{x\}}$ . More generally: $\mathrm{OT}({\sf\Omega}\vec{x})=\bot_{\{x_{1},\dots,x_{n}\}}$ .
(iii)

$\mathrm{OT}({\sf Y})=\lambda f.f\cdot^{\{f\}}(f\cdot^{\{f\}}(f\cdot^{\{f\}}(\,% \cdots)))$ . In fact, it is easy to check that for all closed fpcs $Y\in\Lambda_{\sf I}$ , we have $\mathrm{OT}(Y)=\mathrm{OT}({\sf Y})\cong\mathrm{BT}({\sf Y})$ .
(iv)

In $\mathrm{OT}(\text{\scalebox{0.8}{\faBible}}_{\,l})$ the variable $l$ which is pushed into infinity becomes visible: $\mathrm{OT}(\text{\scalebox{0.8}{\faBible}}_{\,l})=\mathrm{OT}(\Theta_{l})=% \lambda f.f\cdot^{\{f,l\}}(f\cdot^{\{f,l\}}(f\cdot^{\{f,l\}}(\,\cdots)))$ . Thus $\mathrm{OT}(\text{\scalebox{0.8}{\faBible}}_{\,l})\neq\mathrm{OT}(\Theta_{x})$ when $x\neq l$ .

Other examples of Ohana trees are depicted in Figure 1. Note that the Ohana trees of ${\sf E}_{x}$ and ${\sf O}_{x}$ are now distinguished. The interest of ${{\sf YR}l}$ is that it pushes into infinity an increasing amount of variables:

{\sf YR}l=_{\beta}\lambda x_{0}.x_{0}(({\sf YR})(x_{0}l))=_{\beta}\lambda x_{0% }.x_{0}(\lambda x_{1}.x_{1}(({\sf YR})(x_{1}(x_{0}l))))\,{=_{\beta}}\cdots

So – at the limit – infinitely many variables are pushed into infinity (but only $l$ is free).

$\blacktriangleright$ Remark 12.

If $M\in\Lambda_{\sf I}$ has a $\beta$ -nf $N$ , then there is an isomorphism $\mathrm{OT}(M)\cong N$ . In fact, since $N$ is finite, it is possible to reconstruct all the labels in $\mathrm{OT}(M)$ .

We are going to show that Ohana trees are invariant under $\beta$ -reduction (Prop. 19 plus Thm. 20), and that the equality induced on $\lambda{\sf I}$ -terms is a $\lambda{\sf I}$ -theory (Corollary 45).

3.2 The associated approximation theory

We introduce a theory of program approximation that captures Ohana trees, by adapting the well-established approach originally developed for Böhm trees [31, 48] (see also [4, Ch. 14]). We start by defining the approximants with memory, corresponding to finite Ohana trees.

Definition 13.

(i)

The set of approximants with memory is $\mathcal{A}_{\mathsf{m}}\coloneqq\coprod_{X\subseteq_{\mathrm{f}}\mathcal{V}}% \mathcal{A}_{\mathsf{m}}(X)$ , where $\mathcal{A}_{\mathsf{m}}(X)$ is defined by (for $A_{i}\in\mathcal{A}_{\mathsf{m}}(X_{i})$ , $X_{i}\subseteq X$ , $y\in X\cup\{\vec{x}\}$ and $\vec{x}\in\bigcup_{i=1}^{k}X_{i}$ ):

$\mathcal{A}_{\mathsf{m}}(X)\quad\ni\quad A\mathrel{\Coloneqq}\bot_{X}\mid% \lambda x_{1}\ldots x_{n}.yA_{1}\cdots A_{k}$

(ii)

We define $\mathord{\sqsubseteq}\subseteq\mathcal{A}_{\mathsf{m}}^{2}$ as the least partial order closed under the following rules:

\bot_{X}\sqsubseteq AA\in\mathcal{A}_{\mathsf{m}}(X)\qquad\lambda x_{1}\dots x% _{n}.y\,A_{1}\cdots A_{k}\sqsubseteq\lambda x_{1}\dots x_{n}.y\,A^{\prime}_{1}% \cdots A^{\prime}_{k}\lx@proof@logical@and A_{i}\sqsubseteq A^{\prime}_{i}A_{i% },A^{\prime}_{i}\in\mathcal{A}_{\mathsf{m}}(X_{i})\textrm{for all }1\leq i\leq k% \vec{x}\in\{y\}\cup\big{(}\bigcup_{i=1}^{k}X_{i}\big{)}

Each $(\mathcal{A}_{\mathsf{m}}(X),\sqsubseteq)$ is a pointed poset (partially ordered set) with bottom element $\bot_{X}$ , while the poset $(\mathcal{A}_{\mathsf{m}},\sqsubseteq)$ is not pointed because it has countably many minimal elements. Note that we do not annotate the application symbols in $A\in\mathcal{A}_{\mathsf{m}}$ with the sets of variables $X_{i}$ , since the labels in its $\bot$ -nodes carry enough information to reconstruct the finite Ohana tree associated with $A$ .

Lemma 14.

There is a bijection between $\mathcal{A}_{\mathsf{m}}$ and the set of finite Ohana trees of $\lambda{\sf I}$ -terms.

We now give the recipe to compute the set of approximants with memory of a $\lambda{\sf I}$ -term.

Definition 15.

(i)

The direct approximant of $M\in\Lambda_{\sf I}(X)$ is given by:

$\omega_{\mathsf{m}}(M)\coloneqq\begin{cases}\lambda x_{1}\ldots x_{n}.y\,% \omega_{\mathsf{m}}(M_{1})\cdots\omega_{\mathsf{m}}(M_{k}),&\textrm{if }M=% \lambda x_{1}\ldots x_{n}.yM_{1}\cdots M_{k},\\ \bot_{X},&\textrm{otherwise.}\end{cases}$
(ii)

The set $\mathrm{App}_{\mathsf{m}}(M)$ of approximants with memory of $M\in\Lambda_{\sf I}$ is defined by:

$\mathrm{App}_{\mathsf{m}}(M)\coloneqq\{A\in\mathcal{A}_{\mathsf{m}}\mid\exists N% \in\Lambda_{\sf I}\,.\,M\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow% }_{\beta}N\textrm{ and }A\sqsubseteq\omega_{\mathsf{m}}(N)\}$

$\blacktriangleright$ Remark 16.

For all $M\in\Lambda_{\sf I}(X)$ , we have $\omega_{\mathsf{m}}(M)\in\mathcal{A}_{\mathsf{m}}(X)$ and $\mathrm{App}_{\mathsf{m}}(M)\subseteq\mathcal{A}_{\mathsf{m}}(X)$ .

Example 17.

(i)

$\mathrm{App}_{\mathsf{m}}({\sf D})=\{\bot_{\varnothing},\lambda x.x\bot_{\{x\}% },{\sf D}\}$ , $\mathrm{App}_{\mathsf{m}}({\sf\Omega})=\{\bot_{\varnothing}\}$ .
(ii)

$\mathrm{App}_{\mathsf{m}}({\sf Y})=\{\bot_{\varnothing}\}\cup\{\lambda f.f^{n}% (\bot_{\{f\}})\mid n\in\mathbb{N}\}$ .
(iii)

$\mathrm{App}_{\mathsf{m}}(\text{\scalebox{0.8}{\faBible}}_{\,l})=\{\bot_{\{l\}% }\}\cup\{\lambda f.f^{n}(\bot_{\{f,l\}})\mid n\in\mathbb{N}\}$ .
(iv)

$\mathrm{App}_{\mathsf{m}}({\sf YR}l)=\{\bot_{\{l\}},\lambda x_{0}.x_{0}(\bot_{% \{x_{0},l\}}),\lambda x_{0}.x_{0}(\lambda x_{1}.x_{1}(\bot_{\{x_{0},x_{1},l\}}% )),\dots\}$ .

Lemma 18.

(i)

For every $M,N\in\Lambda_{\sf I}$ , $M\rightarrow_{\beta}N$ entails $\omega_{\mathsf{m}}(M)\sqsubseteq\omega_{\mathsf{m}}(N)$ .
(ii)
For all $M\in\Lambda_{\sf I}(X)$ , $\mathrm{App}_{\mathsf{m}}(M)$ is an ideal of the poset $(\mathcal{A}_{\mathsf{m}}(X),\sqsubseteq)$ . More precisely:
1. (a)
  
  non-emptiness: $\bot_{X}\in\mathrm{App}_{\mathsf{m}}(M)$ ;
2. (b)
  
  downward closure: $A\in\mathrm{App}_{\mathsf{m}}(M)$ and $A^{\prime}\sqsubseteq A$ imply $A^{\prime}\in\mathrm{App}_{\mathsf{m}}(M)$ ;
3. (c)
  
  directedness: $\forall A_{1},A_{2}\in\mathrm{App}_{\mathsf{m}}(M),\exists A_{3}\in\mathrm{App% }_{\mathsf{m}}(M)$ such that $A_{1}\sqsubseteq A_{3}\sqsupseteq A_{2}$ .

Proof.

(i)

By an easy induction on the structure of $M\in\Lambda_{\sf I}(X)$ , using Remarks 2 and 7.
(ii)

(a) and (b) are trivial. For (c), define $\sqcup$ by setting: $\bot_{X}\sqcup A=A\sqcup\bot_{X}=A$ , $x\sqcup x=x$ , if $A_{1},A^{\prime}_{1}$ and $A_{2},A^{\prime}_{2}$ are compatible, then $(\lambda x.A_{1})\sqcup(\lambda x.A^{\prime}_{1})=\lambda x.(A_{1}\sqcup A^{% \prime}_{1})$ and $A_{1}A_{2}\sqcup A^{\prime}_{1}A^{\prime}_{2}=(A_{1}\sqcup A^{\prime}_{1})(A_{% 2}\sqcup A^{\prime}_{2})$ . Check that $A_{3}=A_{1}\sqcup A_{2}$ is their supremum.

$\hfill\blacktriangleleft$

The next result shows that $\beta$ -convertible terms share the same the set of approximants.

Proposition 19.

Let $M,N\in\Lambda_{\sf I}(X)$ . If $M\rightarrow_{\beta}N$ , then $\mathrm{App}_{\mathsf{m}}(M)=\mathrm{App}_{\mathsf{m}}(N)$ .

Proof.

By confluence of $\rightarrow_{\beta}$ , using Lemma 18(i). $\hfill\blacktriangleleft$

Theorem 20.

There is a bijection ${\cal A}(\cdot)$ between the set of Ohana trees and the set of approximants of $\lambda{\sf I}$ -terms satisfying ${\cal A}(\mathrm{OT}(M))=\mathrm{App}_{\mathsf{m}}(M)$ , for all $M\in\Lambda_{\sf I}$ .

Proof.

From $\mathrm{OT}(M)$ to $\mathrm{App}_{\mathsf{m}}(M)$ . Let $\mathrm{OT}(M)^{\star}$ be the set of all finite subtrees of $\mathrm{OT}(M)$ , where each truncated subtree $T$ is replaced by $\bot_{\mathrm{fv}(T)}$ . By Lemma 14, $\mathrm{OT}(M)^{\star}\cong\mathrm{App}_{\mathsf{m}}(M)$ .

From $\mathrm{App}_{\mathsf{m}}(M)$ to $\mathrm{OT}(M)$ . For every finite path $\sigma$ in $\mathrm{OT}(M)$ , there is an $A\in\mathrm{App}_{\mathsf{m}}(M)$ representing $\mathrm{OT}(M)$ along $\sigma$ . Conclude since $\mathrm{OT}(M)$ is the supremum of all such $\sigma$ . $\hfill\blacktriangleleft$

4 A resource calculus with memory

In this section we introduce the $\lambda{\sf I}$ -resource calculus refining the (finite) resource calculus [19], best known as the target language of Ehrhard and Regnier’s Taylor expansion [21]. So, the resource calculus is not meant to be a stand-alone language, but rather another theory of approximations for the $\lambda$ -calculus. Before going further, we recall its main properties.

We consider here the promotion-free fragment of the resource calculus introduced in [39]. Its syntax is similar to the $\lambda$ -calculus, except for the applications that are of shape $s\bar{t}$ , where $\bar{t}=[t_{1},\dots,t_{n}]$ is a multiset of resources called bag. The resources populating $\bar{t}$ are linear as they cannot be erased or copied by $s$ , they must be used exactly once along the reduction. When contracting a term of the form $s=(\lambda x.s^{\prime})[t_{1},\dots,t_{n}]$ there are two possibilities.

1.

If the number of occurrences of $x$ in $s^{\prime}$ is exactly $n$ , then each occurrence is substituted by a different $t_{i}$ . Since the elements in the bag are unordered, there is no canonical bijection between the resources and the occurrences of $x$ . The solution consists in collecting all possibilities in a formal sum of terms, the sum representing an inner-choice operator.
2.

If there is a mismatch between the number of occurrences and the amount of resources, then $s$ reduces to the empty-sum, $\mathbf{0}$ . From a programming-language perspective, this can be thought of as a program terminating abruptly after throwing an uncaught exception.

The first-class citizens of the resource calculus are therefore finite sums of resource terms, that are needed to ensure the (strong) confluence of reductions. Another important property is strong normalization, that follows from the fact that no resource can be duplicated.

4.1 $\lambda{\sf I}$ -resource expressions and $\lambda{\sf I}$ -resource sums

Our version of the resource calculus is extended with labels representing the memory of free variables that were present in the $\lambda{\sf I}$ -term they approximate. Just like in Definition 13(i) we endowed the constant $\bot$ with a finite set $X$ of variables, here we annotate:

$\blacksquare$

the empty bag $1$ of resource terms, since an empty bag of approximants of $M$ should remember the free variables of $M$ ;
$\blacksquare$

the empty sum $\mathbf{0}$ of resource terms. Indeed, if a resource term vanishes during reduction because of the mismatch described above, its free variables should be remembered.

Definition 21.

(i)

For all $X\subseteq_{\mathrm{f}}\mathcal{V}$ , the sets $\mathord{\Delta_{{\sf I}}}(X)$ and $\mathord{!\Delta_{{\sf I}}}(X)$ are defined by induction:

	$\displaystyle x\in\mathord{\Delta_{{\sf I}}}(\{x\})\qquad\lambda x.s\in% \mathord{\Delta_{{\sf I}}}(X-\{x\})\lx@proof@logical@and s\in\mathord{\Delta_{% {\sf I}}}(X)x\in X\qquad s\bar{t}\in\mathord{\Delta_{{\sf I}}}(X\cup Y)% \lx@proof@logical@and s\in\mathord{\Delta_{{\sf I}}}(X)\bar{t}\in\mathord{!% \Delta_{{\sf I}}}(Y)$
	$\displaystyle 1_{X}\in\mathord{!\Delta_{{\sf I}}}(X)\qquad[t_{0},\dots,t_{n}]% \in\mathord{!\Delta_{{\sf I}}}(X)\lx@proof@logical@and t_{0}\in\mathord{\Delta% _{{\sf I}}}(X)\cdots t_{n}\in\mathord{\Delta_{{\sf I}}}(X)$

(ii)

The set $\mathord{\Delta_{{\sf I}}}$ of $\lambda{\sf I}$ -resource terms and the set $\mathord{!\Delta_{{\sf I}}}$ of bags are given by:

$\mathord{\Delta_{{\sf I}}}\coloneqq\coprod_{X\subseteq_{\mathrm{f}}\mathcal{V}% }\mathord{\Delta_{{\sf I}}}(X)\quad\text{and}\quad\mathord{!\Delta_{{\sf I}}}% \coloneqq\coprod_{X\subseteq_{\mathrm{f}}\mathcal{V}}\mathord{!\Delta_{{\sf I}% }}(X).$

As a matter of notation, we let $\mathord{(!)\Delta_{{\sf I}}}$ denote either $\mathord{\Delta_{{\sf I}}}$ or $\mathord{!\Delta_{{\sf I}}}$ , indistinctly but coherently. We call resource expressions generic elements $s,t\in\mathord{(!)\Delta_{{\sf I}}}$ . We denote the union of two bags $\bar{t},\bar{u}\in\mathord{!\Delta_{{\sf I}}}(X)$ multiplicatively by $\bar{t}\cdot\bar{u}$ , whose neutral element is the empty bag, $1_{X}$ .

$\blacktriangleright$ Remark 22.

(i)

In every $\lambda{\sf I}$ -resource term of the form $\lambda x.s$ , the variable $x$ must occur freely in $s$ : it may appear in the undecorated underlying term, or in the “memory” $X$ decorating $1_{X}$ . Therefore, it makes sense to define $\mathrm{fv}(s)\coloneqq X$ whenever $s\in\mathord{(!)\Delta_{{\sf I}}}(X)$ .
(ii)

Each set $\mathord{!\Delta_{{\sf I}}}(X)$ is isomorphic to the monoid of multisets of elements of $\mathord{\Delta_{{\sf I}}}(X)$ . Notice that $\mathord{!\Delta_{{\sf I}}}$ is not the set of all bags of elements of $\mathord{\Delta_{{\sf I}}}$ , just its subset of bags whose elements have the same free variables (and so inductively in the subterms).

Example 23.

(i)

The identity ${\sf I}$ belongs to $\mathord{\Delta_{{\sf I}}}$ , whereas the projections do not: ${\sf K},{\sf F}\notin\mathord{\Delta_{{\sf I}}}$ .
(ii)

Note that $\lambda xy.x1_{\varnothing}\notin\mathord{\Delta_{{\sf I}}}$ since $y\notin\mathrm{fv}(x1_{\varnothing})$ , but $\lambda xy.x1_{\{y\}}\in\mathord{\Delta_{{\sf I}}}$ because $y\in\{y\}$ .
(iii)

The terms ${\sf D}_{0}=\lambda x.x1_{\{x\}}$ and ${\sf D}_{n+1}=\lambda x.x[x,\ldots,x]$ , where the bag contains $n+1$ occurrences of $x$ , are $\lambda{\sf I}$ -resource terms. By Remark 22(ii), we obtain:
(iv)

$[x,y]\notin\mathord{!\Delta_{{\sf I}}}$ , while $[x,x[x],x[\lambda y.y,\lambda y.y[y]],(\lambda y.y)[x],\lambda y.y1_{\{x\}}]% \in\mathord{!\Delta_{{\sf I}}}(\{x\})\subseteq\mathord{!\Delta_{{\sf I}}}$ .

We consider resource expressions up to $\alpha$ -equivalence, under the proviso that abstractions bind linear occurrences of variables as well as occurrences in the memory of empty bags. For instance, $\lambda xyz.x1_{\{x\}}1_{\{x,y,z\}}$ and $\lambda x^{\prime}y^{\prime}z.x^{\prime}1_{\{x^{\prime}\}}1_{\{x^{\prime},y^{% \prime},z\}}$ are considered $\alpha$ -equivalent.

Definition 24.

For all $X\subseteq_{\mathrm{f}}\mathcal{V}$ , the set $\mathbb{N}[\mathord{(!)\Delta_{{\sf I}}}(X)]$ of sums of $\lambda{\sf I}$ -resource terms (“resource sums”, for short) is defined as the $\mathbb{N}$ -semimodule of finitely supported formal sums of expressions in $\mathord{(!)\Delta_{{\sf I}}}(X)$ , with coefficients in $\mathbb{N}$ . Explicitly, it can be presented as:

\mathbb{N}[\mathord{(!)\Delta_{{\sf I}}}(X)]\quad\ni\quad\mathbf{s},\mathbf{t}% \mathrel{\Coloneqq}\mathbf{0}_{X}\mid r\mid r+\mathbf{s}\quad(\text{for $r\in% \mathord{(!)\Delta_{{\sf I}}}(X)$})

quotiented by associativity and commutativity of $+$ , as well as neutrality of $\mathbf{0}_{X}$ .

Note that $\mathord{(!)\Delta_{{\sf I}}}(X)\subseteq\mathbb{N}[\mathord{(!)\Delta_{{\sf I% }}}(X)]$ , that is, resource expressions are assimilated to the corresponding one-element sum. The constructors of the calculus are extended to resource sums by (bi)linearity, i.e. for $s\in\mathord{\Delta_{{\sf I}}}(X)$ , $\mathbf{s}\in\mathbb{N}[\mathord{\Delta_{{\sf I}}}(X)]$ , $\bar{t}\in\mathord{!\Delta_{{\sf I}}}(Y)$ , $\bar{\mathbf{t}}\in\mathbb{N}[\mathord{!\Delta_{{\sf I}}}(Y)]$ , $u\in\mathord{\Delta_{{\sf I}}}(Y)$ and $\mathbf{u}\in\mathbb{N}[\mathord{\Delta_{{\sf I}}}(Y)]$ , we have:

\begin{array}[]{llll}(s+\mathbf{s})\bar{t}\coloneqq s\bar{t}+\mathbf{s}\bar{t}% ,&\mathbf{0}_{X}\bar{t}\coloneqq\mathbf{0}_{X\cup Y},&\lambda x.(s+\mathbf{s})% \coloneqq\lambda x.s+\lambda x.\mathbf{s},&\lambda x.\mathbf{0}_{X}\coloneqq% \mathbf{0}_{X-\{x\}},\\[4.30554pt] s(\bar{t}+\bar{\mathbf{t}})\coloneqq s\bar{t}+s\bar{\mathbf{t}},&s\mathbf{0}_{% Y}\coloneqq\mathbf{0}_{X\cup Y},&[u+\mathbf{u}]\cdot\bar{t}\coloneqq[u]\cdot% \bar{t}+[\mathbf{u}]\cdot\bar{t},&[\mathbf{0}_{Y}]\cdot\bar{t}\coloneqq\mathbf% {0}_{Y}.\end{array}

Therefore, if $\mathbf{0}_{X}$ occurs in $s$ not as a summand but as a proper subterm, then $s=\mathbf{0}_{\mathrm{fv}(s)}$ .

4.2 Memory substitution and resource substitution

While the usual finite resource calculus is completely linear, the variables we store in the memory of $1_{X}$ and $\mathbf{0}_{X}$ are not. The memory $X$ remembers the variables present in $X$ not their amounts, this is the reason why it is modelled as a set, not as a multiset. This consideration leads us to define two kinds of substitutions.

The (non-linear) memory substitution of a set $Y\subseteq_{\mathrm{f}}\mathcal{V}$ for a variable $x$ in a $\lambda{\sf I}$ -resource term $s$ does not interact with the linear occurrences of $x$ in $s$ (i.e., they remain unchanged), it just replaces the “memory” of $x$ in the empty bags with the content of $Y$ .

Definition 25.

(i)

For all $X,Y\subseteq_{\mathrm{f}}\mathcal{V}$ and $x\in\mathcal{V}$ , define

$X\left\{Y\middle/x\right\}\coloneqq\begin{cases}X-\{x\}\cup Y,&\text{if $x\in X% $,}\\ X,&\text{otherwise.}\\ \end{cases}$

(ii)

Given $s\in\mathord{(!)\Delta_{{\sf I}}}(X)$ , the memory substitution of $x$ by $Y\subseteq_{\mathrm{f}}\mathcal{V}$ in $s$ is the resource term $s\left\{Y\middle/x\right\}$ defined as follows (for $x\neq y$ and, in the abstraction case, $y\notin Y$ ):

	$\displaystyle x\left\{Y\middle/x\right\}$	$\displaystyle\coloneqq x,$	$\displaystyle 1_{X}\left\{Y\middle/x\right\}$	$\displaystyle\coloneqq 1_{X\left\{Y\middle/x\right\}},$	$\displaystyle(s\bar{t})\left\{Y\middle/x\right\}$	$\displaystyle\coloneqq(s\left\{Y\middle/x\right\})(\bar{t}\left\{Y\middle/x% \right\}),$
	$\displaystyle y\left\{Y\middle/x\right\}$	$\displaystyle\coloneqq y,$	$\displaystyle(\lambda y.s)\left\{Y\middle/x\right\}$	$\displaystyle\coloneqq\lambda y.s\left\{Y\middle/x\right\},$	$\displaystyle([s]\cdot\bar{t})\left\{Y\middle/x\right\}$	$\displaystyle\coloneqq[s\left\{Y\middle/x\right\}]\cdot(\bar{t}\left\{Y\middle% /x\right\}).$

We now define the resource substitution of a bag $\bar{u}$ for $x$ in $s$ , whose effect is twofold. 1) It non-deterministically replaces each linear occurrence of $x$ with a resource from the bag (as usual). 2) It applies the memory substitution of $x$ by $\mathrm{fv}(\bar{u})$ to the resulting sum of terms.

Definition 26.

Given $s\in\mathord{(!)\Delta_{{\sf I}}}(X)$ , $x\in\mathcal{V}$ and $\bar{u}\in\mathord{!\Delta_{{\sf I}}}(Y)$ , the resource substitution of $x$ by $\bar{u}$ in $s$ is the resource sum $s\left\langle\bar{u}\middle/x\right\rangle\in\mathbb{N}[\mathord{(!)\Delta_{{% \sf I}}}(X\left\{Y\middle/x\right\})]$ defined as follows:

$\displaystyle x\left\langle\bar{u}\middle/x\right\rangle$	$\displaystyle\coloneqq\begin{cases}u,&\text{if $\bar{u}=[u]$},\\ \mathbf{0}_{Y},&\text{otherwise},\end{cases}$	$\displaystyle(s\bar{t})\left\langle\bar{u}\middle/x\right\rangle$	$\displaystyle\coloneqq\sum_{\bar{u}=\bar{v}\cdot\bar{w}}(s\left\langle\bar{v}% \middle/x\right\rangle)(\bar{t}\left\langle\bar{w}\middle/x\right\rangle),$
$\displaystyle y\left\langle\bar{u}\middle/x\right\rangle$	$\displaystyle\coloneqq\begin{cases}y,&\text{if $\bar{u}=1_{Y}$,}\\ \mathbf{0}_{\{y\}},&\text{otherwise},\end{cases}$	$\displaystyle 1_{X}\left\langle\bar{u}\middle/x\right\rangle$	$\displaystyle\coloneqq\begin{cases}1_{X\left\{Y\middle/x\right\}},&\text{if $% \bar{u}=1_{Y}$},\\ \mathbf{0}_{X\left\{Y\middle/x\right\}},&\text{otherwise,}\\ \end{cases}$
$\displaystyle(\lambda y.s)\left\langle\bar{u}\middle/x\right\rangle$	$\displaystyle\coloneqq\lambda y.s\left\langle\bar{u}\middle/x\right\rangle,$	$\displaystyle([s]\cdot\bar{t})\left\langle\bar{u}\middle/x\right\rangle$	$\displaystyle\coloneqq\sum_{\bar{u}=\bar{v}\cdot\bar{w}}[s\left\langle\bar{v}% \middle/x\right\rangle]\cdot(\bar{t}\left\langle\bar{w}\middle/x\right\rangle).$

with $x\neq y$ and in the abstraction case $y\notin Y$ . We extend it to sums in $\mathbb{N}[\mathord{(!)\Delta_{{\sf I}}}(X)]$ by setting:

	$\displaystyle\mathbf{0}_{X}\left\langle\bar{u}\middle/x\right\rangle$	$\displaystyle\coloneqq\mathbf{0}_{X\left\{Y\middle/x\right\}}$	$\displaystyle(s+\mathbf{s})\left\langle\bar{u}\middle/x\right\rangle$	$\displaystyle\coloneqq s\left\langle\bar{u}\middle/x\right\rangle+\mathbf{s}% \left\langle\bar{u}\middle/x\right\rangle$
	$\displaystyle s\left\langle\mathbf{0}_{Y}\middle/x\right\rangle$	$\displaystyle\coloneqq\mathbf{0}_{X\left\{Y\middle/x\right\}}$	$\displaystyle s\left\langle(\bar{u}+\bar{\mathbf{u}})\middle/x\right\rangle$	$\displaystyle\coloneqq s\left\langle\bar{u}\middle/x\right\rangle+s\left% \langle\bar{\mathbf{u}}\middle/x\right\rangle.$

It is easy to verify that the definition above does indeed define a resource sum in $\mathbb{N}[\mathord{(!)\Delta_{{\sf I}}}(X\left\{Y\middle/x\right\})]$ , and that it is stable under the quotients of Definition 24.

Definition 27.

The linear degree $\deg_{x}(s)$ of $x\in\mathcal{V}$ in some $s\in\mathord{(!)\Delta_{{\sf I}}}$ is defined by:

	$\displaystyle\deg_{x}(x)$	$\displaystyle\coloneqq 1,$	$\displaystyle\deg_{x}(\lambda y.s)$	$\displaystyle\coloneqq\deg_{x}(s)\text{, wlog. $x\neq y$,}$	$\displaystyle\deg_{x}(1_{X})$	$\displaystyle\coloneqq 0,$
	$\displaystyle\deg_{x}(y)$	$\displaystyle\coloneqq 0,$	$\displaystyle\deg_{x}(s\bar{t})$	$\displaystyle\coloneqq\deg_{x}(s)+\deg_{x}(\bar{t}),$	$\displaystyle\deg_{x}([s]\cdot\bar{t})$	$\displaystyle\coloneqq\deg_{x}(s)+\deg_{x}(\bar{t}).$

The next lemma is not strictly needed, but helps understanding resource substitution.

Lemma 28.

Consider $s\in\mathord{(!)\Delta_{{\sf I}}}(X)$ , $x\in\mathcal{V}$ and $\bar{u}\in\mathord{!\Delta_{{\sf I}}}(Y)$ , and write $n\coloneqq\deg_{x}(s)$ . Then

s\left\langle\bar{u}\middle/x\right\rangle=\begin{cases}\sum\limits_{\sigma\in% \mathfrak{S}(n)}s\left[u_{\sigma(1)}/x^{(1)},\dots,u_{\sigma(n)}/x^{(n)}\right% ]\left\{Y\middle/x\right\},&\text{if the cardinality of $\bar{u}$ is $n$,}\\ \mathbf{0}_{X\left\{Y\middle/x\right\}},&\text{otherwise,}\\ \end{cases}

where: $\mathfrak{S}(n)$ is the set of permutations of $\{1,\dots,n\}$ ; $u_{1},\dots,u_{n}$ is any enumeration of the elements in $\bar{u}$ ; $x^{(1)},\dots,x^{(n)}$ enumerate the occurrences of $x$ in $s$ ; and $s\left[u_{\sigma(1)}/x^{(1)},\dots,u_{\sigma(n)}/x^{(n)}\right]$ is the $\lambda{\sf I}$ -resource term obtained by substituting each element $u_{\sigma(i)}$ for the occurrence $x^{(i)}$ .

Proof.

Straightforward induction on $s$ . $\hfill\blacktriangleleft$

The next Substitution Lemma concerns the commutation of resource substitutions, and is the analogous of [4, Lemma 2.1.16]. Notice that the assumptions on the substituted variables are stronger than in the usual resource calculus [21, Lemma 2], where only $x\notin Y$ is required.

Lemma 29.

Given $s\in\mathord{(!)\Delta_{{\sf I}}}(X)$ , $\bar{u}\in\mathord{!\Delta_{{\sf I}}}(Y)$ , $\bar{v}\in\mathord{!\Delta_{{\sf I}}}(Z)$ , and $x\in X-Z$ , $y\in X\cup Y$ ,

s\left\langle\bar{u}\middle/x\right\rangle\left\langle\bar{v}\middle/y\right% \rangle=\sum_{\bar{v}=\bar{v}^{\prime}\cdot\bar{v}^{\prime\prime}}s\left% \langle\bar{v}^{\prime}\middle/y\right\rangle\left\langle\bar{u}\left\langle% \bar{v}^{\prime\prime}\middle/y\right\rangle\middle/x\right\rangle.

Proof.

By structural induction on $s$ , using Lemma 28 in order to apply the induction hypothesis only to those subterms where the hypotheses are actually satisfied. $\hfill\blacktriangleleft$

4.3 The operational semantics

We finally endow resource expressions and resource sums with a notion of reduction $\rightarrow_{\mathsf{r}}$ .

Definition 30.

(i)

For each $X\subseteq_{\mathrm{f}}\mathcal{V}$ , define the resource reduction as a relation between $\lambda{\sf I}$ -resource terms and resource sums, i.e. $\mathord{\rightarrow_{\mathsf{r}}}\subseteq\mathord{(!)\Delta_{{\sf I}}}(X)% \times\mathbb{N}[\mathord{(!)\Delta_{{\sf I}}}(X)]$ :

(\lambda x.s)\bar{t}\rightarrow_{\mathsf{r}}s\left\langle\bar{t}\middle/x% \right\rangle missing\qquad\lambda x.s\rightarrow_{\mathsf{r}}\lambda x.% \mathbf{s}^{\prime}s\rightarrow_{\mathsf{r}}\mathbf{s}^{\prime}\qquad s\bar{t}% \rightarrow_{\mathsf{r}}\mathbf{s}^{\prime}\bar{t}s\rightarrow_{\mathsf{r}}% \mathbf{s}^{\prime}\qquad s\bar{t}\rightarrow_{\mathsf{r}}s\bar{\mathbf{t}}^{% \prime}\bar{t}\rightarrow_{\mathsf{r}}\bar{\mathbf{t}}^{\prime}\qquad[s]\cdot% \bar{t}\rightarrow_{\mathsf{r}}{[\mathbf{s}^{\prime}]}\cdot\bar{t}s\rightarrow% _{\mathsf{r}}\mathbf{s}^{\prime}

(ii)

We extend the reduction relation $\rightarrow_{\mathsf{r}}$ to resource sums $\mathbb{N}[\mathord{(!)\Delta_{{\sf I}}}(X)]\times\mathbb{N}[\mathord{(!)% \Delta_{{\sf I}}}(X)]$ , and simultaneously introduce its reflexive closure $\rightarrow_{\mathsf{r}}^{?}$ , as follows:

$s+\mathbf{t}\rightarrow_{\mathsf{r}}\mathbf{s}^{\prime}+\mathbf{t}^{\prime}% \lx@proof@logical@and s\rightarrow_{\mathsf{r}}\mathbf{s}^{\prime}\mathbf{t}% \rightarrow_{\mathsf{r}}^{?}\mathbf{t}^{\prime}\qquad\mathbf{t}\rightarrow_{% \mathsf{r}}^{?}\mathbf{t}^{\prime}\mathbf{t}\rightarrow_{\mathsf{r}}\mathbf{t}% ^{\prime}\qquad\mathbf{t}\rightarrow_{\mathsf{r}}^{?}\mathbf{t}$
(iii)

We denote by $\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\mathsf{r}}$ the reflexive and transitive closure of the relation $\rightarrow_{\mathsf{r}}$ given in (ii).

Observe that $\rightarrow_{\mathsf{r}}$ is well-defined because $\mathrm{fv}((\lambda x.s)\bar{t})=\mathrm{fv}(s\left\langle\bar{t}\middle/x% \right\rangle)$ . Indeed $\mathrm{fv}((\lambda x.s)\bar{t})=\mathrm{fv}(s)-\{x\}\cup\mathrm{fv}(\bar{t})$ with $x\in\mathrm{fv}(s)$ , whence $\mathrm{fv}(s\left\langle\bar{t}\middle/x\right\rangle)=\mathrm{fv}(s)\left\{% \mathrm{fv}(\bar{t})\middle/x\right\}=\mathrm{fv}(s)-\{x\}\cup\mathrm{fv}(\bar% {t})$ .

Example 31.

We use the resource $\lambda{\sf I}$ -terms ${\sf I}$ and ${\sf D}_{n}$ from Example 23.

(i)

${\sf D}_{0}[z]\rightarrow_{\mathsf{r}}(x1_{\{x\}})\langle[z]/x\rangle=(x% \langle[z]/x\rangle)(1_{\{z\}})+(x\langle 1_{\{z\}}/x\rangle)(1_{\{x\}}\langle% [z]/x\rangle)=z1_{\{z\}}+\mathbf{0}_{\{z\}}=z1_{\{z\}}$ . Similarly, ${\sf D}_{0}[{\sf I}]\rightarrow_{\mathsf{r}}{\sf I}1_{\varnothing}\rightarrow% \mathbf{0}_{\varnothing}$ .
(ii)

$(\lambda x.{\sf D_{0}}[x])[z]$ has two redexes. Contracting the outermost first gives $(\lambda x.{\sf D_{0}}[x])[z]\rightarrow_{\mathsf{r}}{\sf D_{0}}[z]\rightarrow% _{\mathsf{r}}z1_{\{z\}}$ . Contracting the innermost $(\lambda x.{\sf D_{0}}[x])[z]\rightarrow_{\mathsf{r}}(\lambda x.x1_{\{x\}})[z]% \rightarrow_{\mathsf{r}}z1_{\{z\}}$ .
(iii)

${\sf D}_{1}[{\sf I},{\sf I}]\rightarrow_{\mathsf{r}}{\sf I}[{\sf I}]+{\sf I}[{% \sf I}]\rightarrow_{\mathsf{r}}{\sf I}+{\sf I}[{\sf I}]\rightarrow_{\mathsf{r}% }{\sf I}+{\sf I}=2.{\sf I}$ . Thus, sums can arise from single terms.

We show that $\rightarrow_{\mathsf{r}}$ enjoys the properties of strong confluence and strong normalisation.

Theorem 32.

(i)

The reduction $\rightarrow_{\mathsf{r}}$ is strongly normalising.
(ii)

$\rightarrow_{\mathsf{r}}$ is strongly confluent in the following sense: for all $\mathbf{s},\mathbf{t}_{1},\mathbf{t}_{2}\in\mathbb{N}[\mathord{(!)\Delta_{{\sf I% }}}(X)]$ such that $\mathbf{s}\rightarrow_{\mathsf{r}}\mathbf{t}_{1}$ and $\mathbf{s}\rightarrow_{\mathsf{r}}\mathbf{t}_{2}$ , there exists $\mathbf{u}\in\mathbb{N}[\mathord{(!)\Delta_{{\sf I}}}(X)]$ such that $\mathbf{t}_{1}\rightarrow_{\mathsf{r}}^{?}\mathbf{u}$ and $\mathbf{t}_{2}\rightarrow_{\mathsf{r}}^{?}\mathbf{u}$ .

Proof.

(i)

The size $\mathsf{size}(s)\in\mathbb{N}$ of a resource expression $s\in\mathord{(!)\Delta_{{\sf I}}}$ is defined by structural induction as usual, with base cases $\mathsf{size}(x)=1$ and $\mathsf{size}(1_{X})=0$ , so that $\mathsf{size}(1_{X}\cdot\bar{t})=\mathsf{size}(\bar{t})$ . The sum-size of a resource sum $\mathbf{s}$ is the finite multiset defined by $\mathsf{ssize}(\mathbf{0}_{X})=[]$ and $\mathsf{ssize}(s+\mathbf{t})=[\mathsf{size}(s)]\cdot\mathsf{ssize}(\mathbf{t})$ . Sum-sizes are well-ordered by the usual well-founded ordering $\prec_{\mathbb{N}}$ on finite multisets over $\mathbb{N}$ (see [43, §A.6]).

Now, assume that $\mathbf{s}\rightarrow_{\mathsf{r}}\mathbf{s}^{\prime}$ . Since the contraction of a redex suppresses an abstraction and there is no duplication, we get $\mathsf{ssize}(\mathbf{s})\prec_{\mathbb{N}}\mathsf{ssize}(\mathbf{s}^{\prime})$ . Conclude since $\prec_{\mathbb{N}}$ is well-founded.
(ii)

The sequence of lemmas leading to the result follows a well-trodden path in the resource calculus [46, 10]. It is sufficient to check that they generalize to our setting.

$\hfill\blacktriangleleft$

By (ii) above every $\mathbf{s}\in\mathbb{N}[\mathord{(!)\Delta_{{\sf I}}}(X)]$ has a unique $\mathrm{r}$ -normal form which is denoted $\mathrm{nf}(\mathbf{s})$ .

5 Taylor approximation for Ohana trees

In its original formulation, Ehrhard and Regnier’s Taylor expansion translates a $\lambda$ -term as a power series of iterated derivatives [20]. We now introduce a qualitative Taylor expansion [34] specifically designed for the $\lambda{\sf I}$ -calculus, having as target the $\lambda{\sf I}$ -resource calculus.

5.1 The Taylor approximation

Intuitively, a qualitative Taylor expansion should associate each term $M\in\Lambda_{\sf I}(X)$ with a set of resource approximants $\mathcal{T}_{\mathsf{m}}(M)\subseteq\mathord{\Delta_{{\sf I}}}(X)$ . Therefore the codomain of $\mathcal{T}_{\mathsf{m}}(-)$ should be $\coprod_{X\subseteq_{\mathrm{f}}\mathcal{V}}\cramped{2^{\mathord{\Delta_{{\sf I% }}}(X)}}$ , and what we actually define is $\mathcal{T}_{\mathsf{m}}(M)\coloneqq(X,\mathcal{T}_{\mathsf{m}}^{\bullet}(M))$ with $\mathcal{T}_{\mathsf{m}}^{\bullet}(M)\subseteq\mathord{\Delta_{{\sf I}}}(X)$ . Notice that, whereas all previous constructions of disjoint unions $\coprod_{X\subseteq_{\mathrm{f}}\mathcal{V}}$ were formed from genuinely disjoint sets, this is no longer the case here, as $\varnothing\in\cramped{2^{\mathord{\Delta_{{\sf I}}}(X)}}$ , for all $X$ .

Notation 33.

(i)

For $X\subseteq_{\mathrm{f}}\mathcal{V}$ and $\mathcal{X}\in\cramped{2^{\mathord{\Delta_{{\sf I}}}(X)}}$ , we write $\mathrm{fv}(X,\mathcal{X})\coloneqq X$ .
(ii)

We let $\mathord{\subseteq^{\bullet}}$ denote the order relation on $\coprod_{X\subseteq_{\mathrm{f}}\mathcal{V}}\cramped{2^{\mathord{\Delta_{{\sf I% }}}(X)}}$ such that $(X,\mathcal{X})\subseteq^{\bullet}(Y,\mathcal{Y})$ whenever $X=Y$ and $\mathcal{X}\subseteq\mathcal{Y}$ . We write $\cup^{\bullet}$ for the corresponding least upper bounds.
(iii)

We write $s\in^{\bullet}(X,\mathcal{X})$ to mean that $s\in\mathcal{X}$ .
(iv)

Given $\mathcal{X}\in\cramped{2^{\mathord{\Delta_{{\sf I}}}(X)}}$ , $\mathcal{Y}\in\cramped{2^{\mathord{!\Delta_{{\sf I}}}(Y)}}-\{\varnothing\}$ and $x\in X$ , we write:

$\lambda x.(X,\mathcal{X})\coloneqq(X-\{x\},\{\lambda x.s\ |\ s\in\mathcal{X}\}% ),\qquad(X,\mathcal{X})\mathcal{Y}\coloneqq(X\cup Y,\{s\bar{t}\ |\ s\in% \mathcal{X},\ \bar{t}\in\mathcal{Y}\}).$

Definition 34.

(i)

The Taylor expansion $\mathcal{T}_{\mathsf{m}}(M)\in\coprod_{X\subseteq_{\mathrm{f}}\mathcal{V}}% \cramped{2^{\mathord{\Delta_{{\sf I}}}(X)}}$ of a $\lambda{\sf I}$ -term $M$ , is defined together with $\mathcal{T}_{\mathsf{m}}^{!}(M)\subset\mathord{!\Delta_{{\sf I}}}(\mathrm{fv}(% M))$ by mutual induction:

	$\displaystyle\begin{aligned} \mathcal{T}_{\mathsf{m}}(x)&\coloneqq(\{x\},\{x\}% ),&\mathcal{T}_{\mathsf{m}}(\lambda x.M)&\coloneqq\lambda x.\mathcal{T}_{% \mathsf{m}}(M),&\mathcal{T}_{\mathsf{m}}(MN)&\coloneqq\mathcal{T}_{\mathsf{m}}% (M)\mathcal{T}_{\mathsf{m}}^{!}(N),\end{aligned}$
	$\displaystyle\mathcal{T}_{\mathsf{m}}^{!}(M)\coloneqq\{1_{\mathrm{fv}(M)}\}% \cup\{[t_{0},\dots,t_{n}]\ \|\ n\in\mathbb{N},\ t_{0},\dots,t_{n}\in^{\bullet}% \mathcal{T}_{\mathsf{m}}(M)\}.$

(ii)

The above definition is extended to Ohana trees by setting, for all $M\in\Lambda_{\sf I}$ ,

$\mathcal{T}_{\mathsf{m}}(\mathrm{OT}(M))\coloneqq\mathop{\bigcup\nolimits^{% \mathrlap{\bullet}}}\displaylimits_{A\in\mathrm{App}_{\mathsf{m}}(M)}\mathcal{% T}_{\mathsf{m}}(A),\qquad\text{together with }\left\{\begin{array}[]{r!{\eqdef% }l}\mathcal{T}_{\mathsf{m}}(\bot_{X})\lx@intercol\coloneqq&(X,\varnothing),\\ \mathcal{T}_{\mathsf{m}}^{!}(\bot_{X})\lx@intercol\coloneqq&\{1_{X}\}.\\ \end{array}\right.$

$\blacktriangleright$ Remark 35.

For all $M$ , we have $\mathrm{fv}(\mathcal{T}_{\mathsf{m}}(M))=\mathrm{fv}(M)$ . Similarly, $\mathrm{fv}(\mathcal{T}_{\mathsf{m}}(\mathrm{OT}(M)))=\mathrm{fv}(M)$ , due to Remark 16 and the way we ordered $\coprod_{X\subseteq_{\mathrm{f}}\mathcal{V}}\cramped{2^{\mathord{\Delta_{{\sf I% }}}(X)}}$ .

Example 36.

(i)

$\mathcal{T}_{\mathsf{m}}({\sf I})=(\varnothing,\{{\sf I}\})$ , $\mathcal{T}_{\mathsf{m}}({\sf D})=(\varnothing,\{{\sf D}_{n}\ |\ n\in\mathbb{N% }\})$ .
(ii)

$\mathcal{T}_{\mathsf{m}}(\mathrm{OT}({\sf Y}f))=(\{f\},\mathcal{X}_{{\sf Y}f})$ and $\mathcal{T}_{\mathsf{m}}(\mathrm{OT}(\text{\scalebox{0.8}{\faBible}}_{\,l}f))=% (\{f,l\},\mathcal{X}_{\text{\scalebox{0.8}{\faBible}}_{\,l}f})$ , where the sets of approximants can be described as the smallest (in fact, unique) subsets of $\mathord{\Delta_{{\sf I}}}$ such that:

$\displaystyle\mathcal{X}_{{\sf Y}f}$ $\displaystyle=\{f1_{\{f\}}\}\cup\{f[t_{0},\dots,t_{n}]\ |\ n\in\mathbb{N},\ t_% {0},\dots,t_{n}\in\mathcal{X}_{{\sf Y}f}\},$

$\displaystyle\mathcal{X}_{\text{\scalebox{0.8}{\faBible}}_{\,l}f}$ $\displaystyle=\{f1_{\{f,l\}}\}\cup\{f[t_{0},\dots,t_{n}]\ |\ n\in\mathbb{N},\ % t_{0},\dots,t_{n}\in\mathcal{X}_{\text{\scalebox{0.8}{\faBible}}_{\,l}f}\}.$

We now describe how resource reduction acts on Taylor expansions, i.e. on potentially infinite sets of resource expressions.

Notation 37.

(i)

Given $\mathbf{s}\in\mathbb{N}[\mathord{(!)\Delta_{{\sf I}}}(X)]$ , we denote by $|\mathbf{s}|\in\coprod_{X\subseteq_{\mathrm{f}}\mathcal{V}}\cramped{2^{% \mathord{\Delta_{{\sf I}}}(X)}}$ its support, defined by $|\mathbf{0}_{X}|\coloneqq(X,\varnothing)$ and $|s+\mathbf{t}|\coloneqq(X,\{s\})\cup^{\bullet}|\mathbf{t}|$ . Notice that $s\in^{\bullet}|\mathbf{t}|$ whenever $s$ bears a non-zero coefficient in $\mathbf{t}$ (i.e. $\mathbf{t}=s+\mathbf{t}^{\prime}$ , for some $\mathbf{t}^{\prime}$ ).
(ii)

Given $\mathcal{X}\in\cramped{2^{\mathord{(!)\Delta_{{\sf I}}}(X)}}$ , we write $\mathrm{nf}(X,\mathcal{X})\coloneqq\mathop{\bigcup\nolimits^{\mathrlap{\bullet% }}}\displaylimits_{s\in\mathcal{X}}|\mathrm{nf}(s)|$ . Notice that $\mathrm{fv}(\mathrm{nf}(X,\mathcal{X}))=X$ , and that $\mathrm{nf}(X,\mathcal{X})=(X,\varnothing)$ if and only if $s\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\mathsf{r}}\mathbf{0% }_{X}$ , for all $s\in\mathcal{X}$ .

This allows us to state the following theorem, adapting [20, Theorem 2].

Theorem 38 (Commutation).

For all $M\in\Lambda_{\sf I}$ , $\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(M))=\mathcal{T}_{\mathsf{m}}(\mathrm{OT}(% M))$ .

We outline a proof in the following sequence of lemmas, similar to the one in [2]; alternatively, the variants of [20, 21], [38] and [10, 12] could also be adapted.

Lemma 39.

For all resource sums $\mathbf{s}$ such that $|\mathbf{s}|\subseteq^{\bullet}\mathcal{T}_{\mathsf{m}}(M)$ , there exists a reduction $M\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}N$ such that $|\mathrm{nf}(\mathbf{s})|\subseteq^{\bullet}\mathcal{T}_{\mathsf{m}}(N)$ .

Proof.

By induction on the length of the longest reduction $\mathbf{s}\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\mathsf{r}}% \mathrm{nf}(\mathbf{s})$ . If it is $0$ , take $N\coloneqq M$ . Otherwise, the longest reduction is $\mathbf{s}=t+\mathbf{u}\rightarrow_{\mathsf{r}}\mathbf{t}^{\prime}+\mathbf{u}% \mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\mathsf{r}}\mathrm{nf% }(\mathbf{s})$ . By firing all redexes in $M$ and $\mathbf{u}$ at the same position as the redex fired in $t\rightarrow_{\mathsf{r}}\mathbf{t}^{\prime}$ (formally we do this by induction on this reduction), we obtain $M\rightarrow_{\beta}M^{\prime}$ and $\mathbf{u}\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\mathsf{r}}% \mathbf{u}^{\prime}$ such that $|\mathbf{t}^{\prime}+\mathbf{u}^{\prime}|\subseteq^{\bullet}\mathcal{T}_{% \mathsf{m}}(M^{\prime})$ . By confluence, $\mathbf{t}^{\prime}+\mathbf{u}^{\prime}\mathrel{\rightarrow\mathrel{\mkern-14.% 0mu}\rightarrow}_{\mathsf{r}}\mathrm{nf}(\mathbf{s})$ . We conclude by induction on this (shorter) reduction. $\hfill\blacktriangleleft$

Lemma 40.

If $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(N)$ is in $\mathsf{r}$ -nf, then there exists $A\in\mathrm{App}_{\mathsf{m}}(N)$ such that $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(A)$ .

Proof.

By induction on $t$ . An $\mathsf{r}$ -nf is also a hnf, hence $t=\lambda\vec{x}.y\bar{t}_{1}\cdots\bar{t}_{k}$ and $N=\lambda\vec{x}.yN_{1}\cdots N_{k}$ . For $1\leq i\leq k$ , $\bar{t}_{i}\in\mathcal{T}_{\mathsf{m}}^{!}(N_{i})$ . If $\bar{t}_{i}=1_{\mathrm{fv}(N_{i})}$ define $A_{i}\coloneqq\bot_{\mathrm{fv}(N_{i})}$ . If $\bar{t}_{i}=[t_{i}^{1},\dots,t_{i}^{n}]$ , each $t_{i}^{j}$ is in $\mathsf{r}$ -nf, by induction there is $A_{i}^{j}\in\mathrm{App}_{\mathsf{m}}(N_{i})$ , $t_{i}^{j}\in^{\bullet}\mathcal{T}_{\mathsf{m}}(A_{i}^{j})$ . Define $A_{i}\coloneqq\bigsqcup_{j=1}^{n}A_{i}^{j}\in\mathrm{App}_{\mathsf{m}}(N_{i})$ . Finally, $A\coloneqq\lambda\vec{x}.yA_{1}\cdots A_{k}\in\mathrm{App}_{\mathsf{m}}(N)$ and $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(A)$ . $\hfill\blacktriangleleft$

Lemma 41 (Monotonicity of $\mathcal{T}_{\mathsf{m}}(-)$ ).

(i)

$\mathcal{T}_{\mathsf{m}}(A)\subseteq^{\bullet}\mathcal{T}_{\mathsf{m}}(A^{% \prime})$ if and only if $A\sqsubseteq A^{\prime}$ .
(ii)

For all $N\in\Lambda_{\sf I}$ , we have $\mathcal{T}_{\mathsf{m}}(\omega_{\mathsf{m}}(N))\subseteq^{\bullet}\mathcal{T}% _{\mathsf{m}}(N)$ .

Proof.

Immediate inductions (i) on $A$ and $A^{\prime}$ , and (ii) on the head structure of $N$ . $\hfill\blacktriangleleft$

Lemma 42 (Simulation of $\rightarrow_{\beta}$ ).

If $M\rightarrow_{\beta}N$ , then $\mathcal{T}_{\mathsf{m}}(N)=\mathop{\bigcup\nolimits^{\mathrlap{\bullet}}}% \displaylimits_{s\in^{\bullet}\mathcal{T}_{\mathsf{m}}(M)}|\mathbf{t}_{s}|$ for resource sums $\mathbf{t}_{s}\in\mathbb{N}[\mathord{\Delta_{{\sf I}}}(\mathrm{fv}(M))]$ such that $\forall s\in^{\bullet}\mathcal{T}_{\mathsf{m}}(M),\ s\mathrel{\rightarrow% \mathrel{\mkern-14.0mu}\rightarrow}_{\mathsf{r}}\mathbf{t}_{s}$ .

Proof.

One first shows by induction on $P$ that for all $P,Q\in\Lambda_{\sf I}$ and $x\in\mathrm{fv}(P)$ , $\mathcal{T}_{\mathsf{m}}(P[Q/x])=\mathop{\bigcup\nolimits^{\mathrlap{\bullet}}% }\displaylimits_{s\in^{\bullet}\mathcal{T}_{\mathsf{m}}(P)}\mathop{\bigcup% \nolimits^{\mathrlap{\bullet}}}\displaylimits_{\bar{t}\in\mathcal{T}_{\mathsf{% m}}^{!}(Q)}|s\left\langle\bar{t}\middle/x\right\rangle|$ . Then the proof is an induction on $M\rightarrow_{\beta}N$ , using the previous equality in the base case. See the details of a similar proof in [12, Lemmas 4.1 and 4.2]. $\hfill\blacktriangleleft$

Lemma 43.

If $A\in\mathcal{A}_{\mathsf{m}}$ then all $s\in^{\bullet}\mathcal{T}_{\mathsf{m}}(A)$ are in $\mathsf{r}$ -nf.

Proof.

Immediate induction on $A$ . $\hfill\blacktriangleleft$

Everything is now in place to prove the Commutation Theorem 38.

Proof of Theorem 38.

By Remark 35, $\mathrm{fv}(\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(M)))=\mathrm{fv}(M)=\mathrm{% fv}(\mathcal{T}_{\mathsf{m}}(\mathrm{OT}(M)))$ . Thus, it is sufficient to prove that, for $t\in\mathord{\Delta_{{\sf I}}}(\mathrm{fv}(M))$ : $t\in^{\bullet}\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(M))$ if and only if $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(\mathrm{OT}(M))$ .

Take $t\in^{\bullet}\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(M))$ , i.e. $t\in|\mathrm{nf}(s)|$ for some $s\in^{\bullet}\mathcal{T}_{\mathsf{m}}(M)$ . Then, by Lemma 39, there exists a reduction $M\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}N$ such that $|\mathrm{nf}(s)|\subseteq^{\bullet}\mathcal{T}_{\mathsf{m}}(N)$ . Hence $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(N)$ and $t$ is in $\mathsf{r}$ -nf: Lemma 40 ensures that $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(A)$ for some $A\in\mathrm{App}_{\mathsf{m}}(N)=\mathrm{App}_{\mathsf{m}}(M)$ (by Proposition 19). This means exactly that $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(\mathrm{OT}(M))$ .

Conversely, take $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(\mathrm{OT}(M))$ , i.e. $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(A)$ for some $A\in\mathrm{App}_{\mathsf{m}}(M)$ . By definition there is a reduction $M\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}N$ such that $A\sqsubseteq\omega_{\mathsf{m}}(N)$ . By Lemma 41, $t\in^{\bullet}\mathcal{T}_{\mathsf{m}}(A)\subseteq^{\bullet}\mathcal{T}_{% \mathsf{m}}(\omega_{\mathsf{m}}(N))\subseteq^{\bullet}\mathcal{T}_{\mathsf{m}}% (N)$ . By iterated applications of Lemma 42, there is an $s\in^{\bullet}\mathcal{T}_{\mathsf{m}}(M)$ such that $s\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\mathsf{r}}\mathbf{t% }_{s}$ and $t\in|\mathbf{t}_{s}|$ . By Lemma 43, $t$ is in $\mathsf{r}$ -nf, therefore $t\in^{\bullet}|\mathrm{nf}(s)|\subseteq^{\bullet}\mathrm{nf}(\mathcal{T}_{% \mathsf{m}}(M))$ . $\hfill\blacktriangleleft$

5.2 The $\lambda{\sf I}$ -theory of Ohana trees

Consider the equivalence $\mathcal{O}$ on $\Lambda_{\sf I}$ , defined by $M=_{\mathcal{O}}N$ if and only if $\mathrm{OT}(M)=\mathrm{OT}(N)$ . Thanks to Theorem 38, we are now able to show that this equivalence is a $\lambda{\sf I}$ -theory.

Corollary 44.

For $M,N\in\Lambda_{\sf I}$ , $M=_{\mathcal{O}}N$ if and only if $\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(M))=\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(% N))$ .

Proof.

( $\Rightarrow$ ) Immediate by Theorem 38. ( $\Leftarrow$ ) Take $M, N$ such that $\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(M))=\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(% N))$ . By Theorem 20, it is sufficient to prove $\mathrm{App}_{\mathsf{m}}(M)=\mathrm{App}_{\mathsf{m}}(N)$ . Take $A\in\mathrm{App}_{\mathsf{m}}(M)$ . If $A=\bot_{X}$ , then $A\in\mathrm{App}_{\mathsf{m}}(N)$ is trivial since $\mathrm{App}_{\mathsf{m}}(N)$ is downward closed. Otherwise, by hypothesis and Theorem 38, $\mathcal{T}_{\mathsf{m}}(A)\subseteq^{\bullet}\mathop{\bigcup\nolimits^{% \mathrlap{\bullet}}}\displaylimits_{B\in\mathrm{App}_{\mathsf{m}}(N)}\mathcal{% T}_{\mathsf{m}}(B)$ . There is a $B\in\mathrm{App}_{\mathsf{m}}(N)$ such that $[\![A]\!]_{\mathsf{r}}\in^{\bullet}\mathcal{T}_{\mathsf{m}}(B)$ , where $[\![A]\!]_{\mathsf{r}}\in^{\bullet}\mathcal{T}_{\mathsf{m}}(A)$ is defined by

\begin{array}[]{rcl}[\![x]\!]_{\mathsf{r}}&\coloneqq&x,\\ [\![\lambda\vec{x}.yA_{1}\cdots A_{k}]\!]_{\mathsf{r}}&\coloneqq&\lambda\vec{x% }.y[\![A_{1}]\!]_{\mathsf{r}}^{!}\cdots[\![A_{k}]\!]_{\mathsf{r}}^{!},\\ \end{array}\qquad[\![A]\!]_{\mathsf{r}}^{!}\coloneqq\begin{cases}1_{X},&% \textrm{if }A=\bot_{X},\\ {[[\![A]\!]_{\mathsf{r}}]},&\textrm{otherwise}.\end{cases}

By induction on $A$ , one shows that $[\![A]\!]_{\mathsf{r}}\in^{\bullet}\mathcal{T}_{\mathsf{m}}(B)$ implies $A\sqsubseteq B$ , hence $A\in\mathrm{App}_{\mathsf{m}}(N)$ by downward-closure (Lemma 18(ii)). This shows that $\mathrm{App}_{\mathsf{m}}(M)\subseteq\mathrm{App}_{\mathsf{m}}(N)$ . The converse inclusion is symmetric. $\hfill\blacktriangleleft$

Corollary 45.

$\mathcal{O}$ is a $\lambda{\sf I}$ -theory.

Proof.

The relation $=_{\mathcal{O}}$ is clearly an equivalence. By Propositions 19 and 20, for all $M,N\in\Lambda_{\sf I}$ , $M=_{\beta}N$ entails $M=_{\mathcal{O}}N$ .

For compatibility with abstraction, take $M=_{\mathcal{O}}N$ and $x\in\mathrm{fv}(M)\cap\mathrm{fv}(N)$ . By Corollary 44, we get $\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(\lambda x.M))=\lambda x.\mathrm{nf}(% \mathcal{T}_{\mathsf{m}}(M))=\lambda x.\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(N)% )=\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(\lambda x.N))$ .

For compatibility with application, by Theorem 32 observe that for all $M,N\in\Lambda_{\sf I}$ , $\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(MN))=\mathrm{nf}(\mathcal{T}_{\mathsf{m}}% (M)\mathcal{T}_{\mathsf{m}}^{!}(N))=\mathrm{nf}(\mathrm{nf}(\mathcal{T}_{% \mathsf{m}}(M))\mathrm{nf}(\mathcal{T}_{\mathsf{m}}^{!}(N)))$ , where $\mathrm{nf}(\mathcal{T}_{\mathsf{m}}^{!}(N))$ is defined by adapting Notation 37 to sets of resource bags. Therefore, $\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(M))=\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(% M^{\prime}))$ and $\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(N))=\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(% N^{\prime}))$ imply $\mathrm{nf}(\mathcal{T}_{\mathsf{m}}(MN))=\mathrm{nf}(\mathcal{T}_{\mathsf{m}}% (M^{\prime}N^{\prime}))$ , and we can conclude the proof by Corollary 44. $\hfill\blacktriangleleft$

6 Conclusions and future work

In this paper we introduced the Ohana trees for the $\lambda{\sf I}$ -calculus, together with two theories of program approximations: the former based on finite trees, the latter on resource approximants and Taylor expansion. Our pioneering results look encouraging, so we believe that this approach deserves further investigations.

6.1 Further work on the $\lambda{\sf I}$ -calculus

The Ohana trees introduced in Definition 10 are an adaptation of Böhm trees, since they regard as meaningless the terms without hnf. By considering as meaningless the subset of zero-terms¹¹1I.e., terms without an hnf that never reduce to an abstraction. one obtains Lévy-Longo trees [31, 32], and by taking mute terms²²2Also called root active, mute terms have the property that all their reducts can reduce to a redex. as meaningless one obtains Berarducci trees [7]. Our definition of Ohana trees can be readily adapted to both settings by appropriately modifying the notion of meaningless. Preliminary investigations indicate that all our results extend seamlessly to the Lévy-Longo version. Regarding the Berarducci version, the direct approximants can be generalized without any issues (except for the fact that an oracle is needed, see [45]). We are currently studying whether the corresponding $\lambda{\sf I}$ -resource calculus and Taylor expansion could also be designed.

Our investigation of memory trees started from semantical considerations. The relational model with infinite multiplicities $\mathcal{E}$ , defined in [9], distinguishes ${\sf\Omega}$ from ${\sf\Omega}x$ , and ${\sf Y}$ from $\text{\scalebox{0.8}{\faBible}}_{\,l}$ , just like our memory trees. Unlike our memory trees, it equates $\lambda x.x({\sf\Omega}y)({\sf\Omega}z)$ and $\lambda x.x({\sf\Omega}z)({\sf\Omega}y)$ , thus the induced theory is different from memory trees equality ( $=_{\mathcal{O}}$ ).

Finding a denotational model whose theory captures exactly the Ohana tree equality would reinforce our belief that they are a natural notion of trees for the $\lambda{\sf I}$ -calculus.

Problem 46.

Is there a denotational model of $\Lambda_{\sf I}$ whose theory is exactly $\mathcal{O}$ ?

As pointed out by one of the referees, our Definition 6 of $\lambda{\sf I}$ -terms can most likely be recast in the framework of abstract syntax with binding [23]: just as $\Lambda(-)$ can be described as a canonical presheaf over (a skeleton of) the category of finite sets and functions, $\Lambda_{\sf I}(-)$ would be a presheaf over the category of finite sets and surjections (intuitively, considering only surjective renamings of variables prevents any weakening). Similarly, $\mathord{(!)\Delta_{{\sf I}}}(-)$ would appear as a presheaf over the same category. One could then wonder whether all our work can be presented “over” finite sets and surjections; in particular, would our Taylor expansion act naturally with respect to these presheaf constructions? There is hope that it is the case, given that we followed the inductive structures of both $\lambda{\sf I}$ -terms and $\lambda{\sf I}$ -resource terms, which may pave the way towards building (presheaf) models answering to Problem 46.

We believe that finding a denotational model and studying its categorical properties are important steps towards a deeper mathematical understanding of our Taylor expansion. In particular, it is currently unclear whether our resource calculus stands on a solid notion of differentiation, as it is the case for the usual resource calculus [19], or if it is an ad hoc adaptation.

Problem 47.

Is the $\lambda{\sf I}$ -resource calculus representing some notion of derivative?

We now discuss more speculative extensions, going beyond the setting of $\lambda{\sf I}$ -calculus.

6.2 What about the full $\lambda$ -calculus?

We have seen that the model $\mathcal{E}$ from [9] distinguishes some meaningless terms having different free variables, but equates some $\lambda{\sf I}$ -terms having different Ohana trees. Characterizing its theory seems a very natural question that has been completely overlooked in the literature.

Problem 48.

Is there an operational characterization of the $\lambda$ -theory induced by $\mathcal{E}$ ?

The fact that $\mathcal{E}$ is a model of the full $\lambda$ -calculus witnesses the existence of consistent $\lambda$ -theories that remember variables that are pushed into infinity in the Böhm tree semantics. It is then natural to wonder whether it makes sense to extend the definition of Ohana trees to arbitrary $\lambda$ -terms. The idea is to consider the set of permanent free variables of $M\in\Lambda$ :

\mathrm{pfv}(M)=\{x\mid\forall N\in\Lambda\,.\,M\mathrel{\rightarrow\mathrel{% \mkern-14.0mu}\rightarrow}_{\beta}N\textrm{ implies }x\in\mathrm{fv}(N)\}

Intuitively, $\mathrm{pfv}(M)$ is the set of free variables of $M$ that are never erased along a reduction.

Definition 49.

The Ohana tree of a $\lambda$ -term $M$ can be then defined by setting:

$\blacksquare$

$\mathrm{OT}(M)=\lambda\vec{x}.y\cdot^{\mathrm{pfv}(M_{1})}\mathrm{OT}(M_{1})% \cdots^{\mathrm{pfv}(M_{k})}\mathrm{OT}(M_{k})$ , if $M\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{h}\lambda x_{1}\dots x% _{n}.yM_{1}\cdots M_{k}$ ;
$\blacksquare$

$\bot_{\mathrm{pfv}(M)}$ , otherwise.

For $M\in\Lambda_{\sf I}$ the definition above is equivalent to Definition 10, since $\mathrm{pfv}(M)=\mathrm{fv}(M)$ . For an arbitrary $M\in\Lambda$ , one needs an oracle to compute $\mathrm{pfv}(M)$ , but an oracle is already needed to determine whether $M$ has an hnf, therefore the logical complexity does not increase.

Preliminary investigations show that the above notion of Ohana tree remains invariant by $\rightarrow_{\beta}$ . The key property which is exploited to prove this result is that $\mathrm{pfv}(\lambda\vec{x}.yM_{1}\cdots M_{k})=\{y\}\cup\mathrm{pfv}(M_{1})% \cup\cdots\cup\mathrm{pfv}(M_{k})$ . The main problem of Definition 49 is that the equality induced on $\lambda$ -terms is not a $\lambda$ -theory because it is not compatible with application. The following counterexample exploits the fact that, in general, $\mathrm{pfv}(MN)\neq\mathrm{pfv}(M)\cup\mathrm{pfv}(N)$ . Define:

{\sf W}=\lambda xy.yxy,\qquad M=\lambda z.{\sf W}(zv_{1}v_{2}){\sf W},\qquad N% =\lambda z.{\sf W}(zv_{2}v_{1}){\sf W},\qquad\textrm{ for }v_{1},v_{2}\in% \mathcal{V}.

We have $M\rightarrow_{h}\lambda z.(\lambda y.y(zv_{1}v_{2})y){\sf W}\rightarrow_{h}M$ and $N\rightarrow_{h}\lambda z.(\lambda y.y(zv_{2}v_{1})y){\sf W}\rightarrow_{h}N$ , whence $\mathrm{OT}(M)=\mathrm{OT}(N)=\bot_{\{v_{1},v_{2}\}}$ . By applying these terms to ${\sf K}$ , we obtain $M{\sf K}\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}{\sf W}% v_{1}{\sf W}$ and $N{\sf K}\mathrel{\rightarrow\mathrel{\mkern-14.0mu}\rightarrow}_{\beta}{\sf W}% v_{2}{\sf W}$ , therefore $\mathrm{OT}(M{\sf K})=\bot_{\{v_{1}\}}\neq\bot_{\{v_{2}\}}=\mathrm{OT}(N{\sf K})$ . We conclude that the equality induced on $\Lambda$ is not a $\lambda$ -theory, because it is not compositional. This counterexample is particularly strong because it shows that this is independent from the fact that Ohana trees are generalizations of Böhm trees and not, say, Berarducci trees. Indeed, the $M, N$ constructed above have the same Böhm tree, Lévy-Longo tree and Berarducci tree.

A natural question is whether Ohana trees can be used as a meaningful notion of observation, in the sense of Morris’s observational equivalences [37].

Problem 50.

Is there a denotational model inducing the following $\lambda$ -theory?

M\equiv N\iff\forall C[]\,.\,\mathrm{OT}(C[M])=\mathrm{OT}(C[N])

where $C[]$ denotes a $\lambda$ -calculus context (namely, a $\lambda$ -term containing a hole $[]$ ), and $C[M]$ the $\lambda$ -term obtained by replacing $M$ for the hole $[]$ in $C[]$ , possibly with capture of free variables.

References

[1] Sandra Alves and Mário Florido. Structural rules and algebraic properties of intersection types. In Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu, editors, Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings, volume 13572 of Lecture Notes in Computer Science, pages 60–77. Springer, 2022. doi:10.1007/978-3-031-17715-6_6.
[2] Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proceedings of the ACM on Programming Languages, 4(POPL):1–23, 2019. doi:10.1145/3371069.
[3] Henk Barendregt. The type free lambda calculus. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 1091–1132. North-Holland, Amsterdam, 1977.
[4] Henk Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1984.
[5] Henk Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite. College Publications, 2022. URL: https://www.collegepublications.co.uk/logic/mlf/?00035.
[6] Stefano Berardi and Ugo de’Liguoro. Non-monotonic pre-fix points and learning. Fundam. Informaticae, 150(3-4):259–280, 2017. doi:10.3233/FI-2017-1470.
[7] Alessandro Berarducci. Infinite $\lambda$ -calculus and non-sensible models. In Marcel Dekker, editor, Logic and Algebra, volume 180, pages 339–377, New York, 1996. Presented to the conference in honour of Roberto Magari, Pontignano 1994.
[8] Flavien Breuvart, Giulio Manzonetto, and Domenico Ruoppolo. Relational graph models at work. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:2)2018.
[9] Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. Exponentials with infinite multiplicities. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 170–184. Springer, 2010. doi:10.1007/978-3-642-15205-4_16.
[10] Rémy Cerda. Taylor Approximation and Infinitary $\lambda$ -Calculi. Phd thesis, Aix-Marseille Université, 2024. URL: https://hal.science/tel-04664728.
[11] Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana trees and Taylor expansion for the $\lambda$ I-calculus. No variable gets left behind or forgotten!, 2025. Version of this paper with additional proofs in an appendix. arXiv:2505.06193.
[12] Rémy Cerda and Lionel Vaux Auclair. Finitary simulation of infinitary $\beta$ -reduction via Taylor expansion, and applications. Logical Methods in Computer Science, 19, 2023. doi:10.46298/lmcs-19(4:34)2023.
[13] Alonzo Church. The calculi of lambda conversion. Princeton University Press, 1941.
[14] Lukasz Czajka. A new coinductive confluence proof for infinitary lambda calculus. Log. Methods Comput. Sci., 16(1), 2020. doi:10.23638/LMCS-16(1:31)2020.
[15] Daniel de Carvalho and Lorenzo Tortora de Falco. The relational model is injective for multiplicative exponential linear logic (without weakenings). Ann. Pure Appl. Log., 163(9):1210–1236, 2012. doi:10.1016/J.APAL.2012.01.004.
[16] Daniel de Carvalho and Lorenzo Tortora de Falco. A semantic account of strong normalization in linear logic. Inf. Comput., 248:104–129, 2016. doi:10.1016/J.IC.2015.12.010.
[17] Aloÿs Dufour and Damiano Mazza. Böhm and Taylor for all! In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, volume 299 of LIPIcs, pages 29:1–29:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.FSCD.2024.29.
[18] Lavinia Egidi, Furio Honsell, and Simona Ronchi Della Rocca. Operational, denotational and logical descriptions: a case study. Fundam. Informaticae, 16(1):149–169, 1992.
[19] Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1–41, 2003. doi:10.1016/S0304-3975(03)00392-X.
[20] Thomas Ehrhard and Laurent Regnier. Böhm trees, Krivine’s machine and the Taylor expansion of lambda-terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, Logical Approaches to Computational Barriers (CiE 2006), pages 186–197, 2006. doi:10.1007/11780342_20.
[21] Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2):347–372, 2008. doi:10.1016/j.tcs.2008.06.001.
[22] Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop. Highlights in infinitary rewriting and lambda calculus. Theor. Comput. Sci., 464:48–71, 2012. doi:10.1016/J.TCS.2012.08.018.
[23] Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In 14th Symposium on Logic in Computer Science, 1999. doi:10.1109/lics.1999.782615.
[24] Silvia Ghilezan. Strong normalization and typability with intersection types. Notre Dame J. Formal Log., 37(1):44–52, 1996. doi:10.1305/NDJFL/1040067315.
[25] Furio Honsell and Marina Lenisa. Some results on the full abstraction problem for restricted lambda calculi. In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS’93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings, volume 711 of Lecture Notes in Computer Science, pages 84–104. Springer, 1993. doi:10.1007/3-540-57182-5_6.
[26] J. Martin E. Hyland. A syntactic characterization of the equality in some models for the $\lambda$ -calculus. Journal London Mathematical Society (2), 12(3):361–370, 1975.
[27] Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Degrees of extensionality in the theory of Böhm trees and Sallé’s conjecture. Log. Methods Comput. Sci., 15(1), 2019. doi:10.23638/LMCS-15(1:6)2019.
[28] Bart Jacobs. Semantics of lambda-I and of other substructure lambda calculi. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 195–208. Springer, 1993. doi:10.1007/BFB0037107.
[29] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculi and Böhm models. In Jieh Hsiang, editor, Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings, volume 914 of Lecture Notes in Computer Science, pages 257–270. Springer, 1995. doi:10.1007/3-540-59200-8_62.
[30] Jeroen Ketema, Stefan Blom, Takahito Aoto, and Jakob Grue Simonsen. Rewriting Transfinite Terms, pages 129–144. Lulu Press Inc, United States, 2009.
[31] Jean-Jacques Lévy. An algebraic interpretation of the $\lambda\beta$ K-calculus; and an application of a labelled $\lambda$ -calculus. Theor. Comput. Sci., 2(1):97–114, 1976. doi:10.1016/0304-3975(76)90009-8.
[32] Giuseppe Longo. Set-theoretical models of $\lambda$ -calculus: theories, expansions, isomorphisms. Annals of Pure and Applied Logic, 24(2):153–188, 1983. doi:10.1016/0168-0072(83)90030-1.
[33] Stefania Lusin and Antonino Salibra. The lattice of lambda theories. J. Log. Comput., 14(3):373–394, 2004. doi:10.1093/LOGCOM/14.3.373.
[34] Giulio Manzonetto and Michele Pagani. Böhm’s Theorem for resource lambda calculus through Taylor Expansion. In C.-H. Luke Ong, editor, Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690 of Lecture Notes in Computer Science, pages 153–168. Springer, 2011. doi:10.1007/978-3-642-21691-6_14.
[35] Giulio Manzonetto, Andrew Polonsky, Alexis Saurin, and Jakob Grue Simonsen. The fixed point property and a technique to harness double fixed point combinators. J. Log. Comput., 29(5):831–880, 2019. doi:10.1093/LOGCOM/EXZ013.
[36] Paul-André Melliès. Higher-order parity automata. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12. IEEE Computer Society, 2017. doi:10.1109/LICS.2017.8005077.
[37] James Hiram Morris. Lambda calculus models of programming languages. Phd thesis, Massachusetts Institute of Technology (MIT), 1968.
[38] Federico Olimpieri and Lionel Vaux Auclair. On the Taylor expansion of $\lambda$ -terms and the groupoid structure of their rigid approximants. Logical Methods in Computer Science, 18, 2022. doi:10.46298/lmcs-18(1:1)2022.
[39] Michele Pagani and Paolo Tranquilli. Parallel reduction in resource lambda-calculus. In Zhenjiang Hu, editor, Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, volume 5904 of Lecture Notes in Computer Science, pages 226–242. Springer, 2009. doi:10.1007/978-3-642-10672-9_17.
[40] Simona Ronchi Della Rocca. Characterization theorems for a filter lambda model. Inf. Control., 54(3):201–216, 1982. doi:10.1016/S0019-9958(82)80022-3.
[41] Dana S. Scott. Continuous lattices. In Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97–136. Springer, 1972.
[42] Paula Severi and Fer-Jan de Vries. The infinitary lambda calculus of the infinite $\eta$ -Böhm trees. Math. Struct. Comput. Sci., 27(5):681–733, 2017. doi:10.1017/S096012951500033X.
[43] Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
[44] Steffen van Bakel. Complete restrictions of the intersection type discipline. Theor. Comput. Sci., 102(1):135–163, 1992. doi:10.1016/0304-3975(92)90297-S.
[45] Steffen van Bakel, Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Fer-Jan de Vries. Intersection types for lambda-trees. Theor. Comput. Sci., 272(1-2):3–40, 2002. doi:10.1016/S0304-3975(00)00346-7.
[46] Lionel Vaux. Normalizing the Taylor expansion of non-deterministic $\lambda$ -terms, via parallel reduction of resource vectors. Logical Methods in Computer Science, 15, 2019. doi:10.23638/LMCS-15(3:9)2019.
[47] Christopher P. Wadsworth. The relation between computational and denotational properties for Scott’s $\mathcal{D}_{\infty}$ -models of the lambda-calculus. SIAM J. Comput., 5(3):488–521, 1976. doi:10.1137/0205036.
[48] Christopher P. Wadsworth. Approximate reduction and lambda calculus models. SIAM J. Comput., 7(3):337–356, 1978. doi:10.1137/0207028.

[bib.bib1] [1] Sandra Alves and Mário Florido. Structural rules and algebraic properties of intersection types. In Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu, editors, Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings, volume 13572 of Lecture Notes in Computer Science, pages 60–77. Springer, 2022. doi:10.1007/978-3-031-17715-6_6.

[bib.bib2] [2] Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proceedings of the ACM on Programming Languages, 4(POPL):1–23, 2019. doi:10.1145/3371069.

[bib.bib3] [3] Henk Barendregt. The type free lambda calculus. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 1091–1132. North-Holland, Amsterdam, 1977.

[bib.bib4] [4] Henk Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1984.

[bib.bib5] [5] Henk Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite. College Publications, 2022. URL: https://www.collegepublications.co.uk/logic/mlf/?00035.

[bib.bib6] [6] Stefano Berardi and Ugo de’Liguoro. Non-monotonic pre-fix points and learning. Fundam. Informaticae, 150(3-4):259–280, 2017. doi:10.3233/FI-2017-1470.

[bib.bib7] [7] Alessandro Berarducci. Infinite $\lambda$ -calculus and non-sensible models. In Marcel Dekker, editor, Logic and Algebra, volume 180, pages 339–377, New York, 1996. Presented to the conference in honour of Roberto Magari, Pontignano 1994.

[bib.bib8] [8] Flavien Breuvart, Giulio Manzonetto, and Domenico Ruoppolo. Relational graph models at work. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:2)2018.

[bib.bib9] [9] Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. Exponentials with infinite multiplicities. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 170–184. Springer, 2010. doi:10.1007/978-3-642-15205-4_16.

[bib.bib10] [10] Rémy Cerda. Taylor Approximation and Infinitary $\lambda$ -Calculi. Phd thesis, Aix-Marseille Université, 2024. URL: https://hal.science/tel-04664728.

[bib.bib11] [11] Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana trees and Taylor expansion for the $\lambda$ I-calculus. No variable gets left behind or forgotten!, 2025. Version of this paper with additional proofs in an appendix. arXiv:2505.06193.

[bib.bib12] [12] Rémy Cerda and Lionel Vaux Auclair. Finitary simulation of infinitary $\beta$ -reduction via Taylor expansion, and applications. Logical Methods in Computer Science, 19, 2023. doi:10.46298/lmcs-19(4:34)2023.

[bib.bib13] [13] Alonzo Church. The calculi of lambda conversion. Princeton University Press, 1941.

[bib.bib14] [14] Lukasz Czajka. A new coinductive confluence proof for infinitary lambda calculus. Log. Methods Comput. Sci., 16(1), 2020. doi:10.23638/LMCS-16(1:31)2020.

[bib.bib15] [15] Daniel de Carvalho and Lorenzo Tortora de Falco. The relational model is injective for multiplicative exponential linear logic (without weakenings). Ann. Pure Appl. Log., 163(9):1210–1236, 2012. doi:10.1016/J.APAL.2012.01.004.

[bib.bib16] [16] Daniel de Carvalho and Lorenzo Tortora de Falco. A semantic account of strong normalization in linear logic. Inf. Comput., 248:104–129, 2016. doi:10.1016/J.IC.2015.12.010.

[bib.bib17] [17] Aloÿs Dufour and Damiano Mazza. Böhm and Taylor for all! In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, volume 299 of LIPIcs, pages 29:1–29:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.FSCD.2024.29.

[bib.bib18] [18] Lavinia Egidi, Furio Honsell, and Simona Ronchi Della Rocca. Operational, denotational and logical descriptions: a case study. Fundam. Informaticae, 16(1):149–169, 1992.

[bib.bib19] [19] Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1–41, 2003. doi:10.1016/S0304-3975(03)00392-X.

[bib.bib20] [20] Thomas Ehrhard and Laurent Regnier. Böhm trees, Krivine’s machine and the Taylor expansion of lambda-terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, Logical Approaches to Computational Barriers (CiE 2006), pages 186–197, 2006. doi:10.1007/11780342_20.

[bib.bib21] [21] Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2):347–372, 2008. doi:10.1016/j.tcs.2008.06.001.

[bib.bib22] [22] Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop. Highlights in infinitary rewriting and lambda calculus. Theor. Comput. Sci., 464:48–71, 2012. doi:10.1016/J.TCS.2012.08.018.

[bib.bib23] [23] Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In 14th Symposium on Logic in Computer Science, 1999. doi:10.1109/lics.1999.782615.

[bib.bib24] [24] Silvia Ghilezan. Strong normalization and typability with intersection types. Notre Dame J. Formal Log., 37(1):44–52, 1996. doi:10.1305/NDJFL/1040067315.

[bib.bib25] [25] Furio Honsell and Marina Lenisa. Some results on the full abstraction problem for restricted lambda calculi. In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS’93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings, volume 711 of Lecture Notes in Computer Science, pages 84–104. Springer, 1993. doi:10.1007/3-540-57182-5_6.

[bib.bib26] [26] J. Martin E. Hyland. A syntactic characterization of the equality in some models for the $\lambda$ -calculus. Journal London Mathematical Society (2), 12(3):361–370, 1975.

[bib.bib27] [27] Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Degrees of extensionality in the theory of Böhm trees and Sallé’s conjecture. Log. Methods Comput. Sci., 15(1), 2019. doi:10.23638/LMCS-15(1:6)2019.

[bib.bib28] [28] Bart Jacobs. Semantics of lambda-I and of other substructure lambda calculi. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 195–208. Springer, 1993. doi:10.1007/BFB0037107.

[bib.bib29] [29] Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculi and Böhm models. In Jieh Hsiang, editor, Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings, volume 914 of Lecture Notes in Computer Science, pages 257–270. Springer, 1995. doi:10.1007/3-540-59200-8_62.

[bib.bib30] [30] Jeroen Ketema, Stefan Blom, Takahito Aoto, and Jakob Grue Simonsen. Rewriting Transfinite Terms, pages 129–144. Lulu Press Inc, United States, 2009.

[bib.bib31] [31] Jean-Jacques Lévy. An algebraic interpretation of the $\lambda\beta$ K-calculus; and an application of a labelled $\lambda$ -calculus. Theor. Comput. Sci., 2(1):97–114, 1976. doi:10.1016/0304-3975(76)90009-8.

[bib.bib32] [32] Giuseppe Longo. Set-theoretical models of $\lambda$ -calculus: theories, expansions, isomorphisms. Annals of Pure and Applied Logic, 24(2):153–188, 1983. doi:10.1016/0168-0072(83)90030-1.

[bib.bib33] [33] Stefania Lusin and Antonino Salibra. The lattice of lambda theories. J. Log. Comput., 14(3):373–394, 2004. doi:10.1093/LOGCOM/14.3.373.

[bib.bib34] [34] Giulio Manzonetto and Michele Pagani. Böhm’s Theorem for resource lambda calculus through Taylor Expansion. In C.-H. Luke Ong, editor, Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690 of Lecture Notes in Computer Science, pages 153–168. Springer, 2011. doi:10.1007/978-3-642-21691-6_14.

[bib.bib35] [35] Giulio Manzonetto, Andrew Polonsky, Alexis Saurin, and Jakob Grue Simonsen. The fixed point property and a technique to harness double fixed point combinators. J. Log. Comput., 29(5):831–880, 2019. doi:10.1093/LOGCOM/EXZ013.

[bib.bib36] [36] Paul-André Melliès. Higher-order parity automata. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12. IEEE Computer Society, 2017. doi:10.1109/LICS.2017.8005077.

[bib.bib37] [37] James Hiram Morris. Lambda calculus models of programming languages. Phd thesis, Massachusetts Institute of Technology (MIT), 1968.

[bib.bib38] [38] Federico Olimpieri and Lionel Vaux Auclair. On the Taylor expansion of $\lambda$ -terms and the groupoid structure of their rigid approximants. Logical Methods in Computer Science, 18, 2022. doi:10.46298/lmcs-18(1:1)2022.

[bib.bib39] [39] Michele Pagani and Paolo Tranquilli. Parallel reduction in resource lambda-calculus. In Zhenjiang Hu, editor, Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, volume 5904 of Lecture Notes in Computer Science, pages 226–242. Springer, 2009. doi:10.1007/978-3-642-10672-9_17.

[bib.bib40] [40] Simona Ronchi Della Rocca. Characterization theorems for a filter lambda model. Inf. Control., 54(3):201–216, 1982. doi:10.1016/S0019-9958(82)80022-3.

[bib.bib41] [41] Dana S. Scott. Continuous lattices. In Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97–136. Springer, 1972.

[bib.bib42] [42] Paula Severi and Fer-Jan de Vries. The infinitary lambda calculus of the infinite $\eta$ -Böhm trees. Math. Struct. Comput. Sci., 27(5):681–733, 2017. doi:10.1017/S096012951500033X.

[bib.bib43] [43] Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.

[bib.bib44] [44] Steffen van Bakel. Complete restrictions of the intersection type discipline. Theor. Comput. Sci., 102(1):135–163, 1992. doi:10.1016/0304-3975(92)90297-S.

[bib.bib45] [45] Steffen van Bakel, Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Fer-Jan de Vries. Intersection types for lambda-trees. Theor. Comput. Sci., 272(1-2):3–40, 2002. doi:10.1016/S0304-3975(00)00346-7.

[bib.bib46] [46] Lionel Vaux. Normalizing the Taylor expansion of non-deterministic $\lambda$ -terms, via parallel reduction of resource vectors. Logical Methods in Computer Science, 15, 2019. doi:10.23638/LMCS-15(3:9)2019.

[bib.bib47] [47] Christopher P. Wadsworth. The relation between computational and denotational properties for Scott’s $\mathcal{D}_{\infty}$ -models of the lambda-calculus. SIAM J. Comput., 5(3):488–521, 1976. doi:10.1137/0205036.

[bib.bib48] [48] Christopher P. Wadsworth. Approximate reduction and lambda calculus models. SIAM J. Comput., 7(3):337–356, 1978. doi:10.1137/0207028.

	$\displaystyle\mathcal{X}_{{\sf Y}f}$	$\displaystyle=\{f1_{\{f\}}\}\cup\{f[t_{0},\dots,t_{n}]\ \|\ n\in\mathbb{N},\ t_% {0},\dots,t_{n}\in\mathcal{X}_{{\sf Y}f}\},$
	$\displaystyle\mathcal{X}_{\text{\scalebox{0.8}{\faBible}}_{\,l}f}$	$\displaystyle=\{f1_{\{f,l\}}\}\cup\{f[t_{0},\dots,t_{n}]\ \|\ n\in\mathbb{N},\ % t_{0},\dots,t_{n}\in\mathcal{X}_{\text{\scalebox{0.8}{\faBible}}_{\,l}f}\}.$

Ohana Trees and Taylor Expansion for the λI-Calculus

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Böhm trees and Taylor expansion for the λ⁢𝖨-calculus

Related works

2 Preliminaries

2.1 The λ-calculus, in a nutshell

Example 1.

▶ Remark 2.

Definition 3.

Definition 4.

Example 5.

2.2 The λ⁢𝖨-calculus

Definition 6.

▶ Remark 7.

Definition 8.

Theorem 9.

3 Ohana trees

3.1 The coinductive definition

Definition 10.

Example 11.

▶ Remark 12.

3.2 The associated approximation theory

Definition 13.

Lemma 14.

Definition 15.

▶ Remark 16.

Example 17.

Lemma 18.

Proof.

Proposition 19.

Proof.

Theorem 20.

Proof.

4 A resource calculus with memory

4.1 λ⁢𝖨-resource expressions and λ⁢𝖨-resource sums

Definition 21.

▶ Remark 22.

Example 23.

Definition 24.

4.2 Memory substitution and resource substitution

Definition 25.

Definition 26.

Definition 27.

Lemma 28.

Proof.

Lemma 29.

Proof.

4.3 The operational semantics

Definition 30.

Example 31.

Theorem 32.

Proof.

5 Taylor approximation for Ohana trees

5.1 The Taylor approximation

Notation 33.

Definition 34.

▶ Remark 35.

Example 36.

Notation 37.

Theorem 38 (Commutation).

Lemma 39.

Proof.

Lemma 40.

Proof.

Lemma 41 (Monotonicity of 𝒯𝗆⁢(−)).

Proof.

Lemma 42 (Simulation of →β).

Proof.

Lemma 43.

Ohana Trees and Taylor Expansion
for the λI-Calculus

Böhm trees and Taylor expansion for the $\lambda{\sf I}$ -calculus

2.1 The $\lambda$ -calculus, in a nutshell

$\blacktriangleright$ Remark 2.

2.2 The $\lambda{\sf I}$ -calculus

$\blacktriangleright$ Remark 7.

$\blacktriangleright$ Remark 12.

$\blacktriangleright$ Remark 16.

4.1 $\lambda{\sf I}$ -resource expressions and $\lambda{\sf I}$ -resource sums

$\blacktriangleright$ Remark 22.

$\blacktriangleright$ Remark 35.

Lemma 41 (Monotonicity of $\mathcal{T}_{\mathsf{m}}(-)$ ).

Lemma 42 (Simulation of $\rightarrow_{\beta}$ ).

5.2 The $\lambda{\sf I}$ -theory of Ohana trees

6.1 Further work on the $\lambda{\sf I}$ -calculus

6.2 What about the full $\lambda$ -calculus?