# The Inhabitation Problem for Non-idempotent Intersection Types

Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca

► To cite this version:

Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca. The Inhabitation Problem for Non-idempotent Intersection Types. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.341-354, 10.1007/978-3-662-44602-7_26 . hal-01402082

HAL Id: hal-01402082

https://inria.hal.science/hal-01402082

Submitted on 24 Nov 2016

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
# The inhabitation problem for non-idempotent intersection types

Antonio Bucciarelli<fnref n="1" />, Delia Kesner<fnref n="1" />, and Simona Ronchi Della Rocca<fnref n="2" />

**Abstract.** The inhabitation problem for intersection types is known to be undecidable. We study the problem in the case of non-idempotent intersection, and we prove decidability through a sound and complete algorithm. We then consider the inhabitation problem for an extended system typing the λ-calculus with pairs, and we prove the decidability in this case too. The extended system is interesting in its own, since it allows to characterize solvable terms in the λ-calculus with pairs.

# 1 Introduction

Intersection types have been presented in the literature in many variants. Historically, one of the first versions is the one characterizing solvable terms, that we call system $C$, shown in Fig. 1 [6, 15]. Intersection enjoys associativity, commutativity, and in particular idempotency ($A \wedge A = A$). Given a type $A$ and a typing environment $\Gamma$, the problem of deciding whether there exists a term $t$ such that $\Gamma \vdash t : A$ is provable, is known in the literature both as *emptiness problem* and as *inhabitation problem*. The inhabitation problem for system $C$ has been proved to be undecidable by Urzyczyn [21]. Van Bakel [23] simplified the system, using strict types, where intersection is not allowed on the right side of the arrow; his system $S$ is presented on the left part of Fig. 2, where intersection is naturally represented through set formation, and the universal type $\omega$ by the empty set. The right part of the figure presents the relevant version of $S$, $S_r$, a system being relevant if and only if, in its provable judgments, typing environments only contain the consumed premises. The systems $C$, $S$ and $S_r$ are equivalent with respect to the typability power (neglecting the universal type $\omega$). Urzyczyn's proof of undecidability of the inhabitation problem for system $C$ can be easily adapted to system $S$. Moreover, the inhabitation problem for $C$ seems to reduce to that for $S_r$, proving that the latter is undecidable too [22], so that relevance has nothing to do with the hardness of the inhabitation problem.

<footnote n="1">¹ Univ Paris Diderot, Sorbonne Paris Cit, PPS, UMR 7126, CNRS, Paris, France</footnote>

<footnote n="2">² Dipartimento di Informatica, Università di Torino, Italy</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1: System C</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 2: Systems $\mathcal{S}$ and $\mathcal{S}_r$</figcaption></figure>

In this paper we consider the type assignment system $\mathcal{M}$, which is a variant of $\mathcal{S}_r$, where idempotency of intersection has been removed, and we prove that its inhabitation is decidable, by exploiting the fact that in this case types keep track faithfully of the different uses of variables in terms. System $\mathcal{M}$ characterizes terms having head normal form, so we design a sound and complete algorithm, that, given a typing environment $\Gamma$ and a type $\sigma$, builds a set of approximate normal forms from which all and only the head normal forms $t$ such that $\Gamma \vdash t : \sigma$ can be generated. Then we extend the system, and consequently the language, in order to consider pairs and projections. We obtain a new system $\mathcal{P}$ which characterizes the (suitably defined) solvability in the extended calculus $\Lambda_\pi$, and we prove that inhabitation is decidable also for this extension.

In the last years, growing interest has been devoted to non idempotent intersection types, since they allow to reason about quantitative properties of terms, both from a syntactical and a semantic point of view. In fact, system $\mathcal{M}$ is not new: it is the well known system R of De Carvalho [5], and it is an instance of the class of the essential $\lambda$-models defined in [20], which supplies a logical description of the strongly linear relational $\lambda$-models. Some other type assignment systems with non-idempotent intersection have been studied in the literature, for various purposes: to
compute a bound for the normalization time of terms [7]), to supply
new characterizations of strong normalization [3, 12], to study type in-
ference [14, 17], to study linearity [13], to characterize solvability in the
resource λ-calculus [19, 18]. Moreover intersection without idempotency,
commutativity nor associativity, has been used to study the game seman-
tics of a typed λ-calculus [8]. A unified model-theoretic approach covering
both the relevant and non-relevant cases, and unveiling the relations be-
tween them, is presented in [9]. Returning to the inhabitation problem,
various restrictions of the classical intersection types system have been
shown to have decidable inhabitation [16, 4]. The approach is substan-
tially different from that used in this work, since in all cases intersection
is idempotent, and the decidability is obtained by restricting the use of
rules (∧I) and (∧E), so that the corresponding type assignment does not
characterize interesting classes of terms, anymore.

## 2 The type assignment system $\mathcal{M}$

In this section we consider a relevant type system for the λ-calculus having strict intersection types that enjoy associativity and commutativity, but not idempotency. In order to emphasize this last property we represent intersections as multisets of types.

We recall that terms and contexts of the λ-calculus are generated by
the following grammars, respectively:

$$ t, u, v ::= x \mid \lambda x.t \mid tu \qquad C ::= \square \mid \lambda x.C \mid Ct \mid tC $$

Given a context C and a term t, C[t] denotes the term obtained by replacing the unique occurrence of □ in C by t, allowing the capture of free variables of t. The β-reduction is given by the rule (λx.t)u →$_{β}$ t{u/x} where t{u/x} denotes the capture free replacement of x by u in t.

Let us recall the notion of head-normal forms (hnf), which is the syntactical counter part of the well known notion of solvability for the λ-calculus. A λ-term is in hnf if it is generated by the following grammar $\mathcal{J}$, it has hnf if it β-reduces to a hnf.

$$ \mathcal{J} ::= \lambda x.\mathcal{J} \mid \mathcal{K} \qquad \mathcal{K} ::= x \mid \mathcal{K}t $$

**Definition 1.**

1. The set $\mathcal{T}\mathcal{M}$ of types is defined by the following grammar:

$$ \begin{align*} \sigma, \tau, \rho &::= \alpha \mid A \rightarrow \tau \ (\text{types}) \\ A &::= [\sigma_i]_{i \in I} \quad (\text{multiset types}) \end{align*} $$
where $\alpha$ ranges over a countable set of base types and $I$ is a finite, possibly empty, set of indices.

2. Typing environements, or simply environments, written $\Gamma, \Delta$, are functions from variables to multiset types, assigning the empty multiset to almost all the variables. The domain of $\Gamma$, written $dom(\Gamma)$, is the set of variables whose image is different from $[]$.

3. A typing judgement is a triple of the form $\Gamma \vdash t : A$. The type system $\mathcal{M}$ is given in Fig. 3. If $\Pi$ is derivation with conclusion $\Gamma \vdash t : \sigma$ we write $\Pi \triangleright \Gamma \vdash t : \sigma$, and call $t$ the subject of $\Pi$. The measure of a derivation $\Pi$, written $meas(\Pi)$, is the number of rule applications in $\Pi$. By abuse of notation, $\Gamma \vdash t : \sigma$ also denotes the existence of some derivation with conclusion $\Gamma \vdash t : \sigma$.

4. A derivation $\Pi$ is a left-subtree of a derivation $\Sigma$ if either $\Pi = \Sigma$ or $\Pi \triangleright \Delta \vdash u : \sigma$ is the major premise of $\Sigma' \triangleright \Delta +_{i \in I} \Delta_i \vdash uv : \tau$ and $\Sigma'$ is a left-subtree of $\Sigma$.

Given $\{\Gamma_i\}_{i \in I}$, $+_{i \in I} \Gamma_i$ is the environment mapping $\mathbf{x}$ to $\mathcal{U}_{i \in I} \Gamma_i(\mathbf{x})$, where $\mathcal{U}$ denotes multiset union, where the resulting environment is the one having empty domain for $I = \emptyset$. The notations $\Gamma + \Delta$ and $\Gamma +_{i \in I} \Delta_i$ are just particular cases of the previous one. $\Gamma \setminus \mathbf{x}$ is the environment assigning $[]$ to $\mathbf{x}$, and acting as $\Gamma$ otherwise; $\mathbf{x}_1 : A_1, \dots, \mathbf{x}_n : A_n$ is the environment assigning $A_i$ to $\mathbf{x}_i$, for $1 \le i \le n$, and $[]$ to any other variable.

$$ \frac{\mathbf{x} : [\rho] \vdash \mathbf{x} : \rho \quad (\text{var})}{\Gamma \vdash t : \rho} \quad (\rightarrow I) $$

$$ \frac{\Gamma \vdash t : [\sigma_i]_{i \in I} \rightarrow \rho \quad (\Delta_i \vdash u : \sigma_i)_{i \in I}}{\Gamma +_{i \in I} \Delta_i \vdash tu : \rho} \quad (\rightarrow E) $$

<caption>**Fig. 3:** The type assignment system $\mathcal{M}$ for the $\lambda$-calculus</caption>

Rule $(\rightarrow E)$ enables the typability of non strongly normalizing terms, when $I = \emptyset$. For example $\mathbf{x} : [[]] \rightarrow \alpha] \vdash \mathbf{x}((\lambda y.y)(\lambda y.y)) : \alpha$, where the outermost application is typed neglecting its unsolvable argument. This feature is shared by all the intersection type systems characterizing solvability. The same holds for the fundamental subject reduction property: if $\Pi \triangleright \Gamma \vdash t : \sigma$ and $t \rightarrow \beta u$, then $\Pi' \triangleright \Gamma \vdash u : \sigma$. What is peculiar to $\mathcal{M}$ is the fact that the size of $\Pi'$ is strictly smaller than that of $\Pi$, whenever the reduction $t \rightarrow \beta u$ takes place in an occurrence of $t$ which is typed
in Π. This property, stated in Thm. 1.1 below, allows for an original, combinatorial proof of the fact that typed terms do have hnf.

**Definition 2.**

- The set $o(t)$ of occurrences of $t$ is the set of contexts $C$ such that there exists a term $u$ verifying $C[u] = t$, $u$ being the subterm of $t$ at the occurrence $C$.

- Given $Π \triangleright Γ \vdash t : σ$, the set $to(Π) \subseteq o(t)$ of typed occurrences of $t$ in $Π$ is defined by induction on meas$(Π)$ as follows:

* $to(Π) = \{\Box\}$ if $Π$ is an instance of the axiom.

* $to(Π) = \{\Box\} \cup \{\lambda x.C \mid C \in to(Π')\}$ if the subject of $Π$ is $\lambda x.t$ and $Π'$ is the subderivation of $Π$ typing $t$.

* $to(Π) = \{\Box\} \cup \{Cu \mid C \in to(Π')\} \cup (\bigcup_{i \in I} \{tC \mid C \in to(Π'_i)\})$ if the subject of $Π$ is $tu$, $Π'$ is the subderivation of $Π$ typing $t$, and $Π'_i$, for $i \in I$, are the sub-derivations of $Π$ typing $u$.

- Given $Π \triangleright Γ \vdash t : σ$, we say that $t$ is in $Π$-normal form if for all $C \in to(Π)$, the subterm of $t$ at the occurrence $C$ is not a redex.

**Theorem 1.**

1. (Subject reduction) $Π \triangleright Γ \vdash t : σ$ and $t \to_β u$ imply $Π' \triangleright Γ \vdash σ$ where $meas(Π') \le meas(Π)$. Moreover, if the reduced redex is typed in $Π$, then $meas(Π') < meas(Π)$.

2. (Characterization) $Γ \vdash t : σ$ if and only if $t$ has hnf.

*Proof.* For 1 see [20] and for 2 see [5].

### 3 Inhabitation for system $\mathcal{M}$

The system $\mathcal{M}$ allows to type a term without giving types to all its subterms through the rule $(\to E)$ in case $I = \emptyset$. So in order to reconstruct the subject of a derivation we need a notation for these untyped subterms. We will use the standard notion of *approximate normal form* [1], which can be defined through the following grammar:

$$a, b, c ::= \Omega \mid \mathcal{N} \qquad \mathcal{N} ::= \lambda x.\mathcal{N} \mid \mathcal{L} \qquad \mathcal{L} ::= x \mid \mathcal{L}a$$

Approximate normal forms are ordered by the smallest contextual order $\le$ such that $\Omega \le a$, for all $a$. We write $a \le t$ when the term $t$ is obtained from $a$ by replacing all the occurrences of $\Omega$ by terms.
Let $\mathcal{A}(t) = \{\mathbf{a} \mid \exists \mathbf{u} \ t \to_{\beta}^{*} \mathbf{u} \text{ and } \mathbf{a} \le \mathbf{u}\}$ be the set of approximants of the $\lambda$-term $t$, and let $\bigvee_{\beta}$ denote the least upper bound w.r.t. $\le$. We write $\uparrow_{i \in I} \mathbf{a}_i$ to denote that $\bigvee_{i \in I} \{\mathbf{a}_i\}_{i \in I}$ does exist. It is easy to check that, for every $t$ and $\mathbf{a}_1, \dots, \mathbf{a}_n \in \mathcal{A}(t)$, $\uparrow_{i \in \{1, \dots, n\}} \mathbf{a}_i$. An approximate normal form $\mathbf{a}$ is a head subterm of $\mathbf{b}$ if either $\mathbf{b} = \mathbf{a}$ or $\mathbf{b} = \mathbf{c}\mathbf{c}'$ and $\mathbf{a}$ is a head subterm of $\mathbf{c}$. System $\mathcal{M}$ gives types to approximate normal forms, by simply assuming that no type can be assigned to the constant $\Omega$. It is easy to check that, if $\Gamma \vdash \mathbf{a} : \sigma$ and $\mathbf{a} \le \mathbf{b}$ (resp. $\mathbf{a} \le t$) then $\Gamma \vdash \mathbf{b} : \sigma$ (resp. $\Gamma \vdash t : \sigma$). Given $\Pi \triangleright \Gamma \vdash t : \tau$, where $t$ is in $\Pi$-normal form, we denote by $\mathcal{A}(\Pi)$ the minimal approximant $\mathbf{b}$ of $t$ such that $\Pi \triangleright \Gamma \vdash \mathbf{b} : \tau$. Formally,

**Definition 3.** Given $\Pi \triangleright \Gamma \vdash t : \sigma$, where $t$ is in $\Pi$-normal form, $\mathcal{A}(\Pi) \in \mathcal{A}(t)$ is defined by induction on $\mathbf{meas}(\Pi)$ as follows:

- If $\Pi \triangleright \Gamma \vdash \mathbf{x} : \rho$, then $\mathcal{A}(\Pi) = \mathbf{x}$.

- If $\Pi \triangleright \Gamma \vdash \lambda \mathbf{x} \cdot t : \mathbf{A} \to \rho$ follows from $\Pi' \triangleright \Gamma, \mathbf{x} : \mathbf{A} \vdash t : \rho$, then $\mathcal{A}(\Pi) = \lambda \mathbf{x} \cdot \mathcal{A}(\Pi')$, $t$ being in $\Pi'$-normal form.

- If $\Pi \triangleright \Gamma = \Gamma' +_{i \in I} \Delta_i \vdash \mathbf{t}u : \rho$ follows from $\Pi' \triangleright \Gamma \vdash t : [\sigma_i]_{i \in I} \to \rho$ and $(\Pi'_i \triangleright \Delta_i \vdash \mathbf{u} : \sigma_i)_{i \in I}$, then $\mathcal{A}(\Pi) = \mathcal{A}(\Pi')(\bigvee_{i \in I} \mathcal{A}(\Pi'_i))$ (remark that $t$ is in $\Pi'$-normal form, $\mathbf{u}$ if in $\Pi'_i$-normal form, for all $i \in I$, and that $\uparrow_{i \in I} \mathcal{A}(\Pi'_i)$, since $\mathcal{A}(\Pi'_i) \in \mathcal{A}(\mathbf{u})$, for all $i \in I$).

Remark that, in the final item of the definition above, the approximate normal form corresponding to the case $I = \emptyset$ is $\mathcal{A}(\Pi')\Omega$.

A simple induction on $\mathbf{meas}(\Pi)$ allows to show the following:

**Proposition 1.** If $\Pi \triangleright \Gamma \vdash t : \sigma$ and $t$ is in $\Pi$-normal form, then $\Pi \triangleright \Gamma \vdash \mathcal{A}(\Pi) : \sigma$.

**3.1 The inhabitation algorithm**

The inhabitation rules are given in Fig. 4. The algorithm, given an environment $\Gamma$ and a type $\sigma$, builds the set $\mathbf{T}(\Gamma, \sigma)$ containing all the approximate normal forms $\mathbf{a}$ such that there exists a derivation $\Pi \triangleright \Gamma \vdash \mathbf{a} : \sigma$, with $\mathbf{a} = \mathcal{A}(\Pi)$, then stops. The algorithm uses two auxiliary predicates, namely $\mathbf{TI}(\Gamma, [\sigma_i]_{i \in I})$ and $\mathbf{H}_{\mathbf{a}}^{\Delta}(\Gamma, \sigma) \triangleright \tau$. The set $\mathbf{TI}(\Gamma, [\sigma_i]_{i \in I})$ contains all the approximate normal forms $\mathbf{a} = \bigvee_{i \in I} \mathbf{a}_i$ such that $\Gamma = +_{i \in I} \Gamma_i$, $\mathbf{a}_i \in \mathbf{T}(\Gamma_i, \sigma_i)$ for all $i \in I$, and $\uparrow_{i \in I} \mathbf{a}_i$. Finally, $\mathbf{H}_{\mathbf{a}}^{\Delta}(\Gamma, \sigma) \triangleright \tau$ contains all the approximate normal forms $\mathbf{b}$ such that $\mathbf{a}$ is a head subterm of $\mathbf{b}$, and such that if $\mathbf{a} \in \mathbf{T}(\Delta, \sigma)$ then $\mathbf{b} \in \mathbf{T}(\Gamma + \Delta, \tau)$.

Notice the particular case $I = \emptyset$ in (Union), which gives $\Omega \in \mathbf{TI}(\emptyset, [])$, where $\emptyset$ denotes the environement having empty domain. The algorithm is
$$ \frac{a \in T(\Gamma + (x : A), \tau) \qquad x \notin \mathrm{dom}(\Gamma)}{\lambda x.a \in T(\Gamma, A \to \tau)} \quad (\mathrm{Abs}) $$

$$ \frac{(a_i \in T(\Gamma_i, \sigma_i))_{i \in I} \quad \uparrow_{i \in I} a_i}{\bigvee_{i \in I} a_i \in TI(+_{i \in I} \Gamma_i, [\sigma_i]_{i \in I})} \quad (\mathrm{Union}) $$

$$ \frac{a \in \mathbb{H}_x^{x:\sigma}(\Gamma, \sigma) \triangleright \tau}{a \in T(\Gamma + (x : [\sigma]), \tau)} \quad (\text{Head}) \qquad \frac{\sigma = \tau}{a \in \mathbb{H}_a^{\Delta}(\emptyset, \sigma) \triangleright \tau} \quad (\text{Final}) $$

$$ \frac{\Gamma = \Gamma_0 + \Gamma_1 \qquad b \in TI(\Gamma_0, A) \qquad a \in \mathbb{H}_{cb}^{\Delta+\Gamma_0}(\Gamma_1, \sigma) \triangleright \tau}{a \in \mathbb{H}_c^{\Delta}(\Gamma, A \to \sigma) \triangleright \tau} \quad (\text{Prefix}) $$

<caption>**Fig. 4:** The inhabitation algorithm for the λ-calculus</caption>

not an obvious extension of the classical inhabitation algorithm for simple types [2, 10]. In particular, when restricted to simple types, it reconstructs all the normal forms inhabiting a given type, while the original algorithm reconstructs just the long η-normal forms. This is achieved thanks to a non deterministic behaviour, illustrated in the Example 1.1 below.

**Example 1.**

1. Let $\Gamma = \emptyset$ and $\sigma = [[\alpha] \to \alpha] \to [\alpha] \to \alpha$. Given input $(\Gamma, \sigma)$, the algorithm can have the following two behaviours:

(1) Choosing the sequence of rules: (Abs), (Abs), (Head), (Prefix), (Final) the final approximant is $\lambda xy.x$;

(2) Choosing the sequence of rules: (Abs), (Head), (Final) the final approximant is $\lambda x.x$.

2. Let $\Gamma = \emptyset$ and $\sigma = [[\alpha] \to \alpha] \to \alpha$. Given input $(\Gamma, \sigma)$, by the sequence of rules: (Abs), (Head), (Prefix), ((Union), (Final)) we obtain $\lambda x.x\Omega$.

**Definition 4.** In order to show that the inhabitation algorithm terminates, we define a measure on types and environments, as follows:

$$ \#(\alpha) = 1 \qquad \#([\sigma_i]_{i \in I}) = \sum_{i \in I} \#(\sigma_i) + 1 \\ \#(A \to \rho) = \#(A) + \#(\rho) + 1 \qquad \#(\Gamma) = \sum_{x \in \mathrm{dom}(\Gamma)} \#(\Gamma(x)) $$

The measure is then be extended to the judgements of the algorithm:

$$ \#(\mathrm{T}(\Gamma, \rho)) = \#(\mathbb{H}_b^{\Delta}(\Gamma, \rho) \triangleright \tau) = \#(\Gamma) + \#(\rho) \\ \#(\mathrm{TI}(\Gamma, A)) = \#(\Gamma) + \#(A) $$

**Lemma 1 (Termination).** The inhabitation algorithm terminates.

*Proof Hint.* To each call $C \in \{\mathrm{T}(-, -), \mathrm{TI}(-, -), \mathbb{H}_c(-, -) \triangleright -\}$ of the algorithm, we associate a tree $T_C$ as follows: nodes are labeled with elements of $C$.
A node $n'$ is a son of $n$ iff there exists some instance of a rule having $n$ as conclusion and $n'$ as premise. Thus, all possible runs of $C$ are encoded in the tree $T_C$, which is finitely branching. Moreover, it is easy to see that the measure $\#()$ strictly decreases along the branches of $T_C$, so that every branch has finite depth. Hence, $T_C$ is finite by König's Lemma, i.e. the algorithm terminates.

Soundness and completeness of the inhabitation algorithm follow from
the following Lemma, relating typings of approximate normal forms in
system $\mathcal{M}$ and runs of the algorithm:

**Lemma 2.** $\mathbf{a} \in \mathbf{T}(\Gamma, \sigma) \Leftrightarrow \exists \Pi \triangleright \Gamma \vdash \mathbf{a} : \sigma \text{ such that } \mathbf{a} = \mathcal{A}(\Pi)$.

*Proof.* (⇒): We prove the following statements, by induction on the rules
in Fig. 4:

a) $\mathbf{a} \in \mathbf{T}(\Gamma, \sigma) \Rightarrow \exists \Pi \triangleright \Gamma \vdash \mathbf{a} : \sigma \text{ such that } \mathbf{a} = \mathcal{A}(\Pi)$.

b) $\mathbf{a} \in \mathbf{TI}(+_{i \in I} \Gamma_i, [\sigma_i]_{i \in I}) \Rightarrow \exists (\Pi_i \triangleright \Gamma_i \vdash \mathbf{a}_i : \sigma_i)_{i \in I} \text{ such that } \mathbf{a}_i = \mathcal{A}(\Pi_i)$, for $i \in I$, $\uparrow_{i \in I} \mathbf{a}_i$ and $\mathbf{a} = \bigvee_{i \in I} \mathbf{a}_i$.

c) $\mathbf{a} \in \mathbf{H}_{\mathbf{b}}^{\Delta}(\Gamma, \sigma) \triangleright \tau \Rightarrow$ there exists a function $F$ associating to each derivation $\Sigma \triangleright \Delta \vdash \mathbf{b} : \sigma$ such that $\mathbf{b} = \mathcal{A}(\Sigma)$, a derivation $\Pi \triangleright \Gamma + \Delta \vdash \mathbf{a} : \tau$ such that $\mathbf{a} = \mathcal{A}(\Pi)$.

If $\lambda x.\mathbf{a} \in \mathbf{T}(\Gamma, \mathbf{A} \to \tau)$ follows from $\mathbf{a} \in \mathbf{T}(\Gamma + (\mathbf{x} : \mathbf{A}), \tau)$ by (Abs), then we conclude by the $i.h.(a)$ and by an application of $(\to \mathbf{I})$.

If $\bigvee_{i \in I} \mathbf{a}_i \in \mathbf{TI}(+_{i \in I} \Gamma_i, [\sigma_i]_{i \in I})$ follows from $(\mathbf{a}_i \in \mathbf{T}(\Gamma_i, \sigma_i))_{i \in I}$ and $\uparrow_{i \in I} \mathbf{a}_i$ by (Union), then by $i.h.(a)$, there exist $(\Pi_i \triangleright \Gamma_i \vdash \mathbf{a}_i : \sigma_i)_{i \in I}$ such that for all $i \in I$, $\mathbf{a}_i = \mathcal{A}(\Pi_i)$, and we are done.

If $\mathbf{a} \in \mathbf{T}(\Gamma + (\mathbf{x} : [\sigma]), \tau)$ follows from $\mathbf{a} \in \mathbf{H}_{\mathbf{x}}^{x:[\sigma]}(\Gamma, \sigma) \triangleright \tau$ by (Head), then the i. h. (c) provides a function associating to each derivation $\Sigma \triangleright \mathbf{x} : [\sigma] \vdash \mathbf{x} : \sigma$ a derivation $\Pi \triangleright \Gamma + \mathbf{x} : [\sigma] \vdash \mathbf{a} : \tau$ such that $\mathbf{a} = \mathcal{A}(\Pi)$, since $\mathbf{x} = \mathcal{A}(\Sigma)$. Applying this function to the unique derivation of $\mathbf{x} : [\sigma] \vdash \mathbf{x} : \sigma$, we get the suitable typing of $\mathbf{a}$.

If $\mathbf{a} \in \mathbf{H}_{\mathbf{a}}^{\Delta}(\emptyset, \sigma) \triangleright \tau$ follows from $\sigma = \tau$ by (Final), then the identity function satisfies the requirements of (c).

Finally, if $\mathbf{a} \in \mathbf{H}_{\mathbf{c}}^{\Delta}(\Gamma_0 + \Gamma_1, \mathbf{A} \to \sigma) \triangleright \tau$ follows from $\mathbf{b} \in \mathbf{TI}(\Gamma_0, \mathbf{A})$ and $\mathbf{a} \in \mathbf{H}_{\mathbf{cb}}^{\Delta+\Gamma_0}(\Gamma_1, \sigma) \triangleright \tau$ by (Prefix), then we have to provide a function $F$ associating to each derivation $\Sigma \triangleright \Delta \vdash \mathbf{c} : \mathbf{A} \to \sigma$ such that $\mathbf{c} = \mathcal{A}(\Sigma)$, a derivation $\Pi \triangleright \Delta + \Gamma_0 + \Gamma_1 \vdash \mathbf{a} : \tau$ such that $\mathbf{a} = \mathcal{A}(\Pi)$. To begin with, the $i.h.(b)$ applied to $\mathbf{b} \in \mathbf{TI}(\Gamma_0, \mathbf{A})$ provides a family of derivations $(\Pi_i \triangleright \Gamma_0^i \vdash \mathbf{b}_i : \sigma_i)_{i \in I}$ such that $\mathbf{b}_i = \mathcal{A}(\Pi_i)$, $\Gamma_0 = +_{i \in I} \Gamma_0^i$, $\mathbf{A} = [\sigma_i]_{i \in I}$, $\uparrow_{i \in I} \mathbf{b}_i$ and $\mathbf{b} = \bigvee_{i \in I} \mathbf{b}_i$. Rule ($\to \mathbf{E}$) with premises $\Sigma$ and $\{\Pi_i\}_{i \in I}$, gives
a type derivation $\Pi' \triangleright \Delta + \Gamma_0 \vdash \mathbf{cb} : \sigma$, such that $\mathbf{cb} = \mathcal{A}(\Pi')$. Then, the i.h.(c) applied to $\mathbf{a} \in \mathbb{H}_{\mathbf{cb}}^{\Delta+\Gamma_0}(\Gamma_1, \sigma) \triangleright \tau$ provides a function $F'$ such that $F'(\Pi') \triangleright \Delta + \Gamma_0 + \Gamma_1 \vdash \mathbf{a} : \tau$ and $\mathbf{a} = \mathcal{A}(F'(\Pi'))$. To conclude, we set $F(\Sigma) = F'(\Pi')$.

(=$\Leftarrow$): We prove the following statements, by induction on the definition of $\mathcal{A}(\Pi)$ (Def. 3):

1. Given $\Sigma \triangleright \Delta \vdash \mathbf{b} : \tau$ and $\Pi \triangleright \Gamma \vdash \mathbf{a} : \sigma$, if $\mathbf{b} = \mathcal{A}(\Sigma)$ and $\mathbf{a} = \mathcal{A}(\Pi)$ are $\mathcal{L}$-approximate normal forms, and $\Sigma$ is a left-subtree of $\Pi$, then there exists $\Gamma'$ s.t. $\Gamma = \Gamma' + \Delta$ and $\mathbb{H}_{\mathbf{a}}^{\Delta+\Gamma'}(\Theta, \sigma) \triangleright \rho \subseteq \mathbb{H}_{\mathbf{b}}^{\Delta}(\Theta + \Gamma', \tau) \triangleright \rho$.

2. $\Pi \triangleright \Gamma \vdash \mathbf{a} : \sigma$ and $\mathbf{a} = \mathcal{A}(\Pi)$ imply $\mathbf{a} \in \mathbb{T}(\Gamma, \sigma)$.

1. If $\mathbf{a} = \mathbf{x}$, then $\Pi$ is an instance of the axiom (**var**); $\Sigma$ being a left subtree of $\Pi$, we get $\Sigma = \Pi$, $\mathbf{b} = \mathbf{x}$, $\Gamma' = \emptyset$, $\sigma = \tau$ and the inclusion $\mathbb{H}_{\mathbf{b}}^{\Delta+\Gamma'}(\Theta, \sigma) \triangleright \rho \subseteq \mathbb{H}_{\mathbf{a}}^{\Delta}(\Theta + \Gamma', \tau) \triangleright \rho$ holds trivially.

If $\mathbf{a} = \mathbf{ca}'$, $\mathbf{c}$ being a $\mathcal{L}$-approximate normal form, then the last rule of $\Pi$ is an instance of $(\to \mathbb{E})$, with premises $\Pi' \triangleright \Gamma'' \vdash \mathbf{c} : [\sigma_i]_{i \in I} \to \sigma$ and $(\Pi_i \triangleright \Gamma_i \vdash \mathbf{a}' : \sigma_i)_{i \in I}$, so that $\Gamma = \Gamma'' +_{i \in I} \Gamma_i$; moreover $\Sigma \triangleright \Delta \vdash \mathbf{b} : \tau$ is also a left-subtree of $\Pi'$. We have in this case $\mathbf{a}' = \bigvee_{i \in I} \mathcal{A}(\Pi_i)$, where by the i.h.(2), $\mathcal{A}(\Pi_i) \in \mathbb{T}(\Gamma_i, \sigma_i)$. Then $\mathbb{H}_{\mathbf{ca}'}^{\Delta+\Gamma''+_{i \in I} \Gamma_i}(\Theta, \sigma) \triangleright \rho \subseteq_{(\mathbf{Prefix})} \mathbb{H}_{\mathbf{c}}^{\Delta+\Gamma''}(\Theta +_{i \in I} \Gamma_i, [\sigma_i]_{i \in I} \to \sigma) \triangleright \rho \subseteq_{i.h.(1)} \mathbb{H}_{\mathbf{b}}^{\Delta}(\Theta + \Gamma'' +_{i \in I} \Gamma_i, \sigma) \triangleright \rho$.

2. If $\mathbf{a}$ is a $\mathcal{L}$-approximate normal form, then $\exists \tau$ s.t. $\Gamma = \Gamma_0 + (\mathbf{x} : [\tau])$ and the type derivation $\mathbf{x} : [\tau] \vdash \mathbf{x} : \tau$ is a left subtree of $\Gamma_0 + (\mathbf{x} : [\tau]) \vdash \mathbf{a} : \sigma$. Then we have $\mathbf{a} \in_{(\mathbf{Final})} \mathbb{H}_{\mathbf{a}}^{\Gamma}(\emptyset, \sigma) \triangleright \sigma \subseteq_{(\mathbf{Point}(1))} \mathbb{H}_{\mathbf{x}}^{\mathbf{x}:[\tau]}(\Gamma_0, \tau) \triangleright \sigma \subseteq_{(\mathbf{Head})} \mathbb{T}(\Gamma_0 + \{\mathbf{x} : [\tau]\}, \sigma)$. Otherwise, $\mathbf{a} = \lambda\mathbf{x}.\mathbf{a}'$, and we conclude by the i.h.(2) on $\mathbf{a}'$.

**Theorem 2 (Soundness and Completeness).**

1. If $\mathbf{a} \in \mathbb{T}(\Gamma, \sigma)$ then, for all $\mathbf{t}$ such that $\mathbf{a} \leq \mathbf{t}$, $\Gamma \vdash \mathbf{t} : \sigma$.

2. If $\Pi \triangleright \Gamma \vdash \mathbf{t} : \sigma$ then there exists $\Pi' \triangleright \Gamma \vdash \mathbf{t}' : \sigma$ such that $\mathbf{t}'$ is in $\Pi$'-normal form, and $\mathcal{A}(\Pi') \in \mathbb{T}(\Gamma, \sigma)$.

*Proof.* Soundness follows from Lem. 2 (=$\Rightarrow$) and the remark that, if $\Gamma \vdash \mathbf{a} : \sigma$ and $\mathbf{a} \leq \mathbf{t}$, then $\Gamma \vdash \mathbf{t} : \sigma$. Completeness follows from Thm. 1.1, ensuring that given $\Pi \triangleright \Gamma \vdash \mathbf{t} : \sigma$, there exists $\Pi' \triangleright \Gamma \vdash \mathbf{t}' : \sigma$ such that $\mathbf{t}'$ is in $\Pi$'-normal form, then from Prop. 1 and Lem. 2 ($\Leftarrow$).

**4 Adding pairs and projections**

The language $\Lambda_\pi$ is an extension of $\lambda$-calculus with pairs and projections. Its terms and contexts are defined by the following grammars:
$$ t, u, v ::= x \mid \lambda x.t \mid tu \mid \pi_1 t \mid \pi_2 t \mid \langle t, u \rangle $$

$$ C ::= \square \mid \lambda x.C \mid Ct \mid tC \mid \pi_1 C \mid \pi_2 C \mid \langle t, C \rangle \mid \langle C, t \rangle $$

The reduction relation, also denoted by $\rightarrow$, is the contextual closure of the following rules:

$$ (\lambda x.t)u \rightarrow_{\beta} t\{u/x\} \qquad \pi_1\langle t, u \rangle \rightarrow_{\pi} t \qquad \pi_2\langle t, u \rangle \rightarrow_{\pi} u $$

As usual, $\rightarrow^*$ denotes the reflexive-transitive closure of $\rightarrow$. We write $\bar{t}$ and $\bar{\pi}$ (resp. $\bar{t}_n$ and $\bar{\pi}_n$) to denote a possibly empty sequence (resp. a sequence of length $n$) of terms and projections, respectively.

$\Lambda_{\pi}$ inherits from the $\lambda$-calculus important properties, such as confluence. Solvability is defined as usual, but pairs are solvable independently from their content, since we want to consider them as lazy data structures:

**Definition 5.**

1. A head context is a context of the shape: $(\lambda\bar{x}.\square)\bar{t}$;

2. A term $t$ is solvable if and only if there is a head context $C$ such that $C[t] \rightarrow^* u$, where $u$ is either a pair $\langle u_1, u_2 \rangle$ or the identity $I$.

We will prove that solvability can be syntactically characterized by the notion of **hnf**, defined by the following grammar:

$$ \mathcal{J} ::= \lambda x.\mathcal{J} \mid \langle t, t \rangle \mid \mathcal{P} $$

$$ \mathcal{P} ::= x \mid \mathcal{P}t \mid \pi_1 \mathcal{P} \mid \pi_2 \mathcal{P} $$

The head variable of a term in $\mathcal{P}$ is defined by: $x$ is the head variable of $x$ and $\bar{x}$ is the head variable of $ut$ (resp. $\pi_i u$, $i = 1, 2$) if $\bar{x}$ is the head variable of $u$. A term has hnf if it reduces to a hnf.

We will prove now that if a term has hnf then it is solvable. The converse will be proved through a suitable type assignment system, which will be introduced in the next subsection.

**Lemma 3.** It $t$ has hnf then it is solvable.

*Proof.* Let us define, for every sequence of projections $\bar{\pi}$ and every term $t$, the term $P_{\bar{\pi}}(t)$ such that $\bar{\pi}P_{\bar{\pi}}(t) \rightarrow^* t$. If $\bar{\pi}$ is the empty sequence, $P_{\bar{\pi}}(t) = t$, if $\bar{\pi} = \bar{\pi}'\pi_1$ (resp. $\bar{\pi}'\pi_2$), then $P_{\bar{\pi}}(t) = \langle P_{\bar{\pi}'}(t), I \rangle$ (resp. $\langle I, P_{\bar{\pi}'}(t) \rangle$). Moreover, let $\Pi$ and $J$ be two lists of same length, the first containing sequences of projections and the second one natural numbers. The term $\nabla(\Pi, J)$ is defined inductively as follows:

if $\Pi$ and $J$ are empty, then $\nabla(\Pi, J) = I$ else if $\Pi = \bar{\pi} :: \Pi'$ and $J = j :: J'$ then $\nabla(\Pi, J) = P_{\bar{\pi}}(\lambda\bar{y}_j.\nabla(\Pi', J'))$.

Now we prove that, if $t$ has a $\mathcal{P}$-hnf and $x$ is its head variable, then for all $\Pi, J$ there exists a term $O_{\nabla(\Pi, J)}^t$ such that $t\{O_{\nabla(\Pi, J)}^t/x\} \rightarrow^* \nabla(\Pi, J)$. If $t = x\bar{t}_n$, then $O_{\nabla(\Pi, J)}^t = \lambda\bar{y}_n.\nabla(\Pi, J)$.
If $t = \bar{\pi}ut_n$, then $O_{\nabla(\Pi,J)}^t = O_{\nabla(\bar{\pi}::\Pi,n::J)}^u$. In fact, $\bar{\pi}ut_n\{O_{\nabla(\bar{\pi}::\Pi,n::J)}^u/x\} \to^* \bar{\pi}(u\{O_{\nabla(\bar{\pi}::\Pi,n::J)}^u/x\})t'_n \to^*_{(i.h.)} \bar{\pi}\nabla(\bar{\pi} :: \Pi, n :: J)t'_n$ which reduces to $\bar{\pi}P_{\bar{\pi}}(\lambda\bar{y}_n \cdot \nabla(\Pi, J))t'_n \to^* \nabla(\Pi, J)$, where $t'_n = \bar{t}_n\{O_{\nabla(\bar{\pi}::\Pi,n::J)}^u/x\}$. Now, to show the statement of the lemma we proceed by cases.

If $t \in \mathcal{P}$, then let $x$ be the head of $t$ and let $C = (\lambda x.\Box)O_{\nabla(\epsilon,\epsilon)}^t$. By the previous point we have $C[t] = (\lambda x.t)O_{\nabla(\epsilon,\epsilon)}^t \to t\{O_{\nabla(\epsilon,\epsilon)}^t/x\} \to^* \nabla(\epsilon, \epsilon) = \mathbf{I}$. If $t = \lambda \bar{y}_n \cdot (u, v)$, then let $C = \Box \bar{I}_n$. Then $C[t] \to^* \langle u, v \rangle$. If $t = \lambda \bar{y}_n \cdot u$, where $u \in \mathcal{P}$, then let $x$ be the head of $u$. If $x \notin \bar{y}_n$, we let $C = (\lambda x.\Box)O_{\nabla(\epsilon,\epsilon)}^u \bar{I}_n$. Then $C[t] \to^* (\lambda \bar{y}_n \cdot u\{O_{\nabla(\epsilon,\epsilon)}^u/x\})\bar{I}_n \to^* (\lambda \bar{y}_n \cdot \mathbf{I})\bar{I}_n \to^* \mathbf{I}$. If $x = y_i$, we let $C = (\Box)\bar{I}_{i-1}O_{\nabla(\epsilon,\epsilon)}^u \bar{I}_{n-i}$. Then $C[t] \to^* u\{O_{\nabla(\epsilon,\epsilon)}^u/x\}\{\bar{I}_{n-1}/\bar{y}_{n-1}\} \to^* \mathbf{I}\{\bar{I}_{n-1}/\bar{y}_{n-1}\} = \mathbf{I}$.

## 4.1 The type assignment system $\mathcal{P}$

We now present the system $\mathcal{P}$, an extension of system $\mathcal{M}$ which assigns types to $\Lambda_\pi$-terms in such a way that typability coincides with solvability.

### Definition 6.

1. The set $\mathcal{TP}$ of types is extended using the following grammar:

$$ \begin{array}{l} \sigma, \tau, \rho ::= \omega_{\times} \mid \alpha \mid A \to \tau \mid \times_1(\tau) \mid \times_2(\tau) \quad (\text{types}) \\ A ::= [\sigma_i]_{i \in I} \qquad (\text{multiset types}) \end{array} $$

where $\omega_\times$ is a type constant.

2. A typing judgement is a triple of the form $\Gamma \vdash t : A$, where $\Gamma$ is a typing environment defined as in Def. 1. The type system $\mathcal{P}$ is obtained by adding to the system $\mathcal{M}$ the rules given in Fig. 5.

3. The definition of left-subtree of a derivation $\Sigma$ is as Def. 1.4, with the following additional cases:

- a derivation $\Pi \triangleright \Delta \vdash t : \sigma$ is a left subtree of a derivation $\Sigma$ if $\Pi$ is the premise of $\Sigma' \triangleright \Delta \vdash \langle t, u \rangle : \times_1(\sigma)$ and $\Sigma'$ is a left subtree of $\Sigma$ (and similarly for the case $\times_2(\sigma)$).

- a derivation $\Pi \triangleright \Delta \vdash t : \times_i(\sigma)$ is a left subtree of a derivation $\Sigma$ if $\Pi$ is the premise of $\Sigma' \triangleright \Delta \vdash \pi_i(t) : \sigma$ and $\Sigma'$ is a left subtree of $\Sigma$, for $i = 1, 2$.

The constant $\omega_\times$ is a universal type for pairs, making all pairs typable. The system is relevant, and it enjoys both subject reduction (in a weighted version) and subject expansion. The notions of occurrences and typed occurrences are extended as expected from those of Def. 2.
<figure><img src="image_4.png" /><figcaption>Fig. 5: Typing rules for pairs in $\mathcal{P}$</figcaption></figure>

**Lemma 4.**

1. (Subject reduction) $\Pi \triangleright \Gamma \vdash t : \sigma$ and $t \to u$ imply $\Pi' \triangleright \Gamma \vdash u : \sigma$ where $\text{meas}(\Pi') \le \text{meas}(\Pi)$. In particular, if the reduced redex is typed, then $\text{meas}(\Pi') < \text{meas}(\Pi)$.

2. (Subject expansion) $\Gamma \vdash u : \sigma$ and $t \to u$ imply $\Gamma \to t : \sigma$.

**Lemma 5.** Let $\Pi \triangleright \Gamma \vdash t : \sigma$. Then $t$ has hnf.

*Proof.* By induction on $\text{meas}(\Pi)$ using Lem. 4.1.

The solvability characterization is proved in the next theorem.

**Theorem 3.** The following statements are equivalent: (1) $t$ is solvable; (2) $t$ has hnf; (3) $t$ is typable in system $\mathcal{P}$.

*Proof.* $2 \Rightarrow 1$ holds by Lem. 3 and $3 \Rightarrow 2$ holds by Lem. 5. We now show $1 \Rightarrow 3$: $t$ is solvable implies, by definition, the existence of a context $C$ such that $C = (\lambda \bar{x}.\Box)\bar{v}$ and either $C[t] \to^* I$ or $C[t] \to^* \langle u_1, u_2 \rangle$, for some $u_1, u_2$. Both $I$ and $\langle u_1, u_2 \rangle$ can be typed, so $C[t]$ is typed, by Lem. 4.2. Note that $C[t] = (\lambda \bar{x}.t)\bar{v}$, so for typing $C[t]$ we need to type $t$.

# 5 Inhabitation for system $\mathcal{P}$

We extend approximate normal forms (cf. Sec. 3) as follows:

$$ a, b, c ::= \Omega \mid \mathcal{N} \qquad \mathcal{N} ::= \lambda x. \mathcal{N} \mid \langle a, a \rangle \mid \mathcal{L} \qquad \mathcal{L} ::= x \mid \mathcal{L} a \mid \pi_i \mathcal{L} $$

The order relation $\le$ and the sets $\mathcal{A}(t)$ are defined as in the case of the pure $\lambda$-calculus. The type assignment system $\mathcal{P}$ for the $\Lambda_\pi$-calculus is extended to approximate normal forms, assuming as before that no type can be assigned to the constant $\Omega$. Given $\Pi \triangleright \Gamma \vdash t : \tau$, where $t$ is in hnf, we extend the definition of minimal approximant of $t$.
**Definition 7.** Given $Π▷Γ ⊢ t : σ$, where $t$ is in $Π$-normal form, $A(Π) ∈ A(t)$ is defined by extending Def. 3 with the following additional cases:

- If $Π▷ ⊢ ⟨t, u⟩ : ω_×$, then $A(Π) = ⟨Ω, Ω⟩$.

- If $Π▷ Γ ⊢ ⟨t_1, t_2⟩ : ×_i(τ)$ follows from $Π_i▷ Γ ⊢ t_i : τ$, then $i = 1$ implies $A(Π) = ⟨A(Π_1), Ω⟩$ and $i = 2$ implies $A(Π) = ⟨Ω, A(Π_2)⟩$.

- If $Π▷ Γ ⊢ π_i t : τ$ follows from $Π'▷ Γ ⊢ t : ×_i(τ)$, then $A(Π) = π_i A(Π')$.

## 5.1 The inhabitation algorithm

The algorithm in Fig. 4 is extended with the additional rules in Fig 6.

$$ \frac{\substack{\mathbf{a} \in \mathbb{H}_{\pi_i(b)}^{\Delta}(\Gamma, \sigma) \triangleright \tau \\ \mathbf{a} \in \mathbb{H}_b^{\Delta}(\Gamma, \times_i(\sigma)) \triangleright \tau}}{\langle \Omega, \Omega \rangle \in \mathbb{T}(\emptyset, \omega_\times)} \quad \text{(Proj)} \qquad \frac{\substack{\mathbf{a} \in \mathbb{T}(\Gamma, \tau) \\ \langle \mathbf{a}, \Omega \rangle \in \mathbb{T}(\Gamma, \times_1(\tau))}}{\langle \Omega, \mathbf{a} \rangle \in \mathbb{T}(\Gamma, \times_2(\tau))} \quad \text{(Prod1)} \qquad \frac{\substack{\mathbf{a} \in \mathbb{T}(\Gamma, \tau) \\ \langle \Omega, \mathbf{a} \rangle \in \mathbb{T}(\Gamma, \times_2(\tau))}}{\langle \Omega, \Omega \rangle \in \mathbb{T}(\emptyset, \omega_\times)} \quad \text{(Pair)} $$

<caption>**Fig. 6:** The inhabitation algorithm for the $λ$-calculus with products</caption>

*Example 2.* Let $Γ = \emptyset$ and $τ = \times_1([α] → α)$ and $σ = [τ] → τ$. Then given the input $(Γ, σ)$, the algorithm can have the following two behaviours:

Choosing the sequence of rules: (Abs), (Prod1), (Abs), (Head), (Proj), (Prefix), (Final) the final approximant is $λy.⟨λx.π_1yx, Ω⟩$;

Choosing the sequence of rules: (Abs), (Head), (Final) the final approximant is $λy.y$;

To show that the inhabitation algorithm terminates, we extend the measure given in Sec. 2 by adding $#(ω_×) = 1$ and $#(×_i(τ)) = #(τ) + 1$. Termination and soundness hold, and the extension is straightforward.

**Lemma 6 (Termination).** *The inhabitation algorithm terminates.*

*Proof.* As for Lem. 1, using the extended measure above.

**Lemma 7.** $\mathbf{a} \in \mathbb{T}(\Gamma, \sigma) \Leftrightarrow \exists \Pi \triangleright \Gamma \vdash \mathbf{a} : \sigma$ such that $\mathbf{a} = A(\Pi)$.

*Proof.* We follow the proof of Lem. 2, with the suitable additional cases:

(⇒): Let $\mathbf{a} \in \mathbb{H}_b^{\Delta}(\Gamma, \times_i(\sigma)) \triangleright \tau$ follow from $\mathbf{a} \in \mathbb{H}_{\pi_i(b)}^{\Delta}(\Gamma, \sigma) \triangleright \tau$ by (Proj). Suppose $\Delta \vdash \mathbf{b} : \times_i(\sigma)$ ($i = 1, 2$). Then $\Delta \vdash \pi_i(\mathbf{b}) : \sigma$. By the i.h. (c) we get $Π \triangleright Γ + Δ \vdash \mathbf{a} : τ$, where $\mathbf{a} = A(Π)$ and we are done.
If $\langle\Omega, \Omega\rangle \in \mathbf{T}(\emptyset, \omega_\times)$ follows by (Pair); then $\Pi \triangleright \vdash \langle\Omega, \Omega\rangle : \omega_\times$, and
$\langle\Omega, \Omega\rangle = \mathcal{A}(\Pi)$.

If $\langle a, \Omega \rangle \in \mathbf{T}(\Gamma, \times_1(\tau))$ follows from $a \in \mathbf{T}(\Gamma, \tau)$ by (Prod1), then by the i.h. (a) $\Gamma \vdash a : \tau$. Then by (pair1), $\exists \Pi \triangleright \Gamma \vdash \langle a, \Omega \rangle : \times_1(\tau)$, and we are done, since $\langle a, \Omega \rangle = \mathcal{A}(\Pi)$. Analogsly for (Prod2).

(=$\Leftarrow$:) 1. Let $\mathbf{a} = \pi_i \mathbf{a}'$ ($i=1,2$). By construction $\Pi$ ends by an application of the rule (proji) with premise $\Pi' \triangleright \Gamma \vdash \mathbf{a}' : \times_i(\sigma)$, where by definition $\mathbf{a}' = \mathcal{A}(\Pi')$. Moreover, $\Sigma \triangleright \Delta \vdash \mathbf{b} : \tau$ is also a left-subtree of $\Pi'$ and $\mathcal{A}(\Pi) = \pi_i \mathbf{a}'$ by definition, thus $\mathbf{H}_{\pi_i \mathbf{a}'}^{\Delta+\Gamma'}(\Theta, \sigma) \triangleright \pi \subseteq_{(\text{Proj})} \mathbf{H}_{\mathbf{a}'}^{\Delta+\Gamma'}(\Theta, \times_i(\sigma)) \triangleright \pi \subseteq_{i.h.(1)} \mathbf{H}_{\mathbf{b}}^{\Delta}(\Theta + \Gamma', \tau) \triangleright \pi$.

2. If $\mathbf{a}$ is a pair then there are three cases to consider. If $\Pi \triangleright \vdash \mathbf{a} : \omega_\times$, then $\mathbf{a} = \langle\Omega, \Omega\rangle \in_{(\text{Pair})} \mathbf{T}(\emptyset, \omega_\times)$. If $\Pi \triangleright \Gamma \vdash \mathbf{a} : \times_1(\tau)$ follows from $\Pi' \triangleright \Gamma \vdash \mathbf{a}' : \tau$ by (proj1), then $\mathbf{a} = \langle\mathbf{a}', \Omega\rangle$. We have $\mathbf{a}' \in_{i.h.(2)} \mathbf{T}(\Gamma, \tau)$, so that $\mathbf{a} \in_{(\text{Prod1})} \mathbf{T}(\Gamma, \times_1(\tau))$. The case $\Pi \triangleright \Gamma \vdash \mathbf{a} : \times_2(\tau)$ is similar.

**Theorem 4 (Soundness and Completeness).**

1. If $\mathbf{a} \in \mathbf{T}(\Gamma, \sigma)$ then, for all $t$ such that $\mathbf{a} \leq t$, $\Gamma \vdash t : \sigma$.

2. If $\Pi \triangleright \Gamma \vdash t : \sigma$ then there exists $\Pi' \triangleright \Gamma \vdash t' : \sigma$ such that $t'$ is in $\Pi'$-normal form, and $\mathcal{A}(\Pi') \in \mathbf{T}(\Gamma, \sigma)$.

*Proof.* As in the proof of Thm. 2, but using Lem. 7 ($\Rightarrow$) for soundness, Thm. 4.1 and Lem. 7 ($\Leftarrow$) for completeness.

**6 Conclusion**

We proved that the inhabitation problem is decidable for the types sys-
tems $\mathcal{M}$ and $\mathcal{P}$, based on non-idempotent intersection types, and charac-
terizing solvability for the $\lambda$-calculus and for its extension with pairs and
projections, that we call $\Lambda_\pi$, respectively. To the best of our knowledge,
solvability in $\Lambda_\pi$ had not been studied before. Our result is a first step
towards the study of further extensions of $\Lambda_\pi$, including *patterns* [11].

In fact, the logical characterization of solvability is related to the
inhabitation problem of the underlying type system. While this relation
is implicit for the $\lambda$-calculus, it can become crucial for extensions lacking
a syntactical characterization of solvability.

Concerning denotational models, it is well known that system $\mathcal{M}$ in-
duces a relational model of $\Lambda$. We aim to complete the picture studying
the semantics of $\Lambda_\pi$ through the system $\mathcal{P}$.
References

1. H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, revised edition, 1984.

2. C. Ben-Yelles. Type-assignment in the lambda-calculus; syntax and semantics. PhD thesis, University of Wales Swansea, 1979.

3. A. Bernadet and S. Lengrand. Non-idempotent intersection types and strong normalisation. *Logical Methods in Computer Science*, 9(4), 2013.

4. M. W. Bunder. The inhabitation problem for intersection types. In *CATS'08*, CRPIT 77, pages 7–14. Wollongong, NSW, Australia, 2008.

5. D. D. Carvalho. Sèmantique de la logique linéaire et temps de calcul. PhD thesis, Université de la Méditerranée Aix-Marseille 2, 2007.

6. M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. *Notre Dame J. Form. Log.*, 21(4):685–693, 1980.

7. E. De Benedetti and S. Ronchi Della Rocca. Bounding normalization time through intersection types. In *ITRS'12*, EPTCS 121, pages 48–57, 2013.

8. P. Di Gianantonio, F. Honsell, and M. Lenisa. A type assignment system for game semantics. *Theoretical Computer Science*, 398:150–169, 2008.

9. T. Ehrhard. The Scott model of linear logic is the extensional collapse of its relational model. *Theoretical Computer Science*, 424:20–45, 2012.

10. J. R. Hindley. Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Amsterdam, 2008.

11. C. B. Jay and D. Kesner. First-class patterns. *Journal of Functional Programming*, 19(2):191–225, 2009.

12. D. Kesner and D. Ventura. Quantitative types for the linear substitution calculus. In *TCS*, LNCS, Rome, Italy, 2014.

13. A. J. Kfoury. A Linearization of the Lambda-Calculus and Consequences. *Journal Logic Comp.*, 10(3):411–436, 2000.

14. A. J. Kfoury and J. B. Wells. Principality and type inference for intersection types using expansion variables. *Theoretical Computer Science*, 311(1-3):1–70, 2004.

15. J. L. Krivine. Lambda-Calculus, Types and Models. Masson, Paris, and Ellis Horwood, Hemel Hempstead, 1993.

16. T. Kurata and M. Takahashi. Decidable properties of intersection type systems. In *TLCA'95*, LNCS 902, pages 297–311, 1995.

17. H. Mairson and P. M. Neergaard. Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In *ICFP'04*, pages 138–149, 2004.

18. M. Pagani and S. Ronchi Della Rocca. Linearity, non-determinism and solvability. *Fundamenta Informaticae*, 103:358–373, 2010.

19. M. Pagani and S. Ronchi Della Rocca. Solvability in resource lambda-calculus. In *FOSSACS'10*, LNCS 6014, pages 358–373, 2010.

20. L. Paolini, M. Piccolo, and S. Ronchi Della Rocca. Logical relational lambda-models. Accepted for publication in MSCS.

21. P. Urzyczyn. The emptiness problem for intersection types. *Journal of Symbolic Logic*, 64(3):1195–1215, 1999.

22. P. Urzyczyn. Personal communication, 2014.

23. S. van Bakel. Complete restrictions of the intersection type discipline. *Theoretical Computer Science*, 102:135–163, 1992.