1–LABEL:LastPageDec. 12, 2017Aug. 03, 2018

# Inhabitation for Non-idempotent Intersection Types

Antonio Bucciarellia  ,  Delia Kesnerb  a,bIRIF, CNRS and Univ Paris-Diderot,
France<EMAIL_ADDRESS>and  Simona Ronchi Della Roccac  cDipartimento
di Informatica, Università di Torino, Italy<EMAIL_ADDRESS>In honour of
Furio Honsell, in occasion of his 60th birthday

###### Abstract.

The inhabitation problem for intersection types in $\lambda$-calculus is known
to be undecidable. We study the problem in the case of non-idempotent
intersection, considering several type assignment systems, which characterize
the solvable or the strongly normalizing $\lambda$-terms. We prove the
decidability of the inhabitation problem for all the systems considered, by
providing sound and complete inhabitation algorithms for them.

###### Key words and phrases:

Lambda-calculus, Type-Assignement Systems, Non-idempotent Intersection Types,
Inhabitation Problem

###### 1991 Mathematics Subject Classification:

F.4.1 Mathematical Logic: Lambda calculus and related systems, Proof theory.
F.3.1 Specifying and Verifying and Reasoning about Programs: Logics of
programs

##  1\. Introduction

Given a type assignment system associating types to terms of a given
programming language, two problems naturally arise, namely the typability and
the inhabitation problem (known in the literature also as emptiness problem).
In the former, given a program, one wants to know if it is possible to assign
a typing to it, in the latter, in some specular way, given a typing, one aims
for a program to which the typing can be assigned. Since types are program
specifications, the decidability of the first problem supplies tools for
proving program correctness, whereas the decidability of the second one
provides tools for program synthesis [Rehof15]. Considering the
$\lambda$-calculus as a general paradigm for functional programming languages,
a virtuous example is the simple type assignment system, for which both
problems are decidable, and which is the basis of typed functional languages,
like ML and Haskell. In this paper we study the inhabitation problem for an
extended type assignment system, based on (non-idempotent) intersection types.

Intersection types have been introduced in order to increase the typability
power of simple type assignment systems, but quite early they turned out to be
a very powerful tool for characterizing semantic properties of
$\lambda$-calculus, like solvability and strong normalization, and for
describing models of $\lambda$-calculus in various settings. Intersection
types have been presented in the literature in many variants. Historically,
one of the first versions is the one characterizing solvable terms
[CoppoDezani:NDJoFL-80, krivine93book], that we call system $\cal C$, shown in
Figure 1. In such a system, $\alpha$ denotes any basic type and the universal
type is denoted by the constant $\omega$. Intersection enjoys associativity,
commutativity, and idempotency (${\tt A}\wedge{\tt A}={\tt A}$). Typing
environments $\Gamma$ are functions from variables to types, we represent them
as lists of pairs of the form ${\tt x}:{\tt A}$, where the comma symbol is
used as set constructor. System $\cal C$ assigns types different from $\omega$
to all and only those terms having head-normal forms, which are the
syntactical counterpart of the semantic notion of solvability
[barendregt84nh]. Since it is undecidable to know if a given term is solvable
[barendregt84nh], then typability in system ${\cal C}$ (with types different
from $\omega$) is undecidable too. Moreover, the inhabitation problem for
system ${\cal C}$ has been proved to be undecidable by Urzyczyn [Urzyczyn99].
Remark that system ${\cal C}$ is not syntax directed, so it is difficult to
reason about it. Van Bakel [Bakel92] simplified system ${\cal C}$ by using
strict types, where intersection is not allowed on the right-hand side of the
arrow; his system ${\cal C}_{B}$ is presented in Figure 2, where we represent
intersection through a set constructor, and so the universal type $\omega$ as
the empty set. System ${\cal C}_{B}$ is syntax directed, i.e. there are just
three typing rules, corresponding to the three different constructors of the
$\lambda$-calculus. The systems ${\cal C}$ and ${\cal C}_{B}$ have the same
typability power, neglecting the universal type $\omega$, in the sense that a
term is typable in ${\cal C}$ by a type different form $\omega$ if and only if
it is typable in ${\cal C}_{B}$. In particular, Urzyczyn’s proof of
undecidability of the inhabitation problem for system ${\cal C}$ can be easily
adapted to system ${\cal C}_{B}$, proving that the latter is undecidable too
[UrzyczynPC].

$\begin{array}[]{ccc}\infer{\mbox{ }}{\Gamma\vdash{\tt
t}:\omega}(\mathtt{\omega})&\infer{{\tt x}:{\tt A}\in\Gamma}{\Gamma\vdash{\tt
x}:{\tt A}}(\mathtt{var}_{w})&\infer{\Gamma,{\tt x}:{\tt A}\vdash{\tt t}:{\tt
B}}{\Gamma\vdash\lambda{\tt x}.{\tt t}:{\tt A}\rightarrow{\tt
B}}(\mathtt{\rightarrow_{I}})\\\ &&\\\ \infer{\Gamma\vdash{\tt t}:{\tt
A}\rightarrow{\tt B}\quad\Gamma\vdash{\tt u}:{\tt A}}{\Gamma\vdash{\tt t}{\tt
u}:{\tt B}}(\mathtt{\rightarrow_{E}})&\infer{\Gamma\vdash{\tt t}:{\tt
A}\quad\Gamma\vdash{\tt t}:{\tt B}}{\Gamma\vdash{\tt t}:{\tt A}\wedge{\tt
B}}(\mathtt{\wedge_{I}})&\infer{\Gamma\vdash{\tt t}:{{{\tt A}}_{1}}\wedge{{\tt
A}}_{2}}{\Gamma\vdash{\tt t}:{{{\tt A}}_{i}}\ (i=1,2)}(\mathtt{\wedge_{E}})\\\
\\\ \end{array}$

Types: | Typing environments:
---|---
${\tt A}::=\alpha\mid\omega\mid{\tt A}\rightarrow{\tt A}\mid{\tt A}\wedge{\tt A}$ | $\Gamma::=\emptyset\mid\Gamma,{\tt x}:{\tt A}\ ({\tt x}\not\in{\tt dom}(\Gamma))$

Figure 1. System ${\cal C}$

$\begin{array}[]{c}\infer{{\tt x}:{\tt A}\in\Gamma\hskip
14.22636pt\sigma\in{\tt A}}{\Gamma\vdash{\tt
x}:\sigma}(\mathtt{var}_{w})\quad\quad\infer{\Gamma,{\tt x}:{\tt A}\vdash{\tt
t}:\tau}{\Gamma\vdash\lambda{\tt x}.{\tt t}:{\tt
A}\rightarrow\tau}(\mathtt{\rightarrow_{I}})\\\ \\\ \infer{\Gamma\vdash{\tt
t}:\\!\\{\sigma_{i}\\}_{i\in I}\rightarrow\tau\quad(\Gamma\vdash{\tt
u}:\sigma_{i})_{i\in I}}{\Gamma\vdash{\tt t}{\tt
u}:\tau}(\mathtt{\rightarrow_{E}})\\\ \end{array}$

$\begin{array}[]{l@{\hspace{2cm}}l }\mbox{Types:}\hfil\hskip
56.9055pt&\mbox{Typing environments:}\\\ \sigma,{\tau}::=\alpha\mid{\tt
A}\rightarrow\sigma\ (\mbox{strict types})\hfil\hskip
56.9055pt&\Gamma::=\emptyset\mid\Gamma,{\tt x}:{\tt A}\ ({\tt x}\not\in{\tt
dom}(\Gamma))\\\ {\tt A}::=\emptyset\mid\\{\sigma\\}\mid{\tt A}\cup{\tt A}\
(\mbox{set types})\hfil\hskip 56.9055pt\\\ \end{array}$

Figure 2. System ${\cal C}_{B}$

In this paper we study the inhabitation problem for non-idempotent
intersection types, i.e. considering intersection modulo commutativity and
associativity but not idempotence. It is possible to design various type
assignment systems using non idempotent intersection; we start from a system,
that we call $\mathcal{H}$, which has been introduced in [Gardner94] and
further used by De Carvalho [DeCarvalhoThesis], for the purpose of studying
the complexity of reduction. This system is particularly interesting since it
induces a denotational model of $\lambda$-calculus, in the relational
semantics setting [PPR17]. Moreover, it enjoys relevance and has a
quantitative flavor. We prove that the inhabitation problem is decidable by
exploiting the fact that types keep track faithfully of the different uses of
variables in terms, thanks to the relevance of the system. System
$\mathcal{H}$ characterizes terms having head normal form. An important result
for defining the algorithm solving the inhabitation problem for system
$\mathcal{H}$ is an approximation theorem, proved in section 3.1, saying that
a term can be assigned all and only the types that can be assigned to its
approximants. We solve the inhabitation problem for system $\mathcal{H}$ in a
constructive way, by designing 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 ${\tt t}$ such that
$\Gamma\vdash{\tt t}:\sigma$ can be generated. Then we extend the system with
a weakening rule, yielding system $\mathcal{H}_{w}$, and we prove that
inhabitation remains decidable for such an extension.

In the second part of this paper we present some non-idempotent intersection
types systems characterizing strong normalization, and we show that the
inhabitation problem is decidable for each of them. We take into account
different systems present in literature, also when they do not enjoy good
properties like subject reduction, with the aim of performing a complete
analysis.

#### Interest of the problem

As said before, inhabitation has been used for program synthesis (see for
example [Rehof15]), and it is a technical problem interesting by itself. The
results of this paper show in particular that the two classical problems about
type assignment systems, namely typability and inhabitation, are unrelated
problems, giving a first example of a system for which the first one is
undecidable while the second one is decidable. This fact suggests interesting
questions about the relation between program correctness and program
synthesis.

#### Related work

Various restrictions of the standard intersection type system have been shown
to have decidable inhabitation problems [KurataT95, Urzyczyn10]. The approach
is substantially different from the one used in this work, since in all cases
intersection is idempotent, and the decidability is obtained by restricting
the use of rules $(\mathtt{\wedge_{I}})$ and $(\mathtt{\wedge_{E}})$, so that
the corresponding type assignment system does not characterize interesting
classes of terms, anymore. Recently a new notion of intersection type system
with bounded dimension has been introduced [DBLP:conf/popl/DudenhefnerR17], it
is based on decorations of terms called elaborations, that remember some
information about their typing derivation, and allow a stratification of typed
terms. It has been proved that inhabitation (where inhabitants are decorated
terms) is decidable, and its complexity is EXPSPACE complete. Previously it
had been proved in [Kus07] that the inhabitation of rank two intersection
types is EXPTIME hard.

A preliminary version of our inhabitation algorithm for system $\mathcal{H}$
has been presented in [DBLP:conf/ifipTCS/BucciarelliKR14]. The present paper
simplifies this first algorithm (see discussion in Section
LABEL:s:inhabitation) and extends inhabitation to other systems, as explained
before.

#### Non-idempotent intersection types

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{H}$ is not new: it is the system of Gardner [Gardner94] and
de Carvalho [DeCarvalhoThesis], and it is an instance of the class of the
essential $\lambda$-models defined in [PPR17], 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 [DebeneRonchiITRS12]), to supply new characterizations of strong
normalization [BernadetL13, KV14], to study type inference [kfouryWells04,
MairsonNeergaard04], to study linearity [kfoury00], to characterize
solvability in the resource $\lambda$-calculus [pagani10fossacs,
PaganiRonchi:2010FI], to characterize the set of hereditary head-normalizing
infinite $\lambda$-terms [Vial17]. Moreover intersection without idempotency,
commutativity nor associativity, has been used to study the game semantics of
a typed $\lambda$-calculus [DiGia08]. Non-idempotent types are also useful to
prove observational equivalence of programming languages [Kesner16,
BalabonskiBBK17]. A unified model-theoretical approach covering both the
relevant and non-relevant cases, and unveiling the relations between them, is
presented in [Ehrhard12]. Non-idempotent (intersection and union) types have
also been proposed [KV17] to characterize different operational properties of
the $\lambda\mu$-calculus, a computational interpretation of classical logic
in natural deduction style. A survey on non-idempotent intersection type
assignement systems for the $\lambda$-calculus and the proof techniques for
them can be found in [BKV17].

#### Organization of the paper

Section 2 contains preliminary notions about the $\lambda$-calculus; Section 3
presents the system $\mathcal{H}$ and its inhabitation algorithm; Section
LABEL:section:sn presents the systems $\mathcal{H}_{e,w}$ and
$\mathcal{S}_{w}$, both characterizing strong normalisation, and their
respective inhabitation algorithms. Finally, Section LABEL:sec:concl proposes
some conclusions.

##  2\. Preliminaries

#### The $\lambda$-calculus

Terms and contexts of the $\lambda$-calculus are generated by the following
grammars, respectively:

${\tt t},{\tt u},{\tt v}::={\tt x}\mid\lambda{\tt x}.{\tt t}\mid{\tt t}{\tt
u}\quad\quad\quad\quad{\tt C}::=\square\mid\lambda{\tt x}.{\tt C}\mid{\tt
C}{\tt t}\mid{\tt t}{\tt C}$

where ${\tt x}$ ranges over a countable set of variables. As usual, the
application symbol associates to the left; to avoid ambiguities in the
notation we may use parentheses as e.g. in ${\tt x}({\tt x}{\tt y})$. We use
the notation ${\tt I}$ for the identity function $\lambda{\tt x}.{\tt x}$ and
${\tt D}_{\tt up}$ for $\lambda{\tt x}.{\tt x}{\tt x}$, which duplicates its
argument. We write ${\tt fv}({\tt t})$ to denote the set of free variable of
${\tt t}$ and $=$ for the syntactical equality on terms, modulo renaming of
bound variables. The notation $\lambda{\tt x}{\tt y}.{\tt t}$ is used as an
abbreviation for $\lambda{\tt x}.\lambda{\tt y}.{\tt t}$. We assume an hygiene
condition on variables, i.e. free and bound variables have different names, as
well as variables bound by different binders. Given a context ${\tt C}$ and a
term ${\tt t}$, ${\tt C}[{\tt t}]$ denotes the term obtained by replacing the
unique occurrence of $\square$ in ${\tt C}$ by ${\tt t}$, thus potentially
allowing the capture of free variables of ${\tt t}$. A context ${\tt C}$ is
closing for ${\tt t}$ if ${\tt C}[{\tt t}]$ is closed, i.e. if ${\tt fv}({\tt
C}[{\tt t}])=\emptyset$.

The $\beta$-reduction, denoted by $\rightarrow_{\beta}$, is the contextual
closure of the rule:

$(\lambda{\tt x}.{\tt t}){\tt u}\rightarrow{\tt t}\\{{\tt u}/{\tt x}\\}$

where ${\tt t}\\{{\tt u}/{\tt x}\\}$ denotes the capture-free replacement of
${\tt x}$ by ${\tt u}$ in ${\tt t}$. A term of the form $(\lambda{\tt x}.{\tt
t}){\tt u}$ is called a $\beta$-redex. We use $\rightarrow^{*}_{\beta}$ to
denote the reflexive and transitive closure of $\rightarrow_{\beta}$, and
$=_{\beta}$ the transitive, reflexive and symmetric closure of
$\rightarrow_{\beta}$.

#### Normal forms

A term ${\tt t}$ is in $\beta$-normal form, or just in normal form (nf), when
it does not contain any $\beta$-redex, it has normal form if it can be reduced
to a term in normal form, it is strongly normalizing, written ${\tt t}\in SN$,
if every $\beta$-reduction sequence starting from it eventually stops. Terms
in normal form (${\mathcal{F}}$) are generated by the following grammar:

${\cal F}::=\lambda{\tt x}.{\cal F}\mid{\cal H}\quad\quad\quad\quad\quad{\cal
H}::={\tt x}\mid{\cal H}{\cal F}$

#### Head-normal forms

The notion of head-normal form (hnf) is the syntactical counter part of the
well-known notion of solvability for the $\lambda$-calculus, being a term
${\tt t}$ solvable iff there is a closing context ${\tt C}$ for ${\tt t}$ of
the shape $(\lambda{\tt x}_{1}...{\tt x}_{n}.\square){\tt t}_{1}...{\tt
t}_{m}$ (called a head-context) such that ${\tt C}[{\tt t}]=_{\beta}{\tt I}$.
A $\lambda$-term is in hnf if it is generated by the following grammar ${\cal
J}$, it has hnf if it $\beta$-reduces to a term which is in hnf.

${\cal J}::=\lambda{\tt x}.{\cal J}\mid{\cal K}\quad\quad\quad\quad\quad{\cal
K}::={\tt x}\mid{\cal K}{\tt t}$

For example, ${\tt t}=(\lambda{\tt y}.{\tt y}){\tt x}{\tt D}_{\tt up}$ is not
in hnf but $\beta$-reduces to ${\tt x}{\tt D}_{\tt up}$ which is in hnf, thus
${\tt t}$ has a hnf. The term ${\tt I}$ is solvable while ${\tt D}_{\tt
up}{\tt D}_{\tt up}$ is not.

#### Approximate normal forms

Approximate normal forms [barendregt84nh] are normal forms in an extended
calculus. Let $\Lambda\Omega$ be the $\lambda$-calculus enriched with a
constant $\Omega$, and let $\rightarrow_{\beta\omega}$ be the contextual
closure of the $\beta$-reduction plus the following two reduction rules:

$\Omega{\tt t}\rightarrow\Omega\quad\quad\quad\quad\quad\lambda{\tt
x}.\Omega\rightarrow\Omega$

Normal forms of $\Lambda\Omega$ with respect to $\rightarrow_{\beta\omega}$
are defined through the following grammar:

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

Elements generated by the three grammar rules above are called approximate
normal forms, ${\cal N}$ approximate normal forms and ${\cal L}$ approximate
normal forms, respectively. E.g. both $\lambda{\tt x}{\tt y}.{\tt
x}\Omega(\lambda z.{\tt y}{\tt z}\Omega)$ and $\lambda{\tt x}{\tt y}.{\tt
x}\Omega\Omega$ are approximate normal forms, while $\lambda{\tt x}.\Omega$
and $\lambda{\tt x}.{\tt x}{\tt y}(\Omega{\tt y})$ are not, since they reduce
respectively to $\Omega$ and $\lambda{\tt x}.{\tt x}{\tt y}\Omega$.

#### Approximants of a term

Approximate normal forms can be ordered by the smallest contextual order
$\leq$ such that $\Omega\leq{\tt a}$, for all ${\tt a}$. By abuse of notation,
we write ${\tt a}\leq{\tt t}$ to compare an approximate normal form ${\tt a}$
with a term ${\tt t}$ when ${\tt t}$ is obtained from ${\tt a}$ by replacing
all the occurrences of $\Omega$ by arbitrary terms. Let $\bigvee$ denote the
least upper bound w.r.t. $\leq$. We use the predicate $\uparrow_{i\in I}{\tt
a}_{i}$ to state that $\bigvee\\{{\tt a}_{i}\\}_{i\in I}$ does exist.

The set of approximants of a term ${\tt t}$ is given by:

${\mathcal{A}}({\tt t})=\\{{\tt a}\ |\ \exists{\tt u}\ {\tt
t}\rightarrow_{\beta}^{*}{\tt u}\mbox{ and }{\tt a}\leq{\tt u}\\}$

It is easy to check that, for every ${\tt t}$ and ${\tt a}_{1},\ldots{\tt
a}_{n}\in{\mathcal{A}}({\tt t})$, $\uparrow_{i\in\\{1,\ldots,n\\}}{\tt
a}_{i}$. Thus for example, ${\mathcal{A}}(\lambda{\tt x}.{\tt D}_{\tt up}({\tt
I}{\tt I}))=\\{\Omega,\lambda{\tt x}.\Omega,\lambda{\tt x}{\tt
y}.\Omega,\lambda{\tt x}{\tt y}.{\tt y}\\}$ and
$\bigvee{\mathcal{A}}(\lambda{\tt x}.{\tt D}_{\tt up}({\tt I}{\tt
I}))=\lambda{\tt x}{\tt y}.{\tt y}$.

In many well-behaved models, it is possible to relate the interpretation of a
term to the interpretation of its approximants, the first example being in
[wadsworth76siamjc]. We are going to show such a property, known as the
approximation theorem, for the type assignment system $\mathcal{H}$ presented
below.

##  3\. Systems characterizing head normalization

In this section we consider the inhabitation problem with respect to an
intersection type system for the $\lambda$-calculus that characterizes head-
normal forms. The essential feature of this type system that makes its
inhabitation problem decidable is the non-idempotency of the intersection. The
typing rules are relevant (i.e. the weakening is not allowed), and we
represent non-idempotent intersections as multisets of types. Moreover, in
order to work with a syntax-directed system, we restrict the set of types to
the strict ones [Bakel92].

  1. (1)

The set of types is defined by the following grammar:

$\begin{array}[]{llllll}\sigma,\tau,\rho&::=&\alpha\mid{\tt
A}\rightarrow\tau&(\mbox{types})\\\ {\tt A},{\tt B}&::=&[\sigma_{i}]_{i\in
I}&(\mbox{multiset types})\end{array}$

where $\alpha$ ranges over a countable set of base types. Multiset types are
associated to a finite, possibly empty, set $I$ of indices; the empty multiset
corresponds to the case $I=\emptyset$ and is simply denoted by $[\,]$. To
avoid an excessive number of parentheses, we use for example ${\tt
A}\rightarrow{\tt B}\rightarrow\sigma$ instead of ${\tt A}\rightarrow({\tt
B}\rightarrow\sigma)$.

  2. (2)

Typing environments, which are also simply called environments, written
$\Gamma,\Delta$, are functions from variables to multiset types, assigning the
empty multiset to almost all the variables. We use the symbol $\emptyset$ to
denote the empty typing environment. The domain of $\Gamma$, written ${\tt
dom}(\Gamma)$, is the set of variables whose image is different from $[\,]$.
Given environments $\Gamma$ and $\Delta$, $\Gamma+\Delta$ is the environment
mapping ${\tt x}$ to $\Gamma({\tt x})\uplus\Delta({\tt x})$, where $\uplus$
denotes multiset union; $+_{i\in I}\Delta_{i}$ denotes its obvious extension
to a non-binary case, where the resulting environment has empty domain in the
case $I=\emptyset$. We write $\Gamma\setminus{\tt x}$ for the environment
assigning $[\,]$ to ${\tt x}$, and acting as $\Gamma$ otherwise; ${{\tt
x}}_{1}:{{\tt A}}_{1},\ldots,{{\tt x}}_{n}:{{\tt A}}_{n}$ is the environment
assigning ${{\tt A}}_{i}$ to ${{\tt x}}_{i}$, for $1\leq i\leq n$, and $[\,]$
to any other variable.

  3. (3)

A typing judgement is a triple either of the form $\Gamma\vdash{\tt t}:\sigma$
or $\Gamma\vdash{\tt t}:{\tt A}$. The type system $\mathcal{H}$ is given in
Figure 3.

$\begin{array}[]{c}\infer{\mbox{}}{{\tt x}:[\rho]\vdash{\tt x}:\rho}\
(\mathtt{var})\quad\quad\infer{\Gamma\vdash{\tt t}:\tau}{\Gamma\setminus{\tt
x}\vdash\lambda{\tt x}.{\tt t}:\Gamma({\tt x})\rightarrow\tau}\
(\mathtt{\rightarrow_{I}})\\\ \\\ \infer{(\Delta_{i}\vdash{\tt
t}:\sigma_{i})_{i\in I}}{+_{i\in I}\Delta_{i}\vdash{\tt t}:[\sigma_{i}]_{i\in
I}}(\mathtt{m})\quad\quad\infer{\Gamma\vdash{\tt t}:{\tt
A}\rightarrow\tau\hskip 14.22636pt\Delta\vdash{\tt u}:{\tt
A}}{\Gamma+\Delta\vdash{\tt t}{\tt u}:\tau}\
(\mathtt{\rightarrow_{E}})\end{array}$

Figure 3. The type assignment system $\mathcal{H}$ for the $\lambda$-calculus

Rules $(\mathtt{var})$ and $(\mathtt{\rightarrow_{I}})$ are self explanatory.
Rule $(\mathtt{m})$ can be considered as an auxiliary rule, i.e. it has no
logical meaning but just collects together different typings for the same
term; remark that it cannot be iterated. Rule $(\mathtt{\rightarrow_{E}})$ has
two premises, the one for ${\tt t}$ (resp. ${\tt u}$) is called the major
(resp. minor) premise. In the case ${\tt A}=[\,]$, this rule allows to type a
term without giving types to all its subterms, and in particular it allows to
type an application whose argument is unsolvable. For example, the judgement
${\tt x}:[[\,]\rightarrow\alpha]\vdash{\tt x}({\tt D}_{\tt up}{\tt D}_{\tt
up}):\alpha$ turns to be derivable by taking $I=\emptyset$ in rule
$(\mathtt{m})$ :

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
46.39671pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=92.79343pt\hbox{\kern
3.00003pt${(\mathtt{var})}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\tt
x}:[[\,]\rightarrow\alpha]\vdash{\tt x}:[\,]\rightarrow\alpha}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 14.22636pt\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
28.58327pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=57.16653pt\hbox{\kern
3.00003pt${(\mathtt{m})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\emptyset\vdash{\tt D}_{\tt up}{\tt D}_{\tt
up}:[\,]}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=270.15187pt\hbox{\kern
3.00003pt${(\mathtt{\rightarrow_{E}})}$}}}\hbox{\kern
79.818pt\hbox{$\displaystyle{{\tt x}:[[\,]\rightarrow\alpha]\vdash{\tt x}({\tt
D}_{\tt up}{\tt D}_{\tt up}):\alpha}$}}}}$

This feature is shared by all the intersection type systems characterizing
solvability.

We write $\Pi\triangleright\Gamma\vdash_{\mathcal{H}}{\tt t}:\sigma$, or
simply $\Pi\triangleright\Gamma\vdash{\tt t}:\sigma$ when $\mathcal{H}$ is
clear from the context, to denote a type derivation $\Pi$ in system
$\mathcal{H}$ with conclusion $\Gamma\vdash{\tt t}:\sigma$. We call ${\tt t}$
the subject of $\Pi$. A term ${\tt t}$ is said to be $\mathcal{H}$-typable if
there exists a derivation $\Pi\triangleright\Gamma\vdash_{\mathcal{H}}{\tt
t}:\sigma$. By abuse of notation, we omit sometimes the name of the derivation
by writing simply $\Gamma\vdash{\tt t}:\sigma$ to denote the existence of some
derivation with conclusion $\Gamma\vdash{\tt t}:\sigma$. We extend these
notations to judgements of the shape $\Gamma\vdash{\tt t}:{\tt A}$, when we
want to reason by induction on the structure of a proof.

One important tool is going to be used in the proofs:  The measure of a
derivation $\Pi$, written ${\tt meas}(\Pi)$, is the number of rule
applications in $\Pi$, except rule $(\mathtt{m})$.

Note that the definition of the measure of a type derivation reflects the fact
that $(\mathtt{m})$ is an auxiliary rule. The notion of measure of a
derivation provides an original, combinatorial proof of the fact that typed
terms do have hnf. In fact the fundamental subject reduction property holds as
follows: if $\Pi\triangleright\Gamma\vdash{\tt t}:\sigma$ and ${\tt
t}\rightarrow_{\beta}{\tt u}$, then
$\Pi^{\prime}\triangleright\Gamma\vdash{\tt u}:\sigma$, with the peculiarity
that the measure of $\Pi^{\prime}$ is strictly smaller than that of $\Pi$
whenever the reduction ${\tt t}\rightarrow_{\beta}{\tt u}$ takes place in a
subterm of ${\tt t}$ which is typed in $\Pi$. A formal definition of typed
positions follows.

  * •

The set $\mathtt{o}(t)$ of positions of ${\tt t}$ is the set of contexts ${\tt
C}$ such that there exists a term ${\tt u}$ verifying ${\tt C}[{\tt u}]={\tt
t}$, ${\tt u}$ being the subterm of ${\tt t}$ at position ${\tt C}$.

  * •

Given $\Pi\triangleright\Gamma\vdash{\tt t}:\sigma$, the set
$\mathtt{to}(\Pi)\subseteq\mathtt{o}({\tt t})$ of typed positions of ${\tt t}$
in $\Pi$ is defined by induction on the structure of $\Pi$ as follows:

    * –

$\mathtt{to}(\Pi)=\\{\square\\}$ if $\Pi$ is an instance of the axiom.

    * –

$\mathtt{to}(\Pi)=\\{\square\\}\cup\\{\lambda{\tt x}.{\tt C}\ |\ {\tt
C}\in\mathtt{to}(\Pi^{\prime})\\}$ if the last rule of $\Pi$ is
$(\mathtt{\rightarrow_{I}})$, its subject is $\lambda{\tt x}.{\tt u}$ and its
premise is $\Pi^{\prime}$.

    * –

$\mathtt{to}(\Pi)=\\{\square\\}\cup\\{{\tt C}{\tt v}\ |\ {\tt
C}\in\mathtt{to}(\Pi^{\prime})\\}\cup\\{{\tt u}{\tt C}\ |\ {\tt
C}\in\mathtt{to}(\Delta)\\}$ if the last rule of $\Pi$ is
$(\mathtt{\rightarrow_{E}})$, its subject is ${\tt u}{\tt v}$, $\Pi^{\prime}$
and $\Delta$ are the major and minor premises of $\Pi$ respectively.

    * –

$\mathtt{to}(\Pi)=\bigcup_{i\in I}\\{{\tt C}\ |\ {\tt
C}\in\mathtt{to}(\Pi^{\prime}_{i})\\}$ if the last rule of $\Pi$ is
$(\mathtt{m})$, and $(\Pi^{\prime}_{i})_{i\in I}$ are its premises. A
particular case is when $I=\emptyset$, in which case
$\mathtt{to}(\Pi)=\emptyset$. This coincides with the fact that terms typed by
an empty $(\mathtt{m})$ rule are semantically untyped.

We say that the subterm of ${\tt t}$ at position ${\tt C}$ is typed in $\Pi$
if ${\tt C}$ is a typed position of ${\tt t}$ in $\Pi$.

  * •

Given $\Pi\triangleright\Gamma\vdash{\tt t}:\sigma$ (resp.
$\Pi\triangleright\Gamma\vdash{\tt t}:{\tt A}$), we say that ${\tt t}$ is in
$\Pi$-normal form, written $\Pi\triangleright_{\tt nf}\Gamma\vdash{\tt
t}:\sigma$ (resp. $\Pi\triangleright_{\tt nf}\Gamma\vdash{\tt t}:{\tt A}$), if
for all ${\tt C}\in\mathtt{to}(\Pi)$, ${\tt t}={\tt C}[{\tt u}]$ implies ${\tt
u}$ is not a redex.

Consider the following derivation $\Pi$, where
$\sigma:=[\alpha_{0},\alpha_{1}]\rightarrow[\,]\rightarrow\tau$:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
27.93619pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=55.87238pt\hbox{\kern
3.00003pt${(\mathtt{var})}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\tt
x}:[\sigma]\vdash{\tt x}:\sigma}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
31.41908pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=62.83817pt\hbox{\kern
3.00003pt${(\mathtt{var})}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\tt
y}:[\alpha_{0}]\vdash{\tt y}:\alpha_{0}}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 31.41908pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=62.83817pt\hbox{\kern
3.00003pt${(\mathtt{var})}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\tt
y}:[\alpha_{1}]\vdash{\tt y}:\alpha_{1}}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=236.94745pt\hbox{\kern
3.00003pt${(\mathtt{m})}$}}}\hbox{\kern 70.63542pt\hbox{$\displaystyle{{\tt
y}:[\alpha_{0},\alpha_{1}]\vdash{\tt y}:[\alpha_{0},\alpha_{1}]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=398.78537pt\hbox{\kern
3.00003pt${(\mathtt{\rightarrow_{E}})}$}}}\hbox{\kern
137.37535pt\hbox{$\displaystyle{{\tt x}:[\sigma],{\tt
y}:[\alpha_{0},\alpha_{1}]\vdash{\tt x}{\tt y}:[\,]\rightarrow\tau}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
23.45825pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=46.9165pt\hbox{\kern
3.00003pt${(\mathtt{m})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\emptyset\vdash{\tt I}{\tt D}_{\tt
up}:[\,]}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=444.59314pt\hbox{\kern
3.00003pt${(\mathtt{\rightarrow_{E}})}$}}}\hbox{\kern
156.54303pt\hbox{$\displaystyle{{\tt x}:[\sigma],{\tt
y}:[\alpha_{0},\alpha_{1}]\vdash{\tt x}{\tt y}({\tt I}{\tt D}_{\tt
up}):\tau}$}}}}$

Then,

  * •

${\tt meas}(\Pi)=5$.

  * •

$\mathtt{to}(\Pi)=\\{\Box,\Box{\tt y}({\tt I}{\tt D}_{\tt up}),{\tt
x}\Box({\tt I}{\tt D}_{\tt up}),\Box({\tt I}{\tt D}_{\tt up})\\}$.

  * •

${\tt x}{\tt y}({\tt I}{\tt D}_{\tt up})$ is in $\Pi$-normal form (since its
only redex ${\tt I}{\tt D}_{\tt up}$ is untyped).

######  Theorem 1.

  1. (1)

(Subject reduction and expansion) $\Gamma\vdash{\tt t}:\sigma$ and ${\tt
t}=_{\beta}{\tt u}$ imply $\Gamma\vdash{\tt u}:\sigma$.

  2. (2)

(Characterization) ${\tt t}$ is $\mathcal{H}$-typable if and only if ${\tt t}$
has hnf.

######  Proof 3.1.

See [DeCarvalhoThesis, BKV17]. In particular, the proof of subject reduction
is based on the weighted subject reduction property that
$\Pi\triangleright\Gamma\vdash{\tt t}:\sigma$ and ${\tt
t}\rightarrow_{\beta}{\tt u}$ imply
$\Pi^{\prime}\triangleright\Gamma\vdash{\tt u}:\sigma$, where ${\tt
meas}(\Pi^{\prime})\leq{\tt meas}(\Pi)$. Moreover, if the reduced redex is
typed in $\Pi$, then ${\tt meas}(\Pi^{\prime})<{\tt meas}(\Pi)$. ∎

As a matter of fact, the two properties stated in the theorem above may be
proved using a semantic shortcut: in [PPR17] the class of essential type
systems is introduced, and it is shown that such systems supply a logical
description of the linear relational models of the $\lambda$-calculus, in the
sense of [bucciarelli07csl]. Since the type system $\mathcal{H}$ is an
instance of this class, both statements of Theorem 1 are particular cases of
the results proved in [PPR17].

###  3.1. The key role of approximants

System $\mathcal{H}$ assigns types to terms without giving types to all their
subterms (cf. the rule $(\mathtt{\rightarrow_{E}})$ in case ${\tt A}=[\,]$).
So in order to reconstruct all the possible subjects of derivations we need a
notation for these untyped subterms, which is supplied by the notion of
approximate normal forms introduced in Section 2. As a consequence, some
notions previously defined for terms, naturally apply for approximants too.
Thus for example, given $\Pi\triangleright\Gamma\vdash{\tt a}:\sigma$ or
$\Pi\triangleright\Gamma\vdash{\tt a}:{\tt A}$, ${\tt a}$ is said to be in
$\Pi$-normal form according to Definition 3. But remark that every typing
derivation of an approximant is necessarily in normal form. More precisely, if
$\Pi\triangleright\Gamma\vdash{\tt a}:\sigma$ or
$\Pi\triangleright\Gamma\vdash{\tt a}:{\tt A}$, then ${\tt a}$ is in $\Pi$
normal form. Quite surprisingly, $\Pi\triangleright\Gamma\vdash{\tt
a}:\sigma$, ${\tt a}\leq{\tt t}$ and
$\Pi^{\prime}\triangleright\Gamma\vdash{\tt t}:\sigma$ do not imply that ${\tt
t}$ is in $\Pi^{\prime}$ normal form, as the following example shows.

Let ${\tt a}={\tt x}\Omega({\tt x}{\tt y}{\tt y})\leq{\tt x}({\tt I}{\tt
x})({\tt x}{\tt y}{\tt y})={\tt t}$. Let $\Gamma={\tt
x}:[\sigma_{1},\sigma_{2}],{\tt y}:[\alpha,\alpha]$, where
$\sigma_{1}=[\,]\rightarrow[\alpha]\rightarrow\alpha$ and
$\sigma_{2}=[\alpha]\rightarrow[\alpha]\rightarrow\alpha$. There are type
derivations $\Pi\triangleright\Gamma\vdash{\tt a}:\alpha$ (given on the top)
and $\Pi^{\prime}\triangleright\Gamma\vdash{\tt t}:\alpha$ (given in the
bottom) such that ${\tt a}$ is in $\Pi$-normal form but ${\tt t}$ is not in
$\Pi^{\prime}$-normal form.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
30.73619pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=61.47238pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\tt x}:[\sigma_{1}]\vdash{\tt
x}:\sigma_{1}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip 14.22636pt\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 19.72209pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=39.44418pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\emptyset\vdash\Omega:[\,]}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=183.58058pt\hbox{}}}\hbox{\kern
47.24753pt\hbox{$\displaystyle{{\tt x}:[\sigma_{1}]\vdash{\tt
x}\Omega:[\alpha]\rightarrow\alpha}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\hskip 14.22636pt\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
30.73619pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=61.47238pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\tt x}:[\sigma_{2}]\vdash{\tt
x}:\sigma_{2}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip 14.22636pt\Pi_{\tt
y}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=120.37315pt\hbox{}}}\hbox{\kern
1.61201pt\hbox{$\displaystyle{{\tt x}:[\sigma_{2}],{\tt y}:[\alpha]\vdash{\tt
x}{\tt y}:[\alpha]\rightarrow\alpha}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\hskip 14.22636pt\Pi_{\tt y}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=179.27393pt\hbox{}}}\hbox{\kern
34.2568pt\hbox{$\displaystyle{{\tt x}:[\sigma_{2}],{\tt
y}:[\alpha,\alpha]\vdash{\tt x}{\tt y}{\tt y}:\alpha}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=213.49275pt\hbox{}}}\hbox{\kern
48.58842pt\hbox{$\displaystyle{{\tt x}:[\sigma_{2}],{\tt
y}:[\alpha,\alpha]\vdash{\tt x}{\tt y}{\tt y}:[\alpha]}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=474.73735pt\hbox{}}}\hbox{\kern
165.37033pt\hbox{$\displaystyle{{\tt x}:[\sigma_{1},\sigma_{2}],{\tt
y}:[\alpha,\alpha]\vdash{\tt x}\Omega({\tt x}{\tt y}{\tt y}):\alpha}$}}}}$

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
30.73619pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=61.47238pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\tt x}:[\sigma_{2}]\vdash{\tt
x}:\sigma_{2}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip 14.22636pt\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
27.78572pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=55.57144pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\tt z}:[\alpha]\vdash{\tt z}:\alpha}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=89.79027pt\hbox{}}}\hbox{\kern
16.13718pt\hbox{$\displaystyle{\emptyset\vdash{\tt
I}:[\alpha]\rightarrow\alpha}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip
14.22636pt\Pi_{\tt y}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=148.69104pt\hbox{}}}\hbox{\kern
43.92088pt\hbox{$\displaystyle{{\tt y}:[\alpha]\vdash{\tt I}{\tt
y}:\alpha}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=182.90987pt\hbox{}}}\hbox{\kern
58.2525pt\hbox{$\displaystyle{{\tt y}:[\alpha]\vdash{\tt I}{\tt
y}:[\alpha]}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=327.04626pt\hbox{}}}\hbox{\kern
99.25412pt\hbox{$\displaystyle{{\tt x}:[\sigma_{2}],{\tt y}:[\alpha]\vdash{\tt
x}({\tt I}{\tt y}):[\alpha]\rightarrow\alpha}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 14.22636pt\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
30.73619pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=61.47238pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\tt x}:[\sigma_{1}]\vdash{\tt
x}:\sigma_{1}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip 14.22636pt\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 18.74988pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=37.49976pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{\emptyset\vdash{\tt y}:[\,]}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=181.63615pt\hbox{}}}\hbox{\kern
47.24753pt\hbox{$\displaystyle{{\tt x}:[\sigma_{1}]\vdash{\tt x}{\tt
y}:[\alpha]\rightarrow\alpha}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip
14.22636pt\Pi_{\tt y}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=240.53693pt\hbox{}}}\hbox{\kern
70.30902pt\hbox{$\displaystyle{{\tt x}:[\sigma_{1}],{\tt y}:[\alpha]\vdash{\tt
x}{\tt y}{\tt y}:\alpha}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=274.75575pt\hbox{}}}\hbox{\kern
84.64064pt\hbox{$\displaystyle{{\tt x}:[\sigma_{1}],{\tt y}:[\alpha]\vdash{\tt
x}{\tt y}{\tt y}:[\alpha]}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=679.46603pt\hbox{}}}\hbox{\kern
263.01244pt\hbox{$\displaystyle{{\tt x}:[\sigma_{1},\sigma_{2}],{\tt
y}:[\alpha,\alpha]\vdash{\tt x}({\tt I}{\tt y})({\tt x}{\tt y}{\tt
y}):\alpha}$}}}}$

where $\Pi_{\tt y}$ denotes the following subderivation

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
28.61908pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=57.23816pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{{\tt y}:[\alpha]\vdash{\tt y}:\alpha}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=91.45699pt\hbox{}}}\hbox{\kern
14.33162pt\hbox{$\displaystyle{{\tt y}:[\alpha]\vdash{\tt y}:[\alpha]}$}}}}$

Given $\Pi\triangleright\Gamma\vdash{\tt t}:\tau$, where ${\tt t}$ is in
$\Pi$-normal form, we denote by ${\mathcal{A}}(\Pi)$ the least approximate
normal form ${\tt b}$ of ${\tt t}$ such that
$\Pi\triangleright\Gamma\vdash{\tt b}:\tau$. Formally:

Given $\Pi\triangleright_{\tt nf}\Gamma\vdash{\tt t}:\sigma$, the approximate
normal form ${\mathcal{A}}(\Pi)\in{\mathcal{A}}({\tt t})$, called the
approximant of $\Pi$, is defined by induction on the structure of $\Pi$ as
follows:

  * •

If the last rule of $\Pi$ is $(\mathtt{var})$, then
$\Pi\triangleright\Gamma\vdash{\tt x}:\sigma$, and ${\mathcal{A}}(\Pi):={\tt
x}$.

  * •

If the last rule of $\Pi$ is $(\mathtt{\rightarrow_{I}})$, then $\sigma={\tt
A}\rightarrow\rho$ and $\Pi\triangleright\Gamma\vdash\lambda{\tt x}.{\tt
t}:{\tt A}\rightarrow\rho$ follows from $\Pi^{\prime}\triangleright\Gamma,{\tt
x}:{\tt A}\vdash{\tt t}:\rho$, then ${\mathcal{A}}(\Pi):=\lambda{\tt
x}.{\mathcal{A}}(\Pi^{\prime})$, ${\tt t}$ being in $\Pi^{\prime}$-normal
form.

  * •

If the last rule of $\Pi$ is $(\mathtt{\rightarrow_{E}})$,
$\Pi\triangleright\Gamma+\Delta\vdash{\tt v}{\tt u}:\sigma$ with premises
$\Pi^{\prime}\triangleright\Gamma\vdash{\tt v}:{\tt A}\to\sigma$ and
$\Pi^{\prime\prime}\triangleright\Delta\vdash{\tt u}:{\tt A}$, so by induction
${\mathcal{A}}(\Pi^{\prime})\in{\mathcal{A}}({\tt v})$ and $\\\
Ap(\Pi^{\prime\prime})\in{\mathcal{A}}({\tt u})$. Moreover the hypothesis that
${\tt v}{\tt u}$ is in $\Pi$-normal form implies that ${\tt v}$ is of the form
${\tt x}{\tt v}_{1}\ldots{\tt v}_{n}$, so that
${\mathcal{A}}(\Pi):={\mathcal{A}}(\Pi^{\prime}){\mathcal{A}}(\Pi^{\prime\prime})\in{\mathcal{A}}({\tt
v}{\tt u})$.

  * •

If the last rule of $\Pi$ is $(\mathtt{m})$, then
$\Pi\triangleright\Gamma\vdash{\tt u}:{\tt A}$ follows from
$(\Pi_{i}\triangleright\Gamma_{i}\vdash{\tt u}:\sigma_{i})_{i\in I}$, then
${\mathcal{A}}(\Pi)=\bigvee_{i\in I}{\mathcal{A}}(\Pi_{i})$. In fact
$\uparrow_{i\in I}{\mathcal{A}}(\Pi_{i})$, since
${\mathcal{A}}(\Pi_{i})\in{\mathcal{A}}({\tt u})$, for all $i\in I$.

Remark that in the last case the approximate normal form corresponding to the
case $I=\emptyset$ is $\Omega$. Coming back to the derivation $\Pi$ in Example
3, we have ${\mathcal{A}}(\Pi)={\tt x}{\tt y}\Omega$. More generally, given
$\Pi\triangleright_{\tt nf}\Gamma\vdash{\tt t}:\sigma$, the approximant
${\mathcal{A}}(\Pi)$ can be obtained from ${\tt t}$ by replacing all its
maximal subterms untyped in $\Pi$ by $\Omega$.

Simple inductions on $\Pi$ allow to show the following properties:

######  Proposition 2.

  1. (1)

Let $\Pi\triangleright\Gamma\vdash{\tt a}:\sigma$. If ${\tt a}\leq{\tt b}$
(resp. ${\tt a}\leq{\tt t}$) then there exists $\Pi^{\prime}$ such that
$\Pi^{\prime}\triangleright\Gamma\vdash{\tt b}:\sigma$ (resp.
$\Pi^{\prime}\triangleright_{\tt nf}\Gamma\vdash{\tt t}:\sigma$) and
${\mathcal{A}}(\Pi^{\prime})={\mathcal{A}}(\Pi)$.

  2. (2)

If $\Pi\triangleright\Gamma\vdash{\tt a}:\sigma$ or $\Pi\triangleright_{\tt
nf}\Gamma\vdash{\tt t}:\sigma$, then there exists
$\Pi^{\prime}\triangleright\Gamma\vdash{\mathcal{A}}(\Pi):\sigma$ and
${\mathcal{A}}(\Pi^{\prime})={\mathcal{A}}(\Pi)$.

Proposition 2.2 ensures the completeness of approximants, in the sense that
all the typings having subject ${\tt t}$ may also type some approximant of
${\tt t}$.

On the other hand, it is easy to see that if
$\Pi\triangleright\Gamma\vdash{\tt t}:\sigma$ and ${\tt t}$ is in $\Pi$-normal
form, then ${\mathcal{A}}(\Pi)\leq{\tt t}$. Summing up, we get a new proof of
the approximation theorem for the relational $\lambda$-model associated to
system $\mathcal{H}$, in the sense of [PPR17]:

######  Theorem 3.

The relational $\lambda$-model induced by system $\mathcal{H}$ satisfies the
approximation theorem, i.e. the interpretation of a term is the union of the
interpretations of its approximants.

We are ready to prove that the set of approximate normal forms solving any
given instance of the inhabitation problem is finite. This property allows us
to design a complete inhabitation algorithm, i.e. one which supplies all
solutions. First, we will prove that a derivation in normal form enjoys a sort
of subformula property. Let us define the subtype relation as the transitive
closure of the following one:

  * •

$\sigma$ is a subtype of $\sigma$.

  * •

${\tt A}$ is a subtype of ${\tt A}$.

  * •

${\tt A}$ and $\tau$ are subtypes of ${\tt A}\rightarrow\tau$.

  * •

$\sigma_{i}$ is a subtype of $[\sigma_{i}]_{i\in I}$ for all $i\in I$.

Finally, ${\tt A}$ is a subtype of $\Gamma$ if ${\tt x}:{\tt A}\in\Gamma$.

######  Lemma 4.

Let ${\tt a}$ be an approximate normal form. Let
$\Pi\triangleright\Gamma\vdash{\tt a}:\sigma$. For every subderivation of
$\Pi$ of the shape $\Pi^{\prime}\triangleright\Gamma^{\prime}\vdash{\tt
b}:\tau$, $\tau$ is either a subtype of $\sigma$ or a subtype of $\Gamma$.
Moreover, if ${\tt a}$ is an ${\cal L}$ approximate normal form, then $\sigma$
is a subtype of $\Gamma$.