# Interaction Equivalence

Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, Gabriele Vanoni

► To cite this version:

Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, Gabriele Vanoni. Interaction Equivalence. Proceedings of the ACM on Programming Languages, 2025, 9 (POPL), pp.1627-1656. 10.1145/3704891. hal-05454681

HAL Id: hal-05454681

https://hal.science/hal-05454681v1

Submitted on 12 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Interaction Equivalence

BENIAMINO ACCATTOLI, Inria - École Polytechnique, France

ADRIENNE LANCELOT, Inria - École Polytechnique - Université Paris Cité, France

GIULIO MANZONETTO, Université Paris Cité, France

GABRIELE VANONI, Université Paris Cité, France

Contextual equivalence is the *de facto* standard notion of program equivalence. A key theorem is that contextual equivalence is an *equational theory*. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does *not* induce an equational theory, for an apparently essential reason: cost is not invariant under reduction.

In the paradigmatic case of the untyped $\lambda$-calculus, we introduce *interaction equivalence*. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but—crucially—ignore their internal steps. We prove that interaction equivalence is an equational theory and characterize it as $\mathcal{B}$, the well-known theory induced by Böhm tree equality. It is the first observational characterization of $\mathcal{B}$ obtained *without* enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types.

CCS Concepts: • **Theory of computation** → **Lambda calculus**; **Denotational semantics**.

Additional Key Words and Phrases: Lambda calculus, program equivalences, Böhm trees.

## ACM Reference Format:

Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, and Gabriele Vanoni. 2025. Interaction Equivalence. *Proc. ACM Program. Lang.* 9, POPL, Article 55 (January 2025), 30 pages. https://doi.org/10.1145/3704891

## 1 Introduction

A cornerstone of the theory of programming languages is the acceptance of contextual equivalence as a meaningful notion—if not as *the* notion—of program equivalence. Introduced by Morris [1968] to study the untyped $\lambda$-calculus, contextual equivalence has the advantage that its definition is almost language-agnostic. Given a language $\mathcal{L}$, one simply needs the notion of contexts $C$ of $\mathcal{L}$, usually defined as terms with a single occurrence of a special additional constant $\langle \cdot \rangle$ (the *hole* of the context), and a chosen predicate $\downarrow$ of *observation* for $\mathcal{L}$, typically some notion of termination, which is the only language-specific ingredient. Then, contextual equivalence is defined as:

$$ t \equiv^{\text{ctx}} u \quad \text{if for all contexts } C. \quad [C(t) \downarrow \Leftrightarrow C(u) \downarrow] $$

Contextual equivalence embodies a *black box* behavioral principle with respect to termination. Nothing is said about the structure of $t$ and $u$, it is only prescribed that any use of $t$ in a larger program can be replaced by $u$ (and vice-versa) without affecting the observables. One of the most studied contextual equivalences is *head contextual equivalence* $\equiv_{\text{h}}^{\text{ctx}}$ for the untyped $\lambda$-calculus [Barendregt 1984], where one observes termination of head reduction $\rightarrow_{\text{h}}$. Another contextual equivalence

Authors' Contact Information: Beniamino Accattoli, Inria - École Polytechnique, Palaiseau, France, beniamino.accattoli@inria.fr; Adrienne Lancelot, Inria - École Polytechnique - Université Paris Cité, Palaiseau, France, lancelot@irif.fr; Giulio Manzonetto, Université Paris Cité, Paris, France, gmanzone@irif.fr; Gabriele Vanoni, Université Paris Cité, Paris, France, gabriele.vanoni@irif.fr.

<figure><img src="image_2.png" /></figure>

This work is licensed under a Creative Commons Attribution 4.0 International License.

© 2025 Copyright held by the owner/author(s).

ACM 2475-1421/2025/1-ART55

https://doi.org/10.1145/3704891
that was studied at length is the one of Plotkin's PCF [1977], where the observation is termination on the same value of ground type, typically a natural number. Both played crucial roles in the historical development of denotational semantics of programming languages.

Contextual equivalence is also relevant in more applied settings. The typical example being program transformations at work in compilers, for which contextual equivalence guarantees a strong form of soundness, see, for instance, the survey by Patrignani et al. [2019].

*Equational Contextual Equivalence.* In order for contextual equivalence $\equiv^{\text{ctx}}$ to be a proper semantical notion, one actually has to show that it is an *equational theory* for $\mathcal{L}$. This means that the following two properties must be satisfied:

(1) Compatibility: $\equiv^{\text{ctx}}$ is stable under context closure, that is, $t \equiv^{\text{ctx}} u$ implies $C\langle t \rangle \equiv^{\text{ctx}} C\langle u \rangle$ for all contexts C, and;

(2) Invariance: $\equiv^{\text{ctx}}$ includes $\beta$-conversion $=_{\beta}$, that is, if $t =_{\beta} u$ then $t \equiv^{\text{ctx}} u$.

While compatibility holds by definition, invariance is a non-trivial theorem, because of the universal quantification on contexts in $\equiv^{\text{ctx}}$, which is notoriously hard to manage. For head contextual equivalence $\equiv_{\text{h}}^{\text{ctx}}$, for instance, a rewriting-based proof of the invariance property requires to prove the confluence of $\beta$-reduction and various non-trivial properties of head reduction<fnref n="1" />.

An equational theory for $\mathcal{L}$ can be seen as a semantics for $\mathcal{L}$. The abstract requirement defining denotational models is that their induced equivalence<fnref n="2" /> is an equational theory. Notably, head contextual equivalence $\equiv_{\text{h}}^{\text{ctx}}$ is exactly the equational theory of Scott's $\mathcal{D}_{\infty}$ model [1972], the first model of the untyped $\lambda$-calculus.

*Termination vs Time Cost, Equationally.* It is natural to wonder whether contextual equivalence can be refined by replacing the termination predicate $\downarrow$ with a finer one $\downarrow^k$ indicating termination in $k$ evaluation steps. Intuitively, the number of evaluation steps is taken as a time cost model. With the compiler analogy in mind, it is indeed natural to ask that a program transformation preserves the time behavior. This refinement is exactly Sands' notion of *cost equivalence*, the symmetric form of his more famous *improvement preorder* [1996a; 1996b; 1999]:

$$t \equiv^{\text{cost}} u \quad \text{if for all contexts } C, \exists k \ge 0. \quad [C\langle t \rangle \downarrow^k \Leftrightarrow C\langle u \rangle \downarrow^k]$$

Cost equivalence falls short, however, of being a refinement of contextual equivalence. The price to pay for the added quantitative information is that it can no longer be seen as a semantics, that is, it is *not* an equational theory. The reason is both simple and deep. It is simple because (in, say, the $\lambda$-calculus) if $t \to_{\beta} u$, then $C\langle u \rangle$ might take one step less to terminate than $C\langle t \rangle$, so $\beta$-conversion $=_{\beta}$ cannot be included in cost equivalence $\equiv^{\text{cost}}$, breaking the invariance of equational theories.

*Internal and External.* The issue is deep as it reflects a more general tension between quantitative intensional properties such as time cost, which by their nature cannot be invariant under evaluation, and semantical notions such as equational theories, that are expected to hide the computational process. More generally, one might identify two perspectives on programs. The *internal view* studies programs in isolation, and it is concerned with qualitative properties such as, e.g., termination, confluence, productivity, or quantitative properties such as time or space cost. The *external view*, instead, studies how programs *interact* with other programs, as it is the case for contextual equ valences, labelled transition systems (LTSs), or process calculi. Usually, the external view hides the internal dynamics of programs, for instance via the invariance requirement for contextual equivalence, or via the silent $\tau$ transitions of LTSs.

<footnote n="1">¹For an overview of such a proof, see Appendix A of the longer version on arXiv [Accattoli et al. 2024].</footnote>

<footnote n="2">²The equivalence induced by a model $\mathcal{M}$ is defined as $t =_{\mathcal{M}} u$ if $\llbracket t \rrbracket = \llbracket u \rrbracket$, where $\llbracket \cdot \rrbracket$ is the interpretation in the model.</footnote>
Böhm trees up to possibly infinite $\eta$-equivalence. A natural question then arises: is there an explicit description of interaction equivalence? Does it correspond to anything already known?

*Interaction Equivalence and Böhm Trees.* The second contribution of our work is the answer to these two questions. We prove that interaction equivalence is exactly the well-known equational theory $\mathcal{B}$ induced by Böhm tree equality. In particular, interaction equivalence is *not* extensional, that is, it does not validate any form of $\eta$-equivalence, given that $x$ and $\lambda y(xy)$ clearly have a different number of interactions with any context providing an argument. Therefore, interaction equivalence $\equiv^{\text{int}}$ has a simpler explicit description than head contextual equivalence $\equiv_{\text{h}}^{\text{ctx}}$, and provides an operational insight about $\eta$-equivalence. The failure of $\eta$-equivalence also reveals that, despite the analogy, our framework is not that close to game semantics, where $\eta$ is naturally validated unless additional constraints are imposed to avoid it, as in [Ker et al. 2003; Ong and Di Gianantonio 2002].

Our results actually turn out to solve an open problem in the semantical theory of the untyped $\lambda$-calculus, namely the problem of finding a satisfying description of (non-extensional) Böhm tree equality $\mathcal{B}$ as an observational equivalence. Partial solutions have been presented in the literature and are discussed among related works, in Section 9. Ours is the first solution that does not require adding any extra features such as concurrency or non-determinism, but only refining the analysis.

*Normal Form Bisimilarities.* Some readers might prefer a coinductive formulation of the problem. The equational theory $\mathcal{B}$, indeed, corresponds to head normal form bisimilarity, as shown by Lassen [1999], building over Sangiorgi's work [1994]. Normal form bisimilarities are known to be sound but—in general—*not* complete for contextual equivalences. The open problem from the literature then might be recast as follows: is there an observational equivalence for which normal form bisimilarities are complete? We show that, for the head case, interaction equivalence is the answer.

*Technical Development.* Our results are proved via new interaction-based refinements of standard proof methods in the literature, namely the Böhm-out technique and multi types, overviewed in the next subsection. While the proofs are non-trivial, we believe that they are compact and neat, hopefully reassuring that the introduced framework is not *ad-hoc*.

*Proofs.* Some proofs are omitted; they are in the proof appendix on arXiv [Accattoli et al. 2024].

## Overview of the Proof Techniques

In the study of program equivalences, proving the inclusion of an equivalence into another one is always challenging. As it is customary, we study preorders rather than equivalences, and prove the equality of the Böhm preorder $\sqsubseteq_{\mathcal{B}}$ and the interaction preorder $\sqsubseteq^{\text{int}}$ by showing the two inclusions.

*Proof Technique 1: Böhm-Out.* For $\sqsubseteq^{\text{int}} \subseteq \sqsubseteq_{\mathcal{B}}$, we prove the contrapositive: if $t$ and $u$ have different Böhm trees then they are not interaction equivalent. We adapt the Böhm-out technique at work in Böhm's separation theorem [1968]—a classic result of the untyped $\lambda$-calculus—thus building a context that separates $t$ and $u$. The original technique, used also more recently in [Barendregt and Manzonetto 2022; Boudol and Laneve 1996; Dezani-Ciancaglini et al. 1998; Intrigila et al. 2019], cannot distinguish $\eta$-equivalent terms. We refine it by counting interaction steps: when interacting with a context, $\eta$-equivalent terms give rise to different amounts of interaction.

*Proof Technique 2: Multi Types.* For the inclusion $\sqsubseteq_{\mathcal{B}} \subseteq \sqsubseteq^{\text{int}}$, we use a different technique. The main tool is a new multi type system (also known as non-idempotent intersection types) for the checkers calculus. Multi types are an established tool for the study of untyped $\lambda$-calculi, mediating between operational and denotational studies; see [Bucciarelli et al. 2017] for an introduction.
<figure><img src="image_3.png" /><figcaption>Fig. 1. The $\lambda$-calculus. $\Lambda$ is the set of $\lambda$-terms, $C$ the class of contexts, $\mathcal{H}$ the subclass of head contexts.</figcaption></figure>

Similarly to intersection types, they characterize various termination properties, in the sense that $t$ “converges” if and only if $t$ is typable$^3$. In contrast to intersection types, however, multi types are *quantitative*, which can be expressed in at least two ways. Firstly, the fact that typability implies (head) termination can be proved easily using as a decreasing measure the size of type derivations, while intersection types require more involved techniques. Secondly, multi types allow one to extract a bound of the number of head steps to normal form, as first shown by de Carvalho [2007, 2018], which is impossible with (idempotent) intersection types.

As a disclaimer, please note that multi types are a theoretical tool not meant to be used in real life programming languages, since typability in multi type systems is an undecidable property. Rather, they provide handy type-theoretic presentations of denotational models.

We prove that our multi type system for the checkers calculus characterizes head termination, and we use the type system to introduce a type preorder $\sqsubseteq^{\bullet}_{\text{typ}}$ and show that $\sqsubseteq_{\mathcal{B}} \subseteq \sqsubseteq^{\bullet}_{\text{typ}} \subseteq \sqsubseteq^{\text{int}}$. The first of these two inclusions is proved exploiting the quantitative properties of the multi type system. The second inclusion requires more, namely to characterize the multi type judgements from which one can measure the *exact* number of interaction steps, rather than simply providing a bound. For that, we adapt the *tight* technique of Accattoli et al. [2020], in its turn refining previous work by de Carvalho [2007, 2018]. A possibly interesting point is that the literature uses the tight technique to measure the number of internal steps, while here we use it dually, for measuring interaction steps. The following diagram sums up the technical development:

<figure><img src="image_4.png" /></figure>

In fact, we end up providing *two* characterizations of interaction equivalence/preorder, one as Böhm trees and one as multi types. Our first main result, namely the fact that interaction equivalence is an equational theory (Cor. 3.12(3)), is also proved using tight multi types. Essentially, it is obtained by symmetry from the inclusion $\sqsubseteq^{\bullet}_{\text{typ}} \subseteq \sqsubseteq^{\text{int}}$ above and the fact that $\sqsubseteq^{\bullet}_{\text{typ}}$ is an inequational theory.

## 2 The $\lambda$-Calculus

To keep this article as self-contained as possible, we summarize some definitions and results concerning $\lambda$-calculus that we shall use in the paper. For more information, see [Barendregt 1984].

**DEFINITION 2.1.** The syntax and rewriting rules of $\lambda$-calculus are given in Fig. 1.

**$\lambda$-Terms and Contexts.** The set $\Lambda$ of $\lambda$-terms is constructed over a countable set $VAR$ of variables. We assume that application associates to the left and has a higher precedence than abstraction. Given $k, n \ge 0$ and $t, u, s_1, \dots, s_k \in \Lambda$, we write $\lambda\bar{x}.t$ as an abbreviation of $\lambda x_1 \dots x_n.t$, and $t\bar{s}$ for $ts_1 \dots s_k$. For instance, $\lambda xywz.x y(wz)$ stands for $\lambda x.(\lambda y.(\lambda w.(\lambda z.((xy)(wz))))$.

<footnote>$^3$The notion of convergence that is captured depends on the system that is considered. Here, we consider head normalization.</footnote>
*Contextual Preorders and Equivalences.* A nowadays standard notion in the study of programming languages and λ-calculi is contextual equivalence, and its asymmetric variant of contextual preorder. The idea is to observe the termination of λ-terms when plugged in the same context. Thus, they depend on a notion of termination. In this paper, we focus on termination of head reduction.

**DEFINITION 2.5.** The (head) contextual preorder $\sqsubseteq^{\text{ctx}}$ on λ-terms is defined as follows:

$$ t \sqsubseteq^{\text{ctx}} u \quad \text{if for all contexts } C. \quad [C\langle t \rangle \Downarrow_h \Rightarrow C\langle u \rangle \Downarrow_h] $$

The associated (head) contextual equivalence is defined by setting $t \equiv^{\text{ctx}} u$ if $t \sqsubseteq^{\text{ctx}} u$ and $u \sqsubseteq^{\text{ctx}} t$.

Often the literature requires C to be a closing context, that is, such that both $C\langle t \rangle$ and $C\langle u \rangle$ are closed. In the ordinary λ-calculus, adding/removing the closing requirement does not change the defined relation, which is why we do not add it. It turns out that the head contextual preorder provides an inequational λ-theory.

**THEOREM 2.6 ([BARENDREGT 1984]).** The head contextual preorder $\sqsubseteq^{\text{ctx}}$ is an inequational λ-theory. Moreover, it is consistent and extensional.

As mentioned in the introduction, the proof of the previous theorem is non-trivial. Proving that $\beta$-conversion $=\beta$ is included in $\sqsubseteq^{\text{ctx}}$ indeed is not immediate, because of the famously fastidious universal quantification on contexts in $\sqsubseteq^{\text{ctx}}$. A rewriting-based proof requires the use of both confluence of $\beta$ and the untyped normalization theorem of head reduction (if $t \xrightarrow{\beta}^* u$ and $u$ is normal for head reduction, then $t$ is head normalizing). For an overview, see Appendix A of the longer version on arXiv [Accattoli et al. 2024]. Similarly, a rewriting-based proof that $\eta$-conversion $=\eta$ is included in $\sqsubseteq^{\text{ctx}}$ also rests on non-trivial theorems about $\eta$. Also in this case, for an overview see Appendix A of the longer version on arXiv [Accattoli et al. 2024].

Semantic proofs are possible but not easy anyway, as they rest on soundness of the model. For the similar case of interaction equivalence, we shall develop a semantic proof.

*Background and Notable Variants.* The head contextual preorder has been studied in-depth because it captures the (in)equational theory of Scott's denotational model $D_\infty$ [Scott 1972], the first model of the untyped λ-calculus. The preorder $\sqsubseteq^{\text{ctx}}$ is also the maximal contextual preorder of interest: any strictly larger inequational λ-theory is inconsistent [Barendregt and Manzonetto 2022, Lemma 12.5]. In 1976, Hyland and Wadsworth have shown that the associated equivalence $\equiv^{\text{ctx}}$ coincides with Böhm trees equality up to infinite $\eta$-expansions (Cf. Theorem 4.7, below).

Another relevant contextual preorder is obtained by considering termination with respect to $\beta$-reduction, instead of head reduction. This alternative preorder was originally introduced in Morris's PhD thesis [1968], but has been the subject of fewer investigations than the head one (until recently, see [Intrigila et al. 2019] and [Barendregt and Manzonetto 2022, Ch. 12]). Hyland [1975] showed that the associated equivalence captures Böhm trees equality up to finite $\eta$-expansions.

# 3 The Checkers Calculus

In this section we introduce the *checkers calculus*, obtained from the λ-calculus by duplicating the abstraction and application constructors, that now both come in white and black dresses.

**DEFINITION 3.1.** The syntax and operational semantics of the checkers calculus are defined in Fig. 2.

*Black and White Constructors.* The constructors of abstraction and application receive a tag, called *player*, that can be either white $\circ$ or black $\bullet$. The terms populating the set $\Lambda_\circ$ are called *checkers terms*, and inherit the notions of free variables, $\alpha$-conversion, and substitution from λ-calculus. Note that variables do not receive a player tag. The main reason is simplicity: this way, we do not need to enforce the uniform tagging of all the occurrences of the same variable.
<table><caption>Fig. 2. The checkers calculus.</caption><thead><tr><th>TERMS AND CONTEXTS</th><th>BETA RULES AND REDUCTIONS</th></tr></thead><tbody><tr><td>PLAYERS p, q ::= ◦ | ●</td><td>SILENT (λ<sub>p</sub>x.t) .<sup>P</sup> u ↦→ β<sub>τ</sub> t{x := u}</td></tr><tr><td>TERMS Λ<sub>o</sub> ∋ t, u, s ::= x | λ<sub>p</sub>x.t | t .<sup>P</sup> u</td><td>INTERACTION (λ<sub>p</sub>x.t) .<sup>P</sup> u ↦→ β<sub>e</sub> t{x := u}</td></tr><tr><td>h<sub>o</sub>.-NFS h, h' ::= λ<sub>p̄</sub>x̄.y .<sup>q<sub>1</sub>...q<sub>k</sub></sup> t<sub>1</sub> ... t<sub>k</sub></td><td>SILENT β → β<sub>τ</sub> ::= C<sub>o</sub>.<sup>⟨ ↦→ β<sub>τ</sub> ⟩</sup><br>INTERACTION β → β<sub>e</sub> ::= C<sub>o</sub>.<sup>⟨ ↦→ β<sub>e</sub> ⟩</sup><br>CHECKERS β → β<sub>o</sub>. ::= → β<sub>τ</sub> ∪ → β<sub>e</sub></td></tr><tr><td>C<sub>o</sub> ∋ C ::= ⟨·⟩ | λ<sub>p</sub>x.C | C .<sup>P</sup> u | t .<sup>P</sup> C</td><td>SILENT HEAD → h<sub>τ</sub> ::= H<sub>o</sub>.<sup>⟨ ↦→ β<sub>τ</sub> ⟩</sup></td></tr><tr><td>H<sub>o</sub> ∋ H ::= λ<sub>p̄</sub>x̄.⟨·⟩ .<sup>q<sub>1</sub>...q<sub>k</sub></sup> t<sub>1</sub> ... t<sub>k</sub></td><td>INTERACTION HEAD → h<sub>e</sub> ::= H<sub>o</sub>.<sup>⟨ ↦→ β<sub>e</sub> ⟩</sup><br>CHECKERS HEAD → h<sub>o</sub>. ::= → h<sub>τ</sub> ∪ → h<sub>e</sub></td></tr></tbody></table>

**Notation 3.2.** When the players are actually specified, we simply denote the applications by $t ◦ u$ (and $t • u$) instead of $t ◦ u$ (and $t • u$). Hereafter, we often need to refer to constructors of a fixed but arbitrary player p, thus we use $λ_p x.t$ and $t .^P u$ for abstractions and applications of player p ∈ {◦, ●}. We also use $p^⊥$ to denote the opposite player, defined as $◦^⊥ := •$ and $•^⊥ := ◦$. In case of many consecutive abstractions or applications, we shorten the notations to $λ_{p̄} x.t$ and $t .^P ū$, respectively. The former is sometimes slightly expanded to $λ_{p_1...p_k} x_1...x_k . t$, and the latter to $t .^{p_1...p_k} u_1...u_k$.

**Checkers Contexts.** The class $C_o$ of checkers contexts, and the subclass $H_o$ of checkers head contexts are defined in Fig. 2. Definition 2.2 of contextual closure with respect to a class of contexts, generalizes to this setting in the obvious way. Checkers contexts shall play a key role in the definition of contextual preorders and equivalences on checkers terms (see Definition 3.7, below).

**Silent and Interaction Steps.** There are two kinds of colored $\beta$-redexes ($λ_p x.t$) .$^q$ u, the silent one and the interaction one, each one with its own $\beta$-rule. Silent redexes are $\beta$-redexes where the color of the abstraction p matches the color of the application q. Intuitively, these steps are internal to each player's world. In interaction redexes, instead, the color of the abstraction and the color of the application are different, i.e. p $\neq$ q. This represents the scenario where the two players interact with each other, which, from each player's perspective, amounts to interacting with the external world. Our focus shall be on the number of head interaction steps.

The internal/external dichotomy, and the idea of having two players are strong guiding intuitions but note that, in general, a checkers term can arbitrarily interleave black and white constructors: there is no neat frontier between the parts of a term corresponding to the two players. The key point is that, even if we start with cleanly separated black and white parts, they still end up mixing during the reduction.

**EXAMPLE 3.3.** Consider the black identity $I_o := λ_o x.x$ and the white term $D_o := λ_o y.λ_o x.x ◦ (y ◦ x)$.

(1) If the black identity is black-applied to $D_o$, then it gives rise to a silent step $I_o • D_o → β_τ D_o$, while if it is white-applied to $D_o$ then the step is an interaction one, namely $I_o ◦ D_o → β_e D_o$.

(2) $D_o • I_o • I_o → h_e (λ_o x.x ◦ (I_o ◦ x)) • I_o → β_e (λ_o x.x ◦ x) • I_o → h_e I_o • I_o → h_e I_o$.

**Basic Rewriting Properties.** As the $\lambda$-calculus, the checkers $\lambda$-calculus is an example of orthogonal higher-order rewriting system [Aczel 1978; Klop 1980; Nipkow 1991], that is a class of rewriting systems for which confluence always holds, because of the good shape of their rewriting rules. Similarly, the silent and interaction sub-relations $→ β_τ$ and $→ β_e$ are also confluent and commute.

**THEOREM 3.4 (CONFLUENCE).** Reductions $→ β_o$, $→ β_τ$, and $→ β_e$ are confluent.
Similarly, checkers head reduction inherits various expected properties of head reduction, such as determinism. In particular, we shall use the following immediate substitutivity property.

**LEMMA 3.5 (SUBSTITUTIVITY).** Let $t, t', u \in \Lambda_{\circ\bullet}$ and $R \in \{\beta_{\tau}, \beta_{e}, \beta_{\circ\bullet}, h_{\tau}, h_{e}, h_{\circ\bullet}\}$. If $t \to_R t'$ then $t\{x := u\} \to_R t'\{x := u\}$.

**$\eta$-Conversion.** Note that there are no checkers $\eta$-rules in Fig. 2. A key point in our work, indeed, is that $\eta$-conversion can change the number of interaction steps.

**EXAMPLE 3.6 (THE DELICATE ROLE OF $\eta$).** Consider the black $\eta$-expansion $1_{\bullet} := \lambda_{\bullet}x.\lambda_{\bullet}y.x \bullet y$ of the black identity $I_{\bullet}$ and the following diagram:

<figure><img src="image_5.png" /></figure>

It shows that $\eta$ changes the number of interaction steps. It also shows that standard properties of ordinary $\eta$ do not lift to the checkers case (see Appendix A on arXiv [Accattoli et al. 2024] for definitions): $\to_{\eta}$ cannot be postponed after $\to_{h_e}$, $\to_{\eta}$ and $\to_{h_e}$ do not commute, and adding $\eta$ to $\to_{\beta_{\circ\bullet}}$ breaks confluence.

**Big-Step Notation and Interaction Index.** Recall that $t \Downarrow_{h_e}$ stands for “t is $h_e$-normalizing”. We introduce the notation $t \Vdash_{h_e}^{\beta_{\circ\bullet}}$ for: t is $h_e$-normalizing and the number of head interaction steps $\to_{h_e}$ in its $h_e$-evaluation is $k$. Note that the number $k$ is well-defined because $\to_{h_e}$ is deterministic.

**Interaction Equivalence and Preorders.** We now introduce interaction equivalence $\equiv_{e}^{\text{ctx}}$ as a form of quantitative contextual equivalence for the checkers calculus. Similarly to weak similarity for labeled transition systems, $\equiv_{e}^{\text{ctx}}$ ignores silent head steps. The quantitative aspect is that it requires to preserve the number of interaction head steps. The richer quantitative setting in fact gives rise to two possible preorders, both generating $\equiv_{e}^{\text{ctx}}$ when symmetrized.

**DEFINITION 3.7 (CHECKERS INTERACTION PREORDERS AND EQUIVALENCE).** We define the interaction preorder $\sqsubseteq_{e}^{\text{ctx}}$, the interaction improvement (preorder) $\sqsubseteq_{e}^{\text{ctx-imp}}$, and the interaction equivalence $\equiv_{e}^{\text{ctx}}$ on checkers terms $t, u \in \Lambda_{\circ\bullet}$ as follows:

(i) $t \sqsubseteq_{e}^{\text{ctx}} u$ if $C\langle t \rangle \Vdash_{h_e}^{\beta_{\circ\bullet}}$ implies $C\langle u \rangle \Vdash_{h_e}^{\beta_{\circ\bullet}}$ for all checkers contexts $C \in C_{\circ\bullet}$ and $k \in \mathbb{N}$;

(ii) $t \sqsubseteq_{e}^{\text{ctx-imp}} u$ if $C\langle t \rangle \Vdash_{h_e}^{\beta_{\circ\bullet}}$ implies $C\langle u \rangle \Vdash_{h_e}^{\beta_{\circ\bullet}}$ with $k' \le k$, for all contexts $C \in C_{\circ\bullet}$ and $k \in \mathbb{N}$;

(iii) $t \equiv_{e}^{\text{ctx}} u$ is the equivalence relation induced by $\sqsubseteq_{e}^{\text{ctx}}$, that is, $t \equiv_{e}^{\text{ctx}} u$ if $t \sqsubseteq_{e}^{\text{ctx}} u$ and $u \sqsubseteq_{e}^{\text{ctx}} t$.

The interaction improvement $\sqsubseteq_{e}^{\text{ctx-imp}}$ adapts Sands' improvements [1996a; 1996b; 1999] to our up to silent steps setting. Note that $\sqsubseteq_{e}^{\text{ctx}} \subseteq \sqsubseteq_{e}^{\text{ctx-imp}}$. It is easy to see that the two new preorders are different, i.e. that $\sqsubseteq_{e}^{\text{ctx}} \subsetneq \sqsubseteq_{e}^{\text{ctx-imp}}$. Indeed, $I_{\bullet} \circ I_{\circ}$ $\sqsubseteq_{e}^{\text{ctx-imp}}$ $I_{\circ}$ but $I_{\bullet} \circ I_{\circ} \not\sqsubseteq_{e}^{\text{ctx}}$ $I_{\circ}$, as both checkers terms have $I_{\circ}$ as head normal form but $I_{\bullet} \circ I_{\circ}$ requires one more interaction step to reach it.

The interaction preorder $\sqsubseteq_{e}^{\text{ctx}}$ turns out to be more easily manageable than the interaction improvement $\sqsubseteq_{e}^{\text{ctx-imp}}$. Moreover, from the inclusion $\sqsubseteq_{e}^{\text{ctx}} \subseteq \sqsubseteq_{e}^{\text{ctx-imp}}$ we shall be able to transfer some properties of $\sqsubseteq_{e}^{\text{ctx}}$ to $\sqsubseteq_{e}^{\text{ctx-imp}}$. In this paper, then, we shall rather focus on $\sqsubseteq_{e}^{\text{ctx}}$.

**EXAMPLE 3.8.** Recall that $I_{\bullet}$ and $D_{\circ}$ have been defined in Ex. 3.3, and $1_{\bullet}$ in Ex. 3.6.

(i) $(\lambda_{\circ}x.x \circ x) \circ (\lambda_{\circ}x.x \circ x) \sqsubseteq_{e}^{\text{ctx}} I_{\bullet}$, because the former is not $h_{\circ\bullet}$-normalizable.

(ii) $I_{\bullet} \not\sqsubseteq_{e}^{\text{ctx}} 1_{\bullet}$ and $1_{\bullet} \not\sqsubseteq_{e}^{\text{ctx}} I_{\circ}$, as they are separated by $C = \langle\cdot\rangle \circ z \circ w$, see Ex. 3.6.

(iii) $D_{\circ} \circ (\lambda x_{\circ}x) \circ (\lambda x_{\circ}x) \equiv_{e}^{\text{ctx}} (\lambda x_{\circ}x)$, because they are $\beta_{\tau}$-convertible.
*Back to Ordinary λ-Terms.* Composing the interaction relations for checkers terms defined above with the black embedding of Λ into Λ<sub>◦•</sub>, we obtain new interaction relations on ordinary λ-terms.

**DEFINITION 3.9 (PLAYER LIFTING AND INTERACTION PREORDERS/EQUIVALENCE).**

(i) Given $p \in \{\circ, \bullet\}$, define the player p-lifting of ordinary λ-terms and ordinary contexts, as the maps $\tau^p : \Lambda \to \Lambda_{\circ\bullet}$ and $\tau^{\overline{p}} : C \to C_{\circ\bullet}$ obtained by p-tagging every constructor:

$$ 
\begin{align*}
\bar{x}^p &:= x, & \bar{\lambda}x.t^p &:= \lambda_p x.\bar{t}^p, & \bar{t}u^p &:= \bar{t}^p \cdot_p \bar{u}^p; \\
\langle\cdot\rangle^p &:= \langle\cdot\rangle, & \bar{\lambda}x.C^p &:= \lambda_p x.C^p, & \bar{t}C^p &:= \bar{t}^p \cdot_p C^p, & \bar{C}u^p &:= \bar{C}^p \cdot_p \bar{u}^p.
\end{align*}
$$

(ii) The interaction preorder $\sqsubseteq^\text{int}$, the interaction improvement $\sqsubseteq^\text{int-imp}$, and the interaction equivalence $\equiv^\text{int}$ are the following relations on ordinary λ-terms $t, u \in \Lambda$ defined via black lifting:

• $t \sqsubseteq^\text{int} u$ if $\bar{t}^\bullet \sqsubseteq^\text{ctx} \bar{u}^\bullet$;

• $t \sqsubseteq^\text{int-imp} t'$ if $\bar{t}^\bullet \sqsubseteq^\text{ctx-imp} \bar{u}^\bullet$;

• $t \equiv^\text{int} u$ is the equivalence relation induced by $\sqsubseteq^\text{int}$, that is, $t \equiv^\text{int} u$ if $t \sqsubseteq^\text{int} u$ and $u \sqsubseteq^\text{int} t$.

**EXAMPLE 3.10.** We use the λ-terms introduced in Notation 2.3. We also consider $D := \lambda yx.x(yx)$, having the property that $YD$ is a fixed point operator whose head reduction is 'slower' than that of $Y$.

(i) $YK \sqsubseteq^\text{int} t$, for all $t \in \Lambda$, because $YK$ does not have an hnf. Similarly, $YI =_\beta \Omega \sqsubseteq^\text{int} t$.

(ii) We have $I \not\sqsubseteq^\text{int} 1$, nor $1 \not\sqsubseteq^\text{int} I$ (Cf. Ex. 3.8(ii)). It is easily seen that $K \not\sqsubseteq^\text{int} F$ and $F \not\sqsubseteq^\text{int} K$.

(iii) $YD \equiv^\text{int} Y$, as the former needs more head-reduction steps to converge, but they are silent.

*The Interaction Preorder is Inequational.* We now show that the interaction preorder $\sqsubseteq^\text{int}$ is a semantics of λ-calculus, i.e., it is an inequational λ-theory, from which the corresponding results for $\sqsubseteq^\text{int-imp}$ and $\equiv^\text{int}$ follow. This is our first main result, showing that our framework does solve the internal/external tension evoked in the introduction.

As for contextual equivalence, proving invariance (that is, that $\beta$-conversion is included) is non-trivial, and even harder because of the constraint on the number of interaction steps. It follows from the following theorem for the checkers interaction preorder, which we shall prove in a later section via a semantic proof based on multi types (page 23), rather than via rewriting-based techniques.

**THEOREM 3.11 (THE INTERACTION PREORDER INCLUDES SILENT CONVERSION).** For all checkers terms $t, u \in \Lambda_{\circ\bullet}$, $t =_{\beta_r} u$ entails $t \sqsubseteq^\text{ctx} u$.

**COROLLARY 3.12.**

(1) The interactional preorder $\sqsubseteq^\text{int}$ is a consistent inequational λ-theory. Moreover, it is not semi-extensional, whence not extensional.

(2) The interactional improvement $\sqsubseteq^\text{int-imp}$ is a consistent inequational λ-theory.

(3) Interaction equivalence $\equiv^\text{int}$ is a consistent λ-theory. Moreover, it is not extensional.

**PROOF.** (3) follows from (1).

(1) We unfold the definition of inequational λ-theory, and check the following properties.

• *Preorder*. Reflexivity and transitivity are straightforward.

• *Compatibility*. It follows from the compatibility of $\sqsubseteq^\text{ctx}$. If $t \sqsubseteq^\text{int} u$, then we need to prove that $C\langle t \rangle \sqsubseteq^\text{int} C\langle u \rangle$, for any context $C$. Let $C'$ be a context. If $\overline{C'\langle C\langle t \rangle \rangle} \searrow_{h_{\circ\bullet}}^{{\scriptscriptstyle k}}$ then $\overline{C'\langle C\langle u \rangle \rangle} \searrow_{h_{\circ\bullet}}^{{\scriptscriptstyle k}}$ by $\bar{t}^\bullet \sqsubseteq^\text{ctx} \bar{u}^\bullet$.

• *Invariance*. Let $t =_\beta u$. Then clearly $\bar{t}^\bullet =_{\beta_r} \bar{u}^\bullet$. By Thm. 3.11, $\bar{t}^\bullet \sqsubseteq^\text{ctx} \bar{u}^\bullet$. Then $t \sqsubseteq^\text{int} u$. Consistency of $\sqsubseteq^\text{int}$ is given by the fact that $I \not\sqsubseteq^\text{int} \Omega$, as it can be seen by considering the empty context. The failure of semi-extensionality is shown in Ex. 3.6.

(2) The proof that $\sqsubseteq^\text{int-imp}$ is a compatible and consistent goes as for $\sqsubseteq^\text{int}$. For invariance, just note that $=_\beta \sqsubseteq^\text{int} \sqsubseteq^\text{int-imp}$. $\square$
*Interaction Improvement and η*. Note that the corollary does not say anything about $\sqsubseteq^{\text{int-imp}}$ and $\eta$. We conjecture that $\eta$-reduction is included in $\sqsubseteq^{\text{int-imp}}$, which would imply that the obvious inclusion $\sqsubseteq^{\text{int}} \subseteq \sqsubseteq^{\text{int-imp}}$ is strict, since it is not included in $\sqsubseteq^{\text{int}}$ (Ex. 3.6) (beware that strictness of the inclusion does not follows from $\sqsubseteq_{\bullet}^{\text{ctx}} \subsetneq \sqsubseteq_{\bullet}^{\text{ctx-imp}}$ as strictness in that case relies on black and white terms). For instance, $1 \to \eta$ I and we expect that $1 \sqsubseteq^{\text{int-imp}}$ I because, intuitively, head termination of $C\langle 1_{\bullet} \rangle$ does require at most one more interaction step than for $C\langle I_{\bullet} \rangle$, for all $C \in C_{\circ\bullet}$.

At present, however, it is only a conjecture. There is a real technical difficulty because the properties of $\eta$ that are usually used for rewriting-based proofs of similar facts fail for the checkers calculus, see Ex. 3.6. The semantic tools that we shall develop in the next sections for studying $\sqsubseteq^{\text{int}}$ are not able to deal with $\eta$ either.

*Adding and Removing Players.* The next proposition formalizes the fact that the black-only and white-only fragments of the checkers calculus are embeddings of the ordinary $\lambda$-calculus, not only statically but also dynamically. The statements concern head steps, but generalize to arbitrary steps.

**PROPOSITION 3.13 (LIFTING PROPERTIES).** Let $p \in \{\circ, \bullet\}$ and $t, u \in \Lambda$:

(1) Head steps are turned into silent ones: $\text{if } t \to_h u \text{ then } \bar{t}^p \to_{h_\tau} \bar{u}^p$.

(2) Mono-player head-steps can be pulled back to the ordinary $\lambda$-calculus: if $\bar{t}^p \to_{h_\circ\bullet} s$ then there exists a $\lambda$-term $u \in \Lambda$ such that $t \to_h u$ and $s = \bar{u}^p$.

(3) Head normal forms are preserved: $t$ is a hnf if and only if $\bar{t}^p$ is $h_\circ\bullet$-normal.

Let us also formalize the fact that adding tags to application and abstractions does not change the possible reductions. Let $t \in \Lambda$, a tagging $t^T$ is a checkers term that preserves the syntax but tags its abstractions and applications with players.

**PROPOSITION 3.14.** Let $t \to_h u$ be a reduction in the ordinary $\lambda$-calculus. For any tagging $T$ of $t$, there exists a tagging $T'$ of $u$ such that $t^T \to_{h_\circ\bullet} u^T$ in the checkers calculus.

It follows that sequences of head reductions in the ordinary $\lambda$-calculus are preserved in the checkers calculus, under some tagging determined by the first term in the reduction.

*Hierarchy.* Since $\sqsubseteq_{\bullet}^{\text{ctx}} \subseteq \sqsubseteq_{\bullet}^{\text{ctx-imp}}$, we have $\sqsubseteq^{\text{int}} \subseteq \sqsubseteq^{\text{int-imp}}$ (we showed that $\sqsubseteq_{\bullet}^{\text{ctx}} \subsetneq \sqsubseteq_{\bullet}^{\text{ctx-imp}}$, but not by using black lifted terms, so that does not give us $\sqsubseteq^{\text{int}} \subsetneq \sqsubseteq^{\text{int-imp}}$). The lifting properties above are used to prove the following expected lemma.

**LEMMA 3.15.** $\sqsubseteq^{\text{int-imp}} \subseteq \sqsubseteq^{\text{ctx}}$.

From Ex. 3.6, it follows that $I \not\sqsubseteq^{\text{int-imp}} 1$, while $I \sqsubseteq^{\text{ctx}} 1$ holds. Thus, $\sqsubseteq^{\text{int-imp}} \subsetneq \sqsubseteq^{\text{ctx}}$. Summing up, we obtain the following hierarchy of preorders.

**LEMMA 3.16 (HIERARCHY).** $\sqsubseteq^{\text{int}} \subseteq \sqsubseteq^{\text{int-imp}} \subsetneq \sqsubseteq^{\text{ctx}}$. Similarly, $\equiv^{\text{int}} \subsetneq \equiv^{\text{ctx}}$.

# 4 Böhm Trees

Here starts the second part of the paper, where interaction equivalence $\equiv^{\text{int}}$ shall be characterized as the equational theory $\mathcal{B}$ induced by the equality of Böhm trees. In this section, we recall Böhm trees and two notions of equality between them.

Barendregt proposed to represent the (possibly infinite) behavior of a $\lambda$-term $t$ as a (possibly infinite) tree, obtained by repeatedly slicing it with respect to head termination. We first present the idea informally, and then formally, following the similarity-based approach of Lassen [1999].

**DEFINITION 4.1 (BARENDREGT 1977).** The Böhm tree BT$(t)$ of a $\lambda$-term $t$ is defined as follows:

* If $t$ is head terminating then $t \to_h^* \lambda x_1 \dots x_n.y t_1 \dots t_k$, for some $n, k \ge 0$, and we define:
$$ BT(t) := \lambda x_1 \dots x_n y \quad \vline \quad BT(t_1) \dots BT(t_k) $$

• Otherwise, $t$ is head diverging and we define $BT(t) := \perp$.

Böhm trees are naturally ordered as follows: $BT(t) \leq_{\perp} BT(u)$ whenever $BT(u)$ is obtained from $BT(t)$ by replacing some (possibly zero, or infinitely many) occurrences of $\perp$ by arbitrary trees.

Intuitively, the constant $\perp$ represents the complete lack of information and, accordingly, the relation $BT(t) \leq_{\perp} BT(u)$ captures the fact that the behavior of $u$ is more defined than that of $t$.

**EXAMPLE 4.2.** *Some examples of Böhm trees of notable $\lambda$-terms:*

$$ \begin{array}{lclclclcl} \text{BT}(\Omega) = \perp & \text{BT}(\text{Pz}) = & \lambda x_0.x_0 & \text{BT}(\Upsilon) = & \lambda f.f & \geq_{\perp} & \lambda f.f & \geq_{\perp} & \lambda f.f & \geq_{\perp} \perp \\ \text{BT}(1) = & \lambda xy.x & \lambda x_1.x_1 & & f & & & f & & \perp \\ & \vline & \lambda x_2.x_2 & & f & & & \perp & & \\ & y & & & & & & & & \\ \end{array} $$

where $P = \Upsilon(\lambda yz.x(yz))$ satisfies $Pz =_{\beta} \lambda x.x(Pz)$. Note that $z$ is never erased by $P$, rather "pushed into infinity" in the sense that $Pz \xrightarrow{\beta} t$ entails $z \in \text{fv}(t)$, but $z$ does not occur in $\text{BT}(Pz)$.

It is well-known that Böhm trees are invariant under $\beta$-conversion [Barendregt 1984, Ch. 10]. Informally, the Böhm preorder $\sqsubseteq_{\beta}$ on terms is defined by pulling back the preorder on the associated trees, that is, $t \sqsubseteq_{\beta} u$ if $BT(t) \leq_{\perp} BT(u)$. Formally, we rather define the Böhm preorder as a notion of similarity, following Lassen [1999].

**DEFINITION 4.3 (BÖHM PREORDER, FORMALLY).** *The Böhm preorder $\sqsubseteq_{\beta}$, also known as head (normal form) similarity, is the largest relation $t \sqsubseteq_{\beta} u$ closed under the following clauses:*

(bot) $t \Downarrow_h$ i.e. $t$ has no head normal form.

(H) $t \Downarrow_h \lambda x_1 \dots x_n y t_1 \dots t_k$ and $u \Downarrow_h \lambda x_1 \dots x_n y u_1 \dots u_k$ with $(t_i \sqsubseteq_{\beta} u_i)_{i \leq k}$.

**THEOREM 4.4 ([BARENDREGT 1984, COR. 14.3.20(III)])**. *The Böhm preorder $\sqsubseteq_{\beta}$ is an inequational $\lambda$-theory. Moreover, $\sqsubseteq_{\beta}$ is neither extensional nor semi-extensional.*

The main result of the paper is that $\sqsubseteq_{\beta}$ coincides with the interaction preorder $\sqsubseteq^{\text{int}}$. For the direction $\sqsubseteq^{\text{int}} \subseteq \sqsubseteq_{\beta}$, we shall partly rely on a similar important result in the theory of the $\lambda$-calculus, namely Hyland's semi-separation theorem, which concerns an extensional variant of $\sqsubseteq_{\beta}$ below.

*Extensional Böhm Preorder.* We now formally introduce an extensional version of $\sqsubseteq_{\beta}$ capturing the preorder induced by Scott's model $\mathcal{D}_{\infty}$.

**DEFINITION 4.5 (EXTENSIONAL BÖHM PREORDER).** *The extensional Böhm preorder $\sqsubseteq_{\beta\eta^{\infty}}$ is the largest relation $t \sqsubseteq_{\beta\eta^{\infty}} u$ closed under the following clauses:*

(bot) $t \Downarrow_h$ i.e. $t$ has no head normal form.

(H$\eta$) $t \Downarrow_h h, u \Downarrow_h h'$, and there exist $n, k \geq 0$ such that $h =_{\eta} \lambda x_1 \dots x_n y t_1 \dots t_k$ and $h' =_{\eta} \lambda x_1 \dots x_n y u_1 \dots u_k$ with $(t_i \sqsubseteq_{\beta\eta^{\infty}} u_i)_{i \leq k}$.

**EXAMPLE 4.6.** *Recall that I, 1, K, and F have been defined in Notation 2.3.*

(i) We start with some negative examples: $K \not\sqsubseteq_{\beta\eta^{\infty}} F$ and $F \not\sqsubseteq_{\beta\eta^{\infty}} K$ (their head variables differ).

(ii) Both $I \sqsubseteq_{\beta\eta^{\infty}} 1$ and $1 \sqsubseteq_{\beta\eta^{\infty}} I$ hold. This entails the extensionality of $\sqsubseteq_{\beta\eta^{\infty}}$, hence of $=_{\beta\eta^{\infty}}$.

(iii) $\lambda xy.x \sqsubseteq_{\beta\eta^{\infty}} I$, holds since $\lambda xy.x \Omega \sqsubseteq_{\beta} 1 \sqsubseteq_{\beta\eta^{\infty}} I$ and $\sqsubseteq_{\beta} \sqsubseteq_{\beta\eta^{\infty}}$. Conclude by transitivity.

(iv) To understand the role of the infinitary $\eta$-expansion, consider the $\lambda$-term $J = \Upsilon(\lambda jx.x(jx))$. It is easy to check that $J \sqsubseteq_{\beta\eta^{\infty}} I$ by looking at the in-line depiction of its Böhm tree:
$$BT(J) = \lambda xy_0.x(\lambda y_1.y_0(\lambda y_2.y_1(\lambda y_3.y_2(\cdots)))))$$

The relations $\sqsubseteq_B \eta^\infty$ and $=_{B\eta^\infty}$ have characterizations as contextual preorders/equivalences.

**THEOREM 4.7 (HYLAND 1975/WADSWORTH 1976).** For all $\lambda$-terms $t, u$, we have $t \sqsubseteq^{\text{ctx}} u$ if and only if $t \sqsubseteq_B \eta^\infty u$. Therefore $t \equiv^{\text{ctx}} u$ if and only if $t =_{B\eta^\infty} u$.

# 5 Completeness, or Separating Böhm Different Terms

In this section, we prove that the interaction preorder $\sqsubseteq^{\text{int}}$ is included in the Böhm preorder $\sqsubseteq_B$.

*Proof Technique.* The standard way of proving that a contextual preorder $\sqsubseteq$ is included in a tree similarity $\leq$ is to proceed by proving the contrapositive: one supposes $BT(t) \not\leq BT(u)$, and constructs a context $C$ that:

(1) Extraction of the difference: brings up this difference from possibly deep down the tree structure of $BT(t)$ and $BT(u)$, that is, $C$ is such that $C\langle t \rangle$ and $C\langle u \rangle$ head reduce to two terms $t'$ and $u'$ for which the difference $BT(t') \not\leq BT(u')$ is on the root node, and

(2) Root separation: exploits the root difference to make $t'$ head terminating and $u'$ head divergent, thus obtaining that $t \not\sqsubseteq u$.

In the literature, this extraction process is known as *Böhm out* technique [Böhm 1968]; see also [Barendregt and Manzonetto 2022; Böhm 1968; Boudol and Laneve 1996; Dezani-Ciancaglini et al. 1998; Intrigila et al. 2019]. It is a concise and yet sophisticated technique. The culprit is that the extracting context needs to first *reorganize* the applicative structure of $t$ and $u$ (via *tupler combinator*,s, see below), to then apply the suitable selectors for extracting the discriminating sub-terms.

What raises difficulties is when one has two different terms, say, $t := x_1 t_2$ and $u := x_1 t_3$ with the difference deep down the structure of $t_2$ and $t_3$. Intuitively, to 'extract' $t_2$ and $t_3$ one would simply substitute for $x$ a term that selects the second argument, namely $\lambda yz.z$. Unfortunately, this approach is too simple to work, because then extracting the difference deep down $t_2$ and $t_3$ might require to substitute a different selecting term (say, of the first argument) for another occurrence of $x$ in $t_2$ and $t_3$, but clearly all the occurrences of $x$ must receive the same selecting term. An example of how the Böhm out technique solves this *colliding selectors issue* is discussed below.

*Definitions for the Böhm Out Technique.* On closed $\lambda$-terms, the technique amounts to applying the *tupler* $T_n$ and the *i*-th selector $S_i^n$ defined as follows:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \text{n-tuples} & \langle t_1, \dots, t_n \rangle & \lambda x.x t_1 \cdots t_n, & \text{with } x \text{ fresh;} \\ \text{tuplers} & T_n & \lambda x_1 \dots x_n \langle x_1, \dots, x_n \rangle; & \\ \text{sectors} & S_i^n & \lambda x_1 \dots x_n x_i, & \text{with } 1 \le i \le n. \end{array} $$

So, the tupler $T_n$ takes $n$ arguments $t_1, \dots, t_n$ and returns the tuple $\langle t_1, \dots, t_n \rangle$, while the selector $S_i^n$ takes $n$ arguments $t_1, \dots, t_n$ and returns the $i$-th argument $t_i$. Note that $S_1^n = I$. Then, $T_n t_1 \cdots t_n u \to_h^* u t_1 \cdots t_n$ and $S_i^n t_1 \cdots t_n \to_h^* t_i$, whence we have the following combined extraction property:

$$ T_n t_1 \cdots t_n S_i^n \to_h^* t_i. \qquad (1) $$

In the following, we shall need to locate nodes/hnfs occurring at a certain path in a Böhm tree.

**DEFINITION 5.1.**

* Path: a path is a (possibly empty) finite list of natural numbers $\alpha = \langle a_1, \dots, a_n \rangle$, where $a_i \ge 1$, for each $1 \le i \le n$.

* Concatenation: given $i \in \mathbb{N}$ and a path $\alpha$ as above, their concatenation is $i \cdot \alpha := \langle i, a_1, \dots, a_n \rangle$.

* Node occurring at a path: let $t$ be a $\lambda$-term such that $t \to_h^* \lambda \vec{x}. y t_1 \cdots t_k$. If $\alpha = \langle \rangle$ then $t \upharpoonright_\alpha = \lambda \vec{x}. y t_1 \cdots t_k$, if $\alpha = i \cdot \alpha'$ with $i \le k$ then $t_\alpha = (t_i)_{\alpha'}$. Otherwise, $t \upharpoonright_\alpha$ is undefined.
**EXAMPLE 5.2.** We show how the Böhm out technique is able to construct a context separating the $\lambda$-term $t := \lambda xy.x(x\Omega y)\Omega$ from the $\lambda$-term $u := \lambda xy.x(xy\Omega)\Omega$, which provide an example of the colliding selectors issue. We represent below their Böhm trees:

$$ \text{BT}(t) = \begin{array}{c} \xrightarrow{\lambda xy.x} \\ \xrightarrow[\perp]{x} \\ \xrightarrow[\perp]{y} \end{array} $$

$$ \text{BT}(u) = \begin{array}{c} \xrightarrow{\lambda xy.x} \\ \xrightarrow[\perp]{x} \\ \xrightarrow[\perp]{y} \end{array} $$

Showing that $t \not\sqsubseteq^{\text{ctx}} u$ requires a context $C$ making $t$ converge and $u$ diverge. The path to extract along is $\alpha' = (1, 2)$, which showcases the colliding selectors issue: the first occurrence of $x$ needs to select the first argument, while the second occurrence needs the second argument. Böhm's trick consists in using tuplers, as we now attempt to explain. The Böhm out context is $C := \langle\cdot\rangle T_2 IS_1^2 S_2^2$. The idea is that, by substituting a tupler $T_2$ on $x$ and having as further arguments the right selectors for each occurrence, one exploits the extraction property (1) above to select the right sub-term in each case. The identity $I$ is added like a padding when more arguments are needed. Concretely, we have:

$$ \begin{array}{lclcl} C \langle t \rangle = & (\lambda xy.x(x\Omega y)\Omega) T_2 IS_1^2 S_2^2 & \rightarrow^2 & T_2(T_2\Omega I)\Omega S_1^2 S_2^2 & \rightarrow^2 \\ \text{by (1)} & \rightarrow^* & T_2\Omega IS_2^2 & \rightarrow^2 & T_2(T_2\Omega)\Omega S_1^2 S_2^2 \\ \text{by (1)} & \rightarrow^* & I & \rightarrow^2 & T_2\Omega S_2^2 \\ \text{by (1)} & \rightarrow^* & I & \rightarrow^* & \Omega \end{array} $$

$$ \begin{array}{lclcl} C \langle u \rangle = & (\lambda xy.x(xy\Omega)\Omega) T_2 IS_1^2 S_2^2 & \rightarrow^2 & T_2(T_2\Omega)\Omega S_1^2 S_2^2 & \rightarrow^2 \\ \text{by (1)} & \rightarrow^* & T_2\Omega S_2^2 & \rightarrow^2 & T_2\Omega S_2^2 \\ \text{by (1)} & \rightarrow^* & \Omega & \rightarrow^2 & T_2\Omega S_2^2 \end{array} $$

There are more technicalities of the Böhm out technique, unfortunately. Firstly, since the extraction process works through substitutions of tuplers and selectors, one in general extracts a *substitution instance of a sub-term*, and not the sub-term itself. Secondly, in our example both occurrences of $x$ have two arguments, but in general different occurrences might have different numbers of arguments. Then, one needs to apply a tupler $T_n$ with $n$ "large enough", and this over-approximation may destroy some $\eta$-differences between the two trees. If one observes only termination, then $\eta$-equivalent terms are *not* separable.

In our setting, we are able to discriminate $\eta$-convertible $\lambda$-terms because we observe termination and count the number of interaction steps, which are changed by $\eta$, as showed by Ex. 3.6. The idea is to black dress the differing terms $t$ and $u$ and to white dress the separating context $C$, so that the black $\eta$-differences in $\vec{t}^*$ and $\vec{u}^*$ that are erased by $\bar{C}^\circ$ are turned into interaction steps.

**Interaction Böhm Out.** The following lemma shows how to separate those $\lambda$-terms which have Böhm trees differing only by some (possibly infinitary) $\eta$-expansions, that is, the case when $t \sqsubseteq_{\mathcal{B}\eta^\infty} u$ and $t \not\sqsubseteq_{\mathcal{B}} u$, because the case $t \not\sqsubseteq_{\mathcal{B}\eta^\infty} u$ is handled by Thm. 4.7, that is, via standard Böhm out. Because of its technical nature, it is labeled as a *lemma* and yet it is one of the main technical contributions of the paper. The inclusion $\sqsubseteq^{\text{int}} \subseteq \sqsubseteq_{\mathcal{B}}$ then follows easily.

**LEMMA 5.3 (INTERACTION BÖHM-OUT).** Let $t, u \in \Lambda$ such that $t \sqsubseteq_{\mathcal{B}\eta^\infty} u$ and $t \not\sqsubseteq_{\mathcal{B}} u$. Then, there exists a context $C \in C$ such that $\bar{C}^\circ \langle \vec{t}^* \rangle \coloneqq_i^{\mathcal{B}}$ and $\bar{C}^\circ \langle \vec{u}^* \rangle \coloneqq_{n^*}^{\mathcal{B}}$ with $i^* \neq i$.

**Terminology and Notations for the Proof.** As customary in mathematical analysis, we say that a relation $P(-)$ holds for all $K \in \mathbb{N}$ large enough whenever there exists a $K' \in \mathbb{N}$ such that $P(K)$ holds for all $K \ge K'$. We also use the notation $tu^{\sim n}$ for $(\cdots ((tu)u)\cdots)u$ (n times). Finally, two head normal forms $h, h'$ are *spine equivalent*, written $h =_{\text{sp}} h'$, if there are $n, k \ge 0$ such that:

$$ h = \lambda x_1 \dots x_n \cdot y \, t_1 \cdots t_k \quad \text{and} \quad h' = \lambda x_1 \dots x_n \cdot y \, u_1 \cdots u_k. \qquad (2) $$

**PROOF.** We prove a stronger statement, i.e. that there exist closed terms $\vec{s} \in \Lambda$ such that, for all $\vec{y}$ containing $fv(t) \cup fv(u)$ and for all $K \in \mathbb{N}$ large enough, the following holds:
$$ \bar{t}^{\bullet} \{\bar{y} := \bar{T}_{K}^{\circ}\} \circ \bar{s}^{\circ} \mathcal{J}_{h_{\circ}}^{\bullet i} \quad \text{and} \quad \bar{u}^{\bullet} \{\bar{y} := \bar{T}_{K}^{\circ}\} \circ \bar{s}^{\circ} \mathcal{J}_{h_{\circ}}^{\bullet i'} \quad \text{with } i' \neq i. $$

Given variables $\vec{x}$ and a $\lambda$-term $t$ we write $\sigma_{\vec{x}}$ for $\{\vec{x} := \overline{T_K^\circ}\}$, and $t^{\sigma_{\vec{x}}}$ for $t\{\vec{x} := \overline{T_K^\circ}\}$.

Note that $t \not\subseteq_B u$ is only possible if $t \mathcal{J}_h$. Moreover, $t \mathcal{J}_h h$ and $t \sqsubseteq_{B\eta^\infty} u$ entail $u \mathcal{J}_h h'$, for some $h'$. We proceed by induction on the length of a minimal path $\delta \in \mathbb{N}^*$ such that $t \upharpoonright_\delta \neq_{sp} u \upharpoonright_\delta$.

**Base case** $\delta = \langle\rangle$, i.e. $h \neq_{sp} h'$. Then $t \sqsubseteq_{B\eta^\infty} u$ is only possible if the amount of spine abstractions and applications in $h, h'$ can be matched via $\eta$-expansion, say:

$$ t \xrightarrow{h}^* h = \lambda x_1 \dots x_n y t_1 \dots t_k \quad \text{and} \quad u \xrightarrow{h}^* h' = \lambda x_1 \dots x_n z_1 \dots z_m y u_1 \dots u_{k+m} $$

for $n, k \ge 0$ and $m > 0$. (The symmetrical case where $h$ has more abstractions/applications than $h'$ is omitted because analogous.) There are two subcases to consider, depending on whether $y$ is free.

(1) $y$ is free, i.e. $y \in \bar{y}$. Take any $K \ge k + m$, and empty $\bar{s}$. For $t$, we have:

<table><thead><tr><th>e-STEPS</th><th>TERMS AND τ-STEPS</th><th></th></tr></thead><tbody><tr><td>=</td><td><table><tbody><tr><td><span style="text-decoration: overline;">t</span><sup>*</sup><span style="text-decoration: overline;">{y}:</span><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span></td><td><span style="text-decoration: overline;">h</span><sup>*</sup><span style="text-decoration: overline;">{y}:</span><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span></td><td>by Pr. 3.13(1) &amp; L.3.5</td></tr></tbody></table></td><td></td></tr><tr><td>→<sup>k</sup><sub>h<sub>o</sub></sub></td><td><table><tbody><tr><td>λ<sub>...</sub>...</td><td>x<sub>1</sub>...</td><td>x<sub>n</sub>.</td><td><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span><sup>•</sup><td>σ<sub>y</sub></td><td>•</td><td>...</td><td><span style="text-decoration: overline;">t<sub>1</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td></tr><tr><td>λ<sub>...</sub>...</td><td>x<sub>1</sub>...</td><td>x<sub>n</sub>.</td><td>λ<sub>...</sub>...</td><td>w<sub>k+1</sub>...</td><td>w<sub>K</sub>.</td><td>⟨<span style="text-decoration: overline;">t<sub>1</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td><td>...</td><td><span style="text-decoration: overline;">t<sub>k</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td></tr></tbody></table></td><td></td></tr></tbody></table>

where $\langle-, \dots, -, \rangle_\circ$ denotes the tuple with white applications $\lambda z.z - \circ \cdots \circ -$. For $u$, we have:

<table><thead><tr><th>e-STEPS</th><th>TERMS AND τ-STEPS</th><th></th></tr></thead><tbody><tr><td>=</td><td><table><tbody><tr><td><span style="text-decoration: overline;">u</span><sup>*</sup><span style="text-decoration: overline;">{y}:</span><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span></td><td><span style="text-decoration: overline;">h</span><sup>*</sup><span style="text-decoration: overline;">{y}:</span><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span></td><td>by Pr. 3.13(1) &amp; L.3.5,</td></tr></tbody></table></td><td></td></tr><tr><td>→<sup>k+m</sup><sub>h<sub>o</sub></sub></td><td><table><tbody><tr><td><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span><sup>•</sup><td>σ<sub>y</sub></td><td>•</td><td>...</td><td><span style="text-decoration: overline;">u<sub>k+m</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td></tr><tr><td>λ<sub>...</sub>...</td><td>x<sub>1</sub>...</td><td>x<sub>n</sub>.</td><td>λ<sub>...</sub>...</td><td>w<sub>k+1</sub>...</td><td>w<sub>K</sub>.</td><td>⟨<span style="text-decoration: overline;">u<sub>1</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td><td>...</td><td><span style="text-decoration: overline;">u<sub>k+m</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td></tr></tbody></table></td><td></td></tr></tbody></table>

Summing up, $\bar{t}^{\bullet \sigma_{\bar{y}}} \mathcal{J}_{h_o}^{\bullet k}$ and $\bar{u}^{\bullet \sigma_{\bar{y}}} \mathcal{J}_{h_o}^{\bullet k+m}$. The statement holds because $m > 0$.

(2) $y$ is bound, i.e. $y = x_j \in \vec{x}$. Take any $K \ge k + m$, and let the arguments $\vec{s}$ be $n$ copies of $T_K$ (noted $\overline{T_K^n}$ for short). On the one hand:

<table><thead><tr><th>e-STEPS</th><th>TERMS AND τ-STEPS</th><th></th></tr></thead><tbody><tr><td>=</td><td><table><tbody><tr><td><span style="text-decoration: overline;">t</span><sup>*</sup><span style="text-decoration: overline;">{y}:</span><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span></td><td><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span><sup>•</sup><span style="text-decoration: overline;">~n</span></td><td><span style="text-decoration: overline;">→</span><sup>*</sup><sub>h<sub>r</sub></sub><span style="text-decoration: overline;">{y}:</span><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span></td><td>by Pr. 3.13(1) &amp; L.3.5,</td></tr></tbody></table></td><td></td></tr><tr><td>→<sup>n</sup><sub>h<sub>o</sub></sub></td><td><table><tbody><tr><td>(λ<sub>...</sub>...</td><td>x<sub>1</sub>...</td><td>x<sub>n</sub>.</td><td>x<sub>j</sub> <span style="text-decoration: overline;">•</span><span style="text-decoration: overline;">t<sub>1</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td><td>•</td><td>...</td><td><span style="text-decoration: overline;">t<sub>k</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td></tr><tr><td><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span><sup>•</sup><td>σ<sub>x&#x0303;y</sub></td><td>•</td><td>...</td><td><span style="text-decoration: overline;">t<sub>k</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>x&#x0303;y</sub></td></tr></tbody></table></td><td></td></tr><tr><td>→<sup>k</sup><sub>h<sub>o</sub></sub></td><td><table><tbody><tr><td>λ<sub>...</sub>...</td><td>w<sub>k+1</sub>...</td><td>w<sub>K</sub>.</td><td>⟨<span style="text-decoration: overline;">t<sub>1</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>x&#x0303;y</sub></td><td>...</td><td><span style="text-decoration: overline;">t<sub>k</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>x&#x0303;y</sub></td></tr></tbody></table></td><td></td></tr></tbody></table>

On the other hand:

<table><thead><tr><th>e-STEPS</th><th>TERMS AND τ-STEPS</th><th></th></tr></thead><tbody><tr><td>=</td><td><table><tbody><tr><td><span style="text-decoration: overline;">u</span><sup>*</sup><span style="text-decoration: overline;">{y}:</span><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span></td><td><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span><sup>•</sup><span style="text-decoration: overline;">~n</span></td><td><span style="text-decoration: overline;">→</span><sup>*</sup><sub>h<sub>r</sub></sub><span style="text-decoration: overline;">{y}:</span><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span></td><td>by Pr. 3.13(1) &amp; L.3.5,</td></tr></tbody></table></td><td></td></tr><tr><td>→<sup>n</sup><sub>h<sub>o</sub></sub></td><td><table><tbody><tr><td>(λ<sub>...</sub>...</td><td>x<sub>1</sub>...</td><td>x<sub>n</sub>z&#x0303;.</td><td>x<sub>j</sub> <span style="text-decoration: overline;">•</span><span style="text-decoration: overline;">u<sub>1</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td><td>•</td><td>...</td><td><span style="text-decoration: overline;">u<sub>k+m</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>y</sub></td></tr><tr><td><span style="text-decoration: overline;">T<sub>K</sub><sup>°</sup></span><sup>•</sup><td>σ<sub>x&#x0303;y</sub></td><td>•</td><td>...</td><td><span style="text-decoration: overline;">u<sub>k+m</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>x&#x0303;y</sub></td></tr></tbody></table></td><td></td></tr><tr><td>→<sup>k+m</sup><sub>h<sub>o</sub></sub></td><td><table><tbody><tr><td>λ<sub>...</sub>...</td><td>w<sub>k+m+1</sub>...</td><td>w<sub>K</sub>.</td><td>⟨<span style="text-decoration: overline;">u<sub>1</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>x&#x0303;y</sub></td><td>...</td><td><span style="text-decoration: overline;">u<sub>k+m</sub><sup>*</sup></span><sup>•</sup><td>σ<sub>x&#x0303;y</sub></td></tr></tbody></table></td><td></td></tr></tbody></table>

Summing up, $\bar{t}^{\bullet \sigma_{\bar{y}}} \mathcal{J}_{h_o}^{\bullet n+k}$ and $\bar{u}^{\bullet \sigma_{\bar{y}}} \mathcal{J}_{h_o}^{\bullet n+k+m}$. The statement holds because $m > 0$.

**Inductive case** $\delta = j \cdot \gamma$. In this case, we must have:

$$ t \xrightarrow{h}^* h = \lambda x_1 \dots x_n y t_1 \dots t_k \quad \text{and} \quad u \xrightarrow{h}^* h' = \lambda x_1 \dots x_n y u_1 \dots u_k $$

with $t_j \not\subseteq_B u_j$ and $(t_l \sqsubseteq_{B\eta^\infty} u_l)_{l \le k}$. By i.h., there exists $K'$ and $\vec{s}'$ such that for all $K \ge K'$:
<table><caption>Fig. 3. De Carvalho's multi type system.</caption><thead><tr><th colspan="2">TYPES</th><th colspan="2">TYPING RULES</th></tr></thead><tbody><tr><td>LINEAR</td><td>L, L' ::= A | M → L</td><td rowspan="2">x: [L] ⊎ x: L</td><td rowspan="2">(Γi ⊎ t: L<sub>i</sub>)<sub>i∈I</sub> I finite many<br>ψ<sub>i∈I</sub>Γi ⊎ t: [L<sub>i</sub>]<sub>i∈I</sub></td></tr><tr><td>MULTI</td><td>M, N ::= [L<sub>1</sub>, ..., L<sub>n</sub>] n ≥ 0</td></tr><tr><td>GENERIC</td><td>T, T' ::= L | M</td><td rowspan="2">Γ, x: M ⊎ t: L<br>Γ ⊎ λx.t: M → L</td><td rowspan="2">Γ ⊎ t: M → L Δ ⊎ u: M<br>Γ ψ Δ ⊎ tu: L @</td></tr><tr><td>ZERO</td><td>0 ::= []</td></tr></tbody></table>

M of cardinality $n$ if it is going to be used $n$ times. In particular, if $n > 0$ and $t$ is part of a larger term $u$, then a copy of $t$ shall end up in evaluation (i.e. head) position during the evaluation of $u$.

*Typing Rules.* Judgments have shape $Γ ⊎ t: L$ or $Γ ⊎ t: M$, where $t$ is a $λ$-term, $M$ is a multi type, $L$ is a linear type, and $Γ$ is a *type environment*, i.e., a total function from variables to multi types such that $dom(Γ) := \{x | Γ(x) ≠ 0\}$ is finite. We say that $Γ$ is *empty* if $dom(Γ) = \emptyset$. We write $x_1: M_1, ..., x_n: M_n$ for the environment $Γ$ such that $Γ(y) = M_i$, if $y = x_i ∈ \bar{x}$, $Γ(y) = 0$, otherwise.

Note that the application rule @ requires the argument to be typed with a multi type $M$, which is necessarily introduced by rule many, having as hypotheses a multiset of derivations, indexed by a possibly empty set $I$. When $I$ is empty, the rule @ has no premises and can type every term with $0$. For instance, $⊎ Ω: 0$ is derivable, but no linear type can be assigned to $Ω$. Intuitively, $0$ is the type of erasable terms, and every $λ$-term is erasable in the (call-by-name) $λ$-calculus.

*Technicalities about Types.* The multiset union is denoted by $\oplus$ and is extended to type environments pointwisely, i.e. $(Γ \oplus \Delta)(x) := Γ(x) \oplus \Delta(x)$, for all $x \in VAR$. This notion is extended further to a finite family of type environments as expected. In particular, if $J = \emptyset$ we let $\supset_i \in J \Gamma_i$ be the empty environment. Given two type environments $Γ$ and $\Delta$ having disjoint domain $dom(Γ) \cap dom(\Delta) = \emptyset$, we simply write $Γ, \Delta$ for $Γ \oplus \Delta$. Note that $Γ, x: 0 = Γ$, where we implicitly assume $x \notin dom(Γ)$. We write $π \triangleright Γ ⊎ t: T$ whenever $π$ is a (*type*) *derivation* (i.e. a finite tree constructed bottom up by applying the rules in Fig. 3) with as conclusion the judgment $Γ ⊎ t: T$. We write $π \triangleright t$ if $π \triangleright Γ ⊎ t: T$, for some type environment $Γ$ and some type $T$.

*Type Preorder and Relational Semantics.* The multi type system induces a notion of semantic interpretation into what is known as *relational model* of (the call-by-name) $λ$-calculus. The interpretations of $λ$-terms are naturally ordered by set-theoretical inclusion, and this induces a preorder on $λ$-terms, namely the inequational theory of the model.

**DEFINITION 6.2 (RELATIONAL INTERPRETATION AND TYPE PREORDER).**

(i) *The relational interpretation $[[t]]$ of a $λ$-term $t$ is defined as follows:*

$$[[t]] := \{(Γ, L) | \exists π \triangleright Γ ⊎ t: L\}.$$

(ii) *The type preorder $\sqsubseteq^{\text{typ}}$ on ordinary $λ$-terms is defined as $t \sqsubseteq^{\text{typ}} u$ if $[[t]] \subseteq [[u]]$, and the induced type equivalence is noted $\equiv^{\text{typ}}$.*

We have the following fundamental properties of the multi type preorder.

**THEOREM 6.3 (BREUVART ET AL. [2018]).** Let $t, u \in \Lambda$.

(1) Compatibility: if $t \sqsubseteq^{\text{typ}} u$ then $C\langle t \rangle \sqsubseteq^{\text{typ}} C\langle u \rangle$, for every context $C$.

(2) $β$-invariance: if $t \to \beta$ then $[[t]] = [[u]]$.

(3) $η$-reduction: if $t \to \eta$ then $[[t]] \subseteq [[u]]$.

(4) No $η$-expansion: $λy(xy) \to \eta x$, but $[[x]] \not\subseteq [[λy(xy)]]$.
The failure of $\eta$-expansion, i.e. Point 4 of the theorem, is due to the fact that $x$ can be typed with the atomic type $A$ using an axiom, while there is no way of typing $\lambda y(xy)$ with $A$, since it can only be typed with an arrow type.

**COROLLARY 6.4.** *The relation $\sqsubseteq^{\text{typ}}$ is an inequational $\lambda$-theory. Moreover, $\sqsubseteq^{\text{typ}}$ is semi-extensional but not extensional.*

The corollary captures the soundness of Engeler's relational model. It is possible to prove that $\sqsubseteq^{\text{typ}} \subseteq \sqsubseteq^{\text{ctx}}$, thus obtaining a semantic proof that $\sqsubseteq^{\text{ctx}}$ is an inequational theory (Thm. 2.6). In Sect. 8, we shall follow this approach for proving that the interaction preorder is an inequational theory.

*Adequacy with Respect to Head Reduction.* For showing that typable terms are head terminating, we need a notion of size for type derivations, that shall bound the number of head steps.

**DEFINITION 6.5 (SIZE).** Let $\pi$ be a type derivation. The (applicative) size $|\pi|_{@}$ of $\pi$ is the number of occurrences of rules @ in $\pi$.

**PROPOSITION 6.6 ([BARENDREGT AND MANZONETTO 2022]).** Let $t, t' \in \Lambda$ be such that $t \to_h t'$.

(1) Quantitative subject reduction: if $\pi \triangleright \Gamma \vdash t:L$ then there exists a derivation $\pi' \triangleright \Gamma \vdash t':L$ such that $|\pi'|_{@} = |\pi|_{@} - 1$.

(2) Subject expansion: if $\pi' \triangleright \Gamma \vdash t':L$ then there is a derivation $\pi \triangleright \Gamma \vdash t:L$.

Note the quantitative aspect of subject reduction (Prop. 6.6(1)), stating that the derivation size *strictly decreases* along head steps. It does not say that it decreases at arbitrary $\beta$-steps because the contraction of redexes occurring in sub-terms typed with rule many might not change the size. For instance, if $xt \to_{\beta} xt'$ and $t$ is typed using an empty many rule (i.e. with 0 premises), which is a sub-derivation of size 0, then also $t'$ is typed using an empty many rule, of size 0. In fact, not all typable terms are $\beta$-normalizable: $x\Omega$ is typable as follows, for any linear type $L$, but it has no $\beta$-nf:

$$ \frac{x: [0 \to L] \vdash x:0 \to L \quad ax \quad \frac{\vdash \Omega:0}{x: [0 \to L] \vdash x\Omega:L} \quad \text{many}}{(3) \qquad @} $$

Since the size of type derivations decreases at every head step, it provides a termination measure (only) for the head reduction of typable terms. The fact that typable terms are head terminating is also called *correctness* of the type system.

*Completeness of the type system—i.e.* every head terminating term is typable—is obtained via typability of all head normal forms, proved next, and subject expansion (Prop. 6.6(2)).

**PROPOSITION 6.7 (TYPABILITY OF HEAD NORMAL FORMS. [BARENDREGT AND MANZONETTO 2022]).**
Let $h \in \Lambda$ be a head normal form. Then there exists a derivation $\pi \triangleright \Gamma \vdash h:L$.

Summing up, we obtain the following characterization of head normalization.

**THEOREM 6.8 (TYPABILITY CHARACTERIZES HEAD NORMALIZATION. [BARENDREGT AND MANZONETTO 2022]).** Let $t \in \Lambda$.

(1) Correctness: if $\pi \triangleright t$ then there exists a head normalizing evaluation $t \to_h^n h$ with $h$ normal and $n \le |\pi|_{@}$.

(2) Completeness: if $t \to_h^* h$ is a head normalizing sequence, then there exists a derivation $\pi \triangleright t$. Therefore $[t] \neq \emptyset$ if and only if $t$ is head normalizable. In particular, $\sqsubseteq^{\text{typ}}$ is consistent.
$$
\begin{array}{l@{\hspace{1em}}r@{\hspace{1em}}c@{\hspace{1em}}l@{\hspace{1em}}c@{\hspace{1em}}l}
\text{LINEAR TYPES} & \text{L, L'} & \text{::=} & \text{A} \mid \text{M} & \xrightarrow{\text{pq}} & \text{L} & \text{p, q} \in \{\circ, \bullet\} \\
\text{MULTI TYPES} & \text{M, N} & \text{::=} & \text{[L}_1, \dots, \text{L}_n] & \qquad & n \ge 0 &
\end{array}
$$

$$
\begin{array}{l@{\hspace{1em}}r@{\hspace{1em}}c@{\hspace{1em}}l@{\hspace{1em}}c@{\hspace{1em}}l}
\text{GENERIC TYPES} & \text{T, T'} & \text{::=} & \text{L} \mid \text{M} & & \\
\text{ZERO} & 0 & \text{::=} & \text{[ ]} & &
\end{array}
$$

$$
\begin{array}{c@{\hspace{1em}}c@{\hspace{1em}}c@{\hspace{1em}}c@{\hspace{1em}}c@{\hspace{1em}}c}
\overline{x \mid [L] \vdash_{\mathfrak{e}}^{0} x \mid L} & \text{ax} & \frac{(\Gamma_i \vdash_{\mathfrak{e}}^{k_i} t \mid L_i)_{i \in I}}{\psi_{i \in I} \Gamma_i \vdash_{\sum_{i \in I} k_i} t \mid [L_i]_{i \in I}} & \text{I finite} & \multicolumn{2}{c}{\text{many}} \\
\frac{\Gamma, x \mid M \vdash_{\mathfrak{e}}^{k} t \mid L}{\Gamma \vdash_{\mathfrak{e}}^{k} \lambda_p x.t \mid M \xrightarrow{\text{pq}} L} & \lambda & \frac{\Gamma \vdash_{\mathfrak{e}}^{k_1} t \mid M \xrightarrow{\text{pq}} L}{\Gamma \psi \Delta \vdash_{\mathfrak{e}}^{k} t \cdot q u \mid L} & \Delta \vdash_{\mathfrak{e}}^{k_2} u \mid M & \multicolumn{2}{c}{@} \\
& & & & \frac{\Gamma \vdash_{\mathfrak{e}}^{k_1} t \mid M \xrightarrow{\text{pp}} L}{\Gamma \psi \Delta \vdash_{\mathfrak{e}}^{k_1+k_2} t \cdot p u \mid L} & \Delta \vdash_{\mathfrak{e}}^{k_2} u \mid M \\
& & & & \frac{\Gamma \vdash_{\mathfrak{e}}^{k_1} t \mid M \xrightarrow{\text{pp}^{\perp}} L}{\Gamma \psi \Delta \vdash_{\mathfrak{e}}^{k_1+k_2+1} t \cdot p^{\perp} u \mid L} & @_{\tau} \\
& & & & \frac{\Gamma \vdash_{\mathfrak{e}}^{k_1} t \mid M \xrightarrow{\text{pp}} L}{\Gamma \psi \Delta \vdash_{\mathfrak{e}}^{k_1+k_2+1} t \cdot p^{\perp} u \mid L} & @_{\mathfrak{e}}
\end{array}
$$

In rule @, $k = k_1+k_2$ if $p = q$, otherwise $k = k_1+k_2+1$. Rule @ compactly sums up rules $@_{\tau}$ and $@_{\mathfrak{e}}$.

<caption>Fig. 4. Checkers multi type system $\vdash_{\mathfrak{e}}$.</caption>

*Exact Bounds?* It is natural to wonder whether there are type derivations $\pi$ for which correctness holds with $n = |\pi|_@$. The answer is no: the type derivation in (3), as well as any other type derivation for $x\Omega$, has at least one @ rule even if the $\lambda$-term $x\Omega$ is already a head normal form, whence $n = 0$.

The question has been studied and refined in the literature. Such a mismatch can be improved in two ways, both studied in-depth by Accattoli et al. [2020]. The first one traces back to de Carvalho [2007, 2018], and takes into account the number $|h|_h$ of application constructors in the spine of the head normal form $h$. Then type derivations $\pi$ satisfying a certain *tight predicate* verify $n+|h|_h = |\pi|_@$. The second one is developed in Accattoli et al. [2020]. It introduces:

* A second set of typing rules assigning some new type constants to the constructors that occur in the head normal form, and;

* A tight predicate forcing all such constructors to be typed with these alternative rules.

In such a system, one can actually obtain $n = |\pi|_@$ when the tight predicate holds. The drawback is that in this case one obtains a constants-only type that cannot be composed with any other type.

For the new type system of the next section, we shall give in Sect. 8 a refined technique for exact bounds that exploits player tags. We shall measure the exact number of interaction head steps without resorting to constants-only types, which is a novelty.

# 7 Checkers Multi Types

In this section, we introduce a system $\vdash_{\mathfrak{e}}$ of multi types for the checkers calculus, that can be seen as an annotated version of the standard one presented in Section 6. We shall prove that the new system characterizes termination of checkers head reduction $\rightarrow_{h_{\circ\circ}}$, similarly to the standard system. Despite the similarity, however, the two systems are inherently different because the new one shall *not* be invariant under $\eta$-reduction, while the standard one is (Thm. 6.3(3)).

**DEFINITION 7.1.** *Types and typing rules of the checkers multi types system $\vdash_{\mathfrak{e}}$ are given in Fig. 4.*

*Main Ideas 1: Checkers Arrows.* We start by turning the arrow type $M \rightarrow L$ into a checkers arrow type $M \xrightarrow{pq} L$ carrying two tags $p, q \in \{\circ, \circ\}$, thus giving rise to four possible player combinations. The idea is that if, say, $t: M \xrightarrow{\circ\circ} L$ then $t$ can only be applied via $\bullet$-applications and if it reduces to an abstraction then it must be a $\circ$-abstraction. In the typing rule $\lambda$ for abstractions, the first player $p$ is determined by the external abstraction, while the second player $q$ can be freely chosen. We shall refer to $\xrightarrow{\circ\circ}$ and $\xrightarrow{\bullet\circ}$ as *interaction arrow types*, and to $\xrightarrow{\bullet\bullet}$ and $\xrightarrow{\circ\circ}$ as *silent arrow types*.
**Main Ideas 2: Interaction Application Rule and Index.** The second main ingredient is that there are now two application rules @<sub>τ</sub> and @<sub>e</sub>, one for the application of silent arrows and one for interaction arrows. We provide also a rule @ that sums them up compactly. Moreover, typing judgement Γ ⊢<sub>e</sub><sup>k</sup> t:T now carry an index k which counts the number of @<sub>e</sub> rules in the derivation. These rules, intuitively, type interaction steps, which can be *factual* or *potential*, as we now explain. The application of an abstraction typed with an interaction arrow type gives rise to an interaction step →β<sub>e</sub>, whence it is a factual interaction. The application of a free variable typed with an interaction arrow, for instance, does *not* give rise to an interaction step, but that *potential* interaction is recorded in the type and it might arise if the term is plugged in a context, according to its type. When the interaction index k is irrelevant, we omit it and simply write Γ ⊢<sub>e</sub> t:T.

**DEFINITION 7.2 (CHECKERS RELATIONAL INTERPRETATION AND TYPE PREORDER).**

(i) The checkers relational interpretation [[t]]<sup>e</sup> of a checkers term t ∈ Λ<sub>◦</sub><sub>◦</sub> is defined by:

$$[[t]]^e := \{(\langle \Gamma, k, L \rangle \mid \exists \pi \triangleright \Gamma \vdash_e^k t : L)\}.$$

(ii) The type preorder ≤<sub>e</sub><sup>typ</sup> on checkers λ-terms t, u ∈ Λ<sub>◦</sub><sub>◦</sub> is defined as t ≤<sub>e</sub><sup>typ</sup> u if [[t]]<sup>e</sup> ≤ [[u]]<sup>e</sup>, and the induced type equivalence is noted ≡<sub>e</sub><sup>typ</sup>.

(iii) The black type preorder ≤<sup>•typ</sup> on ordinary λ-terms t, u ∈ Λ is defined as t ≤<sup>•typ</sup> u if $\overline{t^•} \leq_e^{\text{typ}} \overline{u^•}$, and the induced type equivalence is noted ≡<sup>•typ</sup>.

We have the following fundamental properties of the multi type preorder.

**THEOREM 7.3.** Let t, u ∈ Λ<sub>◦</sub><sub>◦</sub>.

(1) Compatibility: if t ≤<sub>e</sub><sup>typ</sup> u then C(t) ≤<sub>e</sub><sup>typ</sup> C(u), for every context C.

(2) Silent β-invariance: if t →β<sub>τ</sub> u then [[t]]<sup>e</sup> = [[u]]<sup>e</sup>.

(3) No η-reduction: for all players p, q ∈ {•, ◦} . [[λ<sub>p</sub>y.x<sup>•q</sup> y]]<sup>e</sup> ⊈ [[x]]<sup>e</sup>.

(4) No η-expansion: for all players p, q ∈ {•, ◦} . [[x]]<sup>e</sup> ⊈ [[λ<sub>p</sub>y.x<sup>•q</sup> y]]<sup>e</sup>.

The fact that the checkers relational interpretation invalidates η-reduction, is specific to interaction arrow types. As an example of Thm. 7.3(3), consider the black η-expansion of x:

$$\frac{\substack{x: [0 \xrightarrow{\circ\bullet} L] \vdash_e^0 x : 0 \xrightarrow{\circ\bullet} L \qquad ax \\ x: [0 \xrightarrow{\circ\bullet} L] \vdash_e^1 x \bullet y : L \\ x: [0 \xrightarrow{\circ\bullet} L] \vdash_e^1 \lambda_{\bullet} y.x \bullet y : 0 \xrightarrow{\bullet p} L}}{\substack{\vdash_e^0 y : 0 \\ @e \\ \lambda}}$$

and note that instead $x: [0 \xrightarrow{\circ\bullet} L] \vdash_e^k x: 0 \xrightarrow{\bullet p} L$, for all indices k and players p. An analogous typing derivation shows that $\lambda_{\bullet}y.x \circ y \notin \vdash_e^{typ} x$.

**COROLLARY 7.4.** The black type preorder ≤<sup>•typ</sup> is an inequational λ-theory. Moreover, ≤<sup>•typ</sup> is neither extensional nor semi-extensional.

**Adequacy with Respect to Checkers Head Reduction.** As in the plain type system, the applicative size $|\pi|_{@}$ of type derivations (which is still defined as the number of rules @ in $\pi$, even if the rule itself has changed) decreases with each head step $\to_{h_{\circ}}$. The difference, however, is that if the step is an interaction one—and only in that case—then also the index k decreases by exactly 1.

**PROPOSITION 7.5.** Let t, t' ∈ Λ<sub>◦</sub><sub>◦</sub> be such that t $\to_{h_{\circ}}$ t'.

(1) Quantitative subject reduction: if $\pi \triangleright \Gamma \vdash_e^k t:L$ then there is a derivation $\pi' \triangleright \Gamma \vdash_e^{k'} t':L$ such that $|\pi'|_{@} = |\pi|_{@} - 1$. Moreover, if $t \to_{h_{\circ}} t'$ then $k' = k - 1$ and if $t \to_{h_{\circ}} t'$ then $k' = k$.

(2) Subject expansion: if $\pi' \triangleright \Gamma \vdash_e^k t:L$ then there is a derivation $\pi \triangleright \Gamma \vdash_e^k t:L$.
As before, quantitative subject reduction entails the correctness of the checkers type system, and the following typability of head normal forms gives its completeness.

**PROPOSITION 7.6 (TYPABILITY OF HEAD NORMAL FORMS).** Let $h \in \Lambda_{\circ\bullet}$ be a head normal form. Then there exists a derivation $\pi \triangleright \Gamma \vdash_{\bullet} h: L$.

Typability of all head normal forms (Prop. 7.6) together with subject expansion (Prop. 7.5(2)) implies the completeness of the type system: every head terminating term is typable. Summing up, we obtain the following characterization of head normalization.

**THEOREM 7.7 (TYPABILITY CHARACTERIZES HEAD NORMALIZATION).** Let $t \in \Lambda_{\circ\bullet}$.

(1) Correctness: if $\pi \triangleright \Gamma \vdash_{\bullet} t: L$ then there exists a $h_{\circ\bullet}$-normal form $h$ and an evaluation sequence $e: t \to_{h_{\circ\bullet}}^n h$ with $n \le |\pi|_@$ and such that the number of interaction steps in $e$ is $\le k$.

(2) Completeness: if $t \to_{h_{\circ\bullet}}^* h$ is a head normalizing sequence, then there exists $\pi \triangleright \Gamma \vdash_{\bullet} t: L$.

Therefore, $[[t]]^{\bullet} \neq \emptyset$ if and only if $t$ is $h_{\circ\bullet}$-normalizable.

# 8 From the Böhm Preorder to the Interaction One, via Multi Types

In this section, we use the obtained results about checkers multi types to prove the chain of inclusions $\sqsubseteq_B \subseteq \sqsubseteq^{\bullet\text{typ}} \subseteq \sqsubseteq^{\text{int}}$, as to complete the proof that $\sqsubseteq_B = \sqsubseteq^{\text{int}}$. The first inclusion $\sqsubseteq_B \subseteq \sqsubseteq^{\bullet\text{typ}}$ is simple: it follows from an easy induction on the size of checkers type derivations, exploiting the properties of the checkers type system. The second inclusion $\sqsubseteq^{\bullet\text{typ}} \subseteq \sqsubseteq^{\text{int}}$ requires slightly more work. The key point is to show that the type preorder preserves the number of interaction steps during head normalization in $\Lambda_{\circ\bullet}$, that is, that if $t \Vdash_{h_{\circ\bullet}}^{\bullet k}$ and $t \sqsubseteq_{\bullet}^{\text{typ}} u$ then $u \Vdash_{h_{\circ\bullet}}^{\bullet k}$. Such a property requires to characterize a class of checkers type derivations whose index captures exactly the number of head interaction steps to head normal form. We do it via a notion of *tight typing*.

*The First Inclusion.* The proof of the following proposition goes by a simple induction on the size of derivations. The use of *quantitative subject reduction* (hence of multi types, instead of idempotent intersection types) is critical in order for the induction argument to go through.

**THEOREM 8.1 (THE BÖHM PREORDER IS INCLUDED IN THE CHECKERS TYPE PREORDER).** Let $t, u \in \Lambda$. If $t \sqsubseteq_B u$ then $t \sqsubseteq^{\bullet\text{typ}} u$.

**PROOF.** Assume $t \sqsubseteq_B u$. If $t \Vdash_h$ then by Proposition 3.13 also $\bar{t}^{\bullet}$ is not $h_{\circ\bullet}$-normalizable. From Thm. 7.7, we obtain $[[\bar{t}^{\bullet}]]^{\bullet} = \emptyset \subseteq [[\bar{u}^{\bullet}]]^{\bullet}$ whence $t \sqsubseteq^{\bullet\text{typ}} u$ (by definition).

Otherwise, we must have $t \Vdash_h h_t := \lambda x_1 \dots x_m \cdot y \ t_1 \dots t_n$ and $u \Vdash_h h_u := \lambda x_1 \dots x_m \cdot y \ u_1 \dots u_n$, with $(t_i \sqsubseteq_B u_i)_{i \le n}$. Let us take any typing $(\Gamma, k, L) \in [[\bar{t}^{\bullet}]]^{\bullet}$, and show that it belongs to $[[\bar{u}^{\bullet}]]^{\bullet}$. We proceed by induction on the size $|\pi|_@$ of a derivation $\pi \triangleright \Gamma \vdash_{\bullet} \bar{t}^{\bullet}: L$. By Prop. 3.13(1) we get $\bar{t}^{\bullet} \to_{h_{\tau}}^{*} \bar{h}_t^{\bullet}$, and by quantitative subject reduction (Prop. 7.5(1)) there is a derivation $\pi_{hnf} \triangleright \vdash_{\bullet}^{k'} \bar{h}_t^{\bullet}: L$ such that $k = k'$ (since all head reductions involved are silent) and $|\pi_{hnf}|_@ \le |\pi|_@$. Moreover,

$$ \pi_{hnf} = \frac{\Delta_0 \vdash_{\bullet}^0 y : N_1 \xrightarrow{p_1} \dots N_n \xrightarrow{p_n} L' \quad (\pi_i \triangleright \Delta_i \vdash_{\bullet}^{k_i} \bar{t}_i^{\bullet} : N_i)_{1 \le i \le n} \quad n \ @ \quad \frac{\Gamma, (x_i : M_i)_{1 \le i \le m} \vdash_{\bullet}^{k} \frac{y t_1 \dots t_n}{\Gamma} : L'}{\Gamma \vdash_{\bullet}^{k} \bar{h}_t^{\bullet} : L = M_1 \xrightarrow{\bullet q_1} \dots M_n \xrightarrow{\bullet q_m} L'} m \lambda}{\pi_{hnf} = \frac{\Delta_0 \vdash_{\bullet}^0 y : N_1 \xrightarrow{p_1} \dots N_n \xrightarrow{p_n} L' \quad (\pi_i \triangleright \Delta_i \vdash_{\bullet}^{k_i} \bar{t}_i^{\bullet} : N_i)_{1 \le i \le n} \quad n \ @ \quad \frac{\Gamma, (x_i : M_i)_{1 \le i \le m} \vdash_{\bullet}^{k} \frac{y t_1 \dots t_n}{\Gamma} : L'}{\Gamma \vdash_{\bullet}^{k} \bar{h}_t^{\bullet} : L = M_1 \xrightarrow{\bullet q_1} \dots M_n \xrightarrow{\bullet q_m} L'} m \lambda} $$

where $n$ @ (resp. $m \lambda$) denotes $n$ (resp. $m$) consecutive applications of the rule, and

$$ - \Gamma, (x_i : M_i)_{1 \le i \le m} = \biguplus_{0 \le i \le n} \Delta_i; $$

$$ - \sum_{1 \le i \le n} (k_i + \gamma_{\bullet}(p_i)) = k, \text{ where } \gamma_{\bullet}(a) := 0 \text{ if } a = \bullet, \text{ and } \gamma_{\bullet}(a) := 1 \text{ otherwise.} $$
Note that, for every $i \le n$, $t_i \subseteq_B u_i$ and $|\pi_i|_@ < |\pi_{hnf}|_@ \le |\pi|_@$, so we can apply the $i.h.$ to each linear type in the multi type $N_i$ and get a derivation $\Delta_i \vdash_{\bullet}^{k_i} \bar{u}_i^\bullet : N_i$. We use these derivations to build the appropriate derivation for $h_u$:

$$ \frac{\Delta_0 \vdash_{\bullet}^0 y : N_1 \xrightarrow{p_1^\bullet} \dotsb \xrightarrow{p_n^\bullet} L' \quad (\pi_{u_i} \triangleright \Delta_i \vdash_{\bullet}^{k_i} \bar{u}_i^\bullet : N_i)_{1 \le i \le n}}{\frac{\Gamma, (x_i : M_i)_{1 \le i \le m} \vdash_{\bullet}^k \overline{y u_1 \dotsb u_n^\bullet} : L'}{\Gamma \vdash_{\bullet}^k \overline{h_u^\bullet} : L = M_1 \xrightarrow{\bullet q_1} \dotsb M_n \xrightarrow{\bullet q_m} L}} m \lambda \quad n @ $$

By Prop. 3.13(1) we get $\overline{u}^\bullet \to_{h_r}^* \overline{h}_u^\bullet$ and by subject expansion (Prop. 7.5(2)) we obtain $\Gamma \vdash_{\bullet}^{k'} \overline{u}^\bullet : L$. Since all head reductions involved are silent, we conclude $k = k'$ and $(\Gamma, k, L) \in [[\overline{u}^\bullet]]^\bullet$.

(Note that a 'hidden' base case is when $n = 0$, as it does not require the induction hypothesis.) $\square$

*The Second Inclusion, via Tight Typings.* Now, we consider a *tight* predicate on type judgements that forces the index $k$ on the type derivation to be exactly the number of head interaction steps to head normal form, as we show below. An essential aspect is the fact that the predicate concerns *types*, and not *type derivations*, so that it can be transferred from $t$ to $u$ when they are related by the type preorder, that is, when $t \subseteq_{\bullet}^{\text{typ}} u$.

**DEFINITION 8.2 (TIGHT TYPINGS AND DERIVATIONS).** Let $t \in \Lambda_{\circ, \bullet}$ and $\Gamma \vdash_{\bullet} t : L$ be a type judgement. The pair $(\Gamma, L)$ is a tight typing if:

(1) All multi types $M$ occurring in $\Gamma$ and $L$ are empty except for one, and

(2) All arrows in $(\Gamma, L)$ are silent.

*For ease of language, we shall also say that a derivation $\pi \triangleright \Gamma \vdash_{\bullet} t : L$ is tight if $(\Gamma, L)$ is a tight typing.*

The definition of tight typing can actually be slightly weakened, by asking that only the arrows in the non-empty multi type are silent, without losing any of its properties. This weakened definition, however, is slightly more technical, which is why we avoid it.

The crucial property ensured by tightness is that tightly typed head normal forms have interaction index 0, and that a tight typing can be derived for every head normal form.

**PROPOSITION 8.3 (TIGHTNESS AND HEAD NORMAL FORMS).** Let $h \in \Lambda_{\circ, \bullet}$ be a $h_{\circ, \bullet}$-normal form.

(1) Existence: there exists a tight derivation $\Gamma \vdash_{\bullet}^k h : L$;

(2) Zero interaction: if $\Gamma \vdash_{\bullet}^k h : L$ is tight then $k = 0$.

From the properties of tightness for head normal forms and the characterization of head reduction (Thm. 7.7), we obtain the following refined characterization.

**THEOREM 8.4 (TIGHT CHARACTERIZATION).** Let $t \in \Lambda_{\circ, \bullet}$.

(1) Correctness: if $\pi : \Gamma \vdash_{\bullet}^k t : L$ is tight then there exists a head normal form $h$ and an evaluation sequence $e : t \to_{h_{\circ, \bullet}}^* h$ such that the number of interaction steps in $e$ is exactly $k$.

(2) Completeness: if $e : t \to_{h_{\circ, \bullet}}^* h$ with $h$ head normal, and $k$ is the number of interaction steps in $e$, then there exists a tight derivation $\pi : \Gamma \vdash_{\bullet}^k t : L$.

**PROOF.**

(1) By correctness (Thm. 7.7(1)), there exists an evaluation sequence $e : t \to_{h_{\circ, \bullet}}^* h$ such that the number of interaction steps in $e$ is $k' \le k$. By quantitative subject reduction (Prop. 7.5(1)), $\Gamma \vdash_{\bullet}^{k-k'} h : L$. Since $(\Gamma, L)$ is tight, by the zero interaction property of tight typings (Prop. 8.3(2)) we obtain $k - k' = 0$, that is, $k' = k$.
(2) By the existence of tight derivations for head normal forms (Prop. 8.3(1)), we obtain a tight derivation $\pi \vdash \Gamma \vdash_\epsilon^0 h : L$. By subject expansion (Prop. 7.5), the same typing types $t$ but with an index $k'$, i.e. $\Gamma \vdash_\epsilon^k k' t : L$. By Point 1, $t \to_{h_{\circ}, \epsilon}^* h'$ for some head normal form $h'$ doing $k'$ interaction steps. By determinism of $\to_{h_{\circ}, \epsilon}$, $h = h'$ and $k = k'$. $\square$

The tight characterization is then used to show that the type preorder is sound with respect to the interaction preorder.

### COROLLARY 8.5.

(1) Tightness of the checkers type preorder: $\text{let } t, u \in \Lambda_{\circ\bullet}$. If $t \Vdash_{h_{\circ\bullet}}^{\epsilon k}$ and $t \sqsubseteq_{\epsilon}^{\text{typ}} u$ then $u \Vdash_{h_{\circ\bullet}}^{\epsilon k}$.

(2) Soundness of the checkers type preorder: $\text{let } t, u \in \Lambda_{\circ\bullet}$. If $t \sqsubseteq_{\epsilon}^{\text{typ}} u$ then $t \sqsubseteq_{\epsilon}^{\text{ctx}} u$.

(3) On ordinary $\lambda$-terms: $\text{let } t, u \in \Lambda$. If $t \sqsubseteq^{\bullet\text{typ}} u$ then $t \sqsubseteq^{\text{int}} u$.

### PROOF. (3) follows immediately from (2).

(1) Let $t$ and $u$ such that $t \sqsubseteq_{\epsilon}^{\text{typ}} u$ and $t \Vdash_{h_{\circ\bullet}}^{\epsilon k}$. By tight completeness (Thm. 8.4(2)), there exists a tight typing $\Gamma, L$ such that $\Gamma \vdash_\epsilon^k t : L$. By $t \sqsubseteq_{\epsilon}^{\text{typ}} u$, we obtain a derivation of $\Gamma \vdash_\epsilon^k u : L$. By tight correctness (Thm. 8.4(1)) and tightness of $(\Gamma, L)$, we obtain $u \Vdash_{h_{\circ\bullet}}^{\epsilon k}$.

(2) Let $t, u \in \Lambda_{\circ\bullet}$ such that $t \sqsubseteq_{\epsilon}^{\text{typ}} u$. By compatibility of $\sqsubseteq_{\epsilon}^{\text{typ}}$ (Thm. 7.3(1)), $C\langle t \rangle \sqsubseteq_{\epsilon}^{\text{typ}} C\langle u \rangle$ for all $C \in C_{\circ\bullet}$. By tightness of $\sqsubseteq_{\epsilon}^{\text{typ}}$ (Point 1), if $C\langle t \rangle \Vdash_{h_{\circ\bullet}}^{\epsilon k}$ then $C\langle u \rangle \Vdash_{h_{\circ\bullet}}^{\epsilon k}$. Hence, $t \sqsubseteq_{\epsilon}^{\text{ctx}} u$. $\square$

We can now put the all the inclusions together, thus obtaining our main theorem.

### THEOREM 8.6 (TREE AND TYPE CHARACTERIZATIONS OF INTERACTION EQUIVALENCE).
The preorders $\sqsubseteq_B$, $\sqsubseteq^{\bullet\text{typ}}$, and $\sqsubseteq^{\text{int}}$ coincide. Therefore, the $\lambda$-theories $=_B$, $\equiv^{\bullet\text{typ}}$, and $\equiv^{\text{int}}$ coincide.

### PROOF. ($\sqsubseteq_B \sqsubseteq^{\bullet\text{typ}}$) By Thm. 8.1. ($\sqsubseteq^{\bullet\text{typ}} \sqsubseteq^{\text{int}}$) By Cor. 8.5(3). ($\sqsubseteq^{\text{int}} \sqsubseteq_B$) By Thm. 5.4. $\square$

*Back to a Delayed Proof.* We can now finally prove Thm. 3.11, stating that silent conversion $=_{\beta_r}$ is included in the checkers interaction preorder $\sqsubseteq^{\text{int}}$, which is the key point of the proof that the interaction preorder $\sqsubseteq^{\text{int}}$ is an inequational $\lambda$-theory (Cor. 3.12).

### THEOREM 3.11 (THE INTERACTION PREORDER INCLUDES SILENT CONVERSION).
For all checkers terms $t, u \in \Lambda_{\circ\bullet}$, $t =_{\beta_r} u$ entails $t \sqsubseteq_{\epsilon}^{\text{ctx}} u$.

### PROOF. From Thm. 7.3(2), if $t =_{\beta_r} u$ then $t \sqsubseteq_{\epsilon}^{\text{typ}} u$. By Cor. 8.5(2), we obtain $t \sqsubseteq_{\epsilon}^{\text{ctx}} u$. $\square$

*Interaction Improvement and $\eta$.* We provided Böhm tree characterizations of $\sqsubseteq^{\text{int}}$ and $\equiv^{\text{int}}$, but not of the interaction improvement $\sqsubseteq^{\text{int-imp}}$. Nonetheless, we almost have one. In the previous sections, we obtained the following chain of relationships:

$$ \sqsubseteq_B =_{T.8.6} \sqsubseteq^{\text{int}} \sqsubseteq_{L.3.16} \sqsubseteq^{\text{int-imp}} \sqsubseteq_{L.3.16} \sqsubseteq^{\text{ctx}} =_{T.4.7} \sqsubseteq_B \eta^{\infty} \quad (4) $$

That is, interaction improvement $\sqsubseteq^{\text{int-imp}}$ possibly enlarges the interaction preorder $\sqsubseteq^{\text{int}}$ and yet stays confined within the further fence of $\eta$-equivalence. Additionally, the fact that $\eta$-reduction can decrease the number of interactions (Ex. 3.6) suggests the following.

### CONJECTURE 8.7.
Interaction improvement $\sqsubseteq^{\text{int-imp}}$ is characterized by $\sqsubseteq_B \eta^{\infty}$, the variant of $\sqsubseteq_B \eta^{\infty}$ (Definition 4.5) up to possibly infinite $\eta$-reduction (rather than $\eta$-equivalence).

Breuvart et al. [2018] prove that the preorder $\sqsubseteq_B \eta^{\infty}$ coincides with the preorder $\sqsubseteq^{\text{typ}}$ induced by (plain) multi types (Definition 6.2), which validates $\eta$-reduction (Thm. 6.3.3). As already mentioned, the difficulty for proving the conjecture is managing $\eta$-reduction in the checkers framework, since both rewriting techniques and checkers multi types fail to handle it. Actually, the variant of Böhm
out technique of Section 5 smoothly adapts from preorder to improvement, giving $\sqsubseteq^{\text{int-imp}} \subseteq \mathcal{B}\eta_{\text{red}}^{\infty}$, that is, $\mathcal{B} \subseteq \sqsubseteq^{\text{int-imp}} \subseteq \mathcal{B}\eta_{\text{red}}^{\infty}$. Therefore, conjecture 8.7 reduces to prove $\mathcal{B}\eta_{\text{red}}^{\infty} \subseteq \sqsubseteq^{\text{int-imp}}$.

*White Contexts Are Enough.* In the proof of the completeness theorem (Thm. 5.4), black terms are separated using only white contexts. The next corollary guarantees that, for the interaction preorder, white contexts are as discriminating as general checkers contexts. Such a strong fact validates the intuition that the interaction preorder amounts to consider the program and the context as *different* players.

COROLLARY 8.8 (THE INTERACTION PREORDER CAN BE RESTRICTED TO WHITE CONTEXTS). Let $t, u \in \Lambda$ and the preorder $t \sqsubseteq^{\text{int}} u$ be defined as: for all ordinary contexts $C \in \mathcal{C}$, if there exists $k$ such that $\bar{C} \stackrel{\bullet}{\sqsubseteq} \langle t^\bullet \rangle \Uparrow_{h_o}^{\bullet k}$ then $\bar{C} \stackrel{\circ}{\sqsubseteq} \langle \bar{u}^\bullet \rangle \Uparrow_{h_o}^{\bullet k}$. Then, $t \sqsubseteq^{\text{int}} u$ if and only if $t \sqsubseteq^{\text{int}} u$.

PROOF. Thm. 5.4 shows that $t \sqsubseteq^{\text{int}} u$ implies $t \sqsubseteq \mathcal{B} u$. Thm. 8.6 shows that $t \sqsubseteq \mathcal{B} u$ implies $t \sqsubseteq^{\text{int}} u$. Clearly $t \sqsubseteq^{\text{int}} u$ implies $t \sqsubseteq^{\text{int}} u$, as $\bar{C}^\circ$ is a checkers context for any $C \in \mathcal{C}$. $\square$

# 9 Related Work

*Improvements.* Improvements [Sands 1996a,b, 1999] were developed in the '90s by Sands and co-authors to prove that various program transformations are time or space improvements [Gustavsson and Sands 2001; Moran and Sands 1999; Sands 1996a], in the context of call-by-need evaluation, and have seen a revival in recent years [Hackett and Hutton 2014, 2015, 2018; Muroya and Hamana 2024; Riely and Prins 2000; Schmidt-Schauß et al. 2018].

*Observational Equivalences and Trees.* The characterization of observational equivalences in terms of equalities on trees originates in [Hyland 1975, 1976; Wadsworth 1976], and is an ongoing line of research whose state of the art is presented in [Intrigila et al. 2019]. The question appears in the TLCA list of open problems [Dezani-Ciancaglini 2001]. This paper contributes to this line of research, somewhat backwards: we introduce a new observational equivalence that matches a known equality on trees, namely non-extensional Böhm tree equality $\mathcal{B}$.

*Böhm Tree Equality.* For the specific case of $\mathcal{B}$, the literature already presents some corresponding observational equivalences. As hinted at in the introduction, however, they are *partial* answers since they all extend the $\lambda$-calculus with computational primitives, or embed it into process algebras:

* Dezani-Ciancaglini et al. [1998] add numerals, tests, and a non-deterministic choice operator, and show that $\mathcal{B}$ corresponds to *may convergence to a natural number* in their calculus.

* In the slightly different setting of *weak head reduction*, Sangiorgi [1994] shows that Lévy-Longo tree equality (the weak variant of $\mathcal{B}$) corresponds to various contextual equivalences all obtained via extended settings, namely the $\pi$-calculus, $\lambda$-calculus with non-determinism, and $\lambda$-calculus with well-formed operators. Similarly, Dezani-Ciancaglini et al. use another non-deterministic $\lambda$-calculus [1999], and Boudol and Laneve [1996] use a $\lambda$-calculus with modified syntax and rewriting rules where—crucially—terms can get stuck.

* Recently, Sakayori and Sangiorgi [2023] provide a characterization of $\mathcal{B}$ via the $\pi$-calculus.

In this paper, we do modify the $\lambda$-calculus via the checkers calculus, but we do *not* add extra features, we only refine the analysis of $\beta$-reduction in a quantitative and interactive way.

*Clocked $\lambda$-Calculus.* The idea of discriminating $\lambda$-terms by counting the head reduction steps in the construction of their Böhm trees also underlies the *clocked $\lambda$-calculus* of Endrullis et al. [2014, 2017]. The analogy ends there, as the clocked $\lambda$-calculus does not allow one to separate the internal/silent steps of terms and contexts from the external/interaction steps between the two.
*Game Semantics.* Our notion of interaction is inspired by the one between Player and Opponent in game semantics [Abramsky et al. 2000; Hyland and Ong 2000]—see Clairambault [2024] for the state of the art—in particular, silent steps are inspired by the hiding mechanism for composing games. We end up, however, with what seems to be a different setting. While the study of the relationship is left to future work, our interaction seems more basic (no need of the technical apparatus of game semantics), perfectly symmetrical, and allows for arbitrary shuffling of the two players in checkers terms, rather than keeping them apart as in game semantics. Moreover, with a few exceptions—namely, [Ker et al. 2003; Ong and Di Gianantonio 2002]—game models usually validate η-equivalence, while interaction equivalence does not. Notably, the game model by Ker et al. [2003] captures exactly *B*.

*Multi Types.* The quantitative analysis of the relational semantics via multi types was pioneered by de Carvalho [2018]. Then Bernadet and Lengrand [2011]; de Carvalho et al. [2011] and especially Accattoli et al. [2020] developed and extended that approach, that has been applied to a variety of settings, including classical logic [Kesner and Vial 2020], the probabilistic λ-calculus [Dal Lago et al. 2021], reasonable space [Accattoli et al. 2022], and Bayesian networks [Faggian et al. 2024].

*Variants of Relational Semantics.* Relational semantics is generalized along several directions by Grellois and Melliès [2015]; Laird et al. [2013]; Ong [2017]. Laird et al.'s generalization of relations $r \subseteq A \times B$ from $r: A \times B \to \text{Bool}$ to $r: A \times B \to \mathcal{R}$ [2013], where $\mathcal{R}$ is a continuous semi-ring, might be used—in principle—to count interaction steps. The exact meaning of the coefficients in the interpretation of programs, however, is well-understood only at ground types, and remains unclear in the untyped case. Any temptation of seeing our checkers type system as a dichromatic version of Grellois and Melliès's *colored linear logic* [2015] should be avoided: in their work, colors need to correctly “match” in a type derivation because they represent different levels of priority.

*Cost-Aware Denotational Semantics.* Another line of research aims at defining cost-sensitive denotational semantics based on *sized* domains [Danner and Licata 2022; Kavvos et al. 2020]. These models are used to interpret a syntactic recurrence extracted from a given program, and prove a bounding theorem about such extraction. Niu and Harper [2023] propose a synthetic language for cost-aware denotational semantics, endowed with phase-separated constructions of intensional and extensional computations. These approaches are designed for typed languages with constants, where observations are made at ground type, but they are hardly generalizable to the untyped case.

There also are cost-aware game models such as Ghica's slot games [2005]—which capture Sands' improvements—and Alcolei et al.'s resource-tracking concurrent games [2019]. The relationship between these concurrency-driven models and our approach is deferred to future investigation.

# 10 Future Work

*Weak Head.* Our study focuses on the paradigmatic case of head reduction, but it could be adapted to weak head reduction (sometimes called *lazy* reduction [Abramsky and Ong 1993]). It is folklore that the Lévy-Longo tree preorder (a weak variant of Böhm trees) matches the weak head type preorder. We conjecture that the Lévy-Longo tree preorder matches exactly the weak head variant of our interaction preorder. Most of our study would adapt smoothly, but for the interaction Böhm out. The culprit is that there is no analogous of Böhm separation theorem for weak head reduction. There exist separation results but they all involve extensions of the λ-calculus (see above among related works). Crafting a weak interaction Böhm out might require some work.

*Call-by-Value.* In call-by-name, the gap between head normal form bisimilarity (aka interaction equivalence), and contextual equivalence is, roughly, extensionality. In call-by-value, the gap contains more computational principles, as stressed in particular by the recent works [Accattoli
et al. 2023; Accattoli and Lancelot 2024]. It would be interesting to adapt interaction equivalence to
call-by-value and explore whether variants of the definition catch theories in between.

*Back to Improvements.* Now that there is a notion of equational improvement, it is natural to adapt it to call-by-need and compare / revisit / extend the results about Sands’ (non-equational) improvements and program transformations in the literature [Gustavsson and Sands 2001; Hackett and Hutton 2014, 2015, 2018; Moran and Sands 1999; Sands 1996a; Schmidt-Schauß et al. 2018].

*Game Semantics.* To relate interaction equivalence with game semantics, it is natural to look at the Böhm tree game model by Ker et al. [2003]. Operational game semantics [Jaber and Sangiorgi 2022; Laird 2007; Levy and Staton 2014], a sub-area of game semantics based on labeled transition systems, is another natural candidate. More generally, our work provides a good justification for a systematic exploration of non-extensional game semantics.

PCF. Game semantics was introduced to capture denotationally PCF contextual equivalence, which is obtained via a quotient on games [Abramsky et al. 2000; Hyland and Ong 2000]. Is there a relationship between game models *before the quotient* and PCF interaction equivalence?

*Higher-Order Model Checking.* Higher-order model checking is strongly connected to game semantics [Ong 2006], intersection/multi types [Kobayashi 2009], and Böhm trees [Clairambault and Murawski 2013]. It is reasonable to expect a connection with interaction equivalence.

*Complete Normal Form Bisimilarities.* In some $\lambda$-calculi with effects, normal form bisimilarities are complete for contextual equivalences [Biernacki et al. 2019; Støvring and Lassen 2009]. We conjecture that, therein, contextual equivalence and interaction equivalence coincide.

*Interaction Cost.* It is natural to wonder what kind of interaction cost emerges from our study and how it relates to both the actual cost of computation and interaction (in)equivalence. The characterization of our interaction improvement in terms of Böhm trees reveals that one can improve the interactive cost of a $\lambda$-term by performing $\eta$-reductions, or by replacing some head-diverging sub-term—that is, an idle looping execution branch—with a non-looping one. Beyond Böhm tree characterizations, this may also relate to the length of interaction sequences in game semantics for the untyped call-by-name $\lambda$-calculus, where interaction improvements could reflect optimizations in communication between player and opponent.

We believe that our interaction semantics can also effectively capture communication costs in the evaluation of functional programs within distributed environments. In this framework, black and white terms correspond to processes running on different machines, with interaction steps modeling inter-process communication, while locally executable steps remain silent. To formalize this idea, we shall first adapt our interaction relations to a process calculus, and then investigate how the resulting improvements in interaction relates with measures of communication complexity.

# 11 Conclusions

Our work stems from the recognition of a tension between the equational aspect of contextual equivalences and the desire to observe the time cost of programs, expressed as the number of evaluation steps. We solve the tension by introducing the *checkers calculus*, a $\lambda$-calculus where the internal and external aspects of computation receive a first-class status. The new setting is then used to define *interaction equivalence*, which induces an equational theory for the ordinary $\lambda$-calculus: a very well-known one, namely the equality $\mathcal{B}$ of Böhm trees without $\eta$.

Beyond the technical aspects, the main takeaway is probably the framework, which is considerably simpler than other theories of interaction such as game semantics or the geometry of interaction, and not *ad-hoc*, as witnessed by the relationship with $\mathcal{B}$ and with multi types.
Acknowledgments

The authors would like to thank Guilhem Jaber for many discussions about operational game semantics for the λ-calculus, which eventually led us to the idea of tagging terms to distinguish between silent and interaction steps.

References

Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Abstraction for PCF. Inf. Comput. 163, 2 (2000), 409-470. https://doi.org/10.1006/INCO.2000.2930

Samson Abramsky and C.-H. Luke Ong. 1993. Full Abstraction in the Lazy Lambda Calculus. Inf. Comput. 105, 2 (1993), 159-267. https://doi.org/10.1006/INCO.1993.1044

Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2022. Multi types and reasonable space. Proc. ACM Program. Lang. 6, ICFP (2022), 799-825. https://doi.org/10.1145/3547650

Beniamino Accattoli, Claudia Faggian, and Adrienne Lancelot. 2023. Normal Form Bisimulations By Value. CoRR abs/2303.08161 (2023). https://doi.org/10.48550/ARXIV.2303.08161 arXiv:2303.08161

Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. 2020. Tight typings and split bounds, fully developed. J. Funct. Program. 30 (2020), e14. https://doi.org/10.1017/S095679682000012X

Beniamino Accattoli and Adrienne Lancelot. 2024. Mirroring Call-By-Need, or Values Acting Silly. In 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia (LIPIcs, Vol. 299), Jakob Rehof (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 23:1-23:24. https://doi.org/10.4230/LIPICS.FSCD.2024.23

Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, and Gabriele Vanoni. 2024. Interaction Equivalence. CoRR abs/2409.18709 (2024). https://doi.org/10.48550/ARXIV.2409.18709 arXiv:2409.18709

Peter Aczel. 1978. *A General Church-Rosser Theorem*. Technical Report. University of Manchester.

Aurore Alcolei, Pierre Clairambault, and Olivier Laurent. 2019. Resource-Tracking Concurrent Games. In Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11425), Mikolaj Bojanczyk and Alex Simpson (Eds.). Springer, 27-44. https://doi.org/10.1007/978-3-030-17127-8_2

Henk Barendregt. 1977. The Type Free Lambda Calculus. In Handbook of Mathematical Logic, Jon Barwise (Ed.). Studies in Logic and the Foundations of Mathematics, Vol. 90. Elsevier, 1091 - 1132.

Henk Barendregt. 1984. *The Lambda Calculus – Its Syntax and Semantics*. Studies in logic and the foundations of mathematics, Vol. 103. North-Holland.

Henk Barendregt and Giulio Manzonetto. 2022. A Lambda Calculus Satellite. College Publications. https://www.collegepublications.co.uk/logic/mlf/700035

Alexis Bernadet and Stéphane Lengrand. 2011. Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types. In Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6604), Martin Hofmann (Ed.). Springer, 88-107. https://doi.org/10.1007/978-3-642-19805-2_7

Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. 2019. A Complete Normal-Form Bisimilarity for State. In Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings (Lecture Notes in Computer Science, Vol. 11425), Mikolaj Bojanczyk and Alex Simpson (Eds.). Springer, 98-114. https://doi.org/10.1007/978-3-030-17127-8_6

Corrado Böhm. 1968. Alcune proprietà delle forme β-η-normali nel λ-K-calcolo. Pubblicazioni dell'istituto per le applicazioni del calcolo 696 (1968), 1-19. Lavoro eseguito all'INAC.

Gérard Boudol and Cosimo Laneve. 1996. The Discriminating Power of Multiplicities in the λ-Calculus. Information and Computation 126, 1 (1996), 83-102. https://doi.org/10.1006/inco.1996.0037

Flavien Breuvart, Giulio Manzonetto, and Domenico Ruopolo. 2018. Relational Graph Models at Work. Log. Methods Comput. Sci. 14, 3 (2018). https://doi.org/10.23638/LMCS-14(3:2)2018

Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. 2017. Non-idempotent intersection types for the Lambda-Calculus. Log. J. IGP 25, 4 (2017), 431-464. https://doi.org/10.1093/JIGPAL/JZX018

Pierre Clairambault. 2024. Causal Investigations in Interactive Semantics. https://tel.archives-ouvertes.fr/tel-04523273

Pierre Clairambault and Andrzej S. Murawski. 2013. Böhm Trees as Higher-Order Recursive Schemes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, December 12-14, 2013, Guwahati, India (LIPIcs, Vol. 24), Anil Seth and Nisheeth K. Vishnoi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 91–102. https://doi.org/10.4230/LIPICS.FSTTCS.2013.91

Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca. 2021. Intersection types and (positive) almost-sure termination. *Proc. ACM Program. Lang.* 5, POPL (2021), 1–32. https://doi.org/10.1145/3434313

Norman Danner and Daniel R. Licata. 2022. Denotational semantics as a foundation for cost recurrence extraction for functional languages. *J. Funct. Program.* 32 (2022), e8. https://doi.org/10.1017/S095679682200003X

Daniel de Carvalho. 2007. *Sémantiques de la logique linéaire et temps de calcul*. Thèse de Doctorat. Université Aix-Marseille II.

Daniel de Carvalho. 2018. Execution time of $\lambda$-terms via denotational semantics and intersection types. *Math. Struct. Comput. Sci.* 28, 7 (2018), 1169–1203. https://doi.org/10.1017/S0960129516000396

Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. 2011. A semantic measure of the execution time in linear logic. *Theor. Comput. Sci.* 412, 20 (2011), 1884–1902. https://doi.org/10.1016/j.tcs.2010.12.017

Mariangiola Dezani-Ciancaglini. 2001. TLCA list, Problem #18: Find trees representing contextual equivalences. See http://tlca.di.unito.it/opltla/.

Mariangiola Dezani-Ciancaglini, Benedetto Intrigila, and Marisa Venturini-Zilli. 1998. Böhm's theorem for Böhm trees. In *ICTCS*, Vol. 98. World Scientific, 1–23.

Mariangiola Dezani-Ciancaglini, Jerzy Tiuryn, and Pawel Urzyczyn. 1999. Discrimination by Parallel Observers: The Algorithm. *Information and Computation* 150, 2 (1999), 153–186. https://doi.org/10.1006/inco.1998.2773

Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky. 2014. Discriminating Lambda-Terms Using Clocked Boehm Trees. *Logical Methods in Computer Science* 10, 2 (2014). https://doi.org/10.2168/LMCS-10(2:4)2014

Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky. 2017. Clocked lambda calculus. *Math. Struct. Comput. Sci.* 27, 5 (2017), 782–806. https://doi.org/10.1017/S0960129515000389

Claudia Faggian, Daniele Pautasso, and Gabriele Vanoni. 2024. Higher Order Bayesian Networks, Exactly. *Proc. ACM Program. Lang.* 8, POPL (2024), 2514–2546. https://doi.org/10.1145/3632926

Dan R. Ghica. 2005. Slot games: a quantitative model of computation. In *Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005*, Long Beach, California, USA, January 12-14, 2005, Jens Palssberg and Martín Abadi (Eds.). ACM, 85–97. https://doi.org/10.1145/1040305.1040313

Charles Grellois and Paul-André Melliès. 2015. Relational Semantics of Linear Logic and Higher-order Model Checking. In *24th EACSL Annual Conference on Computer Science Logic, CSL 2015*, September 7-10, 2015, Berlin, Germany (LIPIcs, Vol. 41), Stephan Kreutzer (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 260–276. https://doi.org/10.4230/LIPICS.CSL.2015.260

Jörgen Gustavsson and David Sands. 2001. Possibilities and Limitations of Call-by-Need Space Improvement. In *Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01)*, Firenze (Florence), Italy, September 3-5, 2001, Benjamin C. Pierce (Ed.). ACM, 265–276. https://doi.org/10.1145/507635.507667

Jennifer Hackett and Graham Hutton. 2014. Worker/wrapper/makes it/faster. In *Proceedings of the 19th ACM SIGPLAN international conference on Functional programming*, Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 95–107. https://doi.org/10.1145/2628136.2628142

Jennifer Hackett and Graham Hutton. 2015. Programs for Cheap! In *30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015*, Kyoto, Japan, July 6-10, 2015. IEEE Computer Society, 115–126. https://doi.org/10.1109/LICS.2015.21

Jennifer Hackett and Graham Hutton. 2018. Parametric polymorphism and operational improvement. *Proc. ACM Program. Lang.* 2, ICFP (2018), 68:1–68:24. https://doi.org/10.1145/3236763

Martin Hyland. 1975. A survey of some useful partial order relations on terms of the lambda calculus. In *Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, Italy, March 25-27, 1975* (Lecture Notes in Computer Science, Vol. 37), Corrado Böhm (Ed.). Springer, 83–95. https://doi.org/10.1007/BF0029520

Martin Hyland. 1976. A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus. *Journal of the London Mathematical Society* s2-12, 3 (1976), 361–370. https://doi.org/10.1112/jlms/s2-12.3.361

Martin Hyland, Misao Nagayama, John Power, and Giuseppe Rosolini. 2004. A Category Theoretic Formulation for Engeler-style Models of the Untyped lambda. 161 (2004), 43–57. https://doi.org/10.1016/j.ENTCS.2006.04.024

Martin Hyland and C.-H. Luke Ong. 2000. On Full Abstraction for PCF: I, II, and III. *Inf. Comput.* 163, 2 (2000), 285–408. https://doi.org/10.1006/INCO.2000.2917

Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. 2019. Degrees of extensionality in the theory of Böhm trees and Sallé's conjecture. *Log. Methods Comput. Sci.* 15, 1 (2019). https://doi.org/10.23638/LMCS-15(1:6)2019

Guilhem Jaber and Davide Sangiorgi. 2022. Games, Mobile Processes, and Functions. In *30th EACSL Annual Conference on Computer Science Logic (CSL 2022)* (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 216), Florin Manea and Alex Simpson (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 25:1–25:18. https://doi.org/10.4230/LIPIcs.CSL.2022.25

G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner. 2020. Recurrence extraction for functional programs through call-by-push-value. *Proc. ACM Program. Lang.* 4, POPL (2020), 15:1–15:31. https://doi.org/10.1145/3371083
Andrew D. Ker, Hanno Nickau, and C.-H. Luke Ong. 2003. Adapting innocent game models for the Böhm tree λ-theory. *Theor. Comput. Sci.* 308, 1-3 (2003), 333-366. https://doi.org/10.1016/S0304-3975(02)00849-6

Delia Kesner and Pierre Vial. 2020. Consuming and Persistent Types for Classical Logic. In *LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020*, Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller (Eds.). ACM, 619-632. https://doi.org/10.1145/3373718.3394774

Jan Willem Klop. 1980. *Combinatory Reduction Systems*. PhD thesis. Utrecht University.

Naoki Kobayashi. 2009. Types and higher-order recursion schemes for verification of higher-order programs. In *Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009*, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 416-428. https://doi.org/10.1145/1480881.1480933

Jim Laird. 2007. A Fully Abstract Trace Semantics for General References. In *Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings (Lecture Notes in Computer Science, Vol. 4596)*, Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki (Eds.). Springer, 667-679. https://doi.org/10.1007/978-3-540-73420-8_58

Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. 2013. Weighted Relational Models of Typed Lambda-Calculi. In *28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013*. IEEE Computer Society, 301-310. https://doi.org/10.1109/LICS.2013.36

Søren B. Lassen. 1999. Bisimulation in Untyped Lambda Calculus: Böhm Trees and Bisimulation up to Context. 20 (1999), 346-374. https://doi.org/10.1016/S1571-0661(04)80083-5

Paul Blain Levy and Sam Staton. 2014. Transition systems over games. In *Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Vienna, Austria) (CSL-LICS '14)*. Association for Computing Machinery, New York, NY, USA, Article 64, 10 pages. https://doi.org/10.1145/2603088.2603150

Andrew Moran and David Sands. 1999. Improvement in a Lazy Context: An Operational Theory for Call-by-Need. In *POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999*, Andrew W. Appel and Alex Aiken (Eds.). ACM, 43-56. https://doi.org/10.1145/292540.292547

James Hiram Morris. 1968. *Lambda-calculus Models of Programming Languages*. Ph. D. Dissertation. Massachusetts Institute of Technology. https://books.google.is/books?id=DklAAQAAIAAJ

Koko Muroya and Makoto Hamana. 2024. Term Evaluation Systems with Refinements: First-Order, Second-Order, and Contextual Improvement. In *Functional and Logic Programming - 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15-17, 2024, Proceedings (Lecture Notes in Computer Science, Vol. 14659)*, Jeremy Gibbons and Dale Miller (Eds.). Springer, 31-61. https://doi.org/10.1007/978-981-97-2300-3_3

Tobias Nipkow. 1991. Higher-Order Critical Pairs. In *Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991*. IEEE Computer Society, 342-349. https://doi.org/10.1109/LICS.1991.151658

Yue Niu and Robert Harper. 2023. A Metalanguage for Cost-Aware Denotational Semantics. In *38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023*. IEEE, 1-14. https://doi.org/10.1109/LICS56636.2023.10175777

C.-H. Luke Ong. 2006. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In *21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings*. IEEE Computer Society, 81-90. https://doi.org/10.1109/LICS.2006.38

C.-H. Luke Ong. 2017. Quantitative semantics of the lambda calculus: Some generalisations of the relational model. In *32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017*. IEEE Computer Society, 1-12. https://doi.org/10.1109/LICS.2017.8005064

C.-H. Luke Ong and Pietro Di Gianantonio. 2002. Games Characterizing Lévy-Longo Trees. In *Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings (Lecture Notes in Computer Science, Vol. 2380)*, Peter Widmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew Hennessy, Stephan J. Eidenbenz, and Ricardo Conejo (Eds.). Springer, 476-487. https://doi.org/10.1007/3-540-45465-9_41

Marco Patrignani, Amal Ahmed, and Dave Clarke. 2019. Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work. *ACM Comput. Surv.* 51, 6 (2019), 125:1-125:36. https://doi.org/10.1145/3280984

Gordon D. Plotkin. 1977. LCF Considered as a Programming Language. *Theor. Comput. Sci.* 5, 3 (1977), 223-255. https://doi.org/10.1016/0304-3975(77)90044-5

James Riely and Jan F. Prins. 2000. Flattening Is an Improvement. In *Static Analysis, 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 1, 2000, Proceedings (Lecture Notes in Computer Science, Vol. 1824)*, Jens Palsberg (Ed.). Springer, 360-376. https://doi.org/10.1007/978-3-540-45099-3_19

Ken Sakayori and Davide Sangiorgi. 2023. Extensional and Non-extensional Functions as Processes. In *38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023*. IEEE, 1-13. https://doi.org/10.1109/LICS56636.2023.10175686
David Sands. 1996a. Proving the Correctness of Recursion-Based Automatic Program Transformations. *Theor. Comput. Sci.* 167, 1&2 (1996), 193–233. https://doi.org/10.1016/0304-3975(96)00074-6

David Sands. 1996b. Total correctness by local improvement in the transformation of functional programs. *ACM Trans. Program. Lang. Syst.* 18, 2 (mar 1996), 175–234. https://doi.org/10.1145/227699.227716

David Sands. 1999. *Improvement theory and its applications*. Cambridge University Press, USA, 275–306.

Davide Sangiorgi. 1994. The Lazy Lambda Calculus in a Concurrency Scenario. *Inf. Comput.* 111, 1 (1994), 120–153. https://doi.org/10.1006/INCO.1994.1042

Manfred Schmidt-Schauß, David Sabel, and Nils Dallmeyer. 2018. Sequential and Parallel Improvements in a Concurrent Functional Programming Language. In *Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018*, David Sabel and Peter Thiemann (Eds.). ACM, 20:1–20:13. https://doi.org/10.1145/3236950.3236952

Dana S. Scott. 1972. Continuous lattices. In *Toposes, Algebraic Geometry and Logic (Lecture Notes in Mathematics, Vol. 274)*, Lawvere (Ed.). Springer, 97–136. https://doi.org/10.1007/BFb0073967

Kristian Støvring and Søren B. Lassen. 2009. A Complete, Co-inductive Syntactic Theory of Sequential Control and State. In *Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday (Lecture Notes in Computer Science, Vol. 5700)*, Jens Palsberg (Ed.). Springer, 329–375. https://doi.org/10.1007/978-3-642-04164-8_17

Christopher P. Wadsworth. 1976. The Relation Between Computational and Denotational Properties for Scott's $D_∞$-Models of the Lambda-Calculus. *SIAM J. Comput.* 5, 3 (1976), 488–521. https://doi.org/10.1137/0205036

Received 2024-07-11; accepted 2024-11-07