1518 LABEL:LastPageJan. 03, 2018Feb. 05, 2019

# A Light Modality for Recursion

Paula Severi  Department of Computer Science, University of Leicester, UK

###### Abstract.

We investigate a modality for controlling the behaviour of recursive
functional programs on infinite structures which is completely silent in the
syntax. The latter means that programs do not contain “marks” showing the
application of the introduction and elimination rules for the modality. This
shifts the burden of controlling recursion from the programmer to the
compiler. To do this, we introduce a typed lambda calculus à la Curry with a
silent modality and guarded recursive types. The typing discipline guarantees
normalisation and can be transformed into an algorithm which infers the type
of a program.

###### Key words and phrases:

Typed lambda calculus, infinite data, productivity, denotational semantics,
type inference

##  1\. Introduction

The quest of finding a typing discipline that guarantees that functions on
coinductive data types are productive has prompted a variety of works that
rely on a modal operator [23, 18, 30, 7, 1, 8, 4, 13]. Typability in these
systems guarantees normalization and non-normalizing programs such as
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}I}$
where
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}I}=\lambda
x.x$ are not typable. All these works except for Nakano’s [23] have explicit
constructors and destructors in the syntax of programs [18, 30, 7, 8, 13].
This has the advantage that type checking and/or type inference are easy but
it has the disadvantage that they do not really liberate the programmer from
the task of controlling recursion since one has to know when to apply the
introduction and elimination rules for the modal operator.

We present a typed lambda calculus with a temporal modal operator $\bullet$
called $\lambda^{\bullet}_{\rightarrow}$ which has the advantage of having the
modal operator silent in the syntax of programs The system
$\lambda^{\bullet}_{\rightarrow}$ does not need to make use of a subtyping
relation as Nakano’s. Even without a subtyping relation, the modal operator is
still challenging to deal with because types are intrinsically non-structural,
not corresponding to any expression form in the calculus.

The modal operator $\bullet$, also called the delay operator, indicates that
the data on the recursive calls will only be available later. Apart from the
modal operator, we also include guarded recursive types which generalize the
recursive equation
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}=t\times\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}$
for streams [18, 30]. This allows us to type productive functions on streams
such as

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}~{}xs=\langle\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}xs\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}xs))\rangle$

which deletes the elements at even positions of a stream using the type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str2}_{{\rm
Nature}}$ where
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str2}_{t}=t\times\bullet\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str2}_{t}$.
The temporal modal operator $\bullet$ allows to type many productive functions
which are rejected by the proof assistant Coq [9].

Lazy functional programming is acknowledged as a paradigm that fosters
software modularity [14] and enables programmers to specify computations over
possibly infinite data structures in elegant and concise ways. We give some
examples that show how modularization and compositionality can be achieved
using the modal operator. An important recursive pattern used in functional
programming for modularisation is
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}foldr}$
defined by

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}foldr}~{}f~{}xs=f~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}xs)~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}foldr}~{}f~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}xs))$

The type of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}foldr}$
which is $(t\to\bullet s\to
s)\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to
s$, is telling us what is the safe way to build functions. While it is
possible to type

$\body~{}f=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}foldr}~{}(\lambda
xy.{\langle f~{}x\texttt{,}y\rangle})$

by assigning the type $t\to t$ to $f$, and assuming
$s=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}$,
it is not possible to type the unproductive function
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}foldr}~{}(\lambda
xy.{y})$. This is because $\lambda xy.{y}$ does not have type $(t\to\bullet
s\to s)$.

In spite of the fact that
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str2}_{{\rm
Nature}}$ is the type of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}$
with the minimal number of bullets, it does not give enough information to the
programmer to know that the composition of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}$
with itself is still typeable. The type inference algorithm for
$\lambda^{\bullet}_{\rightarrow}$ can infer a more general type for
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}$,
which looks like

$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Stream}({N},{X})\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Stream}({N+1},{X})$

where
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Stream}({N},{X})=X\times\bullet^{N}\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Stream}({N},{X})$
and $N$ and $X$ are integer and type variable, respectively. It is clear now
that from the above type, a programmer can deduce that it is possible to do
the composition of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}$
with itself.

###  1.1. Outline

Section 2 defines the typed lambda calculus $\lambda^{\bullet}_{\rightarrow}$
with the silent modal operator and shows some examples. Section 3 proves
subject reduction and normalisation. It also shows that the Lèvy-Longo and
Böhm trees of a typeable expression have no $\bot$ for
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$-free
and tail finite types respectively. Section 4 compares
$\lambda^{\bullet}_{\rightarrow}$ with the type systems of [23] and [18].
Section 5 gives an adequate denotational semantics for
$\lambda^{\bullet}_{\rightarrow}$ in the topos of trees as a way of linking
our system to the work by Birkedal et al [3]. Section 6 shows decidability of
the type inference problem for $\lambda^{\bullet}_{\rightarrow}$. This problem
is solved by an algorithm which has the interesting feature of combining
unification of types with integer linear programming. Sections 7 and 8 discuss
related and future work, respectively.

###  1.2. Contribution

This paper improves and extends [29] in several ways:

  1. (1)

We prove that the typed lambda calculus of Krishnaswami and Benton [18] is
included in $\lambda^{\bullet}_{\rightarrow}$ and that
$\lambda^{\bullet}_{\rightarrow}$ is included in the one of Nakano [23].

  2. (2)

We give conditions on the types that guarantee that the Lèvy-Longo and Böhm
trees of a typable expression have no $\bot$.

  3. (3)

Besides proving soundness for the denotational semantics, we also prove that
it is adequate with respect to an observational equivalence.

  4. (4)

We obtain automatic ways of guaranteeing that the program satisfies the
properties of normalization, having Lèvy-Longo and Böhm tree without $\bot$.

##  2\. The Typed Lambda Calculus with the Delay Modality

This section defines the type discipline for
$\lambda^{\bullet}_{\rightarrow}$. Following [23], we introduce the _delay_
type constructor $\bullet$, so that an expression of type $\bullet t$ denotes
a value of type $t$ that is available “at the next moment in time”. This
constructor is key to control recursion and attain normalisation of
expressions.

###  2.1. Syntax

The syntax for expressions and types is given by the following grammars.

$\begin{array}[]{@{}c@{\quad\quad\quad}c@{}}\begin{array}[t]{r@{~~}c@{~~}l@{\quad}l}e~{}~{}&::=^{ind}\hfil~{}~{}&&\textbf{Expression}\\\
~{}~{}&\hfil~{}~{}&{x}&\text{(variable)}\\\
~{}~{}&|\hfil~{}~{}&\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}&\text{(constant)}\\\
~{}~{}&|\hfil~{}~{}&\lambda{x}.e&\text{(abstraction)}\\\
~{}~{}&|\hfil~{}~{}&ee&\text{(application)}\end{array}&\begin{array}[t]{r@{~~}c@{~~}l@{\quad}l}t~{}~{}&::=^{coind}\hfil~{}~{}&&\textbf{Pseudo-
type}\\\ ~{}~{}&\hfil~{}~{}&X&\text{(type variable)}\\\
~{}~{}&|\hfil~{}~{}&{\rm Nature}&\text{(natural type)}\\\
~{}~{}&|\hfil~{}~{}&t\times t&\text{(product)}\\\ ~{}~{}&|\hfil~{}~{}&t\to
t&\text{(arrow)}\\\ ~{}~{}&|\hfil~{}~{}&\bullet
t&\text{(delay)}\end{array}\end{array}$

In addition to the usual constructs of the $\lambda$-calculus, expressions
include constants, ranged over by
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}$.
Constants are the constructor for pairs
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pair}$,
the projections
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
$. We do not need a primitive constant for the fixed point operator because it
can be expressed and typed inside the language. Expressions are subject to the
usual conventions of the $\lambda$-calculus. In particular, we assume that the
bodies of abstractions extend as much as possible to the right, that
applications associate to the left, and we use parentheses to disambiguate the
notation when necessary. We write $\langle e_{1}\texttt{,}e_{2}\rangle$ in
place of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pair}~{}e_{1}~{}e_{2}$.

The syntax of _pseudo-types_ is defined co-inductively. A type is a possibly
infinite tree, where each internal node is labelled by a type constructor
$\rightarrow$, $\times$ or $\bullet$ and has as many children as the arity of
the constructor. The leaves of the tree (if any) are labelled by basic types
which in this case are type variables or ${\rm Nature}$. The type variables
are needed in $\lambda^{\bullet}_{\rightarrow}$ to express the general type of
functions such as the identity. We use a co-inductive syntax to describe
infinite data structures (such as streams). The syntax for pseudo-types
include the types of the simply typed lambda calculus (arrows and products)
and the _delay_ type constructor $\bullet$ [23].

For simplicity, we only include ${\rm Nature}$ and type variables as basic
types. One could easily add other basic types such as
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Bool}$
and
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Unit}$
together with constants for their values.

######  Definition 2.1 (Types).

We say that a pseudo-type $t$ is

  1. (1)

regular if its tree representation has finitely many distinct sub-trees;

  2. (2)

guarded if every infinite path in its tree representation has infinitely many
$\bullet$’s;

  3. (3)

a _type_ if it is regular and guarded.

The regularity condition implies that we only consider types admitting a
finite representation. It is equivalent to representing types with
$\mu$-notation and a strong equality which allows for an infinite number of
unfoldings. This is also called the equirecursive approach since it views
types as the unique solutions of recursive equations [11] [25, Section 20.2].
The existence and uniqueness of a solution for a pseudo-type satisfying
condition 1 follow from known results (see [10] and also Theorem 7.5.34 of
[6]). For example, there are unique pseudo-types
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str}^{\prime}_{{\rm
Nature}}$,
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}$, and
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$
that respectively satisfy the equations
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str}^{\prime}_{{\rm
Nature}}={\rm
Nature}\times\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str}^{\prime}_{{\rm
Nature}}$,
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}={\rm
Nature}\times\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}$, and
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}=\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$.

The guardedness condition intuitively means that not all parts of an infinite
data structure can be available at once: those whose type is prefixed by a
$\bullet$ are necessarily “delayed” in the sense that recursive calls on them
must be deeper. For example,
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}$ is a type that denotes streams of natural numbers, where each
subsequent element of the stream is delayed by one $\bullet$ compared to its
predecessor. Instead
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str}^{\prime}_{{\rm
Nature}}$ is not a type: it would denote an infinite stream of natural
numbers, whose elements are all available right away. If the types are written
in $\mu$-notation, the guardedness condition means that all occurrences of $X$
in the body $t$ of $\mu X.t$ are in the scope of a $\bullet$.

The type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$
is somehow degenerated in that it contains no actual data constructors.
Unsurprisingly, we will see that non-normalising terms such as
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}\Upomega}=(\lambda{x}.{x}\
{x})(\lambda{x}.{x}\ {x})$ can only be typed with
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$
(see Theorem 3.13). Without condition 2,
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}\Upomega}$
could be given any type since the recursive pseudo-type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}D}=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}D}\rightarrow
t$ would become a type.

We adopt the usual conventions regarding arrow types (which associate to the
right) and assume the following precedence among type constructors: $\to$,
$\times$ and $\bullet$ with $\bullet$ having the highest precedence. Sometimes
we will write $\bullet^{n}t$ in place of
$\smash{\underbrace{\bullet\cdots\bullet}_{n\text{-times}}t}$.

###  2.2. Operational Semantics

Expressions reduce according to a standard _call-by-name_ semantics:

$\begin{array}[]{c}{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{r-beta}}{\text{\scriptsize[{r-beta}]}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
41.73721pt\vbox{\vbox{}\hbox{\hskip-41.7372pt\hbox{\hbox{$\displaystyle\displaystyle(\lambda{x}.e_{1})~{}e_{2}\longrightarrow
e_{1}[e_{2}/{x}]$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{r-first}}{\text{\scriptsize[{r-first}]}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
28.71048pt\vbox{\vbox{}\hbox{\hskip-28.71046pt\hbox{\hbox{$\displaystyle\displaystyle\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}{\langle
e_{1}\texttt{,}e_{2}\rangle}\longrightarrow
e_{1}$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{r-second}}{\text{\scriptsize[{r-second}]}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
30.79381pt\vbox{\vbox{}\hbox{\hskip-30.79381pt\hbox{\hbox{$\displaystyle\displaystyle\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}{\langle
e_{1}\texttt{,}e_{2}\rangle}\longrightarrow
e_{2}$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{r-ctxt}}{\text{\scriptsize[{r-ctxt}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
11.84198pt\vbox{\hbox{\hskip-11.84196pt\hbox{\hbox{$\displaystyle\displaystyle
e\longrightarrow f$}}}\vbox{}}}\over\hbox{\hskip
22.81427pt\vbox{\vbox{}\hbox{\hskip-22.81425pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{E}[e]\longrightarrow\mathrm{E}[f]$}}}}}}$}}}\end{array}$

where the _evaluation contexts_ are
$\mathrm{E}::=[~{}]\mid({\mathrm{E}}~{}{e})\mid(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}\mathrm{E})\mid(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}\mathrm{E})\mid(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}~{}\mathrm{E})$.
Normal forms are defined as usual as expressions that do not reduce. The
reflexive and transitive closure of $\longrightarrow$ is denoted by
$\longrightarrow^{*}$.

Note that $\longrightarrow$ does not allow to reduce expressions which are
inside the body of an abstraction or component of a pair as the usual
$\beta$-reduction of lambda calculus does. In the standard terminology of
lambda calculus, $\longrightarrow$ actually corresponds to weak head reduction
and the normal forms of $\longrightarrow$ are actually called weak head normal
forms.

###  2.3. Type System

First we assume a set $\kappa$ containg the types for the constants:

$\begin{array}[]{l@{\,\,\,}l}\begin{array}[t]{l@{\\!\,\,\,}l@{\\!\,\,\,}l}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pair}&:&t\to
s\to t\times s\\\
\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}&:&t\times
s\to t\\\
\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}&:&t\times
s\to
s\end{array}&\begin{array}[t]{l@{\\!\,\,\,}l@{\\!\,\,\,}l}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}&:&{\rm
Nature}\\\
\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}&:&{\rm
Nature}\to{\rm Nature}\end{array}\end{array}$

The type assignment system $\lambda^{\bullet}_{\rightarrow}$ is defined by the
following rules.

$\begin{array}[]{@{}c@{}}{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{axiom}}{\text{\scriptsize[{axiom}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
16.677pt\vbox{\hbox{\hskip-16.677pt\hbox{\hbox{$\displaystyle\displaystyle{x}:t\in\Upgamma$}}}\vbox{}}}\over\hbox{\hskip
15.01036pt\vbox{\vbox{}\hbox{\hskip-15.01036pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash{x}:t$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{const}}{\text{\scriptsize[{const}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
16.21405pt\vbox{\hbox{\hskip-16.21405pt\hbox{\hbox{$\displaystyle\displaystyle\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}:t\in\kappa$}}}\vbox{}}}\over\hbox{\hskip
14.79163pt\vbox{\vbox{}\hbox{\hskip-14.79163pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}:t$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\bullet$I}}{\text{\scriptsize[{$\displaystyle\bullet$I}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
17.25858pt\vbox{\hbox{\hskip-17.25856pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e:t$}}}\vbox{}}}\over\hbox{\hskip
19.4808pt\vbox{\vbox{}\hbox{\hskip-19.4808pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e:\bullet
t$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$I}}{\text{\scriptsize[{$\displaystyle\to$I}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
30.26581pt\vbox{\hbox{\hskip-30.2658pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma,{x}:\bullet^{n}t\vdash
e:\bullet^{n}s$}}}\vbox{}}}\over\hbox{\hskip
39.55727pt\vbox{\vbox{}\hbox{\hskip-39.55727pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash\lambda{x}.e:\bullet^{n}(t\to
s)$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$E}}{\text{\scriptsize[{$\displaystyle\to$E}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
59.13342pt\vbox{\hbox{\hskip-59.1334pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}:\bullet^{n}(t\to s)\ \ \ \Upgamma\vdash
e_{2}:\bullet^{n}t$}}}\vbox{}}}\over\hbox{\hskip
24.32785pt\vbox{\vbox{}\hbox{\hskip-24.32785pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}e_{2}:\bullet^{n}s$}}}}}}$}}}\end{array}$

The rule [$\bullet$I] introduces the modality. The rule is unusual in the
sense that the expression remains the same. We do not have a constructor for
$\bullet$ at the level of expressions.

The rule [$\bullet$I] does not have any restrictions, i.e. if it is known that
a value will only be available with delay $n$, then it will also be available
with any delay $m\geq n$, but not earlier. Using rule [$\bullet$I] and the
recursive type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}D}=\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}D}\rightarrow
t$, we can derive that the fixed point combinator
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}=\lambda{y}.(\lambda{x}.{y}\
({x}\ {x}))(\lambda{x}.{y}\ ({x}\ {x}))$ has type $(\bullet t\rightarrow
t)\rightarrow t$ by assigning the type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}D}\rightarrow
t$ to the first occurrence of $\lambda{x}.{y}\ ({x}\ {x})$ and
$\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}D}\rightarrow
t$ to the second one [23].

The rules[$\to$I] and [$\to$E] allow for an arbitrary delay in front of the
types of the entities involved. Intuitively, the number of $\bullet$’s
represents the delay at which a value becomes available. So for example, rule
[$\to$I] says that a function which accepts an argument ${x}$ of type $t$
delayed by $n$ and produces a result of type $s$ delayed by the same $n$ has
type $\bullet^{n}(t\to s)$, that is a function delayed by $n$ that maps
elements of $t$ into elements of $s$.

###  2.4. Inductive data types

The temporal modal operator can only be used for defining co-inductive data
types. Inductive data types need to be introduced separately into the
calculus. For example, we can introduce primitive recursion on ${\rm Nature}$
by means of a function
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}:t\to({\rm
Nature}\to t\to t)\to{\rm Nature}\to t$ with the reduction rule:

$\begin{array}[]{ll}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}~{}{f_{1}}~{}f_{2}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}\longrightarrow
f_{1}\quad\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}~{}{f_{1}}~{}f_{2}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
~{}e)\longrightarrow
f_{2}~{}e~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}~{}{f_{1}}~{}f_{2}~{}e)\end{array}$

We can also introduce a type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t}$
for the set of finite lists as an inductive data type with
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}nil}:\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}consl}:t\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}lrec}:s\to(t\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t}\to
s\to
s)\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t}\to
s$ with the reduction rule:

$\begin{array}[]{ll}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}lrec}~{}{f_{1}}~{}f_{2}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}nil}\longrightarrow
f_{1}\quad\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}lrec}~{}{f_{1}}~{}f_{2}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}consl}~{}e_{1}~{}e_{2})\longrightarrow
f_{2}~{}e_{1}~{}e_{2}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}lrec}~{}{f_{1}}~{}f_{2}~{}e_{2})\end{array}$

###  2.5. Disjoint union

We could add the disjoint union $t_{1}+t_{2}$ of two types $t_{1}$ and $t_{2}$
and add constants:

$\begin{array}[]{ll}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}inl}:t_{1}\to
t_{1}+t_{2}\\\
\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}inr}:t_{2}\to
t_{1}+t_{2}\\\
\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}case}:(t_{1}+t_{2})\to(t_{1}\to
s)\to(t_{2}\to s)\to s\end{array}$

the reduction rules:

$\begin{array}[]{ll}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}case}~{}{(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}inl}~{}e)}~{}{f_{1}}{f_{2}}\longrightarrow
f_{1}~{}e\quad\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}case}~{}{(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}inr}~{}e)}~{}{f_{1}}{f_{2}}\longrightarrow
f_{2}~{}e\end{array}$

and the evaluation contexts are extended with
$\mathrm{E}::=...\mid\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}case}~{}{\mathrm{E}}~{}{f_{1}}{f_{2}}$.

Using the disjoint union, we can define the type of finite and infinite lists
as:

$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}coList}_{t}=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Unit}+\bullet
t\times\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}coList}_{t}$

###  2.6. Type of conatural numbers

We can also define the type of conatural numbers as
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}coNat}=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Unit}+\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}coNat}$.
Then
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}z}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}inl}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}unit}$
has type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}coNat}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}s}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}inr}$
has type
$\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}coNat}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}coNat}$.
The set of conatural numbers include
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}s}^{\infty}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}s}$.
The usual definition of addition given by the equations:

$n+0=n\quad n+(m+1)=(n+m)+1$

can be written as

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}add}~{}{x}~{}{y}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}case}~{}{y}~{}(\lambda{y}_{1}.{{x}})~{}(\lambda{y}_{1}.{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}s}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}add}~{}{x}~{}{y}_{1})})$

and it can be typed in $\lambda^{\bullet}_{\rightarrow}$. However, the usual
definition of substraction given by the equations

$n-0=n\quad 0-n=0\quad(n+1)-(m+1)=n-m$

which is expressed as:

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}minus}~{}{x}~{}{y}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}case}~{}{x}~{}(\lambda{x}_{1}.{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}z}})~{}(\lambda{x}_{1}.{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}case}~{}{y}~{}(\lambda{y}_{1}.{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}z}})(\lambda{y}_{1}.{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}minus}~{}{x}_{1}~{}{y}_{1})})}$

is not typable because
$(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}minus}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}s}^{\infty}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}s}^{\infty})$
is not normalizing.

###  2.7. Examples of Typable Expressions in $\lambda^{\bullet}_{\rightarrow}$

We consider the function
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}$
of the introduction that deletes the elements at even positions of a stream.

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}~{}\lambda
fx.{\langle(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}x)\texttt{,}f~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}x))\rangle}$
(2.1)

In order to assign the type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str2}_{{\rm
Nature}}$ to
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}$,
the variable $f$ has to be delayed once and the first occurrence of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}$
has to be delayed twice. Note also that when typing the application
$f~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}x))$
the rule [$\to$E] is used with $n=2$.

The following two functions have type $(t\to
s)\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{s}$
in $\lambda^{\bullet}_{\rightarrow}$.

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}map}~{}f~{}x=\langle
f~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}x)\texttt{,}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}map}\
f\
(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}x)\rangle$
---
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}maap}~{}f~{}x=\langle
f~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}x)\texttt{,}\langle
f~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}x))\texttt{,}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}maap}\
f\
(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}x))\rangle\rangle$

The following function has type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}$ in $\lambda^{\bullet}_{\rightarrow}$.

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}sum}~{}x~{}y=\langle(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}x)+(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}y)\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}sum}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}x)~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}y)\rangle$

The following two functions have type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}$
in $\lambda^{\bullet}_{\rightarrow}$.

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}interleave}~{}x~{}y=\langle\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}x\texttt{,}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}interleave}\
y\
(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}x)\rangle$
---
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}merge}~{}x~{}y=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}if}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}x)\leq(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}y)~{}\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}then}~{}\langle\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}x\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}merge}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}x)~{}y\rangle~{}\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}else}~{}\langle\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}y\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}merge}~{}x~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}y)\rangle$

The following six functions have type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}$ in $\lambda^{\bullet}_{\rightarrow}$.

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}=\langle
1\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}interleave}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}\rangle$
---
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}nats}=\langle
0\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}map}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}nats}\rangle$
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}=\langle
0\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}sum}~{}{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}}~{}{\langle
1\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}\rangle}\rangle$
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}^{\prime}=\langle
0\texttt{,}\langle
1\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}sum}~{}{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}^{\prime}}~{}{(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}^{\prime})}\rangle\rangle$
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}naats}=\langle
0\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}maap}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}nats}\rangle$
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ham}=\langle
1\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}merge}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}map}~{}\lambda{x}.{2*{x}}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ham})~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}merge}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}map}~{}\lambda{x}.{3*{x}}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ham})(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}map}~{}\lambda{x}.{5*{x}}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ham})))\rangle$

The functions
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}merge}$,
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}$,
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}$,
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}^{\prime}$,
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}naats}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ham}$
cannot be typed by the proof assistant Coq because they do not satisfy the
syntactic guardness condition (all recursive calls should be guarded by
constructors) [12]. The function
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}^{\prime}$
cannot be typed with sized types [28].

It is possible to type in $\lambda^{\bullet}_{\rightarrow}$ other programs
shown typable in other papers on the modal operator such as
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}toggle}$,
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}paperfolds}$
[4].

###  2.8. Untypable programs in $\lambda^{\bullet}_{\rightarrow}$

We define the function
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}get}$
as follows:

$\begin{array}[]{l}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}get}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}\lambda{x}{y}{z}.{{y}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}{z})}\end{array}$
(2.2)

The first argument of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}$
has type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to
t$ while the second argument has type ${\rm
Nature}\to(\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to
t)\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to\bullet
t$. It is not difficult to see that
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}get}$
is not typable in $\lambda^{\bullet}_{\rightarrow}$ unless $t=\bullet t$. Note
that if we re-define
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}get}$
on the set of conatural numbers and use
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}$
instead of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}$
then we obtain a function
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}get}^{\prime}$
defined by:

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}get}^{\prime}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}(\lambda
g.\lambda
xy.\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}case}~{}x~{}(\lambda
x_{1}.\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}y)~{}(\lambda
x_{1}.g~{}x_{1}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}y)))$

which is not typable in $\lambda^{\bullet}_{\rightarrow}$ either.

We now consider the function
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}take}$
that takes the first $n$ elements of a stream and returns a finite list in
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t}$
defined by:

$\begin{array}[]{ll}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}take}~{}0~{}{x}&=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}nil}\\\
\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}take}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
~{}n)~{}{x}&=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}consl}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}{x})~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}take}~{}n~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}{x}))\end{array}$

It is expressed using
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}$
as follows:

$\begin{array}[]{l}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}take}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}~{}\lambda{x}.{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}nil}}~{}\lambda{x}{y}{z}.{(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}consl}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}{z})~{}({y}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}{z})))}\end{array}$
(2.3)

The first argument of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}natrec}$
has type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t}$
and the second argument has type ${\rm
Nature}\to(\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t})\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}\to\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}List}_{t}$.
It is not difficult to see that
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}take}$
is not typable in $\lambda^{\bullet}_{\rightarrow}$.

Though the type systems by Clouston et al [8] and the one by Atkey et al [1]
have to introduce explicit constants for the introduction and elimination of
$\bullet$, they can type programs such as
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}get}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}take}$
which $\lambda^{\bullet}_{\rightarrow}$ cannot do.

##  3\. Properties of Typable Expressions

This section proves the two most relevant properties of typable expressions,
which are subject reduction (reduction of expressions preserves their types)
and normalisation. As informally motivated in Section 2, the type constructor
$\bullet$ controls recursion and guarantees normalisation of any expression
that has a type different from
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$.
This section also proves that any typable expression has a Lèvy-Longo and Böhm
tree without $\bot$ if the type is
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$-free
and tail finite respectively.

###  3.1. Inversion and Subject Reduction

######  Lemma 3.1 (Weakening).

If $\Upgamma\vdash e:t$ and $\Upgamma\subseteq\Upgamma^{\prime}$ then
$\Upgamma^{\prime}\vdash e:t$.

###### Proof.

By an easy induction on the derivation. ∎

######  Lemma 3.2 (Delay).

If $\Upgamma_{1},\Upgamma_{2}\vdash e:t$ then
$\Upgamma_{1},\bullet\Upgamma_{2}\vdash e:\bullet t$.

###### Proof.

By induction on the derivation. We only show the case for the rule [$\to$I].

[$\displaystyle\to$I] $\displaystyle\displaystyle{\hbox{\hskip
41.2304pt\vbox{\hbox{\hskip-41.23038pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma_{1},\Upgamma_{2},{x}:\bullet^{n}t_{1}\vdash
e:\bullet^{n}t_{2}$}}}\vbox{}}}\over\hbox{\hskip
47.18858pt\vbox{\vbox{}\hbox{\hskip-47.18858pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma_{1},\Upgamma_{2}\vdash\lambda{x}.e:\bullet^{n}(t_{1}\to
t_{2})$}}}}}}$

By induction hypothesis,
$\Upgamma_{1},\bullet\Upgamma_{2},{x}:\bullet^{n+1}t_{1}\vdash
e:\bullet^{n+1}t_{2}$. By applying the rule [$\to$I], we conclude that
$\Upgamma_{1},\bullet\Upgamma_{2}\vdash\lambda{x}.e:\bullet^{n+1}(t_{1}\to
t_{2})$. ∎

######  Lemma 3.3 (Inversion).

  1. (1)

If
$\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}:t$
then $t=\bullet^{n}t^{\prime}$ and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}:t^{\prime}\in\kappa$.

  2. (2)

If $\Upgamma\vdash{x}:t$ then $t=\bullet^{n}t^{\prime}$ and
${x}:t^{\prime}\in\Upgamma$.

  3. (3)

If $\Upgamma\vdash\lambda{x}.e:t$ then $t=\bullet^{n}(t_{1}\to t_{2})$ and
$\Upgamma,{x}:\bullet^{n}t_{1}\vdash e:\bullet^{n}t_{2}$

  4. (4)

If $\Upgamma\vdash e_{1}e_{2}:t$ then $t=\bullet^{n}t_{2}$ and $\Upgamma\vdash
e_{2}:\bullet^{n}t_{1}$ and $\Upgamma\vdash e_{1}:\bullet^{n}(t_{1}\to t_{2})$

###### Proof.

By case analysis and induction on the derivation. We only show Item 3. A
derivation of $\Upgamma\vdash\lambda{x}.e:t$ ends with an application of
either [$\to$I] or [$\bullet$I]. The proofs for [$\to$I] is immediate. If the
last applied rule is [$\bullet$I] then $t=\bullet t^{\prime}$ and
$\Upgamma\vdash\lambda{x}.e:t^{\prime}$. By induction,
$t^{\prime}=\bullet^{n}(t_{1}\to t_{2})$ and
$\Upgamma,{x}:\bullet^{n}t_{1}\vdash e:\bullet^{n}t_{2}$. Hence, $t=\bullet
t^{\prime}=\bullet^{n+1}(t_{1}\to t_{2})$ and
$\Upgamma,{x}:\bullet^{n+1}t_{1}\vdash e:\bullet^{n+1}t_{2}$ by Lemma 3.2. ∎

######  Lemma 3.4 (Substitution).

If $\Upgamma,{x}:s\vdash e:t$ and $\Upgamma\vdash f:s$ then $\Upgamma\vdash
e[f/{x}]:t$.

###### Proof.

By induction on the structure of expressions. We only show the case when
$e=\lambda{y}.e^{\prime}$. It follows from Item 3 of Lemma 3.3 that
$t=\bullet^{n}(t_{1}\to t_{2})$ and $\Upgamma,{x}:s,{y}:\bullet^{n}t_{1}\vdash
e^{\prime}:\bullet^{n}t_{2}$. By induction hypothesis,
$\Upgamma,{y}:\bullet^{n}t_{1}\vdash e^{\prime}[f/{x}]:\bullet^{n}t_{2}$. By
applying the rule [$\to$I],
$\Upgamma\vdash\lambda{y}.e^{\prime}[f/{x}]:\bullet^{n}(t_{1}\to t_{2})$. ∎

######  Lemma 3.5 (Subject Reduction).

If $\Upgamma\vdash e:t$ and $e\longrightarrow e^{\prime}$ then $\Upgamma\vdash
e^{\prime}:t$.

###### Proof.

By induction on the definition of $\longrightarrow$. We only do the case
$(\lambda{x}.e_{1})~{}e_{2}\longrightarrow e_{1}[e_{2}/{x}]$. Suppose
$\Upgamma\vdash(\lambda{x}.e_{1})~{}e_{2}:t$. By Item 4 of Lemma 3.3 we have
that:

$t=\bullet^{n}t_{2}\quad\quad\Upgamma\vdash
e_{2}:\bullet^{n}t_{1}\quad\quad\Upgamma\vdash(\lambda{x}.e_{1}):\bullet^{n}(t_{1}\to
t_{2})$

It follows from Item 3 of Lemma 3.3 that $\Upgamma,{x}:\bullet^{n}t_{1}\vdash
e_{1}:\bullet^{n}t_{2}$. By applying Substitution Lemma, we deduce that
$\Upgamma\vdash e_{1}[e_{2}/{x}]:\bullet^{n}t_{2}$. ∎

Neither Nakano’s type system nor ours is closed under $\eta$-reduction. For
example, ${y}:\bullet(t\to s)\vdash\lambda{x}.{\mbox{$({y}\
{x})$}}:(t\to\bullet s)$ but ${y}:\bullet(t\to s)\not\vdash{y}:(t\to\bullet
s)$. The lack of subject reduction for $\eta$-reduction is natural in the
context of lazy evaluation where programs are closed terms and only weak head
normalised.

###  3.2. Normalization

We prove that any expression which has a type $t$ such that
$t\not=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$
reduces to a normal form (Theorem 3.13). For this, we define a type
interpretation indexed on the set of natural numbers for dealing with the
temporal operator $\bullet$. The time is discrete and represented using the
set of natural numbers. The semantics reflects the fact that one $\bullet$
corresponds to one unit of time by shifting the interpretation from $i$ to
$i+1$.

Before introducing the type interpretation, we give a few definitions. Let
$\mathbb{E}$ be the set of expressions. We define the following subsets of
$\mathbb{E}$:

$\begin{array}[]{r@{~}l}\mathbb{WN}~{}&=\\{e\mid e\longrightarrow^{*}f\ \&\
f\mbox{ is a normal form}\\}\\\ \mathbb{HV}~{}&=\\{e\mid
e\longrightarrow^{*}\mathrm{E}[{x}]\ \&\ {x}\mbox{ is a
variable}\\}\end{array}$

We will do induction on the rank of types. For ${\rm Nature}$ and type
variables, the rank is always 0. For the other types, the rank measures the
depth of all what we can observe at time $0$. We could also compute it by
taking the maximal $0$-length of all the paths in the tree representation of
the type, where the $0$-length of a path is the number of type constructors
different from $\bullet$ from the root to a leaf or $\bullet$.

######  Definition 3.6 (Rank of a Type).

The rank of a type $t$ (notation $\mathit{rank}(t)$) is defined as follows.

$\begin{array}[]{r@{~}ll}\mathit{rank}({\rm
Nature})~{}&=\mathit{rank}(X)=\mathit{rank}(\bullet t)=0\\\
\mathit{rank}(t\times s)~{}&=max(\mathit{rank}(t),\mathit{rank}(s))+1\\\
\mathit{rank}(t\rightarrow
s)~{}&=max(\mathit{rank}(t),\mathit{rank}(s))+1\end{array}$

The rank is well defined (and finite) because the tree representation of a
type cannot have an infinite branch with no $\bullet$’s at all (Condition 2 in
Definition 2.1) and $\mathit{rank}(\bullet t)$ is set to $0$.

We now define the type interpretation
${(\\![{t}]\\!)}\in\mathbb{N}\rightarrow\mathcal{P}(\mathbb{E})$, which is an
indexed set, where $\mathbb{N}$ is the set of natural numbers and
$\mathcal{P}$ is the powerset constructor.

######  Definition 3.7 (Type Interpretation).

We define ${(\\![{t}]\\!)}_{i}\subseteq\mathbb{E}$ by induction on
$(i,\mathit{rank}(t))$.

$\begin{array}[]{rcl}{(\\![{{\rm Nature}}]\\!)}_{i}&=&\mathbb{HV}\cup\\{e\mid
e\longrightarrow^{*}n\\}\\\\[3.0pt]
{(\\![{X}]\\!)}_{i}&=&\mathbb{HV}\\\\[3.0pt] {(\\![{t\times
s}]\\!)}_{i}&=&\mathbb{HV}\cup\\{e\mid e\longrightarrow^{*}\langle
e_{1}\texttt{,}e_{2}\rangle\mbox{ and }e_{1}\in{(\\![{t}]\\!)}_{i}\mbox{ and
}\ ~{}e_{2}\in{(\\![{s}]\\!)}_{i}\\}\\\\[3.0pt] {(\\![{t\to
s}]\\!)}_{i}&=&\mathbb{HV}\cup\\{e\mid e\longrightarrow^{*}\lambda x.f\mbox{
and }ee^{\prime}\in{(\\![{s}]\\!)}_{j}\ \ \forall
e^{\prime}\in{(\\![{t}]\\!)}_{j},j\leq i\\}\\\\[3.0pt] &&{}\cup\\{e\mid
e\longrightarrow^{*}\mathrm{E}[\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}]\mbox{
and }ee^{\prime}\in{(\\![{s}]\\!)}_{j}\ \ \forall
e^{\prime}\in{(\\![{t}]\\!)}_{j},j\leq i\\}\\\\[3.0pt] {(\\![{\bullet
t}]\\!)}_{0}&=&\mathbb{E}\\\\[3.0pt] {(\\![{\bullet
t}]\\!)}_{i+1}&=&{(\\![{t}]\\!)}_{i}\end{array}$

Note that
${(\\![{\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}}]\\!)}_{i}=\mathbb{E}$
for all $i\in\mathbb{N}$. In the interpretation of the arrow type, the
requirement “for all $j\leq i$” (and not just “for all $i$”) is crucial for
dealing with the contra-variance of the arrow type in the proof of Item 2 of
Lemma 3.9.

######  Lemma 3.8.

  1. (1)

${(\\![{\bullet^{n}t}]\\!)}_{i}=\mathbb{E}$ if $i<n$.

  2. (2)

${(\\![{\bullet^{n}t}]\\!)}_{i}={(\\![{t}]\\!)}_{i-n}$ if $i\geq n$.

###### Proof.

Both items are proved by induction on $n$. ∎

######  Lemma 3.9.

For all types $t$ and $i\in\mathbb{N}$,

  1. (1)

$\mathbb{HV}\subseteq{(\\![{t}]\\!)}_{i}$.

  2. (2)

${(\\![{t}]\\!)}_{i+1}\subseteq{(\\![{t}]\\!)}_{i}$.

###### Proof.

(Item 1) follows by induction on $i$ and doing case analysis on the shape of
the type. (Item 2) follows by induction on $(i,\mathit{rank}(t))$. Suppose
$e\in{(\\![{t\to s}]\\!)}_{i+1}$. Then, $ee^{\prime}\in{(\\![{s}]\\!)}_{j}$
for $j\leq i+1$. This is equivalent to saying that
$ee^{\prime}\in{(\\![{s}]\\!)}_{j^{\prime}+1}$ for $j^{\prime}\leq i$. By
induction hypothesis,
${(\\![{s}]\\!)}_{j^{\prime}+1}\subseteq{(\\![{s}]\\!)}_{j^{\prime}}$. Hence,
$e\in{(\\![{t\to s}]\\!)}_{i}$. ∎

######  Lemma 3.10.

If
$t\not=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$
then $\bigcap_{i\in\mathbb{N}}{(\\![{t}]\\!)}_{i}\subseteq\mathbb{WN}$.

###### Proof.

Suppose $t=\bullet^{n}t_{0}$ and $t_{0}$ is either ${\rm Nature}$, $X$,
$t_{1}\to t_{2}$ or $t_{1}\times t_{2}$. Then, for all $i\geq n$,

${(\\![{\bullet^{n}t_{0}}]\\!)}_{i}={(\\![{t_{0}}]\\!)}_{i-n}\subseteq\mathbb{WN}$

by Lemma 3.8 and the definition of type interpretation. ∎

In order to deal with open expressions we resort to substitution functions, as
usual. A substitution function is a mapping from (a finite set of) variables
to $\mathbb{E}$. We use $\rho$ to range over substitution functions.
Substitution functions allows us to extend the semantics to typing judgements
(notation $\Upgamma\models_{i}e:t$).

######  Definition 3.11 (Typing Judgement Interpretation).

Let $\rho$ be a substitution function.

  1. (1)

$\rho\models_{i}\Upgamma$ if $\rho({x})\in{(\\![{t}]\\!)}_{i}$ for all
${x}:t\in\Upgamma$.

  2. (2)

$\Upgamma\models_{i}e:t$ if $\rho(e)\in{(\\![{t}]\\!)}_{i}$ for all
$\rho\models_{i}\Upgamma$.

As expected we can show the soundness of our type system with respect to the
indexed semantics.

######  Theorem 3.12 (Soundness).

If $\Upgamma\vdash e:t$ then $\Upgamma\models_{i}e:t$ for all
$i\in\mathbb{N}$.

The proof of the above theorem can be found in Appendix A.

######  Theorem 3.13 (Normalisation of Typable Expressions).

If $\Upgamma\vdash e:t$ and
$t\not=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$
then $e$ reduces (in zero or more steps) to a (weak head) normal form.

###### Proof.

It follows from Theorem 3.12 that

$\Upgamma\models_{i}e:t$ (3.1)

for all $i\in\mathbb{N}$. Let $id$ be the identity substitution and suppose
${x}:s\in\Upgamma$. Then

$\begin{array}[]{lll}id({x})={x}&\in\mathbb{HV}\\\
&\subseteq{(\\![{s}]\\!)}_{i}&\mbox{by
{\lx@cref{creftype~refnum}{lemma:wnvar}} of
{\lx@cref{creftype~refnum}{lem:A}}.}\end{array}$

This means that $id\models_{i}\Upgamma$ for all $i\in\mathbb{N}$. From Eq. 3.1
we have that $id(e)=e\in{(\\![{t}]\\!)}_{i}$ for all $i$. Hence,

$e\in\bigcap_{i\in\mathbb{N}}{(\\![{t}]\\!)}_{i}$

It follows from Lemma 3.10 that $e\in\mathbb{WN}$. ∎

Notice that there are normalising expressions that cannot be typed, for
example $\lambda
x.\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}\Upomega}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}I}$,
where
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}\Upomega}=(\lambda{y}.{y}\
{y})(\lambda{y}.{y}\ {y})$ and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}I}=\lambda
z.z$. It is easy to show that
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}I}$
has type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$
and so does
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}\Upomega}$
by Lemma 3.5. By Theorem 3.13, it cannot have other types, and this implies
that the application
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}\Upomega}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}I}$
has no type.

Notice also that there are normalizing expressions of type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$,
e.g.
$x:\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}\vdash
x:\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$.
However, there are no normalizaing closed expressions of type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$
as the next lemma shows.

######  Lemma 3.14.

If $\vdash e:t$ and $e$ is normalizing then
$t\not=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$.

###### Proof.

By Theorems 3.13 and 3.5, we can assume that $e$ is a closed expression in
normal form. Then, $e$ could be either $\lambda x.f$ or $\langle
e_{1}\texttt{,}e_{2}\rangle$ or
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}$
or
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}$
or
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
$ or
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
^{n}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}$.
The type of all these expressions is different from
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$.
∎

The function
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}filter}$
that selects the elements of a list $xs$ that satisfy $p$ defined as

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}filter}~{}p~{}xs=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}if}~{}p~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}xs)~{}\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}then}~{}\langle(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}xs)\texttt{,}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}filter}~{}xs)\rangle\
\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}else}\
(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}filter}~{}xs)$

is normalizing (actually it is in normal form) and it can not be typed in
$\lambda^{\bullet}_{\rightarrow}$. Suppose towards a contradiction that
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}filter}$
is typable. Then,
$(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}filter}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}~{}(\lambda
x.{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}eq?}~{}{x}~{}{0}}))$
is also typable. But
$(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}filter}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}~{}(\lambda
x.{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}eq?}~{}{x}~{}{0}}))$
is not normalizing contradicting Theorem 3.13.

###  3.3. Lévy-Longo and Böhm Trees

A simple way to give meaning to a computation of lambda calculus is to
consider Lévy-Longo and Böhm trees [2, 21, 22]. Consider, for example, a
procedure for computing the decimal expansions of $\pi$; if implemented
appropriately, it can provide partial output as it runs and this ongoing
output is a natural way to assign meaning to the computation. This is in
contrast to a program that loops infinitely without ever providing an output.
These two procedures have very different intuitive meanings. This section
gives a nice characterization of computations that never produce meaningless
information by means of types.

In lambda calculus, expressions such as
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}~{}x$
or
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}~{}(\lambda
xy.x)$ have no finite normal form though they are intuitively meaningfull and
should be distinguished from meaningless expressions such as
$fix~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}I}$.
By analogy with $\pi$, the Lévy-Longo (as well as the Böhm) tree of a term is
obtained as the limit of these partial outputs. If in the process of computing
the Lévy-Longo or Böhm tree of a term, we find a subexpression that has no
meaning such as
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}I}$
then this is recorded by replacing
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}I}$
by $\bot$. Lévy-Longo and Böhm trees differ on the notion of meaningless
expressions: weak head normal forms for the former and head normal forms for
the latter.

######  Definition 3.15 (Lèvy-Longo Tree).

Let $e$ be an expression (it may be untypable). The Lèvy-Longo tree of $e$,
denoted as $\mathit{LLT}(e)$ is defined coinductively as follows.

$\begin{array}[]{ll}\mathit{LLT}(e)&=\left\\{\begin{array}[]{ll}x~{}\mathit{LLT}(e_{1})\ldots\mathit{LLT}(e_{n})&\mbox{if
}e\longrightarrow^{*}x~{}e_{1}\ldots e_{n}\\\
\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}~{}\mathit{LLT}(e_{1})\ldots\mathit{LLT}(e_{n})&\mbox{if
}e\longrightarrow^{*}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}~{}e_{1}\ldots
e_{n}\\\ \lambda x.\mathit{LLT}(e^{\prime})&\mbox{if
}e\longrightarrow^{*}\lambda x.e^{\prime}\\\ \bot&\mbox{ otherwise, i.e.
}e\mbox{ has no (weak head) normal form }\end{array}\right.\end{array}$

######  Definition 3.16 (Böhm Tree).

Let $e$ be an expression (it may be untypable). The Böhm tree of $e$, denoted
as $\mathit{BT}(e)$ is defined coinductively as follows.

$\begin{array}[]{ll}\mathit{BT}(e)&=\left\\{\begin{array}[]{ll}\lambda
x_{1}\ldots x_{k}.x~{}\mathit{BT}(f_{1})\ldots\mathit{BT}(f_{n})&\mbox{ if
}\mathit{hnf}(e)=\lambda x_{1}\ldots x_{k}.x~{}f_{1}\ldots f_{n}\\\ \lambda
x_{1}\ldots
x_{k}.\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}~{}\mathit{BT}(f_{1})\ldots\mathit{BT}(f_{n})&\mbox{
if }\mathit{hnf}(e)=\lambda x_{1}\ldots
x_{k}.\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}~{}f_{1}\ldots
f_{n}\\\ \bot&\mbox{ otherwise }\end{array}\right.\end{array}$

where $\mathit{hnf}(e)$ is the head normal form of $e$ defined as follows:

$\begin{array}[]{ll}\mathit{hnf}(e)=&\left\\{\begin{array}[]{ll}\lambda
x_{1}\ldots x_{k}.x~{}f_{1}\ldots f_{n}&\mbox{ if }e=e_{0}\mbox{ and
}e_{k}\longrightarrow^{*}x~{}f_{1}\ldots f_{n}\\\ &\mbox{ and
}e_{i}\longrightarrow^{*}\lambda x_{i+1}.e_{i+1}\mbox{ for }0\leq i\leq k-1\\\
\lambda x_{1}\ldots
x_{k}.\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}~{}f_{1}\ldots
f_{n}&\mbox{ if }e=e_{0}\mbox{ and
}e_{k}\longrightarrow^{*}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}~{}f_{1}\ldots
f_{n}\\\ &\mbox{ and }e_{i}\longrightarrow^{*}\lambda x_{i+1}.e_{i+1}\mbox{
for }0\leq i\leq k-1\\\ \bot&{otherwise}\end{array}\right.\end{array}$

Lévy-Longo and Böhm trees are obtained as possible infinite normal forms of
possible infinite $\beta$-reduction sequences. Infinitary normalization
formalizes the idea of productivity, i.e. an infinite reduction sequence which
always produces part of the result [16, 17, 30, 20]. Besides the $\beta$-rule,
the infinitary lambda calculus of Lévy-Longo trees has a reduction rule
defined as $M\longrightarrow\bot$ if $M$ has no weak head normal form while
the one of Böhm trees has a similar rule using the condition that $M$ has no
head normal form.

######  Definition 3.17.

We say that $t$ is
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$-free
if it does not contain
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$.

For example,
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}$ and
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}E}_{{\rm
Nature}}$ are
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$-free
where
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}E}_{t}=t\to\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}E}_{t}$.
But
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}}$
and ${\rm
Nature}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$
are not
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$-free.

######  Theorem 3.18 (Productivity I: Lèvy-Longo Trees without $\bot$).

Let $t$ and all types in $\Upgamma$ be
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$-free.
If $\Upgamma\vdash e:t$ then the Lèvy-Longo tree of $e$ has no $\bot$’s.

###### Proof.

We construct the Lèvy-Longo tree depth by depth. By Theorem 3.13, $e$ reduces
to a (weak head) normal form $e_{0}$ which is typable by Lemma 3.5. Suppose
$e_{0}$ is $\lambda x.e^{\prime}$ (the cases when $e_{0}=x~{}e_{1}\ldots
e_{n}$ or
$e_{0}=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}~{}e_{1}\ldots
e_{n}$ are similar). The Lèvy-Longo tree of $e$ contains $\lambda x$ at depth
$0$. It only remains to show that we can construct the Lèvy-Longo tree of
$e^{\prime}$ which will be at depth $n>0$. It follows from Inversion Lemma
that $\Gamma,x:t_{1}\vdash e^{\prime}:t_{2}$ and both $t_{1}$ and $t_{2}$ are
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$-free.
Hence, we can repeat the process to obtain the Lèvy-Longo tree of
$e^{\prime}$. ∎

######  Definition 3.19.

  1. (1)

An infinite alternation of $\bullet$’s and $\to$’s is a type of the form:
$t=\bullet^{n_{1}}(t_{1}\to\bullet^{n_{2}}(t_{2}\to\ldots))$.

  2. (2)

We say that $t$ is tail finite if it is
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$-free
and it does not contain an infinite alternation of $\bullet$’s and $\to$’s.

For example,
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}G}={\rm
Nature}\to\bullet({\rm
Nature}\times\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}G})$
is tail finite but
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}F}={\rm
Nature}\to\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}F}$
is not.

######  Theorem 3.20 (Productivity II: Böhm Trees without $\bot$).

Let all the types in $\Upgamma$ and $t$ be tail finite. If $\Upgamma\vdash
e:t$ then the Böhm tree of $e$ has no $\bot$’s.

###### Proof.

By Theorem 3.18, the Lévy-Longo tree of $e$ has no $\bot$’s. Suppose the Lévy-
Longo tree of $e$ contains a subtree of the form $\lambda x_{1}\lambda
x_{2}\lambda x_{3}.\ldots$. It is not difficult to prove using Lemma 3.3 and
Lemma 3.5 that the type should contain an infinite alternation of $\bullet$’s
and $\to$’s. ∎

Let
$e=\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}~{}(\lambda
xy.x)$. Then $e$ has type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}E}_{{\rm
Nature}}$ which is
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\bullet^{\infty}}}$-free
and $\mathit{LLT}(e)=\lambda x.\lambda x.\ldots$ has no $\bot$. For example,
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib}$
has type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{{\rm
Nature}}$ which is tail finite and
$\mathit{BT}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fib})=\langle
0\texttt{,}\langle 1\texttt{,}\langle 1\texttt{,}\langle
2\texttt{,}\ldots\rangle\rangle\rangle\rangle$ has no $\bot$’s.

##  4\. Formal Comparision with Other Type Systems

This section stablishes a formal relation between
$\lambda^{\bullet}_{\rightarrow}$ and the typed lambda calculi of Krishnaswami
and Benton [18] and Nakano [23].

###  4.1. Embedding the Type System by Krishnaswami and Benton into
$\lambda^{\bullet}_{\rightarrow}$

The typing rules of $\lambda^{\text{K}B}$ defined by Krishnaswami and Benton
[18] are:

$\begin{array}[]{@{}c@{}}{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{axiom}}{\text{\scriptsize[{axiom}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle$}}}\vbox{}}}\over\hbox{\hskip
22.78491pt\vbox{\vbox{}\hbox{\hskip-22.7849pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma,{x}:_{i}t\vdash{x}:_{j}t$}}}}}}$}}}~{}~{}j\geq
i\qquad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{const}}{\text{\scriptsize[{const}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
16.21405pt\vbox{\hbox{\hskip-16.21405pt\hbox{\hbox{$\displaystyle\displaystyle\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}:t\in\kappa$}}}\vbox{}}}\over\hbox{\hskip
14.36742pt\vbox{\vbox{}\hbox{\hskip-14.3674pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}:_{i}t$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\bullet$I}}{\text{\scriptsize[{$\displaystyle\bullet$I}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
20.41214pt\vbox{\hbox{\hskip-20.41212pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e:_{i+1}t$}}}\vbox{}}}\over\hbox{\hskip
22.66768pt\vbox{\vbox{}\hbox{\hskip-22.66768pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash\bullet
e:_{i}\bullet
t$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\bullet$E}}{\text{\scriptsize[{$\displaystyle\bullet$E}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
20.44545pt\vbox{\hbox{\hskip-20.44543pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e:_{i}\bullet t$}}}\vbox{}}}\over\hbox{\hskip
32.35493pt\vbox{\vbox{}\hbox{\hskip-32.35492pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}await}~{}e:_{i+1}t$}}}}}}$}}}\\\
\\\
{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$I}}{\text{\scriptsize[{$\displaystyle\to$I}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
25.22261pt\vbox{\hbox{\hskip-25.2226pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma,{x}:_{i}t\vdash
e:_{i}s$}}}\vbox{}}}\over\hbox{\hskip
36.34125pt\vbox{\vbox{}\hbox{\hskip-36.34123pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash\lambda{x}.e:_{i}(t\to
s)$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$E}}{\text{\scriptsize[{$\displaystyle\to$E}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
55.20139pt\vbox{\hbox{\hskip-55.20137pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}:_{i}(t\to s)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{2}:_{i}t$}}}}\vbox{}}}\over\hbox{\hskip
19.72298pt\vbox{\vbox{}\hbox{\hskip-19.72296pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}e_{2}:_{i}s$}}}}}}$}}}\end{array}$

$\lambda^{\text{K}B}$ has only the recursive types
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}=t\times\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{t}$
for infinite lists with only one $\bullet$. Since
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}$
cannot be expressed in $\lambda^{\text{K}B}$, we need to add it to the set
$\kappa$ of constants:

$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}:(\bullet
t\to t)\to t$

The mapping $\mathit{itob}$ replaces the subindex $i$ by $\bullet^{i}$ in
typing contexts.

$\begin{array}[]{ll}\mathit{itob}(\emptyset)&=\emptyset\\\
\mathit{itob}(\Upgamma,{x}:_{i}t)&=\mathit{itob}(\Upgamma),{x}:\bullet^{i}t\end{array}$

The function $\mathit{clear}$ removes the constructor and destructor of
$\bullet$ from $e$, i.e. $\mathit{clear}(\bullet e^{\prime})=e^{\prime}$ and
$\mathit{clear}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}await}~{}e^{\prime})=e^{\prime}$.

######  Lemma 4.1 (Embedding $\lambda^{\text{K}B}$ into
$\lambda^{\bullet}_{\rightarrow}$).

If $\Upgamma\vdash e:_{i}t$ in $\lambda^{\text{K}B}$ then
$\mathit{itob}(\Upgamma)\vdash\mathit{clear}(e):\bullet^{i}t$ in
$\lambda^{\bullet}_{\rightarrow}$.

###### Proof.

By an easy induction on the derivation. ∎

If only recursive types for lists are available, one cannot create other
recursive types such as trees but having only one bullet also limits the
amount of functions on streams we can type. For example, the functions
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}$
(see Eq. 2.1),
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}^{\prime}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pairup}$
are not typable in $\lambda^{\text{K}B}$ where

$\begin{array}[]{ll}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}^{\prime}=\langle
1\texttt{,}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}interleave}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}^{\prime}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}^{\prime})\rangle\\\
\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pairup}~{}xs=\langle\langle(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}xs)\texttt{,}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}xs))\rangle\texttt{,}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}~{}xs))\rangle\end{array}$

The functions
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}skip}$,
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}^{\prime}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pairup}$
are all typeable in $\lambda^{\bullet}_{\rightarrow}$ because
$\lambda^{\bullet}_{\rightarrow}$ has more flexibility in the location and
number of $\bullet$’s which can be inserted in the types. We can derive that
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}ones}^{\prime}$
has type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{X}$
in $\lambda^{\bullet}_{\rightarrow}$ by assigning the type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{X}\to\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{X}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{X}$
to
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}interleave}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pairup}$
has type
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}StrHalf}_{X}\to\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Str1}_{X}$
where
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}StrHalf}_{X}=X\times
X\times\bullet\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}StrHalf}_{X}$.

###  4.2. Embedding $\lambda^{\bullet}_{\rightarrow}$ into the Type System by
Nakano

We consider the type system by Nakano of [23] without $\top$ and call it
$\lambda_{\text{N}ak}$.

Types in $\lambda_{\text{N}ak}$ are finite, written in $\mu$-notation and
denoted by $T$, $S$. Types in $\lambda_{\text{N}ak}$ are guarded which means
that the type variable $X$ of $\mu X.T$ can occur free in $T$ only under the
scope of a $\bullet$.

Let $\simeq$ the equivalence between types which allows for an infinite number
of unfolding and $\Sigma$ be a set $\\{X_{1}\leq Y_{1},\ldots,X_{n}\leq
Y_{n}\\}$ of subtype assumptions between type variables which cannot contain
twice the same variable. The subtyping relation of $\lambda_{\text{N}ak}$ is
defined as the smallest relation on types closed under the following rules:

$\begin{array}[]{@{}c@{}}{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\leq\bullet$}}{\text{\scriptsize[{$\displaystyle\leq\bullet$}]}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
25.56589pt\vbox{\vbox{}\hbox{\hskip-25.56587pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
T\leq\bullet
T$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\bullet\to$}}{\text{\scriptsize[{$\displaystyle\bullet\to$}]}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
45.05186pt\vbox{\vbox{}\hbox{\hskip-45.05186pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
T\to S\leq\bullet T\to\bullet
S$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to\bullet$}}{\text{\scriptsize[{$\displaystyle\to\bullet$}]}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
51.16301pt\vbox{\vbox{}\hbox{\hskip-51.163pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash\bullet
T\to\bullet S\leq\bullet(T\to
S)$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{var}}{\text{\scriptsize[{var}]}}}}}\hbox{$\displaystyle\vbox{\hbox{\hskip
42.09703pt\vbox{\vbox{}\hbox{\hskip-42.09702pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma,X\leq
Y\vdash X\leq Y$}}}}}}$}}}\\\ \\\
{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\simeq$}}{\text{\scriptsize[{$\displaystyle\simeq$}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
13.6371pt\vbox{\hbox{\hskip-13.63708pt\hbox{\hbox{$\displaystyle\displaystyle
T\simeq S$}}}\vbox{}}}\over\hbox{\hskip
23.08148pt\vbox{\vbox{}\hbox{\hskip-23.08147pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
T\leq
S$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\mu$}}{\text{\scriptsize[{$\displaystyle\mu$}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
40.5189pt\vbox{\hbox{\hskip-40.51889pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma,X\leq
Y\vdash T\leq S$}}}\vbox{}}}\over\hbox{\hskip
40.98886pt\vbox{\vbox{}\hbox{\hskip-40.98886pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash\mu
X.T\leq\mu
Y.S$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\bullet$}}{\text{\scriptsize[{$\displaystyle\bullet$}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
23.08148pt\vbox{\hbox{\hskip-23.08147pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
T\leq S$}}}\vbox{}}}\over\hbox{\hskip
27.52596pt\vbox{\vbox{}\hbox{\hskip-27.52594pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash\bullet
T\leq\bullet
S$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$}}{\text{\scriptsize[{$\displaystyle\to$}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
54.00755pt\vbox{\hbox{\hskip-54.00754pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma_{1}\vdash
S_{1}\leq T_{1}\quad\Sigma_{2}\vdash T_{2}\leq
S_{2}$}}}\vbox{}}}\over\hbox{\hskip
51.50752pt\vbox{\vbox{}\hbox{\hskip-51.50752pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma_{1}\cup\Sigma_{2}\vdash
T_{1}\to T_{2}\leq S_{1}\to S_{2}$}}}}}}$}}}\end{array}$

In $\Sigma\vdash T\leq S$, we assume that all the free type variables of $T$
and $S$ are in $\Sigma$ and that the $X$’s cannot occur on the right hand side
of $\leq$ and the $Y$’s cannot occur on the left. The typing rules of
$\lambda_{\text{N}ak}$ are defined as follows.

$\begin{array}[]{@{}c@{\qquad}c@{}}{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{axiom}}{\text{\scriptsize[{axiom}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
18.48778pt\vbox{\hbox{\hskip-18.48776pt\hbox{\hbox{$\displaystyle\displaystyle{x}:T\in\Upgamma$}}}\vbox{}}}\over\hbox{\hskip
16.82114pt\vbox{\vbox{}\hbox{\hskip-16.82112pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash{x}:T$}}}}}}$}}}&{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\leq$}}{\text{\scriptsize[{$\displaystyle\leq$}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
41.2386pt\vbox{\hbox{\hskip-41.23859pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e:T\ \ \ T\leq T^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
19.83934pt\vbox{\vbox{}\hbox{\hskip-19.83932pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e:T^{\prime}$}}}}}}$}}}\\\
{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\bullet$
E}}{\text{\scriptsize[{$\displaystyle\bullet$
E}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
26.01375pt\vbox{\hbox{\hskip-26.01375pt\hbox{\hbox{$\displaystyle\displaystyle\bullet\Upgamma\vdash
e:\bullet T$}}}\vbox{}}}\over\hbox{\hskip
17.68048pt\vbox{\vbox{}\hbox{\hskip-17.68048pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e:T$}}}}}}$}}}{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$I}}{\text{\scriptsize[{$\displaystyle\to$I}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
28.89221pt\vbox{\hbox{\hskip-28.89221pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma,{x}:T\vdash
e:S$}}}\vbox{}}}\over\hbox{\hskip
39.58664pt\vbox{\vbox{}\hbox{\hskip-39.58662pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash\lambda{x}.e:(T\to
S)$}}}}}}$}}}&{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$E}}{\text{\scriptsize[{$\displaystyle\to$E}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
63.76537pt\vbox{\hbox{\hskip-63.76535pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}:\bullet^{n}(T\to S)\ \ \ \Upgamma\vdash
e_{2}:\bullet^{n}T$}}}\vbox{}}}\over\hbox{\hskip
25.33826pt\vbox{\vbox{}\hbox{\hskip-25.33826pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}e_{2}:\bullet^{n}S$}}}}}}$}}}\end{array}$

We define the function $\mathit{nf}_{\\!\\!\\!\mu}$ on guarded $\mu$-types as
follows.

$\begin{array}[]{ll}\begin{array}[]{r@{}l}\mathit{nf}_{\\!\\!\\!\mu}(X)&=X\\\
\mathit{nf}_{\\!\\!\\!\mu}(\bullet T)&=\bullet
T\end{array}&\begin{array}[]{r@{}l}\mathit{nf}_{\\!\\!\\!\mu}(T\to
S)&=\mathit{nf}_{\\!\\!\\!\mu}(T)\to\mathit{nf}_{\\!\\!\\!\mu}(TS)\\\
\mathit{nf}_{\\!\\!\\!\mu}(\mu X.T)&=\mathit{nf}_{\\!\\!\\!\mu}(T)\\{X\mapsto
T\\}\end{array}\end{array}$

We define the translation $\mathit{tree}$ from $\mu$-types to types in
$\lambda^{\bullet}_{\rightarrow}$ by coinduction as follows:

$\begin{array}[]{ll}\mathit{tree}(T)=\left\\{\begin{array}[]{ll}\mathit{tree}(X)&\mbox{
if }\mathit{nf}_{\\!\\!\\!\mu}(T)=X\\\ \bullet\mathit{tree}(S)&\mbox{ if
}\mathit{nf}_{\\!\\!\\!\mu}(T)=\bullet S\\\
\mathit{tree}(T_{1})\to\mathit{tree}(T_{2})&\mbox{ if
}\mathit{nf}_{\\!\\!\\!\mu}(T)=T_{1}\to T_{2}\\\
\end{array}\right.\end{array}$

The translation $\mathit{tree}(\Sigma)$ is extended to typing contexts in the
obvious way.

######  Lemma 4.2 (Embedding $\lambda^{\bullet}_{\rightarrow}$ into
$\lambda_{\text{N}ak}$).

If $\mathit{tree}(\Upgamma)\vdash e:\mathit{tree}(T)$ in
$\lambda^{\bullet}_{\rightarrow}$ without using rule [const] then
$\Upgamma\vdash e:T$ in $\lambda_{\text{N}ak}$.

###### Proof.

It follows by induction on the derivation. It is easy to see that the typing
rules [$\to$I] and [$\bullet$I] of $\lambda^{\bullet}_{\rightarrow}$ are
admissible in $\lambda_{\text{N}ak}$ by making use of the typing rule
[$\leq$]. ∎

Programs in $\lambda_{\text{N}ak}$ have more types than in
$\lambda^{\bullet}_{\rightarrow}$. For example, $\vdash\lambda x.x:(T\to
S)\to(\bullet T\to\bullet S)$ in $\lambda_{\text{N}ak}$ but $\not\vdash\lambda
x.x:(T\to S)\to(\bullet T\to\bullet S)$ in $\lambda^{\bullet}_{\rightarrow}$.

##  5\. Denotational Semantics

This section gives a denotational semantics for
$\lambda^{\bullet}_{\rightarrow}$ where types and expressions are interpreted
as objects and morphisms in the topos of trees [3]. We give a self-contained
description of this topos as a cartesian closed category for a reader familiar
with $\lambda$-calculus.

The topos $\mathcal{S}$ of trees has as objects $A$ families of sets
$A_{1},A_{2},\ldots$ indexed by positive integers, equipped with family of
restrictions $r^{A}_{i}:A_{i+1}\rightarrow A_{i}$. Types will be interpreted
as family of sets (not just sets). Intuitively the family represents better
and better sets of approximants for the values of that type. Arrows
$f:A\rightarrow B$ are families of functions $f_{i}:A_{i}\rightarrow B_{i}$
obeying the naturality condition $f_{i}\circ r_{i}^{A}=r_{i}^{B}\circ
f_{i+1}$.

$\textstyle{A_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{1}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
A_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{r_{1}^{A}}$$\scriptstyle{f_{2}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
A_{3}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{r_{2}^{A}}$$\scriptstyle{f_{3}}$$\textstyle{\ldots}$$\textstyle{B_{1}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
B_{2}}$$\scriptstyle{r_{1}^{B}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
B_{3}}$$\scriptstyle{r_{2}^{B}}$$\textstyle{\ldots}$

We define $r_{ii}^{A}=id_{A}$ and $r_{ij}^{A}=r_{j}\circ\ldots\circ r_{i-1}$
for $1\leq j<i$. Products are defined pointwise.

Exponentials ${B}^{A}$ have as components the sets:

$({B}^{A})_{i}=\\{(f_{1},\ldots,f_{i})\mid f_{j}:A_{j}\rightarrow B_{j}\mbox{
and }f_{j}\circ r_{j}^{A}=r_{j}^{B}\circ f_{j+1}\\}$

and as restrictions $r^{A\Rightarrow B}_{i}(f_{1},\ldots
f_{i+1})=(f_{1},\ldots,f_{i})$.

We define ${eval}:{B}^{A}\times A\rightarrow B$ as
${eval}_{i}((f_{1},\ldots,f_{i}),a)=f_{i}(a)$ and
${curry}(f):C\rightarrow{B}^{A}$ for $f:C\times A\rightarrow B$ as
${curry}(f)_{i}(c)=(g_{1},\ldots,g_{i})$ where
$g_{j}(a)=f_{j}(r_{ij}^{A}(c),a)$ for all $a\in A_{j}$ and $1\leq j\leq i$.
The functor $\blacktriangleright:\mathcal{S}\rightarrow\mathcal{S}$ is defined
on objects as $(\blacktriangleright A)_{1}=\\{*\\}$ and $(\blacktriangleright
A)_{i+1}=A_{i}$ where $r_{1}^{\blacktriangleright A}=!$ and
$r_{i+1}^{\blacktriangleright A}=r_{i}^{A}$ and on arrows
$(\blacktriangleright f)_{1}=id_{\\{*\\}}$ and $(\blacktriangleright
f)_{i+1}=f_{i}$. We write $\blacktriangleright^{n}$ for the $n$-times
composition of $\blacktriangleright$.

The natural transformation ${}_{A}:A\rightarrow\blacktriangleright A$ is given
by $(_{A})_{1}=!$ and $(_{A})_{i+1}=r_{i}^{A}$ which can easily be extended to
a natural transformation ${next}^{n}_{A}:A\rightarrow\blacktriangleright^{n}A$
. It is not difficult to see that there are isomorphisms
$\theta:\blacktriangleright A\times\blacktriangleright
B\rightarrow\blacktriangleright(A\times B)$ and $\xi:{(\blacktriangleright
B)}^{(\blacktriangleright A)}\rightarrow\blacktriangleright({B}^{A})$ which
are also natural. These can also be easily extended to isomorphisms
$\theta^{n}:\blacktriangleright^{n}A\times\blacktriangleright^{n}B\rightarrow\blacktriangleright^{n}(A\times
B)$ and
$\xi^{n}:{(\blacktriangleright^{n}B)}^{(\blacktriangleright^{n}A)}\rightarrow\blacktriangleright^{n}({B}^{A})$.

The category ${Set}$ is a full subcategory of $\mathcal{S}$ via the functor
$\mathcal{I}$ with $(\mathcal{I}(X))_{i}=X$ and $r^{\mathcal{I}(X)}=id_{X}$
and $(\mathcal{I}(f))_{i}=f$. The unit $1$ of $\mathcal{S}$ is
$\mathcal{I}(*)$.

A type $t$ is interpreted as an object in $\mathcal{S}$ (for simplicity, we
omit type variables).

$\begin{array}[]{ll}\begin{array}[]{llllll}[\\!\\![{\rm
Nature}]\\!\\!]&=&\mathcal{I}({\rm Nature})\\\ [\\!\\![t\times
s]\\!\\!]&=&[\\!\\![t]\\!\\!]\times[\\!\\![s]\\!\\!]\end{array}&\ \ \ \ \ \
\begin{array}[]{llllll}[\\!\\![\bullet
t]\\!\\!]&=&\blacktriangleright\circ[\\!\\![t]\\!\\!]\\\ [\\!\\![t\to
s]\\!\\!]&=&{[\\!\\![s]\\!\\!]}^{[\\!\\![t]\\!\\!]}\end{array}\end{array}$

In order to justify that the interpretation is well-defined, it is necessary
to view the above definition as indexed sets and we do induction on
$(i,\mathit{rank}(t))$ taking the lexicographic order where $\mathit{rank}(t)$
is defined in Section 3.2. By writing the indices explicitly in the definition
of $[\\!\\![t]\\!\\!]$, we obtain:

$\begin{array}[]{llllll}[\\!\\![{\rm Nature}]\\!\\!]_{i}&=&{\rm Nature}\\\
[\\!\\![t\times
s]\\!\\!]_{i}&=&[\\!\\![t]\\!\\!]_{i}\times[\\!\\![s]\\!\\!]_{i}\\\
[\\!\\![t\to s]\\!\\!]_{i}&=&\\{(f_{1},\ldots,f_{i})\mid
f_{j}:[\\!\\![t]\\!\\!]_{j}\rightarrow[\\!\\![s]\\!\\!]_{j}\mbox{ and
}f_{j}\circ r_{j}^{[\\!\\![t]\\!\\!]}=r_{j}^{[\\!\\![s]\\!\\!]}\circ
f_{j+1}\\}\\\ [\\!\\![\bullet t]\\!\\!]_{1}&=&\\{*\\}\\\ [\\!\\![\bullet
t]\\!\\!]_{i+1}&=&[\\!\\![t]\\!\\!]_{i}\end{array}$

As it is common in categorical semantics, the interpretation is not defined on
lambda terms in isolation but on typing judgements. In order to define terms
as morphisms, we need the context and the type to specify their domain and co-
domain. Typing contexts $\Upgamma={x}_{1}:t_{1},\ldots{x}_{k}:t_{k}$ are
interpreted as $[\\!\\![t_{1}]\\!\\!]\times\ldots\times[\\!\\![t_{k}]\\!\\!]$.
The interpretation of typed expressions $[\\!\\![\Upgamma\vdash
e:t]\\!\\!]:[\\!\\![\Upgamma]\\!\\!]\rightarrow[\\!\\![t]\\!\\!]$ is defined
by induction on $e$ (using Inversion Lemma):

$\begin{array}[]{lll}[\\!\\![\Upgamma\vdash{x}:\bullet^{n}t]\\!\\!]&=&{next}^{n}\circ\pi_{j}\mbox{
if $x=x_{j}$ and $t_{j}=t$ and $1\leq j\leq k$}\\\
[\\!\\![\Upgamma\vdash\lambda{x}.e:\bullet^{n}(t_{1}\rightarrow
t_{2})]\\!\\!]&=&\xi^{n}\circ{curry}([\\!\\![\Upgamma,{x}:\bullet^{n}t_{1}\vdash
e:\bullet^{n}t_{2}]\\!\\!])\\\ [\\!\\![\Upgamma\vdash
e_{1}e_{2}:\bullet^{n}s]\\!\\!]&=&{eval}\circ\langle(\xi^{n})^{-1}\circ[\\!\\![\Upgamma\vdash
e_{1}:\bullet^{n}(t\rightarrow s)]\\!\\!],[\\!\\![\Upgamma\vdash
e_{2}:\bullet^{n}t]\\!\\!]\rangle\\\
[\\!\\![\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pair}:(t\to
s\to(t\times s))]\\!\\!]&=&{curry}({curry}(!_{[\\!\\![\Upgamma]\\!\\!]}\times
id_{[\\!\\![t\times s]\\!\\!]}))\\\
[\\!\\![\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}:(t\times
s\to t)]\\!\\!]&=&{curry}(!_{[\\!\\![\Upgamma]\\!\\!]}\times\pi_{1})\\\
[\\!\\![\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}:(t\times
s\to s)]\\!\\!]&=&{curry}(!_{[\\!\\![\Upgamma]\\!\\!]}\times\pi_{2})\\\
[\\!\\![\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}:{\rm
Nature}]\\!\\!]&=&\mathcal{I}(*\mapsto 0)\\\
[\\!\\![\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}:({\rm
Nature}\to{\rm Nature})]\\!\\!]&=&succ\end{array}$

######  Lemma 5.1 (Semantic Substitution).

$[\\!\\![\Upgamma,{x}:t\vdash{e_{1}}:s]\\!\\!]\circ\langle
id,[\\!\\![\Upgamma\vdash
e_{2}:t]\\!\\!]\rangle=[\\!\\![\Upgamma\vdash{e_{1}}[e_{2}/{x}]:s]\\!\\!]$

###### Proof.

This follows by induction on $e_{1}$. We only sketch the proof for the case
$e_{1}={x}$.

$\begin{array}[]{ll}[\\!\\![\Upgamma,{x}:t\vdash{{x}}:\bullet^{n}t]\\!\\!]\circ\langle
id,[\\!\\![\Upgamma\vdash
e_{2}:t]\\!\\!]\rangle&={next}^{n}\circ[\\!\\![\Upgamma\vdash
e_{2}:t]\\!\\!]=[\\!\\![\Upgamma\vdash
e_{2}:\bullet^{n}t]\\!\\!]\mbox{}\end{array}$

######  Theorem 5.2 (Soundness).

If $\Upgamma\vdash e:t$ and $e\longrightarrow e^{\prime}$ then
$[\\!\\![\Upgamma\vdash e:t]\\!\\!]=[\\!\\![\Upgamma\vdash
e^{\prime}:t]\\!\\!]$.

###### Proof.

We show the case of [r-beta]. Let
$v_{1}=[\\!\\![\Upgamma,{x}:\bullet^{n}t_{1}\vdash{e_{1}}:\bullet^{n}t_{2}]\\!\\!]$
and $v_{2}=[\\!\\![\Upgamma\vdash e_{2}:\bullet^{n}t_{1}]\\!\\!]$.

$\begin{array}[b]{lll}[\\!\\![\Upgamma\vdash(\lambda{x}.{e_{1}})e_{2}:\bullet^{n}t_{2}]\\!\\!]&=&{eval}\circ\langle(\xi^{n})^{-1}\circ\xi^{n}\circ{curry}(v_{1}),v_{2}\rangle=v_{1}\circ\langle
id,v_{2}\rangle\\\
&=&[\\!\\![\Upgamma\vdash{e_{1}}[e_{2}/{x}]:\bullet^{n}t_{2}]\\!\\!]\mbox{ by
Lemma \ref{lemma:semanticsubstitution}}\end{array}$

We consider contexts $\mathrm{C}$ without any restriction in the position of
the hole $[]$. We say that $\mathrm{C}$ is a closing context of type $t$ if
$x:s\vdash\mathrm{C}[x]:t$ for some variable $x$ that does not occur in
$\mathrm{C}$.

######  Definition 5.3.

Let $\Upgamma\vdash e_{1}:t$ and $\Upgamma\vdash e_{2}:t$. We say that $e_{1}$
and $e_{2}$ are observationally equivalent, denoted by $e_{1}\approx e_{2}$,
if
$\mathrm{C}[e_{1}]\longrightarrow^{*}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}^{n}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}$
iff
$\mathrm{C}[e_{2}]\longrightarrow^{*}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}^{n}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}$
for all closing contexts $\mathrm{C}$ of type ${\rm Nature}$.

######  Corollary 5.4.

If $[\\!\\![\Upgamma\vdash e_{1}:t]\\!\\!]=[\\!\\![\Upgamma\vdash
e_{2}:t]\\!\\!]$ then, $e_{1}\approx e_{2}$.

###### Proof.

By compositionality of the denotational semantics,
$[\\!\\![\vdash\mathrm{C}[e_{1}]:{\rm
Nature}]\\!\\!]=[\\!\\![\vdash\mathrm{C}[e_{2}]:{\rm Nature}]\\!\\!]$. Suppose
$\mathrm{C}[e_{1}]\longrightarrow^{*}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}^{n}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}$.
By Theorem 5.2, $[\\!\\![\vdash\mathrm{C}[e_{1}]:{\rm
Nature}]\\!\\!]=[\\!\\![\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}^{n}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}]\\!\\!]$.
By Theorem 3.13,
$\mathrm{C}[e_{2}]\longrightarrow^{*}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}^{m}~{}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}$.
It is not difficult to show using the definition of interpretation that $m=n$.
∎

##  6\. A Type Inference Algorithm

In this section, we define a type inference algorithm for
$\lambda^{\bullet}_{\rightarrow}$. Apart from the usual complications that
come from having no type declarations, the difficulty of finding an
appropriate type inference algorithm for $\lambda^{\bullet}_{\rightarrow}$ is
due to the fact that the expressions do not have a constructor and destructor
for $\bullet$. We do not know which sub-expressions need to be delayed as
illustrated by the type derivation of
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fix}$
where the first occurrence of $(\lambda{x}.{y}\ ({x}\ {x}))$ has a different
derivation from the second one since [$\bullet$I] is applied in different
places [23]. Even worse, in case a sub-expression has to be delayed, we do not
know how many times needs to be delayed to be able to type the whole
expression.

###  6.1. A Syntax-directed Type System

We obtain a syntax-directed type system by eliminating the rule [$\bullet$I]
from $\lambda^{\bullet}_{\rightarrow}$. The type assignment system
$(\lambda^{\bullet}_{\rightarrow})^{-}$ is defined by the following rules.

$\begin{array}[]{@{}c@{}}{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{axiom}}{\text{\scriptsize[{axiom}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
16.677pt\vbox{\hbox{\hskip-16.677pt\hbox{\hbox{$\displaystyle\displaystyle{x}:t\in\Upgamma$}}}\vbox{}}}\over\hbox{\hskip
16.41331pt\vbox{\vbox{}\hbox{\hskip-16.41331pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash{x}:\bullet^{n}t$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{const}}{\text{\scriptsize[{const}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
16.21405pt\vbox{\hbox{\hskip-16.21405pt\hbox{\hbox{$\displaystyle\displaystyle\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}:t\in\kappa$}}}\vbox{}}}\over\hbox{\hskip
17.58344pt\vbox{\vbox{}\hbox{\hskip-17.58344pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}:\bullet^{n}t$}}}}}}$}}}\quad\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$I}}{\text{\scriptsize[{$\displaystyle\to$I}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
30.26581pt\vbox{\hbox{\hskip-30.2658pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma,{x}:\bullet^{n}t\vdash
e:\bullet^{n}s$}}}\vbox{}}}\over\hbox{\hskip
39.55727pt\vbox{\vbox{}\hbox{\hskip-39.55727pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash\lambda{x}.e:\bullet^{n}(t\to
s)$}}}}}}$}}}\quad\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$E}}{\text{\scriptsize[{$\displaystyle\to$E}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
59.13342pt\vbox{\hbox{\hskip-59.1334pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}:\bullet^{n}(t\to s)\ \ \ \Upgamma\vdash
e_{2}:\bullet^{n}t$}}}\vbox{}}}\over\hbox{\hskip
24.32785pt\vbox{\vbox{}\hbox{\hskip-24.32785pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}e_{2}:\bullet^{n}s$}}}}}}$}}}\end{array}$

######  Lemma 6.1 (Equivalence between $\lambda^{\bullet}_{\rightarrow}$ and
$(\lambda^{\bullet}_{\rightarrow})^{-}$).

$\Upgamma\vdash e:t$ in $(\lambda^{\bullet}_{\rightarrow})^{-}$ iff
$\Upgamma\vdash e:t$ in $\lambda^{\bullet}_{\rightarrow}$.

###### Proof.

The direction from left to right follows by induction on the derivation. The
direction from right to left follows by induction on $e$ using Lemma 3.3. ∎

Though $\lambda^{\bullet}_{\rightarrow}$ and
$(\lambda^{\bullet}_{\rightarrow})^{-}$ are equivalent in the sense they type
the same expressions, they do not have the same type derivations. The
derivations of $(\lambda^{\bullet}_{\rightarrow})^{-}$ are more restrictive
than the ones of $\lambda^{\bullet}_{\rightarrow}$ since one can only
introduce $\bullet$’s at the beginning of the derivation with the rules
[axiom] and [const].

###  6.2. Meta-types

The type inference algorithm infers meta-types which are a generalization of
types where the $\bullet$ can be exponentiated with integer expressions, e.g.
$\bullet^{N_{1}}X\rightarrow\bullet^{N_{2}-N_{1}}X$. The syntax for meta-types
is defined below. A meta-type can contain type variables and (non-negative)
integer expressions with variables. In this syntax, $\bullet T$ is written as
$\bullet^{1}T$. We identify $\bullet^{0}T$ with $T$ and
$\bullet^{E}\bullet^{E^{\prime}}T$ with $\bullet^{E+E^{\prime}}T$.

$\begin{array}[]{@{}l@{\qquad}l@{}}\begin{array}[t]{r@{~~}c@{~~}l@{\quad}l}E~{}~{}&::=^{ind}\hfil~{}~{}&&\textbf{Integer
Expression}\\\ ~{}~{}&\hfil~{}~{}&N&\text{(integer variable)}\\\
~{}~{}&|\hfil~{}~{}&\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}n}&\text{(integer
number)}\\\ ~{}~{}&|\hfil~{}~{}&E+E&\text{(addition)}\\\
~{}~{}&|\hfil~{}~{}&E-E&\text{(substraction)}\end{array}\quad\begin{array}[t]{r@{~~}c@{~~}l@{\quad}l}T~{}~{}&::=^{coind}\hfil~{}~{}&&\textbf{Pseudo
Meta-type}\\\ ~{}~{}&\hfil~{}~{}&X&\text{(type variable)}\\\
~{}~{}&|\hfil~{}~{}&{\rm Nature}&\text{(natural numbers)}\\\
~{}~{}&|\hfil~{}~{}&T\times T&\text{(product)}\\\ ~{}~{}&|\hfil~{}~{}&T\to
T&\text{(arrow)}\\\
~{}~{}&|\hfil~{}~{}&\bullet^{E}T&\text{(delay)}\end{array}\end{array}$

######  Definition 6.2.

We say that $T$ is positive if all the exponents of $\bullet$ are natural
numbers.

We identify a positive pseudo meta-type with the pseudo-type obtained from
replacing the type constructor $\bullet^{n}$ in the syntax of pseudo meta-
types with $n$ consecutive $\bullet$’s in the syntax of pseudo-types.

######  Definition 6.3 (Integer Expression and Type Substitution).

Let $\tau=\\{X_{1}\mapsto T_{1},\ldots,X_{n}\mapsto T_{n}\\}$ be a finite
mapping from type variables to pseudo meta-types where
${dom}(\tau)=\\{X_{1},\ldots,X_{n}\\}$. Let $\theta=\\{N_{1}\mapsto
E_{1},\ldots,N_{m}\mapsto E_{m}\\}$ be a finite mapping from integer variables
to integer expressions where ${dom}(\theta)=\\{N_{1},\ldots,N_{m}\\}$. Let
also $\sigma=\tau\cup\theta$. We define the substitutions $\theta(E)$ on an
integer expression $E$ and $\sigma(T)$ on a pseudo meta-type $T$ as follows.

$\begin{array}[]{lll}\begin{array}[]{lll}\theta(N)&=&\left\\{\begin{array}[]{ll}E&\mbox{
if $N\mapsto E\in\theta$ }\\\ N&\mbox{ otherwise}\end{array}\right.\\\
\theta(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}n})&=&\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}n}\\\
\theta(E_{1}+E_{2})&=&\theta(E_{1})+\theta(E_{2})\\\
\theta(E_{1}-E_{2})&=&\theta(E_{1})-\theta(E_{2})\end{array}\quad\begin{array}[]{lll}\sigma(X)&=&\left\\{\begin{array}[]{ll}T&\mbox{
if $X\mapsto T\in\tau$ }\\\ X&\mbox{ otherwise}\end{array}\right.\\\
\sigma({\rm Nature})&=&{\rm Nature}\\\ \sigma(T_{1}\to
T_{2})&=&\sigma(T_{1})\to\sigma(T_{2})\\\ \sigma(T_{1}\times
T_{2})&=&\sigma(T_{1})\times\sigma(T_{2})\\\
\sigma(\bullet^{E}T)&=&\bullet^{\theta(E)}\sigma(T)\end{array}\end{array}$

If the substitution $\tau$ is $\\{X\mapsto T\\}$ then $\tau(T)$ is also
denoted as $T\\{X\mapsto T\\}$ as usual.

Composition of substitutions is defined as usual. Note that the empty set is
the identity substitution and $\sigma=\theta\circ\tau$ if
$\sigma=\tau\cup\theta$.

######  Definition 6.4.

We say that $\theta$ is natural if it maps all integer variables into natural
numbers, i.e. $\theta(N)\in\mathbb{N}$ for all $N\in{dom}(\tau)$.

For example, the substitution $\theta=\\{N\mapsto 3,M\mapsto 5\\}$ is natural
but $\theta(\bullet^{N-M}{\rm Nature})$ is not positive.

We can define regular pseudo meta-types similar to Definition 2.1. We say that
a pseudo meta-type $T$ is guarded if $\theta(T)$ is positive and guarded (as a
pseudo type) for all natural $\theta$.

The pseudo meta-type which is solution of the recursive equation $T={\rm
Nature}\times\bullet^{N}T$ is not guarded but it is guarded if we substitute
$N$ by $M+1$.

######  Definition 6.5.

A meta-type is a pseudo meta-type that is regular and guarded.

Note that finite pseudo meta-types are always meta-types, e.g. ${\rm
Nature}\times\bullet^{N}X$ is a meta-type.

######  Definition 6.6.

We say that the substitution $\sigma=\tau\cup\theta$ is:

  1. (1)

guarded if $\sigma(X)$ is guarded for all $X\in{dom}(\tau)$.

  2. (2)

meta-type if it is a substitution from type variables to meta-types.

  3. (3)

positive if $\theta$ is natural and $\theta(\tau(X))$ is positive for all
$X\in{dom}(\tau)$.

  4. (4)

type if it is meta-type and positive.

Note that a type substitution $\sigma=\tau\cup\theta$ is a substitution from
type variables to types where $\theta$ is natural.

######  Definition 6.7 (Constraints).

There are two types of constraints.

  1. (1)

A meta-type constraint is $T\stackrel{{\scriptstyle{?}}}{{{=}}}T^{\prime}$ for
finite meta-types $T$ and $T^{\prime}$.

  2. (2)

An integer constraint is either
$E\stackrel{{\scriptstyle{?}}}{{{=}}}E^{\prime}$ or $E\
\stackrel{{\scriptstyle{?}}}{{{\geq}\ }}E^{\prime}$ or $E\
\stackrel{{\scriptstyle{?}}}{{{<}}}\ E^{\prime}$.

Sets of constraints are denoted by $\mathcal{C},\mathcal{E}$, etc. If
$\mathcal{C}$ is a set of meta-type constraints then,

  1. (1)

${\mathcal{C}}^{=}$ denotes the subset of equality constraints from
$\mathcal{C}$,

  2. (2)

$\mathcal{C}^{\mathbb{N}}$ denotes the set of integer constraints from
$\mathcal{C}$.

Moreover, $\sigma\models T\stackrel{{\scriptstyle{?}}}{{{=}}}T^{\prime}$ means
that $\sigma(T)=\sigma(T^{\prime})$. Similarly, we define $\theta\models
E\stackrel{{\scriptstyle{?}}}{{{=}}}E^{\prime}$, $\theta\models E\
\stackrel{{\scriptstyle{?}}}{{{\geq}\ }}E^{\prime}$ and $\theta\models E\
\stackrel{{\scriptstyle{?}}}{{{<}}}\ E^{\prime}$. This notation extends to
sets $\mathcal{C}$ of constraints in the obvious way. When
$\sigma\models\mathcal{C}$, we say that $\sigma$ is a solution (unifier) for
$\mathcal{C}$.

######  Definition 6.8.

We say that $\tau$ is:

  1. (1)

$\mathcal{E}$-guarded if $\theta\circ\tau$ is guarded for all natural
substitution $\theta$ such that $\theta\models\mathcal{E}$.

  2. (2)

$\mathcal{E}$-positive if $\theta\circ\tau$ is positive for all natural
substitution $\theta$ such that $\theta\models\mathcal{E}$.

Recall that
$\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Stream}({N},{Y})=Y\times\bullet^{N}\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Stream}({N},{Y})$.
For example,

  1. (1)

$\tau=\\{X\mapsto\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Stream}({N},{Y})\\}$
is $\mathcal{E}$-guarded but it is not $\emptyset$-guarded for
$\mathcal{E}=\\{N\ \stackrel{{\scriptstyle{?}}}{{{\geq}\ }}1\\}$ and,

  2. (2)

$\tau=\\{X\mapsto\bullet^{M-N}{\rm Nature}\\}$ is $\mathcal{E}$-positive but
it is not $\emptyset$-positive for $\mathcal{E}=\\{M\
\stackrel{{\scriptstyle{?}}}{{{\geq}\ }}N\\}$.

######  Definition 6.9.

We say that $\mathcal{C}$ is _substitutional_ if
${\mathcal{C}}^{=}=\\{X_{1}\stackrel{{\scriptstyle{?}}}{{{=}}}T_{1},\ldots,X_{n}\stackrel{{\scriptstyle{?}}}{{{=}}}T_{n}\\}$,
all variables $X_{1},\ldots,X_{n}$ are pairwise different.

Since a substitutional $\mathcal{C}$ corresponds to a set of recursive
equations where $T_{1},\ldots,T_{n}$ are finite meta-types, there exists a
unique solution $\tau_{\mathcal{C}}$ such that $\tau_{\mathcal{C}}(X_{i})$ is
regular for all $1\leq i\leq n$ [10], [6, Theorem 7.5.34]. The mapping
$\tau_{\mathcal{C}}$ is the most general unifier, i.e. if
$\sigma\models\mathcal{C}$ then there exists $\sigma^{\prime}$ such that
$\sigma=\sigma^{\prime}\circ\tau_{\mathcal{C}}$. Moreover, if
$\sigma=\tau\cup\theta$ then $\sigma^{\prime}=\tau^{\prime}\cup\theta$ where

$\begin{array}[]{ll}\tau^{\prime}(X)&=\left\\{\begin{array}[]{ll}\tau(X)&\mbox{
if }X\neq X_{i}\mbox{ for all }1\leq i\leq n\\\
X&\mbox{otherwise}\end{array}\right.\end{array}$

For example, if
$\mathcal{C}=\\{X\stackrel{{\scriptstyle{?}}}{{{=}}}Y\times\bullet^{N}X\\}$
then
$\tau_{\mathcal{C}}(X)=\mathtt{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}Stream}({N},{Y})$.
If $\sigma\models\mathcal{C}$ and $\sigma=\tau\cup\theta$ then
$\sigma=\sigma^{\prime}\circ\tau_{\mathcal{C}}$ and
$\sigma^{\prime}=\tau^{\prime}\cup\theta$ and
$\tau^{\prime}=\\{Y\mapsto\tau(Y)\\}$.

Note that the unicity of the solution of a set of recursive equations would
not be guaranteed if we were following the iso-recursive approach which allows
only for a finite number of unfoldings $\mu X.t=t\\{X\mapsto\mu X.t\\}$ [5,
6].

For $1\leq i\leq n$, we know that $\tau_{\mathcal{C}}(X_{i})$ is regular but
we do not know yet if $\tau_{\mathcal{C}}$ is guarded or positive. Below, we
show some examples:

  1. (1)

Let $\mathcal{C}=\\{X_{1}\stackrel{{\scriptstyle{?}}}{{{=}}}X_{2}\to\bullet
X_{1},X_{2}\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet X_{1}\to\bullet
X_{2}\\}$. Then, $\tau_{\mathcal{C}}=\\{X_{1}\mapsto t_{1},X_{2}\mapsto
t_{2}\\}$ is a type substitution where $t_{1}$ and $t_{2}$ satisfy the
recursive equations $t_{1}=t_{2}\to\bullet t_{1}$ and $t_{2}=\bullet
t_{1}\to\bullet t_{2}$.

  2. (2)

Let $\mathcal{C}=\\{X_{1}\stackrel{{\scriptstyle{?}}}{{{=}}}X_{2}\to\bullet
X_{1},X_{2}\stackrel{{\scriptstyle{?}}}{{{=}}}X_{1}\to\bullet X_{2}\\}$. Then,
$\tau_{\mathcal{C}}=\\{X_{1}\mapsto t_{1},X_{2}\mapsto t_{2}\\}$ is positive
where $t_{1}$ and $t_{2}$ satisfy the recursive equations
$t_{1}=t_{2}\to\bullet t_{1}$ and $t_{2}=t_{1}\to\bullet t_{2}$. But
$\tau_{\mathcal{C}}$ is not guarded since there is an infinite branch in the
tree representations of $t_{1}$ and $t_{2}$ that has no $\bullet$’s. Observe
that $t_{1}=(t_{1}\to\bullet t_{2})\to\bullet t_{1}$ and
$t_{2}=(t_{2}\to\bullet t_{1})\to\bullet t_{2}$.

  3. (3)

Let
$\mathcal{C}=\\{X_{1}\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{N+1}(X_{2}\to\bullet
X_{1}),X_{2}\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{M}X_{1}\\}$. Then,
$\tau_{\mathcal{C}}=\\{X_{1}\mapsto T_{1},X_{2}\mapsto T_{2}\\}$ is a meta-
type substitution where $T_{1}$ and $T_{2}$ satisfy the recursive equations
$T_{1}=\bullet^{N+1}(T_{2}\to\bullet T_{1})$ and $T_{2}=\bullet^{M}T_{1}$. But
$\tau_{\mathcal{C}}$ is not positive since $N$ and $M$ are integer variables.

######  Definition 6.10.

We say that $\mathcal{C}$ is

  1. (1)

always positive if all the meta-types in $\theta({\mathcal{C}}^{=})$ are
positive for all natural substitution $\theta$ such that
$\theta\models\mathcal{C}^{\mathbb{N}}$.

  2. (2)

simple if $0\ \stackrel{{\scriptstyle{?}}}{{{<}}}\ E\in\mathcal{C}$ for all
$X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{E}X^{\prime}\in\mathcal{C}$.

For example,
$\mathcal{C}=\\{X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{N}(X_{1}\to
X_{2}),N\ \stackrel{{\scriptstyle{?}}}{{{\geq}\ }}1\\}$ is always positive
while $\mathcal{C}=\\{X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{N}(X_{1}\to
X_{2})\\}$ is not.

###  6.3. Constraint Typing Rules

The constraint typing rules for $\lambda^{\bullet}_{\rightarrow}$ are given in
Table 1. Since
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pair}$,
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst}$
and
$\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}$
are actually ‘polymorphic’, we need to generate different fresh variables
depending on their position. For convenience, we define the following
function:

$\begin{array}[]{ll}\mathtt{typeOf}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pair},X_{1},X_{2})&=X_{1}\to
X_{2}\to X_{1}\times X_{2}\\\
\mathtt{typeOf}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst},X_{1},X_{2})&=X_{1}\times
X_{2}\to X_{1}\\\
\mathtt{typeOf}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd},X_{1},X_{2})&=X_{1}\times
X_{2}\to X_{2}\end{array}$

Table 1. Constraint Typing Rules for $\lambda^{\bullet}_{\rightarrow}$

$\begin{array}[]{@{}l@{}l}{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{axiom}}{\text{\scriptsize[{axiom}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
21.71529pt\vbox{\hbox{\hskip-21.71527pt\hbox{\hbox{$\displaystyle\displaystyle
N\mbox{ is fresh}$}}}\vbox{}}}\over\hbox{\hskip
44.83961pt\vbox{\vbox{}\hbox{\hskip-44.83961pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,{x}:X\vdash{x}:\bullet^{N}X\
\mid\
\emptyset$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\times$
const}}{\text{\scriptsize[{$\displaystyle\times$
const}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
41.0708pt\vbox{\hbox{\hskip-41.07079pt\hbox{\hbox{$\displaystyle\displaystyle
N,X_{1},X_{2}\mbox{ are fresh}$}}}\vbox{}}}\over\hbox{\hskip
66.36887pt\vbox{\vbox{}\hbox{\hskip-66.36887pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}:\bullet^{N}\mathtt{typeOf}(\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k},X_{1},X_{2})\
\mid\
\emptyset$}}}}}}$}}}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}k}\in\\{\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}pair},\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}fst},\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}snd}\\}\\\
\\\ {\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{${\rm
Nature}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}$}}{\text{\scriptsize[{$\displaystyle{\rm
Nature}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}$}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
21.71529pt\vbox{\hbox{\hskip-21.71527pt\hbox{\hbox{$\displaystyle\displaystyle
N\mbox{ is fresh}$}}}\vbox{}}}\over\hbox{\hskip
43.54109pt\vbox{\vbox{}\hbox{\hskip-43.54109pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}0}:\bullet^{N}{\rm
Nature}\ \mid\
\emptyset$}}}}}}$}}}\quad{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{${\rm
Nature}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
$}}{\text{\scriptsize[{$\displaystyle{\rm
Nature}\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
$}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
21.71529pt\vbox{\hbox{\hskip-21.71527pt\hbox{\hbox{$\displaystyle\displaystyle
N\mbox{ is fresh}$}}}\vbox{}}}\over\hbox{\hskip
75.6661pt\vbox{\vbox{}\hbox{\hskip-75.6661pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathtt{\color[rgb]{0.5,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0,0.5}succ}\
:\bullet^{N}({\rm Nature}\to{\rm Nature})\ \mid\ \emptyset$}}}}}}$}}}\\\ \\\
{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$I}}{\text{\scriptsize[{$\displaystyle\to$I}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
101.44212pt\vbox{\hbox{\hskip-101.44212pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,{x}:X\vdash
e:T\ \mid\ \mathcal{C}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle X,X_{1},X_{2},N\mbox{ are
fresh}$}}}}\vbox{}}}\over\hbox{\hskip
114.29605pt\vbox{\vbox{}\hbox{\hskip-114.29604pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\lambda{x}.e:\bullet^{N}(X_{1}\to
X_{2})\ \mid\
\mathcal{C}\cup\\{X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{N}X_{1},T\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{N}X_{2}\\}$}}}}}}$}}}\\\
\\\
{\vbox{\hbox{\hbox{\small\small{\hypertarget{rule:{$\to$E}}{\text{\scriptsize[{$\displaystyle\to$E}]}}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
131.08171pt\vbox{\hbox{\hskip-131.08171pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash
e_{1}:T_{1}\ \mid\ \mathcal{C}_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash e_{2}:T_{2}\
\mid\ \mathcal{C}_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle X_{1},X_{2},N\mbox{ are
fresh}$}}}}}\vbox{}}}\over\hbox{\hskip
120.83157pt\vbox{\vbox{}\hbox{\hskip-120.83156pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash
e_{1}e_{2}:\bullet^{N}X_{2}\ \mid\
\mathcal{C}_{1}\cup\mathcal{C}_{2}\cup\\{\bullet^{N}(X_{1}\to
X_{2})\stackrel{{\scriptstyle{?}}}{{{=}}}T_{1},\bullet^{N}X_{1}\stackrel{{\scriptstyle{?}}}{{{=}}}T_{2}\\}$}}}}}}$}}}\end{array}$

The typing rules should be read bottom-up. We start from an empty context and
a closed expression and we build the typing context $\Delta$ and the set
$\mathcal{C}$ of constraints. We can, then, assume that the typing context
$\Delta$ only contains declarations of the form ${x}:X$ and the set
$\mathcal{C}$ contains only equality constraints between finite meta-types.The
type variables in the contexts $\Delta$ are all fresh and they are created by
the rule [$\to$I] for the abstraction.

If instead of generating the fresh variable $X$ in [$\to$I] we directly put
$\bullet^{N}X_{1}$ in the context, then the algorithm would not be complete.
For example, consider $x:\bullet^{5}{\rm Nature}\vdash x:\bullet^{7}{\rm
Nature}$. Then $N$ should be assigned the value $3$ and not $5$ if later we
derive that $\lambda x.x:\bullet^{2}(\bullet^{3}{\rm Nature}\to\bullet^{5}{\rm
Nature})$.

######  Theorem 6.11 (Soundness of Constraint Typing).

Let $\sigma$ be a type substitution. If $\Delta\vdash e:T\ \mid\ \mathcal{C}$
and $\sigma\models\mathcal{C}$ then $\sigma(\Delta)\vdash e:\sigma(T)$ in
$(\lambda^{\bullet}_{\rightarrow})^{-}$ and $\sigma(T)$ is a type.

###### Proof.

We proceed by induction on the derivation of $\Delta\vdash e:T\ \mid\
\mathcal{C}$. Suppose the last rule in the derivation of $\Delta\vdash e:T\
\mid\ \mathcal{C}$ is:

[$\displaystyle\to$I] $\displaystyle\displaystyle{\hbox{\hskip
102.21213pt\vbox{\hbox{\hskip-102.21211pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,{x}:X\vdash
e:T^{\prime}\ \mid\ \mathcal{C}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle X,X_{1},X_{2},N\mbox{ are
fresh}$}}}}\vbox{}}}\over\hbox{\hskip
115.06604pt\vbox{\vbox{}\hbox{\hskip-115.06604pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\lambda{x}.e:\bullet^{N}(X_{1}\to
X_{2})\ \mid\
\mathcal{C}\cup\\{X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{N}X_{1},T^{\prime}\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{N}X_{2}\\}$}}}}}}$

It follows from induction hypothesis that $\sigma(\Delta),{x}:\sigma(X)\vdash
e:\sigma(T^{\prime})$. Since
$\sigma\models\\{X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{N}X_{1},T^{\prime}\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{N}X_{2}\\}$,
we also have that $\sigma(\Delta),{x}:\bullet^{\sigma(N)}\sigma(X_{1})\vdash
e:\bullet^{\sigma(N)}\sigma(X_{2})$. We can, then, apply [$\to$I] of
$(\lambda^{\bullet}_{\rightarrow})^{-}$ to conclude that
$\sigma(\Delta)\vdash\lambda{x}.e:\bullet^{\sigma(N)}(\sigma(X_{1})\to\sigma(X_{2}))$.
It follows from the fact that $\sigma$ is a type substitution that
$\sigma(T)=\bullet^{\sigma(N)}(\sigma(X_{1})\to\sigma(X_{2}))$ is a type. ∎

######  Theorem 6.12 (Completeness of Constraint Typing).

Let $\Upgamma={x}_{1}:t_{1},\ldots,{x}_{m}:t_{m}$ and
$\Delta={x}_{1}:X_{1},\ldots,{x}_{m}:X_{m}$. If $\Upgamma\vdash e:t$ in
$(\lambda^{\bullet}_{\rightarrow})^{-}$ then there are $T$ and $\mathcal{C}$
such that

  1. (1)

$\Delta\vdash e:T\ \mid\ \mathcal{C}$

  2. (2)

there exists a type substitution $\sigma\supseteq\\{X_{1}\mapsto
t_{1},\ldots,X_{m}\mapsto t_{m}\\}$ such that $\sigma\models\mathcal{C}$ and
$\sigma(T)=t$ and ${dom}(\sigma)\setminus\\{X_{1},\ldots,X_{m}\\}$ is the set
of fresh variables in the derivation of $\Delta\vdash e:T\ \mid\ \mathcal{C}$.

###### Proof.

We proceed by induction on the derivation. Suppose the last typing rule in the
derivation is:

[axiom] $\displaystyle\displaystyle{\hbox{\hskip
17.21742pt\vbox{\hbox{\hskip-17.21742pt\hbox{\hbox{$\displaystyle\displaystyle{x}_{i}:t_{i}\in\Upgamma$}}}\vbox{}}}\over\hbox{\hskip
19.73145pt\vbox{\vbox{}\hbox{\hskip-19.73145pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash{x}_{i}:\bullet^{n}t_{i}$}}}}}}$

Then, $\Delta\vdash{x}_{i}:\bullet^{N}X_{i}\ \mid\ \emptyset$. We define
$\sigma=\\{X_{1}\mapsto t_{1},\ldots,X_{m}\mapsto t_{m}\\}\cup\\{N\mapsto
n\\}$. It is easy to see that $\sigma(\Delta)=\Upgamma$ and
$t=\sigma(\bullet^{N}X_{i})$.

Suppose the last typing rule in the derivation is:

[$\displaystyle\to$E] $\displaystyle\displaystyle{\hbox{\hskip
59.13342pt\vbox{\hbox{\hskip-59.1334pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}:\bullet^{n}(t\to s)\ \ \ \Upgamma\vdash
e_{2}:\bullet^{n}t$}}}\vbox{}}}\over\hbox{\hskip
24.32785pt\vbox{\vbox{}\hbox{\hskip-24.32785pt\hbox{\hbox{$\displaystyle\displaystyle\Upgamma\vdash
e_{1}e_{2}:\bullet^{n}s$}}}}}}$

By induction hypotheses,

  * $-$

$\Delta\vdash e_{1}:T_{1}\ \mid\ \mathcal{C}_{1}$ and $\Delta\vdash
e_{2}:T_{2}\ \mid\ \mathcal{C}_{2}$,

  * $-$

$\sigma_{1}\models\mathcal{C}_{1}$ and $\sigma_{2}\models\mathcal{C}_{2}$ and
$\sigma_{1}(T_{1})=\bullet^{n}(t\to s)$ and $\sigma_{2}(T_{1})=\bullet^{n}s$
for $\sigma_{1},\sigma_{2}\supseteq\\{X_{1}\mapsto t_{1},\ldots,X_{m}\mapsto
t_{m}\\}$,

  * $-$

${dom}(\sigma_{1})\setminus\\{X_{1},\ldots,X_{m}\\}$ and
${dom}(\sigma_{2})\setminus\\{X_{1},\ldots,X_{m}\\}$ are the sets of fresh
variables in the derivation of $\Delta\vdash e_{1}:T_{1}\ \mid\
\mathcal{C}_{1}$ and $\Delta\vdash e_{2}:T_{2}\ \mid\ \mathcal{C}_{2}$,
respectively.

It follows from the latter that $\sigma_{1}\cup\sigma_{2}$ is a function and
we can define the substitution $\sigma$ as
$(\sigma_{1}\cup\sigma_{2})\\{N\mapsto n\\}\\{X_{1}\mapsto t\\}\\{X_{2}\mapsto
s\\}$. ∎

###  6.4. Unification Algorithm

Algorithm 1 solves the unification problem. The input consists of a set
$\mathcal{C}$ of constraints and an extra argument $\mathcal{V}$ that keeps
tracks of the “visited equality constraints” and guarantees termination.

Function  _$\mathtt{unify}(\mathcal{C},\mathcal{V})$_

input : $\mathcal{C}$ is a set of constraints and $\mathcal{V}$ is the set of
visited equality constraints

output :
$\\{\langle\tau,\mathcal{E}\rangle\mid\tau\cup\theta\models\mathcal{C}\
\forall\theta\models\mathcal{E}\\}$

1

2 if  _$\mathcal{C}$ is substitutional and simple _ then

3
$\mathcal{E}\leftarrow\mathcal{C}^{\mathbb{N}}\cup\mathtt{guard}(\mathcal{C})$
;

4 if  _ $\mathcal{E}$ has a solution of non-negative integers _ then return
_$\\{\langle\tau_{\mathcal{C}},\mathcal{E}\rangle\\}$_ else return
_$\emptyset$_ ;

5

6 else if  _$T\stackrel{{\scriptstyle{?}}}{{{=}}}S\in\mathcal{C}$ _ then

7
$\mathcal{C}^{\prime}\leftarrow\mathcal{C}\setminus\\{T\stackrel{{\scriptstyle{?}}}{{{=}}}S\\}$;
$\mathcal{V}^{\prime}\leftarrow\mathcal{V}\cup\\{T\stackrel{{\scriptstyle{?}}}{{{=}}}S\\}$

8 case  _$S=T$_ do $\mathtt{unify}(\mathcal{C}^{\prime},\mathcal{V}^{\prime})$
/* $T\stackrel{{\scriptstyle{?}}}{{{=}}}T$ */;

9

10 case  _ $T=X$ and
_$X\stackrel{{\scriptstyle{?}}}{{{=}}}S^{\prime}\in\mathcal{C}^{\prime}$_ /*
$X\stackrel{{\scriptstyle{?}}}{{{=}}}S$ and
$X\stackrel{{\scriptstyle{?}}}{{{=}}}S^{\prime}$ */ _ do

11 if  _$T\stackrel{{\scriptstyle{?}}}{{{=}}}S\not\in\mathcal{V}$_ then return
_$\mathtt{unify}(\mathcal{C}^{\prime}\cup\\{S\stackrel{{\scriptstyle{?}}}{{{=}}}S^{\prime}\\},\mathcal{V}^{\prime})$_
;

12 else return _$\mathtt{unify}(\mathcal{C}^{\prime},\mathcal{V}^{\prime})$_ ;

13

14

15 case  _ $T=T_{1}\;\mathtt{op}\;T_{2}$ and _ $S=S_{1}\;\mathtt{op}\;S_{2}$_
/*
$T_{1}\;\mathtt{op}\;T_{2}\stackrel{{\scriptstyle{?}}}{{{=}}}S_{1}\;\mathtt{op}\;S_{2}$
*/_ do

16 return
_$\mathtt{unify}(\mathcal{C}^{\prime}\cup\\{T_{1}\stackrel{{\scriptstyle{?}}}{{{=}}}S_{1},T_{2}\stackrel{{\scriptstyle{?}}}{{{=}}}S_{2}\\},\mathcal{V}^{\prime})$
_

17

18 case  _ $T=X$ and _ $S=\bullet^{E}X^{\prime}$_ and
_$X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{E}X^{\prime}\not\in\mathcal{V}$_
/* $X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{E}X^{\prime}$ */ _ do

19
$\mathcal{C}_{1}\leftarrow\mathcal{C}^{\prime}\cup\\{X\stackrel{{\scriptstyle{?}}}{{{=}}}X^{\prime},E\stackrel{{\scriptstyle{?}}}{{{=}}}0\\}$;
/* 1st option */

20
$\mathcal{C}_{2}\leftarrow\mathcal{C}^{\prime}\cup\\{X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{E}X^{\prime},0\
\stackrel{{\scriptstyle{?}}}{{{<}}}\ E\\}$ /* 2nd option */

21 return
_$\mathtt{unify}(\mathcal{C}_{1},\mathcal{V}^{\prime})\cup\mathtt{unify}(\mathcal{C}_{2},\mathcal{V}^{\prime})$
_

22

23 case  _$T=\bullet^{E}X$ and _ $S=\bullet^{E^{\prime}}X^{\prime}$_ /*
$\bullet^{E}X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{E^{\prime}}X^{\prime}$
*/_ do

24
$\mathcal{C}_{1}\leftarrow\mathcal{C}^{\prime}\cup\\{X\stackrel{{\scriptstyle{?}}}{{{=}}}\bullet^{E^{\prime}-E}X^{\prime},E^{\prime}\
\stackrel{{\scriptstyle{?}}}{{{\geq}\ }}E,E\
\stackrel{{\scriptstyle{?}}}{{{\geq}\ }}0\\}$; /* 1st option */

25