# Separating Terms by Means of Multi Types, Coinductively

Adrienne Lancelot

► To cite this version:

Adrienne Lancelot. Separating Terms by Means of Multi Types, Coinductively. TYPES 2024 - 30th International Conference on Types for Proofs and Programs, Jun 2024, Copenhagen, Denmark. https://drops.dagstuhl.de/entities/volume/LIPIcs-volume-336, 10.4230/LIPIcs.TYPES.2024.4. hal-05470030

HAL Id: hal-05470030

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

Submitted on 21 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
# Separating Terms by Means of Multi Types, Coinductively

Adrienne Lancelot

Inria & LIX, École Polytechnique, UMR 7161, Palaiseau, France

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

## Abstract

Intersection type systems, as adequate models of the λ-calculus, induce an equational theory on terms, that we refer to as type equivalence. We give a new proof technique to coinductively characterize type equivalence. To do so, we explore a simple setting, namely weak head type equivalence, which is the equational theory induced by a weak head non-idempotent intersection type system.

We prove a folklore result: weak head type equivalence coincides with Sangiorgi's normal form bisimilarity. What is new in our development is that we only rely on coinductive program equivalences, bypassing the need to introduce term approximants, which were used in previous works characterizing type equivalence.

The crucial part of this characterization is to show that type equivalent terms are normal form bisimilar: we do so by constructing *shape typings* that can only type terms of a specific normal form structure. Shape typings are a light form of principal types, a technique often used in intersection types to generate from one or few principal typing all possible typings of a term.

**2012 ACM Subject Classification** Theory of computation → Lambda calculus

**Keywords and phrases** lambda calculus, intersection types, program equivalence

**Digital Object Identifier** 10.4230/LIPIcs.TYPES.2024.4

**Acknowledgements** I am grateful to the reviewers for their careful read of the paper and helpful comments and to Beniamino Accattoli for providing me feedback on a first draft.

## 1 Introduction

Intersection types were developed to study the theory of programming languages and are at the intersection between operational and denotational techniques. While only a certain subset of terminating programs are typable in a simple type system, all terminating programs are typable in an *intersection* type system. As they can give a meaning to all terminating terms, intersection type systems may give syntactic presentations of denotational models [21, 12].

Non-idempotent intersection types, here referred to as *multi types*, have been especially successful syntactic presentations of the relational model, both in Head Call-by-Name (CbN) [14] and Call-by-Value (CbV) [17]. In this work we focus on another variant, namely *Weak Head Call-by-Name* (further restricting head reduction to forbid reduction under lambdas).

In this work, we will syntactically characterize the equational theory induced on terms by multi type systems. Such a characterization is already known for CbN: Böhm tree equivalence exactly represents the equational theory induced by the CbN idempotent intersection type system [22] and by the CbN non-idempotent variant [13]. Both developments introduce term approximants to carefully define the syntactic program equivalence that will match the equational theory induced by the type system. Terms approximants are a powerful but heavy tool in the study of program equivalences; in particular, they require to extend the calculus to a calculus of approximants. The aim of this paper is to show that approximants can be avoided and replaced by a simple use of coinduction, namely normal form bisimulations [23, 19].

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

© Adrienne Lancelot;

licensed under Creative Commons License CC-BY 4.0

30th International Conference on Types for Proofs and Programs (TYPES 2024).

Editors: Rasmus Ejlers Møgelberg and Benno van den Berg; Article No. 4; pp. 4:1–4:18

Leibniz International Proceedings in Informatics

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

LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 4:2 Separating Terms by Means of Multi Types, Coinductively

**Syntactic Equality and Normal Form Bisimilarities.** Denotational models give rise to mathematical interpretations of the λ-calculus, where different λ-terms may be sent to the same mathematical object. Equivalence classes of λ-terms in these models should always include syntactical equality–that only equates programs that have exactly the same syntax (up to α-equivalence)–and β-equivalence. Indeed, $I := \lambda x.x$ and $II$ have different syntax but represent the same identity function. The computational theory $\lambda\beta$, that only quotients by β-equivalence, is still far from reaching most denotational models’ theories. Indeed, some terms are not β-equivalent but have the same behavior–the paradigmatic example being fixpoint combinators. To be able to relate those terms, one needs to define syntactical theories based on infinite trees, namely normal form bisimilarities.

Normal form bisimilarity is an intensional equivalence, that compares the structure of the terms' (possibly infinite) normal forms. The normal form bisimilarity of interest here is Sangiorgi's normal form bisimilarity, denoted $\simeq_{\text{wh}}$. It is obtained from the study of bisimulations in the $\pi$-calculus and the translation of the $\lambda$-calculus into the $\pi$-calculus [23]. Later, Lassen related this bisimilarity, there called weak head normal form bisimilarity, to Lévy-Longo tree equivalence [19].

**Weak Head Multi Types.** Adequate intersection types for weak head call-by-name evaluation were first introduced in an idempotent setting by Dezani-Ciancaglini et al. [16] and then refined by Bucciarelli et al. [15] in a non-idempotent setting, allowing for quantitative information and lighter proofs. We shall use the latter presentation, via multi types defined later in Section 3. The quantitative aspect will play a crucial role, as explained in Section 5.

**Type Equivalence.** Given an intersection type system, one can define what we call here *type equivalence* $\simeq_{\text{type}}$, which is the equational theory induced by the model syntactically represented by the type system. Two terms are type equivalent if they are typable by exactly the same pairs of typing contexts and types. While it is easier to prove type equivalence than contextual equivalence on certain pairs of terms, it is still quantified universally and, unlike normal form bisimilarities, does not provide a straightforward proof technique. Type equivalence is included in contextual equivalence, but this inclusion is in general strict.

In the case of weak head multi types, type equivalence $\simeq_{\text{type}}$ does not validate well-known examples of equations validated by contextual equivalence $\simeq_{\text{ctx}}$ (that are also examples of incompleteness for Sangiorgi's normal form bisimilarity): for instance, $x\lambda y(xy \simeq_{\text{ctx}} xx)$ but $x\lambda y(xy \not\simeq_{\text{type}} xx)$ (and $x\lambda y(xy \not\simeq_{\text{wh}} xx)$ [1, 23].

**This Paper: Coinductively Characterizing Type Equivalence.** Our main result is that type equivalence induced by the weak head multi type system coincides with Sangiorgi's normal form bisimilarity. This characterization may be folklore for experts of the topic but we provide here a clean development of the coinductive proof technique.

There are various related works on characterizing syntactically the equational theory of a model. To the best of our knowledge, characterizations regarding intersection types all mention term approximants. Approximants are an inductive way to look at infinitary behaviors and were the core of the original definition of Böhm trees. Coinduction is a more modern way to define infinitary computation and it is particularly successful in defining (Böhm) tree equivalence as normal form bisimilarity. By avoiding approximants, we do not need to complexify theorem statements to include approximants (on top of terms). The proof technique is more easily breakable into sub-lemmas, as it rests on a coinductive argument.
We split the characterization proof in two directions:

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

Typing transfer shows that normal form bisimilar terms are typable by the same pairs of typing contexts and types (in fact, sometimes even using the same type derivations). This first direction is the easy one, done by induction, exploiting quantitative arguments of multi types. The other direction uses coinduction and is shown by building shape typings, which explicitly specify that type equivalent terms have matching normal forms. Shape typings are reminiscent of principal types, and share some of their properties. They are however lighter and principal types for intersection/multi types are a quite technical topic beyond the scope of this paper.

Going back to finitary normal forms, we give an intersection type variant of Böhm theorem: for any two distinct $\beta$-normal forms, there exists a typing context and a type that may only type one of the normal forms and not the other (in the weak head intersection type system).

**Monotonicity of Normal Form Bisimilarity, for free.** Once Sangiorgi's normal form bisimilarity is proven equivalent to type equivalence, we can deduce the monotonicity of Sangiorgi's normal form bisimilarity without much work. A relation is monotone if it is stable by context closure. Such a property is not trivial for intensional equivalences like Böhm tree equivalence or normal form bisimilarity, as they are not defined compositionally. On the other hand, proving monotonicity for type equivalence is an immediate induction on derivations, as derivations are built compositionally.

While there exists some techniques to show that normal form bisimilarities are monotone, they do not scale up so easily. Lassen's adaptation of Howe's method for normal form bisimilarity [19] is a tedious but efficient process for Böhm tree equivalence and Sangiorgi's normal form bisimilarity. It does not scale up to extensional call-by-value bisimilarities, where Biernacki et al. need to introduce an extension of the proof method [11]. These limits justify looking for alternative proof techniques of monotonicity.

**On Related Separation Constructions.** The crucial part of the proof relies in the separation construction, where it is shown that type equivalent terms are normal form bisimilar. Our construction of shape typings is not so different than the separation described in the book of Barendregt and Manzonetto [10], which is exactly the proof from Breuvart et al. [13].

Separation theorems are not a new concept, see Barendregt's book about the $\lambda$-calculus [9] for an overview. These techniques are also reminiscent of the well-known Böhm out technique [9], where from two terms that are not normal form bisimilar, one builds a context separating them for contextual equivalence. However these techniques are usually presented via contrapositive: from a difference in Böhm trees, one can extract a context/type that can separate them. In our case, we do not explicitly go by contrapositive but specify principal types, closer to Ronchi Della Rocca's development [22] where principal types are carefully defined and used.

**A Single Ground Type is Enough.** We delve into a more technical aspect of multi types. Intersection types for call-by-name evaluation, whether it is head or weak head, require ground types, that are atom types for variables of a term. In general, it is sufficient to have only one ground type, as properties of multi types are still preserved, hence we sometimes only
4:4 Separating Terms by Means of Multi Types, Coinductively

use one ground type for simplicity [4]. To characterize type equivalence, however, Breuvart
et al. deliberately use infinitely many ground types to ease the separation of terms [13]. We
follow at first their simplification and clearly outline where these ground types are needed.
We are then able to give an alternative construction that only requires a single ground type.

2 Weak Head Reduction

We briefly survey the definition of weak head reduction and its associated contextual
equivalence.

**Weak Head Reduction.** We focus on a specific reduction of the λ-calculus, weak head reduction, the variant of head reduction that does not reduce under lambdas.

$$
\text{TERMS} \quad \Lambda \ni t, u, s \quad ::= \quad x \mid \lambda x.t \mid tu
$$

$$
\text{WEAK HEAD CTXS} \quad E ::= \langle \cdot \rangle \mid Et
$$

Weak head reduction, denoted →<sub>wh</sub>, is the closure of the beta rule (λx.t)u ↦→<sub>β</sub> t{x↔u} under applicative weak head contexts. In essence, all →<sub>wh</sub> steps are of the shape (λx.t)u s<sub>1</sub> ... s<sub>k</sub> →<sub>wh</sub> t{x↔u} s<sub>1</sub> ... s<sub>k</sub> for k ≥ 0.

Normal forms with respect to →<sub>wh</sub> are exactly characterized by the following grammar,
separating normal forms into rigid terms and abstractions:

$$
\text{RIGID TERMS} \quad r, r' ::= x \mid rt
$$

$$
\text{WEAK HEAD NORMAL FORMS} \quad w, w' ::= \lambda x.t \mid r
$$

We say that a term is →<sub>wh</sub>-normalizing if it reduces to a →<sub>wh</sub>-normal form. Note that by well-known normalization theorems for weak head reduction, the fact that a term β-reduces to a →<sub>wh</sub>-normal form is equivalent to →<sub>wh</sub>-reducing to a →<sub>wh</sub>-normal form. We define the contextual preorder and equivalence based on weak head termination.

► **Definition 1 (Contextual Preorder and Equivalence).** The weak head contextual preorder ≲<sub>ctx</sub> and contextual equivalence ≃<sub>ctx</sub> are defined as follows:

- t ≲<sub>ctx</sub> t' if, for all context C such that C(t) and C(t') are closed terms, whenever C(t) is
  →<sub>wh</sub>-normalizing, so is C(t').

- t ≃<sub>ctx</sub> t' is the equivalence relation induced by ≲<sub>C</sub>, that is, t ≃<sub>ctx</sub> t' ⇐⇒ t ≲<sub>ctx</sub> t' and t' ≲<sub>ctx</sub> t.

Contrarily to the usual call-by-name contextual equivalence (based on head termination), Ω and λx.Ω are not contextually equivalent. Indeed, in the empty context, the former does not terminate whereas the latter is in weak head normal form.

**On Contextual Equivalence and η-equivalence.** As a consequence, the η rule does not hold in general: Ω and λx.Ωx are not contextually equivalent (for Ω := (λx.xx)(λx.xx), the paradigmatic looping term). In fact, if one is interested in the weak head contextual preorder, λx.xx refines *t* but *t* does not always refine λx.xx (*t* ≲<sub>ctx</sub> λx.xx for all *t* but λx.yx ≲<sub>ctx</sub> *y* for all variables *y*). If *t* converges to an abstraction, there is no difference between both terms, as this η-equivalence is actually included in β equivalence. Otherwise, it is in fact not true that *t* refines λx.xx as *t* can be non terminating whereas λx.xx is *always* a weak head normal form.

Issues with η-equivalence and weak head reduction actually go beyond this first observation.
There exists η-equivalent terms that are contextually equivalent, the paradigmatic example
being xλy.xy ≃<sub>ctx</sub> xx [1, 23]. These two terms are contextually equivalent even though λy.xy
and x are not. Contextual *inequivalence* is somehow non-compositional in presence of η.
<figure><img src="image_5.png" /><figcaption>Figure 1 WH Multi Type System.</figcaption></figure>

## 3 Weak Head Multi Types WH

We follow the definitions of multi types for weak head reduction as designed by Bucciarelli et al. [15], recalled in Fig. 1.

**Multi Types.** Multi types $M$ are finite multisets of linear types $L$ that are either base types $\star_k$ or arrow types $M \to L$. In the original presentation of Bucciarelli et al. [15], there are distinct ground types and an abstraction type $\sharp$: we unify both for simplicity. Note that there is a countable number of distinct base types, following Breuvart et al. [13], to simplify separating terms by types.

Typing contexts $\Gamma$ are finite-support maps from variables to multi types, denoted $x_1: M_1, \dots, x_k:M_k$. Any omitted variable is implicitly typed by the empty type $[]$. The empty typing context, where all variables are typed by the empty type, is denoted $\emptyset$.

**Typing Rules.** The typing rules described in 1 are the rules to infer the type of a term.

There are two axiom rules, one for variables (ax) and one for abstractions ($\lambda_k$). The latter is specific to weak head call-by-name, by allowing to type all abstractions.

There is another rule to type abstractions ($\lambda$) whose only premise gives a type for the body of the abstraction, given a multi type for the binded variable, that now moves to the typing context.

The application rule ($@$) is the only way to type terms of the form $tu$. Intuitively, this rule requires the argument $u$ to be typed for every occurrence that will be used in typing the function $t$. The premices of the rule indeed require to type $t$ with a linear type $[L_1, \dots, L_k] \to L$ and $u$ with many linear types $L_1, \dots, L_k$, giving a different type derivation for each of the linear types in the argument position of the type of $t$. In particular, if $t$ is typed with the linear type $[] \to L$, then one does not have to provide any type derivation for $u$ to apply the @-rule.

**► Definition 2 (Typing).** A typing of a term $t$ is a pair $(\Gamma, L)$ of a typing context $\Gamma$ and a linear type $L$ such that there exists a derivation $\pi$ with final judgment $\Gamma \vdash t: L$.

We write $\pi \triangleright \Gamma \vdash t: L$ if $\pi$ is a type derivation with final judgment $\Gamma \vdash t: L$.

**Results about Multi Types.** Intersection types are in particular known for the fact that typability may exactly capture normalizable terms. This system is an example of such characterization, as a term is typable in $WH$ if and only if it is weak head normalizable.

**► Theorem 3 (Characterization of Termination, [15]).** A term $t$ is typable in $WH$ if and only if $t \to_{wh} n$ where $n$ is a weak head normal form.
4:6 Separating Terms by Means of Multi Types, Coinductively

Proving characterization of termination for idempotent intersection types is generally
obtained by reducibility arguments, but this proof technique can be avoided by switching
to multi types–where characterization of termination can be shown with combinatorial
arguments. The main selling point of multi types, the non-idempotent variant of intersection
types, is indeed to obtain quantitative results from typing judgments. The most famous
example is the following statement of quantitative subject reduction, that allows to show that
any type of a term is stable by reduction, and the derivation of the reduct shall be of a
strictly smaller size. The size of a derivation |π| is its total number of rules.

► **Proposition 4** (Quantitative Subject Reduction, [15]). For all $(\pi, \Gamma, L, t, t')$ such that $\pi \triangleright \Gamma \vdash t:L$ and $t \to_{wh} t'$, there exists $\pi' \triangleright \Gamma \vdash t':L$ with $|\pi'| < |\pi|$.

From quantitative subject reduction, it is typical to deduce (without reducibility argu-
ments!) that the intersection type system is correct, i.e. all typable terms are normalizing.
For the converse implication to hold, thus completing the characterization of termination,
one can easily deduce it from subject expansion. Note that the following statement of subject
expansion contains quantitative information about the size of derivations but the quantitative
argument plays no role in proving that all normalizing terms are typable (the induction is
done on the number of steps to normalization).

► **Proposition 5** (Quantitative Subject Expansion, [15]). For all $(\pi, \Gamma, L, t, t')$ such that $\pi \triangleright \Gamma \vdash t':L$ and $t \to_{wh} t'$, there exists $\pi' \triangleright \Gamma \vdash t:L$ with $|\pi'| > |\pi|$.

Quantitative arguments are also sometimes taken a step further, introducing alternative type systems that exactly measure the length of the reduction sequence to normal forms, see Accattoli et al. [3].

**The Equational Theory Induced by the Multi Type System.** In this work, we focus on the program equivalence induced by the multi type system of Fig. 1. Indeed, multi type systems induce a model, that we shall not discuss here, and every model induces an equivalence relation on terms (by relating terms with the same interpretation in the model). We introduce the type preorder, that exactly rephrases the (in)equational theory induced by the weak head multi type system.

► **Definition 6** (*Type Preorder*). The type preorder $\preceq_{type}$ and type equivalence $\simeq_{type}$ are relations on terms defined as follows:

■ $t \preceq_{type} t'$ if for all $\Gamma, L$ such that there exists $\pi \triangleright \Gamma \vdash t:L$ then there exists $\pi' \triangleright \Gamma \vdash t':L$.

■ Type equivalence is defined by symmetry: $t \simeq_{type} t'$ iff $t \preceq_{type} t'$ and $t' \preceq_{type} t$.

It is easy to check that $\preceq_{type}$ is indeed a preorder (reflexive and transitive). Furthermore
by subject reduction and subject expansion it is invariant by $\to_{wh}$ and *adequate*. As it is also
stable by contexts, the type preorder satisfies the usual definition of an (in)equational theory
[9, 10].

We say that $t'$ (type-)improves $t$ if $t \preceq_{type} t'$, that is if all typings of $t$ are typings of $t'$.
Symmetrically, two terms are type equivalent if that they have the same set of typings.

► **Proposition 7.** The type preorder enjoys the following properties:

1. wh-invariance: if $t \to_{wh} t'$ then $t \preceq_{type} t'$ and $t' \preceq_{type} t$;

2. Adequacy: if $t \preceq_{type} t'$ and $t$ is $\to_{wh}$-normalizing then $t'$ is $\to_{wh}$-normalizing;

3. Monotonicity: if $t \preceq_{type} t'$ then $C\langle t \rangle \preceq_{type} C\langle t' \rangle$ for any context $C$.

As a direct corollary of Point 2 and 3 of Proposition 7, the type preorder is included in
the contextual preorder.

► **Corollary 8.** The type preorder is included in the contextual preorder, i.e. $\preceq_{type} \subseteq \preceq_{ctx}$.
*Similarly for equivalences:* $\simeq_{type} \subseteq \simeq_{ctx}$.
# 4 Weak Head Normal Form Bisimilarity

In this section, we recall the definition of Sangiorgi's normal form (bi)similarity and show the correspondence with the type preorder.

First, from a relation $\mathcal{R}$ on terms we define its closure on $\to_{\text{wh}}$-normal forms $\langle\mathcal{R}\rangle_{\text{nf}}$. Formally, $\langle\mathcal{R}\rangle_{\text{nf}}$ is defined, by induction, as the smallest relation including the three following rules:

$$ \frac{x \langle\mathcal{R}\rangle_{\text{nf}} x}{\mathcal{R}} \qquad \frac{r \langle\mathcal{R}\rangle_{\text{nf}} r' \quad t \mathcal{R} u}{rt \langle\mathcal{R}\rangle_{\text{nf}} r' u} \qquad \frac{t \mathcal{R} u}{\lambda x.t \langle\mathcal{R}\rangle_{\text{nf}} \lambda x.u} $$

**► Definition 9 (Weak head normal form simulation).** A relation on terms $\mathcal{R}$ is a weak head normal form (whnf) simulation if for all $t, t'$ such that $t \mathcal{R} t'$ either $t$ does not $\to_{\text{wh}}$-terminate, or $t \to_{\text{wh}}$-reduces to a normal form $w$ and $t' \to_{\text{wh}}$-reduces to a normal form $w'$ such that $w \langle\mathcal{R}\rangle_{\text{nf}} w'$.

Whnf similarity, noted $\lesssim_{\text{wh}}$, is defined, by coinduction, as the largest whnf simulation.

Note that the definition here is slightly different than Sangiorgi's and Lassen's well-known presentations [23, 19] as we make explicit an inductive definition for rigid terms, via $\langle\mathcal{R}\rangle_{\text{nf}}$.

We define an F-operator, $F: \Lambda \times \Lambda \to \Lambda \times \Lambda$, where $F(\mathcal{R})$ is the whnf simulation induced by $\mathcal{R}$. Formally:

$$ F(\mathcal{R}) := \left\{ (t, t') \mid \begin{array}{l} \text{either } t \text{ does not } \to_{\text{wh}}\text{-terminate,} \\ \text{or } t \to_{\text{wh}}\text{-reduces to a normal form } w \text{ and} \\ \qquad t' \to_{\text{wh}}\text{-reduces to a normal form } w' \text{ such that } w \langle\mathcal{R}\rangle_{\text{nf}} w' \end{array} \right\} $$

We have that $\mathcal{R}$ is a whnf simulation iff $\mathcal{R} \subseteq F(\mathcal{R})$. To ensure that whnf similarity can be coinductively defined, we prove that the F-operator is monotone.

**► Proposition 10 (Monotonicity of whnf simulations).** If $\mathcal{R} \subseteq \mathcal{R}'$ then $F(\mathcal{R}) \subseteq F(\mathcal{R}')$

**Proof.** Let $(t, t') \in F(\mathcal{R})$. We have two cases:

- If $t$ does not $\to_{\text{wh}}$-terminate, then $(t, t') \in F(\mathcal{R})$.

- Otherwise, $t \to_{\text{wh}}$-reduces to a normal form $w$ and $t' \to_{\text{wh}}$-reduces to a normal form $w'$ such that $w \langle\mathcal{R}\rangle_{\text{nf}} w'$. As $\mathcal{R} \subseteq \mathcal{R}'$, we have that $w \langle\mathcal{R}'\rangle_{\text{nf}} w'$ (by an easy induction on $\langle\cdot\rangle_{\text{nf}}$). We conclude that $(t, t') \in F(\mathcal{R}')$ by definition. ◀

**Type equivalence exactly matches normal form bisimilarity.** In the two following sections, we will exactly characterize the type preorder by whnf similarity, i.e. $\lesssim_{\text{wh}}=\lesssim_{\text{type}}$. We call soundness $\lesssim_{\text{wh}}\subseteq\lesssim_{\text{type}}$, the easy part, and completeness $\lesssim_{\text{wh}}\supseteq\lesssim_{\text{type}}$, the difficult part.

**Monotonicity, for free.** An interesting corollary of this characterization is an alternative of monotonicity for whnf similarity (i.e. that $\lesssim_{\text{wh}}$ is stable by contexts). Such a property is often also called compatibility and is the main technical point when showing soundness of a similarity with respect to contextual equivalence. The proof of such a property is not always complex, as there is a general method described by Lassen, but can be quite lengthy. Note that in some cases, Lassen's method does not directly apply and requires adjustments [11], thus motivating the need for alternative and lighter proof techniques.

**► Proposition 11 (Monotonicity of $\lesssim_{\text{wh}}$).** If $t \lesssim_{\text{wh}} u$ then for all $C$, $C\langle t \rangle \lesssim_{\text{wh}} C\langle u \rangle$.

The proof follows from the exact characterization of $\lesssim_{\text{wh}}$ by $\lesssim_{\text{type}}$ (Theorem 26) and the fact that the latter enjoys monotonicity (Point 3 of Proposition 7).
## 5 Soundness via Typing Transfer

We shall first show soundness and we do so via the following *typing transfer* proposition. It says that if two terms are whnf similar, then any typing of *t* transfers to *t'* (note that if *t* and *t'* are normal forms, even part of the structure of the derivation transfers). We show such a result via induction on the size of the derivation. A crucial ingredient is that subject reduction does not increase the size of the derivation, otherwise the induction argument would not work. The quantitative aspect of the subject reduction proof is therefore crucial and justifies the need of *multi types*.

**Proposition 12 (Typing Transfer).** Let $\mathcal{R}$ be a whnf simulation. If $t \in \mathcal{R}$ and there exists a derivation $\pi \vdash \Gamma \vdash t: L$ then there exists a derivation $\pi' \vdash \Gamma \vdash t': L$.

*Proof.* By induction on the size of the derivation $\pi \vdash \Gamma \vdash t: L$.

The term $t$ is typable by the derivation $\pi \vdash \Gamma \vdash t: L$ therefore it is normalizable by Theorem 3. Hence we have $t \to_{wh}^k w$ and therefore (since $\mathcal{R}$ is a bisimulation) $t' \to_{wh}^* w'$ with $w \langle \mathcal{R} \rangle_{nf} w'$ with $w$ and $w'$ weak head normal forms. By quantitative subject reduction (Proposition 4), there is a derivation $\pi_1 \vdash \Gamma \vdash w: M$ whose size is at most the size of $\pi$. Instead of looking for a derivation $\pi'$ of $t'$, we can look for a derivation $\pi'_1$ of $w'$ and conclude by (qualitative) subject expansion for wh-reduction (Proposition 5).

Now, from $w \langle \mathcal{R} \rangle_{nf} w'$ and $\pi_1 \vdash \Gamma \vdash w: L$, we build the derivation $\pi'_1 \vdash \Gamma \vdash w': L$. By case analysis on the last rule of the derivation $\pi_1$:

1. Axiom rule.

$$ \pi_1: \frac{x: [L] \vdash w = x: L}{x} \quad \mathbf{ax} $$

Then by $w = x \langle \mathcal{R} \rangle_{nf} w'$, $w' = x$ and $\pi'_1 := \pi_1$ types $w'$ accordingly.

2. Abstraction-★ rule.

$$ \pi_1: \frac{\vdash w = \lambda x.t: \star_i}{\lambda} $$

Then by $w = \lambda x.t \langle \mathcal{R} \rangle_{nf} w'$, $w' = \lambda x.u$ and $\pi'_1 := \pi_1$ types $w'$ accordingly.

3. Abstraction rule.

$$ \pi_1: \frac{\Gamma, x: M \vdash u: L'}{\Gamma \vdash w = \lambda x.u: L = M \dashv L'} \quad \lambda $$

Then by $w = \lambda x.u \langle \mathcal{R} \rangle_{nf} w'$, $w' = \lambda x.u'$ with $u \in \mathcal{R}$ and $u'$.

The derivation $\pi_2 \vdash \Gamma, x: M \vdash u: L'$ is of a strictly smaller size than $\pi$. By induction, since $u \in \mathcal{R}$ and $u'$, there is a derivation $\pi'_2 \vdash \Gamma, x: M \vdash u': L'$.

We build the derivation $\pi'_1$ by applying the $\lambda$ typing rule to $\pi'_2$.

4. Application rule.

$$ \pi_1: \frac{\Gamma \vdash r: [L_i]_{i \in I} \dashv L \quad (\Delta_i \vdash t: L_i)_{i \in I}}{\Gamma \vdash (\bigcirc_{i \in I} \Delta_i) \vdash w = rt: L} @ $$

Then by $w = rt \langle \mathcal{R} \rangle_{nf} w'$, $w' = r'u$ with $r \in \mathcal{R}$ and $r' \in \mathcal{R}$ such that $r \prec \mathcal{R} u$. By induction on the sub-derivations, we get the appropriate derivation for $w'$. $\quad \blacksquare$

From the fact that typings transfer for any whnf simulation, we deduce easily soundness ($\prec_{wh} \subseteq \prec_{type}$) as typings transfer, in particular, for the largest whnf simulation that is whnf similarity.

**Theorem 13.** For all terms $t, u$, if $t \prec_{wh} u$ then $t \prec_{type} u$.

*Proof.* Let $t, u$ terms such that $t \prec_{wh} u$. Let $\Gamma \vdash t: L$ a typing for $t$. As $\prec_{wh}$ is a whnf bisimulation, by Proposition 12, we have that $\Gamma \vdash u: L$. Hence $t \prec_{type} u$. $\quad \blacksquare$
# 6 Completeness via Shape Typings

It remains now to show that if two terms are typable by the same intersection types, then they have to be syntactically similar, specifically that they have to be weak head normal form bisimilar.

**Coinductive Argument.** To prove completeness, i.e. that $\leq_{type} \subseteq \leq_{wh}$, we shall use coin-
duction. We first show that $\leq_{type}$ is a whnf simulation, which implies it is included in the
largest whnf simulation, namely whnf similarity $\leq_{wh}$.

**Building Shape Typings, Principally.** To prove that the type preorder is a whnf simulation, we build specific *shape typings* that specify the shape of the normal form of a term. As an example, there exists $\Gamma_x, L_x$ that ensure that for any term $t$ typable by this typing, i.e. $\Gamma_x \vdash t: L_x$, we have that $t$ weak head normalizes to $x$. In this specific case, $\Gamma_x := x: [\star_0]$ and $L_x := \star_0$.

These shape typings specify the structure of normal form of any term they type. We choose them with some flexibility in mind so that they may be used compositionally. In that sense, they are *principal typings* in that they generate a number of other possible typings for terms that they may type. Indeed, another choice for $\Gamma_x, L_x$ could be to replace $\star_0$ by any linear type. As an example, $\Gamma_x := x: [[\star_0] \to \star_1]$ and $L_x := [\star_0] \to \star_1$ is also a correct typing for $x$ but it is not separating, since it also types $\lambda y.x.y$.

A first definition of shape typings can be seen with the following (*sub-*type system (only typing weak head normal forms):

$$ \underline{x: [\star_k] \vdash_{\text{shape}} x: \star_k} \quad \text{shape-ax} $$

$$ \frac{\Gamma \vdash_{\text{shape}} r: \star_k \quad \star_k \text{ appears only once in } \Gamma}{\Gamma \{\star_k \leftarrow [] \to \star_{k'}\} \vdash_{\text{shape}} rt: \star_{k'}} \quad \text{shape-@} $$

$$ \emptyset \vdash_{\text{shape}} \lambda x.t: \star_k \quad \text{shape-}\lambda_k $$

where $\Gamma\{\star_k \leftarrow L\}$ denotes the substitution of a type variable (ground type) by a linear type $L$.

Dry typing systems follow similar definitions (see [2] where dry typings are defined in a more complex setting than weak head reduction). Coming up with these first shape typings resembles finding a typing only inhabited by one or few terms (up to $\beta$-conversion). Arrial's implementation of the inhabitation algorithm [7] was helpful to check ideas of shape typings (algorithm developed and proven correct in [8]).

This system is an *outer shape typing system* in the following sense:

1. Any normal form can be typed in the $\vdash_{\text{shape}}$ system;

2. The $\vdash_{\text{shape}}$ system is sound for the weak head multi type system $\vdash : \text{ if } \Gamma \vdash_{\text{shape}} t: L$ then } \Gamma \vdash t: L$;

3. These shape typings allow us to distinguish terms with different outer shape normal forms.

Point 1 is immediate given the definition of $\vdash_{\text{shape}}$. Point 2—which is the fact that this transformation is sound with respect to the original weak head type system—is formalized with Lemma 16 (note that the lemma is more general, somehow allowing to substitute a linear type for another one). Point 3 is the starting point of our separation construction, formally specified in Proposition 17.
4:10 Separating Terms by Means of Multi Types, Coinductively

Proposition 17 (and the shape typing system $\vdash_{\text{shape}}$) is not enough to complete the proof that type equivalent terms generate the same (infinitary) Lévy-Longo tree (i.e. are normal form bisimilar), as some terms have the same outer shape but differ on a deeper syntax level (a difference between $t$ and $t'$ generates a difference between $\lambda x.t$ and $\lambda x.t'$, and between $xt$ and $xt'$). We therefore need to generalize our shape typing technique to be able to detect deep differences (formally proven in the so-called Normal Inversion Lemma 21).

In a nutshell, the proof technique of this section will be decomposed in two steps:

1. Look for a possible outer difference with $\vdash_{\text{shape}}$;

2. If the outer syntax matches, go deeper with the inversion lemma.

We'll (coinductively) repeat the process to show that, if $t$ type-improves $t'$ then $t$ is whnf similar to $t'$.

**Building Shape Typings, Formally.** Now, we formally prove completeness, by exhibiting our shape typings. We first specify a family of types, erasing types, that will be helpful to discriminate between terms and act as shape types for rigid normal forms.

**► Definition 14 (Erasing Type).** The $(k, i)$ erasing type, written $E_i^k$, represents a computation that erases $k$ arguments and returns the $i$th ground type. Precisely, $E_i^k := ([ ] \to^k \star_i)$.

Erasing types can be used to type any rigid term $x t_1 \cdots t_k$, by assigning a $(k, i)$ erasing type $([ ] \to^k \star_i$ to the head variable $x$, resulting in the rigid term to be typed with the $(0, i)$ erasing type $\star_i$ ($k$ is the number of arguments applied to the head variable).

To formally prove this, with the following lemma, we strengthen the inductive hypothesis by showing that assigning a $(n, i)$ erasing type to the head variable $x$ results in the rigid term to be typed with the $(n - k, i)$ erasing type.

**► Lemma 15 (Shape Typings for Rigid Terms).** Let $r$ be a rigid term of head variable $x$ and such that the head variable is applied to $k$ arguments. Then, for all $n \ge 0$ and $i$, $x: [E_i^{k+n}] \vdash r: E_i^n$.

In particular, for any $i$, $x: [E_i^k] \vdash r: \star_i$ is an (outer) shape typing for the rigid term $r$.<fnref n="1" />

**Proof.** By induction on rigid terms(/the number $k$).

- Variable i.e. $r = x$. Then the head variable of $r$ is $x$ and it is applied to 0 arguments. We conclude as $x: [E_i^n] \vdash x: E_i^n$ is a correct derivation for all $n$ consisting only of the axiom rule.

- Application i.e. $r = r't$. We have that $r'$ has the same head variable as $r$ and that head variable is applied to $k - 1$ arguments in $r'$. Let $n$ be a natural number.

By induction, $x: [E_i^{k+n}] \vdash r': E_i^{n+1}$. We conclude by building the following derivation:

$$ \frac{x: [E_i^{k+n}] \vdash r': E_i^{n+1}}{x: [E_i^{k+n}] \vdash r't: E_i^n} \text{ @} $$

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

The second property we shall use about shape typings is the following: all typings of rigid terms can be seen as extensions of shape typings, as there exists (1) a type for the head variable, (2) which determines the type of the rigid term.

<footnote n="1">¹ Note that this is the same shape typing as the one provided in the shape type system $\vdash_{\text{shape}}$, but written in a direct way.</footnote>
**► Lemma 16 (Typings of Rigid Terms follow Shape Typings).** Let $r$ be a rigid term with head variable $x$ and such that the head variable is applied to $k$ arguments.

For any typing $\Gamma \vdash r : L$, there exist $k$ multi types $(M_i)_{1 \le i \le k}$ such that:

1. $[M_1 \to \dots \to M_k \to L] \subseteq \Gamma(x)$;

2. For any linear type $L'$, we have a new typing $\Gamma' \uplus x : [M_1 \to \dots \to M_k \to L'] \vdash r : L'$, with $\Gamma' := \Gamma \setminus (x : [M_1 \to \dots \to M_k \to L])^2$.

**Proof.** By induction on $r$.

- Variable i.e. $r = x$. The last rule of any derivation must be the axiom rule, which ensures that $\Gamma(x) = [L]$. For the second point, it suffices to see that $x : [L'] \vdash x : L'$ is valid for any $L'$.

- Application i.e. $r = r't$. The last rule of any derivation must be the application rule.

$$ \frac{\Delta \vdash r' : [L_i]_{i \in I} \to L \quad (\Pi_i \vdash t : L_i)_{i \in I} \quad @}{\Gamma = \Delta \uplus \Pi_{i \in I} \vdash r : L} $$

By induction there exists $k-1$ multi types $(M_i)_{1 \le i \le k}$ such that $[M_1 \to \dots M_{k-1} \to ([L_i]_{i \in I} \to L)] \subseteq \Delta(x)$. Set $M_k := [L_i]_{i \in I}$ then $[M_1 \to \dots M_k \to L)] \subseteq \Gamma(x)$ as $\Delta \subseteq \Gamma$. For the second point, by induction, for all linear type $L'$, we have that $x : [M_1 \to \dots M_{k-1} \to ([L_i]_{i \in I} \to L')] \vdash \Delta' \vdash r : ([L_i]_{i \in I} \to L')$, hence we conclude by applying the application rule. ◀

A first step towards showing that the type preorder is a whnf simulation is to show that the structure of the normal forms are preserved (the outermost syntax), which is specified in the following proposition. In the proof, we use shape typings for rigid terms, as well as a shape typing for abstractions $(\emptyset, \star_0)$.

**► Proposition 17 (Type preorder preserves the shape of normal forms).** Let $w$ be a weak normal form, $t$ a term, and $r$ a rigid term.

1. Variable Preservation: if $x \preceq_{\text{type}} w$, then $w = x$.

2. Abstraction Preservation: if $\lambda x.t \preceq_{\text{type}} w$, then $w = \lambda x.u$ for some term $u$.

3. Rigid Preservation: if $rt \preceq_{\text{type}} w$, then $w = r'u$ for some rigid $r'$ and some term $u$.

**Proof.**

1. Suppose $w \neq x$. Cases of $w$:

- Different Variable: if $w = y$, then $x : [\star_0] \vdash x : \star_0$, but $y$ is not typable by $(x : [\star_0], \star_0)$.

- Abstraction: if $w = \lambda y.u$, then $x : [\star_0] \vdash x : \star_0$, but $\lambda y.u$ is not typable by $(x : [\star_0], \star_0)$, since typing by $\star_0$ requires an empty context for abstractions.

- Rigid Term: if $w = r'u$, then $x : [\star_0] \vdash x : \star_0$, but $x : [\star_0] \vdash r'u : \star_0$, as a non variable rigid term needs an arrow type in the context for its head variable (per Lemma 16).

2. We know that $\emptyset \vdash \lambda x.t : \star_0$ however $\emptyset \vdash r : \star_0$ for all rigid term $r$ (at least one variable has to appear with a non-empty type in the context by Lemma 16). Thus, $w$ is an abstraction of the form $\lambda x.u$ for some term $u$.

3. There exists a derivation $x : [E_0^k] \vdash rt : \star_0$ where $k \ge 1$ by Lemma 15 but $x : [E_0^k] \not\vdash y : \star_0$ for all $y$ variables and $x : [E_0^k] \vdash \lambda y.s : \star_0$ for all abstraction $\lambda y.s$. Hence $w$ is a non-variable rigid term. ◀

<footnote n="2">² The notation $\Gamma' := \Gamma \setminus \Delta$ means that $\Gamma'$ is such that $\Gamma = \Gamma' \uplus \Delta$. Note that this definition does not constrain the domains of $\Gamma'$ and $\Delta$ to be disjoint.</footnote>
## 4:12 Separating Terms by Means of Multi Types, Coinductively

The main properties of shape typings (Lemma 16) are used to prove the two following lemmas, which shall be key to be able to know the structure of typing derivation.

**Lemma 18.** Let $r$ be a rigid term of head variable $x$ such that $\Gamma \vdash r: L$. If $x: [[ ] \to )^k L] \subseteq \Gamma$ for some $k \ge 0$ and $L$ does not appear in other types in $\Gamma$, then $\Gamma = x: [[ ] \to )^k L]$.

*Proof.* By induction on rigid terms:

- $r = x$. Then the only derivation possible for $r$ is $x: [L] \vdash x: L$, for which the statement holds.

- $r = r't$. Then the derivation $\Gamma \vdash r: L$ must start with a typing rule @:

$$ \frac{\Gamma_0 \vdash r': [L_i]_{i \in I} \to L \quad (\Gamma_i \vdash t': L_i)_{i \in I}}{\Gamma \vdash r: L} $$

with $\Gamma = \Gamma_0 \uplus (\uplus_{i \in I} \Gamma_i)$.

By Lemma 16, $x: [[ ] \to )^k L]$ is included in $\Gamma_0$ (as it is the only occurrence of the $L$ type).

By induction hypothesis, $\Gamma_0 = x: [[ ] \to )^k L]$. Then by Lemma 16, $I$ must be empty (otherwise it would reflect in the type of $x$). Hence $\Gamma = x: [[ ] \to )^k L]$. ◀

**Lemma 19.** Let $r$ be a rigid term of head variable $x$ such that $\Gamma \vdash r: M_i \to \dots \to M_k \to L$ for some $i \le k$. If $x: [N_1 \to \dots \to N_k \to L] \subseteq \Gamma$ for some $k \ge 0$ and $L$ does not appear in other types in $\Gamma$, then $M_j = N_j$ for $i \le j \le k$.

*Proof.* By induction on rigid terms:

- $r = x$. Then the only derivation possible for $r$ is $x: [M_1 \to \dots \to M_k \to L] \vdash x: M_1 \to \dots \to M_k \to L$, for which the statement holds.

- $r = r't$. Then the derivation $\Gamma \vdash r: M_i \to \dots \to M_k \to L$ starts with a typing rule @:

$$ \frac{\Gamma_0 \vdash r': [L_i]_{i \in I} \to M_i \to \dots \to M_k \to L \quad (\Gamma_i \vdash t': L_i)_{i \in I}}{\Gamma \vdash r: M_i \to \dots \to M_k \to L} $$

with $\Gamma = \Gamma_0 \uplus (\uplus_{i \in I} \Gamma_i)$.

By Lemma 16, $x: [N_1 \to \dots \to N_k \to L]$ is included in $\Gamma_0$ (as it is the only occurrence of the $L$ type).

By induction hypothesis, $N_{i-1} = [L_i]_{i \in I}$ and $M_j = N_j$ for $i \le j \le k$, which concludes the proof. ◀

The following proposition is the only point where we use the fact that there are countably many distinct ground types: in all other proofs, we either rely on this proposition or only use the first ground type $\star_0$. This restriction is actually not needed but eases the proof. In fact, it is enough to have only one ground type and be able to specify large enough types. We show after the proof how to choose the right typings if there is only a single ground type.

The proposition states that normal forms related by the type preorder may be broken apart into subterms that are still related by the type preorder. In this sense, the type preorder is *decompositional* on normal forms.

**Proposition 20 (Decompositionality of $\leq_{\text{type}}$).** Let $t, t'$ be terms and $r, r'$ be rigid terms.

1. Left preservation: if $rt \leq_{\text{type}} r't'$ then $r \leq_{\text{type}} r'$.

2. Right preservation: if $rt \leq_{\text{type}} r't'$ and $r \leq_{\text{type}} r'$ then $t \leq_{\text{type}} t'$.
Proof.

1. Let $\Gamma, L$ such that $\Gamma \vdash r: L$. We shall show that $\Gamma \vdash r': L$ as well.

Let $i$ be the maximum index of $\star_i$ that appears in $\Gamma, L$ (if it does not appear, $i=0$).

By Lemma 16, we can set $L' := [ ] \dashv \star_{i+1}$ and $\Delta := \Gamma', x: [M_1 \dashv \dots \dashv M_k \dashv L']$ (where $\Gamma = \Gamma', x: [M_1 \dashv \dots \dashv M_k \dashv L]$) and we still have that $\Delta \vdash r: L'$. It is clear that $(\Delta, \star_{i+1})$ types $rt$:

$$ \frac{\Delta \vdash r: [ ] \dashv \star_{i+1}}{\Delta \vdash rt: \star_{i+1}} $$

By hypothesis, we have that $r't'$ is typable by $(\Delta, \star_{i+1})$. The derivation starts as:

$$ \frac{\Gamma_0 \vdash r': [L_i]_{i \in I} \dashv \star_{i+1} \quad (\Gamma_i \vdash t': L_i)_{i \in I}}{\Delta \vdash r't': \star_{i+1}} $$

By Lemma 16, $x: [M_1 \dashv \dots \dashv M_k \dashv L']$ is included in $\Gamma_0$ (as $L'$ is the only type where $\star_{i+1}$ occurs in $\Gamma$). By Lemma 19 applied on $\Gamma_0 \vdash r': [L_i]_{i \in I} \dashv \star_{i+1}$, we know $[L_i]_{i \in I} = []$. Hence $I$ is empty and $\Gamma_0 = \Delta$.

Hence, we have a derivation of final judgment $\Delta \vdash r': L'$. By Lemma 16 and as $\star_{i+1}$ only appears in one linear type in $\Delta$, we have that $\Gamma \vdash r': L$ as well.

2. Let $\Gamma, L$ such that $\Gamma \vdash t: L$. We shall show that $\Gamma \vdash t': L$.

Let $i$ be the maximum index of $\star_i$ that appears in $\Gamma, L$ (if it does not appear, $i=0$).

Let $\Delta := x: [[ ] \dashv \dots \dashv [L] \dashv \star_{i+1}]$ such that $\Delta \vdash r: [L] \dashv \star_{i+1}$ ($x$ is then the head variable of $r$).

$$ \frac{\Delta \vdash r: [L] \dashv \star_{i+1} \quad \Gamma \vdash t: L}{\Delta \uplus \Gamma \vdash rt: \star_{i+1}} $$

Then, as $r \preceq_{\text{type}} r'$, we also have that $\Delta \vdash r': [L] \dashv \star_{i+1}$.

By hypothesis, we have that $\Delta \uplus \Gamma \vdash r't': \star_{i+1}$. The derivation starts with the application rule:

$$ \frac{\Gamma_0 \vdash r': [L_i]_{i \in I} \dashv \star_{i+1} \quad (\Gamma_i \vdash t': L_i)_{i \in I}}{\Delta \uplus \Gamma \vdash r't': \star_{i+1}} $$

By Lemma 16, $\Delta$ must be included in $\Gamma_0$ (as it is the only occurrence of the $\star_{i+1}$ type). The only derivation of $r'$ containing $\Delta$ in the context must be $\Delta \vdash r': [L_i]_{i \in I} \dashv \star_{i+1}$ by Lemma 18. Hence $I$ only contains one element and $L_1 = L$ (by Lemma 16, as the type $[L_i]_{i \in I} \dashv \star_{i+1}$ must appear in $\Delta$).

Hence, we have a derivation of final judgment $\Gamma \vdash t': L$ which concludes the proof. ◀

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

**A Single Ground Type is Enough.** The proof above uses the fact that there is a countable number of distinct ground types in our multi types-but it is not needed. Alternatively, the key point is to set up a notion of size of linear types by counting the number of top-most arrows in linear types (counting only arrows appearing outside of multi types). We shall use types of size $i$ (that is, with $i$ arrows outside of multi types) as replacement for $i$-th ground types. Then one has to lookup in $\Gamma, L$ the largest linear type ($i :=$ the maximum number of top-most arrows of a type $L'$ that appears in $\Gamma, L-L'$ can appear anywhere, even inside
4:14 Separating Terms by Means of Multi Types, Coinductively

multi types) and set up a strictly larger linear type (that is, with strictly more arrows) as our $\star_{i+1}$. Then the proof follows by using Lemma 16, Lemma 18 and Lemma 19 similarly (these lemmas are not particular for countable ground types but mention linear types appearing only once).

**Back to the Completeness Proof.** The following technical lemma is straightforward and used in subsequent proofs of other lemmas.

**Lemma 21.** If $r \prec_{\mathcal{Type}} r'$ then $r \prec_{\mathcal{Type}} r'$.

*Proof.* By induction on rigid terms:

- $r = x$, then by $r \prec_{\mathcal{Type}} r'$ we have that $r' = x$. It is trivial to show that $r \prec_{\mathcal{Type}} r'$.

- $r = r_1 t_1$, then by $r \prec_{\mathcal{Type}} r'$ we have that $r' = r_2 t_2$ such that $r_1 \prec_{\mathcal{Type}} r_2$ and $t_1 \prec_{\mathcal{Type}} t_2$. By induction we have that $r_1 \prec_{\mathcal{Type}} r_2$, and hence $r_1 t_1 \prec_{\mathcal{Type}} r_2 t_2$ by compositionality of $\prec_{\mathcal{Type}}$. ◀

Another technical lemma is the reverse implication of Lemma 21, which is slightly less straightforward. We separate them as this second lemma’s proof is more intricate, relying on Proposition 20.

**Lemma 22.** If $r \prec_{\mathcal{Type}} r'$ then $r \prec_{\mathcal{Type}} r'$.

*Proof.* By induction on $r$:

- *Variable:* $r = x$. By Point 1 of Proposition 17, $r' = x$, hence $r \prec_{\mathcal{Type}} r'$.

- *Applied Rigid Term:* $r = r_1 t_1$. By Point 3 of Proposition 17, $r' = r_2 t_2$. By Point 1 and subsequently Point 2 of Proposition 20, both $r_1 \prec_{\mathcal{Type}} r_2$ and $t_1 \prec_{\mathcal{Type}} t_2$. By induction, $r_1 \prec_{\mathcal{Type}} r_2$. We can now conclude that $r = r_1 t_1 \prec_{\mathcal{Type}} r_2 t_2 = r'$. ◀

Proposition 17 states that normal forms related by the type preorder must have the same normal form structure. The next lemma completes this, by stating that normal forms with the same structure and related by the type preorder have inner sub-terms related by the type preorder as well. This lemma is similar to an inversion lemma, but only working on normal forms, hence its name of normal inversion lemma.

**Lemma 23 (Normal Inversion Lemma for $\prec_{\mathcal{Type}}$).** Let $t, t'$ be terms and $r, r'$ be rigid terms.

1. Body of Abstractions: if $\lambda x.t \prec_{\mathcal{Type}} \lambda x.t'$ then $t \prec_{\mathcal{Type}} t'$.

2. Rigid Head: if $rt \prec_{\mathcal{Type}} r't'$ then $r \prec_{\mathcal{Type}} r'$.

3. Rigid Arguments: if $rt \prec_{\mathcal{Type}} r't'$ and $r \prec_{\mathcal{Type}} r'$ then $t \prec_{\mathcal{Type}} t'$.

*Proof.*

1. Let $\Gamma, M, L$ such that $\Gamma; x: M \vdash t: L$. We shall show that $\Gamma; x: M \vdash t': L$. It is easy to see that $\Gamma \vdash \lambda x.t: M \to L$ by applying rule $\lambda$. By hypothesis, we have that the same typing works for $\lambda x.t'$, i.e. $\Gamma \vdash \lambda x.t': M \to L$. Then the typing derivation starts by the rule $\lambda$ and the premise will read $\Gamma; x: M \vdash t': L$, which concludes the proof.

2. By Point 1 of Prop. 20, $r \prec_{\mathcal{Type}} r'$. By Lemma 22, we have that $r \prec_{\mathcal{Type}} r'$. By Point 2 of Prop. 20, we conclude that $t \prec_{\mathcal{Type}} t'$. ◀

3. By Lemma 21, as $r \prec_{\mathcal{Type}} r'$ we have that $r \prec_{\mathcal{Type}} r'$. By Point 2 of Prop. 20, we conclude that $t \prec_{\mathcal{Type}} t'$. ◀

Now, we are able to prove that for all normal forms, if they are related by the type preorder, then they are related by one step of simulation over the type preorder. The proof uses, first, the fact that the outer shape of normal forms match (Proposition 17) and, second, the normal inversion lemma (Lemma 23).
**► Theorem 24.** Let $w$ and $w'$ be two wh-normal forms such that $w \preceq_{\text{type}} w'$. Then $w \prec_{\preceq_{\text{type}}} w'$.

*Proof.* By case analysis on $w$:

1. If $w = x$, then by Point 1 of Prop. 17 we have that $w' = x$.

2. If $w = \lambda x.t$. Then by Point 2 of Prop. 17, we have that $w' = \lambda x.u$ for some term $u$. By Point 1 of Lemma 23, we have that $t \preceq_{\text{type}} u$.

3. If $w = rt$, then by Point 3 of Prop. 17, we have that $w' = r'u$ for some rigid term $r'$ and some term $u$. By Point 2 of Lemma 23, we have that $r \prec_{\preceq_{\text{type}}} w'$, By Point 3 of Lemma 23, we have that $t \preceq_{\text{type}} u$. ◀

The previous theorem is enough to prove that the type preorder is a whnf simulation, as whnf simulations only compare normal forms. We are then able to prove our final theorem that concludes the syntactic characterization of the type preorder.

**► Theorem 25.**

1. The type preorder $\preceq_{\text{type}}$ is a whnf simulation.

2. Completeness: $\preceq_{\text{type}} \subseteq \preceq_{\text{wh}}$

*Proof.*

1. Let $t$ and $t'$ be such that $t \preceq_{\text{type}} t'$. If $t$ does not $	o_{\text{wh}}$-terminate, we have nothing else to check.

Otherwise, we have that $t \to_{\text{wh}}^* w$ such that $w$ is a weak head normal form and by Point 2 of Proposition 7, we have that $t' \to_{\text{wh}}^* w'$ such that $w'$ is also a weak head normal form. As $t \preceq_{\text{type}} t'$, and by subject expansion and reduction, $w \preceq_{\text{type}} w'$. By Theorem 24, we have that $w \prec_{\preceq_{\text{type}}} w'$, which concludes the proof.

2. We can finally apply the coinductive argument: $\preceq_{\text{type}}$ is a whnf simulation by Point 1 and $\preceq_{\text{wh}}$ is the largest whnf simulation by definition. ◀

By combining soundness (Theorem 13) and completeness (Theorem 25), we get the complete syntactic characterization of the weak head type preorder $\preceq_{\text{type}}$.

**► Theorem 26.** *Weak head normal form similarity coincides with the weak type preorder, that is, for all terms $t, u$, $t \preceq_{\text{wh}} u$ iff $t \preceq_{\text{type}} u$. By symmetry, $\simeq_{\text{wh}} = \simeq_{\text{type}}$ as well.*

**Type-Böhm Theorem for Weak Head.** A corollary is a separation theorem (akin to Böhm theorem, but adapted for types) for $\beta$-normal forms. The standard Böhm theorem gives separating evaluation contexts for distinct $\beta\eta$-normal forms. Here, we give separating *types* and for distinct $\beta$-normal forms: our weak head types are able to distinguish $\eta$-equivalent terms.

**► Corollary 27 (Type-Böhm Theorem).** Let $n, n'$ be two syntactically distinct $\beta$-normal forms. There exists a typing context $\Gamma$ and a type $L$ such that $\Gamma \vdash n: L$ but $\Gamma \not\vdash n': L$.

*Proof.* It is clear that $n \preceq_{\text{wh}} n'$ for distinct $\beta$-normal forms $n$ and $n'$. Then, one can apply Theorem 25 to deduce a separating typing context and type. ◀

# 7 Conclusions

We study the equational theory induced by multi types and focus, in particular, on the proof technique to coinductively characterize it. We are able to avoid introducing term approximants, refining previous works by Breuvart et al. [13] and Ronchi Della Rocca [22].
4:16 Separating Terms by Means of Multi Types, Coinductively

We apply the proof technique to a simple case where one considers weak head multi types,
the appropriate multi types for weak head evaluation. We construct shape typings in order
to show that terms that are typable by the same types must have the same normal forms.
Building these shape typings is done explicitly, and they resemble the types built by Breuvart
et al. [13] in the case of head reduction in order to show that different approximants cannot
be type equivalent. After carefully examining the proof, we are able to clearly state that a
countable number of ground types are not needed, a single ground type being enough. We also
go for a more direct proof, without considering the contrapositive statement (syntactically
different terms implies that there exists a separating typing), closer to Ronchi Della Rocca's
separation [22], which is also based on head reduction.

This work bridges between two programming languages approaches: the study of the
untyped λ-calculus with its models and bisimilarity, a technique imported from process
calculi. While the main result is folklore for experts of the λ-calculus (Lévy-Longo tree
equivalence coincides with type equivalence), the coinductive flavor of bisimilarity appears to
be new in that equivalence–and makes for quite independent lemmas and easy proofs.

**Future Work.** The work presented here focuses on *non-idempotent* intersection types, which clearly plays a critical role in the soundness proof but appears to be less critical in our completeness development. Techniques with term approximants have been successful in the idempotent setting to characterize the equational theory, which raises the question whether or not our coinductive presentation can also work with idempotent intersection type systems.

We are working on re-using the proof technique described in this paper to a trickier
setting, namely the call-by-value λ-calculus. It would be interesting to give a syntactical
characterization of the equational theory induced by Ehrhard's call-by-value relational
semantics [17], for which there are none. A first (wrong) conjecture appeared in [18].
Preliminary results containing only typing transfer are already available on arXiv [5].

Recent work on CbN idempotent intersection types by Polonsky and Statman discuss uniqueness typings to separate terms up to $\beta\eta$ equivalence [20]. It would be interesting to see if their results generalize to normal form bisimilarity.

Recent developments have been able to refine contextual equivalence to a quantitative contextual equivalence, while crucially retaining the fact that this equivalence is invariant by $\beta$ (therefore, an equational theory) [6]. This work focusses on call-by-name and head reduction, where it is shown that Böhm tree equivalence coincides with this new quantitative equivalence. The authors conjecture that Lévy-Longo tree equivalence could match a *weak head* quantitative contextual equivalence.

As said in the introduction, we do not use a contrapositive statement to show that type
equivalence implies normal form bisimilarity. In intermediate lemmas, we may use classical
reasoning techniques. It would be interesting to check (possibly via a proof assistant) which
steps can be done only with constructive/intuistionistic reasoning. In the case of Böhm out
technique, we are not aware of a result that does not use the contrapositive yet the result is
deeply constructive (constructing explicitly a separating context).

References

1 S. Abramsky and C. H. L. Ong. Full Abstraction in the Lazy Lambda Calculus. *Information and Computation*, 105(2):159-267, 1993. doi:10.1006/inco.1993.1044.

2 Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. In Aniello Murano and Alexandra Silva, editors, *32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)*, volume 288 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 7:1-7:24, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2024.7.
3 Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. *PACMPL*, 2(ICFP):94:1–94:30, 2018. doi:10.1145/3236789.

4 Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Types by need. In *Luís Caires, editor, Programming Languages and Systems*, pages 410–439, Cham, 2019. Springer International Publishing. doi:10.1007/978-3-030-17184-1_15.

5 Beniamino Accattoli, Adrienne Lancelot, and Claudia Faggian. Normal form bisimulations by value, 2023. doi:10.48550/arXiv.2303.08161.

6 Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, and Gabriele Vanoni. Interaction equivalence. *Proc. ACM Program. Lang.*, 9(POPL), January 2025. doi:10.1145/3704891.

7 Victor Arrial, Giulio Guerrieri, and Delia Kesner. An implementation of the quantitative inhabitation for different lambda calculi in a unifying framework, 2023. doi:10.1145/3554339.

8 Victor Arrial, Giulio Guerrieri, and Delia Kesner. Quantitative inhabitation for different lambda calculi in a unifying framework. *Proc. ACM Program. Lang.*, 7(POPL):1483–1513, 2023. doi:10.1145/3571244.

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

10 Henk Barendregt and Giulio Manzonetto. *A Lambda Calculus Satellite*. College Publications, 2022. URL: https://www.collegepublications.co.uk/logic/mlf/?00035.

11 Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Proving soundness of extensional normal-form bisimilarities. *Electronic Notes in Theoretical Computer Science*, 336:41–56, 2018. The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII). doi:10.1016/j.entcs.2018.03.015.

12 Viviana Bono and Mariangiola Dezani-Ciancaglini. A tale of intersection types. In *Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '20, pages 7–20, New York, NY, USA, 2020. Association for Computing Machinery. doi:10.1145/3373718.3394733.

13 Flavien Breuvart, Giulio Manzonetto, and Domenico Ruoppolo. Relational Graph Models at Work. *Logical Methods in Computer Science*, Volume 14, Issue 3, July 2018. doi:10.23638/LMCS-14(3:2)2018.

14 Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Jacques Duparc and Thomas A. Henzinger, editors, *Computer Science Logic*, pages 298–312, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-74915-8_24.

15 Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. *Logic Journal of the IGPL*, 25(4):431–464, 2017. doi:10.1093/jigpal/jzx018.

16 Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Silvia Likavec. Behavioural inverse limit λ-models. *Theoretical Computer Science*, 316(1):49–74, 2004. Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott. doi:10.1016/j.tcs.2004.01.023.

17 Thomas Ehrhard. Collapsing non-idempotent intersection types. In Patrick Cégielski and Arnaud Durand, editors, *Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France*, volume 16 of *LIPIcs*, pages 259–273. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2012. doi:10.4230/LIPIcs.CSL.2012.259.

18 Axel Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting call-by-value böhm trees in light of their taylor expansion. *Log. Methods Comput. Sci.*, 16(3), 2020. URL: https://lmcs.episciences.org/6638.

19 Søren B. Lassen. Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. In Stephen D. Brookes, Achim Jung, Michael W. Mislove, and Andre Scedrov, editors, *Fifteenth Conference on Mathematical Foundations of Programming Semantics, MFPS 1999, Tulane University, New Orleans, LA, USA, April 28 - May 1, 1999*, volume 20 of *Electronic Notes in Theoretical Computer Science*, pages 346–374. Elsevier, 1999. doi:10.1016/S1571-0661(04)80083-5.
4:18 Separating Terms by Means of Multi Types, Coinductively

20 Andrew Polonsky and Richard Statman. On sets of terms having a given intersection type. *Logical Methods in Computer Science*, Volume 18, Issue 3, September 2022. doi:10.46298/lmcs-18(3:35)2022.

21 Simona Ronchi Della Rocca. Intersection Types and Denotational Semantics: An Extended Abstract. In Silvia Ghilezan, Herman Geuvers, and Jelena Ivetic, editors, *22nd International Conference on Types for Proofs and Programs (TYPES 2016)*, volume 97 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 2:1–2:7, Dagstuhl, Germany, 2018. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.TYPES.2016.2.

22 Simonetta Ronchi Della Rocca. Characterization theorems for a filter lambda model. *Information and Control*, 54(3):201–216, 1982. doi:10.1016/S0019-9958(82)80022-3.

23 Davide Sangiorgi. The lazy lambda calculus in a concurrency scenario. *Information and Computation*, 111(1):120–153, 1994. doi:10.1006/inco.1994.1042.