Separating Terms by Means of Multi Types, Coinductively

Denotational models give rise to mathematical interpretations of the $\lambda$-calculus, where different $\lambda$-terms may be sent to the same mathematical object. Equivalence classes of $\lambda$-terms in these models should always include syntactical equality–that only equates programs that have exactly the same syntax (up to $\alpha$-equivalence)–and $\beta$-equivalence. Indeed, $𝙸≔\lambda x.x$ and $\mathrm{𝙸𝙸}$ have different syntax but represent the same identity function. The computational theory $\lambda \beta$, that only quotients by $\beta$-equivalence, is still far from reaching most denotational models’ theories. Indeed, some terms are not $\beta$-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 }_{\mathrm{𝗐𝗁}}$. 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].

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.

Given an intersection type system, one can define what we call here type equivalence ${\simeq }_{\mathrm{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 }_{\mathrm{type}}$ does not validate well-known examples of equations validated by contextual equivalence ${\simeq }_{\mathrm{ctx}}$ (that are also examples of incompleteness for Sangiorgi’s normal form bisimilarity): for instance, $x\lambda y.xy{\simeq }_{\mathrm{ctx}}xx$ but $x\lambda y.xy{\simeq ̸}_{\mathrm{type}}xx$ (and $x\lambda y.xy{\simeq ̸}_{\mathrm{𝗐𝗁}}xx$) [1, 23].

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:

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 explictly 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).

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.

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.

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 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.

We focus on a specific reduction of the $\lambda$-calculus, weak head reduction, the variant of head reduction that does not reduce under lambdas.

Weak head reduction, denoted ${\to }_{\mathrm{𝗐𝗁}}$, is the closure of the beta rule $(\lambda x.t)u{\mapsto }_{\beta }t\{x\leftarrow u\}$ under applicative weak head contexts. In essence, all ${\to }_{\mathrm{𝗐𝗁}}$ steps are of the shape $(\lambda x.t)u{s}_1\mathrm{\dots }{s}_k{\to }_{\mathrm{𝗐𝗁}}t\{x\leftarrow u\}{s}_1\mathrm{\dots }{s}_k$ for $k\ge 0$.

Normal forms with respect to ${\to }_{\mathrm{𝗐𝗁}}$ are exactly characterized by the following grammar, separating normal forms into rigid terms and abstractions:

We say that a term is ${\to }_{\mathrm{𝗐𝗁}}$-normalizing if it reduces to a ${\to }_{\mathrm{𝗐𝗁}}$-normal form. Note that by well-known normalization theorems for weak head reduction, the fact that a term $\beta$-reduces to a ${\to }_{\mathrm{𝗐𝗁}}$-normal form is equivalent to ${\to }_{\mathrm{𝗐𝗁}}$-reducing to a ${\to }_{\mathrm{𝗐𝗁}}$-normal form. We define the contextual preorder and equivalence based on weak head termination.

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

As a consequence, the $\eta$ rule does not hold in general: $\mathrm{\Omega }$ and $\lambda x.\mathrm{\Omega }x$ are not contextually equivalent (for $\mathrm{\Omega }≔(\lambda x.xx)(\lambda x.xx)$, the paradigmatic looping term). In fact, if one is interested in the weak head contextual preorder, $\lambda x.tx$ refines $t$ but $t$ does not always refine $\lambda x.tx$ ($t{\precsim }_{\mathrm{ctx}}\lambda x.tx$ for all $t$ but $\lambda x.yx{\precsim ̸}_{\mathrm{ctx}}y$ for all variables $y$). If $t$ converges to an abstraction, there is no difference between both terms, as this $\eta$-equivalence is actually included in $\beta$ equivalence. Otherwise, it is in fact not true that $t$ refines $\lambda x.tx$ as $t$ can be non terminating whereas $\lambda x.tx$ is always a weak head normal form.

Issues with $\eta$-equivalence and weak head reduction actually go beyond this first observation. There exists $\eta$-equivalent terms that are contextually equivalent, the paradigmatic example being $x\lambda y.xy{\simeq }_{\mathrm{ctx}}xx$ [1, 23]. These two terms are contextually equivalent even though $\lambda y.xy$ and $x$ are not. Contextual inequivalence is somehow non-compositional in presence of $\eta$.

Multi types $M$ are finite multisets of linear types $L$ that are either base types ${\star }_k$ or arrow types $M⊸L$. In the original presentation of Bucciarelli et al. [15], there are distinct ground types and an abstraction type $\mathrm{♯}$: 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 $\mathrm{\Gamma }$ are finite-support maps from variables to multi types, denoted $x_1:M_1,\mathrm{\cdots },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 $\mathrm{\varnothing }$.

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

There are two axiom rules, one for variables ($\mathrm{𝖺𝗑}$) 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 ($\mathrm{@}$) 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,\mathrm{\cdots },L_k]⊸L$ and $u$ with many linear types $L_1,\mathrm{\cdots },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 $[]⊸L$, then one does not have to provide any type derivation for $u$ to apply the $\mathrm{@}$-rule.

We write $\pi ⊳\mathrm{\Gamma }⊢t:L$ if $\pi$ is a type derivation with final judgment $\mathrm{\Gamma }⊢t:L$.

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 $𝒲\mathscr{H}$ if and only if it is weak head normalizable.

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 $|\pi |$ is its total number of rules.

From quantitative subject reduction, it is typical to deduce (without reducibility arguments!) 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).

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].

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.

It is easy to check that ${\precsim }_{\mathrm{type}}$ is indeed a preorder (reflexive and transitive). Furthermore by subject reduction and subject expansion it is invariant by ${\to }_{\mathrm{𝗐𝗁}}$ 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^{\prime }$ (type-)improves $t$ if $t{\precsim }_{\mathrm{type}}{t}^{\prime }$, that is if all typings of $t$ are typings of $t^{\prime }$. Symmetrically, two terms are type equivalent if that they have the same set of typings.

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

Let $(t,t^{\prime })\in 𝙵(ℛ)$. We have two cases:

• $\mathrm{■}$

  If $t$ does not ${\to }_{\mathrm{𝗐𝗁}}$-terminate, then $(t,t^{\prime })\in 𝙵(ℛ)$.

• $\mathrm{■}$

  Otherwise, $t$ ${\to }_{\mathrm{𝗐𝗁}}$-reduces to a normal form $w$ and $t^{\prime }$ ${\to }_{\mathrm{𝗐𝗁}}$-reduces to a normal form $w^{\prime }$ such that $w{⟨ℛ⟩}_{\mathrm{𝑛𝑓}}{w}^{\prime }$. As $ℛ\subseteq {ℛ}^{\prime }$, we have that $w{⟨{ℛ}^{\prime }⟩}_{\mathrm{𝑛𝑓}}{w}^{\prime }$ (by an easy induction on ${⟨\cdot ⟩}_{\mathrm{𝑛𝑓}}$). We conclude that $(t,t^{\prime })\in 𝙵({ℛ}^{\prime })$ by definition.

$◀$

In the two following sections, we will exactly characterize the type preorder by whnf similarity, i.e. ${\precsim }_{\mathrm{𝗐𝗁}}={\precsim }_{\mathrm{type}}$. We call soundness ${\precsim }_{\mathrm{𝗐𝗁}}\subseteq {\precsim }_{\mathrm{type}}$, the easy part, and completeness ${\precsim }_{\mathrm{𝗐𝗁}}\supseteq {\precsim }_{\mathrm{type}}$, the difficult part.

An interesting corollary of this characterization is an alternative of monotonicity for whnf similarity (i.e. that ${\precsim }_{\mathrm{𝗐𝗁}}$ 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.

The proof follows from the exact characterization of ${\precsim }_{\mathrm{𝗐𝗁}}$ by ${\precsim }_{\mathrm{type}}$ (Theorem 26) and the fact that the latter enjoys monotonicity (Point 3 of Proposition 7).

By induction on the size of the derivation $\pi ⊳\mathrm{\Gamma }⊢t:L$.

The term $t$ is typable by the derivation $\pi ⊳\mathrm{\Gamma }⊢t:L$ therefore it is normalizable by Theorem 3. Hence we have $t{\to }_{\mathrm{𝗐𝗁}}^{k}w$ and therefore (since $ℛ$ is a bisimulation) $t^{\prime }{\to }_{\mathrm{𝗐𝗁}}^{\ast }{w}^{\prime }$ with $w{⟨ℛ⟩}_{\mathrm{𝑛𝑓}}{w}^{\prime }$ with $w$ and $w$ weak head normal forms. By quantitative subject reduction (Proposition 4), there is a derivation ${\pi }_1⊳\mathrm{\Gamma }⊢w:M$ whose size is at most the size of $\pi$. Instead of looking for a derivation ${\pi }^{\prime }$ of $t^{\prime }$, we can look for a derivation ${\pi }_1^{\prime }$ of $w^{\prime }$ and conclude by (qualitative) subject expansion for $\mathrm{𝗐𝗁}$-reduction (Proposition 5).

Now, from $w{⟨ℛ⟩}_{\mathrm{𝑛𝑓}}{w}^{\prime }$ and ${\pi }_1⊳\mathrm{\Gamma }⊢w:L$, we build the derivation ${\pi }_1^{\prime }⊳\mathrm{\Gamma }⊢w^{\prime }:L$. By case analysis on the last rule of the derivation ${\pi }_1$:

1. 1.

   Axiom rule.

   Then by $w=x{⟨ℛ⟩}_{\mathrm{𝑛𝑓}}{w}^{\prime }$, $w^{\prime }=x$ and ${\pi }_1^{\prime }≔{\pi }_1$ types $w^{\prime }$ accordingly.

2. 2.

   Abstraction-$\star$ rule.

   Then by $w=\lambda x.t{⟨ℛ⟩}_{\mathrm{𝑛𝑓}}{w}^{\prime }$, $w^{\prime }=\lambda x.u$ and ${\pi }_1^{\prime }≔{\pi }_1$ types $w^{\prime }$ accordingly.

3. 3.

   Abstraction rule.

   Then by $w=\lambda x.u{⟨ℛ⟩}_{\mathrm{𝑛𝑓}}{w}^{\prime }$, $w^{\prime }=\lambda x.u^{\prime }$ with $uℛu^{\prime }$.

   The derivation ${\pi }_2⊳\mathrm{\Gamma },x:M⊢u:L^{\prime }$ is of a strictly smaller size than $\pi$. By induction, since $uℛu^{\prime }$, there is a derivation ${\pi }_2^{\prime }⊳\mathrm{\Gamma },x:M⊢u^{\prime }:L^{\prime }$.

   We build the derivation ${\pi }_1^{\prime }$ by applying the $\lambda$ typing rule to ${\pi }_2^{\prime }$.

4. 4.

   Application rule.

   Then by $w=rt{⟨ℛ⟩}_{\mathrm{𝑛𝑓}}{w}^{\prime }$, $w^{\prime }=r^{\prime }u$ with $r{⟨ℛ⟩}_{\mathrm{𝑛𝑓}}{r}^{\prime }$ and $tℛu$. By induction on the sub-derivations, we get the appropriate derivation for $w^{\prime }$.

$◀$

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

Let $t,u$ terms such that $t{\precsim }_{\mathrm{𝗐𝗁}}u$. Let $\mathrm{\Gamma }⊢t:L$ a typing for $t$. As ${\precsim }_{\mathrm{𝗐𝗁}}$ is a whnf bisimulation, by Proposition 12, we have that $\mathrm{\Gamma }⊢u:L$. Hence $t{\precsim }_{\mathrm{type}}u$. $◀$

To prove completeness, i.e. that ${\precsim }_{\mathrm{type}}\subseteq {\precsim }_{\mathrm{𝗐𝗁}}$, we shall use coinduction. We first show that ${\precsim }_{\mathrm{type}}$ is a whnf simulation, which implies it is included in the largest whnf simulation, namely whnf similarity ${\precsim }_{\mathrm{𝗐𝗁}}$.

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 ${\mathrm{\Gamma }}_x,L_x$ that ensure that for any term $t$ typable by this typing, i.e. ${\mathrm{\Gamma }}_x⊢t:L_x$, we have that $t$ weak head normalizes to $x$. In this specific case, ${\mathrm{\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 ${\mathrm{\Gamma }}_x,L_x$ could be to replace ${\star }_0$ by any linear type. As an example, ${\mathrm{\Gamma }}_x≔x:[[{\star }_0]⊸{\star }_1]$ and $L_x≔[{\star }_0]⊸{\star }_1$ is also a correct typing for $x$ but it is not separating, since it also types $\lambda y.xy$.

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

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. 1.

   Any normal form can be typed in the ${⊢}_{\mathrm{shape}}$ system;

2. 2.

   The ${⊢}_{\mathrm{shape}}$ system is sound for the weak head multi type system $⊢$ : if $\mathrm{\Gamma }{⊢}_{\mathrm{shape}}t:L$ then $\mathrm{\Gamma }⊢t:L$;

3. 3.

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

Point 1 is immediate given the definition of ${⊢}_{\mathrm{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.

Proposition 17 (and the shape typing system ${⊢}_{\mathrm{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^{\prime }$ generates a difference between $\lambda x.t$ and $\lambda x.t^{\prime }$, and between $xt$ and $x{t}^{\prime }$). 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. 1.

   Look for a possible outer difference with ${⊢}_{\mathrm{shape}}$;

2. 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^{\prime }$ then $t$ is whnf similar to $t^{\prime }$.

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.

Erasing types can be used to type any rigid term $x{t}_1\mathrm{\cdots }{t}_k$, by assigning a $(k,i)$ erasing type ${([]⊸)}^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.

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

• $\mathrm{■}$

  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]⊢x:E_i^n$ is a correct derivation for all $n$ consisting only of the axiom rule.

• $\mathrm{■}$

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

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

$◀$

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.

By induction on $r$.

• $\mathrm{■}$

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

• $\mathrm{■}$

  Application i.e. $r=r^{\prime }t$. The last rule of any derivation must be the application rule.

  By induction there exists $k-1$ multi types ${(M_i)}_{1\le i\le k}$ such that $[M_1⊸\mathrm{\dots }{M}_{k-1}⊸({[L_i]}_{i\in I}⊸L)]\subseteq \mathrm{\Delta }(x)$. Set $M_k≔{[L_i]}_{i\in I}$ then $[M_1⊸\mathrm{\dots }{M}_k⊸L)]\subseteq \mathrm{\Gamma }(x)$ as $\mathrm{\Delta }\subseteq \mathrm{\Gamma }$.

  For the second point, by induction, for all linear type $L^{\prime }$, we have that $x:[M_1⊸\mathrm{\dots }{M}_{k-1}⊸({[L_i]}_{i\in I}⊸L^{\prime })],{\mathrm{\Delta }}^{\prime }⊢r:({[L_i]}_{i\in I}⊸L^{\prime })$, 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 $(\mathrm{\varnothing },{\star }_0)$.

1. 1.

   Suppose $w\ne x$. Cases of $w$:

   • $\mathrm{■}$

     Different Variable: if $w=y$, then $x:[{\star }_0]⊢x:{\star }_0$, but $y$ is not typable by $(x:[{\star }_0],{\star }_0)$.

   • $\mathrm{■}$

     Abstraction: if $w=\lambda y.u$, then $x:[{\star }_0]⊢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.

   • $\mathrm{■}$

     Rigid Term: if $w=r^{\prime }u$, then $x:[{\star }_0]⊢x:{\star }_0$, but $x:[{\star }_0]⊬r^{\prime }u:{\star }_0$, as a non variable rigid term needs an arrow type in the context for its head variable (per Lemma 16).

2. 2.

   We know that $\mathrm{\varnothing }⊢\lambda x.t:{\star }_0$ however $\mathrm{\varnothing }⊬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. 3.

   There exists a derivation $x:[E_0^k]⊢rt:{\star }_0$ where $k\ge 1$ by Lemma 15 but $x:[E_0^k]⊬y:{\star }_0$ for all $y$ variables and $x:[E_0^k]⊬\lambda y.s:{\star }_0$ for all abstraction $\lambda y.s$. Hence $w$ is a non-variable rigid term.

$◀$

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.

By induction on rigid terms:

• $\mathrm{■}$

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

• $\mathrm{■}$

  $r=r^{\prime }t$. Then the derivation $\mathrm{\Gamma }⊢r:L$ must start with a typing rule $\mathrm{@}$:

  with $\mathrm{\Gamma }={\mathrm{\Gamma }}_0\uplus ({\uplus }_{i\in I}{\mathrm{\Gamma }}_i)$.

  By Lemma 16, $x:[{([]⊸)}^{k}L]$ is included in ${\mathrm{\Gamma }}_0$ (as it is the only occurrence of the $L$ type).

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

$◀$

By induction on rigid terms:

• $\mathrm{■}$

  $r=x$. Then the only derivation possible for $r$ is $x:[M_1⊸\mathrm{\cdots }⊸M_k⊸L]⊢x:M_1⊸\mathrm{\cdots }⊸M_k⊸L$, for which the statement holds.

• $\mathrm{■}$

  $r=r^{\prime }t$. Then the derivation $\mathrm{\Gamma }⊢r:M_i⊸\mathrm{\cdots }⊸M_k⊸L$ starts with a typing rule $\mathrm{@}$:

  with $\mathrm{\Gamma }={\mathrm{\Gamma }}_0\uplus ({\uplus }_{i\in I}{\mathrm{\Gamma }}_i)$.

  By Lemma 16, $x:[N_1⊸\mathrm{\cdots }⊸N_k⊸L]$ is included in ${\mathrm{\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.

1. 1.

   Let $\mathrm{\Gamma },L$ such that $\mathrm{\Gamma }⊢r:L$. We shall show that $\mathrm{\Gamma }⊢r^{\prime }:L$ as well.

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

   By Lemma 16, we can set $L^{\prime }≔[]⊸{\star }_{i+1}$ and $\mathrm{\Delta }≔{\mathrm{\Gamma }}^{\prime },x:[M_1⊸\mathrm{\cdots }⊸M_k⊸L^{\prime }]$ (where $\mathrm{\Gamma }={\mathrm{\Gamma }}^{\prime },x:[M_1⊸\mathrm{\cdots }⊸M_k⊸L]$) and we still have that $\mathrm{\Delta }⊢r:L^{\prime }$. It is clear that $(\mathrm{\Delta },{\star }_{i+1})$ types $rt$:

   By hypothesis, we have that $r^{\prime }{t}^{\prime }$ is typable by $(\mathrm{\Delta },{\star }_{i+1})$. The derivation starts as:

   By Lemma 16, $x:[M_1⊸\mathrm{\cdots }⊸M_k⊸L^{\prime }]$ is included in ${\mathrm{\Gamma }}_0$ (as $L^{\prime }$ is the only type where ${\star }_{i+1}$ occurs in $\mathrm{\Gamma }$). By Lemma 19 applied on ${\mathrm{\Gamma }}_0⊢r^{\prime }:{[L_i]}_{i\in I}⊸{\star }_{i+1}$, we know ${[L_i]}_{i\in I}=[]$. Hence $I$ is empty and ${\mathrm{\Gamma }}_0=\mathrm{\Delta }$.

   Hence, we have a derivation of final judgment $\mathrm{\Delta }⊢r^{\prime }:L^{\prime }$. By Lemma 16 and as ${\star }_{i+1}$ only appears in one linear type in $\mathrm{\Delta }$, we have that $\mathrm{\Gamma }⊢r^{\prime }:L$ as well.

2. 2.

   Let $\mathrm{\Gamma },L$ such that $\mathrm{\Gamma }⊢t:L$. We shall show that $\mathrm{\Gamma }⊢t^{\prime }:L$.

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

   Let $\mathrm{\Delta }≔x:[{([]⊸)}^k⊸[L]⊸{\star }_{i+1}]$ such that $\mathrm{\Delta }⊢r:[L]⊸{\star }_{i+1}$ ($x$ is then the head variable of $r$).

   Then, as $r{\precsim }_{\mathrm{type}}{r}^{\prime }$, we also have that $\mathrm{\Delta }⊢r^{\prime }:[L]⊸{\star }_{i+1}$.

   By hypothesis, we have that $\mathrm{\Delta }\uplus \mathrm{\Gamma }⊢r^{\prime }{t}^{\prime }:{\star }_{i+1}$. The derivation starts with the application rule:

   By Lemma 16, $\mathrm{\Delta }$ must be included in ${\mathrm{\Gamma }}_0$ (as it is the only occurrence of the ${\star }_{i+1}$ type). The only derivation of $r^{\prime }$ containing $\mathrm{\Delta }$ in the context must be $\mathrm{\Delta }⊢r^{\prime }:{[L_i]}_{i\in I}⊸{\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}⊸{\star }_{i+1}$ must appear in $\mathrm{\Delta }$).

   Hence, we have a derivation of final judgment $\mathrm{\Gamma }⊢t^{\prime }:L$ which concludes the proof.

$◀$

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 $\mathrm{\Gamma },L$ the largest linear type ($i≔$ the maximum number of top-most arrows of a type $L^{\prime }$ that appears in $\mathrm{\Gamma },L$–$L^{\prime }$ can appear anywhere, even inside 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).

The following technical lemma is straightforward and used in subsequent proofs of other lemmas.

By induction on rigid terms:

• $\mathrm{■}$

  $r=x$, then by $r{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{r}^{\prime }$ we have that $r^{\prime }=x$. It is trivial to show that $r{\precsim }_{\mathrm{type}}{r}^{\prime }$.

• $\mathrm{■}$

  $r=r_1{t}_1$, then by $r{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{r}^{\prime }$ we have that $r^{\prime }=r_2{t}_2$ such that $r_1{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{r}_2$ and $t_1{\precsim }_{\mathrm{type}}{t}_2$. By induction we have that $r_1{\precsim }_{\mathrm{type}}{r}_2$, and hence $r_1{t}_1{\precsim }_{\mathrm{type}}{r}_2{t}_2$ by compositionality of ${\precsim }_{\mathrm{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.

By induction on $r$:

• $\mathrm{■}$

  Variable: $r=x$. By Point 1 of Proposition 17, $r^{\prime }=x$, hence $r{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{r}^{\prime }$.

• $\mathrm{■}$

  Applied Rigid Term: $r=r_1{t}_1$. By Point 3 of Proposition 17, $r^{\prime }=r_2{t}_2$.

  By Point 1 and subsequently Point 2 of Proposition 20, both $r_1{\precsim }_{\mathrm{type}}{r}_2$ and $t_1{\precsim }_{\mathrm{type}}{t}_2$. By induction, $r_1{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{r}_2$. We can now conclude that $r=r_1{t}_1{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{r}_2{t}_2=r^{\prime }$.

$◀$

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.

1. 1.

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

2. 2.

   By Point 1 of Prop. 20, $r{\precsim }_{\mathrm{type}}{r}^{\prime }$. By Lemma 22, we have that $r{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{r}^{\prime }$.

3. 3.

   By Lemma 21, as $r{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{r}^{\prime }$ we have that $r{\precsim }_{\mathrm{type}}{r}^{\prime }$. By Point 2 of Prop. 20, we conclude that $t{\precsim }_{\mathrm{type}}{t}^{\prime }$.

$◀$

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).

By case analysis on $w$:

1. 1.

   If $w=x$, then by Point 1 of Prop. 17 we have that $w^{\prime }=x$.

2. 2.

   If $w=\lambda x.t$. Then by Point 2 of Prop. 17, we have that $w^{\prime }=\lambda x.u$ for some term $u$. By Point 1 of Lemma 23, we have that $t{\precsim }_{\mathrm{type}}u$.

3. 3.

   If $w=rt$, then by Point 3 of Prop. 17, we have that $w^{\prime }=r^{\prime }u$ for some rigid term $r^{\prime }$ and some term $u$. By Point 2 of Lemma 23, we have that $r{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{r}^{\prime }$. By Point 3 of Lemma 23, we have that $t{\precsim }_{\mathrm{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.

1. 1.

   Let $t$ and $t^{\prime }$ be such that $t{\precsim }_{\mathrm{type}}{t}^{\prime }$. If $t$ does not ${\to }_{\mathrm{𝗐𝗁}}$-terminate, we have nothing else to check.

   Otherwise, we have that $t{\to }_{\mathrm{𝗐𝗁}}^{\ast }w$ such that $w$ is a weak head normal form and by Point 2 of Proposition 7, we have that $t^{\prime }{\to }_{\mathrm{𝗐𝗁}}^{\ast }{w}^{\prime }$ such that $w^{\prime }$ is also a weak head normal form. As $t{\precsim }_{\mathrm{type}}{t}^{\prime }$, and by subject expansion and reduction, $w{\precsim }_{\mathrm{type}}{w}^{\prime }$. By Theorem 24, we have that $w{⟨{\precsim }_{\mathrm{type}}⟩}_{\mathrm{𝑛𝑓}}{w}^{\prime }$, which concludes the proof.

2. 2.

   We can finally apply the coinductive argument: ${\precsim }_{\mathrm{type}}$ is a whnf simulation by Point 1 and ${\precsim }_{\mathrm{𝗐𝗁}}$ 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 ${\precsim }_{\mathrm{type}}$.

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.

It is clear that $n{\precsim ̸}_{\mathrm{𝗐𝗁}}{n}^{\prime }$ for distinct $\beta$-normal forms $n$ and $n^{\prime }$. Then, one can apply Theorem 25 to deduce a separating typing context and type. $◀$

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 $\lambda$-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).