# Semantic Bounds and Multi Types, Revisited

Beniamino Accattoli

► To cite this version:

Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. CSL 2024 - 32nd EACSL Annual Conference on Computer Science Logic, Feb 2024, Naples, Italy. 10.4230/LIPIcs.CSL.2024.7 . hal-04837714

HAL Id: hal-04837714

https://inria.hal.science/hal-04837714v1

Submitted on 13 Dec 2024

**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 Attribution 4.0 International License
# Semantic Bounds and Multi Types, Revisited

Beniamino Accattoli

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

Inria & LIX, École Poytechnique, Palaiseau, France

## Abstract

Intersection types are a standard tool in operational and semantical studies of the λ-calculus. De Carvalho showed how multi types, a quantitative variant of intersection types providing a handy presentation of the relational denotational model, allows one to extract precise bounds on the number of β-steps and the size of normal forms.

In the last few years, de Carvalho's work has been extended and adapted to a number of λ-calculi, evaluation strategies, and abstract machines. These works, however, only adapt the first part of his work, that extracts bounds from multi type *derivations*, while never consider the second part, which deals with extracting bounds from the multi types themselves. The reason is that this second part is more technical, and requires to reason up to *type substitutions*. It is however also the most interesting, because it shows that the bounding power is *inherent* to the relational model (which is induced by the types, without the derivations), independently of its presentation as a type system.

Here we dissect and clarify the second part of de Carvalho's work, establishing a link with principal multi types, and isolating a key property independent of type substitutions.

**2012 ACM Subject Classification** Theory of computation → Lambda calculus; Theory of computation → Denotational semantics; Theory of computation → Operational semantics

**Keywords and phrases** Lambda calculus, intersection types, denotational semantics, linear logic

**Digital Object Identifier** 10.4230/LIPIcs.CSL.2024.7

**Related Version** Paper with proof appendix hosted on arXiv: http://arxiv.org/abs/2311.18233 [1]

## 1 Introduction

Denotational semantics studies invariants of program evaluation. The typical way in which it is connected to the operational semantics of λ-calculi is at the *qualitative* level, via *adequacy*: the denotational interpretation $[[t]]$ of a λ-term $t$ is non-trivial (typically non-empty) if and only if the evaluation of $t$ terminates.

At first sight, denotational semantics cannot provide *quantitative* operational insights such as evaluation lengths, because of its invariance by evaluation. Things are in fact not so black and white. Being invariant by evaluation, denotational semantics models normal forms, and in a *compositional* way: by composing the interpretations of two terms one can obtain the interpretation of the result of their application – therefore, denotational semantics does reflect the evaluation process *somehow*.

The aim of this paper is to revisit some overlooked – but we believe important – results for the λ-calculus by de Carvalho, about the extraction of bounds on evaluation lengths and the size of normal forms from the interpretation of terms into the relational model.

**Relational Semantics and Multi Types.** The relational model [37, 17] is a simple denotational semantics of the λ-calculus induced by the relational model of linear logic, via the representation of the λ-calculus in linear logic. It is a paradigmatic model, underlying many others [30, 31, 24, 45, 48], mainly studied by Ehrhard and his students and co-authors [38, 18, 21, 16, 32, 33, 34, 26, 47, 46, 49, 15], the importance of which has emerged slowly. One of its features is that it admits a handy presentation via an intersection type system.

The distinguished property of intersection types is that they *characterize* termination properties, in the sense that they not only enforce termination, but they also type *all* terminating terms. Additionally, by tuning the definition of the type system, one can capture

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

© Beniamino Accattoli;

licensed under Creative Commons License CC-BY 4.0

32nd EACSL Annual Conference on Computer Science Logic (CSL 2024).

Editors: Aniello Murano and Alexandra Silva; Article No. 7; pp. 7:1–7:24

Leibniz International Proceedings in Informatics

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

LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 7:2 Semantic Bounds and Multi Types, Revisited

different notions of termination (weak head/head/leftmost termination, strong normalization, call-by-value/need, etc). Such a characterization usually induces a model: the set of types for a term *t* is an invariant of the characterized notion of evaluation →, which gives rise to a denotational semantics which is adequate for →. Therefore, intersection type systems are a tool halfway the operational and the denotational semantics of the λ-calculus.

Multi types are a *linear logic-related* variant of intersection types where intersections are *non-idempotent* (they are also known as *non-idempotent intersection types*), that is where $A \cap A \neq A$. The set of multi types judgements derivable for a term *t* provides a denotation $[t]$ which coincides with the interpretation into the relational model.

**Multi Types and Quantitative Bounds.** In a seminal work, de Carvalho used the multi type system to obtain exact bounds on the evaluation lengths and the size of normal form for λ-terms [25, 27]. The relevance of his work was fully appreciated by the community only a decade later (as surveyed below), when it blossomed into a number of variations and extensions by other authors. De Carvalho developed *two* main results, but only the first one has widely permeated the community. The second one is arguably the most technical but also the deeper one. The aim of this paper is to make it accessible to a wider audience.

De Carvalho’s original presentation in [25, 27] uses multi types to measure two forms of strong evaluations realized by abstract machines, implementing the head and leftmost call-by-name strategies. In this overview, we prefer to slightly depart from the (by now somewhat outdated) details of his work, forgetting about abstract machines, focussing on leftmost evaluation (the head case is treated at the end of the paper), and isolating three (rather than two) kinds of bounds:

1. *Bounds from type derivations.* The size $|\Phi|$ of a type derivation $\Phi \vdash \Gamma \vdash t: L$ bounds the number of leftmost steps from *t* to its normal form *nf*(*t*) plus the size $|nf(t)|$ of the normal form. Moreover, derivations of minimal size provide exact bounds.

2. *Size bounds from types.* The types in the final judgment – a point of the relational interpretation $[t]$ – also provide a bound, independently of the derivation $\Phi$. Being invariant by evaluation, they cannot bound evaluation lengths. They do however bound the size $|nf(t)|$ of the normal form, and bounds are exact when types are minimal.

3. *Bounds from composable types.* De Carvalho shows that types can be used to bound evaluation lengths compositionally: from the types in $[t]$ and $[u]$ it is possible to extract bounds about the leftmost evaluation and the normal form of *tu*, with *no reference to type derivations*. Exact bounds rest on a complex construction involving type substitutions. The third kind of bounds is de Carvalho’s second result, and it is where the bounding power of the multi type system (which is just one possible way of defining relational semantics) is *lifted* to relational semantics. Therefore, the lifting guarantees that the bounding power is an *inherent* feature of the relational model – multi types are just a handy tool to show it.

Of the three results, the third one is the most technical. In particular, it requires to enrich the type system with an infinity of type variables and work up to type substitutions. The puzzling fact is that these extra features play no role in the two previous points.

**De Carvalho's Legacy.** De Carvalho developed his results in his PhD, defended in 2007 [25]. His work was known by the community thanks to a technical report, turned into a journal paper only much later, in 2018 [27]. Soon after his PhD, he adapted his work to linear logic, with Pagani and Tortora de Falco [28, 29]. Then, Bernadet and Graham-Lengrand adapted his work to measure the longest evaluation in the λ-calculus [14], but they only provided bounds of the first kind (*from type derivations*).
At the time, it was not known whether it would make sense to count the number of $\beta$-steps (or linear logic cut-elimination steps) as a reasonable measure of complexity. After the case of the $\lambda$-calculus was clarified in the positive by Accattoli and Dal Lago [2], de Carvalho's work has been revisited by Accattoli et al. [7]. The revisitation started a new wave of works adapting de Carvalho's study to many evaluation strategies and extensions of the $\lambda$-calculus, including call-by-value [8, 9], call-by-need [10], a linear logic presentation of call-by-push-value [19, 42], the $\lambda\mu$-calculus [41], the $\lambda$-calculus with pattern matching [13], generalized applications [35], fully lazy sharing [39], global state [12], the probabilistic $\lambda$-calculus [23], the abstract machine underlying the geometry of interaction [3], and even adapted as to measure space [4, 5]. All these works provide bounds of the first kind, and some of them also of the second kind, but none of them deals with those of the third kind (bounds from composable types).

**Contributions.** This paper revisits the *bounds from composable types*, appeared only in [27, 28]. Beyond providing cleaner proofs of the results, we have a very close look at these bounds, isolating the subtleties and decomposing the proofs in smaller steps. In particular:

- *Subtlety 1, minimality does not work:* when bounding a single term, both derivations and types provide exact bounds when they are minimal. When dealing with the application of $t$ to $u$, every pair of composable types for them provides bounds. We stress that the technicalities for bounds from composable types are inherent to the problem, since the minimal composable pair in general does *not* provide exact bounds.

- *Subtlety 2, the gap between derivations and types:* we draw attention to the fact that the previous subtlety stems from a fact about derivations in *isolation*, namely that, for a normal term $t$, both the derivation $\Phi \vdash \Gamma \vdash t:L$ and the types in $\Gamma$ and $L$ provide bounds for $|t|$, but they may not coincide. In general, the bound from types is *laxer*. The bounds gap hinders the possibility of lifting the bounding power from derivations to types, if bounds from some derivations are not reflected by any type in the interpretation $[t]$.

- *Dry representation and type substitutions:* we isolate the property behind de Carvalho's solution of this problem, which rests on type variables and type substitutions, and we connect it with the study of principal types. The idea is that given a type derivation $\Phi \vdash \Gamma \vdash t:L$ for which there is a gap between the bound from $\Phi$ and the bound from $\Gamma$ and $L$, there always is a second *dry* derivation $\Psi \vdash \Delta \vdash t:L'$, whose types $\Delta$ and $L'$ give the same bound as the first derivation $\Phi$, plus a type substitution $\sigma$ turning $\Psi$ into $\Phi$. Then, all bounds coming from derivations can also be seen as coming from types, potentially from the types of other derivations – the *dry ones* – but related via type substitutions.

- *Removing substitutions:* lastly, we show that *weaker* bounds from composable types can be obtained *without* dealing with an infinity of type variables and type substitutions. This point provides both a simplified route to the (slightly weaker) bounds and an explanation of why these additional technicalities are needed for the full result.

**Internal vs External View.** The problem studied in the paper can also be seen in a more abstract way. Terms, or more generally programs, can be studied from two perspectives, which are distinct and yet entangled. The internal view considers programs as closed systems and looks at their internal evaluation in isolation. In the external view, programs are seen as parts of larger systems. What is relevant is how programs compose and interact with each other, their internal evaluation is instead secondary and hidden.
7:4 Semantic Bounds and Multi Types, Revisited

Cost analyses are usually done following the internal view, while denotational semantics and types are external-oriented tools. Normal forms can be seen as internalizing the external information, as they are normal for the internal process and thus retain only information for potential external interactions. Multi type derivations capture both the number of steps of typed terms (which is an internal information) and the structure of their normal forms (which is the internalization of external information). Multi types instead capture the external information only (each type capturing a potential interaction).

Bounds from composable types connect internal and external information, as they use types (that are external) to bound the length of evaluation (which is internal) of the isolated system given by the two composed terms. The bounds are obtained building over the connection between types and normal forms. The difficulty in this study stems from the fact that in general there is a gap between how the external information is represented in types (richly, distinguishing between different interactions) and how it is internalized in normal forms (in a raw way, all possible interactions are flattened on a single object).

**Limits of de Carvalho's Approach.** The aim of this paper is also to highlight a fundamental limitation of de Carvalho's work. As we ourselves suggested, bounds from composable types can be seen as lifting the bounding power from the type system to the relational model. There is however a delicate point, as the lifting does not cover the whole of the model. The relational model, indeed, does not only interpret full normal forms and terminating terms, but also *head* normal forms and terms that are *head normalizable*. In particular, there are terms that are *hereditarily* head normalizing and yet never fully normalize, such as fix-point combiners. For these terms, which have non-empty interpretation in the relational model, de Carvalho's study does not say anything, because it assumes that the terms to be composed are fully normal. De Carvalho's bounds for head reduction do not solve the issue, they rather make it worse, since his theorems for the head case still have to assume that the composed terms are fully normal, which seems an unnatural assumption that is nonetheless mandatory.

Consequently, de Carvalho's technique does not apply to all terms having non-empty interpretation in the relational model. Here, we point out the problem, which is a first essential step. We do not aim at solving it, because it seems to require the development of a new approach, not just a refinement of de Carvalho's. Abstractly, the limits of his technique come from the fact that external information is measured by reducing it to internal information, rather than measuring it *separately* from it, which would allow one to measure external information even when the internal evaluation process does not fully terminate.

**Proofs.** A few proofs are omitted and can be found in the Proof Appendix available on ArXiv [1].

2 Head and Leftmost Reductions and Normal Forms

**Basics of $\lambda$.** The set $\Lambda$ of untyped $\lambda$-terms is defined by $t ::= x \mid \lambda x.t \mid tt$, which are considered as quotiented by $\alpha$-equivalence. The capture-avoiding substitution of $x$ by $u$ in $t$ is written $t\{x\leftarrow u\}$.

**$\beta$-Reduction and Normal Forms.** $\beta$-reduction $\rightarrow_{\beta} \subseteq \Lambda \times \Lambda$ is defined as follows:

$\beta$-REDUCTION

$\frac{\overline{(\lambda x.t)u \to_{\beta} t\{x \leftarrow u\}}^{ax}}{}$

$\frac{t \to_{\beta} t' \qquad \lambda}{\lambda x.t \to_{\beta} \lambda x.t'}$

$\frac{t \to_{\beta} t' \qquad @l}{tu \to_{\beta} t'u}$

$\frac{t \to_{\beta} t' \qquad @r}{ut \to_{\beta} ut'}$
It is well known that $\beta$-reduction is non-deterministic but confluent, that is, a term can have at most one normal form. Normal forms (for $\beta$) are described by the following grammar relying on the mutually inductive notion of neutral term:

$$ \text{NEUTRAL TERMS} \quad n ::= x \mid nf \qquad \text{NORMAL FORMS} \quad f ::= n \mid \lambda x.f $$

An alternative streamlined definition of normal forms is $f := \lambda x_1 \dots \lambda x_n (y f_1 \dots f_k)$ with $n, k \ge 0$, $y$ possibly equal to one of the $x_i$, and the terms $f_j$ normal forms themselves.

For our quantitative study, we need a notion of size of normal forms. We use the following inner one, which counts the number of inner nodes of a term, when seen as a tree having variables as leaves, as it is the one that best matches what shall be measured via multi types.

**► Definition 1 (Inner size).** The inner size of $\lambda$-terms is defined as follows:

$$ |x|_{\text{in}} ::= 0 \qquad |\lambda x.u|_{\text{in}} ::= |u|_{\text{in}} + 1 \qquad |u r|_{\text{in}} ::= |u|_{\text{in}} + |r|_{\text{in}} + 1 $$

**Head Reduction.** A deterministic notion of evaluation for $\lambda$-terms is head reduction, which reduces only the left branch of a term, when seen as a tree. The definition follows (it is obtained by omitting rule $@r$ in the definition of $\beta$, and constraining $t$ not to be an abstraction in rule $@l$):

**HEAD REDUCTION**

$$ \frac{\overline{(\lambda x.t)u \to_h t \{x \leftarrow u\}}^{ax}}{\lambda x.t \to_h \lambda x.t'} \lambda \qquad \frac{t \to_h t' \quad t \neq \lambda x.r}{tu \to_h t'u} @l $$

Let $l := \lambda z.z$ be the identity combinator, $\delta := \lambda x.xx$ be the duplicator, and consider the following examples: $\delta lt \to_h ll$ and $\lambda y.(\delta l) \to_h \lambda y.ll$ but $(\lambda y.(\delta l))t \not\to_h (\lambda y.ll)t$, as it rather reduces to $(\delta l)\{y \leftarrow t\} = \delta l$.

Head reduction might not compute normal forms, since it does not evaluate arguments. Its notion of normal form follows:

$$ \text{HEAD NORMAL FORMS} \quad h ::= \lambda x_1 \dots \lambda x_n (yt_1 \dots t_k) \qquad \text{with } n, k \ge 0 \text{ and } y \text{ possibly equal to one of the } x_i. $$

We shall also need a notion of head size for head normal forms defined as $|h|_h := n + k$ if $h = \lambda x_1 \dots \lambda x_n (yt_1 \dots t_k)$.

**Leftmost Reduction.** Leftmost-outermost reduction $\to_{1o}$ (shortened to leftmost) is a deterministic extension of head reduction as to reduce arguments and reach normal forms. The definition relies on the notion of neutral term $n$ used to describe normal forms.

**LEFTMOST(-OUTERMOST) REDUCTION**

$$ \frac{\overline{(\lambda x.t)u \to_{1o} t \{x \leftarrow u\}}^{ax}}{\lambda x.t \to_{1o} \lambda x.t'} \lambda \qquad \frac{t \to_{1o} t' \quad t \neq \lambda x.r}{nt \to_{1o} nt'} @r $$

Examples: $x(II)(II) \to_{1o} xI(II)$ but $x(II)(II) \not\to_{1o} x(II)I$ and $\delta(II)(II) \not\to_{1o} \delta(II)$.

Leftmost normal forms are simply normal forms and – crucially – leftmost reduction is normalizing, that is, if $t$ has a $\beta$-reduction $t \to_{\beta} f$ to normal form then leftmost reduction reaches that normal form, that is, $t \to_{1o} f$. For a recent simple proof of this classic result see Accattoli et al. [6].
## 7:6 Semantic Bounds and Multi Types, Revisited

$$ \frac{x: [L] \vdash x: L}{\Gamma \vdash t: L} \quad \lambda \quad \frac{\Gamma \vdash t: M \to L \quad \Delta \vdash u: M}{\Gamma \vdash \Delta \vdash tu: L} \quad @ \quad \frac{[\Gamma_i \vdash t: L_i]_{i \in I}}{\biguplus_{i \in I} \Gamma_i \vdash t: [L_i]_{i \in I}} \quad \text{many} $$

<caption>Figure 1 De Carvalho's multi type system.</caption>

# 3 Multi Types, Head Reduction, and Bounds From Type Derivations

In this section, we give our presentation of de Carvalho's system of multi types, and recall some results from the literature. In particular, we recall the characterization of head reduction, how multi types induce the relational model, and the bounds that can be extracted from type derivations for the length of head evaluations and the head size of head normal forms.

**Multi Types.** There are two layers of types, *linear* and *multi types*, built over a countably infinite set of (linear) type variables:

$$ \begin{array}{l@{\quad}l@{\quad}l} \text{LINEAR TYPE VARIABLES} & \mathit{TyVars} & := \{X, Y, Z, W, X_1, Y', Z_2, \dots\} \\ \text{LINEAR TYPES} & L, L' & ::= X \in \mathit{TyVars} \mid M \to L \\ \text{MULTI TYPES} & M, N & ::= [L_1, \dots, L_n] \quad n \in \mathbb{N} \\ \text{GENERIC TYPES} & T, T' & ::= L \mid M \end{array} $$

where $[L_1, \dots, L_n]$ is our notation for finite multisets. The empty multi type [] obtained by taking $n = 0$ is also denoted by $\mathbf{0}$. Often, multi types are presented using a single type variable $X$ instead of countably many. Most results are unaffected, but we shall see that for de Carvalho's semantic bounds we need countably many type variables.

A multi type $[L_1, \dots, L_n]$ has to be intended as a conjunction $L_1 \wedge \dots \wedge L_n$ of linear types $L_1, \dots, L_n$, for a commutative, associative, non-idempotent conjunction $\wedge$ (morally a tensor $\otimes$), of neutral element $\mathbf{0}$. The intuition is that a linear type corresponds to a single use of a term $t$, and that $t$ is typed with a multiset $M$ of $n$ linear types if it is going to be used (at most) $n$ times, that is, if $t$ is part of a larger term $u$, then a copy of $t$ shall end up in evaluation position during the evaluation of $u$.

**Typing Rules.** The derivation rules for the multi types system are in Figure 1. *Judgments* have shape $\Gamma \vdash t: M$ or $\Gamma \vdash t: L$ where $t$ is a term, $M$ is a multi type, $L$ is a linear type, and $\Gamma$ is a *type context*, that is, a total function from variables to multi types such that $\mathrm{dom}(\Gamma) := \{x \mid \Gamma(x) \neq \mathbf{0}\}$ is finite, usually represented as $x_1 : M_1, \dots, x_n : M_n$ (for some $n \in \mathbb{N}$) if $\mathrm{dom}(\Gamma) \subseteq \{x_1, \dots, x_n\}$ and $\Gamma(x_i) = M_i$ for all $1 \le i \le n$.

The abstraction rule $\lambda$ uses the notation $\Gamma \\xrightarrow{\phantom{\Gamma}} x$ for the type context defined as $\Gamma$ on every variable but possibly $x$, for which $(\Gamma \\xrightarrow{\phantom{\Gamma}} x)(x) = \mathbf{0}$. It is a compact way to express the rule in both the cases $x \in \mathrm{dom}(\Gamma)$ and $x \notin \mathrm{dom}(\Gamma)$. Note that the application rule $@$ requires the argument to be typed with a multi type $M$, which is necessarily introduced by rule *many*, the hypotheses of which are a multi set of derivations, indexed by a possibly empty set $I$. When $I$ is empty, the rule has no premises and can type every term. For instance, $\vdash \Omega: \mathbf{0}$ is derivable, but no linear type can be assigned to $\Omega$. Essentially, $\mathbf{0}$ is the type of erasable terms, and every term is erasable in the $\lambda$-calculus.

**Technicalities about Types.** The type context $\Gamma$ is empty if $\mathrm{dom}(\Gamma) = \emptyset$. *Multi-set sum* $\uplus$ is extended to type contexts point-wise, i.e. $(\Gamma \uplus \Delta)(x) := \Gamma(x) \uplus \Delta(x)$ for each variable $x$. This notion is extended to a finite family of type contexts as expected, in particular $\biguplus_{i \in J} \Gamma_i$ is the empty context when $J = \emptyset$. Given two type contexts $\Gamma$ and $\Delta$ such that
$dom(\Gamma) \cap dom(\Delta) = \emptyset$, the type context $\Gamma, \Delta$ is defined by $(\Gamma, \Delta)(x) := \Gamma(x)$ if $x \in dom(\Gamma)$, $(\Gamma, \Delta)(x) := \Delta(x)$ if $x \in dom(\Delta)$, and $(\Gamma, \Delta)(x) := 0$ otherwise. Note that $\Gamma, x: 0 = \Gamma$, where we implicitly assume $x \notin dom(\Gamma)$.

**Type Derivations.** We write $\Phi \triangleright \Gamma \vdash t: T$ if $\Phi$ is a (type) derivation (i.e. a tree constructed using the rules in Figure 1) with conclusion the multi judgment $\Gamma \vdash t: T$. In particular, we write $\Phi \triangleright \vdash t: T$ when $\Gamma$ is empty. We write $\Phi \triangleright t$ if $\Phi \triangleright \Gamma \vdash t: T$ for some type context $\Gamma$ and some type $T$.

We need a notion of size of type derivations, which shall be used to extract bounds for the number of evaluation steps and the size of normal forms.

**Definition 2 (Inner size of derivations).** Let $\Phi$ be a type derivation. The inner size $|\Phi|_{in}$ of $\Phi$ is the number of occurrences of rules $\lambda$ and $@$ in $\Phi$.

**Subject Reduction and Expansion, and Relational Semantics.** The first properties of the type system that we recall are subject reduction and expansion, which hold for every $\beta$-step.

**Proposition 3.** Let $t \to_{\beta} t'$.

1. Subject reduction: if $\Phi \triangleright \Gamma \vdash t: L$ then there is a derivation $\Phi' \triangleright \Gamma \vdash t': L$ such that $|\Phi'|_{in} \le |\Phi|_{in}$. Moreover, if $t \to_h t'$ then $|\Phi'|_{in} = |\Phi|_{in} - 2$.

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

Together, subject reduction and expansion state that type judgements are *invariants* of $\beta$-reduction. Such invariants actually induce a denotational model of the $\lambda$-calculus, its (call-by-name) *relational semantics*.

Let $t$ be a term and $x_1, \dots, x_n$ ($n \ge 0$) be pairwise distinct variables. The list $\vec{x} = (x_1, \dots, x_n)$ is suitable for $t$ if $fv(t) \subseteq \{x_1, \dots, x_n\}$. If $\vec{x} = (x_1, \dots, x_n)$ is suitable for $t$, the *relational semantics* $[[t]]_{\vec{x}}$ of $t$ for $\vec{x}$ is defined by:

$$[[t]]_{\vec{x}} := \{( (M_1, \dots, M_n), L ) | \exists \Phi \triangleright x_1 : M_1, \dots, x_n : M_n \vdash t : L \}.$$

The following property is an immediate corollary of subject reduction and expansion.

**Proposition 4 (Invariance).** Let $\vec{x} = (x_1, \dots, x_n)$ be suitable for two terms $t$ and $u$. If $t \to_{\beta} u$ then $[[t]]_{\vec{x}} = [[u]]_{\vec{x}}$.

**Characterizing Head Termination.** Note the quantitative aspect of subject reduction (Prop. 3.1), stating that the derivation size *cannot increase* after a reduction step, and that it *decreases* with head steps (of 2 because removing a head $\beta$ redex removes a $\lambda$ and a $@$ rule). It does not say that it decreases at every step because steps occurring in sub-terms typed with rule *many* might not change the size. For instance, if $xt \to xt'$ and $t$ is typed using an empty *many* rule (i.e. with 0 premises), which is a sub-derivation of size 0, then also $t'$ is typed using an empty *many* rule, of size 0. Therefore, not all typable terms terminate, as for instance $x\Omega$ is typable as follows, for any linear type $L$, but it has no normal form:

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

<footnote n="0">⁰ More precisely, such a model is the restriction of the relational model for linear logic to the image of Girard's [36] call-by-name translation $(A \Rightarrow B)^n =!A^n \to B^n$ of the intuitionistic arrow into linear logic.</footnote>
7:8 Semantic Bounds and Multi Types, Revisited

Since the size of type derivations decreases at every head step, it provides a termination measure for the head reduction of typable terms. Therefore, typable terms are head terminating – this is also called correctness of the type system (with respect to head reduction). Conversely, every head normal forms is typable. Additionally, one can show that the size of type derivations bounds the head size of head normal forms, and that there exists derivations having exactly the head size of the normal form, as in the example (1) above.

**► Proposition 5 (Typability of head normal forms).** Let $h$ be a head normal form.

1. Lax bounds for all pairs: if $\Phi \triangleright \Gamma \vdash h: L$ then $|h|_h \le |\Phi|_{in}$;

2. Existence and exact bounds: there exists a derivation $\Phi \triangleright \Gamma \vdash h: L$ such that $|h|_h = |\Phi|_{in}$.

Typability of all head normal forms (Prop. 5.2) together with subject expansion (Prop. 3.2) implies the completeness of the type system: every head terminating term is typable.

**► Theorem 6 (Typability characterizes head normalization).**

1. Correctness: if $\Phi \triangleright t$ then there exists a head normalizing evaluation $t \to^n_h h$ with $h$ normal and $2n + |h|_h \le |\Phi|_{in}$.

2. Completeness: if $t \to^n_h h$ is a head normalizing evaluation, then there exists a derivation $\Phi \triangleright t$. In particular, there is a derivation $\Phi$ for which $2n + |h|_h = |\Phi|_{in}$.

The quantitative bounds involve $2n$ rather than $n$ because every $\beta$ redex is typed in a type derivation $\Phi$ using two rules ($\lambda$ and $@$). The type derivation captures only the head size of the normal form, because in general it ignores arguments, and so it cannot catch the inner size. For instance, for the head normal form $x\Omega$ of head size $|x\Omega|_h = 1$ (but inner size $|x\Omega|_{in} = 6$) the derivation (1) has inner size 1.

The head characterization theorem implies the following property of the semantics.

**► Theorem 7 (Adequacy of relational semantics for head reduction).** Let $\vec{x} = (x_1, \dots, x_n)$ be suitable for $t$. Then $[t]_{\vec{x}}$ is non-empty if and only if $t$ is $\to_h$-normalizing.

Summing up, multi types naturally model head reduction. De Carvalho's bounds from composable types, however, rest on normal forms, which are reached by leftmost reduction, rather than on head normal forms and head reduction. Therefore, the next section recalls how multi types relate to leftmost reduction and normal forms.

4 Bounds From Derivations Via (Unitary) Shrinking

In this section, we recall how to extend the results of the previous section to leftmost reduction $\to_{1o}$ and full normal forms, via the so called shrinking constraint. We follow the presentation of Accattoli et al. [7] (removing some of the aspects of their work that are not relevant here), but the definition of shrinking judgements is standard and not due to [7], see for instance Krivine's book [44], de Carvalho [44, 27], Kesner and Ventura [40], or Bucciarelli et al. [20].

**The Need for Shrinking.** Consider the derivation of end sequent $x: [0 \to L] \vdash x\Omega: L$ in (1). Since $x\Omega$ is $\to_{1o}$-diverging, this derivation has to be excluded somehow. The problem here is that since $x$ has an erasing type – that is an arrow type with **0** on the left – then the diverging subterm $\Omega$ does not get typed. Excluding the use of **0** is too drastic, because the paradigmatic erasing term $\lambda y.x$ is normal and can be typed only with $x: [L] \vdash \lambda y.x: 0 \to L$.

The idea is that only some occurrences of **0** are dangerous. The given examples seem to suggest that if **0** occurs on the right side of $\vdash$ it is fine, while if it occurs in the typing context it is not. Things are subtler. Extending example (1) with an abstraction, one obtains the $\to_{1o}$-diverging term $\lambda x.x\Omega$ and the typing $\vdash \lambda x.x\Omega: [0 \to L] \to L$, that show that **0** can be
dangerous also on the right of $\vdash$. The dangerous occurrences of 0 turn out to be those on the left of an *even number of arrows*, considering the $\vdash$ symbols as an arrow. This is formalized by the *shrinking* constraint, which allows one to characterize leftmost termination.

**Defining Shrinking.** There are two mutually defined notions of shrinking types, *left* and *right*, the key point of which is that right multi types *cannot be empty* (note $n \ge 1$), so that 0 is forbidden on the left of top arrows $\to$ for left linear types. Their definition follows:

LEFT AND RIGHT (SHRINKING) TYPES

Right linear type $L^R$ ::= $X \in \text{TyVars} | M^L \to L^R$

Left linear type $L^L$ ::= $X \in \text{TyVars} | M^R \to L^L$

Right multi type $M^R$ ::= $[L_1^R, \dots, L_n^R] \quad n \ge 1$

Left multi type $M^L$ ::= $[L_1^L, \dots, L_n^L] \quad n \ge 0$

The notions extend to type contexts and to derivations as follows:

- A type context $x_1:M_1, \dots, x_n:M_n$ is left if each $M_i$ is left;

- A derivation $\Phi \vdash \Gamma \vdash t: L$ is shrinking if $\Gamma$ is left and $L$ is right.

For instance, $[X]$ is both left and right, while $0$ is left but not right, and $[0 \to X]$ is right but not left. Note that the derivation in (1) is not shrinking. By adding the shrinking constraint, we can now characterize leftmost normalization with multi types, with quantitative bounds involving the inner size of the normal form.

**► Theorem 8 (Shrinking typability characterizes leftmost normalization, [7]).**

1. Correctness: if $\Phi \vdash t$ is a shrinking derivation, then there exists a normalizing evaluation $t \to^{n} f$ with $f$ normal and $2n + |f|_{\text{in}} \le |\Phi|_{\text{in}}$.

2. Completeness: if $t \to_{1o}^* f$ is a normalizing evaluation, then there exists a shrinking derivation $\Phi \vdash t$.

**Unitary Shrinking.** Shrinking is enough to ensure termination, but not to capture the exact number of steps to normal form together with the exact size of the normal form. The point is somewhat dual to shrinkingness, as it concerns arguments that have to be typed, but that should not be typed *too many times*. Consider the evaluation $y(lz) \to_{1o} yz$ that involves 1 leftmost step and produces a normal form of inner size 1. The following shrinking derivation types the argument $lz$ twice (the easy derivation of $z: [X] \vdash lz: X$ of inner size 2 is omitted), instead of once, and it has size 5, instead of the required 3 (obtained as $2*1+1$):

$$ \frac{\substack{[z: [X] \vdash lz: X]_{i=1,2} \\ y: [[X,X] \to Y] \vdash y: [X,X] \to Y}}{z: [X,X] \vdash lz: [X,X]} \quad \text{ax} \quad \text{many} \quad (2) $$
$$ \frac{y: [[X,X] \to Y], z: [X,X] \vdash y(lz): Y}{[z: [X] \vdash lz: X]_{i=1,2}} \quad @ $$

To obtain exact bounds, one needs *unitary shrinking types* and *derivations*, that type arguments of normal forms only once, obtained by constraining some multi-sets – the right ones – to be singletons. The definition follows:

UNITARY LEFT AND RIGHT (SHRINKING) TYPES

Unitary right linear types $L^{UR}$ ::= $X \in \text{TyVars} | M^{UL} \to L^{UR}$

Unitary left linear types $L^{LL}$ ::= $X \in \text{TyVars} | M^{LL} \to L^{LL}$

Unitary right multi types $M^{UR}$ ::= $[L^{UR}]$

Unitary left multi types $M^{LL}$ ::= $[L_1^{LL}, \dots, L_n^{LL}] \quad n \ge 0$

The notions extend to type contexts and to derivations as expected:
7:10 Semantic Bounds and Multi Types, Revisited

A type context $x_1:M_1, \dots, x_n:M_n$ is *unitary left* if each $M_i$ is unitary left;

A derivation $\Phi \vdash \Gamma \vdash t: L$ is *unitary shrinking* if $\Gamma$ is unitary left and $L$ is unitary right.
For instance, the derivation in (2) is not unitary shrinking, because the multi type $[[X,X] \stackrel{\sim}{\to} Y]$ of $y$ is not unitary left, since $[X,X]$ is not unitary right. A derivable unitary shrinking typing for $y(lz)$ is $y : [[X] \stackrel{\sim}{\to} Y], z : [X] \vdash y(lz):Y$, obtained via a derivation of inner size 3.

The following refinement of the shrinking characterization theorem (Thm. 8) holds.

**Theorem 9** (Unitary shrinking typability measures leftmost evaluation, [7]).

1. Correctness: if $\Phi \vdash t$ is a unitary shrinking derivation, then there exists a normalizing evaluation $t \to_{l_0}^n f$ with $f$ normal and $2n + |f|_{in} = |\Phi|_{in}$.

2. Completeness: if $t \to_{l_0}^* f$ is a normalizing evaluation, then there exists a unitary shrinking derivation $\Phi \vdash t$.

**Normal Forms.** The proof of the last theorem rests on two properties of normal forms that it is useful to state explicitly, for comparison with the study of the next sections.

**Proposition 10** (Unitary shrinking derivations and normal forms, [7]). Let $f$ be normal.

1. Lax bounds: if $\Phi \vdash f$ is a shrinking derivation then $|f|_{in} \le |\Phi|_{in}$;

2. Exact bounds: there exists a unitary shrinking derivation $\Phi \vdash f$ such that $|f|_{in} = |\Phi|_{in}$.

5 Bounds from Types

In this section, we recall the bounds on the size of normal forms that can be extracted from types rather than from type derivations.

**Bounds from Types.** The types appearing in the final judgement of a shrinking derivation for $t$ bound the inner size $|f|_{in}$ of the normal form $f$ of $t$, according to a notion of type size given below, and independently of the derivation itself. For example, consider the easily derivable (unitary shrinking) derivation $\Phi \vdash \delta : [[X] \stackrel{\sim}{\to} X, X] \stackrel{\sim}{\to} X$ for $\delta = \lambda x.xx$. There are two arrows in the type (judgement) and the normal form has inner size two. Of course, one also has to take into account the arrow symbols appearing in the typing context, when present.

Note, however, that types – even unitary shrinking ones – in general do not provide exact bounds: taking the derivation of $\Phi$ for $\delta$ and substituting $X$ with $[Y] \stackrel{\sim}{\to} Y$ everywhere in $\Phi$ one obtains a unitary shrinking derivation $\Psi$ having the same size of $\Phi$ but final (still unitary shrinking) judgement:

$$ \Psi \vdash \delta : [[Y] \stackrel{\sim}{\to} Y] \stackrel{\sim}{\to} [Y] \stackrel{\sim}{\to} Y, [Y] \stackrel{\sim}{\to} Y] \stackrel{\sim}{\to} [Y] \stackrel{\sim}{\to} Y $$

which has six arrows while $|\delta|_{in} = 2$.

**Definition 11** (Type size). The size $|\cdot|$ of types and typing contexts is defined as follows:

$$ \begin{array}{lclcl} \texttt{TYPES} & |X| & := & 0 & |M \stackrel{\sim}{\to} L| & := |M| + |L| + 1 & |[L_1, \dots, L_n]| := \sum_{i=1}^{n} |L_i| \\ \texttt{TYPE CTXS} & |\epsilon| & := & 0 & |x : M; \Gamma| & := |M| + |\Gamma| & \end{array} $$

Clearly, $|T| \ge 0$ and $|M| = 0$ if and only if $M$ is a possibly empty multi set of type variables.

Given a type context $\Gamma = x_1:M_1, \dots, x_n:M_n$ we often consider the list of its types, noted $\hat{\Gamma} := (M_1, \dots, M_n)$. Since any list of multi types $(M_1, \dots, M_n)$ can be seen as extracted from a type context $\Gamma$, we use the notation $\hat{\Gamma}$ for lists of multi types. The size of a list of multi types is $|(M_1, \dots, M_n)| := \sum_{i=1}^{n} |M_i|$, and that of the conclusion of a derivation $\pi \vdash \Gamma \vdash e: L$ is $|(\hat{\Gamma}, L)| := |\hat{\Gamma}| + |L|$. Clearly, $\text{dom}(\Gamma) = \emptyset$ implies $|\hat{\Gamma}| = 0$.
**► Proposition 12** (Shrinking types bound the size of normal forms, [7]). Let $f$ be a normal form.

1. Lax bounds for all types: if $\Phi \triangleright \Gamma \vdash f:L$ is a shrinking derivation then $|f|_{in} \le |(\hat{\Gamma}, L)|$;

2. Exact bounds for special types: there exists a unitary shrinking derivation $\Phi \triangleright \Gamma \vdash f:L$ such that $|f|_{in} = |(\hat{\Gamma}, L)|$.

# 6 Dissecting Bounds From Types via Skeletons and Dry Judgements

In this section, we decompose and elaborate over the bounds on the size of normal forms extracted from types given in the previous section. The analysis is the main contribution of this paper. In particular, we develop notions and tools that shall be used in the next section to understand the issues concerning how to extract exact bounds from composable types.

**Types Bound the Size of Derivations.** The first observation is that the lax bounds of Prop. 12.1 are a consequence of the more general fact that types bound the size of derivations, proved next, together with the already proved fact that derivations bound the size of normal forms (Prop. 10). The second point of the following proposition is the main statement, the first one is an auxiliary one that is needed for the proof to go through.

**► Proposition 13** (Types bound the size of derivations for normal forms). Let $\Phi \triangleright \Gamma \vdash t:T$ be a derivation.

1. Neutral: if $t$ is a neutral term then $|\Phi|_{in} \le |\hat{\Gamma}| - |T|$.

2. Normal: if $t$ is a normal form then $|\Phi|_{in} \le |\hat{\Gamma}| + |T|$.

**Proof.** By mutual induction on the definition of neutral and normal terms, followed by an induction on the type derivation $\Phi$.

1. $t$ is a neutral term. Cases of the last rule:

- Rule many. Then $T$ is a multi type $M = [L_i]_{i \in I}$ and the last rule is necessarily many. So, necessarily, for some finite set of indices $I$,

$$ \Phi = \frac{[ \Phi_i \triangleright \Gamma_i \vdash t:L_i ]_{i \in I}}{\psi_{i \in I} \Gamma_i \vdash t:[L_i]_{i \in I}} \text{ many} $$

where $\Gamma = \psi_{i \in I} \Gamma_i$. By i.h. (on $\Phi_i$), $|\Phi_i|_{in} \le |\hat{\Gamma}_i| - |L_i|$, thus $|\Phi|_{in} = \sum_{i \in I} |\Phi_i|_{in} \le \sum_{i \in I} |\hat{\Gamma}_i| - \sum_{i \in I} |L_i| = |\hat{\Gamma}| - |M|$.

- Rule ax, that is, $t = x$. Then:

$$ \Phi = \overline{x:[L] \vdash x:L}^{\text{ax}} $$

where $T = L$ and $\Gamma = x:[L]$. Since $|\Phi|_{in} = 0$ and $|T| = |L| = |[L]| = |\hat{\Gamma}|$, then $|\Phi|_{in} = 0 = |\hat{\Gamma}| - |T|$.

- Rule @, that is, $t = nf$. Then necessarily:

$$ \Phi = \frac{\Phi_n \triangleright \Delta \vdash n:N \sim L \quad \Phi_f \triangleright \Sigma \vdash f:N}{\Delta \psi \Sigma \vdash nf:L} @ $$

where $T = L$ and $\Gamma = \Delta \psi \Sigma$. By i.h. (on the definition of neutral terms and normal forms), $|\Phi_n|_{in} \le |\hat{\Delta}| - |N \sim L| = |\hat{\Delta}| - |N| - |L| - 1$ and $|\Phi_f|_{in} \le |\hat{\Sigma}| + |N|$. Therefore,

$$ \begin{align*} |\Phi|_{in} &= |\Phi_n|_{in} + |\Phi_f|_{in} + 1 & \le_{i.h.} & |\hat{\Delta}| - |N| - |L| - 1 + |\Phi_f|_{in} + 1 \\ &= |\hat{\Delta}| - |N| - |L| + |\Phi_f|_{in} & \le_{i.h.} & |\hat{\Delta}| - |N| - |L| + |\hat{\Sigma}| + |N| \\ &= |\hat{\Delta}| + |\hat{\Sigma}| - |L| & = & |\hat{\Gamma}| - |T|. \end{align*} $$
7:12 Semantic Bounds and Multi Types, Revisited

2. *t is a normal form.* If *t* is a neutral term, then the statement follows from Point 1, which stronger than the statement that we need to prove. Otherwise, *t* is an abstraction. If the last rule is many then we reason exactly as for neutral terms. The remaining cases is when the last rule is *λ*, that is, *t = λx.f* and *Φ* is necessarily of the form:

$$ \frac{\Phi' \succ \Delta \vdash f : L'}{\Delta \Vdash x \vdash \lambda x.f : \Delta(x) \dashv L'} \lambda $$

where $\mathbf{T} = \Delta(x) \dashv L'$ and $\mathbf{\Gamma} = \Delta \Vdash x$. By i.h.,

$$ |\Phi'|_{\text{in}} \leq_{i.h.} |\hat{\Delta}| + |L'| = |\Delta \Vdash x| + |\Delta(x)| + |L'| = |\Delta \Vdash x| + |\Delta(x) \dashv L'| - 1 $$

Therefore,

$$ \begin{align*} |\Phi|_{\text{in}} &= |\Phi'|_{\text{in}} + 1 & \leq & |\Delta \Vdash x| + |\Delta(x) \dashv L'| - 1 + 1 \\ &= |\Delta \Vdash x| + |\Delta(x) \dashv L'| & = & |\hat{\Gamma}| + |\mathbf{T}|. \end{align*} \quad \blacksquare $$

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

Note that the bound holds for every derivation, without requiring them to be shrinking. This fact means that the connection between types and derivations is stronger than the one between derivations and normal forms. Note also that the bound does not hold for head normal forms, as can be seen by inspecting examples (1) (p. 7) and (2) (p. 9).

**Exact Bounds from Types.** We now turn our attention to exact bounds. Having showed that bounds for normal forms factor through bounds for derivations (Prop. 13), we actually turn to exact bounds for derivations, from types. The idea, as usual, is that exact bounds are given by types of minimal size. To describe such minimal types we shall use a modified *dry* typing system for normal forms related to principal judgements, that shall derive only minimal types. Additionally, we use a relation between derivations having the same structure but assigning possibly different types, also considered by de Carvalho.

**Skeleton Equivalence.** We formalize the notion of derivations having the same skeleton, that is, the same *mute* structure. Skeleton equivalence ~ relates derivations having the same rules arranged in the same way, but not necessarily having the same types.

► **Definition 14 (Skeleton equivalence).** Let *t* be a term. Two derivations $\Phi \succ t$ and $\Psi \succ t$ are skeleton equivalent, noted $\Phi \sim \Psi$, if they end with the same kind of rule and the derivations on the premises are $\sim$-equivalent, namely they fall in one of the following cases:

- Both $\Phi$ and $\Psi$ are axioms.

- Both $\Phi$ and $\Psi$ end with rule @, their two left premises $\Phi_l$ and $\Psi_l$ satisfy $\Phi_l \sim \Psi_l$, and their right premises $\Phi_r$ and $\Psi_r$ satisfy $\Phi_r \sim \Psi_r$ - similarly for rules $\lambda$.

- Both $\Phi$ and $\Psi$ end with a rule many with $n$ premises and there is a permutation $\rho$ of $\{1, \dots, n\}$ such that the $i$-th premise $\Phi_i$ of $\Phi$ and the $\rho(i)$-th premise $\Psi_{\rho(i)}$ of $\Psi$ satisfy $\Phi_i \sim \Psi_{\rho(i)}$ for $i \in \{1, \dots, n\}$.

The next lemma shows that skeleton equivalence preserves more or less everything one can imagine, but types. We denote by $\#m$ the cardinality of a multiset $m$.

► **Lemma 15 (Skeletal invariants).** Let $\Phi \succ \Gamma \vdash t : \mathbf{T}$ and $\Psi \succ \Delta \vdash t : \mathbf{T}'$ be two derivations such that $\Phi \sim \Psi$. Then $|\Phi|_{\text{in}} = |\Psi|_{\text{in}}$, $\text{dom}(\Gamma) = \text{dom}(\Delta)$, $\#(\Gamma(x)) = \#(\Delta(x))$ for every variable $x$, and $\mathbf{T}$ is a multi type if and only if $\mathbf{T}'$ is, and in that case $\#\mathbf{T} = \#\mathbf{T}'$. Moreover, $\Phi$ is shrinking (resp. unitary shrinking) if and only if $\Psi$ is.

**Proof.** Straightforward induction on $\Phi$. ▼

<figure><img src="image_6.png" /></figure>
<figure><img src="image_7.png" /><figcaption>Figure 2 Dry multi type system for normal forms.</figcaption></figure>

**Principal and Dry Judgements.** Simple types admits *principal judgements* (or *typings*), that is, for every term $t$ there exists a principal judgement $\Gamma \vdash t : A$ such that for every other judgement $\Delta \vdash t : B$ for $t$ there exists a type substitution $\sigma$ such that $\Gamma \sigma = \Delta$ and $A \sigma = B$. Multi types do not have principal judgements, since there is no *single* judgement for a term that subsumes all others *up to substitutions*. The literature has studied a weakened notion of principal judgement, subsuming all judgements up to substitution and up to another (very technical) operation called *expansion*, which – roughly – duplicates multi sets [22, 50, 43].

What we are going to do next, intuitively, is following the other natural route when principal judgements do not exist: we study a notion of principal *set* of special judgements for a term $t$, called *dry* judgements, which are such that every ordinary judgement for $t$ can be seen as a dry judgement up to substitution. In fact, we only study this property for normal forms, and we also relate the derivations producing those judgements. We need some definitions.

**Supports and Substitutions.** The *support* of a type derivation $\Phi \triangleright \Gamma \vdash t : \mathbf{T}$ is the set $\text{TyVars}(\Phi) := \{\mathbf{X} \mid \mathbf{X} \text{ occurs in } \Phi\}$ of type variables appearing in $\Phi$, and the *final support* is the set $\text{TyVarsF}(\Phi) := \{\mathbf{X} \mid \mathbf{X} \text{ occurs in } \Gamma \text{ or } \mathbf{T}\}$ of type variables appearing in the last judgement of $\Phi$. We write $\Phi \# \Psi$ as a shortcut for $\text{TyVars}(\Phi) \cap \text{TyVars}(\Psi) = \emptyset$ and given $\{\Phi_i\}_{i \in I}$ we write $\#_{i \in I} \Phi_i$ when $\text{TyVars}(\Phi_h) \cap \text{TyVars}(\Phi_k) = \emptyset$ for any two distinct $h, k \in I$.

A type substitution $\sigma$ is a function from type variables to linear types that is the identity but a for finite number of type variables. It is extended to act on types, multi types, type contexts, and derivations as expected.

**Dry Judgements.** Dry judgements for normal forms are derived using the rules in Fig. 2. There are three key points. Firstly, only normal forms are typable. Secondly, neutral terms are always typed with a type variable (which is minimal) and when they are applied (in rule @*) their type is *enlarged* on-the-fly via a type substitution $\{\mathbf{X} \leftarrow (\mathbf{M} \dashv \mathbf{Y})\}$ depending on the type of the argument. Thirdly, the system uses many type variables, and for the rules with more than one premise (i.e. @* and many*) it requires them to have disjoint supports. This is where having countably many type variables plays a role, as having only a finite number would not allow one to prove the *subsumption up to substitutions* property of dry derivations, given by Thm. 19.2 below.

Dry derivations can be seen as standard derivations, as the second point of the next lemma states. It is obtained using the straightforward fact that standard derivations are stable by type substitutions. Note the use of skeleton equivalence.

**► Lemma 16.** Let $t$ be a term and $f$ be a normal form.

1. Substitutivity for standard: if $\Phi \triangleright \Gamma \vdash t : \mathbf{L}$ then for any linear type $\mathbf{L}'$ there exists $\Phi_{\{\mathbf{X} \leftarrow \mathbf{L}'\}} \triangleright \Gamma \{\mathbf{X} \leftarrow \mathbf{L}'\} \vdash t : \mathbf{L} \{\mathbf{X} \leftarrow \mathbf{L}'\}$ such that $\Phi \sim \Phi_{\{\mathbf{X} \leftarrow \mathbf{L}'\}}$.

2. Dry derivations are standard: if $\Phi \triangleright \Gamma \vdash^d f : \mathbf{L}$ then there exists $\Psi \triangleright \Gamma \vdash f : \mathbf{L}$ such that $\Phi \sim \Psi$.
7:14 Semantic Bounds and Multi Types, Revisited

**Proof.** The first point is a straightforward induction on $\Phi$. The second point is by induction on $\Phi$. The only rule of the dry system that is not a rule of the standard system is @*:

$$ \frac{\Phi_n \triangleright \Gamma_n \vdash^d n : \mathbf{X} \quad \Phi_{f'} \triangleright \Gamma_{f'} \vdash^d f' : \mathbf{M} \quad \mathbf{Y} \text{ fresh}, \Phi \ \# \ \Psi}{\Gamma_n \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \uplus \Gamma_{f'} \vdash^d nf' : \mathbf{Y}} @^* $$

with $f = nf'$, $\Gamma = \Gamma_n \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \uplus \Gamma_{f'}$, $T = \mathbf{Y}$. By i.h., there exist $\Psi_n \triangleright \Gamma_n \vdash n : \mathbf{X}$ and $\Psi_{f'} \triangleright \Gamma_{f'} \vdash f' : \mathbf{M}$. By Point 1, there exists a derivation: $\Psi_n \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \triangleright \Gamma_n \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \vdash n : \mathbf{M} \to \mathbf{Y}$. Then we build $\Psi$ as follows:

$$ \frac{\Psi_n \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \triangleright \Gamma_n \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \vdash n : \mathbf{M} \to \mathbf{Y} \quad \Psi_{f'} \triangleright \Gamma_{f'} \vdash f' : \mathbf{M}}{\Gamma_n \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \uplus \Gamma_{f'} \vdash nf' : \mathbf{Y}} @ $$

Skeleton equivalence of $\Phi$ and $\Psi$ follows immediately from the skeleton equivalences of the i.h. plus the one of Point 1. ▼

Next, we prove that types in dry judgements are always minimal and – crucially – capture the size of the derivation itself. This is obtained via a strong property for type variables in dry judgements, reminiscent of similar properties in multiplicative linear logic, and enforced by the requirements about disjoint supports in the derivation rules.

**Proposition 17.** Let $f$ be a normal form.

1. Dry derivations and variable types occurrences: if $\Phi \triangleright \Gamma \vdash^d f : T$ then $X$ has exactly two occurrences in $(\Gamma, T)$ for every $X \in \text{TyVarsF}(\Phi)$.

2. Dry derivations are minimal: if $\Phi \triangleright \Gamma \vdash^d f : L$ then $|\Phi|_{in} = |(\hat{\Gamma}, L)|$.

**Proof.**

1. By induction on $\Phi$, looking at its last rule. For ax*, the statement evidently holds, and for $\lambda^*$ and rule many* it follows from the i.h., since these rules preserve and do not introduce occurrences of type variable. If the last rule of $\Phi$ is @*, then $\Phi$ has shape:

$$ \Phi = \frac{\Phi_1 \triangleright \Delta \vdash^d n : \mathbf{X} \quad \Phi_2 \triangleright \Sigma \vdash^d f' : \mathbf{M} \quad \mathbf{Y} \text{ fresh}, \Phi \ \# \ \Psi}{\Delta \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \uplus \Sigma \vdash^d nf' : \mathbf{Y}} @^* $$

with $f = nf'$, $T = \mathbf{Y}$, and $\Gamma = \Delta \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \uplus \Sigma$. By i.h., $X$ occurs exactly once in $\Delta$, thus $Y$ occurs exactly twice in $(\Gamma, T)$. Note that $\text{TyVarsF}(\Phi) = (\text{TyVarsF}(\Phi_1) \setminus \{X\}) \cup \text{TyVarsF}(\Phi_2) \cup \{Y\}$. By i.h., each type variable in $\text{TyVarsF}(\Phi_1) \setminus \{X\}$ (resp. $\text{TyVarsF}(\Phi_2)$) occurs exactly twice in $\Delta$ (resp. $(\Sigma, M)$). Moreover, by hypothesis $\text{TyVars}(\Phi_1) \cap \text{TyVars}(\Phi_2) = \emptyset$, so each such type variable occurs exactly twice in $(\Gamma, T)$.

2. By induction on $\Phi$, looking at its last rule. Cases:

- Rule ax*: the statement holds because $|\Phi|_{in} = 0 = |([X], X)|$.

- Rule many*: it follows from the i.h.

- Rule $\lambda^*$: it follows from the i.h. because rule $\lambda^*$ add 1 to the size of the derivation, but the size of the judgement also grows of 1, because of the introduced arrow.

- Rule @*: then $\Phi$ has the following shape:

$$ \frac{\Phi_1 \triangleright \Delta \vdash^d n : \mathbf{X} \quad \Phi_2 \triangleright \Sigma \vdash^d f : \mathbf{M} \quad \mathbf{Y} \text{ fresh}, \Phi \ \# \ \Psi}{\Delta \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \uplus \Sigma \vdash^d nf : \mathbf{Y}} @^* $$

with $\Gamma = \Delta \{\mathbf{X} \leftarrow (\mathbf{M} \to \mathbf{Y})\} \uplus \Sigma$. By Point 1, $X$ occurs exactly once in $\Delta$. Then we have:

$$ \begin{align*} |\Phi|_{in} &= |\Phi_1|_{in} + |\Phi_2|_{in} + 1 &&=_{i.h.} |\Delta| + |\Sigma| + |M| + 1 \\ &= |\Delta| + |\Sigma| + |M \to Y| &&=_{P.1} |\Delta\{X \leftarrow (M \to Y)\}| + |\Sigma| \\ &= |\Delta\{X \leftarrow (M \to Y)\}| + |\Sigma| + |Y| \end{align*} $$

◀
**Dry Representation.** We now prove the key property of the analysis, which also justifies seeing dry derivations as defining a set of principal judgements. The idea is that every (standard) derivation $\Phi$ admits a dry derivation $\Psi$ that is skeleton equivalent to $\Phi$ – which by the skeletal invariants above entails that they have the same size – and such that there is a substitution turning $\Psi$ into $\Phi$. We need an auxiliary lemma that shall also be useful in the next section, about renamings of dry derivations.

**Lemma 18 (Dry derivations are stable by renaming).** Let $\Phi \triangleright \Gamma \vdash^d f : T$ be a dry type derivation $\text{TyVars}(\Phi) = \{X_1, \dots, X_n\}$ and $Y_1, \dots, Y_n$ be distinct type variables $\Phi$. Then the derivation $\Phi_{\{X_1, \dots, X_n \leftarrow Y_1, \dots, Y_n\}}$ obtained by simultaneously replacing $X_i$ with $Y_i$ in $\Phi$ for $i \in \{1, \dots, n\}$ is a dry type derivation such that $\Phi \sim \Phi_{\{X_1, \dots, X_n \leftarrow Y_1, \dots, Y_n\}}$.

**Proof.** Straightforward induction on $\Phi$.

**Theorem 19.** Let $f$ be a normal form and $\Phi \triangleright \Gamma \vdash f : T$ be a type derivation.

1. Dry representation: there exists a dry derivation $\Psi \triangleright \Delta \vdash^d f : T'$ such that $\Phi \sim \Psi$;

2. Type substitution: there exists a type substitution $\sigma$ such that $\Delta\sigma = \Gamma$ and $T'\sigma = T$.

**Proof.** By induction on $\Phi$. Cases of the last rule:

- Rule ax. Then $\Phi$ is a ax rule of conclusion $x: [L] \vdash x:L$. The dry representation $\Psi$ of $\Phi$ is an ax rule of conclusion $x: [X] \vdash^d x:X$. The type substitution of the statement is $\{X \leftarrow L\}$.

- Rule $\lambda$: it follows by the i.h.

- Rule many: it follows by the i.h. Note that, by stability of dry derivations under renaming (Lemma 18), we can assume that all the derivations $\Psi_i$ given by the i.h. are on disjoint supports, so that the constraint $\#i \in I \Psi_i$ for rule many* is satisfied.

- Rule @: then $f = nf'$ and $\Phi$ has the following shape:

$$ \frac{\Phi_n \triangleright \Gamma_n \vdash n : M \sim L \qquad \Phi_{f'} \triangleright \Gamma_{f'} \vdash f' : M}{\Gamma_n \uplus \Gamma_{f'} \vdash n f' : L} @ $$

with $\Gamma = \Gamma_n \uplus \Gamma_{f'}$ and $T = L$. About the dry representation, by i.h. there are dry derivations $\Psi_n \triangleright \Delta_n \vdash^d n : X$ and $\Psi_{f'} \triangleright \Delta_{f'} \vdash^d f' : N$ such that $\Phi_n \sim \Psi_n$ and $\Phi_{f'} \sim \Psi_{f'}$. By stability of dry derivations under renaming (Lemma 18), we can assume that $\Psi_n \# \Psi_n$. Then $\Psi$ is obtained as follows:

$$ \frac{\Psi_n \triangleright \Delta_n \vdash^d n : X \qquad \Psi_{f'} \triangleright \Delta_{f'} \vdash^d f' : N \qquad Y \text{ fresh, } \Psi_n \# \Psi_n}{\Delta_n \{X \leftarrow (N \sim Y)\} \uplus \Delta_{f'} \vdash^d n f' : Y} @^* $$

About the type substitution, by i.h., there are substitutions $\sigma_n$ and $\sigma_{f'}$ such that $\Delta_n \sigma_n = \Gamma_n$ and $X\sigma_n = M \sim L$, and $\Delta_{f'} \sigma_{f'} = \Gamma_{f'}$ and $N\sigma_{f'} = M$. We can assume that $\text{dom}(\sigma_n) = \text{dom}(\Delta_n)$ and $\text{dom}(\sigma_{f'}) = \text{dom}(\Delta_{f'})$, and we know that $\text{dom}(\sigma_n) \cap \text{dom}(\sigma_{f'}) = \emptyset$. Define the substitution $\sigma$ as $\sigma_n$ on $\text{dom}(\sigma_n) \setminus \{X\}$, as $\sigma_{f'}$ on $\text{dom}(\sigma_{f'})$, and as $\{Y \leftarrow L\}$ on $Y$. Note that $\sigma_n(X) = M \sim L$ and let $\sigma'_n$ be $\sigma_n$ without $\{X \leftarrow (M \sim L)\}$. Then:

$$ \begin{align*} (\Delta_n\{X \leftarrow (N \sim Y)\} \uplus \Delta_{f'})\sigma &= \Delta_n\sigma'_n\{X \leftarrow (N\sigma_{f'} \sim Y\{Y \leftarrow L\})\} \uplus \Delta_{f'}\sigma_{f'} \\ &= \begin{aligned}[t] \text{i.h.} \quad \Delta_n\sigma'_n\{X \leftarrow (M \sim L)\} \uplus \Gamma_{f'} \end{aligned} \\ &= \Delta_n\sigma_n \uplus \Gamma_{f'} = \text{i.h.} \quad \Gamma_n \uplus \Gamma_{f'} = \Gamma \end{align*} $$

and $Y\sigma = Y\{Y \leftarrow L\} = L = T$.

◀
**Removing Substitutions.** In the previous theorem, the substitution part rests on the properties of dry derivations enabled by the countable number of type variables in the type system. We now show that a slightly weaker result is possible even with only one type variable and without dry derivations. The type substitution part shall not be recoverable, but the representation and the quantitative bounds are.

Let $\Gamma \vdash^1 t: L$ denote a (standard) type derivation built using only 1-types, that is, types built using a single fixed type variable $X$.

**Theorem 20 (Size representation).** Let $f$ be a normal term and $\Phi \triangleright \Gamma \vdash f: L$ be a derivation. Then there exists a derivation $\Psi \triangleright \Delta \vdash^1 f: L'$ such that $\Psi \sim \Phi$ and $|\Psi|_{in} = |\hat{\Delta}| + |L'|$.

The proof of the theorem in fact requires a stronger statement for the induction to go through, in particular having a separate point about neutral terms, for which a stronger property holds. See the technical report [1].

7 Bounds From Composable Types

In this section, we finally study bounds from composable types for leftmost evaluation and normal forms, which is the technical and neglected part of de Carvalho's work. To ease the study, we restrict to closed terms, so that type contexts disappear – de Carvalho does the same. There are however no issues in dealing with open terms.

**Composable Types.** De Carvalho's idea is that, given two normal forms $t$ and $u$, one can extract bounds for $tu$ by looking only at the types of $t$ and $u$ – that is, at $[[t]]$ and $[[u]]$ – because a derivation for $tu$ is just the application of a derivation for $t$ and one for $u$. We need to give a formal status to composable types, and we also need a notion of types that compose up to a type substitution.

**Definition 21 (Composable pairs).** Let $t$ and $u$ be closed terms.

- $A$ (shrinking) composable pair (of types) for $t$ and $u$ is a pair $p = (L, M)$ such that $L = M \dashv^o L' \in [[t]]$, $M \in [[u]]$, and $L'$ is right. The set of composable pairs of $t$ and $u$ is noted $\text{ShComPairs}(t, u)$.

- $A$ (shrinking) composable pair up to substitution for $t$ and $u$ is a pair $p = (L, M)$ such that there exists a type substitution $\sigma$ such that $(L\sigma, M\sigma) \in \text{ShComPairs}(t, u)$. The set of composable pairs up to substitution of $t$ and $u$ is noted as $\text{ShComPairsSub}(t, u)$.

Note that if $(M \dashv^o L', M) \in \text{ShComPairs}(t, u)$ only $L'$ is required to be a right shrinking type (as it is the only type in the judgement for $tu$ after composition), while $M \dashv^o L'$ might very well not be a right shrinking type (if $M$ is not left). The constraint that $L'$ is right in the definition of $\text{ShComPairs}(t, u)$ ensures the following property.

**Lemma 22 (Normalization and composable types).** Let $t$ and $u$ be closed terms. Then $tu \to_{1o} \text{-normalizes if and only if } \text{ShComPairs}(t, u) \neq \emptyset$.

**Proof.** If $tu$ normalizes then by shrinking completeness (Thm. 8) there exists a shrinking derivation $\Phi \vdash^1 tu: L$ with $L$ right. The last rule of $\Phi$ is @ and its premises give a composable pair $(M \dashv^o L, M)$ for $t$ and $u$, for some $M$. Therefore, $\text{ShComPairs}(t, u) \supset \{(M \dashv^o L, M)\} \neq \emptyset$.

Vice versa, if $\text{ShComPairs}(t, u) \neq \emptyset$ then every composable pair induces a shrinking derivation for $tu$, by connecting the two derivations producing the composable pair via rule @. Thus, $tu$ is typable. By shrinking correctness (Thm. 8), $tu$ is $\to_{1o}$-normalizing. $\quad \blacksquare$
**Normal Forms and Composable Types.** To warm up, we first show how to bound the size of normal forms from composable pairs.

**► Theorem 23 (Normal form bounds from composable types).** Let $t$ and $u$ be closed terms such that there is a normalizing evaluation $d: tu \to_{l_0}^* f$.

1. Lax bounds: $|f|_{in} \le |L|$ for every composable pair $(M \to L, M) \in \text{ShComPairs}(t, u)$.

2. Exact bounds from special pairs: moreover, there exists a composable pair $(M \to L, M) \in \text{ShComPairs}(t, u)$ such that $|f|_{in} = |L|$.

**Proof.**

1. Let $(M \to L, M) \in \text{ShComPairs}(t, u)$ be a composable pair. Then, there are derivations $\Phi_t \vdash t: M \to L$ and $\Phi_u \vdash u: M$. We compose them as a derivation $\Phi$ for $tu$ via rule @:

$$ \Phi := \frac{\Phi_t \vdash t: M \to L \quad \Phi_u \vdash u: M}{\vdash tu: L} @ $$

Note that the definition of composable pair guarantees that $L$ is right (shrinking), so that $\Phi$ is shrinking. By shrinking correctness (Thm. 8), there is a derivation $\vdash f: L$. Since shrinking types bound the size of normal forms (Prop. 12), $|f|_{in} \le |L|$.

2. By Prop. 12.2, there exists a unitary shrinking derivation $\Psi \vdash f: L$ for $f$ such that $|L| = |f|_{in}$. Pulling back the final judgement of $\Psi$ using subject expansion (Prop. 3.2), we obtain a derivation $\Theta \vdash tu: L$. The last rule of $\Theta$ is @ and its premises give a composable pair $(M \to L, M)$ for $t$ and $u$, for some $M$. ◀

**Lax Evaluation Bounds from Composable Types.** Now, we study how to additionally extract (bounds on) the number of leftmost step from a composable pair. Obtaining lax bounds is easy. The idea is that the composed type bounds the size of a derivation for $tu$, which in turns provides bounds about $tu$, as shown in Sect. 4. We also show that even composable pairs up to substitution yield bounds.

**► Theorem 24 (Lax bounds from composable types).** Let $f$ and $f'$ be closed normal terms such that $d: ff' \to_{l_0}^* f''$ with $f''$ normal. Then:

1. Lax bounds and types: $2|d| + |f''|_{in} \le |L| + |M| + 1$ for every composable pair $(L, M) \in \text{ShComPairs}(f, f')$.

2. Lax bounds and types, up to substitutions: $2|d| + |f''|_{in} \le |L| + |M| + 1$ for every composable pair up to substitution $(L, M) \in \text{ShComPairsSub}(f, f')$.

**Proof.**

1. Let $(L, M) \in \text{ShComPairs}(f, f')$ be a composable pair, which implies $L = M \to L'$ for some right $L'$. Then, there are two derivations $\Phi_f \vdash f: M \to L'$ and $\Phi_{f'} \vdash f': M$. We compose them via a @ rule into a derivation $\Phi$ for $ff'$:

$$ \Phi := \frac{\Phi_f \vdash f: M \to L' \quad \Phi_{f'} \vdash f': M}{\vdash ff': L'} @ $$

By definition of composable pair, $L'$ is right shrinking, so that $\Phi$ is shrinking. By shrinking correctness (Thm. 8), $2|d| + |f''|_{in} \le |\Phi|_{in} = |\Phi_f|_{in} + |\Phi_{f'}|_{in} + 1$. Now, since types bound the size of the derivation for normal terms (Prop. 13), we obtain $|\Phi_f|_{in} \le |M \to L'|$ and $|\Phi_{f'}|_{in} \le |M|$. Therefore, $2|d| + |f''|_{in} \le |\Phi|_{in} \le |M \to L'| + |M| + 1$, as required.

2. Let $(L, M) \in \text{ShComPairsSub}(f, f')$ be a composable pair up to substitution, which implies that there exist a type substitution $\sigma$ such that $L\sigma = N \to L'$, $M\sigma = N$ for some right $L'$ and some $N$. Then, there are two derivations $\Phi_f \vdash f: L$ and $\Phi_{f'} \vdash f': M$. By
7:18 Semantic Bounds and Multi Types, Revisited

<figure><img src="image_8.png" /><figcaption>Figure 3 Unitary shrinking derivation $\Psi_{\delta l}$ of minimal type for $\delta l$, where $W^2 := [W] \dashv W$.</figcaption></figure>

Lemma 16.1, applying $\sigma$ to $\Phi_f$ and $\Phi_{f'}$ we obtain two derivations $\Psi_f \triangleright \vdash f:N \dashv L'$ and $\Psi_{f'} \triangleright \vdash f':N$ such that $\Phi_f \sim \Psi_f$ and $\Phi_{f'} \sim \Psi_{f'}$. We compose them via a @ rule into a derivation $\Psi$ for $ff'$:

$$ \Psi := \frac{\Psi_f \triangleright \vdash f:N \dashv L' \quad \Psi_{f'} \triangleright \vdash f':N}{\vdash f f':L'} @ $$

Since $L'$ is right, $\Psi$ is shrinking. By shrinking correctness (Thm. 8), $2|d| + |f''|_{in} \le |\Psi|_{in} = |\Psi_f|_{in} + |\Psi_{f'}|_{in} + 1$. By the skeletal invariants (Lemma 15), we obtain $|\Psi_f|_{in} + |\Psi_{f'}|_{in} + 1 = |\Phi_f|_{in} + |\Phi_{f'}|_{in} + 1$. Since types bound the size of the derivation for normal terms (Prop. 13), $|\Phi_f|_{in} \le |L|$ and $|\Phi_{f'}|_{in} \le |M|$. Therefore, $2|d| + |f''|_{in} \le |L| + |M| + 1$, as required. ◀

Note that the hypotheses for bounding evaluation lengths are stronger than for bounding normal forms (Thm. 23), as the two applied terms $f$ and $f'$ are required to be normal. If the two composed terms are not normal, then there is no way to measure the extra steps to their normal forms using their types, because types are invariant by reduction. The stronger hypotheses limit the scope of the result: if $t := \lambda x.x \Omega f$ with $f$ normal and $u := \lambda y.\lambda z.z$ then $tu \to_{1o} f$ and Thm. 23 can be applied, while Thm. 24 cannot, because of the diverging $\Omega$ sub-term in $t$.

**Exact Bounds from Composable Types.** Now, the tricky point is how to obtain *exact* bounds. The problem is that for the application of two normal terms $f$ and $f'$, the minimal composable pair in general does *not* provide exact bounds, and – dually – minimal types for $f$ and $f'$ do *not* compose. The following example pinpoints the subtleties.

**Key Example.** Consider the unitary shrinking derivations $\Phi_\delta$ and $\Phi_I$ of minimal types for $\delta := \lambda x.xx$ and for $I := \lambda y.y$:

$$ \Phi_{\delta} = \frac{\overline{x: [[Z] \dashv Z] \vdash x: [Z] \dashv Z}^{\text{ax}} \quad \overline{x: [Z] \vdash x: Z}^{\text{ax}} @}{\overline{x: [[Z] \dashv Z, Z] \vdash x x: Z}^{\text{ax}} \quad \overline{\vdash \lambda x.x x: [[Z] \dashv Z, Z] \dashv Z}^{\text{ax}}} \quad \Phi_I = \frac{\overline{y: [W] \vdash y: W}^{\text{ax}}}{\overline{\vdash \lambda y.y: [W] \dashv W}^{\text{ax}}} \lambda $$

Note that, pleasantly, $|\Phi_\delta|_{in} = 2 = |[[Z] \dashv Z, Z] \dashv Z| = |\delta|_{in}$, and $|\Phi_I|_{in} = 1 = |[W] \dashv W| = |I|_{in}$. Now, consider the application $\delta l$. Note that, unfortunately, the two obtained minimal types do *not* compose, and not just because they use different type variables: identifying $Z$ and $W$ would not be enough, one actually needs to identify $Z$ with $W^2 := [W] \dashv W$. The unitary shrinking derivation $\Psi_{\delta l}$ for $\delta l$ with minimal types (which provides exact information for $\delta l$) obtained in this way is in Fig. 3. Note that its sub-derivations $\Psi_\delta$ and $\Psi_I$ for $\delta$ and $I$ do *not* derive minimal types. The derivation $\Psi_{\delta l}$ indeed is obtained by composing:

1. The variant $\Psi_\delta$ of $\Phi_\delta$ which has the same exact structure of $\Phi_\delta$ and where every occurrence of $Z$ has been replaced by $W^2$, obtaining the type $[[[W^2] \dashv W^2, W^2]] \dashv W^2$,
2. With $\Psi_I$, which puts together two derivations for $I$, one being $\Phi_I$ (of type $W^2$), and one being the variant $\Phi'_I$ of $\Phi_I$ (of type $[W^2] \dashv W^2$) where $W$ has been replaced by $W^2$. Note that there is a gap between:

- The length of the evaluation $d : \delta I \to_{I_0} II \to_{I_0} I$, that takes 2 steps, plus the size of the normal form $||I_{in}| = 1$, so that $2|d| + ||I_{in}| = 5$, and

- The size of the composable pair $p = ([Z^2] \dashv Z^2, Z^2] \dashv Z^2, [[Z^2] \dashv Z^2, Z^2])$, which is 10. The point is that the types derived by $\Psi_\delta$ and $\Psi_I$ are not minimal, so their sizes are bigger than $|\Psi_\delta|_{in}$ and $|\Psi_I|_{in}$, and do not provide exact bounds for $\delta I$. For instance, the size of $[[W^2] \dashv W^2, W^2] \dashv W^2$, which is the type of $\Psi_\delta$, is 6, while $|\Psi_\delta|_{in} = 2$ – this is an instance of the mentioned gap. Summing up, minimal types do not compose, and composable types do not give exact bounds.

**Out of the Impasse.** De Carvalho solves this cul-de-sac using composable pairs up to substitution. With respect to our example, he considers the composable pair $p$ given by $\Psi$, but computes the bound using the pair $p' = ([Z] \dashv Y, Z] \dashv Y, [[X] \dashv X, [X'] \dashv X'])$, which is minimal and non-composable. It is obtained by collecting the types of the dry version of $\Psi_\delta$ (of type $[[Z] \dashv Y, Z] \dashv Y$) and the dry version of $\Psi_I$ (typing $I$ twice thus having type $[[X] \dashv X, [X'] \dashv X'$]). The last bit is noting that $p'$ is composable up to the substitution $\sigma := \{Z \dashv W^2\} \{Y \dashv W^2\} \{X \dashv W^2\} \{X' \dashv W\}$, since $p'\sigma = p$.

Roughly, for minimal types to compose, they usually have to be expanded, as we have done in the example when substituting $Z$ with $W^2$. Such an expansion introduces some noise in the measures, so that even minimal composable pairs might not provide exact bounds. De Carvalho's trick is to reverse the expansion, considering composable pairs up to substitution. Our notion of dry derivation makes the expansion reversal technically clean.

**Main Result.** We can now prove the main result of the paper, namely de Carvalho's exact bounds from composable types.

**► Theorem 25 (Exact bounds from composable types).** Let $f$ and $f'$ be normal. If $d : ff' \to_{I_0}^* f''$ and $f''$ is normal. Then:

1. Exact bounds: there exist $L \in [f]$ and $M \in [f']$ such that $2|d| + |f''|_{in} = |L| + |M| + 1$, and $L$ and $M$ are obtained by drying the composable pair induced by a unitary shrinking derivation for $ff'$.

2. From types composable up to substitution: moreover, $(L, M)$ are composable up to substitution, that is, $(L, M) \in \text{ShComPairsSub}(f, f')$.

**Proof.**

1. By unitary shrinking completeness (Thm. 9), there is a unitary shrinking derivation $\Phi \vdash ff'$ which, by unitary shrinking correctness, satisfies $2|d| + |f''|_{in} = |\Phi|_{in}$. The last rule of $\Phi$ is an @ rule, that is, $\Phi$ has the following shape:

$$ \frac{\Phi_f \vdash f : \mathbf{N} \dashv \mathbf{L}' \qquad \Phi_{f'} \vdash f' : \mathbf{N}}{\vdash f f' : \mathbf{L}'} \text{ @} $$

With $\mathbf{L}'$ right linear type. Note that $|\Phi|_{in} = |\Phi_f|_{in} + |\Phi_{f'}|_{in} + 1$. By dry representation (Thm. 19.1), there are dry derivations $\Psi_f \vdash f : \mathbf{L}$ and $\Psi_{f'} \vdash f' : \mathbf{M}$ such that $\Phi_f \sim \Psi_f$ and $\Phi_{f'} \sim \Psi_{f'}$. By the properties of skeletal invariants (Lemma 15), $|\Phi_f|_{in} = |\Psi_f|_{in}$ and $|\Phi_{f'}|_{in} = |\Psi_{f'}|_{in}$. By the fact that dry derivations have minimal types (Prop. 17), $|\Psi_f|_{in} = |\mathbf{L}|$ and $|\Psi_{f'}|_{in} = |\mathbf{M}|$. Putting it all together, we obtain:

$$ \begin{aligned} 2|d| + |f''|_{in} &= T_{.9} & |\Phi_f|_{in} + |\Phi_{f'}|_{in} + 1 \\ &= L_{.15} & |\Psi_f|_{in} + |\Psi_{f'}|_{in} + 1 &= Pr. 17 & |\mathbf{L}| + |\mathbf{M}| + 1 \end{aligned} $$
2. By the *type substitution* part of the dry representation theorem (Thm. 19.2), there exist substitutions $\sigma_f$ and $\sigma_{f'}$ such that $L\sigma_f = N \dashv L'$ and $M\sigma_{f'} = N$. By stability of dry derivations under renaming (Lemma 18), we can assume that the supports of $\Psi_f$ and $\Psi_{f'}$ are disjoint, so that the domains of $\sigma_f$ and $\sigma_{f'}$ are disjoint, allowing us to define $\sigma$ as $\sigma_f \cup \sigma_{f'}$, for which $L\sigma = L\sigma_f = N \dashv L'$ and $M\sigma = M\sigma_{f'} = N$. Finally, note that $L'$ is right by hypothesis (because $\Phi$ is shrinking), so that $(L, M) \in \text{ShComPairsSub}(f, f')$. ◀

## 8 The Less Satisfying Head Case

We conclude our study by adapting the bounds from composable types to the case of head reduction. The study is slightly different in that we omit the study of type substitutions and dry derivations. We do so to show that one can obtain the first part of the de Carvalho's result – which in our opinion is the important one – by resting only on the simpler size representation theorem of Sect. 6, with no need of bothering about countably many type variables and dry derivations.

We give only the proof of the main theorem, as the other ones are variants of those in the previous section. They can be found in the technical report [1].

**The Head Case.** Let $\text{ComPairs}(t, u)$ and $\text{ComPairsSub}(t, u)$ be the analogous sets of $\text{ShComPairs}(t, u)$ and $\text{ShComPairsSub}(t, u)$ but without asking that the composed type is right shrinking, which is not needed for characterizing head termination.

**Lemma 26 (Head normalization and composable types).** Let $t$ and $u$ be closed terms. Then $tu \to_h$-normalizes if and only if $\text{ComPairs}(t, u) \neq \emptyset$.

The next theorem adapts lax bounds.

**Theorem 27 (Lax bounds for head reduction from composable types).** Let $f$ and $f'$ be closed normal terms such that $d : ff' \to_{10}^* h$ with $h$ head normal. Then:

1. Lax bounds and types: $2|d| + |h|_h \le |L| + |M| + 1$ for every composable pair $(L, M) \in \text{ComPairs}(f, f')$.

2. Lax bounds and types, up to substitutions: $2|d| + |h|_h \le |L| + |M| + 1$ for every composable pair up to substitution $(L, M) \in \text{ComPairsSub}(f, f')$.

**Theorem 28 (Exact bounds for head reduction from composable types).** Let $f$ and $f'$ be normal and such that $d : ff' \to_h^* h$ with $h$ head normal. Then there exist $L \in [f]$ and $M \in [f']$ such that $2|d| + |h|_h = |L| + |M| + 1$.

**Proof.** By head completeness (Thm. 6), there is a derivation $\Phi \vdash ff'$ satisfying $2|d| + |h|_h = |\Phi|_{\text{in}}$. The last rule of $\Phi$ is an @ rule, that is, $\Phi$ has the following shape:

$$ \frac{\Phi_f \vdash f : N \dashv L' \quad \Phi_{f'} \vdash f' : N}{\vdash f f' : L'} \text{ @} $$

Note that $|\Phi|_{\text{in}} = |\Phi_f|_{\text{in}} + |\Phi_{f'}|_{\text{in}} + 1$. By size representation (Thm. 20), there are $\Psi_f \vdash f : L$ and $\Psi_{f'} \vdash f' : M$ such that $\Phi_f \sim \Psi_f$ and $|\Psi_f|_{\text{in}} = |L|$, and $\Phi_{f'} \sim \Psi_{f'}$ and $|\Psi_{f'}|_{\text{in}} = |M|$.

By the properties of skeletal invariants (Lemma 15), $|\Phi_f|_{\text{in}} = |\Psi_f|_{\text{in}}$ and $|\Phi_{f'}|_{\text{in}} = |\Psi_{f'}|_{\text{in}}$. Putting it all together, we obtain:

$$ \begin{aligned} 2|d| + |h|_h &=_{T.6} |\Phi_f|_{\text{in}} + |\Phi_{f'}|_{\text{in}} + 1 \\ &=_{L.15} |\Psi_f|_{\text{in}} + |\Psi_{f'}|_{\text{in}} + 1 =_{T.20} |L| + |M| + 1. \end{aligned} \quad \text{◀} $$
Note that the hypotheses *f* and *f'* are normal is not a typo, we do mean *normal*, not *head normal*. The stronger hypotheses are required because the evaluation *d* leading to *h* might involve arbitrary sub-terms of *f* and *f'*, not just their heads. For instance if *f* := λx.xt and *f'* := I then *ff'* →<sub>h</sub> It →<sub>h</sub> t, and *t* is not a head sub-term of *f*.

This is where the results are less satisfying. Having to assume that *f* and *f'* are normal
might be acceptable for leftmost reduction but it limits considerably the value of de Carvalho's
analysis in the head case, which is the case naturally corresponding to relational semantics.
Indeed, there are many head normalizing terms that have no normal form – the paradigmatic
example begin given by *fix-point operators* – and about which Thm. 28 does not say anything.

9 Conclusions

In 2007, de Carvalho developed a sharp quantitative analysis of the λ-calculus using multi
types and the relational model. His study has been influential, leading to a recent new
wave of studies in the λ-calculus halfway between operational and denotational semantics.
Only the first and simpler half of de Carvalho’s results, however, has really permeated the
community. The second more technical – and probably even more interesting – part, which
lifts the quantitative analysis to the relational model, has instead been ignored by the recent
literature. This paper dissects it and revisits it, pointing out the underlying subtleties and
clarifying the concepts and tools for its proof.

A preliminary version of this work led to the adaption of de Carvalho’s compositional
bounds to call-by-value, which can be found in the technical report [11] by Accattoli et al.
Hopefully, further adaptations to other λ-calculi will be developed.

About future work, a sharper study for the head case should be developed, as to avoid
the normal form hypotheses. The main weakness of de Carvalho’s results, indeed, is that
they really work only for strong reduction, at present. As we hinted at in the introduction,
probably a finer understanding of the external *vs* internal behaviour of terms is needed.

References

1 Beniamino Accattoli. Semantic bound and multi types, revisited, 2023. arXiv:2311.18233.

2 Beniamino Accattoli and Ugo Dal Lago. (Leftmost-outermost) Beta reduction is invariant, indeed. *Logical Methods in Computer Science*, 12(1), 2016. doi:10.2168/LMCS-12(1:4)2016.

3 Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The (in)efficiency of interaction. *Proc. ACM Program. Lang.*, 5(POPL):1–33, 2021. doi:10.1145/3434332.

4 Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The space of interaction. In *36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 – July 2, 2021*, pages 1–13. IEEE, 2021. doi:10.1109/LICS52264.2021.9470726.

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

6 Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorization and normalization, essentially. In Anthony Widjaja Lin, editor, *Programming Languages and Systems – 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings*, volume 11893 of *Lecture Notes in Computer Science*, pages 159–180. Springer, 2019. doi:10.1007/978-3-030-34175-6_9.

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

8 Beniamino Accattoli and Giulio Guerrieri. Types of fireballs. In *Programming Languages and Systems – 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings*, volume 11275 of *Lecture Notes in Computer Science*, pages 45–66. Springer, 2018. doi:10.1007/978-3-030-02768-1_3.
9 Beniamino Accattoli and Giulio Guerrieri. The theory of call-by-value solvability. *Proc. ACM Program. Lang.*, 6(ICFP):855–885, 2022. doi:10.1145/3547652.

10 Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Types by need. In *Programming Languages and Systems – 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings*, volume 11423 of *Lecture Notes in Computer Science*, pages 410–439. Springer, 2019. doi:10.1007/978-3-030-17184-1_15.

11 Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Semantic bounds and strong call-by-value normalization. *CoRR*, abs/2104.13979, 2021. URL: https://arxiv.org/abs/2104.13979.

12 Sandra Alves, Delia Kesner, and Miguel Ramos. Quantitative global memory. In Helle Hvid Hansen, Andre Scedrov, and Ruy J. G. B. de Queiroz, editors, *Logic, Language, Information, and Computation – 29th International Workshop, WoLLIC 2023, Halifax, NS, Canada, July 11-14, 2023, Proceedings*, volume 13923 of *Lecture Notes in Computer Science*, pages 53–68. Springer, 2023. doi:10.1007/978-3-031-39784-4_4.

13 Sandra Alves, Delia Kesner, and Daniel Ventura. A quantitative understanding of pattern matching. In *25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway*, volume 175 of *LIPIcs*, pages 3:1–3:36. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.TYPES.2019.3.

14 Alexis Bernadet and Stéphane Lengrand. Non-idempotent intersection types and strong normalisation. *Logical Methods in Computer Science*, 9(4), 2013. doi:10.2168/LMCS-9(4:3):2013.

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

16 Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full abstraction for resource calculus with tests. In Marc Bezem, editor, *Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings*, volume 12 of *LIPIcs*, pages 97–111. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2011. doi:10.4230/LIPIcs.CSL.2011.97.

17 Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. *Ann. Pure Appl. Logic*, 109(3):205–241, 2001. doi:10.1016/S0168-0072(00)00056-7.

18 Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. A relational model of a parallel and non-deterministic lambda-calculus. In Sergei N. Artëmov and Anil Nerode, editors, *Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings*, volume 5407 of *Lecture Notes in Computer Science*, pages 107–121. Springer, 2009. doi:10.1007/978-3-540-92687-0_8.

19 Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. In *Functional and Logic Programming – 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings*, pages 13–32. Springer, 2020. doi:10.1007/978-3-030-59025-3_2.

20 Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. *Log. J. IGPL*, 25(4):431–464, 2017. doi:10.1093/JIGPAL/JZX018.

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

22 Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. *Math. Log. Q.*, 27(2-6):45–58, 1981. doi:10.1002/malq.19810270205.
23 Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca. Intersection types and (positive) almost-sure termination. *Proc. ACM Program. Lang.*, 5(POPL):1–32, 2021. doi: 10.1145/3434313.

24 Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. *Inf. Comput.*, 209(6):966–991, 2011. doi:10.1016/j.ic.2011.02.001.

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

26 Daniel de Carvalho. The relational model is injective for multiplicative exponential linear logic. In Jean-Marc Talbot and Laurent Regnier, editors, *25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 – September 1, 2016, Marseille, France*, volume 62 of LIPIcs, pages 41:1–41:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPIcs.CSL.2016.41.

27 Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. *Math. Str. in Comput. Sci.*, 28(7):1169–1203, 2018. doi:10.1017/S0960129516000396.

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

29 Daniel de Carvalho and Lorenzo Tortora de Falco. A semantic account of strong normalization in linear logic. *Inf. Comput.*, 248:104–129, 2016. doi:10.1016/j.ic.2015.12.010.

30 Thomas Ehrhard. Hypercoherences: A strongly stable model of linear logic. *Math. Struct. Comput. Sci.*, 3(4):365–385, 1993. doi:10.1017/S0960129500000281.

31 Thomas Ehrhard. Finiteness spaces. *Math. Struct. Comput. Sci.*, 15(4):615–646, 2005. doi:10.1017/S0960129504004645.

32 Thomas Ehrhard. Collapsing non-idempotent intersection types. In *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.

33 Thomas Ehrhard. The scott model of linear logic is the extensional collapse of its relational model. *Theor. Comput. Sci.*, 424:20–45, 2012. doi:10.1016/j.tcs.2011.11.027.

34 Thomas Ehrhard. Non-idempotent intersection types in logical form. In Jean Goubault-Larrecq and Barbara König, editors, *Foundations of Software Science and Computation Structures – 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings*, volume 12077 of Lecture Notes in Computer Science, pages 198–216. Springer, 2020. doi:10.1007/978-3-030-45231-5_11.

35 José Espírito Santo, Delia Kesner, and Loïc Peyrot. A faithful and quantitative notion of distant reduction for generalized applications. In Patricia Bouyer and Lutz Schröder, editors, *Foundations of Software Science and Computation Structures – 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings*, volume 13242 of Lecture Notes in Computer Science, pages 285–304. Springer, 2022. doi: 10.1007/978-3-030-99253-8_15.

36 Jean-Yves Girard. Linear Logic. *Theoretical Computer Science*, 50:1–102, 1987. doi:10.1016/0304-3975(87)90045-4.

37 Jean-Yves Girard. Normal functors, power series and the λ-calculus. *Annals of Pure and Applied Logic*, 37:129–177, 1988. doi:10.1016/0168-0072(88)90025-5.

38 Martin Hyland, Misao Nagayama, John Power, and Giuseppe Rosolini. A category theoretic formulation for engeler-style models of the untyped λ-calculus. *Electronic Notes in Theoretical Computer Science*, 161:43–57, 2006. Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2004). doi:10.1016/j.entcs.2006.04.024.
39 Delia Kesner, Loïc Peyrot, and Daniel Ventura. The spirit of node replication. In Stefan Kiefer and Christine Tasson, editors, *Foundations of Software Science and Computation Structures – 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings*, volume 12650 of *Lecture Notes in Computer Science*, pages 344–364. Springer, 2021. doi:10.1007/978-3-030-71995-1_18.

40 Delia Kesner and Daniel Ventura. Quantitative types for the linear substitution calculus. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, *Theoretical Computer Science – 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings*, volume 8705 of *Lecture Notes in Computer Science*, pages 296–310. Springer, 2014. doi:10.1007/978-3-662-44602-7_23.

41 Delia Kesner and Pierre Vial. Consuming and persistent types for classical logic. In *LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020*, pages 619–632, 2020. doi:10.1145/3373718.3394774.

42 Delia Kesner and Andrés Viso. Encoding tight typing in a unified framework. In Florin Manea and Alex Simpson, editors, *30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference)*, volume 216 of *LIPIcs*, pages 27:1–27:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.CSL.2022.27.

43 A. J. Kfoury and J. B. Wells. Principality and type inference for intersection types using expansion variables. *Theor. Comput. Sci.*, 311(1-3):1-70, 2004. doi:10.1016/j.tcs.2003.10.032.

44 Jean-Louis Krivine. *Lambda-calculus, types and models*. Ellis Horwood series. Masson, 1993.

45 Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In *28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013*, pages 301–310. IEEE Computer Society, 2013. doi:10.1109/LICS.2013.36.

46 Giulio Manzonetto. A general class of models of $H^*$. In Rastislav Královic and Damian Niwinski, editors, *Mathematical Foundations of Computer Science 2009, 34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Proceedings*, volume 5734 of *Lecture Notes in Computer Science*, pages 574–586. Springer, 2009. doi:10.1007/978-3-642-03816-7_49.

47 Giulio Manzonetto and Domenico Ruoppolo. Relational graph models, taylor expansion and extensionality. In Bart Jacobs, Alexandra Silva, and Sam Staton, editors, *Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2014, Ithaca, NY, USA, June 12-15, 2014*, volume 308 of *Electronic Notes in Theoretical Computer Science*, pages 245–272. Elsevier, 2014. doi:10.1016/j.entcs.2014.10.014.

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

49 Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Essential and relational models. *Math. Struct. Comput. Sci.*, 27(5):626–650, 2017. doi:10.1017/S0960129515000316.

50 Simona Ronchi Della Rocca. Principal type scheme and unification for intersection type discipline. *Theor. Comput. Sci.*, 59:181–209, 1988. doi:10.1016/0304-3975(88)90101-6.