11institutetext: Heriot-Watt University, Edinburgh, UK

# Intersection Types via Finite-Set Declarations

Fairouz Kamareddine  Joe Wells

###### Abstract

The $\lambda$-cube is a famous pure type system (PTS) cube of eight powerful
explicit type systems that include the simple, polymorphic and depen- dent
type theories. The $\lambda$-cube only types Strongly Normalising (SN) terms
but not all of them. It is well known that even the most powerful system of
the $\lambda$-cube can only type the same pure untyped $\lambda$-terms that
are typable by the higher-order polymorphic implicitly typed
$\lambda$-calculus $F_{\omega}$, and that there is an untyped $\lambda$-term
$\dot{U}$ that is SN but is not typable in $F_{\omega}$ or the $\lambda$-cube.
Hence, neither system can type all the SN terms it expresses. In this paper,
we present the f-cube, an extension of the $\lambda$-cube with finite-set
declarations (FSDs) like $y\mathord{\overline{\in}}\\{C_{1},\cdots,C_{n}\\}:B$
which means that $y$ is of type $B$ and can only be one of
$C_{1},\cdots,C_{n}$. The novelty of our FSDs is that they allow to represent
intersection types as $\Pi$-types. We show how to translate and type the term
$\dot{U}$ in the f-cube using an encoding of intersection types based on FSDs.
Notably, our translation works without needing anything like the usual
troublesome intersection-introduction rule that proves a pure untyped
$\lambda$-term $M$ has an intersection type $\Phi_{1}\cap\cdots\cap\Phi_{k}$
using $k$ independent subderivations. As such, our approach is useful for
language implementers who want the power of intersection types without the
pain of the intersection-introduction rule.

###### Keywords:

Intersection Types, Typability, Strong Normalisation.

##  1 The Troublesome Intersection-Introduction Rule

Type theory was first developed by Bertrand Russell to avoid the
contradictions in Frege’s work. Since, type theory was adapted and used by
Ramsey, Hilbert/Ackermann and Church and later exploded into powerful exciting
formalisms that played a substantial role in the development of programming
languages and theorem provers, and in the verification of software. As
advocated by Russell, type theory remains to this day a powerful tool at
avoiding loops/contradictions and at characterising strong normalization (SN).
There are 2 styles of typing: explicit (à la Church) as in $\lambda x:T.x$ and
implicit (à la Curry) as in $\lambda x:x$. We call the latter untyped. A type
assignment engine needs to work harder to assign a type to an untyped term
than to an explicitly typed one.

Intersection types were independently invented near the end of the 1970s by
Coppo and Dezani [7] and Pottinger [12] with aims such as the analysis of
normalization properties, which requires a very precise analysis (see also [4,
10, 14]). Aiming to make use of this precision, the members of the Church
Project worked on a compiler that used intersection types not only to support
the usual kind of type polymorphism but also to represent a precise
polyvariant flow analysis that was used to enable optimizing representation
transformations [20]. Among the many challenges that were faced, a major
difficulty was the intersection-introduction typing rule, which made it
complicated to do local optimizations (an essential task for a compiler) while
at the same time retaining type information and the ability to verify it. The
intersection-introduction rule usually looks like this:

$\frac{E\vdash M:\sigma\hskip 36.135ptE\vdash M:\tau}{E\vdash
M:\sigma\cap\tau}\hfill\quad{(\mbox{$\cap$-Intro})}$

The proof terms are the same for both premises and the conclusion! No syntax
is introduced. A system with this rule does not fit into the proofs-as-terms
(PAT, a.k.a. propositions-as-types and Curry/Howard) correspondence, because
it has proof terms that do not encode deductions. This trouble is related to
the fact that the $\cap$ type constructor is not a truth-functional
propositional connective, but rather one that depends on the proofs of the
propositions it connects sharing some specific key structural details but not
all details [19].

There is an immediate puzzle in how to make a type-annotated variant of the
system. The usual strategy fails immediately, e.g.:

$\frac{E\vdash(\lambda x:\sigma.x):\sigma\rightarrow\sigma\hskip
36.135ptE\vdash(\lambda x:\tau.x):\tau\rightarrow\tau}{E\vdash(\lambda
x:\framebox{???}.x):(\sigma\rightarrow\sigma)\cap(\tau\rightarrow\tau)}$

Where ??? appears, what should be written? A compiler using intersection types
must have some way of organizing the type information of the separate typing
subderivations for the same program points, because a transformation at a
program point must simultaneously deal with all of the separate
subderivations. It would be nice if this was principled rather than _ad hoc_.

The various solutions to this problem each have their own strengths and
weaknesses. The most basic strategy is to accept the usual style of
($\cap$-Intro), and not try to have proof terms that contain type annotations
[8, 11].This is fine if the plan is to discard much or most type information
early in compilation, but is unhelpful if checkable type-correctness is to be
maintained through program transformations.

Another strategy is to have proof terms whose structure makes multiple copies
of subprograms typed with the ($\cap$-Intro) rule [20]. This means that proof
terms can not be merely annotated versions of the $\lambda$-terms being typed,
because the branching structure of the proof terms can not be the same as that
of the $\lambda$-terms. Our experience is that this makes local program
transformations complicated and awkward if checkable type-correctness is to be
maintained. Another option is to limit the possible typings and the set of
typable terms, and accept not having the full power of intersection types [6].
However, this causes difficulty when the purpose of using intersection types
is to support arbitrarily precise program analyses, and also when program
transformations go outside of the restricted set of typings that are
supported.

These issues led us to search for ways to get the power of intersection types
without the usual multiple-premise-style ($\cap$-Intro) rule ([21] gives an
overview of earlier solutions). Some solutions do manage to merge the premises
of the ($\cap$-Intro) rule into just one premise, but do not provide proof
terms containing type information for variable bindings or any other easy-to-
manipulate representation of typing derivations [13, 5].

##  2 Finite-Set Declarations and Encoding $\cap$-Types

Pure type systems (PTSs) were independently given in [2] and [16] and have
been used to reason simultaneously about families of type systems and logics.
The well known $\lambda$-cube of 8 specific PTS’s [1] captured the core
essence of polymorphic, dependent and Calculus of Constructions (CoC) systems.
PTSs were extended with definitions [3, 15] in order to better represent
mathematics and computation. In addition to old $x:A$ declarations, these
definitions allow declarations of the form $x=_{d}D:A$ which declare $x$ to be
$A$ and to have type $B$. Of course extra typing rules are added to type the
new terms with definitions.

While analysing the troublesome ($\cap$-Intro) rule, we noted that definitions
can be generalised to represent intersection types. This article is the result
of this observation. We present the new syntax which extends the
$\lambda$-cube with finite set declarations that generalise definitions to
support intersection types without the troublesome ($\cap$-Intro) rule.
Instead of definitions $\lambda x=_{d}D:A.B$, the new syntax adds finite-set
declarations (FSDs) $\lambda
x\mathord{\overline{\in}}\\{D_{1},D_{2},\cdots,D_{n}\\}:A.B$ where $n\geq 1$.
This latter term is a function like $\lambda x:A.B$ that also requires its
argument $x$ to exhibit at most the behaviors of $D_{1},\cdots,D_{n}$.

We show that FSDs give the power of intersection types by translating an
intersection type $\Phi_{1}\cap\cdots\cap\Phi_{k}$ to a $\Pi$-term of the
form:

$\Pi
z\mathord{\overline{\in}}\\{P_{1,k},\cdots,P_{k,k}\\}:\ast_{k}.z\Phi_{1}\cdots\Phi_{k}$

where $\ast_{k}$ abbreviates
$\underbrace{\ast\rightarrow\cdots\rightarrow\ast\rightarrow\ast}_{k\>\tiny{\mbox{arrows}}}$
and $P_{i,k}=(\lambda x_{1}:\ast.\cdots.\lambda x_{k}:\ast.x_{i})$ picks the
$i$-th of $k$ arguments. So, if $z=P_{i,k}$, then
$z\Phi_{1}\cdots\Phi_{k}=\Phi_{i}$. Notably, our translation from intersection
types works without anything in the translation result like the usual
($\cap$-Intro) rule that proves a pure untyped $\lambda$-term $\dot{M}$ has an
intersection type $\Phi_{1}\cap\cdots\cap\Phi_{k}$ using $k$ independent
subderivations. In PTS style, these “subderivations” are done simultaneously
because in the scope of the declaration
$z\mathord{\overline{\in}}\\{P_{1,k},\cdots,P_{k,k}\\}:\ast_{k}$, the type
$z(A_{1}\rightarrow B_{1})\cdots(A_{k}\rightarrow B_{k})$ can be converted to
the equal type $(zA_{1}\cdots A_{k})\rightarrow(zB_{1}\cdots B_{k})$.

Existing methods for getting rid of the ($\cap$-Intro) rule which support some
kind of type equivalence [21] differ from our method in that our type
equivalence is a consequence of the FSDs restriction on $z$, which is added to
a system supporting $\Pi$-types, including those usually referred to as
“higher-order polymorphic types” and “dependent types”. Thus, FSDs might be a
good way to add the power of intersection types to languages like Coq, Agda,
and Idris. By supporting the full power of intersection types, FSDs might also
help represent results of arbitrarily precise program analyses (e.g., a
polyvariant flow analysis) in language implementations that have $\Pi$-types
in their internal representation.

FSDs can do more than support a translation of intersection types. FSDs can
represent a “definition” by a $\beta$-redex where the abstraction has a FSD
with only one term in the restriction. The point of using a definition like
$(\lambda x\mathord{\overline{\in}}\\{D\\}:C.B)D$ instead of a $\beta$-redex
like $(\lambda x:C.B)D$ is that in the former, $x$ is $D$ can be used to help
justify type-correctness of $B$, which might otherwise require replacing many
instances of $x$ by $D$. Although using an FSD instead of a traditional
definition requires forming the abstraction $\lambda
x\mathord{\overline{\in}}\\{D\\}:C.B$ and its type, and hence an additional
type formation rule, it is worth noting that, adding support for FSDs to
suitable systems does not require huge changes. This is the case since
although not always prominently stated in theory papers, in practice, proof
assistants support definitions in the formal systems of their implementations.

Section 3 introduces into the $\lambda$-cube the new feature of finite-set
declarations. Section 4 presents examples that demonstrate how the new syntax
can be used to simulate intersection types and shows how a term of Urzyczyn
which is untypable in the $\lambda$-cube can be typed in the f-cube.

Let $\mathbb{N}_{1}=\mathbb{N}\setminus\\{0\\}$ be the positive natural
numbers. Given $i,j\in\mathbb{Z}$, define $i..j=\\{k\in\mathbb{Z}\mid i\leq
k\leq j\\}$ and $[i..j)=i..(j-1)$. Write $|S|$ for the size of set $S$.

As usual, the composition $X\circ Y$ is $\\{(y,x)\mid\exists z.(y,z)\in
Y\mbox{ and }(z,x)\in X\\}$. Given $n\in\mathbb{N}_{1}$, let $X^{n}$ be such
that $X^{1}=X$ and $X^{i+1}=X\circ(X^{i})$ for $i\in\mathbb{N}_{1}$.

##  3 Extending the Syntax of the $\lambda$-cube

The new syntax has declarations of the form $x\rho:A$, meaning that the
variable $x$ has type $A$ and $x$ also obeys restriction
$\rho=\mathord{\overline{\in}}\\{A_{1},\cdots,A_{k}\\}$ for $k\in\mathbb{N}$.
When $k=0$, then $x\mathord{\overline{\in}}\\{\\}:A$ is the usual
(unrestricted) declaration $x:A$ of the $\lambda$-cube. When
$k\in\mathbb{N}_{1}$, we get the new restricted finite-set declaration (FSD)
$x\rho:B$ which only permits $x$ to be one of the $A_{i}$’s. These FSDs are
the innovation of the f-cube.

######  Definition 1 (Syntax)

Figures 1 and 2 use the usual pseudo-grammar notation to define the sets of
syntactic entities. Many of these entities are clear from the usual type-
free/typed $\lambda$-calculus. In the $\lambda$-cube we have the sorts $\ast$
and $\Box$, the rules $\mathbfit{R}\in{\mathsf{RuleSet}}$, and the
declarations $\delta$ and contexts $\Delta$. In the extended cube however, the
declarations are a generalised version of those of the $\lambda$-cube and a
declaration $\delta$ may not only be of the the usual form $x:A$ (which we
also write as $x\diamond:A$ and states that $x$ is of type $A$) but may also
be of the form $x\mathord{\overline{\in}}\\{A_{1},\cdots,A_{i}\\}:A$ which
states that $x$ is declared as any of the $A_{j}$s (for $j\in 1..i$) and is of
type $A$. We call declarations of the form
$x\mathord{\overline{\in}}\\{A_{1},\cdots,A_{i}\\}:A$, where $i\not=0$
restricted declarations and these belong to $\mathsf{RDeclaration}$.

Expressions of the f-cube and the pure $\lambda$-calculus are given
respectively by $\mathsf{Term}$ and $\mathsf{LTerm}$. Figure 1 defines default
set ranges for metavariables. $\mathsf{Variable}$ is used as the set of what
we call names. There are two name classes: $\mathsf{Variable}^{\ast}$ marked
with sort $\ast$ and $\mathsf{Variable}^{\Box}$ marked with sort $\Box$. For
embedding reasons, it is usual to take the type free $\lambda$-calculus
variables $\mathsf{LVariable}$ to be $\mathsf{Variable}^{\ast}$. So,
$x^{\ast}$ and $\dot{x}$ range over
$\mathsf{Variable}^{\ast}=\mathsf{LVariable}$ whereas $x^{\Box}$ ranges over
$\mathsf{Variable}^{\Box}$. If no confusion occurs, we simply write $x$ to
range over
$\mathsf{Variable}=\mathsf{Variable}^{\ast}\cup\mathsf{Variable}^{\Box}$.

$\begin{array}[]{@{}r@{\ \in\ }l@{\ \mathrel{::=}\ }l@{}}a,b,\quad
i,\ldots,n,\quad q,r&\lx@intercol\mathbb{N}\hfil\\\
\varsigma&\mathsf{Sort}&\ast\mid\Box\\\
a^{\varsigma},\ldots,z^{\varsigma}&\lx@intercol\mathsf{Variable}^{\varsigma}\hfil\\\
f,g,h,\quad q,\ldots,z&\lx@intercol\mathsf{Variable}\hfil\ =\
&\mathsf{Variable}^{\ast}\cup\mathsf{Variable}^{\Box}\\\
\dot{a},\cdots,\dot{h},\quad\dot{k},\cdots,\dot{z}&\lx@intercol\mathsf{LVariable}\hfil\
=\ &\mathsf{Variable}^{\ast}\\\
\dot{A},\cdots,\dot{Z}&\mathsf{LTerm}&\dot{x}\mid\lambda\dot{x}.\dot{M}\mid\dot{M}\dot{N}\quad\hfill\mbox{{(type-
free $\lambda$terms)}}\vspace{-0.1in}\end{array}$

Figure 1: Metavariable declarations and type free terms.

Let $\mathsf{Syntax}$ be the uniton of all the sets of syntactic entities that
we define in Figures 1 and 2. Let $\chi$ range over $\mathsf{Syntax}$. We
assume the usual assumptions of binding, $\alpha$-conversion and the
Barendregt variable renaming. We take $\alpha$-convertible expressions to
denote the same syntactic entities, e.g., even if $\dot{x}\not=\dot{y}$, it
nonetheless holds that $\lambda\dot{x}.\dot{x}=\lambda\dot{y}.\dot{y}$. As
usual, let $\mathsf{FV}({{\chi}})$ be the collection of all variables in
${\chi}$. We say $\chi$ is closed iff $\mathsf{FV}({{\chi}})=\\{\\}$. We
assume the usual substitution in the $\lambda$calculus where the capture of
free variables must be avoided.

$\begin{array}[]{@{}r@{\: \in\:}l@{\ \mathrel{::=}\
}l@{}}\pi\>\in\>&\mathsf{Binder}&\lambda\mid\Pi\\\
\rho\>\in\>&\mathsf{Restriction}&\overline{\in}\\{A_{1},\dots,A_{i}\\}\quad\mbox{where
}i\in\mathbb{N}\\\
\delta\>\in\>&\mathsf{Declaration}&{{x}\,{\rho}\,{:}\,{A}}\\\
\Delta\>\in\>&\mathsf{Context}&\varepsilon\mid{\delta}_{1},\ldots,{\delta}_{i}\quad\mbox{where
}i\in\mathbb{N}_{1}\\\
\gamma\>\in\>&\mathsf{RDeclaration}&{{x}\,{\rho}}\quad\mbox{where
$\rho\not=\diamond$}\\\
\Gamma\>\in\>&\mathsf{RContext}&\varepsilon\mid{\gamma}_{1},\ldots,{\gamma}_{i}\quad\mbox{where
}i\in\mathbb{N}_{1}\\\ A,\ldots,H,\quad J,\quad
L,\ldots,W\>\in\>&\mathsf{Term}&\varsigma\mid x\mid{{\pi}\mskip
1.5mu{\delta}.\,{A}}\mid{{A}\,{B}}\\\
\lx@intercol\hfil&\mathsf{Rule}&(\varsigma,\varsigma^{\prime})\\\
\mathbfit{R}\>\in\>&\lx@intercol\mathsf{RuleSet}\hfil\ ::=\
&\\{X\subseteq\mathsf{Rule}\mid(\ast,\ast)\in X\\}\vspace{-0.1in}\end{array}$
• Define the null restriction $\diamond=\mathord{\overline{\in}}\\{\\}$ and
write $x\diamond:A$ as the usual declaration $x:A$. • Define the restriction
declarations of $\Delta$ by:
$\mathsf{rdec}({{x}\,{\diamond}\,{:}\,{A}},\Delta)=\mathsf{rdec}(\Delta);$
$\mathsf{rdec}(\varepsilon)=\varepsilon;\quad$ and
$\mathsf{rdec}({{x}\,{\mathord{\overline{\in}}\\{A_{1},\dots,A_{k}\\}}\,{:}\,{A}},\Delta)={{x}\,{\mathord{\overline{\in}}\\{A_{1},\dots,A_{k}\\}}},\mathsf{rdec}(\Delta)$.
• For the $\lambda$-cube, $\mathsf{Restriction}=\\{\diamond\\}$;
$\mathsf{RDeclaration}=\emptyset$ and $\mathsf{rdec}(\Delta)=\varepsilon$. •
Define the variables of a $\delta$ or $\gamma$ by:
$\mathsf{vars}\left(x\rho:A\right)=\mathsf{vars}\left(x\rho\right)=\\{x\\}$
and define $\mathsf{vars}\left(\varepsilon\right)=\\{\\}$;
$\mathsf{vars}\left(\delta,\Delta\right)={\mathsf{var}(\delta)}\cup\mathsf{vars}\left(\Delta\right)$;
$\mathsf{vars}\left(\gamma,\Gamma\right)={\mathsf{var}(\gamma)}\cup\mathsf{vars}\left(\Gamma\right)$.
• Define $\sharp(B)$, the degree of $B$ where
$\sharp\in\mathsf{Term}\mathbin{\to}{0..3}$ by:
$\sharp(\Box)=3$, $\sharp(\ast)=2$,
$\sharp(x^{\varsigma})=\sharp(\varsigma)-2$, and $\sharp({{\pi}\mskip
1.5mu{\delta}.\,{A}})=\sharp({{A}\,{B}})=\sharp(A)$. • Define $\mathsf{rsort}$
and $\mathsf{tsort}$ by: – If $\sharp(B)=0$ then $\mathsf{rsort}(B)=\ast$ and
if $\sharp(B)=1$ then $\mathsf{rsort}(B)=\Box$. – If $\sharp(B)=1$ then
$\mathsf{tsort}(B)=\ast$ and if $\sharp(B)=2$ then $\mathsf{tsort}(B)=\Box$.

Figure 2: $\lambda$\- and f-cube systems syntax definitions.

######  Definition 2 (Rewriting)

We use the usual notion of _compatibility_ of a relation on syntactic
entities. Let $\mathrel{\underline{\beta}}$ and $\beta$ be the smallest
compatible relations where:

$\begin{array}[]{@{}r@{\ \;}c@{\ \;}l@{}}({{\lambda}\mskip
1.5mu{x}.\,{\dot{M}}})\dot{N}&\mathrel{\underline{\beta}}&\dot{M}[x:=\dot{N}]\\\\[2.15277pt]
{{({{\lambda}\mskip
1.5mu{{{x}\,{\rho}\,{:}\,{A}}}.\,{B}})}\,{C}}&\mathrel{\beta}&B[x:=C]\end{array}$

For $r\in\\{\mathrel{\underline{\beta}},\beta\\}$, let $\rightarrow_{r}$,
$\mathrel{\rightarrow\rightarrow}_{r}$, and $=_{r}$ be defined as usual:
$(\rightarrow_{r})=(r)$; and $\mathrel{\rightarrow\rightarrow}_{r}$ is the
smallest transitive relation containing $r$ that is reflexive on
$\mathsf{Syntax}$; and $=_{r}$ is the smallest transitive symmetric relation
containing $\mathrel{\rightarrow\rightarrow}_{r}$.

The following theorem shows that our rewriting rules are confluent.

######  Theorem 3.1 (Confluence for $\beta$)

If $\chi_{1}\mathrel{\rightarrow\rightarrow}_{\beta}\chi_{2}$ and
$\chi_{1}\mathrel{\rightarrow\rightarrow}_{\beta}\chi_{3}$ then there exists
$\chi_{4}\in\mathsf{Syntax}$ such that
$\chi_{2}\mathrel{\rightarrow\rightarrow}_{\beta}\chi_{4}$ and
$\chi_{3}\mathrel{\rightarrow\rightarrow}_{\beta}\chi_{4}$.

###### Proof

First, translate $\mathsf{Syntax}$ and $\beta$ into a higher-order rewriting
(HOR) framework, e.g., van Oostrom’s framework [18]. It is then
straightforward to show that $\beta$ is _orthogonal_. It follows by a standard
HOR result that $\beta$ is _confluent_. $\boxtimes$

######  Definition 3 (Normal Forms)

A syntactic entity $\chi$ _is a normal form_ , written $\mathsf{isnf}(\chi)$,
iff there is no $\chi^{\prime}$ such that $\chi\rightarrow_{r}\chi^{\prime}$
for $r\in\\{\mathrel{\underline{\beta}},\beta\\}$. The _normal form of_
$\chi$, written $\mathsf{nf}(\chi)$, is the unique syntactic entity
$\chi^{\prime}$ such that
$\chi\mathrel{\rightarrow\rightarrow}_{r}\chi^{\prime}$ for
$r\in\\{\mathrel{\underline{\beta}},\beta\\}$ and
$\mathsf{isnf}(\chi^{\prime})$. (Note that $\mathsf{nf}(\chi)$ might be
undefined, e.g., consider $\chi={{B}\,{B}}\in\mathsf{Term}$ where
$B={{\lambda}\mskip 1.5mu{{{x}\,{\diamond}\,{:}\,{y}}}.\,{{{x}\,{x}}}}$, has
no normal form (and is also not type-correct).) A syntactic entity $\chi$ is
strongly normalizing, written $\mathsf{SN}(\chi)$, iff there is no infinite
$r$-rewriting sequence starting at $\chi$ for
$r\in\\{\mathrel{\underline{\beta}},\beta\\}$.

Each of the $\lambda$-cube and the f-cube has 8 type systems each defined by a
set $\mathbfit{R}$ which contains type formation rules which the $(\Pi)$ and
$(\lambda)$ rules use to regulate the allowed abstractions. Figure 3 gives the
8 systems defined by these $\mathbfit{R}$s. E.g., $\widehat{\lambda C}$ uses
all combinations $(\varsigma,\varsigma^{\prime})$ where
$\varsigma\in\\{\ast,\Box\\}$.

$\widehat{{\lambda}{\rightarrow}}$ | $(\ast,\ast)$ |  |  |
---|---|---|---|---
$\widehat{\lambda 2}$ | $(\ast,\ast)$ | $(\Box,\ast)$ |  |
$\widehat{\lambda P}$ | $(\ast,\ast)$ |  | $(\ast,\Box)$ |
$\widehat{\lambda P2}$ | $(\ast,\ast)$ | $(\Box,\ast)$ | $(\ast,\Box)$ |
$\widehat{\lambda\underline{\omega}}$ | $(\ast,\ast)$ |  |  | $(\Box,\Box)$
$\widehat{\lambda\omega}$ | $(\ast,\ast)$ | $(\Box,\ast)$ |  | $(\Box,\Box)$
$\widehat{\lambda\mbox{P}}\underline{\omega}$ | $(\ast,\ast)$ |  | $(\ast,\Box)$ | $(\Box,\Box)$
$\widehat{\lambda C}$ | $(\ast,\ast)$ | $(\Box,\ast)$ | $(\ast,\Box)$ | $(\Box,\Box)$

$\widehat{\lambda{\rightarrow}}$$\widehat{\lambda P}$$\widehat{\lambda
2}$$\widehat{\lambda
P2}$$\widehat{\lambda\underline{\omega}}$$\widehat{\lambda
P}\underline{\omega}$$\widehat{\lambda C}$$\widehat{\lambda\omega}$

$(\ast,\Box)$$(\Box,\Box)$$(\Box,\ast)$

Figure 3: The rule sets for the $\lambda$-cube and f-cube

$\mbox{(ref)}\ \frac{i\in 1..n;\hskip
36.135ptB=_{\beta}A_{i}}{\varepsilon\Vdash
B\mathord{\overline{\in}}\\{A_{1},\cdots,A_{n}\\}}$ $\mbox{(ctR)}\
\frac{\displaystyle
x\not\in\mathsf{vars}\left(\Gamma\right);\quad{\forall}\mskip
1.5mu{i\mathbin{\in}1..n}.\,\Gamma[x:=A_{i}]\Vdash
B[x:=A_{i}]\,\rho[x:=A_{i}]}{\displaystyle{{x}\,{\mathord{\overline{\in}}\\{A_{1},\dots,A_{n}\\}}},\Gamma\Vdash
B\,\rho}$

Figure 4: Restriction Satisfaction/Utilisation Judgements ($\Gamma\Vdash
B\rho$)

######  Definition 4 (Typing Rules and Judgements and Type Systems)

The typing rules for the $\lambda$\- and f-cubes are given in figure 5. If
${\Delta}\vdash^{\mathbfit{R}}{A}\mathbin{:}{B}$ then:

  * •

In type system $\lambda^{\mathbfit{R}}$ and in context $\Delta$ the term $A$
has _type_ $B$.

  * •

$\Delta$, $A$, and $B$ are _$\lambda^{\mathbfit{R}}$ -legal_ (or simply legal)
and $A$ and $B$ are _$\Delta\mbox{-terms}$_.

  * •

$A$ has sort $\varsigma$ if also
${\Delta}\vdash^{\mathbfit{R}}{B}\mathbin{:}{\varsigma}$ holds (in this case,
note that $\mathsf{sort}(A)=\varsigma$).

Let ${\Delta}\vdash^{\mathbfit{R}}{A}\mathbin{:}{B}\mathbin{:}{C}$ stand for
${\Delta}\vdash^{\mathbfit{R}}{A}\mathbin{:}{B}$ and
${\Delta}\vdash^{\mathbfit{R}}{B}\mathbin{:}{C}$. If $\mathbfit{R}$ is omitted
from $\vdash^{\mathbfit{R}}$, then the reader should infer it.

As we see in Figure 5, the $\lambda$\- and f-cubes only differ in rules
(start), (app) and (conv). For the f-cube, (start) is an obvious
generalisation of that of the $\lambda$-cube (checking that the $B_{j}$s have
the correct type), whereas (app) and (conv) use Figure 4 to check that only
well behaved restrictions are used. Here, $\mathsf{rdec}(\Delta)\Vdash
A\,\rho$ and $\mathsf{rdec}(\Delta)\Vdash B\mathord{\overline{\in}}\\{C\\}$
ensure that the restrictions via FSDs are activated according to Figure 4 so
that if $\rho=\mathord{\overline{\in}}\\{C_{1},\cdots,C_{n}\\}$, then for all
$i$, $A=_{\beta}C_{i}$ modulo substitutions based on FSDs in
$\mathsf{rdec}(\Delta)$. Thus, if there are no FSDs, i.e.
$\mathsf{rdec}(\Delta)=\varepsilon$, then the $\mathsf{rdec}(\Delta)\Vdash
B\mathord{\overline{\in}}\\{C\\}$ of (conv) becomes the $B=_{\beta}C$ in the
$\lambda$-cube.111The (weak) rule differs slighly from that of the
$\lambda$-cube, but a simple check shows that this formalisation of the
$\lambda$-cube is equivalent to that of [1].

$\begin{array}[]{@{}c@{}}\mbox{(axiom)}\
\varepsilon\vdash^{\mathbfit{R}}\ast:\Box\quad\qquad\mbox{(weak)}\
\displaystyle\frac{\displaystyle\Delta,\delta\vdash^{\mathbfit{R}}A:B;\qquad\Delta\vdash^{\mathbfit{R}}C:D}{\displaystyle\Delta,\delta\vdash^{\mathbfit{R}}C:D}\\\\[11.62495pt]
\mbox{(start)}\
\displaystyle\frac{\displaystyle\left(\begin{array}[]{@{}l@{}}x^{\varsigma}\not\in\mathsf{vars}\left(\Delta\right);\qquad\Delta\vdash^{\mathbfit{R}}A:\varsigma;\\\
\mbox{if $\rho=\mathord{\overline{\in}}\\{B_{1},\cdots,B_{n}\\}$ then
}{\forall}\mskip 1.5mu{j\in
1..n}.\,\Delta\vdash^{\mathbfit{R}}B_{j}:A\end{array}\right)}{\displaystyle\Delta,{{x^{\varsigma}}\,{\rho}\,{:}\,{A}}\vdash^{\mathbfit{R}}x^{\varsigma}:A}\\\\[11.62495pt]
\mbox{($\Pi$)}\
\displaystyle\frac{\displaystyle\Delta,{{x}\,{\rho}\,{:}\,{A}}\vdash^{\mathbfit{R}}B:\varsigma;\qquad\Delta\vdash^{\mathbfit{R}}A:\varsigma^{\prime};\qquad(\varsigma^{\prime},\varsigma)\in\mathbfit{R}}{\displaystyle\Delta\vdash^{\mathbfit{R}}{{\Pi}\mskip
1.5mu{{{x}\,{\rho}\,{:}\,{A}}}.\,{B}}:\varsigma}\\\\[11.62495pt]
\mbox{($\lambda$)}\
\displaystyle\frac{\displaystyle\Delta,\delta\vdash^{\mathbfit{R}}B^{\prime}:B;\qquad\Delta\vdash^{\mathbfit{R}}{{\Pi}\mskip
1.5mu{\delta}.\,{B}}:\varsigma}{\displaystyle\Delta\vdash^{\mathbfit{R}}{{\lambda}\mskip
1.5mu{\delta}.\,{B^{\prime}}}:{{\Pi}\mskip
1.5mu{\delta}.\,{B}}}\\\\[11.62495pt] \mbox{(app)}\
\displaystyle\frac{\displaystyle\Delta\vdash^{\mathbfit{R}}F:({{\Pi}\mskip
1.5mu{{{x}\,{\rho}\,{:}\,{C}}}.\,{B}});\qquad\Delta\vdash^{\mathbfit{R}}A:C;\qquad(\mbox{
if }\rho\not=\diamond\mbox{ then }\mathsf{rdec}(\Delta)\Vdash
A\,\rho)}{\displaystyle\Delta\vdash^{\mathbfit{R}}{{F}\,{A}}:B[x:=A]}\\\\[11.62495pt]
\mbox{(conv)}\
\displaystyle\frac{\displaystyle\Delta\vdash^{\mathbfit{R}}A:B;\qquad\Delta\vdash^{\mathbfit{R}}C:\varsigma;\qquad\mathsf{rdec}(\Delta)\Vdash
B\mathord{\overline{\in}}\\{C\\}}{\displaystyle\Delta\vdash^{\mathbfit{R}}A:C}\par\vspace{-0.1in}\end{array}$
• In the $\lambda$-cube, the if-then statements of (start) and (app) do not
apply, and the $\mathsf{rdec}(\Delta)\Vdash B\mathord{\overline{\in}}\\{C\\}$
of (conv) becomes $b=_{\beta}C$ by Figure 4. • We write
$\Delta\vdash^{\mathbfit{R}}_{\lambda}A:B$ resp.
$\Delta\vdash^{\mathbfit{R}}_{{\mathchoice{\mbox{f}}{\mbox{f}}{\mbox{\scriptsize
f}}{\mbox{\scriptsize f}}}}A:B$ for type derivation in the $\lambda$\- resp.
f-cube.

Figure 5: Typing rules of the $\lambda$\- and f-cubes.

The next definition gives the function $\mathsf{TE}$ which erases types and
all information at degree 1 or more from elements of $\mathsf{Term}$ to return
pure untyped $\lambda$-terms. $\mathsf{TE}$ is like the function E of [9], but
is simpler because we only need $\mathsf{TE}(A)$ to be meaningful when
$\Delta\vdash_{\mathchoice{\mbox{f}}{\mbox{f}}{\mbox{\scriptsize
f}}{\mbox{\scriptsize f}}}A:B:\ast$. If $A$ is not legal or the sort (type of
the type) of $A$ is not $\ast$, then we do not care whether $\mathsf{TE}(A)$
is defined or if so what it is.

######  Definition 5 (Type Erasure)

Let $\mathsf{TE}\in\mathsf{Term}\rightarrow\mathsf{LTerm}$ be the smallest
function where: $\mathsf{TE}(x)=x$ and
$\begin{array}[]{@{}l@{\ =\ }l@{\qquad\qquad}l@{\ =\
}l@{}}\mathsf{TE}({{A}\,{B}})&{{\mathsf{TE}(A)}\,{\mathsf{TE}(B)}}\quad\mbox{if
$\sharp(B)=0$}&\mathsf{TE}({{\lambda}\mskip
1.5mu{{{x^{\ast}}\,{\rho}\,{:}\,{A}}}.\,{B}})&{{\lambda}\mskip
1.5mu{x^{\ast}}.\,{\mathsf{TE}(B)}}\\\
\mathsf{TE}({{A}\,{B}})&\mathsf{TE}(A)\quad\quad\quad\quad\mbox{if
$\sharp(B)=1$}&\mathsf{TE}({{\lambda}\mskip
1.5mu{{{x^{\Box}}\,{\rho}\,{:}\,{A}}}.\,{B}})&\quad\quad\mathsf{TE}(B)\end{array}$

Definition 4 stated how we can type explicily typed terms (those of
$\mathsf{Term}$). The next definition states how to type pure type-free terms
(those of $\mathsf{LTerm}$).

######  Definition 6 (Typability of Pure $\lambda$-Terms)

A pure $\lambda$-term $\dot{M}$ is _typable_ iff there exist $\Delta$, $A$,
and $B$ such that
$\Delta\vdash_{{\mathchoice{\mbox{f}}{\mbox{f}}{\mbox{\scriptsize
f}}{\mbox{\scriptsize f}}}}A:B:\ast$ and $\mathsf{TE}(A)=\dot{M}$.

##  4 Implementing Intersection Types

This section defines intersection types using FSDs and shows that Urzyczyn’s
famous term is typable in the f-cube. Throughout, assume we are using one of
the 2 systems that allow forming functions “from types to types” (“type
constructors”) and “from types to terms” (“type polymorphism”). Thus, prefix
every statement with “If $\\{(\Box,\Box),(\Box,\ast)\\}\subseteq\mathbfit{R}$,
then $\cdots$” and read every “$\vdash$” as
“$\vdash{R}_{\mathchoice{\mbox{f}}{\mbox{f}}{\mbox{\scriptsize
f}}{\mbox{\scriptsize f}}}$”.

The next definitions give pieces of syntax and abbreviations that are needed
to define intersection types in the f-cubes.

######  Definition 7 (General Syntax Abbreviations)

  * •

$A\mathbin{\to}B={{\Pi}\mskip 1.5mu{{w^{\varsigma}}\mskip 1.75mu{:}\mskip
1.75mu{A}}.\,{B}}\mbox{ where }w^{\varsigma}\not\in\mathsf{FV}({B})\mbox{ and
}\varsigma=\mathsf{tsort}(A)$.
$\mathbin{\to}$ associates to the right, that is,
$A\mathbin{\to}B\mathbin{\to}C$ stands for $A\mathbin{\to}(B\mathbin{\to}C)$.

  * •

$\ast_{0}=\ast\quad$ and $\quad\ast_{i+1}=\ast\mathbin{\to}\ast_{i}$.

  * •

Given names for declarations $\delta^{v_{1}}$, $\ldots$, $\delta^{v_{n}}$,
define: $\Delta^{v_{1},\ldots,v_{n}}=\delta^{v_{1}},\ldots,\delta^{v_{n}}$.

######  Definition 8 (Pieces of Syntax Used in Intersection Types)

The translations use the $y_{j}$’s to represent type variables, use the
$x_{i}$’s to build type-choice combinators, and use the $z_{q}^{j}$’s as
variables restricted to range over type-choice combinators. We implement these
specialized purposes by using the declarations, restrictions, and terms
defined for $i,j\in\mathbb{N}$ and $q\in\mathbb{N}_{1}$ by:
$\begin{array}[b]{@{}l@{\ =\
\;}l@{\quad}l@{}}\delta^{y_{j}}&{{y_{j}^{\Box}}\,{\diamond}\,{:}\,{\ast}}&\\\
\delta^{x_{i}}&{{x_{i}^{\Box}}\,{\diamond}\,{:}\,{\ast}}&\\\
P_{i,q}&{\lambda}\mskip 1.5mu{\delta^{x_{1}}}.\,\cdots.{{\lambda}\mskip
1.5mu{\delta^{x_{q}}}.\,{x_{i}}}&\mbox{where }i\in 1..q\quad\hfill\mbox{{($P$
for ``projection'')}}\\\
\rho^{P_{..{q}}}&\mathord{\overline{\in}}\\{P_{1,q},\dots,P_{q,q}\\}&\\\
\delta^{z^{j}_{q}}&{{{z^{j}_{q}}^{\Box}}\,{\rho^{P_{..{q}}}}\,{:}\,{\ast_{q}}}&\\\
\gamma^{z^{j}_{q}}&\mathsf{rdec}(\delta^{z^{j}_{q}})\quad=\quad{{z^{j}_{q}}\,{\rho^{P_{..{q}}}}}&\end{array}$

We are ready to define intersection types in the f-cube. We only take the
intersection of terms whose degree is 1 and hence whose required sort is
$\Box$ (these terms correspond to types). From definition 8,
${{z^{j}_{q}}\,{\rho^{P_{..{q}}}}}$ is
${{z^{j}_{q}}\,{\mathord{\overline{\in}}\\{P_{1,q},\dots,P_{q,q}\\}}}$ and
hence whichever $P_{i,q}$ is chosen from
$\mathord{\overline{\in}}\\{P_{1,q},\dots,P_{q,q}\\}$ for ${z^{j}_{q}}$, we
get $({z^{j}_{q}}\,A_{1}\,\cdots\,A_{q})=_{\beta}A_{i}$ and we see that
${{\Pi}\mskip
1.5mu{\delta^{z^{j}_{q}}}.\,{({z^{j}_{q}}\,A_{1}\,\cdots\,A_{q})}}$ is the
intersection of $A_{1},\cdots,A_{q}$.

######  Definition 9 (Intersection Types in the f-cube)

Given $\Delta$-terms $A_{1}$, $\ldots$, $A_{q}$ where $q\in\mathbb{N}_{1}$ and
$\sharp(A_{1})=\dots=\sharp(A_{q})=1$, the intersection of $A_{1}$, $\ldots$,
$A_{q}$ is defined as:
$\phantom{\quad}\phantom{\quad}{\mathrel{\bigcap\cdot}}\>\\{A_{1},\ldots,A_{q}\\}\quad=\quad{{\Pi}\mskip
1.5mu{\delta^{z^{j}_{q}}}.\,{({z^{j}_{q}}\,A_{1}\,\cdots\,A_{q})}}\quad\mbox{where
}{z^{j}_{q}}\notin\mathsf{FV}({A_{i}})\mbox{ for }i\in 1..q.$

######  Definition 10 (Syntax Abbreviations for Intersection Types)

  * •

For translations that use only $y_{0}$ from the $y$’s, let: $y=y_{0}$ and
$\delta^{y}=\delta^{y_{0}}$.

  * •

For examples that use only one of the $z$’s at a particular arity
$q\in\mathbb{N}_{1}$, let:
$z_{q}=z^{0}_{q}\qquad\qquad\delta^{z_{q}}=\delta^{z^{0}_{q}}\qquad\qquad\gamma^{z_{q}}=\gamma^{z^{0}_{q}}.$

  * •

Let $\overline{A}=A\mathbin{\to}A$ $\widetilde{A}=\overline{A}\mathbin{\to}A$
$\underline{A}=(A\mathbin{\to}\widetilde{A})=A\mathbin{\to}((A\mathbin{\to}A)\mathbin{\to}A)$
$\overline{A}^{0}=A\mbox{ and }\overline{A}^{i+1}=\overline{\overline{A}^{i}}$
$\underline{A}_{0}=A\mbox{ and
}\underline{A}_{i+1}=\underline{\underline{A}_{i}}$.

The following lemma sets a type-building toolkit to be used in our examples.
Its proof is straightforward using the machinery of PTSs.

######  Lemma 1 (Type-Building Toolkit for Examples)

The following hold:

  1. 1.

For $i,j\in\mathbb{N}$ and $q\in\mathbb{N}_{1}$,
$\varepsilon\vdash\ast_{i}:\Box$; $\varepsilon\vdash P_{i,q}:\ast_{q}$ for
$i\in 1..q$; $\delta^{z_{q}^{j}}\vdash z_{q}^{j}:\ast_{q}$.

  2. 2.

If $\Delta$ is legal and ${{u^{\varsigma}}\,{\rho}\,{:}\,{A}}\in\Delta$, then
$\Delta\vdash u^{\varsigma}:A:\varsigma$.

  3. 3.

Let $j\in\mathbb{N}$, let $i\in\mathbb{N}_{1}$, let $n\in 1..i$, and let
$u_{1},\ldots,u_{n}\in\\{y_{k}\mid k\in\mathbb{N}\\}$. Suppose for $l\in 1..n$
that $A_{l}\in\\{u_{l},\overline{u_{l}}\\}$. Let $\Delta$ be legal such that
$\delta^{z_{i}^{j}}\in\Delta$ and for all $l\in 1..n$,
$\delta^{u_{l}}\in\Delta$. Then $\Delta\vdash z_{i}^{j}A_{1}\ldots
A_{n}:\ast_{i-n}:\Box$.

  4. 4.

If $q\in\mathbb{N}_{1}$, and $\Delta\vdash A:\ast_{q}$, and $\Delta\vdash
B_{i}:\ast$ for $i\in[0..q)$, then for $j\in[0..q)$ it holds that
$\Delta\vdash{{A}\,{B_{0}}}\cdots\,B_{j}:\ast_{q-(j+1)}$.

  5. 5.

If $\Delta\vdash A:\ast$ and $\Delta\vdash B:\ast$ then $\Delta\vdash
A\mathbin{\to}B:\ast$.

  6. 6.

If $\Delta\vdash A:\ast$ and $i\in\mathbb{N}$ then
$\Delta\vdash\overline{A}^{i}:\ast$ and $\Delta\vdash\underline{A}_{i}:\ast$
and $\Delta\vdash\widetilde{A}:\ast$.

###  4.1 Simple Examples

######  Definition 11 (Needed Terms and Declarations)

Define the following:
$\begin{array}[b]{@{}l@{\;{=}\;}l@{\qquad}l@{\;{=}\;}l@{\qquad}l@{\;{=}\;}l@{}}U&{{z_{2}}\,{y}\,{\overline{y}}}&\delta^{u}&{u}\mskip
1.75mu{:}\mskip 1.75mu{U}\mbox{ where $u\not=z_{2}$ and
$u\not=y$}&V&{{z_{2}}\,{\,\overline{y}}\,{\,\overline{y}^{2}}}\\\
W^{\prime}&({{\lambda}\mskip 1.5mu{\delta^{z_{2}}}.\,{{{\lambda}\mskip
1.5mu{\delta^{u}}.\,{u}}}})&W&({{\Pi}\mskip
1.5mu{\delta^{z_{2}}}.\,{{{\Pi}\mskip
1.5mu{\delta^{u}}.\,{U}}}})=({{\Pi}\mskip
1.5mu{\delta^{z_{2}}}.\,{(U\mathbin{\to}U)}})&\delta^{w}&{w}\mskip
1.75mu{:}\mskip 1.75mu{W}\end{array}$

######  Example 1 (Derivation Simulating Polymorphic Identity with
Intersection Types)

All the derivations in this example follow from Lemma 1 and the typing rules.

  * 1.

${\Delta^{y,z_{2}}\vdash U:\ast}$ by Lemma 1.

  * 2.

${\Delta^{y,z_{2},u}\vdash u:U}$ by Lemma 1.

  * 3.

${\Delta^{y,z_{2}}\vdash({{\lambda}\mskip
1.5mu{\delta^{u}}.\,{u}}):({{\Pi}\mskip 1.5mu{\delta^{u}}.\,{U}}):\ast}$ by
$(\lambda)$ and (app).

  * 4.

${\delta^{y}\vdash W^{\prime}:W:\ast}$ by $(\lambda)$ and (app).

We have a polymorphic identity function $W^{\prime}$, but the type
$W={{\Pi}\mskip 1.5mu{\delta^{z_{2}}}.\,{({{\Pi}\mskip
1.5mu{\delta^{u}}.\,{U}})}}={{\Pi}\mskip
1.5mu{\delta^{z_{2}}}.\,{(U\mathbin{\to}U)}}$ doesn’t look like an
intersection type. Let’s see if we can reach something that looks more like an
intersection type instead.

  * 5.

${\Delta^{y,z_{2}}\mbox{ is legal}}$

  * 6.

${\Delta^{y,z_{2}}\vdash y:\ast}$ and
${\Delta^{y,z_{2}}\vdash\overline{y}:\ast}$ and
${\Delta^{y,z_{2}}\vdash\overline{y}^{2}:\ast}$ by Lemma 1.

  * 7.

${\Delta^{y,z_{2}}\vdash z_{2}:\ast_{2}}$ and ${\Delta^{y,z_{2}}\vdash
V:\ast}$ by Lemma 1.

  * 8.

${{\forall}\mskip 1.5mu{i\mathbin{\in}1..2}.\,\>{({{\Pi}\mskip
1.5mu{\delta^{u}}.\,{U}})}[{z_{2}}\mathbin{:=}{P_{i,2}}]=({P_{i,2}}\,{y}\,{\overline{y}})\mathbin{\to}({P_{i,2}}\,{y}\,{\overline{y}})=_{\beta}\overline{y}^{2}=_{\beta}}$
$\phantom{\quad}\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad{({P_{i,2}}\,{\overline{y}}\,{\overline{y}^{2}})={V}[{z_{2}}\mathbin{:=}{P_{i,2}}]}$

  * 9.

${{{\forall}\mskip
1.5mu{i\mathbin{\in}1..2}.\,{\>\varepsilon\Vdash({{\Pi}\mskip
1.5mu{\delta^{u}}.\,{U}})[z_{2}:=P_{i,2}]\,\mathord{\overline{\in}}\\{V[z_{2}:=P_{i,2}]\\}}}}$
by (ref) of Figure 4.

  * 10.

${\gamma^{z_{2}}\Vdash{{\Pi}\mskip
1.5mu{\delta^{u}}.\,{U}}\,\mathord{\overline{\in}}\\{V\\}}$ by (ctR) of Figure
4.

  * 11.

${\Delta^{y,z_{2}}\vdash({{\lambda}\mskip 1.5mu{\delta^{u}}.\,{u}}):V:\ast}$
by 3., 10., and (conv).

  * 12.

${\delta^{y}\vdash W^{\prime}:({{\Pi}\mskip
1.5mu{\delta^{z_{2}}}.\,{V}}):\ast}$ by 11., and ($\lambda$).

The result type here looks better: ${{\Pi}\mskip
1.5mu{\delta^{z_{2}}}.\,{V}}={{\Pi}\mskip
1.5mu{\delta^{z_{2}}}.\,{({{{{z_{2}}\,{}\,{\overline{y}}}}\,{}\,{\overline{y}^{2}}})}}=\mathrel{\bigcap\cdot}\\{{\overline{y}},{\overline{y}^{2}}\\}$.
It is more obvious that one can simply choose either $\overline{y}$ or
$\overline{y}^{2}$, just like with the intersection type
$\overline{y}\cap\overline{y}^{2}$. So what would that choice look like?
Instantiating ${{\Pi}\mskip 1.5mu{\delta^{z_{2}}}.\,{V}}$ to either
$\overline{y}$ or $\overline{y}^{2}$ goes like this:

  * 13.

${\delta^{y}\mbox{ is legal (as a context)}}$

  * 14.

${{{\forall}\mskip 1.5mu{i\mathbin{\in}1..2}.\,{\>\delta^{y}\vdash
P_{i,2}:\ast_{2}:\Box}}}$ by Lemma 1 and (weak).

  * 15.

${{{\forall}\mskip 1.5mu{i\mathbin{\in}1..2}.\,{\>\varepsilon\Vdash
P_{i,2}\,\mathord{\overline{\in}}\\{P_{1,2},P_{2,2}\\}}}}$ by (ref) of Figure
4.

  * 16.

${{{\forall}\mskip
1.5mu{i\mathbin{\in}1..2}.\,{\>\mathsf{rdec}(\delta^{y})\Vdash
P_{i,2}\,\mathord{\overline{\in}}\\{P_{1,2},P_{2,2}\\}}}}$ by (ctR) of Figure
4.

  * 17.

${{{\forall}\mskip
1.5mu{i\mathbin{\in}1..2}.\,{\>\delta^{y}\vdash({{\lambda}\mskip
1.5mu{\delta^{u}}.\,{u}})[z_{2}:=P_{i,2}]:V[z_{2}:=P_{i,2}]:\ast}}}$ by 11.,
15., substitution.

  * 18.

${{\forall}\mskip 1.5mu{i\mathbin{\in}1..2}.\,\>{({{\lambda}\mskip
1.5mu{\delta^{u}}.\,{u}})}[{z_{2}}\mathbin{:=}{P_{i,2}}]=({{\lambda}\mskip
1.5mu{{u}\mskip 1.75mu{:}\mskip
1.75mu{({P_{i,2}}\,{y}\,{\overline{y}})}}.\,{u}})\rightarrow_{\beta}({{\lambda}\mskip
1.5mu{{u}\mskip 1.75mu{:}\mskip 1.75mu{\overline{y}^{i-1}}}.\,{u}})}$

  * 19.

${{\forall}\mskip
1.5mu{i\mathbin{\in}1..2}.\,\>{V}[{z_{2}}\mathbin{:=}{P_{i,2}}]=({P_{i,2}}\,{\overline{y}}\,{\overline{y}^{2}})\rightarrow_{\beta}\overline{y}^{i}}$

  * 20.

${{\forall}\mskip
1.5mu{i\mathbin{\in}1..2}.\,{\>\delta^{y}\vdash({{\lambda}\mskip
1.5mu{{u}\mskip 1.75mu{:}\mskip
1.75mu{\overline{y}^{i-1}}}.\,{u}}):{\overline{y}^{i}}:\ast}}$ by 17., 18.,
19., and subject reduction.

So both 4., and 12., above are roughly like $({{\lambda}\mskip
1.5mu{u}.\,{u}}):\overline{y}\cap\overline{y}^{2}$ with intersection types and
the instantiations are like $({{\lambda}\mskip 1.5mu{u}.\,{u}}):\overline{y}$
and $({{\lambda}\mskip 1.5mu{u}.\,{u}}):\overline{y}^{2}$.

######  Example 2 (Derivation for ${{({{\lambda}\mskip
1.5mu{w}.\,{{{w}\,{w}}}})}\,{({{\lambda}\mskip 1.5mu{u}.\,{u}})}}$ in
Intersection Types Style)

We make use of 1., 4., 14., and 15. of example 1 in the following.

  * 21.

${\delta^{y}\vdash W:\ast:\Box}$ by 1., of example 1.

  * 22.

${\Delta^{y,w}\vdash w:W:\ast}$ by 21., & (start).

  * 23.

${\Delta^{y,w}\mbox{ is legal}}$ by 22., & definition 4.

  * 24.

${{{\forall}\mskip 1.5mu{i\mathbin{\in}1..2}.\,{\>\Delta^{y,w}\vdash
P_{i,2}:\ast_{2}:\Box}}}$ by 23., & 14., of example 1

  * 25.

${{{\forall}\mskip
1.5mu{i\mathbin{\in}1..2}.\,{\>\mathsf{rdec}(\Delta^{y,w})\Vdash
P_{i,2}\,\mathord{\overline{\in}}\\{P_{1,2},P_{2,2}\\}}}}$ by 16., of example
1.

  * 26.

${{{\forall}\mskip 1.5mu{i\in
1..2}.\,{\>\Delta^{y,w}\vdash{{w}\,{P_{i,2}}}:(\Pi\delta^{u}.U)[z_{2}:=P_{i,2}]:\ast}}}$
by 22., 24., 25., & (app).

  * 27.

${{\forall}\mskip 1.5mu{i\in
1..2}.\,\>\Delta^{y,w}\vdash{{w}\,{P_{i,2}}}:({{\Pi}\mskip 1.5mu{{u}\mskip
1.75mu{:}\mskip
1.75mu{({P_{i,2}}\,{y}\,{\overline{y}})}}.\,{({P_{i,2}}\,{y}\,{\overline{y}})}}):\ast}$
by 26.

  * 28.

${\Delta^{y,w}\vdash{{w}\,{P_{1,2}}}:\overline{y}:\ast}$ by 27.

  * 29.

${\Delta^{y,w}\vdash{{w}\,{P_{2,2}}}:{\overline{y}}\mathbin{\to}{\overline{y}}:\ast}$
by 27.

  * 30.

${\Delta^{y,w}\vdash({{{{w}\,{P_{2,2}}}}\,{({{w}\,{P_{1,2}}})}}):\overline{y}:\ast}$
by 28., 29., & (app)

  * 31.

${\delta^{y}\vdash({{\lambda}\mskip
1.5mu{\delta^{w}}.\,{{{{{w}\,{P_{2,2}}}}\,{({{w}\,{P_{1,2}}})}}}}):W\mathbin{\to}\overline{y}:\ast}$
by 30., & $(\lambda)$

  * 32.

${\delta^{y}\vdash{{({{\lambda}\mskip
1.5mu{\delta^{w}}.\,{{{{{w}\,{P_{2,2}}}}\,{({{w}\,{P_{1,2}}})}}}})}\,{W^{\prime}}}:\overline{y}:\ast}$
by 4., of example 1, 31.

This is the equivalent of typing ${{({{\lambda}\mskip
1.5mu{w}.\,{{{w}\,{w}}}})}\,{({{\lambda}\mskip 1.5mu{u}.\,{u}})}}$ with
intersection types.

###  4.2 Typing Urzyczyn’s Untypable Term

Urzyczyn [17] proved $\dot{U}=(\lambda r.\,h(r(\lambda f\lambda
s.\,f\,s))(r(\lambda q.\lambda g.\,g\,q)))(\lambda o.\,o\,o\,o)$ is untypable
in $F_{\omega}$. [9] proved every pure $\lambda$-term is typable in
$F_{\omega}$ iff it is typable in the $\lambda$-cube. Hence $\dot{U}$ is
untypable in the $\lambda$-cube. This section types $\dot{U}$ in the f-cube by
using finite-set declarations.

######  Definition 12 (Terms of Type $\ast$ and Sort $\Box$ for Urzyczyn’s
Term)

$\begin{array}[b]{ll}F={z_{3}}\,{\overline{y}^{3}}\,{\overline{y}^{2}}\,{\overline{y}}&Q={z_{3}}\,{\underline{y}}\,{y}\,{\underline{y}}\\\\[4.30554pt]
S={z_{3}}\,{\overline{y}^{2}}\,{\overline{y}^{1}}\,{y}&G={z_{3}}\,{\underline{y}_{2}}\,{\overline{y}}\,{\overline{(\underline{y})}}\\\\[4.30554pt]
&M={z_{3}}\,{\widetilde{(\underline{y})}}\,{y}\,{\underline{y}}\\\\[2.15277pt]
B=F\mathbin{\to}S\mathbin{\to}S&A=Q\mathbin{\to}G\mathbin{\to}M\\\\[2.15277pt]
E_{1}=\overline{y}^{4}&D_{1}=\underline{y}\mathbin{\to}\underline{y}_{2}\mathbin{\to}\widetilde{(\underline{y})}\\\\[2.15277pt]
E_{2}=\overline{y}^{3}&D_{2}=\underline{y}\\\\[2.15277pt]
E_{3}=\overline{y}^{2}&D_{3}=\underline{y}_{2}\\\\[4.30554pt] E={{\Pi}\mskip
1.5mu{\delta^{z_{3}}}.\,{B}}&D=\Pi\delta^{z_{3}}.A\\\\[2.15277pt]
C_{1}=\overline{y}^{2}&R^{\prime}=O\mathbin{\to}C\\\\[2.15277pt]
C_{2}=\widetilde{(\underline{y})}&R_{1}=E\mathbin{\to}C_{1}\\\\[2.15277pt]
C={z_{2}}\,{C_{1}}\,{C_{2}}&R_{2}=D\mathbin{\to}C_{2}\\\\[2.15277pt]
O={z_{2}}\,{E}\,{D}&R=\Pi\delta^{z_{2}}.R^{\prime}\end{array}$

The proof of the following lemma is straightforward from the typing rules.

###### Lemma 2

Let $H\in\\{F,S,B,Q,G,M,A\\}$ and $J\in\\{E,D,R\\}$. The following hold:
$\delta^{y},\delta^{z_{3}}\vdash H:\ast$ and $\delta^{y}\vdash J:\ast$ and
$\delta^{y},\delta^{z_{2}}\vdash C:\ast$ and $\delta^{y},\delta^{z_{2}}\vdash
R^{\prime}:\ast$.

######  Example 3 (Viewing $E$, $D$, and $R$ as Intersection Types)

$\begin{array}[]{|llllllllll|}\hline\cr
E&=&\Pi\delta^{z_{3}}.&F&\mathbin{\to}&S&\mathbin{\to}&S&&\\\
\mathsf{nf}(B[z_{3}:=P_{1,3}])&=&&\overline{y}^{3}&\mathbin{\to}&\overline{y}^{2}&\mathbin{\to}&\overline{y}^{2}&=\overline{y}^{4}&=E_{1}\\\
\mathsf{nf}(B[z_{3}:=P_{2,3}])&=&&\overline{y}^{2}&\mathbin{\to}&\overline{y}^{1}&\mathbin{\to}&\overline{y}^{1}&=\overline{y}^{3}&=E_{2}\\\
\mathsf{nf}(B[z_{3}:=P_{3,3}])&=&&\overline{y}&\mathbin{\to}&y&\mathbin{\to}&y&=\overline{y}^{2}&=E_{3}\\\
\hline\cr&&&&&&&&&\\\\[-8.61108pt]
D&=&\Pi\delta^{z_{3}}.&Q&\mathbin{\to}&G&\mathbin{\to}&M&&\\\
\mathsf{nf}(A[z_{3}:=P_{1,3}])&=&&\underline{y}&\mathbin{\to}&\underline{y}_{2}&\mathbin{\to}&\widetilde{(\underline{y})}&&=D_{1}\\\
\mathsf{nf}(A[z_{3}:=P_{2,3}])&=&&{y}&\mathbin{\to}&\overline{y}&\mathbin{\to}&y&=\underline{y}&=D_{2}\\\
\mathsf{nf}(A[z_{3}:=P_{3,3}])&=&&\underline{y}&\mathbin{\to}&\overline{(\underline{y})}&\mathbin{\to}&\underline{y}&=\underline{y}_{2}&=D_{3}\\\\[4.30554pt]
\hline\cr&&&&&&&&&\\\\[-8.61108pt]
R&=&\Pi\delta^{z_{2}}.&O&\mathbin{\to}&C&&&&\\\
\mathsf{nf}(R^{\prime}[z_{2}:=P_{1,2}])&=&&E&\mathbin{\to}&C_{1}&&&&=R_{1}\\\
\mathsf{nf}(R^{\prime}[z_{2}:=P_{2,2}])&=&&D&\mathbin{\to}&C_{2}&&&&=R_{2}\\\\[4.30554pt]
\hline\cr\end{array}$

Consider the type $E$ and its component types $F$ and $S$ which we list in
separate columns in the table above. Both $F$ and $S$ act like tuples of 3
types. The restriction in the declaration of $z_{3}$ forces whatever replaces
$z_{3}$ to simply pick one of the three types. By looking at the above table,
we see that the column with $F$ at the top lists the components of $F$ in the
three rows below, and the columns with $S$ at the top work similarly. The
first row lists $E$ and the three rows below list the results of the three
possible instantiations of $E$. In effect, $E$ works like the intersection
type $\overline{y}^{4}\cap\overline{y}^{3}\cap\overline{y}^{2}=E_{1}\cap
E_{2}\cap E_{3}$.

The same argument shows that the type $D$ works like the intersection type
$D_{1}\cap{D_{2}}\cap{D_{3}}$ and that the type $R$ works like the
intersection type $R_{1}\cap{R_{2}}$.

######  Definition 13 (Declarations for Urzyczyn’s Term)

Let $\delta^{h}={h}\mskip 1.75mu{:}\mskip
1.75mu{(C_{1}\mathbin{\to}C_{2}\mathbin{\to}y)}$; $\delta^{r}={r}\mskip
1.75mu{:}\mskip 1.75mu{R};\quad\delta^{o}={o}\mskip 1.75mu{:}\mskip
1.75mu{O};\quad\delta^{f}={f}\mskip 1.75mu{:}\mskip
1.75mu{F};\quad\delta^{s}={s}\mskip 1.75mu{:}\mskip
1.75mu{S};\quad\delta^{q}={q}\mskip 1.75mu{:}\mskip 1.75mu{Q};\quad$ and
$\delta^{g}={g}\mskip 1.75mu{:}\mskip 1.75mu{G}.$

######  Definition 14 (Terms of Sort $\ast$ for Urzyczyn’s Term)

Let
$\begin{array}[b]{@{}l@{}}T={{\lambda}\mskip
1.5mu{\delta^{z_{3}}}.\,{{{\lambda}\mskip
1.5mu{\delta^{f}}.\,{{{\lambda}\mskip 1.5mu{\delta^{s}}.\,{{{f}\,{s}}}}}}}}\
\qquad J={{\lambda}\mskip 1.5mu{\delta^{z_{3}}}.\,{{{\lambda}\mskip
1.5mu{\delta^{q}}.\,{{{\lambda}\mskip 1.5mu{\delta^{g}}.\,{{{g}\,{q}}}}}}}}\
\qquad
L={{h}\,{({{r}\,{}\,{P_{1,2}}\,{T}})}\,{({{r}\,{}\,{P_{2,2}}\,{J}})}}\\\
V={{\lambda}\mskip 1.5mu{\delta^{z_{2}}}.\,{{{\lambda}\mskip
1.5mu{\delta^{o}}.\,{{{o}\,{}\,{P_{1,3}}\,{({{o}\,{}\,{P_{2,3}}})}\,{({{o}\,{}\,{P_{3,3}}})}}}}}}\quad\qquad
U={{({{\lambda}\mskip 1.5mu{\delta^{r}}.\,{L}})}\,{V}}\end{array}$

Again the following lemma is straightforward according to the typing rules.

###### Lemma 3

The following hold:

  1. 1.

    1. (a)

$\gamma^{z_{3}}\Vdash F\,\mathord{\overline{\in}}\\{S\mathbin{\to}S\\}$

    2. (b)

$\gamma^{z_{3}}\Vdash G\,\mathord{\overline{\in}}\\{Q\mathbin{\to}M\\}$,

    3. (c)

$\gamma^{z_{2}}\Vdash O\,\mathord{\overline{\in}}\\{{{\Pi}\mskip
1.5mu{\delta^{z_{3}}}.\,{({{{{z_{2}}\,{}\,{B}}}\,{}\,{A}})}}\\}$

  2. 2.

$\delta^{y}\vdash T:E:\ast$.

  3. 3.

$\delta^{y}\vdash J:D:\ast$.

  4. 4.

    1. (a)

$\Delta^{y,{z_{2}},o}\vdash({{o}\,{}\,{P_{i,3}}}):({{{{{z_{2}}\,{}\,{E_{i}}}}\,{}\,{D_{i}}}}):\ast$
for $i\in\\{1,2,3\\}$.

    2. (b)

$\Delta^{y,{z_{2}},o}\vdash(o\,P_{1,3})(o\,P_{2,3})(o\,P_{3,3}):C:\ast$.

    3. (c)

$\delta^{y}\vdash V:R:\ast$.

  5. 5.

    1. (a)

$\Delta^{y,h,r}\vdash({{r}\,{}\,{P_{i,2}}}):R_{i}:\ast$ for $i\in\\{1,2\\}$.

    2. (b)

$\Delta^{y,h,r}\vdash({{{{r}\,{}\,{P_{1,2}}}}\,{}\,{T}}):C_{1}:\ast$.

    3. (c)

$\Delta^{y,h,r}\vdash({{{{r}\,{}\,{P_{2,2}}}}\,{}\,{J}}):C_{2}:\ast$.

  6. 6.

$\Delta^{y,h,r}\vdash L:y:\ast$ and
$\Delta^{y,h}\vdash\lambda\delta^{r}.L:\Pi\delta^{r}.y:\ast$.

  7. 7.

$\Delta^{y,h}\vdash U:y:\ast$.

Now we show that Urzyczyn’s famous term is typable in the f-cube.

######  Example 4 (Urzyczyn’s Term Is Typable)

Clearly, Urzyczyn’s term $\dot{U}=\mathsf{TE}(U)$. Since Lemma 3.7 shows that
$\Delta^{y,h}\vdash U:y:\ast$, then by Definition 6, $\dot{U}$ is typable.

##  5 Conclusion

In this paper we introduced an extension of the PTS $\lambda$-cube using
finite set declarations that allow us to translate intersection types as
$\lambda$-terms. We gave the translation of Urzyczyn’s famous term $U$ (which
is untypable in the $\lambda$-cube) in the f-cube and showed that this term is
indeed typable in the f-cube. The set up and machinery presented in this paper
can be followed to prove that the f-cube characterizes all strongly
normalising terms.

## References

  * [1] H. P. Barendregt.  Lambda calculi with types.  In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, eds., Handbook of Logic in Computer Science, vol. 2. Oxford University Press, 1992.
  * [2] S. Berardi.  Type Dependency and Constructive Mathematics.  Phd thesis, Carnegie Mellon University and Università di Torino, 1990\.
  * [3] R. Bloo, F. Kamareddine, R. Nederpelt.  The Barendregt cube with definitions and generalised reduction.  Inform. & Comput., 126(2), 1996.
  * [4] V. Bono, B. Venneri, L. Bettini.  A typed lambda calculus with intersection types.  Theoretical Computer Science, 398, pages 95–113, 2008.
  * [5] B. Capitani, M. Loreti, B. Venneri.  Hyperformulae, parallel deductions and intersection types.  Electronic Notes in Theoretical Computer Science, 50, 2001.  Proceedings of ICALP 2001 workshop: Bohm’s Theorem: Applications to Computer Science Theory (BOTH 2001), Crete, Greece, 2001-07-13.
  * [6] A. B. Compagnoni, B. C. Pierce.  Higher-order intersection types and multiple inheritance.  Math. Structures Comput. Sci., 6(5), 1996.
  * [7] M. Coppo, M. Dezani-Ciancaglini.  An extension of the basic functionality theory for the $\lambda$-calculus.  Notre Dame J. Formal Logic, 21(4), 1980.
  * [8] J. Dunfield.  Elaborating intersection and union types.  J. Functional Programming, 24(2–3), 2014.
  * [9] P. Giannini, F. Honsell, S. Ronchi Della Rocca.  Type inference: Some results, some problems.  Fund. Inform., 19(1/2), 1993.
  * [10] L. Liquori and S. Ronchi Della Rocca.  Intersection-types à la Church.  Information and Computation, 205 (9), pages 1371–1386, 2007.
  * [11] B. D. Oliveira, Z. Shi, J. Alpuim.  Disjoint intersection types.  In Proc. ICFP, 2016.
  * [12] G. Pottinger.  A type assignment for the strongly normalizable $\lambda$-terms.  In J. R. Hindley, J. P. Seldin, eds., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980\.
  * [13] S. Ronchi Della Rocca, L. Roversi.  Intersection logic.  In Computer Science Logic, CSL ’01. Springer, 2001.
  * [14] S. Ronchi Della Rocca.  Intersection Typed lambda-calculus.  Intersection Types and Related Systems, ITRS 2002. Electronic Notes in Theoretical Computer Science, 70, pages 163–181, 2002\.
  * [15] P. Severi, E. Poll.  Pure type systems with definitions.  In Proc. 3rd Int’l Conf. on Logical Foundations of Computer Science (LFCS ’94), vol. 813 of LNCS. Springer, 1994.
  * [16] J. Terlouw.  Een nadere bewijstheoretische analyse van GSTT’s.  Manuscript, 1989.
  * [17] P. Urzyczyn.  Type reconstruction in $\mathrm{F}_{\omega}$.  Math. Structures Comput. Sci., 7(4), 1997.
  * [18] V. van Oostrom.  Confluence for Abstract and Higher-Order Rewriting.  PhD thesis, Vrije Universiteit Amsterdam, 1994.
  * [19] B. Venneri.  Intersection types as logical formulae.  J. Logic Comput., 4(2), 1994.
  * [20] J. B. Wells, A. Dimock, R. Muller, F. Turbak.  A calculus with polymorphic and polyvariant flow types.  J. Funct. Programming, 12(3), 2002.
  * [21] J. B. Wells, C. Haack.  Branching types.  In Programming Languages & Systems, 11th European Symp. Programming, vol. 2305 of LNCS. Springer, 2002.