TWO LIGHT MODALITIES FOR RECURSION
PAULA SEVERI

arXiv:1801.00285v2 [cs.LO] 25 Feb 2018

Department of Computer Science, University of Leicester, UK

A BSTRACT. We investigate the interplay between two modalities for controlling the behaviour of recursive functional programs on infinite structures which are 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 modalities. 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 two silent modalities and guarded
recursive types. The first modality ‚ delays the data while the second one ‚ removes the delays. The
typing discipline guarantees normalisation and can be transformed into an algorithm which infers the
type of a program.

1. I NTRODUCTION
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, 8, 1, 9, 5].
Typability in these systems guarantees normalization and non-normalizing programs such as fix I
where I “ λ 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, 8, 9]. This has the advantage that type inference
is 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.
Our FOSSACS 2017 paper presents a typed lambda calculus with a temporal modal operator
‚ which has the advantage of having the modal operator silent in the syntax of pro‚ called λÑ
‚ does not need to make use of a subtyping relation as Nakano’s. In
grams [29]. The system λÑ
‚
this paper, we extend λÑ to include the modal operator ‚ which removes ‚ in a controlled way
and can type more programs [9, 2]. We show that the new extension called λ‚‚ enjoys normalisation and decidability of type inference. Even without a subtyping relation, the modal operators are
still challenging to deal with because they are intrinsically non-structural, not corresponding to any
expression form in the calculus.
Apart from the modal operators, we also include guarded recursive types which generalize
the recursive equation Str1t “ t ˆ ‚Str1t for streams [18, 30]. This allows us to type productive
functions on streams such as
skip xs “ xfst xs,skip psnd psnd xsqqy
Key words and phrases: Typed lambda calculus, infinite data, productivity, denotational semantics, type inference.

LOGICAL METHODS
IN COMPUTER SCIENCE

DOI:10.2168/LMCS-???

1

c Paula Severi
Creative Commons

2

PAULA SEVERI

which deletes the elements at even positions of a stream using the type Str1Nat Ñ Str2Nat where
Str2t “ t ˆ ‚ ‚ Str2t . The temporal modal operator ‚ allows to type many productive functions
which are rejected by the proof assistant Coq [10].
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 foldr defined by
foldr f xs “ f pfst xsq pfoldr f psnd xsqq
The type of foldr which is pt Ñ ‚s Ñ sq Ñ Str1t Ñ s, is telling us what is the safe way to build
functions. While it is possible to type
iterate f “ foldr pλ xy.x f x,yyq
by assigning the type t Ñ t to f , and assuming s “ Str1t , it is not possible to type the unproductive
function foldr pλ xy.yq. This is because λ xy.y does not have type pt Ñ ‚s Ñ sq. The modal operator
‚, also called the delay operator, indicates that the data on the recursive calls will only be available
later.
In spite of the fact that Str1Nat Ñ Str2Nat is the type of skip with the minimal number of
bullets, it does not give enough information to the programmer to know that the composition of
skip with itself is still typeable. The type inference algorithm of our FOSSACS 2017 paper can
infer a more general type for skip, which looks like
StreampN, Xq Ñ StreampN ` 1, Xq
ˆ ‚N StreampN, Xq

where StreampN, Xq “ 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 skip with itself.
A more flexible solution for typing skip and other functions on streams would be to use an
everything now operator ‚ inspired on the denotational semantics of the modal operator defined by
Clouston et al [9] (which was inspired on the clocks by Atkey et al [2]). This operator has the power
of eating ‚’s (it satisfies the property ‚ ‚ t “ ‚t) and it can only be used in type definitions of the
form t “ Fptq in a restrictive way: ‚ cannot occur before X in FpXq. This operator allows us to type
skip with StrNat Ñ StrNat where StrNat “ ‚Str1Nat .
More important, the new modal operator allows us to type more programs. When we combine
‚ . For example,
inductive with co-inductive data types, some functions become untypable in λÑ
consider the set of natural numbers and the function get that selects the n-th element of a stream
defined by 1:
get 0 xs “ fst xs
(1.1)
get psucc nq xs “ get n psnd xsq
‚ . The reason why it is not typable in
The function get is typable in λ‚‚ but it is not typable in λÑ
‚ is that the result needs a different number of bullets depending on the natural number n.
λÑ
1It is defined using natrec (see Section 2.4).

TWO LIGHT MODALITIES FOR RECURSION

3

1.1. Outline. Section 2 defines the typed lambda calculus λ‚‚ with the silent modal operators 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 K for ‚8 -free and tail finite
‚ with the type systems of [23] and [18]. Section 5 gives
types respectively. Section 4 compares λÑ
an adequate denotational semantics for λ‚‚ in the topos of trees as a way of linking our system
to the work by Birkedal et al [4]. Section 6 shows decidability of the type inference problem
for λ‚‚ . 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. Contributions. This paper extends our FOSSACS 2017 paper in several ways [29]:
‚ to include the new modal operator ‚.
(1) We extend the types and the typing rules of λÑ
(2) We prove that the typed lambda calculus of Krishnaswami and Benton [18] is included in
‚ and that λ ‚ is included in the one of Nakano [23].
λÑ
Ñ
(3) We prove normalisation for λ‚‚ which is not so obvious since ‚ could easily destroy this
property due to its ravenous behaviour.
(4) We give conditions on the types that guarantee that the Lèvy-Longo and Böhm trees of a
typable expression have no K.
(5) Besides extending the denotational semantics to include ‚ and proving soundness, we also
prove that it is adequate with respect to an observational equivalence.
(6) We extend the type inference algorithm of [29] to include ‚.
(7) We obtain automatic ways of guaranteeing that the program satisfies the properties of normalization, having Lèvy-Longo and Böhm tree without K.
2. T HE T YPED L AMBDA C ALCULUS WITH T WO M ODALITIES
This section defines the type discipline for λ‚‚ . Following [23], we introduce the delay type constructor ‚, so that an expression of type ‚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. Following [2, 9], we introduce the now type constructor ‚. The now operator ‚ interacts with
‚ in a non-trivial way by means of a type conversion which brings the data from the future to the
present moment.
2.1. Syntax. The syntax for expressions and types is given by the following grammars.
e ::“ind
|
|
|

x
k
λ x.e
ee

Expression
(variable)
(constant)
(abstraction)
(application)

t ::“coind
|
|
|
|
|

X
Nat
t ˆt
t Ñt
‚t
‚t

Pseudo-type
(type variable)
(natural type)
(product)
(arrow)
(delay)
(now)

In addition to the usual constructs of the λ -calculus, expressions include constants, ranged
over by k. Constants are the constructor for pairs pair, the projections fst and snd and 0 and
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 λ -calculus.
In particular, we assume that the bodies of abstractions extend as much as possible to the right,

4

PAULA SEVERI

that applications associate to the left, and we use parentheses to disambiguate the notation when
necessary. We write xe1 ,e2 y in place of pair e1 e2 .
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 Ñ, ˆ, ‚ or ‚ 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 Nat. 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 two modalities: the delay type constructor ‚ [23] and the now type
constructor ‚ [9]. An expression of type ‚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. An expression of type ‚t denotes a value of type t that “returns from the future to the present moment”. The
use of the operator ‚ will be restricted by the syntax of types and the typing rules (see Definition
2.1 and Section 2.3). Once the recursive type is constructed, it is safe to make all the data available
right now.
For simplicity, we only include Nat and type variables as basic types. One could easily add
other basic types such as Bool and Unit together with constants for their values.
Definition 2.1 (Types). We say that a pseudo-type t is
(1) regular if its tree representation has finitely many distinct sub-trees;
(2) guarded if every infinite path in its tree representation has infinitely many ‚’s;
(3) local if every infinite path in its tree representation has finitely many ‚’s;
(4) a type if it is regular, guarded and local.
The regularity condition implies that we only consider types admitting a finite representation.
It is equivalent to representing types with µ-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 [12] [25, Section 20.2]. The existence and uniqueness
of a solution for a pseudo-type satisfying condition 1 follow from known results (see [11] and
also Theorem 7.5.34 of [7]). For example, there are unique pseudo-types Str1Nat , Str1Nat , and
‚8 that respectively satisfy the equations Str1Nat “ Nat ˆ Str1Nat , Str1Nat “ Nat ˆ ‚Str1Nat , and
‚8 “ ‚‚8 .
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 ‚ are necessarily “delayed” in the sense that
recursive calls on them must be deeper. For example, Str1Nat is a type that denotes streams of
natural numbers, where each subsequent element of the stream is delayed by one ‚ compared to its
predecessor. Instead Str1Nat 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 µ-notation, the guardedness
condition means that all occurrences of X in the body t of µX.t are in the scope of a ‚.
The type ‚8 is somehow degenerated in that it contains no actual data constructors. Unsurprisingly, we will see that non-normalising terms such as Ω “ pλ x.x xqpλ x.x xq can only be typed
with ‚8 and ‚n ‚ ‚8 (see Theorem 3.14). Without condition 2, Ω could be given any type since the
recursive pseudo-type D “ D Ñ t would become a type.
The locality condition allows to remove the delays when a recursive type has been fully constructed. If the types are written in µ-notation, the locality condition means that no occurrence of
X in the body t of µX.t can be in the scope of a ‚. This condition allows to have types such as
Strt “ ‚Str1t and StrStrt and it forbids types such as t “ ‚ ‚ t or t “ ‚pNat ˆ ‚tq.
We adopt the usual conventions regarding arrow types (which associate to the right) and assume the following precedence among type constructors: Ñ, ˆ, ‚, ‚ with ‚ and ‚ having the

TWO LIGHT MODALITIES FOR RECURSION

5

highest precedence. Sometimes we will write ‚nt in place of ‚l ¨jh
¨¨n
‚ t.
n-times

We define the weak conversion –w between types as the smallest equivalence relation that
contains the following rules:
‚Nat –w Nat

‚ ‚ t –w ‚t

‚ ‚t –w ‚t

t –w t 1
‚t –w ‚t 1

The second axiom states that ‚ can eat any finite number of ‚’s and the third one that ‚ is
idempotent. For example, ‚ ‚ ‚Str1Nat –w ‚Str1Nat and ‚‚8 –w ‚‚8 .
The conversion – extends –w to infinite types and it is defined by coinduction, as the biggest
equivalence relation such that for all types t and s if t – s then either one of the following holds:
(1) t –w Nat and s –w Nat
(2) t –w t1 Ñ t2 and s –w s1 Ñ s2 and t1 – s1 and t2 – s2
(3) t –w t1 ˆ t2 and s –w s1 ˆ s2 and t1 – s1 and t2 – s2
(4) t –w ‚nt 1 and s –w ‚n s1 and t 1 – s1 .
(5) t –w ‚t 1 and s –w ‚s1 and t 1 – s1 .
For example, Str1‚‚Nat – Str1Nat but Str1‚‚Nat ­–w Str1Nat .
The conversion between types is one of the novelties for defining ‚. Neither the modal operator
‚ by Clouston et al nor the clocks by Atkey et al have the syntactic properties stated by the axioms
of – [9, 2].
2.2. Operational Semantics. Expressions reduce according to a standard call-by-name semantics:
[ R - CTXT ]
[ R - BETA ]

[ R - FIRST ]

[ R - SECOND ]

pλ x.e1 q e2 ÝÑ e1 re2 {xs fst xe1 ,e2 y ÝÑ e1

snd xe1 ,e2 y ÝÑ e2

e ÝÑ f
Eres ÝÑ Er f s

where the evaluation contexts are E ::“ r s | pE eq | pfst Eq | psnd Eq | psucc Eq. Normal forms
are defined as usual as expressions that do not reduce. The reflexive and transitive closure of ÝÑ is
denoted by ÝÑ˚ .
‚ with the rules [‚I], [–] and [‚Ñ E] [29]. The type
2.3. Type System. We define λ‚‚ which extends λÑ
conversion – is extended to typing contexts in the obvious way.
First we assume a set κ containg the types for the constants:

pair : t Ñ s Ñ t ˆ s
fst : t ˆ s Ñ t
snd : t ˆ s Ñ s

0
: Nat
succ : Nat Ñ Nat

The type assignment system λ‚‚ is defined by the following rules.
[ AXIOM ]

[ CONST ]

[‚I]

[‚I]

[–]

x:t PΓ
Γ $x:t

k:t Pκ
Γ $k:t

Γ1 , Γ2 $ e : t
Γ1 , ‚Γ2 $ e : ‚t

Γ2 $ e : t
Γ1 , ‚Γ2 $ e : ‚t

Γ $ e : t t – t1 Γ – Γ 1
Γ 1 $ e : t1

[ÑI]

[ÑE]

[‚Ñ E]

Γ , x : ‚nt $ e : ‚n s
Γ $ λ x.e : ‚n pt Ñ sq

Γ $ e1 : ‚n pt Ñ sq Γ $ e2 : ‚nt
Γ $ e1 e2 : ‚n s

Γ $ e1 : ‚n ‚ pt Ñ sq Γ $ e2 : ‚n ‚ t
Γ $ e1 e2 : ‚n ‚ s

6

PAULA SEVERI

The rules [‚I] and [‚I] introduce the modalities and [–] allows for type conversion. These rules
are unusual in the sense that the expression remains the same. We do not have a constructor for
either ‚ or ‚ at the level of expressions.
The rule [‚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 ě n, but not earlier. Using rule [‚I] and the recursive type D “ ‚D Ñ t, we can derive that the fixed point combinator
fix “ λ y.pλ x.y px xqqpλ x.y px xqq has type p‚t Ñ tq Ñ t by assigning the type D Ñ t to the first
occurrence of λ x.y px xq and ‚D Ñ t to the second one [23].
The rules[ÑI], [ÑE] and [‚Ñ E] allow for an arbitrary delay in front of the types of the entities
involved. Intuitively, the number of ‚’s represents the delay at which a value becomes available. So
for example, rule [Ñ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 ‚n pt Ñ sq, that is a function delayed by n
that maps elements of t into elements of s.
It is possible to anticipate a delayed value only in a very restricted way through the rules [‚I]
and [‚Ñ E]. The rule [‚I] anticipates the type of an expression if the type of all its free variables are
anticipated as well. It is crucial not to include the following rule:
[‚ ÑI]

Γ , x : ‚n ‚ t $ e : ‚n ‚ s
7
Γ $ λ x.e : ‚n ‚ pt Ñ sq
If we had included the rule [‚ ÑI], it would have been possible to type fix I which is not normalising.
With respect to the two semantics, the rule [‚I] is sound while the rule [‚ ÑI] above is not. The first
semantics, given in Section 3.2, interprets ‚ as intersection and the second one, given in Section 5,
interprets ‚ as homS p1, _q.
The following lemma is very easy to prove.
Lemma 2.2. The following typing rules are admissible:
[fix]

[fix1 ]

$ e : ‚t Ñ t
$ fix e : ‚t

$ e : ‚pt1 Ñ t2 q Ñ t1 Ñ t2
$ λ x.fix e x : ‚t1 Ñ ‚t2

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 Nat by means of a function natrec : t Ñ pNat Ñ t Ñ tq Ñ
Nat Ñ t with the reduction rule:
natrec f1 f2 0 ÝÑ f1

natrec f1 f2 psucc eq ÝÑ f2 e pnatrec f1 f2 eq

We can also introduce a type Listt for the set of finite lists as an inductive data type with
nil : Listt and consl : t Ñ Listt Ñ Listt and lrec : s Ñ pt Ñ Listt Ñ s Ñ sq Ñ Listt Ñ s
with the reduction rule:
lrec f1 f2 nil ÝÑ f1

lrec f1 f2 pconsl e1 e2 q ÝÑ f2 e1 e2 plrec f1 f2 e2 q

TWO LIGHT MODALITIES FOR RECURSION

7

2.5. Disjoint union. We could add the disjoint union t1 `t2 of two types t1 and t2 and add constants:
inl : t1 Ñ t1 ` t2
inr : t2 Ñ t1 ` t2
case : pt1 ` t2 q Ñ pt1 Ñ sq Ñ pt2 Ñ sq Ñ s
the reduction rules:
case pinl eq f1 f2 ÝÑ f1 e case pinr eq f1 f2 ÝÑ f2 e
and the evaluation contexts are extended with E ::“ ... | case E f1 f2 .
Using the disjoint union, we can define the type of finite and infinite lists as:
coListt “ Unit ` ‚t ˆ coListt
and we can also define the type of conatural numbers as shown in Section 2.6.
2.6. Type of conatural numbers. The type of conatural numbers can be defined as coNat “
Unit ` ‚coNat. Then z “ inl unit has type coNat and s “ inr has type ‚coNat Ñ coNat.
The set of conatural numbers include s8 “ fix s. The usual definition of addition given by the
equations:
n ` 0 “ n n ` pm ` 1q “ pn ` mq ` 1
can be written as
add x y “ case y pλ y1 .xq pλ y1 .s padd x y1 qq
‚
and it can be typed in λÑ . However, the usual definition of substraction given by the equations
n´0 “ n 0´n “ 0

pn ` 1q ´ pm ` 1q “ n ´ m

which is expressed as:
minus x y “ case x pλ x1 .zq pλ x1 .case y pλ y1 .zqpλ y1 .minus x1 y1 qq
is not typable because pminus s8 s8 q is not normalizing.
‚ . We show examples of typable programs that do
2.7. Examples of Typable Expressions in λÑ
‚ .
not involve ‚ for their typing, i.e. they are typable in λÑ
We consider the function skip of the introduction that deletes the elements at even positions
of a stream.
skip “ fix λ f x.xpfst xq, f psnd psnd xqqy
(2.1)
In order to assign the type Str1Nat Ñ Str2Nat to skip, the variable f has to be delayed once
and the first occurrence of snd has to be delayed twice. Note also that when typing the application
f psnd psnd xqq the rule [ÑE] is used with n “ 2.

8

PAULA SEVERI

Other examples of typable functions are:
interleave x y “ xfst x,pinterleave y psnd xqy
map f x “ x f pfst xq,pmap f psnd xqy
nats “ x0,map succ natsy
maap f x “ x f pfst xq,x f pfst psnd xqq,pmaap f psnd psnd xqqyy
sum x y “ xpfst xq ` pfst yq,sum psnd xq psnd yqy
merge x y “ if pfst xq ď pfst yq then xfst x,merge psnd xq yy else xfst y,merge x psnd yqy
ones “ x1,interleave ones onesy
fib “ x0,sum fib x1,fibyy
fib1 “ x0,x1,sum fib1 psnd fib1 qyy
naats “ x0,maap succ natsy
ham “ x1,merge pmap λ x.2 ˚ x hamq pmerge pmap λ x.3 ˚ x hamqpmap λ x.5 ˚ x hamqqqy
The last six examples 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) [13]. The
function fib1 cannot be typed with sized types [28].
‚ other programs shown typable in other papers on modal operators
It is possible to type in λÑ
such as toggle, paperfolds [5].
‚ . The function get already introduced in Eq. (1.1) can be defined
2.8. Untypable programs in λÑ
using natrec (see Section 2.4) as follows:

get “ natrec fst λ xyz.y psnd zq

(2.2)

The first argument of natrec has type Str1t Ñ t while the second argument has type Nat Ñ
‚ unless t “ ‚t.
pStr1t Ñ tq Ñ Str1t Ñ ‚t. It is not difficult to see that get is not typable in λÑ
Note that if we re-define get on the set of conatural numbers and use fix instead of natrec then
we obtain a function get1 defined by:
get1 “ fixpλ g.λ xy.case x pλ x1 .fst yq pλ x1 .g x1 psnd yqqq
‚ nor λ ‚ .
which is typable in neither λÑ
‚
We now consider the function take that takes the first n elements of a stream and returns a
finite list in Listt defined by:

take 0 x
“ nil
take psucc nq x “ consl pfst xq ptake n psnd xqq
It is expressed using natrec as follows:
take “ natrec λ x.nil λ xyz.pconsl pfst zq py psnd zqqq

(2.3)

The first argument of natrec has type Str1t Ñ Listt and the second argument has type Nat Ñ
‚ .
pStr1t Ñ Listt q Ñ Str1t Ñ ‚Listt . It is not difficult to see that take is not typable in λÑ
Below we will see that we can type get and take using ‚.

TWO LIGHT MODALITIES FOR RECURSION

9

2.9. Examples of Typable Expressions using ‚. Recall that Strt “ ‚Str1t . We can define cons,
head and tail by η-expanding pair, fst and snd and assign them the following types where
some ‚’s have disappeared:
cons “ λ xy.pair x y : Nat Ñ StrNat Ñ StrNat
head “ λ x.fst x
: StrNat Ñ Nat
tail “ λ x.snd x
: StrNat Ñ StrNat
We can now type the function get of Eq. (2.2) by re-writing it using head and tail as follows:
get “ natrec head λ xyz.y ptail zq
Then, get has now type Nat Ñ StrNat Ñ Nat in λ‚‚ .
Similarly, we can re-write the function take of Eq. (2.3) using head and tail as follows:
take “ natrec λ x.nil λ xyz.pconsl phead zq py ptail zqqq

(2.4)

Then, take has type Nat Ñ Strt Ñ Listt in λ‚‚ . Note that if we define take1 as a function whose
range is coListt instead of Listt then
take1 “ natrec λ x.pinl unitq λ xyz.pinrpxfst z,y psnd zqyq
‚ without any need of ‚.
has type Nat Ñ Str1t Ñ coListt in λÑ
We can also re-define skip of Eq. (2.1) as λ x.fix e x where e “ λ f .λ x.xpfst xq, f psnd psnd xqqy.
Then e has type ‚pStrNat Ñ Str1Nat q Ñ pStrNat Ñ Str1Nat q and skip has now type StrNat Ñ
StrNat .

3. P ROPERTIES OF T YPABLE E XPRESSIONS
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 ‚ controls recursion and guarantees normalisation of any expression
that has a type different from ‚8 and ‚n ‚ ‚8 . This section also proves that any typable expression
has a Lèvy-Longo and Böhm tree without K if the type is ‚8 -free and tail finite respectively.
3.1. Inversion and Subject Reduction.
Lemma 3.1 (Weakening). If Γ $ e : t and Γ Ď Γ 1 then Γ 1 $ e : t.
Proof. By an easy induction on the derivation.
Lemma 3.2 (Inversion).
(1) If Γ $ k : t then either t – ‚nt 1 and k : t 1 P κ or t – ‚n ‚ t 1 and k : t 1 P κ.
(2) If Γ $ x : t then t – ‚nt 1 and x : t 1 P Γ .
(3) If Γ $ λ x.e : t then there are two possibilities:
i) t – ‚n pt1 Ñ t2 q and Γ , x : ‚nt1 $ e : ‚nt2
ii) t – ‚n ‚ pt1 Ñ t2 q and Γ21 , x : ‚mt1 $ e : ‚mt2 and Γ “ Γ1 , Γ2 and Γ21 “ tx1 : s1 , . . . , xk : sk u
and Γ2 – tx1 : ‚n1 ‚ s1 , . . . , xk : ‚nk ‚ sk u and maxpn1 , . . . , nk q ď n.
(4) If Γ $ e1 e2 : t then there are two possibilites:
i) t – ‚nt2 and Γ $ e2 : ‚nt1 and Γ $ e1 : ‚n pt1 Ñ t2 q
ii) t – ‚n ‚ t2 and Γ $ e2 : ‚n ‚ t1 and Γ $ e1 : ‚n ‚ pt1 Ñ t2 q.

10

PAULA SEVERI

Proof. By case analysis and induction on the derivation. We only show Item 3. A derivation of
Γ $ λ x.e : t ends with an application of either [ÑI] or [–] or [‚I] or [‚I]. The proofs for the first two
cases are immediate. If the last applied rule is [‚I] then t “ ‚t 1 and Γ1 , Γ2 $ λ x.e : t 1 and Γ “ Γ1 , ‚Γ2 .
By induction we have two possibilities:
(i) t 1 – ‚n pt1 Ñ t2 q and Γ1 , Γ2 , x : ‚nt1 $ e : ‚nt2 . Hence t “ ‚t 1 – ‚n`1 pt1 Ñ t2 q and Γ1 , ‚Γ2 , x :
‚n`1t1 $ e : ‚n`1t2 by applying the rule [‚I].
(ii) t 1 – ‚n ‚ pt1 Ñ t2 q and Γ41 , x : ‚mt1 $ e : ‚mt2 and Γ “ Γ3 , Γ4 and Γ41 “ tx1 : s1 , . . . , xk : sk u and
Γ4 – tx1 : ‚n1 ‚ s1 , . . . , xk : ‚nk ‚ sk u and maxpn1 , . . . , nk q ď n. Then, t – ‚n`1 ‚ pt1 Ñ t2 q and
1
1
Γ “ Γ3 , Γ5 where Γ5 “ tx1 : ‚n1 ‚ s1 , . . . , xk : ‚nk ‚ sk u and maxpn11 , . . . , n1k q ď n ` 1.
If the last applied rule is [‚I] then t “ ‚t 1 and Γ2 $ e : t 1 and Γ “ Γ1 , ‚Γ2 . By induction we have two
possibilities:
(i) t 1 – ‚n pt1 Ñ t2 q and Γ2 , x : ‚nt1 $ e : ‚nt2 . Since Γ “ Γ1 , ‚Γ2 , this is Item 3ii.
(ii) t 1 – ‚n ‚ pt1 Ñ t2 q and Γ41 , x : ‚mt1 $ e : ‚mt2 and Γ2 “ Γ3 , Γ4 and Γ41 “ tx1 : s1 , . . . , xk : sk u and
Γ4 – tx1 : ‚n1 ‚ s1 , . . . , xk : ‚nk ‚ sk u and maxpn1 , . . . , nk q ď n. It follows from Lemma 3.1 that
Γ3 , Γ41 , x : ‚mt1 $ e : ‚mt2 . It is easy to see that ‚Γ2 “ ‚Γ3 , ‚Γ4 and ‚Γ4 – tx1 : ‚s1 , . . . , xk : ‚sk u.
Lemma 3.3 (Substitution). If Γ , x : s $ e : t and Γ $ f : s then Γ $ er f {xs : t.
Proof. By an easy induction on the structure of expressions.
Lemma 3.4 (Subject Reduction). If Γ $ e : t and e ÝÑ e1 then Γ $ e1 : t.
Proof. By induction on the definition of ÝÑ. We only do the case pλ x.e1 q e2 ÝÑ e1 re2 {xs. Suppose
Γ $ pλ x.e1 q e2 : t. By Item 4 of Lemma 3.2 we have two cases. The first case is:
t – ‚ n t2
Γ $ e2 : ‚nt1
Γ $ pλ x.e1 q : ‚n pt1 Ñ t2 q
It follows from Item 3i of Lemma 3.2 that Γ , x : ‚nt1 $ e1 : ‚nt2 . By applying Substitution Lemma,
we deduce that Γ $ e1 re2 {xs : ‚nt2 .
The second case is:
t – ‚ n ‚ t2

Γ $ e2 : ‚n ‚ t1

Γ $ pλ x.e1 q : ‚n ‚ pt1 Ñ t2 q

It follows from Item 3ii of Lemma 3.2 that
Γ21 , x : ‚mt1 $ e1 : ‚mt2

(3.1)

and Γ “ Γ1 , Γ2 and Γ21 “ tx1 : s1 , . . . , xk : sk u and Γ2 – tx1 : ‚n1 ‚s1 , . . . , xk : ‚nk ‚sk u and maxpn1 , . . . , nk q ď
n. By applying rules [‚I], [‚I] and [–] to Eq. (3.1), we get that Γ , x : ‚n ‚t1 $ e1 : ‚n ‚t2 . By Substitution
Lemma, Γ $ e1 re2 {xs : ‚n ‚ t2 .
Neither Nakano’s type system nor ours is closed under η-reduction. For example, y : ‚pt Ñ
sq $ λ x.py xq : pt Ñ ‚sq but y : ‚pt Ñ sq 0 y : pt Ñ ‚sq. The lack of subject reduction for η-reduction
is natural in the context of lazy evaluation where programs are closed terms and only weak head
normalised.

TWO LIGHT MODALITIES FOR RECURSION

11

3.2. Normalization. We prove that any expression which has a type t such that t ­“ ‚8 and t ­–
‚n ‚ ‚8 reduces to a normal form (Theorem 3.14). For this, we define a type interpretation indexed
on the set of natural numbers for dealing with the temporal operator ‚. The time is discrete and
represented using the set of natural numbers. The semantics reflects the fact that one ‚ corresponds
to one unit of time by shifting the interpretation from i to i ` 1 and that ‚ is resilient to time as the
intersection of all interpretations at times greater than i.
Before introducing the type interpretation, we give a few definitions. Let E be the set of expressions. We define the following subsets of E:
WN “ te | e ÝÑ˚ f & f is a normal formu
WNx “ te | e ÝÑ˚ Erxs & x is a variableu
We will do induction on the rank of types. For Nat 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 ‚ from the root to a
leaf or ‚ or ‚.
Definition 3.5 (Rank of a Type). The rank of a type t (notation rankptq) is defined as follows.
rankpNatq “ rankpXq “ rankp‚tq “ rankp‚tq “ 0
rankpt ˆ sq “ maxprankptq, rankpsqq ` 1
rankpt Ñ sq “ maxprankptq, rankpsqq ` 1
The rank is well defined (and finite) because the tree representation of a type cannot have an
infinite branch with no ‚’s at all (Condition 2 in Definition 2.1) and rankp‚tq is set to 0.
Definition 3.6. We define nboxptq as follows.
nboxptq “ 0 if t has no ‚
nboxpt ˆ sq “ maxpnboxptq, nboxpsqq
nboxpt Ñ sq “ maxpnboxptq, nboxpsqq
nboxp‚tq “ nboxptq ` 1
Note that nbox is well defined because a type cannot have a branch with an infinite number of
‚’s. We now define the type interpretation prtsq P N Ñ PpEq, which is an indexed set, where N is
the set of natural numbers and P is the powerset constructor.
Definition 3.7 (Type Interpretation). We define prtsqi Ď E by induction on pnboxptq, i, rankptqq.
prNatsqi
prXsqi
prt ˆ ssqi
prt Ñ ssqi
pr‚tsq0
pr‚tsqi`1
pr‚tsqi

WNx Y te | e ÝÑ˚ nu
WNx
WNx Y te | e ÝÑ˚ xe1 ,e2 y and e1 P prtsqi and e2 P prssqi u
WNx Y te | e ÝÑ˚ λ x. f and ee1 P prssq j @e1 P prtsq j , j ď iu
Y te | e ÝÑ˚ Erks and ee1 P prssq j @e1 P prtsq j , j ď iu
“ E
“ prtsqi
Ş
“
jěi prtsq j

“
“
“
“

Note that pr‚8 sqi “ pr‚n ‚ ‚8 sqi “ E for all i P N. In the interpretation of the arrow type, the requirement “for all j ď 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.

12

PAULA SEVERI

Lemma 3.8.
(1) pr‚ntsqi “ E if i ă n.
(2) pr‚ntsqi “ prtsqi´n if i ě n.
Proof. Both items are proved by induction on n.
Lemma 3.9. For all types t and i P N,
(1) WNx Ď prtsqi .
(2) prtsqi`1 Ď prtsqi .
Proof. (Item 1) follows by induction on pnboxptq, iq and doing case analysis on the shape of the type.
(Item 2) follows by induction on pnboxptq, i, rankptqq. Suppose e P prt Ñ ssqi`1 . Then, ee1 P prssq j
for j ď i ` 1. This is equivalent to saying that ee1 P prssq j1 `1 for j1 ď i. By induction hypothesis,
prssq j1 `1 Ď prssq j1 . Hence, e P prt Ñ ssqi .
Lemma 3.10. For all i P N, if t – t 1 then prtsqi “ prt 1 sqi .
Proof. The equality pr‚Natsqi “ prNatsqi follows from the definition of type interpretation. The
equalities pr‚ ‚ tsqi “ pr‚tsqi and pr‚ ‚ tsqi “ pr‚tsqi follow using Item 2 of Lemma 3.9 and the definition
of type interpretation.
Ş
Lemma 3.11. If t ­“ ‚8 and t ­– ‚n ‚ ‚8 then iPN prtsqi Ď WN.
Proof. Suppose t “ ‚nt0 and t0 is either Nat, X, t1 Ñ t2 or t1 ˆ t2 . Then, for all i ě n,
pr‚nt0 sqi “ prt0 sqi´n Ď WN
by Lemma 3.8 and the definition of type interpretation.
Suppose t – ‚n ‚ t0 and t0 is either Nat, X, t1 Ñ t2 or t1 ˆ t2 . Then, for all i ě n,
č
prtsqi “ pr‚n ‚ t0 sqi “
prt0 sq j Ď WN
jěi´n

by Lemmas 3.8 and 3.10 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 E. We use ρ to range over substitution
functions. Substitution functions allows us to extend the semantics to typing judgements (notation
Γ |ùi e : t).
Definition 3.12 (Typing Judgement Interpretation). Let ρ be a substitution function.
(1) ρ |ùi Γ if ρpxq P prtsqi for all x : t P Γ .
(2) Γ |ùi e : t if ρpeq P prtsqi for all ρ |ùi Γ .
As expected we can show the soundness of our type system with respect to the indexed semantics.
Theorem 3.13 (Soundness). If Γ $ e : t then Γ |ùi e : t for all i P N.
The proof of the above theorem can be found in Appendix A.
Theorem 3.14 (Normalisation of Typable Expressions). If Γ $ e : t and t ­“ ‚8 and t ­– ‚n ‚ ‚8 then
e reduces (in zero or more steps) to a (weak head) normal form.

TWO LIGHT MODALITIES FOR RECURSION

13

Proof. It follows from Theorem 3.13 that
Γ |ùi e : t

(3.2)

for all i P N. Let id be the identity substitution and suppose x : s P Γ . Then
idpxq “ x P WNx
Ď prssqi by Item 1 of Lemma 3.9.
This means that id |ùi Γ for all i P N. From Eq. (3.2) we have that idpeq “ e P prtsqi for all i. Hence,
č
e P prtsqi
iPN

It follows from Lemma 3.11 that e P WN.
Notice that there are normalising expressions that cannot be typed, for example λ x.ΩI, where
Ω “ pλ y.y yqpλ y.y yq and I “ λ z.z. In fact Ω has type ‚8 and ‚n ‚ ‚8 . By Theorem 3.14, it cannot
have other types, and this implies that the application ΩI has no type.
The function filter that selects the elements of a list xs that satisfy p defined as
filter p xs “ if p pfst xsq then xpfst xsq,pfilter xsqy else pfilter xsq
‚ nor in λ ‚ . Suppose
is normalizing (actually it is in normal form) and it can be typed neither in λÑ
‚
towards a contradiction that filter is typable. Then, pfilter ones pλ x.eq? x 0qq is also typable.
But pfilter ones pλ x.eq? x 0qq is not normalizing contradicting Theorem 3.14.

3.3. Lévy-Longo and Böhm Trees. Lévy-Longo and Böhm Trees without K are obtained as (possible infinite) normal forms of (possible infinite) reduction sequences when we allow to reduce
inside the body of an abstraction and inside the components of a pair [3, 21, 22]. Infinitary normalization formalizes the idea of productivity, i.e. an infinite reduction sequence which always produce
part of the result [16, 17, 30, 20].
We say that t is ‚8 -free if it does not contain ‚8 . For example, Str1Nat and ENat are ‚8 -free
where Et “ t Ñ ‚Et . But Str1‚8 and Nat Ñ ‚8 and ‚‚8 are not ‚8 -free.
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 LLTpeq is defined coinductively as follows.
$
x LLTpe1 q . . . LLTpen q if e ÝÑ˚ x e1 . . . en
’
’
&
k LLTpe1 q . . . LLTpen q if e ÝÑ˚ k e1 . . . en
LLTpeq “
λ x.LLTpe1 q
if e ÝÑ˚ λ x.e1
’
’
%
K
otherwise, i.e. e has no (weak head) normal form
Let e “ fix pλ xy.xq. Then e has type ENat which is ‚8 -free and LLTpeq “ λ x.λ x. . . . has no K.
Theorem 3.16 (Productivity I: Lèvy-Longo Trees without K). Let t and all types in Γ be ‚8 -free.
If Γ $ e : t then the Lèvy-Longo tree of e has no K’s.
Proof. We construct the Lèvy-Longo tree depth by depth. By Theorem 3.14, e reduces to a (weak
head) normal form e0 which is typable by Lemma 3.4. Suppose e0 is λ x.e1 (the cases when e0 “
x e1 . . . en or e0 “ k e1 . . . en are similar). The Lèvy-Longo tree of e contains λ x at depth 0. It only
remains to show that we can construct the Lèvy-Longo tree of e1 which will be at depth n ą 0. It
follows from Inversion Lemma that Γ, x : t1 $ e1 : t2 and both t1 and t2 are ‚8 -free. Hence, we can
repeat the process to obtain the Lèvy-Longo tree of e1 .

14

PAULA SEVERI

An infinite alternation of ‚’s and Ñ’s is a type of the form: t “ ‚n1 pt1 Ñ ‚n2 pt2 Ñ . . .qq. We
say that t is tail finite if it is ‚8 -free and it does not contain an infinite alternation of ‚’s and Ñ’s.
For example, G “ Nat Ñ ‚pNat ˆ Gq is tail finite but F “ Nat Ñ ‚F is not.
The head normal form of e is defined as follows:
$
λ x1 . . . xk .x f1 . . . fn if e “ e0 and ek ÝÑ˚ x f1 . . . fn
’
’
’
’
and ei ÝÑ˚ λ xi`1 .ei`1 for 0 ď i ď k ´ 1
&
λ x1 . . . xk .k f1 . . . fn if e “ e0 and ek ÝÑ˚ k f1 . . . fn
hnf peq “
’
’
and ei ÝÑ˚ λ xi`1 .ei`1 for 0 ď i ď k ´ 1
’
’
%
K
otherwise
Definition 3.17 (Böhm Tree). Let e be an expression (it may be untypable). The Böhm tree of e,
denoted as BTpeq is defined coinductively as follows.
$
& λ x1 . . . xk .x BTp f1 q . . . BTp fn q if hnf peq “ λ x1 . . . xk .x f1 . . . fn
λ x1 . . . xk .k BTp f1 q . . . BTp fn q if hnf peq “ λ x1 . . . xk .k f1 . . . fn
BTpeq “
%
K
otherwise
For example, fib has type Str1Nat which is tail finite and BTpfibq “ x0,x1,x1,x2, . . .yyyy
has no K’s.
Theorem 3.18 (Productivity II: Böhm Trees without K). Let all the types in Γ and t be tail finite. If
Γ $ e : t then the Böhm tree of e has no K’s.
Proof. By Theorem 3.16, the Lévy-Longo tree of e has no K’s. Suppose the Lévy-Longo tree of
e contains a subtree of the form λ x1 λ x2 λ x3 . . . .. It is not difficult to prove using Lemma 3.2 and
Lemma 3.4 that the type should contain an infinite alternation of ‚’s and Ñ’s.
4. F ORMAL C OMPARISION WITH OTHER T YPE S YSTEMS
‚ and the typed lambda calculi of Krishnaswami
This section stablishes a formal relation between λÑ
and Benton [18] and Nakano [23].
‚ . The typing rules of
4.1. Embedding the Type System by Krishnaswami and Benton into λÑ
λ KB defined by Krishnaswami and Benton [18] are:
[ AXIOM ]

[ CONST ]

[‚I]

[‚E]

Γ , x :i t $ x : j t

k:t Pκ
Γ $ k :i t

Γ $ e :i`1 t
Γ $ ‚e :i ‚t

Γ $ e :i ‚t
Γ $ await e :i`1 t

jěi

[ÑI]

[ÑE]

Γ , x :i t $ e :i s
Γ $ λ x.e :i pt Ñ sq

Γ $ e1 :i pt Ñ sq
Γ $ e 2 :i t
Γ $ e1 e2 :i s

λ KB has only the recursive types Str1t “ t ˆ ‚Str1t for infinite lists with only one ‚. Since
fix cannot be expressed in λ KB , we need to add it to the set κ of constants:
fix : p‚t Ñ tq Ñ t
The mapping itob replaces the subindex i by ‚i in typing contexts.
itobpHq
“H
itobpΓ , x :i tq “ itobpΓ q, x : ‚it

TWO LIGHT MODALITIES FOR RECURSION

15

The function clear removes the constructor and destructor of ‚ from e, i.e. clearp‚e1 q “ e1 and
clearpawait e1 q “ e1 .
‚ ). If Γ $ e : t in λ KB then itobpΓ q $ clearpeq : ‚it in λ ‚ .
Lemma 4.1 (Embedding λ KB into λÑ
i
Ñ

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 skip (see Eq. (2.1)), ones1 and pairup are not typable in λ KB where
ones1 “ x1,interleave ones1 psnd ones1 qy
pairup xs “ xxpfst xsq,pfst psnd xsqqy,psnd psnd xsqqy
‚ because λ ‚ has more flexibility in
The functions skip, ones1 and pairup are all typeable in λÑ
Ñ
the location and number of ‚’s which can be inserted in the types. We can derive that ones1 has
‚ by assigning the type Str1 Ñ ‚Str1 Ñ Str1 to interleave and pairup
type Str1X in λÑ
X
X
X
has type StrHalfX Ñ Str1X where StrHalfX “ X ˆ X ˆ ‚StrHalfX .
‚ into the Type System by Nakano. We consider the type system by Nakano
4.2. Embedding λÑ
of [23] without J and call it λNak .
Types in λNak are finite, written in µ-notation and denoted by T , S. Types in λNak are guarded
which means that the type variable X of µX.T can occur free in T only under the scope of a ‚.
Let » the equivalence between types which allows for an infinite number of unfolding and Σ be
a set tX1 ď Y1 , . . . , Xn ď Yn u of subtype assumptions between type variables which cannot contain
twice the same variable. The subtyping relation of λNak is defined as the smallest relation on types
closed under the following rules:
[ď ‚]

[‚ Ñ]

[Ñ ‚]

[ VAR ]

Σ $ T ď ‚T

Σ $ T Ñ S ď ‚T Ñ ‚S

Σ $ ‚T Ñ ‚S ď ‚pT Ñ Sq

Σ, X ď Y $ X ď Y

[»]

[µ ]

[‚]

[Ñ]

T »S
Σ$T ďS

Σ, X ď Y $ T ď S
Σ $ µX.T ď µY.S

Σ$T ďS
Σ $ ‚T ď ‚S

Σ1 $ S1 ď T1 Σ2 $ T2 ď S2
Σ1 Y Σ2 $ T1 Ñ T2 ď S1 Ñ S2

In Σ $ T ď S, we assume that all the free type variables of T and S are in Σ and that the X’s cannot
occur on the right hand side of ď and the Y ’s cannot occur on the left. The typing rules of λNak are
defined as follows.
[ AXIOM ]

[ď]

[‚ E]

x:T PΓ
Γ $x:T

Γ $ e : T T ď T1
Γ $ e : T1

‚Γ $ e : ‚T Γ , x : T $ e : S
Γ $ e : T Γ $ λ x.e : pT Ñ Sq

[ÑI]

[ÑE]

Γ $ e1 : ‚n pT Ñ Sq Γ $ e2 : ‚n T
Γ $ e1 e2 : ‚n S

We define the function nfµ on guarded µ-types as follows.
nfµ pXq“ X
nfµ p‚T q“ ‚T

nfµ pT Ñ Sq“ nfµ pT q Ñ nfµ pT Sq
nfµ pµX.T q“ nfµ pT qtX ÞÑ T u

‚ by coinduction as follows:
We define the translation tree from µ-types to types in λÑ
$
if nfµ pT q “ X
& treepXq
‚treepSq
if nfµ pT q “ ‚S
treepT q “
%
treepT1 q Ñ treepT2 q if nfµ pT q “ T1 Ñ T2

The translation treepΣq is extended to typing contexts in the obvious way.

16

PAULA SEVERI

‚ into λ
‚
Lemma 4.2 (Embedding λÑ
Nak ). If treepΓ q $ e : treepT q in λÑ without using rule
then Γ $ e : T in λNak .

[CONST]

Proof. It follows by induction on the derivation. It is easy to see that the typing rules [ÑI] and [‚I] of
‚ are admissible in λ
λÑ
Nak by making use of the typing rule [ď].
‚ . For example, $ λ x.x : pT Ñ Sq Ñ p‚T Ñ ‚Sq
Programs in λNak have more types than in λÑ
‚
in λNak but 0 λ x.x : pT Ñ Sq Ñ p‚T Ñ ‚Sq in λÑ .
There are programs that can be typed in λ‚‚ but they cannot be typed in λNak , e.g. get.

5. D ENOTATIONAL S EMANTICS
This section gives a denotational semantics for λ‚‚ where types and expressions are interpreted as
objects and morphisms in the topos of trees [4]. We give a self-contained description of this topos
as a cartesian closed category for a reader familiar with λ -calculus.
The topos S of trees has as objects A families of sets A1 , A2 , . . . indexed by positive integers,
equipped with family of restrictions riA : Ai`1 Ñ Ai . 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 Ñ B are families of functions fi : Ai Ñ Bi obeying the naturality condition
fi ˝ riA “ riB ˝ fi`1 .
A1 o
f1

r1A

f2



B1 o

A2 o

r1B

r2A

f3



B2 o

A3

r2B



B3

...
...

We define riiA “ idA and riAj “ r j ˝ . . . ˝ ri´1 for 1 ď j ă i. Products are defined pointwise.
Exponentials BA have as components the sets:
pBA qi “ tp f1 , . . . , fi q | f j : A j Ñ B j and f j ˝ rAj “ rBj ˝ f j`1 u
and as restrictions riAñB p f1 , . . . fi`1 q “ p f1 , . . . , fi q.
We define eval : BA ˆ A Ñ B as eval i pp f1 , . . . , fi q, aq “ fi paq and curryp f q : C Ñ BA for f :
C ˆ A Ñ B as curryp f qi pcq “ pg1 , . . . , gi q where g j paq “ f j priAj pcq, aq for all a P A j and 1 ď j ď i.
The functor I: S Ñ S is defined on objects as pI Aq1 “ t˚u and pI Aqi`1 “ Ai where r1IA “! and
IA
ri`1
“ riA and on arrows pI f q1 “ idt˚u and pI f qi`1 “ fi . We write In for the n-times composition
of I.
The natural transformation next A : A ÑI A is given by pnext A q1 “! and pnext A qi`1 “ riA which
can easily be extended to a natural transformation next nA : A ÑIn A . It is not difficult to see that
there are isomorphisms θ :I Aˆ I B ÑI pA ˆ Bq and ξ : pI BqpIAq ÑI pBA q which are also
natural. These can also be easily extended to isomorphisms θ n :In Aˆ In B ÑIn pA ˆ Bq and
n
ξ n : pIn BqpI Aq ÑIn pBA q.
The category Set is a full subcategory of S via the functor I with pI pXqqi “ X and rI pXq “
idX and pI p f qqi “ f . The unit 1 of S is I p˚q. We define the functor  : S Ñ S as  “ I ˝
homS p1, ´q. We also define ψ : pBA q Ñ BA as ψi p f q “ pg1 , . . . , gi q where g j pxq “ eval ˝p f ˆxq
for all 1 ď j ď i and f P homp1, BA q and x P homp1, Aq.
A type t is interpreted as an object in S (for simplicity, we omit type variables).

TWO LIGHT MODALITIES FOR RECURSION

17

rrNatss “ I pNatq
rr‚tss “ I ˝rrtss
rrt ˆ sss “ rrtss ˆ rrsss
r
r‚tss “  ˝ rrtss
rrt Ñ sss “ rrsssrrtss
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 pnboxptq, i, rankptqq taking the lexicographic order where
nboxptq and rankptq are defined in Section 3.2. By writing the indices explicitly in the definition of
rrtss, we obtain:
rrNatssi
rrt ˆ sssi
rrt Ñ sssi
rr‚tss1
rr‚tssi`1
rr‚tssi

“
“
“
“
“
“

Nat
rrtssi ˆ rrsssi
rrtss
rrsss
tp f1 , . . . , fi q | f j : rrtss j Ñ rrsss j and f j ˝ r j “ r j ˝ f j`1 u
t˚u
rrtssi
homS p1, rrtssq

It is easy to show that rrtss “ rrsss if t – s.
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 Γ “ x1 : t1 , . . . xk : tk are interpreted
as rrt1 ss ˆ . . . ˆ rrtk ss. The interpretation of typed expressions rrΓ $ e : tss : rrΓ ss Ñ rrtss is defined by
induction on the derivation.
The last rule in the derivation is [AXIOM].
rrΓ $ x : tss “ π j if x “ x j and t j “ t and 1 ď j ď k
The last rule in the derivation is [CONST].
rrΓ $ pair : pt Ñ s Ñ pt ˆ sqqss
rrΓ $ fst : pt ˆ s Ñ tqss
rrΓ $ snd : pt ˆ s Ñ sqss
rrΓ $ 0 : Natss
rrΓ $ succ : pNat Ñ Natqss

“
“
“
“
“

currypcurryp!rrΓ ss ˆ idrrtˆsss qq
curryp!rrΓ ss ˆ π1 q
curryp!rrΓ ss ˆ π2 q
I p˚ ÞÑ 0q
succ

The last rules in the derivation are [‚I], [ÑE] or [‚Ñ E].
rrΓ $ λ x.e : ‚n pt Ñ sqss “ ξ n ˝ curryprrΓ , x : ‚nt $ e : ‚n sssq
rrΓ $ e1 e2 : ‚n sss
“ eval ˝ xpξ n q´1 ˝ rrΓ $ e1 : ‚n pt Ñ sqss, rrΓ $ e2 : ‚ntssy
n
rrΓ $ e1 e2 : ‚ ‚ sss
“ eval ˝ xpξ n q´1 ˝ In pψq ˝ rrΓ $ e1 : ‚n ‚ pt Ñ sqss, rrΓ $ e2 : ‚n ‚ tssy
The last rule in the derivation is [‚I].
rrΓ1 , ‚Γ2 $ e : ‚tss “ !rrΓ1 ss ˆ prrΓ2 $ e : tssqq
The last rule in the derivation is [‚I].
rrΓ1 , ‚Γ2 $ e : ‚tss “ shi f tprrΓ1 , Γ2 $ e : tssq
where shi f tp f q “ uncurrypξ ´1 ˝ next ˝ curryp f qq.
The last rule in the derivation is [–].
rrΓ 1 $ e : t 1 ss “ rrΓ $ e : tss
Lemma 5.1 (Semantic Substitution).
rrΓ , x : t $ e1 : sss ˝ xid, rrΓ $ e2 : tssy “ rrΓ $ e1 re2 {xs : sss

18

PAULA SEVERI

Proof. This follows by induction on e1 . We only sketch the proof for the case e1 “ x.
rrΓ , x : t $ x : ‚ntss ˝ xid, rrΓ $ e2 : tssy “ next n ˝ rrΓ $ e2 : tss “ rrΓ $ e2 : ‚ntss
Theorem 5.2 (Soundness). If Γ $ e : t and e ÝÑ e1 then rrΓ $ e : tss “ rrΓ $ e1 : tss.
Proof. We sketch the case of [R - BETA] which is divided into two subcases.
Suppose first that v1 “ rrΓ , x : ‚nt1 $ e1 : ‚nt2 ss and v2 “ rrΓ $ e2 : ‚nt1 ss.
rrΓ $ pλ x.e1 qe2 : ‚nt2 ss “ eval ˝ xpξ n q´1 ˝ ξ n ˝ currypv1 q, v2 y “ v1 ˝ xid, v2 y
“ rrΓ $ e1 re2 {xs : ‚nt2 ss by Lemma 5.1
Suppose now v1 “ rrΓ21 , x : ‚mt1 $ e1 : ‚mt2 ss and v2 “ rrΓ $ e2 : ‚n ‚ t1 ss where Γ “ Γ1 , Γ2 and
“ tx1 : s1 , . . . , xk : sk u and Γ2 – tx1 : ‚n1 ‚ s1 , . . . , xk : ‚nk ‚ sk u and maxpn1 , . . . , nk q ď n. Let v3 “
rrΓ , x : ‚n ‚ t1 $ e1 : ‚n ‚ t2 ss “!rrΓ1 ss ˆ shi f t n ppv1 qq.
Γ21

rrΓ $ pλ x.e1 qe2 : ‚n ‚ t2 ss “ eval ˝ xpξ n q´1 ˝ In pψq ˝ p!rrΓ1 ss ˆ shi f t n ppcurrypv1 qqq, v2 y
“ eval ˝ xcurrypv3 q, v2 y “ v3 ˝ xid, v2 y
“ rrΓ $ e1 re2 {xs : ‚nt2 ss by Lemma 5.1
We consider contexts C without any restriction in the position of the hole rs. We say that C is a
closing context of type t if x : s $ Crxs : t for some variable x that does not occur in C.
Definition 5.3. Let Γ $ e1 : t and Γ $ e2 : t. We say that e1 and e2 are observationally equivalent,
denoted by e1 « e2 , if Cre1 s ÝÑ˚ succn 0 iff Cre2 s ÝÑ˚ succn 0 for all closing contexts C of type
Nat.
Corollary 5.4. If rrΓ $ e1 : tss “ rrΓ $ e2 : tss then, e1 « e2 .
Proof. By compositionality of the denotational semantics, rr$ Cre1 s : tss “ rr$ Cre2 s : tss. Suppose
Cre1 s ÝÑ˚ succn 0. By Theorem 5.2, rrΓ $ Cre1 s : tss “ rrsuccn 0ss. By the definition of interpretation, Cre2 s ÝÑ˚ succn 0.
6. A T YPE I NFERENCE A LGORITHM
In this section, we define a type inference algorithm for λ‚‚ . Apart from the usual complications
that come from having no type declarations, the difficulty of finding an appropriate type inference
algorithm for λ‚‚ is due to the fact that the expressions do not have a constructor and destructor
for ‚ and ‚. We do not know which sub-expressions need to be delayed as illustrated by the type
derivation of fix where the first occurrence of pλ x.y px xqq has a different derivation from the
second one since [‚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. All this is complicated even more by the fact that [‚I] could be applied as well at any
point in the derivation when the expression is closed.

TWO LIGHT MODALITIES FOR RECURSION

19

6.1. Towards a Syntax-directed Type System. We will eliminate the rules [‚I], [‚I] and [–] from
λ‚‚ and obtain a type system pλ‚‚ q´ . In order to eliminate the rule [–], we need to normalize the
types.
Definition 6.1. A type is in normal form if it does not contain subexpressions of the form ‚ ‚ t or
‚ ‚ t. A context Γ is in normal form if all the types in Γ are in normal form.
Definition 6.2 (Normal Form of a Type). We define nf by coinduction.
$
Nat
if wnf ptq “ Nat
’
’
’
’
nf
ps
q
ˆ
nf
ps
q
if
wnf ptq “ s1 ˆ s2
1
2
’
&
nf ps1 q Ñ nf ps2 q if wnf ptq “ s1 Ñ s2
nf ptq “
’
’
’
‚nf psq
if wnf ptq “ ‚s
’
’
%
‚nf psq
if wnf ptq “ ‚s
where wnf is defined by induction on nboxptq as follows.
wnf ptq “ t $
if t ­“ ‚s
Nat
’
’
&
‚s
wnf p‚tq “
‚s
’
’
%
‚wnf ptq

if wnf ptq “ ‚n Nat
if wnf ptq “ ‚n s and s ­“ ‚s1 and s ­“ ‚s1
if wnf ptq “ ‚n ‚ s
otherwise

Note that nf ptq is in normal form. It is not difficult to show that if t –w t 1 then wnf ptq “ wnf pt 1 q
and that if t – t 1 then nf ptq “ nf pt 1 q.
The function nf is extended to typing contexts in the obvious way.
The type assignment system pλ‚‚ q´ is defined by the following rules.
[ AXIOM ]

[ CONST ]

[ ‚ CONST ]

[ÑI]

x:t PΓ
Γ $ x : ‚nt

k:t Pκ
Γ $ k : ‚nt

k:t Pκ
Γ $ k : ‚n ‚ t

Γ , x : ‚nt $ e : ‚n s
Γ $ λ x.e : ‚n pt Ñ sq

[‚ ÑI]

ty1 : s1 , . . . , yk : sk u Y tx : ‚mtu $ e : ‚m s
maxpn1 , . . . , nk q ď n
n1
nk
Γ Y ty1 : ‚ nf p‚s1 q, . . . , yk : ‚ nf p‚sk qu $ λ x.e : ‚n ‚ pt Ñ sq
[ÑE]

[‚Ñ E]

Γ $ e1 : ‚n pt Ñ sq Γ $ e2 : ‚nt
Γ $ e1 e2 : ‚n s

Γ $ e1 : ‚n ‚ pt Ñ sq Γ $ e2 : ‚n nf p‚tq
Γ $ e1 e2 : ‚n nf p‚sq

Note that all the typing rules are duplicated except for [AXIOM]. The type system pλ‚‚ q´ is not
syntax directed. However, this is the best we can get since either ‚ and ‚ could be introduced at any
point in the derivation and this is not marked in the program.
Lemma 6.3 (Equivalence between λ‚‚ and pλ‚‚ q´ ).
(1) If Γ $ e : t in pλ‚‚ q´ then Γ $ e : t in λ‚‚ .
(2) If Γ $ e : t in λ‚‚ then nf pΓ q $ e : nf ptq in pλ‚‚ q´ .
Proof. The first part follows by an easy induction on the derivation. The second part follows by
induction on e using Lemma 3.2.

20

PAULA SEVERI

6.2. Meta-types. The type inference algorithm infers meta-types which are a generalization of
types where the ‚ can be exponentiated with integer expressions, e.g. ‚N1 X Ñ ‚N2 ´N1 X. The syntax
for meta-types is defined below. A meta-type can contain type variables and (non-negative) integer
1
expressions with variables. In this syntax, ‚T is written as ‚1 T . We identify ‚0 T with T and ‚E ‚E T
1
with ‚E`E T .
E ::“ind
|
|
|

N
n
E `E
E ´E

Integer Expression
(integer variable)
(integer number)
(addition)
(substraction)

T ::“coind
|
|
|
|
|
|

X
Nat
T ˆT
T ÑT
‚E T
‚T
‚E nfp‚Xq

Pseudo Meta-type
(type variable)
(natural numbers)
(product)
(arrow)
(delay)
(now)
(normalize)

The constant nf is a mark in the meta-type that indicates that what comes after needs to be
normalized. The constant nf will be introduced by the constraint typing rules (Table 2) and later be
handled by the unification algorithm. It allows the constraint typing rules to delegate the problem
of considering all the possibilities for X in ‚X to the unification algorithm.
Definition 6.4. We say that T is positive if all the exponents of ‚ are natural numbers.
We identify a positive pseudo meta-type with the pseudo-type obtained from replacing the type
constructor ‚n in the syntax of pseudo meta-types with n consecutive ‚’s in the syntax of pseudotypes.
Definition 6.5. A pseudo meta-type is in normal form if it does not contain subexpressions of the
form ‚ ‚E T or ‚ ‚ T .
For example, the meta-type ‚ ‚N Nat is not in normal form. The function nf is defined on
meta-types similar to Definition 6.2.
Definition 6.6 (Integer Expression and Type Substitution). Let τ “ tX1 ÞÑ T1 , . . . , Xn ÞÑ Tn u be
a finite mapping from type variables to pseudo meta-types where dompτq “ tX1 , . . . , Xn u. Let
θ “ tN1 ÞÑ E1 , . . . , Nm ÞÑ Em u be a finite mapping from integer variables to integer expressions
where dompθ q “ tN1 , . . . , Nm u. Let also σ “ τ Y θ . We define the substitutions θ pEq on an integer
expression E and σ pT q on a pseudo meta-type T as follows.
"
T if X ÞÑ T P τ
σ
pXq
“
"
X otherwise
E if N ÞÑ E P θ
σ
pNatq
“
Nat
θ pNq
“
N otherwise
σ pT1 Ñ T2 q
“ σ pT1 q Ñ σ pT2 q
θ pnq
“ n
σ pT1 ˆ T2 q
“ σ pT1 q ˆ σ pT2 q
θ pE1 ` E2 q “ θ pE1 q ` θ pE2 q
σ p‚E T q
“ ‚θ pEq σ pT q
θ pE1 ´ E2 q “ θ pE1 q ´ θ pE2 q
σ p‚T q
“ ‚pσ pT qq
σ p‚E nfp‚Xqq “ ‚θ pEq nf pσ p‚Xqq
If the substitution τ is tX ÞÑ T u then τpT q is also denoted as T tX ÞÑ T u as usual.
Composition of substitutions is defined as usual. Note that the empty set is the identity substitution and σ “ θ ˝ τ if σ “ τ Y θ .

TWO LIGHT MODALITIES FOR RECURSION

21

Definition 6.7. We say that θ is natural if it maps all integer variables into natural numbers, i.e.
θ pNq P N for all N P dompτq.
For example, the substitution θ “ tN ÞÑ 3, M ÞÑ 5u is natural but θ p‚N´M Natq is not positive.
We can define regular and local pseudo meta-types similar to Definition 2.1. We say that a
pseudo meta-type T is guarded if θ pT q is positive and guarded (as a pseudo type) for all natural θ .
The pseudo meta-type which is solution of the recursive equation T “ Natˆ‚N T is not guarded
but it is guarded if we substitute N by M ` 1.
Definition 6.8. A meta-type is a pseudo meta-type that is regular, local and guarded.
Note that finite pseudo meta-types are always meta-types, e.g. Nat ˆ ‚N X is a meta-type.
Definition 6.9. We say that the substitution σ “ τ Y θ is:
(1) guarded if σ pXq is guarded for all X P dompτq.
(2) local if σ pXq is local for all X P dompτq.
(3) meta-type if it is guarded and local, i.e. it is a substitution from type variables to meta-types.
(4) positive if θ is natural and θ pτpXqq is positive for all X P dompτq.
(5) type if it is meta-type and positive, i.e. it is a substitution from type variables to types.
(6) normal if σ pXq is in normal form for all X P dompτq.
(7) always normal if σ 1 ˝ σ is normal for all σ 1 normal.
For example, τ “ tX ÞÑ ‚pY1 ˆY2 qu is always normal while τ “ tX ÞÑ ‚Y u is not.
Definition 6.10 (Constraints). There are two types of constraints.
?

(1) A meta-type constraint is T “ T 1 for finite meta-types T and T 1 .
?

?

?

(2) An integer constraint is either E “ E 1 or E ě E 1 or E ă E 1 .
Sets of constraints are denoted by C , E , etc. If C is a set of meta-type constraints then,
(1) C “ denotes the subset of equality constraints from C ,
(2) C N denotes the set of integer constraints from C .
?

?

?

Moreover, σ |ù T “ T 1 means that σ pT q “ σ pT 1 q. Similarly, we define θ |ù E “ E 1 , θ |ù E ě
?

E 1 and θ |ù E ă E 1 . This notation extends to sets C of constraints in the obvious way. When
σ |ù C , we say that σ is a solution (unifier) for C .
Definition 6.11. We say that τ is:
(1) E -guarded if θ ˝ τ is guarded for all natural substitution θ such that θ |ù E .
(2) E -positive if θ ˝ τ is positive for all natural substitution θ such that θ |ù E .
Recall that StreampN,Y q “ Y ˆ ‚N StreampN,Y q. For example,
?

(1) τ “ tX ÞÑ StreampN,Y qu is E -guarded but it is not H-guarded for E “ tN ě 1u and,
?

(2) τ “ tX ÞÑ ‚M´N Natu is E -positive but it is not H-positive for E “ tM ě Nu.
?

?

Definition 6.12. We say that C is substitutional if C “ “ tX1 “ T1 , . . . , Xn “ Tn u, all variables
X1 , . . . , Xn are pairwise different and none of the meta-types T1 , . . . , Tn contain the constant nf.
Since a substitutional C corresponds to a set of recursive equations where T1 , . . . , Tn are finite
meta-types, there exists a unique solution τC such that τC pXi q is regular for all 1 ď i ď n [11], [7,

22

PAULA SEVERI

Theorem 7.5.34]. The mapping τC is the most general unifier, i.e. if σ |ù C then there exists σ 1
such that σ “ σ 1 ˝ τC . Moreover, if σ “ τ Y θ then σ 1 “ τ 1 Y θ where
"
τpXq if X ‰ Xi for all 1 ď i ď n
τ 1 pXq “
X
otherwise
?

For example, if C “ tX “ Y ˆ ‚N Xu then τC pXq “ StreampN,Y q. If σ |ù C and σ “ τ Y θ then
σ “ σ 1 ˝ τC and σ 1 “ τ 1 Y θ and τ 1 “ tY ÞÑ τpY qu.
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
µX.t “ ttX ÞÑ µX.tu [6, 7].
For 1 ď i ď n, we know that τC pXi q is regular but we do not know yet if τC is guarded, local,
positive or normal. Below, we show some examples:
?

?

(1) Let C “ tX1 “ X2 Ñ ‚X1 , X2 “ ‚X1 Ñ ‚X2 u. Then, τC “ tX1 ÞÑ t1 , X2 ÞÑ t2 u is a normal type
substitution where t1 and t2 satisfy the recursive equations t1 “ t2 Ñ ‚t1 and t2 “ ‚t1 Ñ ‚t2 .
?
?
(2) Let C “ tX1 “ X2 Ñ ‚X1 , X2 “ X1 Ñ ‚X2 u. Then, τC “ tX1 ÞÑ t1 , X2 ÞÑ t2 u is local, positive,
normal where t1 and t2 satisfy the recursive equations t1 “ t2 Ñ ‚t1 and t2 “ t1 Ñ ‚t2 . But
τC is not guarded since there is an infinite branch in the tree representations of t1 and t2 that
has no ‚’s. Observe that t1 “ pt1 Ñ ‚t2 q Ñ ‚t1 and t2 “ pt2 Ñ ‚t1 q Ñ ‚t2 .
?
?
(3) Let C “ tX1 “ X2 Ñ ‚X1 , X2 “ ‚p‚X1 Ñ X2 qu. Then, τC “ tX1 ÞÑ t1 , X2 ÞÑ t2 u is guarded,
positive and normal where t1 and t2 satisfy the recursive equations t1 “ t2 Ñ ‚t1 and t2 “
‚p‚t1 Ñ t2 q. But τC is not local since the tree representations of t1 and t2 have an infinite
branch with an infinite number of ‚’s. Observe that t2 “ ‚p‚pt2 Ñ ‚t1 q Ñ t2 q.
?
?
(4) Let C “ tX1 “ ‚N`1 pX2 Ñ ‚X1 q, X2 “ ‚M X1 u. Then, τC “ tX1 ÞÑ T1 , X2 ÞÑ T2 u is a normal
meta-type substitution where T1 and T2 satisfy the recursive equations T1 “ ‚N`1 pT2 Ñ ‚T1 q
and T2 “ ‚M T1 . But τC is not positive since N and M are integer variables.
?
?
(5) Let C “ tX1 “ ‚X2 , X2 “ ‚pNat ˆ X2 qu. Then, τC “ tX1 ÞÑ t1 , X2 ÞÑ t2 u is a type substitution
where t1 and t2 satisfy the recursive equations t1 “ ‚t2 and t2 “ ‚pNat ˆ t2 q. But τC is not
normal since t1 is not in normal form. Observe that t1 “ ‚ ‚ pNat ˆ t2 q.
Definition 6.13.
(1) We say that C is always positive if all the meta-types in θ pC “ q are positive
for all natural substitution θ such that θ |ù C N .
(2) We say that a meta-type T is always in normal form if σ pT q is in normal form for all normal
substitution σ .
(3) We say that C is always normal if the meta-types in C are always in normal form.
For example,
?

?

?

(1) C “ tX “ ‚N pX1 Ñ X2 q, N ě 1u is always positive while C “ tX “ ‚N pX1 Ñ X2 qu is not.
?
?
(2) C “ tX “ ‚pX1 Ñ X2 qu is always normal while C “ tX “ ‚Y u is not.
6.3. Constraint Typing Rules. The constraint typing rules for λ‚‚ consists of the typing rules of
Table 1 together with the ones of Table 2.
Since pair, fst and snd are actually ‘polymorphic’, we need to generate different fresh variables depending on their position. For convenience, we define the following function:
typeOfppair, X1 , X2 q “ X1 Ñ X2 Ñ X1 ˆ X2
typeOfpfst, X1 , X2 q “ X1 ˆ X2 Ñ X1
typeOfpsnd, X1 , X2 q “ X1 ˆ X2 Ñ X2

TWO LIGHT MODALITIES FOR RECURSION

23

‚
Table 1: Constraint Typing Rules for λÑ
[ AXIOM ]

[ˆ CONST ]

N, X1 , X2 are fresh

N is fresh
N

∆ $ k : ‚N typeOfpk, X1 , X2 q | H

∆, x : X $ x : ‚ X | H

k P tpair, fst, sndu

[Natsucc ]

[Nat0]

N is fresh

N is fresh

N

∆ $ succ : ‚N pNat Ñ Natq | H

∆ $ 0 : ‚ Nat | H
[ÑI]

∆, x : X $ e : T | C

X, X1 , X2 , N are fresh
?

?

∆ $ λ x.e : ‚N pX1 Ñ X2 q | C Y tX “ ‚N X1 , T “ ‚N X2 u
[ÑE]

∆ $ e1 : T1 | C1

∆ $ e2 : T2 | C2

X1 , X2 , N are fresh
?

?

∆ $ e1 e2 : ‚ X2 | C1 Y C2 Y t‚ pX1 Ñ X2 q “ T1 , ‚N X1 “ T2 u
N

N

The typing rules should be read bottom-up. We start from an empty context and a closed
expression and we build the typing context ∆ and the set C of constraints. We can, then, assume
that the typing context ∆ only contains declarations of the form x : X and the set C contains only
equality constraints between finite meta-types.The type variables in the contexts ∆ are all fresh and
they are created by the rules [ÑI] and [‚ ÑI] for the abstraction.
If instead of generating the fresh variable X in [ÑI] we directly put ‚N X1 in the context, then the
algorithm would not be complete. For example, consider x : ‚5 Nat $ x : ‚7 Nat. Then N should be
assigned the value 3 and not 5 if later we derive that λ x.x : ‚2 p‚3 Nat Ñ ‚5 Natq.
Note that a positive meta-type in normal form can be identified with a type (Definition 2.1)
which is in normal form (see Definition 6.1). If σ is a positive and normal substitution from metavariables to meta-types, then all the meta-types in σ p∆q are actually types in normal form.
Theorem 6.14 (Soundness of Constraint Typing). Let σ be a normal type substitution. If ∆ $ e :
T | C and σ |ù C then σ p∆q $ e : σ pT q in pλ‚‚ q´ and σ pT q is a type in normal form.
Proof. We proceed by induction on the derivation of ∆ $ e : T | C . Suppose the last rule in the
derivation of ∆ $ e : T | C is:
[ÑI]

∆, x : X $ e : T 1 | C

X, X1 , X2 , N are fresh
?

?

∆ $ λ x.e : ‚ pX1 Ñ X2 q | C Y tX “ ‚N X1 , T 1 “ ‚N X2 u
N

?

?

It follows from induction hypothesis that σ p∆q, x : σ pXq $ e : σ pT 1 q. Since σ |ù tX “ ‚N X1 , T 1 “
‚N X2 u, we also have that σ p∆q, x : ‚σ pNq σ pX1 q $ e : ‚σ pNq σ pX2 q. We can, then, apply [ÑI] of pλ‚‚ q´
to conclude that σ p∆q $ λ x.e : ‚σ pNq pσ pX1 q Ñ σ pX2 qq. It follows from the fact that σ is a normal
type substitution that σ pT q “ ‚σ pNq pσ pX1 q Ñ σ pX2 qq is a type in normal form.

24

PAULA SEVERI

Table 2: Constraint Typing Rules for ‚
[‚ˆ CONST ]

N, X1 , X2 are fresh
∆ $ k : ‚N ‚ typeOfpk, X1 , X2 q | H
[‚Nat0]

k P tpair, fst, sndu

[‚Natsucc ]

N is fresh

N is fresh

N

∆ $ 0 : ‚ ‚ Nat | H

∆ $ succ : ‚N ‚ pNat Ñ Natq | H

[‚ ÑI]

ty1 : Y1 , . . . , yk : Yk u Y tx : Xu $ e : T | C
?

?

C1 “ tX “ ‚M X1 , T “ ‚M X2 u

tX, X1 , X2 , N, Mu Y tYi , Ni | 1 ď i ď ku are fresh
?

?

C2 “ tZi “ ‚Ni nfp‚Yi q | 1 ď i ď ku Y tN ě Ni | 1 ď i ď ku

∆ Y ty1 : Z1 , . . . , yk : Zk u $ λ x.e : ‚N ‚ pX1 Ñ X2 q | C Y C1 Y C2
[‚Ñ E]

∆ $ e1 : T1 | C1

∆ $ e2 : T2 | C2

X1 , X2 , N are fresh
?

?

∆ $ e1 e2 : ‚ nfp‚X2 q | C1 Y C2 Y t‚ ‚ pX1 Ñ X2 q “ T1 , ‚N nfp‚X1 q “ T2 u
N

N

Suppose the last rule in the derivation of ∆ $ e : T | C is:
[‚Ñ E]

∆ $ e1 : T1 | C1

∆ $ e2 : T2 | C2

X1 , X2 , N are fresh
?

?

∆ $ e1 e2 : ‚N nfp‚X2 q | C1 Y C2 Y t‚N ‚ pX1 Ñ X2 q “ T1 , ‚N nfp‚X1 q “ T2 u
It follows from induction hypothesis that σ p∆q $ e1 : σ pT1 q and σ p∆q $ e2 : σ pT2 q. Since σ |ù C ,
we also have that σ p∆q $ e1 : ‚σ pNq ‚ pσ pX1 q Ñ σ pX2 qq and σ p∆q $ e2 : ‚σ pNq σ pnfp‚X1 qq. Hence,
σ p∆q $ e1 e2 : σ p‚N nfp‚X2 qq. Since σ is a normal type substitution, σ p‚N nfp‚X2 qq is a type in
normal form. Note that σ p‚X2 q may not be in normal form even though σ pX2 q is in normal form.
Theorem 6.15 (Completeness of Constraint Typing). Let Γ “ x1 : t1 , . . . , xm : tm be in normal form
and ∆ “ x1 : X1 , . . . , xm : Xm . If Γ $ e : t in pλ‚‚ q´ then there are T and C such that
(1) ∆ $ e : T | C
(2) there exists a normal type substitution σ Ě tX1 ÞÑ t1 , . . . , Xm ÞÑ tm u such that σ |ù C and
σ pT q “ t and dompσ qztX1 , . . . , Xm u is the set of fresh variables in the derivation of ∆ $ e :
T | C.
Proof. We proceed by induction on the derivation. Suppose the last typing rule in the derivation is:
[ AXIOM ]

xi : ti P Γ
Γ $ xi : ‚nti
Then, ∆ $ xi : ‚N Xi | H. We define σ “ tX1 ÞÑ t1 , . . . , Xm ÞÑ tm u Y tN ÞÑ nu. It is easy to see that
σ p∆q “ Γ and t “ σ p‚N Xi q.

TWO LIGHT MODALITIES FOR RECURSION

25

Suppose the last typing rule in the derivation is:
[ÑE]

Γ $ e1 : ‚n pt Ñ sq Γ $ e2 : ‚nt
Γ $ e1 e2 : ‚n s
By induction hypotheses,
´ ∆ $ e1 : T1 | C1 and ∆ $ e2 : T2 | C2 ,
´ σ1 |ù C1 and σ2 |ù C2 and σ1 pT1 q “ ‚n pt Ñ sq and σ2 pT1 q “ ‚n s for σ1 , σ2 Ě tX1 ÞÑ
t1 , . . . , Xm ÞÑ tm u,
´ dompσ1 qztX1 , . . . , Xm u and dompσ2 qztX1 , . . . , Xm u are the sets of fresh variables in the derivation of ∆ $ e1 : T1 | C1 and ∆ $ e2 : T2 | C2 , respectively.
It follows from the latter that σ1 Y σ2 is a function and we can define the substitution σ as
pσ1 Y σ2 qtN ÞÑ nutX1 ÞÑ tutX2 ÞÑ su.
6.4. Unification Algorithm. Algorithm 1 solves the unification problem. The input consists of a
set C of constraints and an extra argument V that keeps tracks of the “visited equality constraints”
and guarantees termination.
The base case on Line 1 is when the set C “ C “ Y C N is substitutional (see Definitions 6.10
and 6.12). The set C N guarantee that the exponents of the ‚’s are positive. Line 2 invokes the
function guard which creates a set of constraints to ensure guardedness. Line 3 checks whether
E “ C N Y guardpC q has a solution and τC is local. Altogether, this implies that θ ˝ τC is guarded,
local and positive for all natural θ |ù E . The functions guard and local? are defined in Algorithm 3
and Algorithm 4 (Appendix B) respectively.
In order to check that E has a solution of non-negative integers (Line 3), we can use any
algorithm for linear integer programming [24].
If C is not substitutional we examine the equations in C “ (Line 4 onwards).
The function unify does not return only one solution but a set of solutions. This is because
1
?
?
there are several ways of solving certain equality constraints, i.e. T “ ‚E nfp‚Xq and ‚E X “ ‚E X 1
(Lines 6 and 16).
?

?

?

?

(1) If T “ ‚E nfp‚Xq, then T “ ‚E ‚Y and either X “ ‚E ‚Y or X “ ‚E Y . In order to guarantee
?
that the set of constraints is always normal (see Definition 6.13), we add either Y “ Nat or
?
?
Y “ Y1 Ñ Y2 or Y “ Y1 ˆY2 .
?

1

?

?

1

?

?

1

(2) If ‚E X “ ‚E X 1 , we solve either E ě E 1 and X 1 “ ‚E´E X or E 1 ě E and X “ ‚E ´E X 1 .
?

The case that eliminates two equality constraints for the same variable (Line 13) removes X “ S
?
?
?
from C but it adds S “ S1 . If V already contains X “ S, it means that X “ S has already been
processed and it will not be added again avoiding non-termination. The unification algorithm for the
simply typed lambda calculus solves the problem of termination in this case by reducing the number
of variables, i.e. checks if X R S and then, substitutes the variable X by S in the remaining set of
constraints. With recursive types, however, we do not perform the occur check and the number of
variables may not decrease since the variable X may not disappear after substituting X by S (because
X occurs in S). In order to decrease the number of variables, we could perhaps substitute X by the
solution of the recursive equation X “ S (which may be infinite). But the problem of guaranteeing
termination would still be present because the meta-types in the constraints can be infinite and the
size of the equality constraints may not decrease. We would also have a similar problem with

26

PAULA SEVERI

termination if we use multi-equations and a rewrite relation instead of giving a function such as
unify [26].
The case on Lines 20 uses the function NatOpBox?pT q which returns true iff T is either Nat
or pS1 op S2 q or ‚S (see Algorithm 5 in Appendix B). It is clear that if E 1 ă E, then the equation
1
?
?
‚E X “ ‚E S1 does not have a solution, e.g. ‚5 X “ ‚2 pT1 ˆ T2 q.
The cases on Lines 22 and 24 use the function EqualCons?pT, Sq which returns true iff both
types are equal ‘at depth 0’ (see Algorithm 6 in Appendix B).
?
We assume that the case T “ nfp‚Xq without any ‚’s in front of nf does not happen since this
is the way these constraints appear in Table 2.
?
The algorithm analyses the form of the equation T “ S and the cases are done in order which
means that at Line 30, the equation does not have any of the forms described in the above cases
?
but it could be that S “ T does. For this, the algorithm swaps the equation and calls unify again.
Termination is guaranteed by checking that the constraint does not belong to V . In the last case
(Line 32), the algorithm returns the empty set of solutions when all the previous cases have failed.
?
?
?
Instead of adding either Y “ Nat or Y “ Y1 Ñ Y2 or Y “ Y1 ˆ Y2 on Line 9, we could have
?

?

difference constraints T 1 ‰ ‚r s and T 1 ‰ ‚r s. However, the solutions would have to be equipped
?
with diference constraints as well. For example, the solution of C “ tX “ ‚Y u is τC pXq “ ‚Y
provided Y ‰ ‚r s and Y ‰ ‚r s. Difference constraints do not make the algorithm simpler because
the algorithm would have to generate integer constraints guaranteeing that the difference constraints
?

?

have a solution. For example, to check whether the set C “ tX “ ‚N Nat, X ‰ ‚r su has a solution,
?
the algorithm would have to generate the set tN “ 0u and check if that set has a solution. Similarly,
?

?

?

for C “ tX “ ‚N ‚ Nat, X ‰ ‚r su the algorithm would have to generate t0 ă Nu.
The size |C | of a set of meta-type constraints is the sum of the number of type variables and
type constructors in the left hand side of the equality constraints. Since the meta-types in C are
finite, the size is always finite. We define
?

SubTpC q “ tT | S1 “ S2 P C and either S1 or S2 contains T u
?
SubCpC q “ tT1 “ T2 | T1 , T2 P SubTpC qu
We also define #nf pC q as the number of nf1 in C .
Theorem 6.16 (Termination). Let C and V be sets of constraints. Then, unifypC , V q terminates
Proof. Let C0 “ C and V0 “ V . Suppose towards a contradiction that there is an infinite sequence
of recursive calls:
unifypC0 , V0 q, unifypC1 , V1 q, unifypC2 , V2 q, . . .
(6.1)
This means that unifypCi , Vi q recursively calls unifypCi`1 , Vi`1 q for all i ě 0. From the definition
of the algorithm, one can see that Ci Ď SubCpC0 q and Vi Ď V0 Y SubCpC0 q for all i ě 0. We define
now a measure that decreases with each recursive call:
ri “ p|SubCpC0 q| ` |V0 | ´ |Vi |, #nf pCi q, |Ci |q
It is not difficult to show that ri ą ri`1 contradicting the fact that the sequence in Eq. (6.1) is infinite.
Note that on Line 6 of the algorithm the number of nf’s decreases.

TWO LIGHT MODALITIES FOR RECURSION

27

Algorithm 1: Unification Algorithm
Function unifypC , V q
input : C is a set of constraints and V is the set of visited equality constraints
output: txτ, E y | τ Y θ |ù C @θ |ù E u
1
if C is substitutional then
2
E Ð C N Y guardpC q ;
3
if local?pτC q and E has a solution of non-negative integers then return txτC , E yu
else return H ;
4
5
6
7

?

else if T “ S P C then
?
?
C 1 Ð C ztT “ Su; V 1 Ð V Y tT “ Su
?

case S “ ‚E nfp‚Xq
Choose N,Y,Y1 ,Y2 fresh

/* T “ ‚E nfp‚Xq */ do
/* elimination of nf */;

?

?

8

D1 Ð tX “ ‚N ‚Y u; D2 Ð tX “ ‚N Y u;

9

F1 Ð tY “ Natu; F2 Ð tY “ Y1 Ñ Y2 u; F3 Ð tY “ Y1 ˆY2 u ;

10
11
12

?

?

?

?

Ci j Ð C 1 Y tT “ ‚E ‚Y u Y Di Y F j
Ť
1
return
iPt1,2u jPt1,2,3u unifypCi j , V q

/* 6 options */;
?

case S “ T do unifypC 1 , V 1 q

/* T “ T */;

?

?

?

15

case T “ X and X “ S1 P C 1
/* X “ S and X “ S1 */ do
?
?
if T “ S R V then return unifypC 1 Y tS “ S1 u, V 1 q;
else return unifypC 1 , V 1 q;

16

case T “ ‚E X and S “ ‚E X 1

13
14

17

?

1

?

C1 Ð C 1 Y tX “ ‚
?

E 1 ´E

?

?

19
20

case T “ ‚E X and S “ ‚E S1 and NatOpBox?pS1 q

21
22
23
24
25
26
27
28
29

/* 2nd option */
?

1

1

/* ‚E X “ ‚E S1 */ do

?
?
1
?
return unifypC 1 Y tX “ ‚E ´E S1 , E 1 ě E, E ě 0u, V 1 q
1

case T “ ‚E T 1 and S “ ‚E S1 and EqualCons?pT 1 , S1 q
?
?
return unifypC 1 Y tT 1 “ S1 , E “ E 1 u, V 1 q
case T “ ‚E T 1 and EqualCons?pT 1 , Sq
?
?
return unifypC 1 Y tT 1 “ S, E “ 0u, V 1 q
case T “ T1 op T2 and S “ S1 op S2
?
?
return unifypC 1 Y tT1 “ S1 , T2 “ S2 u, V 1 q
case T “ ‚T 1 and S “ ‚S1
?
return unifypC 1 Y tT 1 “ S1 u, V 1 q
?

31

case T “ S R V
?
return unifypC 1 Y tS “ T u, V 1 q

32

otherwise do return H

30

/* 1st option */

?

C2 Ð C 1 Y tX 1 “ ‚
X, E ě E 1 , E 1 ě 0u
return unifypC1 , V 1 q Y unifypC2 , V 1 q

18

*/ do

?

X 1 , E 1 ě E, E ě 0u;

E´E 1

1

/* ‚E X “ ‚E X 1

?

1

/* ‚E T 1 “ ‚E S1 */ do
?

/* ‚E T 1 “ S */ do
?

/* T1 op T2 “ S1 op S2 */ do
?

/* ‚T 1 “ ‚S1 */ do
?

/* T “ S */ do
/* swap metatypes (symmetry) */
/* failure */ ;

28

PAULA SEVERI

Theorem 6.17 (Completeness of Unification). Let σ be a normal type substitution. If σ |ù C then
there exists xτ, E y P unifypC , V q such that σ “ σ 1 ˝ τ dompσ q and σ 1 “ τ 1 Y θ 1 and θ 1 |ù E .
Proof. By induction on the number of recursive calls which is finite by Theorem 6.16. We do only
two cases.
Suppose C is substitutional. Since τ “ τC is the most general unifier, there exists σ 1 “ τ 1 Y θ 1
such that σ “ σ 1 ˝ τC . Since σ is guarded, so is θ 1 ˝ τC and θ 1 |ù E “ guardpC q.
?
Suppose the constraint of C which is being processed is T “ ‚E nfp‚Xq. Then,
σ pT q “ ‚σ pEq nf p‚σ pXqq
Hence, σ pT q “ ‚σ pEq ‚t is in normal form where t is either Nat or t1 Ñ t2 or t1 ˆt2 for t1 and t2
types in normal form. Since σ is normal, σ pXq is in normal form and it could be either ‚n ‚ t or ‚nt.
We only show the case t “ t1 Ñ t2 and σ pXq “ ‚n ‚ t. The proof of the other cases is similar. We
extend σ to σ1 “ σ Y tN ÞÑ n,Y ÞÑ pt1 Ñ t2 q,Y1 ÞÑ t1 ,Y2 ÞÑ t2 u. It is easy to see that σ1 |ù C12 . By
induction hypothesis, there exists xτ, E y P unifypC12 , V 1 q such that σ1 “ σ11 ˝ τ and σ11 “ τ11 Y θ 1
and θ 1 |ù E . For Z P dompσ q, σ pZq “ σ1 pZq “ σ11 ˝ τpZq and hence, σ “ σ11 ˝ τ dompσ q .
Theorem 6.18 (Soundness of Unification). Let C be always positive and always normal. If xτ, E y P
unifypC , V q then
(1) there exists a natural θ such that θ |ù E and,
(2) for all natural θ such that θ |ù E ,
(i) τ Y θ |ù C and,
(ii) τ Y θ is an always normal type substitution.
Proof. By induction on the number of recursive calls which is finite by Theorem 6.16. We do only
two cases.
Suppose first that C is substitutional. Then, τ “ τC and E “ C N Y guardpC q. Item 1 follows
from the check on Line 3. Assume that θ |ù E . Then, θ |ù guardpC q and θ |ù C N . Then, τC Y θ is
guarded. The fact that τC Y θ is local follow from the check on Line 3. Since C is always positive,
θ pC “ q is positive and also τC Y θ is positive. It follows from the fact that C is always normal that
τC Y θ is always normal too.
?
Suppose now that the constraint is T “ ‚E nfp‚Xq and xτ, E y P unifypC12 , V 1 q where C12 “
?
?
?
tT “ ‚E ‚ Y, X “ ‚N ‚ Y,Y “ Y1 Ñ Y2 u. It is easy to show that C12 is always positive and normal.
By induction hypothesis, τ Y θ |ù C12 and τ is (always) normal. Let σ “ τ Y θ and θ |ù E . Then,
σ pY1 q and σ pY2 q are in normal form and also:
σ pT q “ ‚σ pEq ‚ pσ pY1 q Ñ σ pY2 qq “ ‚σ pEq nf p‚ ‚σ pNq ‚pσ pY1 q Ñ σ pY2 qqq
?

Hence, σ |ù T “ ‚E nfp‚Xq.
The cases xτ, E y P unifypCi j , V 1 q for 1 ď i ď 2 and 1 ď j ď 3 and i ­“ 1 and j ­“ 2 are proved
similarly.
6.5. Type Inference Algorithm. Algorithm 2 solves the type inference problem in λ‚‚ . It returns a
finite set of meta-types that cover all the possible types of a closed expression e, i.e. any type of e is
an instantiation of one of those meta-types.
Line 2 generates all possible derivations H $ e : T | C from the constraint typing rules of Section 6.3. Each one of these derivations has a fixed set C of constraints. Line 3 calls the unification
algorithm. The first argument of unify is the set C and the second one is H for the set of visited

TWO LIGHT MODALITIES FOR RECURSION

29

equality constraints. Line 4 checks that the meta-type is different from ‚8 and ‚n ‚‚8 to exclude the
non-normalizing programs (see Theorem 3.14 in Appendix B). The functions Equal?pT, ‚8 q and
Equal?pT, ‚n ‚ ‚8 q are defined in Algorithm 7. In order to exclude programs that have Lèvy-Longo
trees with K, we can substitute the condition on Line 4 by ‚8-free?pT q which is defined in Algorithm 8 (Appendix B). In order to exclude programs that have Böhm trees with K, we can substitute
the condition on Line 4 by tailfinite?pT q which is defined in Algorithm 9 (Appendix B).
Algorithm 2: Type Inference Algorithm
Function inferpeq
input : e is a closed expression
output: set of pairs xT, E y such that t “ θ pT q and $ e : t for all θ |ù E
1
T ÐH
2
foreach T and C such that H $ e : T | C do
3
foreach xτ, E y P unifypC , Hq do
4
if Equal?pτpT q, ‚8 q and Equal?pτpT q, ‚n ‚ ‚8 q then
T Ð T Y xτpT q, E y;
5

return T

Theorem 6.19 (Completeness of Type Inference). If $ e : t in λ‚‚ and t ­“ ‚8 and t ­– ‚n ‚ ‚8 then
there exists xT, E y P inferpeq such that nf ptq “ σ pT q for some σ “ τ Y θ and θ |ù E .
Proof. This follows from Lemma 6.3, Theorem 6.15 and Theorem 6.17.
Theorem 6.20 (Soundness of Type Inference). If xT, E y P inferpeq then
(1) there exists a natural θ such that θ |ù E and
(2) for all natural θ such that θ |ù E ,
(i) θ pT q “ t is a type always in normal form such that t ­“ ‚8 and t ­“ ‚n ‚ ‚8
(ii) $ e : t in λ‚‚ .
Proof. Suppose xT, E y P inferpeq. It follows from the definition of Algorithm 2 that T “ τpSq for
some H $ e : S | C and xτ, E y P unifypC , Hq.
It is easy to show by induction on the rules of Tables 1 and 2 that C is always positive and
normal. Item 1 follows from Item 1 of Theorem 6.18. In order to prove Item 2, assume that θ |ù E
and take σ “ τ Y θ . It follows from Item 2 of Theorem 6.18 that σ |ù C and σ is an always normal
normal type substitution. By Theorem 6.14, $ e : σ pSq in pλ‚‚ q´ and σ pSq is a type in normal form.
By Lemma 6.3, $ e : σ pSq in λ‚‚ . Then, t “ σ pSq “ θ pτpSqq “ θ pT q is always in normal form since
S is always in normal form and σ is always normal.
6.6. Examples. We now illustrate the type inference algorithm through some examples.
Consider e “ λ x.x. The result of inferpλ x.xq is a set that contains two meta-types:
S1 “ ‚N pX1 Ñ ‚M X1 q
S2 “ ‚N ‚ pX1 Ñ ‚M X1 q
with the implicit set of integer constraints N, M ě 0. These two meta-types cover all solutions, i.e.
any type of e “ λ x.x in λ‚‚ is an instantiation of either S1 or S2 . How are these two meta-types
obtained by the algorithm? We can apply either the rule [ÑI] of Table 1 or [‚ ÑI] of Table 2 which
gives two possible type derivations:

30

PAULA SEVERI

?

?

(1) H $ e : T1 | C1 where T1 “ ‚N pX1 Ñ X2 q and C1 “ tX “ ‚N X1 , X M “ ‚N X2 u. The result of
unifypC1 , Hq is τ1 “ tX ÞÑ ‚N X1 , X2 ÞÑ ‚M X1 u and τ1 pT1 q “ ‚N pX1 Ñ ‚M X1 q “ S1 .
?
?
(2) H $ e : T2 | C2 where T2 “ ‚N ‚ pX1 Ñ X2 q and C2 “ tX “ ‚L X1 , X M “ ‚L X2 u. The result
of unifypC2 , Hq is τ2 “ tX ÞÑ ‚L X1 , X2 ÞÑ ‚M X1 u and τ2 pT2 q “ ‚N ‚ pX1 Ñ ‚M X1 q “ S2 .
Consider now λ x.xx. Then, the result of inferpλ x.xxq is a set that contains four meta-types.
The first meta-type is S1 “ ‚N1 pX1 Ñ ‚N2 ´N1 X4 q where X1 should satisfy the recursive equation:
?

X1 “ ‚N2 ´pN1 `N3 q p‚N1 `N4 ´N2 X1 Ñ X4 q

(6.2)

and the set of integer constraints for S1 is:
E1 “ tN1 ` N4 ě N2 ě N1 ` N3 , N4 ´ N3 ě 1u

(6.3)

The constraints N1 ` N4 ě N2 ě N1 ` N3 guarantee that the exponents of the ‚’s are all positive. The
constraint N4 ´ N3 ě 1 forces the recursive type to be guarded.
The second meta-type is S2 “ ‚N1 p‚N2 ´pN1 `N4 q X3 Ñ ‚N2 ´N1 X4 q where X3 should satisfy the
recursive equation:
?
(6.4)
X3 “ ‚N4 ´N3 pX3 Ñ X4 q
and the set of integer constraints for S2 is:
E2 “ tN2 ą N1 ` N4 , N4 ě N3 , N4 ´ N3 ě 1u

(6.5)

The constraints N2 ą N1 ` N4 and N4 ě N3 guarantee that the exponents of the ‚’s are all positive.
The constraint N4 ´ N3 ě 1 forces the recursive type to be guarded.
The third meta-type is S3 “ ‚N0 ‚ pX1 Ñ ‚N2 ´N1 X4 q where X1 should satisfy the recursive equation in Eq. (6.2) and E3 “ E1 as in Eq. (6.3).
The fourth meta-type is S4 “ ‚N0 ‚ p‚N2 ´pN1 `N4 q X3 Ñ ‚N2 ´N1 X4 q where X3 satisfies the recursive
equation of Eq. (6.4) and E4 “ E2 as in Eq. (6.5).
6.7. Typability and Type Checking. Typability (finding out if the program is typable or not) in
λ‚‚ can be solved by checking whether inferpeq ­“ H. By Theorem 6.19, if inferpeq “ H then
there is no t ­“ ‚8 and t ­– ‚n ‚ ‚8 such that $ e : t in λ‚‚ . By Theorem 6.19, if inferpeq ­“ H then
there exists t ­“ ‚8 and t ­– ‚n ‚ ‚8 such that $ e : t in λ‚‚ .
Type checking for λ‚‚ (given an an expression e and a type t check if $ e : t) can easily be
solved by inferring the (finite) set of meta-types for e and checking whether one of these meta-types
unifies with t.
The type inference algorithm is exponential on the size of the input for two reasons. First, the
number of sets C such that H $ e : T | C is exponential on the size of e (Line 2 of Algorithm 2).
Second, the unification algorithm is also exponential because it branches (cases of Lines 6 and 16
of Algorithm 1). If we are only interested in typability (and not type inference), then the complexity
could be reduced to NP by “guessing the solutions”. We choose the rules of Table 1 and Table 2 nondeterministically and instead of giving the union of the results in Line 11 and Line 19 of Algorithm 1,
we could choose one of the options non-deterministically and call unify only “once”.

TWO LIGHT MODALITIES FOR RECURSION

31

7. R ELATED W ORK
This paper is an improvement over past typed lambda calculi with a temporal modal operator like
‚ in two respects. Firstly, we do not need any subtyping relation as in [23] and secondly programs
are not cluttered with constructs for the introduction and elimination of individuals of type ‚ and ‚
as in [18, 30, 19, 1, 8, 9, 5].
Another type-based approach for ensuring productivity are sized types [15]. Type systems
using size types do not always have neat properties: strong normalisation is gained by contracting
the fixed point operator inside a case and they lack the property of subject reduction [28]. Another
disadvantage of size types is that they do not include negative occurrences of the recursion variable
[15] which are useful for some applications [31].
The proof assistant Coq does not ensure productivity through typing but by means of a syntactic
guardedness condition (the recursive calls should be guarded by constructors) [13, 10] which is
somewhat restrictive since it rules out some interesting functions [30, 9].
A sound but not complete type inference algorithm for Nakano’s type system is presented in
[27]. This means that the expressions typable by the algorithm are also typable in Nakano’s system
but the converse is not true. Though this algorithm is tractable, it is not clear to which type system
it corresponds.
8. C ONCLUSIONS AND F UTURE W ORK
The typability problem is trivial in λ µ because all expressions are typable using µX.pX Ñ Xq. In
λ‚‚ , this problem turns out to be interesting because it gives us a way of filtering programs that do
not satisfy certain properties, i.e. normalization, having a Lèvy-Longo or a Böhm tree without K. It
is also challenging because it involves the generation of integer constraints.
Due to the high complexity of the type inference algorithm, it will be important to find optimization techniques (heuristics, use of concurrency, etc) to make it feasible.
What remains to be done is to give a formal comparision between λ‚‚ and the type systems by
Clouston et al [9] and the one by Atkey et al [2].
It will be interesting to investigate the interaction of these two modal operator with dependent
types. As observed in Section 2, our type system is not closed under η-reduction and this property
may be useful for stablishing a better link with the denotational semantics. We leave the challenge
of attaining a normalising and decidable type system closed under β η-reduction for future research.
Acknowledgments. I am grateful to Mariangiola Dezani-Ciancaglini, the anonymous reviewers of
FOSSSACS 2017 and LMCS for their useful suggestions, which led to substantial improvements.
R EFERENCES
[1] R. Atkey and C. McBride. Productive Coprogramming with Guarded Recursion. In G. Morrisett and T. Uustalu,
editors, proceedings of ICFP’13, pages 197–208. ACM, 2013.
[2] R. Atkey and C. McBride. Productive coprogramming with guarded recursion. In Proceedings of ICFP’13, pages
197–208, 2013.
[3] H. P. Barendregt. The lambda calculus : its syntax and semantics. College Publications, 2012.
[4] L. Birkedal, R. E. Møgelberg, J. Schwinghammer, and K. Støvring. First Steps in Synthetic Guarded Domain
Theory: Step-indexing in the Topos of Trees. Logical Methods in Computer Science, 8(4), 2012.
[5] A. Bizjak, H. B. Grathwohl, R. Clouston, R. E. Møgelberg, and L. Birkedal. Guarded dependent type theory with
coinductive types. In Proceedings of FOSSACS 2016, pages 20–35, 2016.
[6] F. Cardone and M. Coppo. Type inference with recursive types: Syntax and semantics. Inf. Comput., 92(1):48–80,
1991.

32

PAULA SEVERI

[7] F. Cardone and M. Coppo. Recursive types. In H. Barendregt, W. Dekkers, and R. Statman, editors, Lambda Calculus with Types, Perspectives in Logic, pages 377–576. Cambridge, 2013.
[8] A. Cave, F. Ferreira, P. Panangaden, and B. Pientka. Fair Reactive Programming. In S. Jagannathan and P. Sewell,
editors, proceedings of POPL’14, pages 361–372. ACM Press, 2014.
[9] R. Clouston, A. Bizjak, H. B. Grathwohl, and L. Birkedal. Programming and Reasoning with Guarded Recursion
for Coinductive Types. In A. M. Pitts, editor, proceedings of FoSSaCS’15, volume 9034 of LNCS, pages 407–421.
Springer, 2015.
[10] T. Coquand. Infinite Objects in Type Theory. In H. Barendregt and T. Nipkow, editors, proceedings of TYPES’93,
volume 806 of LNCS, pages 62–78. Springer, 1993.
[11] B. Courcelle. Fundamental Properties of Infinite Trees. Theoretical Computer Science, 25:95–169, 1983.
[12] V. Gapeyev, M. Y. Levin, and B. C. Pierce. Recursive subtyping revealed. J. Funct. Program., 12(6):511–548, 2002.
[13] E. Giménez and P. Casterán. A tutorial on [co-]inductive types in coq. Technical report, Inria, 1998.
[14] J. Hughes. Why Functional Programming Matters. Computer Journal, 32(2):98–107, 1989.
[15] J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Proceedings of
POPL’96, pages 410–423, 1996.
[16] J. R. Kennaway, J. W. Klop, M. R. Sleep, and F.-J. de Vries. Infinitary Lambda Calculi and Böhm Models. In RTA,
pages 257–270, 1995.
[17] R. Kennaway, J. W. Klop, M. R. Sleep, and F. de Vries. Infinitary lambda calculus. Theor. Comput. Sci., 175(1):93–
125, 1997.
[18] N. R. Krishnaswami and N. Benton. Ultrametric Semantics of Reactive Programs. In M. Grohe, editor, proceedings
of LICS’11, pages 257–266. IEEE, 2011.
[19] N. R. Krishnaswami, N. Benton, and J. Hoffmann. Higher-order Functional Reactive Programming in Bounded
Space. In Proceedings of POPL’12, pages 45–58. ACM Press, 2012.
[20] A. Kurz, D. Petrisan, P. Severi, and F. de Vries. Nominal coalgebraic data types with applications to lambda calculus.
Logical Methods in Computer Science, 9(4), 2013.
[21] J. Lévy. An algebraic interpretation of the lambda beta - calculus and a labeled lambda - calculus. In LambdaCalculus and Computer Science Theory, Proceedings, pages 147–165, 1975.
[22] G. Longo. Set-theoretical models of lambda calculus: Theories, expansions andisomorphisms. Annals of Pure and
Applied Logic, 1983.
[23] H. Nakano. A Modality for Recursion. In M. Abadi, editor, proceedings of LICS’00, pages 255–266. IEEE, 2000.
[24] C. H. Papadimitriou and K. Steiglitz. Combinatorial optimization : algorithms and complexity. Dover Publications,
Mineola (N.Y.), 1998.
[25] B. C. Pierce. Types and Programming Languages. MIT Press, 2002.
[26] F. Pottier and D. Rémy. The essence of ML type inference. In B. C. Pierce, editor, Advanced Topics in Types and
Programming Languages, pages 389–489. MIT Press, 2005.
[27] R. N. S. Rowe. Semantic Types for Class-based Objects. PhD thesis, Imperial College London, 2012.
[28] J. L. Sacchini. Type-based productivity of stream definitions in the calculus of constructions. In Procedings of LICS
2013, pages 233–242, 2013.
[29] P. Severi. A light modality for recursion. In Proceedings of FOSSACS 2017, pages 499–516, 2017.
[30] P. Severi and F.-J. de Vries. Pure Type Systems with Corecursion on Streams: from Finite to Infinitary Normalisation. In P. Thiemann and R. B. Findler, editors, proceedings of ICFP’12, pages 141–152. ACM Press, 2012.
[31] K. Svendsen and L. Birkedal. Impredicative concurrent abstract predicates. In Proceedings of ESOP 2014, pages
149–168, 2014.

TWO LIGHT MODALITIES FOR RECURSION

33

A PPENDIX A. P ROOF OF T HEOREM 3.13
1
1
Lemma A.1.
(1) Let e ÝÑ
Ş e . Then, e P prtsqi iff e P prtsqi for all i P N and type t.
(2) If k : t P κ, then k P iPN prtsqi .

Proof. (Item 1). By induction on pnboxptq, i, rankptqq.
(Item 2). Using the definition of type intepretation.
Lemma A.2. If ρ |ùi Γ , then ρ |ù j Γ for all j ď i.
Proof. It follows from Item 2 of Lemma 3.9.
Proof of Theorem 3.13.
Proof. We prove that Γ |ùi e : t for all i P N by induction on Γ $ e : t.
Rule [CONST] .
It follows from Item 2 of Lemma A.1.
Rule [‚I] .
Suppose i “ 0. Then,
ρpeq P prtsq0 “ E
Suppose i ą 0 and ρ |ùi Γ1 , ‚Γ2 . If x : s P Γ1 then ρpxq P prssqi Ď prssqi´1 by Item 2 of Lemma 3.9. If
x : ‚s P ‚Γ2 then ρpxq P pr‚ssqi “ prssqi´1 . Hence, ρ |ùi´1 Γ1 , Γ2 . By induction hypothesis, Γ1 , Γ2 |ù j
e : t for all j P N. Hence, ρpeq P prtsqi´1 and
ρpeq P prtsqi´1 “ pr‚tsqi
Rule [‚I] .
ByŞinduction hypothesis, Γ2 |ùi e : t for all i P N. Suppose ρ |ùi Γ1 , ‚Γ2 . This implies that
ρpxq P jěi prssq j for all x : s P Γ2 and hence,
č
ρpeq P prtsq j “ pr‚tsqi
jěi

Rule [–] .
It follows from Lemma 3.10.
Rule [ÑE] .
The derivations ends with the rule:
Γ $ e1 : ‚n ps Ñ tq
Γ $ e2 : ‚n s
Γ $ e1 e2 : ‚nt
with e “ e1 e2 . By induction hypothesis, for all i P N
Γ |ùi e1 : ‚n ps Ñ tq
n

Γ |ùi e2 : ‚ s

(A.1)
(A.2)

We have two cases:
(1) Case i ă n. By Item 1 of Lemma 3.8, pr‚ntsqi “ E. We trivially get
ρpe1 e2 q P pr‚ntsqi
(2) Case i ě n. Suppose that ρ |ùi Γ .
ρpe1 q P pr‚n ps Ñ tqsqi by (A.1)
“ prps Ñ tqsqi´n by Item 2 of Lemma 3.8

(A.3)

34

PAULA SEVERI

ρpe2 q P pr‚n ssqi by (A.2)
“ prssqi´n by Item 2 of Lemma 3.8
By Definition of prps Ñ tqsqi´n and (A.3), there are two possibilities:
(a) Case ρpe1 q P WNx . Then,
ρpe1 e2 q “ ρpe1 qρpe2 q ÝÑ˚ Erxsρpe2 q

(A.4)

(A.5)

Hence,
ρpe1 e2 q P WNx
by (A.5)
n
Ď pr‚ tsqi by Item 1 of Lemma 3.9.
(b) Case ρpe1 q ÝÑ˚ λ x.e1 or ρpe1 q ÝÑ˚ Erks. We also have that
ρpe1 qe2 P prtsqi´n @e2 P prssqi´n
In particular (A.4), implies
ρpe1 e2 q “ ρpe1 qρpe2 q P prtsqi´n
Since prtsqi´n “ pr‚ntsqi by Item 2 of Lemma 3.8, we are done.
Rule [‚Ñ E] .
The derivations ends with the rule:
Γ $ e1 : ‚n ‚ ps Ñ tq
Γ $ e2 : ‚n ‚ s
Γ $ e1 e2 : ‚n ‚ t
with e “ e1 e2 . By induction hypothesis, for all i P N
Γ |ùi e1 : ‚n ‚ ps Ñ tq
n

Γ |ùi e2 : ‚ ‚ s

(A.6)
(A.7)

We have two cases:
(1) Case i ă n. By Item 1 of Lemma 3.8, pr‚n ‚ tsqi “ E. We trivially get
ρpe1 e2 q P pr‚n ‚ tsqi
(2) Case i ě n. Suppose that ρ |ùi Γ .
ρpe1 q P pr‚n ‚ ps Ñ tqsqi by (A.6)
“ pr‚ps
Ş Ñ tqsqi´n by Item 2 of Lemma 3.8
“
jěi´n prps Ñ tqsq j
ρpe2 q P pr‚n ‚ ssqi by (A.7)
“ pr‚ssq
Ş i´n by Item 2 of Lemma 3.8
“
jěi´n prssq j
By Definition of prps Ñ tqsq j and (A.8), there are two possibilities:
(a) Case ρpe1 q P WNx . Then,
ρpe1 e2 q “ ρpe1 qρpe2 q ÝÑ˚ Erxsρpe2 q
Hence,
ρpe1 e2 q P WNx
by (A.10)
Ď pr‚n ‚ tsqi by Item 1 of Lemma 3.9.

(A.8)

(A.9)

(A.10)

TWO LIGHT MODALITIES FOR RECURSION

35

(b) Case ρpe1 q ÝÑ˚ λ x.e1 or ρpe1 q ÝÑ˚ Erks. For all j ě i ´ n, we have that
ρpe1 qe2 P prtsq j @e2 P prssq j
In particular (A.9), implies
ρpe1 e2 q “ ρpe1 qρpe2 q P prtsq j
Since jěi´n prtsq j “ pr‚n ‚ tsqi by Item 2 of Lemma 3.8, we are done.
Rule [ÑI] .
The derivation ends with the rule:
Γ , x : ‚nt $ e : ‚n s
Γ $ λ x.e : ‚n pt Ñ sq
By induction hypothesis, for all i P N
Ş

Γ , x : ‚nt |ùi e : ‚n s

(A.11)

We have two cases:
(1) Case i ă n. By Item 1 of Lemma 3.8, pr‚n pt Ñ sqsqi “ E. We trivially get
ρpλ x.eq P pr‚n pt Ñ sqsqi
(2) Case i ě n. Suppose that ρ |ùi Γ . By Item 2 of Lemma 3.8, it is enough to prove that
ρpλ x.eq P prt Ñ ssqi´n
For this, suppose f P prtsq j for j ď i ´ n. We consider the substitution function defined as
ρ0 “ ρ Y tpx, f qu. We have that
ρ0 |ù j`n Γ , x : ‚nt

(A.12)

because
(a) ρ0 pxq “ f P prtsq j “ pr‚ntsq j`n by Item 2 of Lemma 3.8.
(b) ρ0 |ù j`n Γ by Lemma A.2 and the fact that ρ0 |ùi Γ .
It follows from (A.11) and (A.12) that
ρ0 peq P pr‚n ssq j`n
Therefore, we obtain
pλ x.eq f ÝÑ ρpeqr f {xs “ ρ0 peq P pr‚n ssq j`n by (A.13q
“ prssq j
by Item 2 of Lemma 3.8
By Item 1 of Lemma A.1, we conclude
pλ x.eq f

P prssq j .

(A.13)

36

PAULA SEVERI

A PPENDIX B. AUXILIARY F UNCTIONS FOR THE T YPE I NFERENCE A LGORITHM
This section gives several algorithms (functions) that are used in the unification and type inference
algorithms.
Let treespT q denote the set of subtrees of T and ptreespT q denote the set of proper subtrees
of T . If T is a regular pseudo meta-type then, treespT q and ptreespT q are finite.
B.1. Guardness. Algorithm 3 defines the function guard that given a set C of meta-type constraints returns a set E of integers constraints that guarantees guardedness.
Algorithm 3: Integer constraints to guarantee guardedness
Function guardpC q
input : C is a set of substitutive constraints
output: guardpC q “ E such that θ ˝ τC is guarded iff θ |ù E for all natural θ .
Ť
return XPdompτC q guardpτC pXqq
Function guardpT q
input : T regular pseudo meta-type
output: guardpT q “ E such that θ pT q is guarded iff θ |ù E for all natural θ .
E Ð H;
foreach S P ptreespT q such that S P ptreespSq

/* S “ . . . S . . . */ do

?

E Ð E Y tE ě 1 | E P countpS, Squ
return E
Function countpS, T q
input : S, T regular pseudo meta-types
output: the set of E1 ` . . . ` En such that T “ ‚E1 p. . . p‚En Sq . . .q
if S R ptreespT q then return H;
case T “ S do return t0u;
case T “ ‚E T 1 do return tE ` E 1 | E 1 P countpS, T 1 qu;
case T “ pT1 op T2 q do return countpS, T1 q Y countpS, T2 q;
case T “ ‚T 1 do return countpS, T 1 q;
The function countpS, Sq counts the number of bullets from the root of S to each recursive
occurrence of S, i.e. it gives the set of E1 ` . . . ` En such that S “ ‚E1 p. . . p‚En Sq . . .q In the figure
below, countpS, Sq returns tE1 ` E2 ` E3 , E4 ` E5 u.

E1

E2

E3

S

E4

E5

S

S

TWO LIGHT MODALITIES FOR RECURSION

37

For example,
?

?

(1) Let C “ tX “ ‚N pNat Ñ ‚M Xqu. The set E “ tN ` M ě 1u guarantees that τC is guarded,
i.e. θ ˝ τC is guarded for all θ such that θ |ù E .
?
?
?
(2) Let C “ tX1 “ ‚N1 p‚N2 X1 Ñ ‚N3 X2 q, X2 “ ‚M1 p‚M2 X2 Ñ ‚M3 X3 q, X3 “ ‚K1 p‚K2 X1 Ñ ‚K3 X3 qu.
The set E “ tN1 ` N2 ě 1, N1 ` N3 ` M1 ` M3 ` K1 ` K2 ě 1, M1 ` M2 ě 1, K1 ` K3 ě 1u
enforces that τC is guarded, i.e. i.e. θ ˝ τC is guarded for all θ such that θ |ù E .
B.2. Locality. Algorithm 4 defines the function local? such that local?pC q is true iff τC pXq is
?
local for all X P dompτq. For example, local?pC q is false if C “ tX “ Nat Ñ ‚Xu and it is true if
?
?
C “ tX “ Nat Ñ ‚Y,Y “ Nat Ñ ‚Y u.
Algorithm 4: Checking locality
Function local?pC q
input : C is a substitutive set of constraints
output:Źlocal?pC q is true iff τC is local.
return tlocal?pτC pXqq | X P dompτqu
Function local?pT q
input : T is a regular pseudo meta-type
output: local?pT q is true iff T is local
b Ð true;
foreach S P treespT q do
foreach ‚S1 P treespT q do
if S P treespS1 q then b Ð false;
return b

The justification of the algorithm is shown in the figure below. There exists an infinite path
with an infinite number of ‚ in T iff T contains a subtree S such that S “ . . . p‚p. . . S . . .qq . . ..

S
S'
S

38

PAULA SEVERI

B.3. Other Auxiliary Functions. Algorithm 5 checks whether a given meta-type has certain shape
and Algorithm 6 checks whether two meta-types have the same shape ‘at depth 0’. Algorithm 7 defines two functions for checking whether a meta-type is either equal to ‚8 or to ‚n ‚‚8 . Algorithm 8
checks whether the meta-type is ‚8 -free and Algorithm 9 checks whether the meta-type is tail finite.
Algorithm 5: Checking the shape of the meta-type
Function NatOpBox?pT q
return T “ Nat or T “ S1 op S2 or T “ ‚S

Algorithm 6: Checking that meta-types are equally constructed
Function EqualCons?pT, Sq
return T “ Nat and S “ Nat or T “ X and S “ X or T “ T1 op T2 and S “ S1 op S2 or
T “ ‚T 1 and S “ ‚S1

Algorithm 7: Checking that a meta-type is equal to either ‚8 or ‚n ‚ ‚8
Function Equal?pT, ‚8 q
input : T regular meta-type
output: Equal?pT, ‚8 q is true iff T is different from ‚8 .
if T “ ‚E S and (S “ X or S “ Nat or S “ pt1 Ñ t2 q or S “ pt1 ˆ t2 q or S “ ‚S1 ) then
return false
else return true;
Function Equal?pT, ‚n ‚ ‚8 q
input : T regular meta-type in normal form
output: Equal?pT, ‚n ‚ ‚8 q is true iff T is different from ‚n ‚ ‚8 .
if T “ ‚E ‚ S and (S “ X or S “ Nat or S “ pt1 Ñ t2 q or S “ pt1 ˆ t2 q) then
return false
else return true;

Algorithm 8: Checking that a meta-type is ‚8 -free
Function ‚8-free?pT q
input : T regular meta-type in normal form
output: ‚8-free?pT q is true iff T is ‚8 -free.
foreach S P treespT q do
if Equal?pS, ‚8 q then return false;
return true

TWO LIGHT MODALITIES FOR RECURSION

Algorithm 9: Checking that a meta-type is tail finite
Function tailfinite?pT q
input : T regular meta-type in normal form
output: tailfinite?pT q is true iff T is tail finite.
if ‚8-free?pT q then return false;
E Ð H;
foreach S P ptreespT q such that S P ptreespSq
/* S “ . . . S . . . */ do
if arrowspS, Sq then return false;
return true
Function arrowspS, T q
input : S, T regular pseudo meta-types
output: arrowspS, T q true iff T “ ‚E1 pT1 Ñ . . . pTn Ñ ‚En Sq . . .q
if T “ ‚E pT1 Ñ T2 q and S P ptreespT2 q then return arrowspS, T2 q;
else return false;

39

