Linear Recursion

arXiv:1001.3368v4 [cs.LO] 25 Nov 2016

Sandra Alves1 , Maribel Fernández2 , Mário Florido1 , and Ian Mackie3
1

University of Porto, Faculty of Science & LIACC,
R. do Campo Alegre 1021/55, 4169-007, Porto, Portugal
2
King’s College London, Department of Informatics
Strand, London WC2R 2LS, U.K.
3
LIX, CNRS UMR 7161, École Polytechnique
91128 Palaiseau Cedex, France
Abstract
We define two extensions of the typed linear lambda-calculus that yield minimal Turingcomplete systems. The extensions are based on unbounded recursion in one case, and bounded
recursion with minimisation in the other. We show that both approaches are compatible with
linearity and typeability constraints. Both extensions of the typed linear lambda-calculus
are minimal, in the sense that taking out any of the components breaks the universality of
the system. We discuss implementation techniques that exploit the linearity of the calculi.
Finally, we apply the results to languages with fixpoint operators: we give a compilation of the
programming language PCF into a linear lambda-calculus with linear unbounded recursion.

1

Introduction

Turing completeness is significant in computer science because it is a standard measure of computational power: all general purpose programming languages are Turing complete. There are a
number of Turing-complete models of computation: Turing Machines, the λ-calculus, term rewriting systems, partial recursive functions, etc. We refer to these as computation models rather than
programming languages, as the former can be seen as abstract representations of computing devices, where the emphasis is in the essential notions, whereas the latter include additional features
to make representing data and algorithms easier.
In this paper, we are interested in minimal models of computation that are Turing complete
(or universal). In particular, we contribute to the collection of universal systems based on the
typed λ-calculus, which is a paradigmatic model of functional computation.
There are several approaches to build a Turing complete system starting from a typed λcalculus. To obtain a minimal system, our starting point is the typed linear λ-calculus, and we
add the least machinery needed to obtain a complete system.
The linear λ-calculus [1] is a restriction of the λ-calculus that models linear functions, defined
by syntactically linear terms where each variable occurs exactly once [38]. The linear λ-calculus
captures the essence of functional computation, but it is computationally weak: all the functions
terminate in linear time. In fact, the linear λ-calculus is operationally linear, that is, functions
cannot duplicate or erase arguments during evaluation (see also [8, 41]). Operational linearity has
great impact when the management of resources (copying and erasing of arguments) is important,
as it can be used to efficiently implement garbage collection, for instance. Note however, that
checking if a system is operationally linear relies on evaluation. On the other hand, syntactical
linearity is easy to check, and it is well-known that compilers can make use of this information to
optimise code. Syntactic linearity is relevant in several program analysis techniques, for instance,
strictness analysis, pointer analysis, effects and resource analysis (see, e.g., [16, 22, 56, 54, 55,

1

49, 35, 21]). Linear functions are also relevant in hardware compilation [26]: circuits are static
(i.e., they cannot be copied at run-time), so linear computations are more naturally compiled into
hardware.
Starting from the linear λ-calculus, we define two Turing-complete typed λ-calculi that are
universal and syntactically linear: one is based on bounded iteration and minimisation, and the
other uses unbounded recursion.
In the context of the simply typed λ-calculus, interesting classes of programs can be captured by
extensions of the linear λ-calculus based on bounded iteration (see, e.g., [27, 31, 9, 11, 34, 45, 52]).
In particular, a linear version of Gödel’s System T , which we call System L, captures exactly
the class of primitive recursive functions (PR), if iterators use only closed linear functions [19],
whereas the same system with a closed reduction strategy [23] has all the computation power of
System T [6]. The latter result shows some redundancy regarding duplication in System T , which
can be achieved through iteration or through non-linear occurrences of the bound variable in the
body of a function.
In recursion theory, Turing completeness can be achieved by adding a minimisation operator
to a first-order linear system built from a set of linear initial functions and a linear primitive
recursion scheme [4]. A similar result is shown in this paper for the linear λ-calculus: an extension
of System L with a minimiser, which we call System Lµ , is Turing-complete. In System Lµ , both
iteration and minimisation are needed to achieve completeness.
Alternatively, Turing completeness can be achieved by adding a fixpoint operator to a typed
λ-calculus (as it is done in PCF [51]). This approach has been used to extend linear functional
calculi (see, e.g., [46, 15, 50, 17]), however, it relies on the existence of a non-linear conditional
which throws away a possibly infinite computation in one of the branches.
The question that arises is, what is the minimal extension of the typed linear λ-calculus that
yields a Turing complete system, compatible with the notion of linear function? We show how to
obtain a Turing-complete typed linear λ-calculus through the use of an unbounded recursor with
a built-in test on pairs, which allows the encoding of both finite iteration and minimisation. More
precisely, we define System Lrec , a linear λ-calculus extended with numbers, pairs and a linear
unbounded recursor, with a closed-reduction strategy. We show that Lrec is Turing-complete and
can be easily implemented: we give an abstract machine whose configurations consist simply of a
pair of term and a stack of terms.
System L, System Lrec and System Lµ use a closed-reduction strategy in order to preserve
linearity and accommodate iteration or recursion. This strategy is inspired by the closed cutelimination strategy defined by Girard [29] for proof nets, which was adapted to the λ-calculus
in [23]. Closed cut elimination is a simple and exceptionally efficient strategy in terms of the
number of cut elimination steps. In the λ-calculus, it avoids α-conversion while allowing reductions
inside abstractions (in contrast with standard weak strategies), thus achieving more sharing of
computation. An alternative approach to preserve linearity of systems with iterators or recursors
is to consider a “closed-at-construction” discipline: the function used in a bounded or unbounded
recursor should be closed when the recursor is built (rather than closed at the time of reduction).
In this paper, we consider both approaches and analyse their computational power. Although in
the case of linear calculi with bounded recursion closed reduction and closed construction capture
different classes of functions, we show that both disciplines yield Turing-complete systems in calculi
with unbounded recursion.
Summarising, this paper investigates the relationship between linearity and bounded/unbounded
recursion in typed functional theories, aiming at obtaining minimal Turing complete systems. The
main contributions are:
• We define two extensions of the typed linear λ-calculus: Lrec , a linear calculus with numbers,
pairs and an unbounded recursor, with a closed-reduction strategy; and Lµ , a linear λcalculus extended with numbers, pairs, a bounded recursor and a minimisation operator,
also with a closed-reduction strategy. We show some properties regarding reduction (such
as subject-reduction and confluence), and prove Turing completeness of both systems by
encoding the set of partial recursive functions in Lrec and Lµ . We also show that both systems
2

are minimal, in the sense that taking out any of their components breaks the universality
of the system. Lrec relies only on unbounded recursion, whereas Lµ needs both the iterator
and the minimiser.
• We explore some implementation issues for Lrec : we give call-by-name and call-by-value
evaluation strategies, and define a simple abstract machine, exploiting its linearity.
• We study the interplay between linearity and recursion based on fixpoint combinators, and
define an encoding of PCF into Lrec , which combined with the definition of an abstract
machine for Lrec , gives a new implementation of PCF via a simple stack-based abstract
machine.
• We study the interplay between linearity and closed-reduction/closed-construction disciplines in systems with bounded iteration and in systems with unbounded recursion.
Related Work Extensions of the linear λ-calculus based on bounded iteration capture interesting classes of programs and have been used to characterise complexity classes (see, e.g.,
[27, 31, 9, 11, 34, 45, 52]). However, in this paper we are interested in Turing complete systems,
so bounded iteration is not sufficient.
Several approaches to obtain Turing complete system are described in the literature, inspired by
the work on linear logic [28]. In linear logic, linearity is the default, and copying is obtained by the
use of the “of course” exponential operator (!). To recover the full power of linear logic, the linear
calculi defined in [1, 46, 36] provide explicit syntactical constructs for copying and erasing terms,
corresponding to the exponentials in linear logic. However, adding only copy and erase constructs
to the typed linear λ-calculus does not yield a universal system (see Section 3). In these works,
some form of unbounded recursion (using for instance fixpoint combinators and conditionals) is
also included. Moreover, copy and erase constructs are superfluous once recursion is added: a
PCF-like language with explicit resource management is not minimal (copy and erase constructs
are not needed). Instead, copy and erase can be encoded through bounded or unbounded recursion
as shown in this paper (see also [10, 2, 3]).
Several abstract machines for linear calculi are available in the literature (see for instance [47,
55, 44]). The novelty here is that we implement a calculus that is syntactically linear (in the sense
that each variable is linear in Lrec terms) and therefore there is no need to include in the abstract
machine an environment (or store in the terminology of [55]) to store bindings for variables. As
an application, we give a compilation of the full PCF language into Lrec , establishing a relation
between unbounded recursion and recursion through the use of fixpoint operators.
For Lrec , which combines syntactical linearity with closed reduction, the fragment without
recursion is operationally linear; erasing and duplication can only be done by the recursor (in
linear logic [28] this is done by the use of exponentials, and in other linear calculi [1, 46, 36, 55] by
explicit syntactical constructs). Moreover, only closed terms can be erased or duplicated in Lrec .
There are several other domains where linearity plays a key role. For instance, in the area of
quantum computation, the no-cloning theorem, which states that qubits cannot be duplicated, is
one of the most important results in the area. This property is captured by a linear calculus [53]. In
concurrent calculi, like the π-calculus [48], a key aspect is the notion of name, and the dual role that
names play as communication channels and variables. The linear π-calculus [43] has linear (useonce) channels, which leads to clear gains in efficiency and on program analysis avoiding several
problems of channel sharing. Also, inspired by the works by Kobayashi, Pierce and Turner [43]
and the works by Honda [37] on session types, several type systems for the π-calculus rely directly
on linearity to deal with resources, non-interference and effects [32, 57]. In this paper we focus
on functional computations, and aim at obtaining linear, universal models of computation that
can serve as a basis for the design of programming languages. Our approach is to begin with the
linear λ-calculus, and achieve Turing-completeness in a controlled way.
This paper is an extended and revised version of [7], where Lrec was first defined. Here, we
provide proofs of Subject Reduction, confluence and Turing completeness of Lrec , introduce Lµ ,

3

analyse the power of iteration, minimisation, recursion and fixpoint operators in linear calculi,
and compare the closed-reduction and closed-construction approaches.

2

Preliminaries: Linear Iteration

In this section we recall the definition of System L [6], a linear version of Gödel’s System T (for
details on the latter see [30]). We assume the reader is familiar with the λ-calculus [12].
System L is an extension of the linear λ-calculus [1] with numbers, pairs, and an iterator.
Linear λ-terms t, u, . . . are inductively defined by: x ∈ Λ, λx.t ∈ Λ if x ∈ fv(t), and tu ∈ Λ if
fv(t)∩fv(u) = ∅. Note that x is used at least once in the body of the abstraction, and the condition
on the application ensures that all variables are used at most once. Thus these conditions ensure
syntactic linearity (variables occur exactly once). In System L we also have numbers, generated
by 0 and S, with an iterator:
iter t u v if fv(t) ∩ fv(u) = fv(u) ∩ fv(v) = fv(v) ∩ fv(t) = ∅
and pairs:
ht, ui
let hx, yi = t in u

if fv(t) ∩ fv(u) = ∅
if x, y ∈ fv(u) and

fv(t) ∩ (fv(u) − {x, y}) = ∅

Since λ and let are binders, terms are defined modulo α-equivalence as usual.
Note that, when projecting from a pair, we use both projections. A simple example is the
function that swaps the components of a pair: λx.let hy, zi = x in hz, yi. In examples below we use
tuples of any size, built from pairs. For example, hx1 , x2 , x3 i = hx1 , hx2 , x3 ii and let hx1 , x2 , x3 i =
u in t represents the term let hx1 , yi = u in let hx2 , x3 i = y in t.
System L uses a closed reduction strategy. The reduction rules for System L are given in
Table 1. Substitution is a meta-operation defined as usual, and reductions can take place in any
context.
Name
Beta
Let
Iter0
IterS

Reduction
(λx.t)v
→
let hx, yi = ht, ui in v →
iter 0 u v
→
iter (S t) u v
→

t[v/x]
(v[t/x])[u/y]
u
v(iter t u v)

Condition
fv(v) = ∅
fv(t) = fv(u) = ∅
fv(v) = ∅
fv(v) = ∅

Table 1: Closed reduction in System L
Note that the Iter rules are only triggered when the function v is closed. Thanks to the use
of a closed reduction strategy, iterators on open linear functions are accepted in System L (since
these terms are syntactically linear), and reduction preserves linearity. The closedness conditions
in rules Beta and Let are not necessary to preserve linearity (since variables are used linearly
in abstractions and lets), but they ensure that all the substitutions created during reduction are
closed (thus, there is no need to perform α-conversions during reduction). Normal forms are not
the same as in the λ-calculus (for example, λx.(λy.y)x is a normal form), but closed reduction
is still adequate for the evaluation of closed terms (if a closed term has a weak head normal
form, it will be reached [6]). Closed reduction can also be used to evaluate open terms, using the
“normalisation by evaluation” technique [14] as shown in [23, 24] (in the latter director strings are
used to implement closedness tests as local checks on terms).
System L is a typed calculus. Note that, although linear, some untyped terms are not strongly
normalisable. For instance, ∆∆ where ∆ = λx.iter S 2 0 (λxy.xy) (λy.yx) reduces to itself. However, the linear type system defined in [6] ensures strong normalisation. We recall the type definitions for System L below.

4

Axiom and Structural Rule:
Γ, x : A, y : B, ∆ ⊢ t : C

(Axiom)

x:A⊢x:A

Γ, y : B, x : A, ∆ ⊢ t : C

(Exchange)

Logical Rules:
Γ, x : A ⊢ t : B
Γ ⊢ λx.t : A −◦ B
Γ⊢t:A ∆⊢u:B
Γ, ∆ ⊢ ht, ui : A ⊗ B

Γ ⊢ t : A −◦ B

(−◦Intro)

(⊗Intro)

Γ, ∆ ⊢ tu : B
Γ ⊢t: A⊗B

Numbers:
⊢0:N
Γ⊢t:N

∆⊢u:A

(Zero)

(−◦Elim)

∆, x : A, y : B ⊢ u : C

Γ, ∆ ⊢ let hx, yi = t in u : C

(⊗Elim)

Γ⊢n:N

(Succ)
Γ⊢Sn:N
Θ ⊢ u : A ∆ ⊢ v : A −◦ A

Γ, Θ, ∆ ⊢ iter t u v : A

(Iter)

Table 2: Type System for System L
The syntax of terms in L does not include type annotations, instead we will use a type assignment system based on linear types. The set of linear types is generated by the grammar:
A, B ::= N | A −◦ B | A ⊗ B
where N is the type of numbers. A type environment Γ is a list of type assumptions of the form
x : A where x is a variable and A a type, and each variable occurs at most once in Γ. We write
dom(Γ) to denote the set of variables that occur in Γ.
We write Γ ⊢ t : A if the term t can be assigned the type A in the environment Γ using the
typing rules in Table 2. Note that the only structural rule is Exchange, we do not have Weakening
and Contraction rules: we are in a linear system. For the same reason, the logical rules split the
context between the premises (i.e., the variable conditions in Table 3 are enforced by the typing
rules).
System L has all the power of System T ; we refer to [6] for more details and examples.

3

Towards a Minimal Universal Type System

In this section we will present two universal type systems which extend the linear λ-calculus: Lrec
and Lµ . While Lrec is a linear calculus with an unbounded recursor, Lµ is a linear calculus where
recursion is obtained through iteration and minimisation. We show that both typed calculi are
universal and minimal (in the sense that all their constructors are necessary for the system to be
universal).
We avoid introducing superfluous operators and rules, such as copy and erase combinators.
Indeed, these can be encoded using recursion, as we will show in this section. The reverse is not
true (although in an untyped system, adding copy and erase combinators to the linear λ-calculus
would produce a Turing-complete system). More precisely, the untyped linear λ-calculus extended
with linear pairs and projections, and copy and erase combinators (c and w) with the following
reduction rules:
c t → ht, ti
fv(t) = ∅
w t → (λx.x) f v(t) = ∅
has the computational power of the pure untyped λ-calculus, but the same does not follow if we

5

Construction
0
St
rec t1 t2 t3 t4
x
tu
λx.t
ht, ui
let hx, yi = t in u

Variable Constraint
−
−
fv(ti ) ∩ fv(tj ) = ∅, for i 6= j
−
fv(t) ∩ fv(u) = ∅
x ∈ fv(t)
fv(t) ∩ fv(u) = ∅
x, y ∈ fv(u), fv(t) ∩ fv(u) = ∅

Free Variables (fv)
∅
fv(t)
∪fv(ti )
{x}
fv(t) ∪ fv(u)
fv(t) r {x}
fv(t) ∪ fv(u)
fv(t) ∪ (fv(u) r {x, y})

Table 3: Terms in System Lrec
Name
Rec0
RecS

rec h0, t′ i u v w
rec hS t, t′ i u v w

Reduction
→ u
→ v(rec (wht, t′ i) u v w)

Condition
fv(t′ vw) = ∅
fv(vw) = ∅

Table 4: Closed reduction for recursion
consider typed terms. The typing rules for c and w are:
Γ⊢t:A

Γ⊢t:B

Γ ⊢ c t:A⊗A

Γ ⊢ w t : A −◦ A

Since this system can be encoded in System L (see [6]), which is not Turing complete (all typable
terms are terminating), we conclude that the typed linear λ-calculus with pairs, projections and
the combinators c and w is not universal.
Another way to obtain Turing completeness of typed λ-calculi is via fixpoint operators and
conditionals, as done in PCF [51]. In Section 5 we discuss fixpoints in the presence of linearity
and study the relation between Lrec and PCF.

3.1

Linear Unbounded Recursion

In this section we define Lrec , an extension of the linear λ-calculus [1] with numbers, pairs, and a
typed unbounded recursor with a closed reduction strategy that preserves syntactic linearity. We
prove that this system is Turing complete.
The syntax of System Lrec is similar to that of System L (recalled in Section 2), except that
instead of a bounded iterator we have a recursor working on pairs of natural numbers. Table 3
summarises the syntax of terms in Lrec . We assume Barendregt’s convention regarding names of
free and bound variables in terms (in particular, bound names are different from free names).
The reduction rules for Lrec are Beta and Let, given in Table 1, together with two rules for the
recursor shown in Table 4.
Note that the Rec rules are only triggered when the closedness conditions hold, thus linearity is
preserved by reduction. The conditions on Beta and Let are orthogonal to the linearity issues (as
explained in the previous section, they simply produce a more efficient strategy of reduction) and
do not affect the technical results of the paper (we discuss the role of closed reduction in System
L and System Lrec in more detail in Section 6).
The Rec rules pattern-match on a pair of numbers (the usual bounded recursor works on
a single number). This is because we are representing both bounded and unbounded recursion
with the same operator (as the examples below illustrate), which requires (for a particular n and
function f ) being able to test the value of f (n), and access the value n. An alternative would be
to have an extra parameter of type N in the recursor.

6

Example 1 We illustrate the use of the recursor by encoding some standard functions in System
Lrec .
• Bounded iteration Let I be the identity function λx.x. System L’s iterator can be encoded
in Lrec using the term “iter” defined as follows:
def

“iter” t u v = rec ht, 0i u v I
We will show later that this term has the same behaviour as System L’s iterator.
• Projections and duplication of natural numbers The first and second projection functions on pairs ha, bi of natural numbers can be defined by using the numbers in a recursor.
pr 1
pr 2

=
=

λx.let ha, bi = x in rec hb, 0i a I I
λx.let ha, bi = x in rec ha, 0i b I I

The following function C can be used to copy numbers:
C = λx.rec hx, 0i h0, 0i (λx.let x = ha, bi in hSa, Sbi) I
Other mechanisms to erase and copy numbers in Lrec will be shown later.
• Arithmetic functions We can now define some arithmetic functions that we will use in
the paper.
– add = λmn.rec hm, 0i n (λx.Sx) I;
– mult = λmn.rec hm, 0i 0 (add n) I;
– pred = λn.pr 1 (rec hn, 0i h0, 0i F I)
where F = λx.let ht, ui = C(pr 2 x) in ht, S ui;
– iszero = λn.pr 1 (rec hn, 0i h0, S 0i (λx.C(pr 2 x)) I).
The correctness of these encodings can be easily proved by induction.
• Minimisation The examples above can also be defined in System L, using bounded recursion. Lrec is a more powerful system: it can encode the minimisation operator µf used to
define partial recursive functions. Recall that if f : N → N is a total function on natural
numbers, µf = min{x ∈ N | f (x) = 0}.
Let f be a closed λ-term in Lrec representing a total function f on natural numbers. The
encoding of µf is
M = rec hf 0, 0i 0 (λx.S(x)) F
where F = λx.let hy, zi = C(pr 2 x) in hf (Sy), Szi. We prove the correctness of this encoding
below (see Theorem 2).
We use the same notation for typing judgements in System L and System Lrec , since there will
be no ambiguity. We write Γ ⊢ t : A if the term t can be assigned the type A in the environment Γ
using the typing rules in Table 2, where we replace the rule for the iterator by the following rule:
Γ⊢t:N⊗N

Θ⊢u:A

∆ ⊢ v : A −◦ A Σ ⊢ w : N ⊗ N −◦ N ⊗ N

Γ, Θ, ∆, Σ ⊢ rec t u v w : A
Note that all the terms given in the example above can be typed.
Theorem 1 (Properties of reductions in System Lrec )
1. If Γ ⊢ t : T then dom(Γ) = fv(t).
2. Subject Reduction: Reductions preserve types.
7

(Rec)

3. Church-Rosser: System Lrec is confluent.
4. Adequacy: If ⊢ t : T in System Lrec , and t is a normal form, then:
T =N
T =A⊗B
T = A −◦ B

⇒ t = S(S . . . (S 0))
⇒ t = hu, si
⇒ t = λx.s

5. System Lrec is not strongly normalising, even for typeable terms.
Proof:
1. By induction on type derivations.
2. By induction on type derivations, using a substitution lemma as usual. We show the case
where the term has the form rec ht, t′ i u v w (for the other cases, the proof is the same as
for System L [6]).
Assume Γ ⊢ rec ht, t′ i u v w : A. If the reduction takes place inside t, t′ , u, v or w the
property follows directly by induction. If the reduction takes place at the root, there are
two cases:
(a) rec h0, t′ i u v w → u if fv(t′ vw) = ∅. Then, by part 1, dom(Γ) = fv(rec h0, t′ i u v w) =
fv(u). The type derivation may end with (Exchange), in which case the result is trivial,
or with (Rec), in which case the derivation has conclusion Γ ⊢ rec h0, t′ i u v w : A with
premises: ⊢ h0, t′ i : N ⊗ N, Γ ⊢ u : A, ⊢ v : A −◦ A, ⊢ w : N ⊗ N −◦ N ⊗ N. Therefore
the property holds, directly from Γ ⊢ u : A.
(b) rec hS t, t′ i u v w → v(rec (wht, t′ i) u v w) if fv(vw) = ∅. Reasoning in a similar
way, we note that when the type derivation ends with an application of the rule (Rec),
it has conclusion Γ, ∆ ⊢ rec hSt, t′ i u v w : A with premises Γ ⊢ hSt, t′ i : N ⊗ N,
∆ ⊢ u : A, ⊢ v : A −◦ A, and ⊢ w : N ⊗ N −◦ N ⊗ N. If Γ ⊢ hSt, t′ i : N ⊗ N, then we can
deduce Γ ⊢ ht, t′ i : N ⊗ N, therefore we have Γ ⊢ wht, t′ i : N ⊗ N. Thus we can obtain
Γ, ∆ ⊢ rec (wht, t′ i) u v w : A. From these we deduce Γ, ∆ ⊢ v(rec wht, t′ i u v w) : A as
required.
3. Confluence can be proved directly, using Martin-Löf’s technique (as it was done for System
L, see [2]) or can be obtained as a consequence of Klop’s theorem for orthogonal higher-order
reduction systems [42].
4. By induction on t. If t = 0, λx.t′ or ht1 , t2 i, then we are done. Otherwise:
• If t = S t, it follows by induction.
• If t = rec t0 t1 t2 t3 . Since t is in normal form, so are the terms ti . Since t is typable,
t0 must be a term of type N ⊗ N, and by induction, t0 is a pair of numbers. But then
one of the recursor rules applies (contradiction).
• The cases of application and let are similar.
5. The following term is typable but is not strongly normalisable:
rec hS(0), 0i 0 I (λx.let hy, zi = x in hS(y), zi)
Another non-terminating typable term will be given later, using the encoding of a fixpoint
operator.


8

Γ⊢t:N
Γ ⊢ ht, 0i : N ⊗ N

Θ⊢u:A

∆ ⊢ v : A −◦ A

⊢ I : N ⊗ N −◦ N ⊗ N

Γ, Θ, ∆ ⊢ rec ht, 0i u v I : A
Figure 1: Type derivation for “iter” t u v
The Computational Power of System Lrec
We now prove that System Lrec is Turing complete. Since System L can encode all the primitive recursive functions [2, 6], it suffices to show that System L is a subset of Lrec (therefore Lrec
also encodes primitive recursion), and that one can encode minimisation.
First we show that the encoding of System L’s iterator, defined in Example 1, behaves as
expected. System L is a sub-system of Lrec .
Proposition 1
“iter” t u v →∗ u
“iter” t u v →∗ v(“iter” t1 u v)

if t →∗ 0, fv(v) = ∅
if t →∗ S(t1 ), fv(v) = ∅

Proof:
• If t →∗ 0:
“iter” t u v

def

=

rec ht, 0i u v I →∗ rec h0, 0i u v I → u, if fv(v) = ∅

• If t →∗ S(t1 ):
def

= rec ht, 0i u v I →∗ rec hS(t1 ), 0i u v I
→ v(rec Iht1 , 0i u v I), if fv(t1 v) = ∅

“iter” t u v

def

→ v(rec ht1 , 0i u v I) = v(“iter” t1 u v)

If Γ ⊢ t : N, Θ ⊢ u : A, and ∆ ⊢ v : A −◦ A, then Γ, Θ, ∆ ⊢ rec ht, 0i u v I : A, that is “iter” t u v
is properly typed in System Lrec , as shown in Figure 1.
Corollary 1 System Lrec has all the computation power of System L, thus, any function definable
in System T can be defined in Lrec .
We now show that the encoding of the minimiser given in Section 1 behaves as expected.
Theorem 2 (Minimisation in System Lrec ) Let f be a closed λ-term in Lrec , encoding the
total function f on natural numbers. Consider the term M = rec hf 0, 0i 0 (λx.S(x)) F , with
F = λx.let hy, zi = C(pr 2 x) in hf (Sy), Szi. The term M encodes µf .
Proof: Consider the non-empty sequence S = f (i), f (i + 1), . . . , f (i + n), such that f (i + n) is
the first element in the sequence that is equal to zero. Then
rec hf (Si 0), Si 0i 0 (λx.S(x)) F →∗ Sn 0
We proceed by induction on the length of S.
• Basis: S = f (i). Thus
∗

→

rec hf (Si 0), Si 0i 0 (λx.S(x)) F
rec h0, Si 0i 0 (λx.S(x)) F → 0
9

• Induction: If S = f (i), f (i + 1), . . . , f (i + n), then f (i) > 0, therefore f i reduces to a term
of the form (S t). One easily notice that
∗

→
→∗

(I.H.)
∗

→

rec hf (Si 0), Si 0i 0 (λx.S(x)) F
rec hSt, Si 0i 0 (λx.S(x)) F
S(rec hf (Si+1 0), Si+1 0i 0 (λx.S(x)) F )
S(Sn−1 0) = Sn 0

Now, let j = min{x ∈ N | f (x) = 0}, and consider the sequence f (0), . . . , f (j). One easily notices
that rec hf 0, 0i 0 (λx.S(x)) F →∗ Sj 0. Note that, if there exists no x such that f (x) = 0, then
rec hf 0, 0i 0 (λx.S(x)) F diverges, and so does the minimisation of f .

Corollary 2 System Lrec is Turing complete.
Erasing and Duplicating in Lrec
There are various ways of encoding erasing and duplicating in Lrec . First note that, although
in the linear λ-calculus we are not able to discard arguments of functions, terms are consumed
by reduction. The idea of erasing by consuming is related to the notion of Solvability (see [12],
Chapter 8) as it relies on reduction to the identity. Using this technique, in [2, 6] it is shown that
in System L there is a general form of erasing. In Lrec this technique can be used to erase terms
of type A, where A is a type generated by the grammar: A, B ::= N | A ⊗ B. In the definition
of the erasing function E(t, A) we use a function M(A) to build a term of type A (E and M are
mutually recursive).
Definition 1 (Erasing) If Γ ⊢ t : A, then E(t, A) is defined as follows:
E(t, N)
E(t, A ⊗ B)
E(t, A −◦ B)
and
M(N)
M(A ⊗ B)
M(A −◦ B)
Theorem 3

= rec ht, 0i I I I
= let hx, yi = t in E(x, A)E(y, B)
= E(tM(A), B)
= 0
= hM(A), M(B)i
= λx.E(x, A)M(B)

1. If Γ ⊢ t : T then Γ ⊢ E(t, T ) : B −◦ B, for any type B.

2. M(T ) is closed and typeable: ⊢ M(T ) : T .
3. For any type T , E(M(T ), T ) →∗ I.
4. M(T ) is normalisable.
Proof: The first two parts are proved by simultaneous induction on T , as done for System L [6].
The third part is proved by induction on T .
• If T = N, then M(T ) = 0, and E(0, N) = rec h0, 0i I I I → I.
• If T = A ⊗ B, then M(A ⊗ B) = hM(A), M(B)i, then
E(hM(A), M(B)i, A ⊗ B)

=

let hx, yi = hM(A), M(B)i in E(x, A)E(y, B)
(I.H.)

→ E(M(A), A)E(M(B), B) →∗ II → I
Note that, by induction, E(M(A), A) →∗ I and E(M(B), B) →∗ I.

10

• If T = A −◦ B then M(T ) = λx.E(x, A)M(B), therefore
=
→
(I.H.)
∗

→

E(λx.E(x, A)M(B), A −◦ B)
E((λx.E(x, A)M(B))M(A), B)
E(E(M(A), A)M(B), B)
(I.H.)

E(IM(B), B) → E(M(B), B) →∗ I

The last part is proved by induction on T .



Lrec , unlike System L, is not normalising, and there are terms that cannot be consumed
using the technique described above. There are even normalising terms that cannot be erased
by reduction. For example, consider the following term YN which represents a fixpoint operator
(more details are given in Section 5):
YN = λf.rec hS(0), 0i 0 f (λx.let hy, zi = x in hS(y), zi)
This term is typable (it has type (N −◦ N) −◦ N) and is a normal form (the recursor rules do
not apply because f is a variable). However, the term
E(YN , (N −◦ N) −◦ N) = rec hYN (λx.E(x, N)0), 0i I I I
does not have a normal form. On the positive side, closed terms of type N, or tuples where the
elements are terms of type N, can indeed be erased using this technique. Erasing “by consuming”
reflects the work that needs to be done to effectively dispose of a data structure (where each
component is garbage collected). For arrow types, a different erasing mechanism will be defined
in Section 5.
Theorem 4 Let T be a type generated by the grammar: A, B ::= N | A ⊗ B. If ⊢ t : T and t has
a normal form, then E(t, T ) →∗ I.
Proof: By induction on T .
• If T = N, then E(t, T ) = rec ht, 0i I I I. Since t is normalising, t →∗ v, and by the Adequacy
result (Theorem 1), v = Sn 0, n ≥ 0. Therefore rec ht, 0i I I I →∗ rec hSn 0, 0i I I I →∗ I.
• If T = A ⊗ B: E(t, T ) = let hx, yi = t in E(x, A)E(y, B). Since t is normalisable then,
by Adequacy (Theorem 1), t →∗ v = hu, si. Thus let hx, yi = t in E(x, A)E(y, B) →∗
let hx, yi = hu, si in E(x, A)E(y, B) → E(u, A)E(s, B). By induction hypothesis E(u, A) →∗
I and E(s, B) →∗ I, therefore E(u, A)E(s, B) →∗ II → I.

There is also a mechanism to copy closed terms in Lrec :
Definition 2 (Duplication) Define DA : A −◦ A ⊗ A as:
λx.rec hS(S 0), 0i hM(A), M(A)i F I
where F = (λy.let hz, wi = y in E(z, A)hw, xi).
Theorem 5 If ⊢ t : A then DA t →∗ ht, ti.
Proof: By the definition of →.
DA t

→
→∗
→∗
→∗
→∗

rec hS(S 0), 0i hM(A), M(A)i (λy.let hz, wi = y in E(z, A)hw, ti) I
(λy.let hz, wi = y in E(z, A)hw, ti)2 hM(A), M(A)i
(λy.let hz, wi = y in E(z, A)hw, ti)(E(M(A), A)hM(A), ti)
(λy.let hz, wi = y in E(z, A)hw, ti)hM(A), ti
E(M(A), A)ht, ti →∗ ht, ti

11

3.2

System Lµ : Minimisation vs. Unbounded Recursion

There are two standard ways of extending the primitive recursive functions so that all partial
recursive functions are obtained. One is unbounded minimisation, the other is unbounded recursion. For first-order functions (i.e., functions of type level 1), both methods are equivalent, see for
instance [13]. In this section we extend System L with a minimisation operator – we will refer to
this extension as System Lµ – and establish its relation with System Lrec . Starting from System
L, we add a minimiser with a typing rule
Γ⊢t:N

Θ⊢u:N

∆ ⊢ f : N −◦ N

Γ, Θ, ∆ ⊢ µ t u f : N

(Min)

and two reduction rules:
µ0uf
µ (S t) u f

→ u,
→ µ (f (S u)) (S u) f

fv(f ) = ∅
fv(f tu) = ∅

Theorem 6 (Properties of reductions in System Lµ )
1. If Γ ⊢ t : T then dom(Γ) = fv(t).
2. Subject Reduction: If Γ ⊢ t : T and t −→ t′ then Γ ⊢ t′ : T .
3. System Lµ is confluent: If t −→∗ u and t −→∗ v then there is some term s such that u −→∗ s
and v −→∗ s.
Proof:
1. By induction on the type derivation.
2. Straightforward extension of the proof given for System L in [6], by induction on the type
derivation Γ ⊢ t : T . We show the case where the term t is µ s u f and there is a type
derivation ending in:
Γ⊢s:N

Θ⊢u:N

∆ ⊢ f : N −◦ N

Γ, Θ, ∆ ⊢ µ s u f : N

(Min)

If the reduction step takes place inside s, u or f , the result follows directly by induction. If
reduction takes place at the root, we have two cases:
(a) µ 0 u f → u, with fv(f ) = ∅. Note that f v(µ 0 u f ) = fv(u) = dom(Θ) by part 1, and
we have Θ ⊢ u : N.
(b) µ (S t) u f → µ (f (S u)) (S u) f , with fv(tuf ) = ∅. Then f v(µ (S t) u f ) = ∅, and
we have:
⊢St:N

⊢u:N

⊢ f : N −◦ N

⊢ µ (S t) u f : N

Therefore:

⊢ f : N −◦ N

⊢Su:N

⊢ f (S u) : N

(Min)

⊢u:N
⊢Su:N

⊢ f : N −◦ N

⊢ µ (f (S u)) (S u) f : N

(Min)

3. Using Tait-Martin-Löf’s method (see [12] for more details).

Since System L, and therefore System Lµ , includes all the primitive recursive functions, to
show Turing completeness of System Lµ it is sufficient to show that unbounded minimisation can
be encoded. First, we recall the following result from Kleene [39], which uses the well-known
minimisation operator µ (already mentioned in Example 1).

12

Theorem 7 (The Kleene normal form) Let h be a partial recursive function on Nk . Then,
a number n and two primitive recursive functions f , g can be found such that h(x1 , . . . , xk ) =
f (µg (n, x1 , . . . , xk )) where µg is the minimisation operator on the last argument of g, that is,
µg (n, x1 , . . . , xk ) = min{y | g(n, x1 , . . . , xk , y) = 0}.
As a consequence of Kleene’s theorem, we only have to prove that we can encode minimisation
of primitive recursive functions in order to show Turing-completeness of Lµ , relying on the fact
that primitive recursive functions can be encoded in System L. Below we give the encoding of
minimisation for functions of arity 1 (the extension to functions of arity n > 1 is straightforward).
Theorem 8 (Unbounded minimisation in System Lµ ) If f : N → N is a primitive recursive
function and f is its encoding in System Lµ , then
µf = µ (f 0) 0 f
Proof: Similar to the proof for System Lrec (Theorem 2), considering the non-empty sequence
S = f (i), f (i + 1), . . . , f (i + j), such that f (i + j) is the first element in the sequence that is equal
to zero, and showing (by induction on the length of S) that:
µ (f i) i f →∗ i + j.

Corollary 3 System Lµ is Turing complete.
We can also encode System Lrec into System Lµ , simulating the recursor with iter and µ. Consider
the following term:
f = λn.pr 1 (iter n ht, t′ i (w ◦ pred1 )
where pred1 is such that pred1 hS(t), t′ i = ht, ti. The function f , given n, will produce pr 1 ((w ◦
pred1 )n ht, t′ i). Now consider (µ t 0 f ), which will lead to the following sequence:
µ t 0 f → µ f (1) 1 f → µ f (2) 2 f → µ f (3) 3 f → ... → n
where n is the minimum number such that (w ◦pred1 )n ht, t′ i produces h0, t′′ i. Now, one can encode
rec ht, ti u v w as:
iter (µ t 0 f ) u v
Intuitively, rec hSt, t′ i u v w will iterate v until wht, t′ i is equal to zero, and that µ t 0 f will
count the number of iterations that will actually be necessary, or will go on forever if that never
happens.
System Lµ is a minimal universal system in the sense that the subsystems obtained by taking
out iter and µ, respectively, are not universal. Note that the subsystem without µ corresponds
to System L and is therefore strongly normalising. Also note that, the minimiser cannot replace
bounded iteration, either in recursion theory or in the typed λ-calculus, as we now show.
Partial Recursive Functions without Bounded Iteration
Lemma 1 For any function f (x1 , . . . , xm ), m ≥ 0, defined from the initial functions (0, S and projections) and composition, without using the primitive recursive scheme, there is a constant k such
that, f (n1 , n2 , . . . , nm ) = ni +k or f (n1 , n2 , . . . , nm ) = k, for any given arguments n1 , . . . , nm ∈ N.
Proof: Assume f (x1 , . . . , xm ) is defined by the expression e. We proceed by induction on e: The
base cases (e = 0, e = S(x) and e = pr in (x1 , . . . , xm )) are trivial. Let us consider the composition
case. If e = g(f1 (x1 , . . . , xm ), . . . , fj (x1 , . . . , xm )), where g and fi are previously defined functions,
then by induction hypothesis fi (n1 , . . . , nm ) = ki , where ki = ki or ki = ni + ki for some constant
ki . But then, by induction hypothesis g(k1 , . . . , kj ) = k or ki + k, and the result follows.


13

V is a value
V ⇓V
t ⇓ ht1 , t2 i

V al

s ⇓ λx.u

st⇓V

t1 ⇓ 0 u ⇓ V

rec t u v w ⇓ V

u[t/x] ⇓ V

Rec1

App

t ⇓ ht1 , t2 i (λxy.u)t1 t2 ⇓ V
let hx, yi = t in u ⇓ V

t ⇓ ht1 , t2 i t1 ⇓ S t′

Let

v(rec (wht′ , t2 i) u v w) ⇓ V

rec t u v w ⇓ V

Rec2

Table 5: CBN evaluation for System Lrec
Theorem 9 Minimisation applied to functions in the previous class either returns 0 or is not
defined.
Proof: By the previous lemma, when f (x1 , . . . , xn ) = 0, then either it is the constant function
returning 0, or it returns 0 when the argument xi = 0. In the first case µf returns 0, and in the
second case either i = n and then µf returns 0, or µf diverges.

System Lµ without Iteration
Lemma 2 If ⊢ f : N −◦ N is a term in System Lµ without iter, µ:
f (S t) →∗ S k 0, where k 6= 0
Proof: First note that f (S t) : N, and it is strongly normalisable1 . Therefore, by Adequacy,
f (S t) →∗ Sk 0, for some k ≥ 0. Since f is linear, it cannot erase the S in its argument, therefore
k 6= 0.

Theorem 10 Let ⊢ t : N, ⊢ u : N, ⊢ f : N −◦ N be terms in System Lµ without iter, µ. Then
µ t u f either reduces to a reduct of u, or diverges.
Proof: By Adequacy, t →∗ Sk 0, for some k. If k = 0, then µ 0 u f → u →∗ m, using the first
rule for µ. If k 6= 0 then, using the second rule for µ, the computation diverges because, by the
previous lemma, f (Sk 0) with k 6= 0, will never reduce to 0.

This theorem is stated for closed terms, but is valid also if t →∗ 0 and u is an open term. Otherwise,
if we have open terms the rule for µ will not apply.
Lrec can be seen as a more compact version of System Lµ where the recursor can perform both
bounded iteration or minimisation.

4

Evaluation Strategies for System Lrec

In this section we define two evaluation strategies for System Lrec and derive a stack-based abstract
machine.
Call-by-name The CBN evaluation relation for closed terms in System Lrec is defined in Table 5.
The notation t ⇓ V means that the closed term t evaluates in System Lrec to the value V .
Values are terms of the form 0, St, λx.t and hs, ti, i.e., weak head normal forms (whnf). Note
that System Lrec does not evaluate under a S symbol, since S is used as a constructor for natural
numbers. Also note that no closedness conditions are needed in the evaluation rules for closed
terms. The rule Let is given using application to simplify the presentation (in this way, we will be
able to reuse this rule when we define the call-by-value evaluation relation below).
The evaluation relation · ⇓ · corresponds to standard reduction to weak head normal form.
Recall that a reduction is called standard if the contraction of redexes is made from left-to-right
1 We

are in a proper subset of System L, for which the properties of Strong Normalisation and Adequacy hold [6].

14

(i.e., leftmost-outermost). It is well known that for the λ-calculus [12], the standard reduction is
normalising, that is, if a term has a normal form, then it will be reached. A “standardisation”
result holds for closed terms in Lrec , as the following theorem shows.
Theorem 11 (Standardisation) If ⊢ t : T (i.e., t is a closed term in Lrec ) and t has a whnf, then
t ⇓ V , for some value V .
Proof: We rely on Klop’s result [40, 20], which states that leftmost-outermost reduction is normalising for left-normal orthogonal Combinatory Reduction Systems (CRSs). A CRS is orthogonal if
its rules are left-linear (i.e., the left hand-sides of the rewrite rules contain no duplicated variables)
and non-overlapping (there are no critical pairs). A CRS is left-normal if on the left hand-sides of
the rewrite rules, all the function symbols appear before the variables. The λ-calculus is an example of a left-normal orthogonal CRS, as is System Lrec . Therefore, leftmost-outermost reduction
is normalising for Lrec . The result follows, since CBN performs leftmost-outermost reduction. 
For open terms, the set of weak head normal forms includes not only values but also other
kinds of terms, since, for instance, reduction of an application is blocked if the argument is open.
However, an evaluation procedure can also be defined for open terms using closed reduction, if we
consider all the free variables as constants as shown in [23] (see also [14]).
Call-by-value A call-by-value evaluation relation for System Lrec can be obtained from the
CBN relation by changing the rule for application, as usual.
s ⇓ λx.u

t⇓V′

u[V ′ /x] ⇓ V

st⇓V
There is no change in the Rec and Let rules, since they rely on the App rule. Unlike CBN,
the CBV strategy does not always reach a value, even if a closed term has one (Theorem 11
does not hold for a CBV strategy). For example, recall the term YN in Section 3.1, and consider
(λxy.rec h0, 0i I E(x, N) I)y)(YN I). This term has a value under the CBN strategy, but not under
CBV. In fact, innermost strategies are normalising in an orthogonal system if and only if the
system is itself strongly normalising.

4.1

Stack Machine for System Lrec

Intermediate languages that incorporate linearity have well known implementation advantages
whether in compilers, static analysis, or whenever resources are limited [44, 46, 15, 55]. Inspired
by these previous works, we finish this section by illustrating how simply System Lrec can be
implemented as a stack machine. We show a call-by-name version, but it is straightforward to
modify to other reduction strategies.
The basic principle of the machine is to find the next redex, using a stack S to store future
computations. The elements of the stack are terms in an extension of Lrec that includes the
following additional kinds of terms: LET (x, y, t), REC(u, v, w), REC ′ (n, u, v, w), where x, y are
variables bound in LET (x, y, t) and n, t, u, v, w are Lrec terms.
The configurations of the machine are pairs consisting of a term and a stack of extended terms.
Unlike Krivine’s machine or its variants (see for instance [33, 18, 25]) we do not need to include an
environment (sometimes called store, as in [55]) in the configurations. Indeed, the environment is
used to store bindings for variables, but here as soon as a binding of a variable to a term is known
we can replace the unique occurrence of that variable (the calculus is syntactically linear). In
other words, instead of building an environment, we use “assignment” and replace the occurrence
of the variable by the term.
The transitions of the machine are given in Table 6. For a program (closed term t), the machine
is started with an empty stack: (t, []). The machine stops when no rule can apply.
The use of “assignment” means that there is no manipulation (no copying, erasing, or even
searching for bindings) in environments usually associated to these kinds of implementations.
15

(app)
(abs)
(let)
(pair1)
(rec)
(pair2)
(zero)
(succ)

(st, S)
(λx.u, t : S)
(let hx, yi = t in u, S)
(ht1 , t2 i, LET (x, y, u) : S)
(rec t u v w, S)
(ht1 , t2 i, REC(u, v, w) : S)
(0, REC ′ (t2 , u, v, w) : S)
(S(t1 ), REC ′ (t2 , u, v, w) : S)

⇒
⇒
⇒
⇒
⇒
⇒
⇒
⇒

(s, t : S)
(u[t/x], S)
(t, LET (x, y, u) : S)
(u[t1 /x][t2 /y], S)
(t, REC(u, v, w) : S)
(t1 , REC ′ (t2 , u, v, w) : S)
(u, S)
(v, (rec (wht1 , t2 i) u v w) : S)

Table 6: Stack machine for System Lrec
The correctness of the machine with respect to the CBN evaluation relation is proved in the
usual way: first we show that if a typeable term has a value, the machine will find it (it cannot
remain blocked) and then we show that if the machine starting with a configuration (t, []) stops
at a value, then this value is a reduct of t in the calculus.
Theorem 12 (Completeness) If ⊢ t : T and there is a value V such that t ⇓ V , then (t, []) ⇒∗
(V, []).
Proof: By induction on the evaluation relation, using Subject Reduction (Theorem 1) and the
following property:
If (t, S) ⇒ (t′ , S ′ ) then (t, S ++ S ′′ ) ⇒ (t′ , S ′ ++ S ′′ ).
This property is proved by induction on (t, S). Intuitively, since only the top of the stack is
used to select a transition, it is clear that appending elements at the bottom of the stack does not
affect the computation.

Theorem 13 (Soundness) If ⊢ t : T and (t, []) ⇒∗ (V, []) then t →∗ V .
Proof: First, we define a readback function that converts a machine configuration (t, S) into a
term, by induction on S as follows:
Readback(t, [])
Readback(t, LET (x, y, u) : S)
Readback(t, REC(u, v, w) : S)
Readback(t1 , REC ′ (t2 , u, v, w) : S)
Readback(s, t : S)

=
=
=
=
=

t
Readback(let hx, yi = t in u, S)
Readback(rec t u v w, S)
Readback(rec ht1 , t2 i u v w, S)
Readback(st, S), otherwise

Then, we show that a machine transition does not change the meaning of the configuration: If
(t, S) ⇒ (t′ , S ′ ) then Readback(t, S) →∗ Readback(t′ , S ′ ). To prove this result we distinguish
cases depending on the transition rule applied from Table 6.
If the transition (t, S) ⇒ (t′ , S ′ ) is an instance of the rules (app), (let), (rec) or (pair2), the
result follows trivially since the readback is the same for both configurations: Readback(t, S) =
Readback(t′ , S ′ ).
If the transition (t, S) ⇒ (t′ , S ′ ) is an instance of rule (abs), (pair1), (zero) or (succ) then we
can prove that Readback(t, S) → Readback(t′ , S ′ ) as follows. We observe that by definition of the
readback function, in each of these cases there are terms t1 , t2 such that t1 → t2 , Readback(t, S) =
Readback(t1 , S) and Readback(t′ , S ′ ) = Readback(t2 , S). Finally, by induction on the definition
of the readback function, we show that if t1 → t2 then Readback(t1 , S) → Readback(t2 , S).
Having shown that a single transition (t, S) ⇒ (t′ , S ′ ) is sound, we derive the soundness
of the machine by induction on the length of the transition sequence: If (t, []) ⇒∗ (V, []) then
t = Readback(t, []) →∗ Readback(V, []) = V .


16

·
·
·
⊢ hS(0), 0i : N ⊗ N

·
·
·
⊢ M(A) : A

f : A −◦ A ⊢ f : A −◦ A

·
·
·
⊢ W : N ⊗ N −◦ N ⊗ N

f : A −◦ A ⊢ rec hS(0), 0i M(A) f W : A
⊢ λf.rec hS(0), 0i M(A) f W : (A −◦ A) −◦ A
Figure 2: Type derivation for YA

5

Applications: Fixpoint Operators and PCF

We now study the relation between Lrec and languages with fixpoint operators, in particular PCF.

5.1

The Role of Conditionals

Recursive function definitions based on fixpoint operators rely on the use of a non-linear conditional that should discard the branch corresponding to an infinite computation. For instance, the
definition of factorial:
fact = Y (λf n.cond n 1 (n ∗ f (n − 1)))
relies on the fact that cond will return 1 when the input number is 0, and discard the nonterminating “else” branch. Enabling the occurrence of the (bound) variable, used to iterate the
function (f in the above definition), in only one branch of the conditional is crucial for the definition
of interesting recursive programs. This is why denotational linear versions of PCF [50] allow stable
variables to be used non-linearly but not to be abstracted, since their only purpose is to obtain
fixpoints.
Fixpoint operators can be encoded in System Lrec : recall the term YN in Section 3.1. More
generally, for any type A we define the term
YA = λf.rec hS(0), 0i M(A) f W
where W represents the term (λx.let hy, zi = x in hS(y), zi). For every type A, YA : (A−◦ A)−◦ A
is well-typed in System Lrec (see Figure 2). Note that, for any closed term f of type A −◦ A, we
have:
YA f = rec hS(0), 0i M(A) f W
→∗ f (rec (let hy, zi = h0, 0i in hS(y), zi) M(A) f W )
→ f (rec hS(0), 0i M(A) f W ) = f (YA f )
Although YA behaves like a fixpoint operator, one cannot write useful recursive programs using
fixpoint operators alone (i.e. without a conditional): if we apply YA to a linear function f , we
obtain a non-normalisable term (recall the example in Section 3.1). Instead, in System Lrec ,
recursive functions, such as factorial, can be easily encoded using rec:
λn.pr 2 (rec hn, 0i hS(0), S(0)i (λx.let ht, ui = x in F ) I)
where F = let ht1 , t2 i = DN t in hS t1 , mult u t2 i and DN is the duplicator term defined previously
(see Definition 2). Note that, although conditionals are not part of System Lrec syntax, reduction
rules for rec use pattern-matching. In the remainder of this section we show how we can encode
in System Lrec recursive functions defined using fixpoints.

5.2

Encoding PCF in System Lrec

PCF (Programming Language for Computable Functions) [51] can be seen as a minimalistic typed
functional programming language. It is an extension of the simply typed λ-calculus with numbers,
a fixpoint operator, and a conditional. Let us first recall its syntax. PCF is a variant of the typed
λ-calculus, with a basic type N for numbers and the following constants:
17

• n : N, for n = 0, 1, 2, . . .
• succ, pred : N → N
• iszero : N → N, such that
iszero 0
→ 0
iszero (n + 1) → 1
• for each type A, condA : N → A → A → A, such that
condA 0 u v
condA (n + 1) u v

→ u
→ v

• for each type A, YA : (A → A) → A, such that YA f → f (YA f ).
Definition 3 PCF types and environments are translated into System Lrec types using h ·ii:
h Nii
h A → Bii
h x1 : T1 , . . . , xn : Tn i

=
=
=

N
h Aii −◦ h Bii
x1 : h T1 i , . . . , xn : h Tn i

Since System Lrec is Turing complete, it can simulate any PCF program. Furthermore, it is possible
to define an encoding in System Lrec for all the terms in PCF. We give a definition below, which is
inspired by the encoding of System T [6]. For convenience, we make the following abbreviations,
where the variables x1 and x2 are assumed fresh, and [x]t is defined below:
x1 ,x2
t
Cx:A
Axy t

= let hx1 , x2 i = DA x in t
= ([x]t)[y/x]

Definition 4 Let t be a PCF term such that f v(t) = {x1 , . . . , xn } and x1 : A1 , . . . , xn : An ⊢ t : A.
2
An
1
The compilation into System Lrec , is defined as: [xA
1 ] . . . [xn ]hhtii , where h ·ii is defined in Table
7, and for a term t and a variable x, such that x ∈ fv(t), [x]t is inductively defined in the following
way:
[x](S u)
= S([x]u)
[x]x
= x
[x](λy.u) = λy.[x]u
 x ,x
1
2
x
x

Cx:A (Ax1 s)(Ax2 u) x ∈ fv(s) ∩ fv(u)
[xA ](su) =
([x]s)u
x∈
/ fv(u)


s([x]u)
x∈
/ fv(s)

Notice that [x]t is not defined for the entire syntax of System Lrec . The reason for this is
that, although other syntactic constructors (like recursors or pairs) may appear in t, they are the
outcome of h ·ii and therefore are closed terms, where x does not occur free.
Some observations about the encoding follow.
First, we remark that succ is not encoded as λx.Sx, since Lrec does not evaluate under λ or S.
We should not encode a divergent PCF program into a terminating term in Lrec . In particular,
the translation of condA (succ(YN I)) P Q is h condA i (hhsuccii(hhYN i I)) h P i h Qii, which diverges (if
we encode succ as λx.Sx, then we obtain h Qii, which is not right).
Regarding abstractions or conditionals, the encoding is different from the one used in for
System T in [6]. We cannot use the same encoding as in System L, where terms are erased by
“consuming them”, because PCF, unlike System T , is not strongly normalising. The technique
used here for erasing could have been used for System L, but erasing “by consuming” reflects the
work needed to erase a data structure.
2 We

omit the types of variables when they do not play a role in the compilation.

18

h nii
h succii
h predii
h iszeroii
h YA i
h condA i
h xii
h uvii

=
=
=
=
=
=
=
=

h λxA .tii

=

Sn 0
λn.rec hn, 0i (S 0) (λx.Sx) I
λn.pr 1 (rec hn, 0i h0, 0i (λx.let ht, ui = DN (pr 2 x) in ht, S ui) I)
λn.pr 1 (rec hn, 0i h0, S 0i (λx.DN (pr 2 x)) I)
λf.rec hS(0), 0i M(hhAii) f (λx.let hy, zi = x in hS(y), zi)
λtuv.rec ht, 0i u (λx.(rec h0, 0i I E(x, h Aii) I)v) I
x
h(uiih vii
λx.[xA ]hhtii
if x ∈ fv(t)
λx.(rec h0, 0i I λy.E(E(y, h Bii −◦ h Bii)x, h Aii) I)hhtii otherwise
Table 7: PCF compilation into Lrec

t : N ⊢ ht, 0i : N ⊗ N

u : h Aii ⊢ u : h Aii

v : h Aii ⊢ V : h Aii −◦ h Aii

⊢ I : N ⊗ N −◦ N ⊗ N

t : N, u : h Aii, v : h Aii ⊢ rec ht, 0i u V I : h Aii
·
·
·
⊢ condA : N −◦ h Aii −◦ h Aii −◦ h Aii
Figure 3: Type derivation for condA
The second case in the encoding for abstractions (see Table 7) uses a recursor on zero to
discard the argument, where the function parameter is λy.E(E(y, h Bii −◦ h Bii)x, h Aii). The reason
for this is that one cannot use x directly as the function parameter because that might make the
term untypable, and just using E(x, h Aii) would make the types work, but could encode strongly
normalisable terms into terms with infinite reduction sequences (because E(x, h Aii) might not
terminate). For example, consider the encoding of (λxy.y)YN .
The translation of a typable PCF term is also typable in System Lrec (this is proved below). In
particular, for any type A, the term h condA i is well-typed. In Figure 3, we show the type derivation
for the encoding of the conditional (we use V to represent the term λx.(rec h0, 0i I E(x, h Aii) I)v).
The type derivation for V depends on the fact that, if Γ ⊢ t : A, then for any type B, we have
Γ ⊢ E(t, A) : B −◦ B by Theorem 3. Note that the recursor on h0, 0i in V discards the remaining
recursion (corresponding to the branch of the conditional that is not needed), returning Iv.
We prove by induction that the encoding respects types. To make the induction work, we need
to define and intermediate system where certain variables (not yet affected by the encoding) may
occur non-linearly. More precisely, we consider an extension to System Lrec , which allows variables
on a certain set X to appear non-linearly in a term. We call the extended system System L+X
rec ;
and it is defined by the rules in Table 8. Intuitively, if X is the set of free-variables of t, then h tii
will be a System Lrec term, except for the variables X = fv(t), which may occur non-linearly, and
[x1 ] . . . [xn ]hhtii, will be a typed System Lrec term. We can prove the following results regarding
System L+X
rec .
′

Lemma 3 If Γ ⊢+X t : A, where dom(Γ) = fv(t) and x ∈ X ⊆ fv(t), then Γ ⊢+X [x]t : A, where
X ′ = X \ {x}.
Proof: By induction on t, using the fact that x : A ⊢+∅ DA x : A ⊗ A. We show the cases for
variable and application.
• t ≡ x. Then [x]x = x, and using the axiom we obtain both x : A ⊢+{x} x : A and
x : A ⊢+∅ x : A.
• t ≡ uv, and x ∈ fv(u), x ∈
/ fv(v) (the case where x ∈
/ fv(u), x ∈ fv(v) is similar). Then
[x]uv = ([x]u)v and Γ ⊢+X uv : A. Let Γ1 = Γ|fv(u) and Γ2 = Γ|fv(v) . Then Γ1 ⊢+X u :
19

Axiom and Structural Rule:
x : A ⊢+X x : A
Γ ⊢+X t : B
Γ, x : A ⊢

and x ∈ X
+X

Γ, x : A, y : B, ∆ ⊢+X t : C

(Axiom)

Γ, y : B, x : A, ∆ ⊢+X t : C
Γ, x : A, x : A ⊢+X t : B

(Weakening)

t:B

(Exchange)

Γ, x : A ⊢

+X

and x ∈ X
t:B

(Contraction)

Logical Rules:
Γ, x : A ⊢+X t : B
Γ ⊢+X λx.t : A −◦ B

(−◦Intro)

Γ ⊢+X1 t : A ∆ ⊢+X2 u : B
Γ, ∆ ⊢+(X1 ∪X2 ) ht, ui : A ⊗ B

(⊗Intro)

Γ, ∆ ⊢+(X1 ∪X2 ) tu : B
Γ ⊢+X1 t : A ⊗ B

Numbers:
⊢
Γ ⊢+X1 t : N ⊗ N

+∅

0:N

∆ ⊢+X2 u : A

Γ ⊢+X1 t : A −◦ B

(Zero)

(−◦Elim)

x : A, y : B, ∆ ⊢+X2 u : C

Γ, ∆ ⊢+(X1 ∪X2 ) let hx, yi = t in u : C
Γ ⊢+X t : N
Γ ⊢+X S(t) : N

(⊗Elim)

(Succ)

Θ ⊢+X2 u : A ∆ ⊢+X3 v : A −◦ A Σ ⊢+X4 w : N ⊗ N −◦ N ⊗ N
Γ, Θ, ∆, Σ ⊢+(X1 ∪X2 ∪X3 ∪X4 ) rec t u v w : A

(Rec)

Table 8: Typing rules for System L+X
rec
B −◦ A and Γ2 ⊢+X v : B, where Γ1 and Γ2 can only share variables in X. By induction
′
hypothesis Γ1 ⊢+X [x]u : B −◦ A. Also, since x ∈
/ fv(v) and dom(Γ2 ) = fv(v), we have
′
′
Γ2 ⊢+X v : B. Therefore Γ ⊢+X (x[u])v : A.
• t ≡ uv, x ∈ fv(u), and x ∈ fv(v). Let Γ1 = Γ|fv(u)\{x} and Γ2 = Γ|fv(v)\{x} and assume C
is the type associated to x in Γ. Then Γ1 , x : C ⊢+X u : B −◦ A and Γ2 , x : C ⊢+X v : B.
′
′
By induction hypothesis Γ1 , x : C ⊢+X [x]u : B −◦ A, and Γ2 , x : C ⊢+X [x]v : B. Thus
+X ′
+X ′
Γ1 , x1 : C ⊢
([x]u)[x1 /x] : B −◦ A, and Γ2 , x2 : C ⊢
([x]v)[x2 /x] : B. Therefore
′
Γ1 , x1 : C, Γ2 , x2 : C ⊢+X (Axx1 u)(Axx2 v) : A. Also x : C ⊢+∅ Dx : C ⊗ C, therefore
′
Γ1 , Γ2 , x : C ⊢+X let hx1 , x2 i = Dx in (Axx1 u)(Axx2 v) : A.

Lemma 4 If t is a PCF term of type A, then h Γ|fv(t) i ⊢+fv(t) h tii : h Aii where the notation Γ|X is
used to denote the restriction of Γ to the variables in X.
Proof: By induction on the PCF type derivation for t, as done for System T in [6].

Theorem 14 If t is a PCF term of type A under a set of assumptions Γ for its free variables
{x1 , . . . , xn }, then h Γ|fv(t) i ⊢ [x1 ] . . . [xn ]hhtii : h Aii
Proof: By induction on the number of free variables of t, using Lemmas 3 and 4.



Using the encodings given above, it is possible to simulate the evaluation of a PCF program
in System Lrec . More precisely, if t is a closed PCF term of type N, which evaluates to V under a

20

V is a value

s ⇓PCF V ′

V ⇓PCF V

V ′ t ⇓PCF V

u[t/x] ⇓PCF V

s is not a value

(λx.u) t ⇓PCF V

s t ⇓PCF V

t ⇓PCF 0

t ⇓PCF n + 1

t ⇓PCF n

t ⇓PCF 0

t ⇓PCF n + 1

pred t ⇓PCF 0

pred t ⇓PCF n

succ t ⇓PCF n + 1

iszero t ⇓PCF 0

iszero t ⇓PCF 1

t ⇓PCF 0 u ⇓PCF V
condA t u v ⇓PCF V

t ⇓PCF n + 1

v ⇓PCF V

f (YA f ) ⇓PCF V

condA t u v ⇓PCF V

YA f ⇓PCF V

Table 9: CBN evaluation for PCF
CBN semantics for PCF [51], then the encoding of t reduces in System Lrec to the encoding of V ,
and evaluates under a CBN semantics to a value which is equal to the encoding of V . In Table 9
we recall the CBN rules for PCF: t ⇓PCF V means that the closed term t evaluates to the value V
(a value is either a number, a λ-abstraction, a constant, or a partially applied conditional).
Lemma 5 (Substitution) Let t be a term in System Lrec .
1. If x ∈ fv(t), and fv(u) = ∅, then h tii[hhuii/x] = h t[u/x]ii
2. If x ∈ fv(t), then ([x]t)[u/x] →∗ t[u/x].
Proof: By induction on t.



Lemma 6 Let t be a closed PCF term. If t ⇓PCF V , then h tii →∗ h V i .
Proof: By induction on the evaluation relation, using a technique similar to the one used for
System T in [6]. Here we show the main steps of reduction for condA t u v where u, v are closed
terms by assumption.
• If t ⇓PCF 0:
h condA t u vii

=

h condA i h tii h uii h vii

(I.H.)
∗

→

condA 0 h uii h vii

→∗

h uii →∗ h V i

(I.H.)

• If t ⇓PCF n + 1, let v ′ be the term (λx.(rec h0, 0i I E(x, A) I)hhvii):
h condA t u vii

=
→∗

h condA i (Sn+1 0) h uii h vii
rec hSn+1 0, 0i h uii v ′ I

→∗

Ihhvii → h vii →∗ h V i .

(I.H.)

For application, we rely on the substitution lemmas above. Note that for an application uv, where
u is a constant, we rely on the correctness of the encodings for constants, which can be easily
proved by induction. For example, in the case of succ it is trivial to prove that, if t is a number
Sn 0 in Lrec (n ≥ 0), then rec ht, 0i (S 0) (λx.Sx) I →∗ Sn+1 0.

Theorem 15 Let t be a closed PCF term. If t ⇓PCF V , then ∃V ′ such that h tii ⇓ V ′ , and
V ′ =Lrec h V i .
Proof: By Lemma 6, t ⇓PCF V implies h tii →∗ h V i . By Theorem 11, h tii ⇓ V ′ . Therefore, since

⇓ ⊂→∗ and the system is confluent (Theorem 1), V ′ =Lrec h V i .

21

Lemma 7 If t ⇓ V and t =Lrec u, then u ⇓ V ′ and V =Lrec V ′ .
Proof: By transitivity of the equality relation.



Theorem 16 Let t be a closed PCF term. If h tii ⇓ V , then ∃V ′ , such that, t ⇓PCF V ′ and
h V ′ i =Lrec V .
Proof: By induction on the evaluation relation, using Lemma 7. Note that, if t is a value
different from a partially applied conditional, the result follows because t = V ′ and h tii is also
a value, i.e. h tii = V , therefore h tii = h V ′ i = V . If t is an application uv then h tii = h uiih vii,
therefore h uiih vii ⇓ V if h uii ⇓ λx.s and s[hhvii/x] ⇓ V . If h uii ⇓ λx.s, then by I.H. u ⇓PCF W , and
h W i =Lrec λx.s. Note that W is a value of arrow type, which compilation equals an abstraction,
therefore W = λx.s′ , pred, succ, iszero, Y, cond, cond p or cond p q.
• If W = λx.s′ , we have two cases:
– x ∈ fv(s′ ): then h W i = λx.[x]hhs′ i =Lrec λx.s, thus [x]hhs′ i =Lrec s. Since s[hhvii/x] ⇓ V
and s[hhvii/x] =Lrec [x]hhs′ i [hhvii/x] then, by Lemma 5.2 [x]hhs′ i [hhvii/x] →∗ h s′ i [hhvii/x],
which, by Lemma 5.1, equals h s′ [v/x]ii, therefore (by Lemma 7) h s′ [v/x]ii ⇓ V ′′ , and
V =Lrec V ′′ . By I.H., s′ [v/x] ⇓PCF V ′ and h V ′ i = V , therefore uv ⇓PCF V ′ and
h V ′ i =Lrec V ′′ =Lrec V .
– x ∈
/ fv(s′ ): let v ′ represent the term λy.E(E(y, h Bii −◦ h Bii)x, h Aii). Then h W i =
λx.(rec h0, 0i I v ′ I)hhs′ i =Lrec λx.s, therefore (rec h0, 0i I v ′ I)hhs′ i =Lrec s. Note that
s[hhvii/x] = (rec h0, 0i I v ′ [hhvii/x] I)hhs′ i and (rec h0, 0i I v ′ [hhvii/x] I)hhs′ i ⇓ V if h s′ i ⇓ V ,
then, since s′ [v/x] = s′ , by I.H., s′ ⇓PCF V ′ and h V ′ i =Lrec V , therefore uv ⇓PCF V ′ and
h V ′ i =Lrec V as required.
• W = succ: then h W i = λx.rec hx, 0i S 0 (λx.Sx) I =Lrec λx.s, then rec hx, 0i S 1 (λx.Sx) I =Lrec
s. Then s[hhvii/x] = rec hhhvii, 0i S 0 (λx.Sx) I and s[hhvii/x] ⇓ V if h vii ⇓ W ′ , in which case we
have two possibilities:
– W ′ = 0: then rec hhhvii, 0i S 0 (λx.Sx) I ⇓ V if S 0 ⇓ V , in which case V = S 0. By I.H.,
v ⇓PCF W ′′ , and h W ′′ i =Lrec 0, therefore W ′′ = 0 (0 is the only value of type N that
compiles to 0). Therefore succ v ⇓PCF 1 and h 1ii = S 0 =Lrec V .
– W ′ = Sp: then rec hhhvii , 0i S 0 (λx.Sx) I ⇓ V if (λx.Sx)(rec hp, 0i S 0 (λx.Sx) I) ⇓ V .
By I.H., v ⇓PCF W ′′ , and h W ′′ i =Lrec Sp, thus W ′′ = n+1 (W ′′ is a number in PCF and it
must different from 0, otherwise its compilation would be 0) and p =Lrec Sn 0. Note that
(λx.Sx)(rec hSn 0, 0i S 0 (λx.Sx) I) →∗ Sn+2 0, therefore, by Lemma 7, V =Lrec Sn+2 0.
Now it suffices to notice that succ v ⇓PCF n + 2, and h n + 2ii = Sn+2 0 =Lrec V as
required.
• For pred and iszero, the proof is similar to the case of succ.
• If W = YA : let w′ represent the term (λy.let hy1 , y2 i = y in hS(y1 ), y2 i). Then h W i =
λx.rec hS(0), 0i M(hhAii) x w′ =Lrec λx.s, therefore rec hS(0), 0i M(hhAii) x w′ =Lrec s. Then,
since s[hhvii/x] = rec hS(0), 0i M(hhAii) h vii w′ , s[hhvii/x] ⇓ V if h vii(hhYA i h vii) ⇓ V (and
h vii(hhYA i h vii) = h v(YA v)ii). Thus, by I.H. v(YA v) ⇓PCF V ′ and h V ′ i =Lrec V , therefore
YA v ⇓PCF V ′ and h V ′ i =Lrec V as required.
• W = condA : let v ′ represent the term (λz.(rec h0, 0i I E(z, h Aii) I)q). Then h W i =
λxpq.rec hx, 0i p v ′ I =Lrec λx.s, therefore λpq.rec hx, 0i p v ′ I =Lrec s. Then s[hhvii/x] =
λpq.rec hhhvii , 0i p v ′ I and s[hhvii/x] ⇓ λpq.rec hhhvii , 0i p v ′ I. Note that condA v ⇓PCF condA v,
because it is a value, and h condA vii =Lrec λpq.rec hhhvii, 0i p v ′ I.

22

• W = condA p1 : let v ′ represent the term (λz.(rec h0, 0i I E(z, h Aii) I)q). Then h W i =
(λpxq.rec hp, 0i x v ′ I)hhp1 i =Lrec λxq.rec hhhp1 i , 0i x v ′ I =Lrec λx.s, therefore
λq.rec hhhp1 i , 0i x v ′ I =Lrec s. Then s[hhvii/x] = λq.rec hhhp1 i , 0i h vii v ′ I and s[hhvii/x] ⇓
λq.rec hhhp1 i , 0i h vii v ′ I. Note that condA p1 v ⇓PCF condA p1 v, because it is a value, and
h condA p1 vii =Lrec λy.rec hhhp1 i , 0i h vii v ′ I.
• W = condA p1 p2 : let v ′ represent the term (λz.(rec h0, 0i I E(z, h Aii) I)x). Then h W i =
(λpqx.rec hp, 0i q v ′ I)hhp1 i h p2 i =Lrec λx.rec hhhp1 i , 0i h p2 i v ′ I =Lrec λx.s, therefore s =Lrec
rec hhhp1 i , 0i h p2 i v ′ I. Then s[hhvii/x] = rec hhhp1 i , 0i h p2 i v ′ [hhvii/x] I and s[hhvii/x] ⇓ V if
h p1 i ⇓ W ′ , in which case we have two possibilities:
– W ′ = 0: then rec hhhp1 i , 0i h p2 i v ′ [hhvii/x] I ⇓ V if h p2 i ⇓ V . By I.H., p1 ⇓PCF W ′′ , and
h W ′′ i =Lrec 0, therefore W ′′ = 0 (0 is the only value of type N that compiles to 0). Also
by I.H, p2 ⇓PCF V ′ and h V ′ i =Lrec V , therefore condA p1 p2 v ⇓PCF V ′ , thus uv ⇓PCF V ′ ,
and h V ′ i =Lrec V as required.
– W ′ = Sp′ : then rec hhhp1 i , 0i h p2 i v ′ [hhvii/x] I ⇓ V if h vii ⇓ V . By I.H., p1 ⇓PCF W ′′ ,
and h W ′′ i =Lrec Sp′ , thus W ′′ = n + 1 (W ′′ is a number in PCF and it must different
from 0, otherwise its compilation would be 0). Also by I.H, t ⇓PCF V ′ and h V ′ i =Lrec V ,
therefore condA p1 p2 v ⇓PCF V ′ and h V ′ i =Lrec V as required.

This completes the proof of soundness and completeness of the encoding.
Note that the terms of the form rec h0, 0i I t I used in the encoding of conditionals and λabstractions allow us to discard terms without evaluating them. This is a feature of the encoding,
otherwise terminating programs in PCF could be translated to non-terminating programs in System Lrec . This differs from the definition of erasing given in Section 3.1, where terms are consumed
and not discarded (in pure linear systems functions do not discard their arguments). However,
allowing terms to be discarded without being evaluated, is crucial when defining recursion based
on fixpoints.
Once a PCF term is compiled into Lrec it can be implemented using the techniques in Section
4, thus we obtain a new stack machine implementation of PCF.

6

Closed Reduction vs Closed Construction in Calculi with
Recursion

Both System L and System Lrec use a closed reduction strategy that waits for arguments to
become closed before firing redexes. We now look in more detail at the implications of using a
closed reduction strategy, instead of imposing functions used in iteration/recursion to be closedby-construction (a viable alternative in the presence of linearity).
As mentioned in the Introduction, the closed reduction strategy for the λ-calculus avoids
α-conversion while allowing reductions inside abstractions, thus achieving more sharing of computation. When applied to System L and System Lrec , it imposes certain conditions on reduction
rules; in particular iterated functions should be closed. The intuition here is that we should only
copy closed terms because then all the resources are there. In linear logic words, we can promote
a term that is closed.
The closed reduction strategy waits, to reduce an iterator/recursor term, until the iterated
functions are closed. One can ask a stronger constraint on the construction of terms, that is, to
constrain iterators/recursors to be closed on construction (i.e., we have a syntactical constraint
that only terms without free variables are used in this context). For System L, to follow the
closed-construction approach one imposes an extra condition on the iterated function v, when
defining iterators:
iter t u v
if fv(t) ∩ fv(u) = ∅ and fv(v) = ∅

23

For System Lrec , one imposes an extra condition on v and w:
rec t u v w,

if fv(t) ∩ fv(u) = ∅ and fv(vw) = ∅

In the rest of this section we compare the computation power of linear calculi with closed
reduction vs closed construction. We consider first calculi with bounded recursion (iterators) and
then unbounded recursion.

6.1

Closed Reduction/Closed Construction and Iteration

Dal Lago [19] defines a linear λ-calculus with bounded iteration that encodes exactly the set
of primitive recursive functions following the closed construction approach. A similar system
allowing iterators to be open at construction, but imposing a closed condition on reduction, allows
to encode more than the primitive recursive functions, and in particular allows the encoding of
the Ackermann function, as shown in [5]. Thus, imposing a closed-at-construction restriction on
iterators clearly has an impact in the presence of linearity.
For Gödel’s System T , the fact that we do not allow iterators to be open at construction,
does not affect the set of definable functions. If we define v = λxy.y(xy), then each iterator term
iter n b f in System T , where f may be an open term, can be translated into the typable term
(iter n (λx.b) v)f , where x 6∈ fv(b). It is easy to see that iter n b f and (iter n (λx.b) v)f have the
same normal form f (. . . (f b)). It is worth remarking that we rely on a non-linear term v to get
this result. Indeed, iterating v is essentially equivalent to constructing a Church numeral.
For a linear system with iteration such as System L, although some functions are naturally
defined using an open function, for example: mult = λmn.iter m 0 (add n), one can encode them
using a closed-at-construction iteration. In general, an iterator with an open function where the
free variables are of type N can be encoded using a closed-at-construction iterator, as follows.
Consider iter t u v, where v is open, for free variables x1 , . . . , xn of type N. Then let
F
W

≡
≡

let Cx′1 = hx1 , x′′1 i in . . . let Cxk = hxk , x′′k i in hvx0 , x′′1 , x′′k i
λx.let x = hx0 , x′1 , x′k i in F

Then we simulate iter t u v using a closed iterator as follows: π1 (iter t hu, x1 , xk i W ).
This technique can also be applied to open functions where the free variables are of type τ , for
τ generated by the following grammar: τ ::= N | τ ⊗ τ . More generally, open functions where the
free variables have base type can be encoded when we consider iteration closed-at-construction.

6.2

Closed Construction and Unbounded Recursion

We now consider what happens when we use the closed-at-construction approach in a linear system
with unbounded recursion such as System Lrec .
Notice that the encoding of µf in Lrec given in Section 3.1 is a term closed-at-construction. Since
all the primitive recursive functions are definable using closed-at-construction iterators, which are
trivially encoded using closed Lrec recursors, we conclude that imposing a closed-at-construction
condition on System Lrec still gives a Turing complete system.
Note however that, although System Lrec can encode all the computable functions, that does
not mean one can encode all the computational behaviours. For example for any closed function
f , one can encode in Lrec a term Y , such that, Y f → f (Y f ). However, this relies on the fact that
one can copy any closed function f , which can be done both in System L and System Lrec with
closed reduction, but so far there is no known encoding when one imposes a closed-at-construction
condition.

7

Conclusions

This paper completes a line of work investigating the power of linear functions, from the set
of primitive recursive functions to the full set of computable functions, with a strong focus on
24

Turing complete systems based on linear calculi. In previous work, we investigated linear primitive
recursive functions, and a linear version of Gödel’s System T . Here, we extended these notions to
general recursion, using iteration and minimisation (Lµ ) and, alternatively, unbounded recursion
(Lrec ). System Lrec is a syntactically linear calculus, but only the fragment without the recursor is
operationally linear. The linear recursor allows us to encode duplicating and erasing, thus playing
a similar role to the exponentials in linear logic. It encompasses bounded recursion (iteration) and
minimisation in just one operator. Summarising, a typed linear λ-calculus with bounded iteration
(System L) is not Turing complete, but replacing the iterator with an unbounded recursor (Lrec ),
or adding a minimiser (Lµ ), yields a universal system.
Linear calculi have been successfully used to characterise complexity classes, for instance, as a
consequence of Dal Lago’s results [19], we know that a closed-by-construction discipline in System
L gives exactly the set of PR functions, whereas closed reduction recovers the power of System T .
Interestingly, a closed-construction discipline does not weaken Lrec (the encoding of µ is closed).
The encoding of PCF in Lrec is type-respecting, and Lrec seems a potentially useful intermediate language for compilation. The meaning of the linear recursor will be further analysed in a
denotational setting in future work and the pragmatical impact of these results is currently being
investigated within the language Lilac [46].

References
[1] S. Abramsky. Computational Interpretations of Linear Logic. Theoretical Computer Science,
111:3–57, 1993.
[2] S. Alves. Linearisation of the Lambda Calculus. PhD thesis, Faculty of Science - University
of Porto, April 2007.
[3] S. Alves, M. Fernández, M. Florido, and I. Mackie. The power of linear functions. In Computer
Science Logic, volume 4207 of LNCS, pages 119–134. Springer, 2006.
[4] S. Alves, M. Fernández, M. Florido, and I. Mackie. Linear recursive functions. In Rewriting,
Computation and Proof, volume 4600 of LNCS, pages 182–195. Springer, 2007.
[5] S. Alves, M. Fernández, M. Florido, and I. Mackie. The power of closed reduction strategies.
ENTCS, 174(10):57–74, 2007.
[6] S. Alves, M. Fernández, M. Florido, and I. Mackie. Gödel’s system T revisited. Theor.
Comput. Sci., 411(11-13):1484–1500, 2010.
[7] S. Alves, M. Fernández, M. Florido, and I. Mackie. Linearity and recursion in a typed
lambda-calculus. In PPDP, 2011.
[8] S. Alves and M. Florido. Weak linearization of the lambda calculus. Theoretical Computer
Science, 342(1):79–103, 2005.
[9] A. Asperti and L. Roversi. Intuitionistic light affine logic. ACM Transactions on Computational Logic, 3(1):137–175, 2002.
[10] D. Baelde and D. Miller. Least and greatest fixed points in linear logic. In LPAR 2007: Logic
for Programming, Artificial Intelligence and Reasoning. Springer, 2007.
[11] P. Baillot and V. Mogbil. Soft lambda-calculus: a language for polynomial time computation.
In Proc. FOSSACS’04, volume 2987 of LNCS, pages 27–41. Springer-Verlag, 2004.
[12] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in
Logic and the Foundations of Mathematics. North-Holland, 1984.

25

[13] U. Berger. Minimisation vs. recursion on the partial continuous functionals. In In the Scope
of Logic, Methodology and Philosophy of Science, volume 1 of Synthese Library 316, pages
57–64. Kluwer, 2002.
[14] U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed lambdacalculus. In Proc. Logic in Computer Science (LICS’91), pages 203–211. IEEE Computer
Society, 1991.
[15] G. M. Bierman, A. M. Pitts, and C. V. Russo. Operational properties of Lily, a polymorphic
linear lambda calculus with recursion. In Workshop on Higher Order Operational Techniques
in Semantics, volume 41 of ENTCS, pages 70–88. Elsevier, 2000.
[16] G. Boudol, P.-L. Curien, and C. Lavatelli. A semantics for lambda calculi with resources.
MSCS, 9(4):437–482, 1999.
[17] T. Braüner. The Girard translation extended with recursion. In Computer Science Logic,
8th International Workshop, CSL’94, Kazimierz, Poland, volume 933 of Lecture Notes in
Computer Science, pages 31–45. Springer, 1994.
[18] P.-L. Curien. An abstract framework for environment machines. Theor. Comput. Sci.,
82(2):389–402, 1991.
[19] U. Dal Lago. The geometry of linear higher-order recursion. In Proc. Logic in Computer
Science (LICS’05), pages 366–375, June 2005.
[20] N. Dershowitz. Term rewriting systems by “terese”. Theory Pract. Log. Program., 5(3):395–
399, 2005.
[21] J. Egger, R. E. Møgelberg, and A. Simpson. Enriching an effect calculus with linear types. In
Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of
the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings, volume 5771 of Lecture
Notes in Computer Science, pages 240–254. Springer, 2009.
[22] T. Ehrhard and L. Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(13):1–41, 2003.
[23] M. Fernández, I. Mackie, and F.-R. Sinot. Closed reduction: explicit substitutions without
alpha conversion. MSCS, 15(2):343–381, 2005.
[24] M. Fernández, I. Mackie, and F.-R. Sinot. Lambda-calculus with director strings. Applicable
Algebra in Engineering, Communication and Computing, 15(6):393–437, 2005.
[25] M. Fernández and N. Siafakas. New developments in environment machines. Electr. Notes
Theor. Comput. Sci., 237:57–73, 2009.
[26] D. R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In POPL, pages
363–375, 2007.
[27] J. Girard. Light linear logic. Inf. and Comp., 143(2):175–204, 1998.
[28] J.-Y. Girard. Linear Logic. Theor. Comp. Sci., 50(1):1–102, 1987.
[29] J.-Y. Girard. Towards a geometry of interaction. In Categories in Computer Science and
Logic: Proc. of the Joint Summer Research Conference, pages 69–108. American Mathematical Society, 1989.
[30] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theor. Comp.
Sci. Cambridge University Press, 1989.

26

[31] J.-Y. Girard, A. Scedrov, and P. J. Scott. Bounded linear logic: A modular approach to
polynomial time computability. Theoretical Computer Science, 97:1–66, 1992.
[32] M. Giunti and V. T. Vasconcelos. A linear account of session types in the pi calculus. In
CONCUR, pages 432–446, 2010.
[33] C. Hankin. An Introduction to Lambda Calculi for Computer Scientists, volume 2. College
Publications, 2004. ISBN 0-9543006-5-3.
[34] M. Hofmann. Linear types and non-size-increasing polynomial time computation. In Proc.
Logic in Computer Science (LICS’99). IEEE Computer Society, 1999.
[35] M. Hofmann and S. Jost. Static prediction of heap space usage for first-order functional
programs. In POPL, pages 185–197, 2003.
[36] S. Holmström. Linear functional programming. In Proc. of the Workshop on Implementation
of Lazy Functional Languages, pages 13–32, 1988.
[37] K. Honda. Types for dyadic interaction. In CONCUR’93, volume 715 of LNCS, pages 509–
523. Springer, 1993.
[38] A. J. Kfoury. A linearization of the lambda-calculus and consequences. Journal of Logic and
Computation, 10(3):411–436, 2000.
[39] S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952.
[40] J. W. Klop. Combinatory Reduction Systems. PhD thesis, Mathematisch Centrum, Amsterdam, 1980.
[41] J. W. Klop. New fixpoint combinators from old. Reflections on Type Theory, 2007.
[42] J.-W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems,
introduction and survey. Theor. Computer Science, 121:279–308, 1993.
[43] N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the pi-calculus. In POPL, pages
358–371, 1996.
[44] Y. Lafont. The linear abstract machine. Theor. Comp. Sci., 59:157–180, 1988.
[45] Y. Lafont. Soft linear logic and polynomial time. Theoretical Computer Science, 318(1-2):163–
180, 2004.
[46] I. Mackie. Lilac: A functional programming language based on linear logic. Journal of
Functional Programming, 4(4):395–433, 1994.
[47] I. Mackie. The geometry of interaction machine. In Principles of Programming Languages
(POPL), pages 198–208. ACM Press, 1995.
[48] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I. Information and
Computation, 100(1):1 – 40, 1992.
[49] E. Nöcker, J. Smetsers, M. van Eekelen, and M. Plasmeijer. Concurrent clean. In PARLE’91,
volume 506 of LNCS, pages 202–219. Springer, 1991.
[50] L. Paolini and M. Piccolo. Semantically linear programming languages. In PPDP, pages
97–107, Valencia, Spain, 2008. ACM.
[51] G. D. Plotkin. LCF Considered as a Programming Language. Theoretical Computer Science,
5:223–255, 1977.
[52] K. Terui. Light affine calculus and polytime strong normalization. In Proc. Logic in Comp
Sci. (LICS’01). IEEE Computer Society, 2001.
27

[53] A. v. Tonder. A lambda calculus for quantum computation. SIAM J. Comput., 33(5):1109–
1135, 2004.
[54] P. Wadler. Linear types can change the world! In IFIP TC 2 Conf. on Progr. Concepts and
Methods, pages 347–359. North Holland, 1990.
[55] D. Walker. Substructural type systems. In Adv. Topics in Types and Progr. Languages,
chapter 1, pages 3–43. MIT Press, Cambridge, 2005.
[56] K. Wansbrough and S. P. Jones. Simple usage polymorphism. In Proc. ACM SIGPLAN
Workshop on Types in Compilation. ACM Press, 2000.
[57] N. Yoshida, K. Honda, and M. Berger. Linearity and bisimulation. In FoSSaCS, LNCS, pages
417–434. Springer-Verlag, 2002.

28

