arXiv:1702.03085v5 [cs.DM] 23 May 2017

Quantitative aspects of
linear and affine closed lambda terms
Pierre Lescanne
University of Lyon
École normale supérieure de Lyon
LIP (UMR 5668 CNRS ENS Lyon UCBL INRIA)
46 allée d’Italie, 69364 Lyon, France
pierre.lescanne@ens-lyon.fr
May 24, 2017
Abstract
Affine λ-terms are λ-terms in which each bound variable occurs at most once and linear λ-terms are
λ-terms in which each bound variable occurs once. and only once. In this paper we count the number of
closed affine λ-terms of size n, closed linear λ-terms of size n, affine β-normal forms of size n and linear
β-normal forms of size n, for different ways of measuring the size of λ-terms. From these formulas, we
show how we can derive programs for generating all the terms of size n for each class. The foundation
of all of this is specific data structures, which are contexts in which one counts all the holes at each level
of abstractions by λ’s.
Keywords: Lambda calculus, combinatorics, functional programming

1

Introduction

The λ-calculus [1] is a well known formal system designed by Alonzo Church [8] for studying the concept
of function. It has three kinds of basic operations: variables, application and abstraction (with an operator
λ which is a binder of variables). We assume the reader familiar with the λ-calculus and with de Bruijn
indices.1
In this paper we are interested in terms in which bound variables occur once. A closed λ-term is a λ-term
in which there is no free variable, i.e., only free variables. An affine λ-term (or BCK term) is a λ−term
in which bound variables occur at most once. A linear λ-term (or BCI term) is a λ-term in which bound
variables occur once and only once.
In this paper we propose a method for counting and generating (including random generation) linear and
affine closed λ-terms based on a data structure which we call SwissCheese because of its holes. Actually we
count those λ-terms up-to α-conversion. Therefore it is adequate to use de Bruijn indices [11], because a
term with de Bruijn indices represents an α-equivalence class. An interesting aspect of these terms is the
fact that they are simply typed [17, 16]. For instance, generated by the program of Section 5 6, there are 16
linear terms of natural size 8:
(λ0 (λ0 λ0))

(λ0 λ(λ0 0))

(λ0 λ(0 λ0))

((λ0 λ0) λ0)

(λ(λ0 0) λ0)

(λ(0 λ0) λ0)

λ(λ0 (λ0 0))

λ(λ0 (0 λ0))

λ((λ0 λ0) 0)

λ(λ(λ0 0) 0)

λ(λ(0 λ0) 0)

λ(0 (λ0 λ0))

λ(0 λ(λ0 0))

λ(0 λ(0 λ0))

λ((λ0 0) λ0)

λ((0 λ0) λ0)

written with explicit variables
λx.x (λx.x λx.x)
1 If

λx.x λy.(λx.x y)

λx.x λy.(y λx.x)

(λx.x λx.x) λx.x

the reader is not familiar with the λ-calculus, we advise him to read the introduction of [15], for instance.

1

λy.(λx.x y) λx.x

λy.(y λx.x) λx.x

λy.(λx.x (λx.x y))

λy.(λx.x (y λx.x))

λy.((λx.x λx.x) y)

λy.(λz.(λx.x z) y)

λy.(λz.(z λx.x) y)

λy.(y (λx.x λx.x))

λy.(y λz.(λx.x z))

λy.(y λz.(z λx.x))

λy.((λx.x y) λx.x)

λy.((y λx.x) λx.x)

and there are 25 affine terms of natural size 7:
(λ0 λλ1)

(λ0 λλλ0)

λ(0 λλλ0)
λλ(0 λλ0)

λ(λ0 λ1)

λλλ(0 1)

(λλ0 λλ0)
λ(λ1 λ0)

λλλ(1 0)

(λλ1 λ0)
λλ(λ0 1)

λλλλ2

(λλλ0 λ0)
λλ(1 λ0)

λλ(λ0 λ0)

λ(λλ1 0)

λ(λ0 λλ0)

λλλ(λ0 0)

λ(λλλ0 0)
λ(λλ0 λ0)

λλλ(0 λ0)

λ(0 λλ1)
λλ(λλ0 0)

λλλλλ1

λλλλλλ0

The Haskell programs of this development are on GitHub: https://github.com/PierreLescanne/
CountingGeneratingAfffineLinearClosedLambdaterms.

Notations
In this paper we use specific notations.
Given a predicate p, the Iverson notation written [p(x)] is the function taking natural values which is 1
if p(x) is true and which is 0 if p(x) is false.
Let m ∈ Np be the p-tuple (m0 , ..., mp−1 ). In Section 5, we consider also infinite tuples. Thus m ∈ Nω is
the sequence (m0 , m1 , ...). Notice in the case of infinite tuples, we are only interested in infinite tuples equal
to 0 after some index.
• p is the length of m, which we write also length m
• The p-tuple (0, ..., 0) is written 0p . 0ω is the infinite tuple made of 0’s.
• The increment of a p-tuple at i is:
m↑i = n ∈ Np where nj = mj if j 6= i and ni = mi + 1
• Putting an element x as head of a tuple is written
x : m = x : (m0 , ...) = (x, m0 , ...)
tail removes the head of a tuple:
tail(x : m) = m.
•  is the componentwise addition on tuples.

2

SwissCheese

The basic concept is this of m-SwissCheese or Swisscheese of characteristic m or simply SwissCheese
if there is no ambiguity on m. A m-SwissCheese or a SwissCheese of characteristic m, where m is of length p)
is, a λ-term with holes at p levels, which are all counted, using m. The p levels of holes are 0 ,... p−1 . A
hole i is meant to be a location for a variable at level i, that is under i λ’s. According to the way bound
variables are inserted when creating abstractions (see below), we consider linear or affine SwissCheeses. The
holes have size 0. An m-SwissCheese or a SwissCheese of characteristic m has m0 holes at level 0, m1 holes at
level 1, ... mp−1 holes at level p − 1. Let ln,m (resp. an,m ) count the linear (resp. the affine) m-SwissCheese
of size n. ln,m = ln,m0 and an,m = an,m0 if m is finite, length m ≥ n, mi = m0i for i ≤ length m, and m0i = 0
for i > length m. ln,0n (resp. an,0n ) counts the closed linear (resp. the closed affine) λ-terms.

2

c1 =

λ

c2 =

@

λ
0

1

@

=

@
c1

0

@

c2

λ

@

@

1

λ
0

1

0

1

Figure 1: Building a SwissCheese by application

λ =

λ

λ

c2

@

@

λ

=

@

λ

1

@

@

2
2

λ

λ
0

1

λ

@

@

1
2

λ
0

1

S
0

Figure 2: Abstracting SwissCheeses without and with binding

2.1

Growing a SwissCheese

Given two SwissCheeses, we can build a SwissCheese by application like in Fig 1. In Fig. 1, c1 is a (0, 1, 0, 0, 0)SwissCheese, c2 is a (1, 1, 0, 0, 0)-SwissCheese and c1 @c2 is a (1, 2, 0, 0, 0)-SwissCheese. Said otherwise, c1
has characteristic (0, 1, 0, 0, 0), c2 has characteristic (1, 1, 0, 0, 0) and c1 @c2 has characteristic (1, 2, 0, 0, 0).
According to what we said, c1 @c2 has characteristic (1, 2) as well as characteristic (1, 2, 0, 0, ...) (a tuple
starting with 1, followed by 2, followed by infinitely many 0’s). We could also say that c1 has characteristic
(0, 1) and c2 has characteristic (1, 1) making @ a binary operation on SwissCheeses of length 2 whereas
previously we have made @ a binary operation on SwissCheeses of length 5. In other words, when counting
SwissCheeses of characteristic m, the trailing 0’s are irrelevant. In actual computations, we make the lengths
of characteristics consistent by adding trailing 0’s to too short ones.
Given a SwissCheese, there are two ways to grow a SwissCheese to make another SwissCheese by abstraction.
1. We put a λ on the top of a m-SwissCheese c. This increases the levels of the holes: a hole i becomes
a hole i+1 . λc is a (0 : m)-SwissCheese. See Fig 2 on the left. This way, no index is bound by the top
λ, therefore this does not preserve linearity (it preserves affinity however). Therefore this construction
is only for building affine SwissCheeses, not for building linear SwissCheeses. In Figure 2 (left), we
colour the added λ in blue and we call it abstraction with no binding.
2. In the second method for growing a SwissCheese by abstraction, we select first a hole i , we top the
SwissCheese by a λ, we increment the levels of the other holes and we replace the chosen hole by S i 0.
In Figure 2 (right), we colour the added λ in green and we call it abstraction with binding.

2.2

Measuring SwissCheese

We considers several ways of measuring the size of a SwissCheese derived from what is done on λ-terms. In
all these sizes, applications @ and abstractions λ have size 1 and holes have size 0. The differences are in
the way variables are measured.

3

• Variables have size 0, we call this variable size 0.
• Variables have size 1, we call this variable size 1 .
• Variables (or de Bruijn indices) S i 0 have size i + 1, we call this natural size.

3

Counting linear closed terms

We start with counting linear terms since they are slightly simpler. We will give recursive formulas first for
ν
0
the numbers ln,m
of linear SwissCheeses of natural size n with holes set by m, then for the numbers ln,m
1
of linear SwissCheeses of size n, for variable size 0, with holes set by m, eventually for the numbers ln,m
of
linear SwissCheeses of size n, for variable size 1, with holes set by m. When we do not want to specify a
chosen size, we write only ln,m without superscript.

3.1

Natural size

First let us count linear SwissCheeses with natural size. This is given by the coefficient lν which has two
arguments: the size n of the SwissCheese and a tuple m which specifies the number of holes of each level.
ν
In other words we are interested in the quantity ln,m
. We assume that the length of m is p, greater than n.
n = 0 whatever size is considered, there is only one SwissCheese of size 0 namely 0 . This means that the
number of SwissCheeses of size 0 is 1 if and only if m = (1, 0, 0, ...):
ν
l0,m

=

0
l0,m

=

1
l0,m

= [m0 = 1 ∧

p−1
^

mj = 0]

j=1

n 6= 0 and application if a λ-term of size n has holes set by m and is an application, then it is obtained
from a λ term of size k with holes set by q and a λ term of size n − k − 1 with holes set by r, with
m = q  r:
n
X X
lk,q ln−1−k,r
qr =m k=0

n 6= 0 and abstraction with binding consider a level i, that is a level of hole i . In this hole we put
ν
a term S i−1 0 of size i. There are mi ways to choose a hole i . Therefore there are mi ln−i−1,m
SwissCheeses which are abstractions with binding in which a i has been replaced by the de Bruijn
ν
↓i
index S i−1 0 among ln,0:m
is m in which mi is decremented. We notice
↓i SwissCheeses, where m
that this refers only to an m starting with 0. Hence by summing over i and adjusting m, this part
contributes as:
p−1
X
ν
(mi + 1) ln−i,m
↑i
i=0
ν
to ln+1,0:m
.
ν
We have the following recursive definitions of ln,m
:

ν
ln+1,0:m

=

X

n
X

ν
ν
lk,q
ln−k,r
+

qr = 0:m k=0
ν
ln+1,(h+1):m

=

X

p−1
X
ν
(mi + 1) ln−i,m
↑i
i=0

n
X

ν
ν
lk,q
ln−k,r

qr=(h+1):m k=0

Numbers of closed linear terms with natural size are given in Figure 3.
4

3.2

Variable size 0

0
The only difference is that the inserted de Bruijn index has size 0. Therefore we have mi ln−1,m
where we
ν
had mi ln−i−1,m for natural size. Hence the formulas:
0
ln+1,0:m

n
X

X

=

0
0
lk,q
ln−k,r
+

p−1
X

qr = 0:m k=0
0
ln+1,(h+1):m

=

i=0

n
X

X

0
(mi + 1) ln,m
↑i

0
0
lk,q
ln−k,r

qr=(h+1):m k=0
0
The sequence ln,0
n of the numbers of closed linear terms is 0, 1, 0, 5, 0, 60, 0, 1105, 0, 27120, 0, 828250, which
is sequence A062980 in the On-line Encyclopedia of Integer Sequences with 0’s at even indices.

3.3

Variable size 1

1
ν
The inserted de Bruijn index has size 1. We have mi ln−2,m
where we had mi ln−i−1,m
for natural size.
1
ln+1,0:m

n
X

X

=

1
1
lk,q
ln−k,r
+

n−1
X

qr = 0:m k=0
1
ln+1,(h+1):m

=

i=0

n
X

X

1
(mi + 1) ln−1,m
↑i

1
1
lk,q
ln−k,r

qr=(h+1):m k=0

As noticed by Grygiel et al. [13] (§ 6.1) There are no linear closed λ-terms of size 3k and 3k + 1. However
for the values 3k + 2 we get the sequence: 1, 5, 60, 1105, 27120, ... which is again sequence A062980 of the
On-line Encyclopedia of Integer Sequences.

4

Counting affine closed terms

We have just to add the case n 6= 0 and abstraction without binding. Since no index is added, the size
increases by 1. The numbers are written aνn,m , a0n,m , a1n,m , and an,m when the size does not matter. There
are (0 : m)-SwissCheeses of size n that are abstraction without binding. We get the recursive formulas:

4.1

Natural size
aνn+1,0:m

=

X

n
X

aνk,q aνn−k,r +

qr = 0:m k=0

aνn+1,(h+1):m

=

X

p−1
X
(mi + 1) aνn−i,m↑i + aνn,m
i=0

n
X

aνk,q aνn−k,r

qr=(h+1):m k=0

The numbers of closed affine size with natural size are given in Figure 4.

4.2

Variable size 0
a0n+1,0:m

=

X

n
X

a0k,q a0n−k,r +

qr = 0:m k=0

a0n+1,(h+1):m

=

X

n
X

p−1
X
i=0

a0k,q a0n−k,r

qr=(h+1):m k=0

5

(mi + 1) a0n,m↑i + a0n,m

The sequence a0n,0ω of the numbers of affine closed terms for variable size 0 is
0, 1, 2, 8, 29, 140, 661, 3622, 19993, 120909, 744890, 4887401, 32795272, ...
It does not appear in the On-line Encyclopedia of Integer Sequences. It corresponds to the coefficients of the
generating function A(z, 0) where
A(z, u) = u + z(A(z, u))2 + z

4.3

∂A(z, u)
+ zA(z, u).
∂u

Variable size 1
a1n+1,0:m

n−1
X

X

=

a1k,q a1n−k,r +

qr = 0:m k=0

a1n+1,(h+1):m

=

(mi + 1) a1n−1,m↑i + a1n,m

i=0

n
X

X

n−1
X

a1k,q a1n−k,r

qr=(h+1):m k=0

The sequence a1n,0ω of the numbers of affine closed terms for variable size 1 is
0, 0, 1, 2, 3, 9, 30, 81, 242, 838, 2799, 9365, 33616, 122937, 449698, 1696724, 6558855, ...
This is sequence A281270 in the On-line Encyclopedia of Integer Sequences. However it corresponds to the
coefficient of the generating function Â(z, 0) where Â(z, u) is the solution of the functional equation:
Â(z, u) = zu + z(Â(z, u))2 + z

∂ Â(z, u)
+ z Â(z, u).
∂u

Notice that this corrects the wrong assumptions of [13] (Section 6.2).

5

Generating functions

Consider families Fm (z) of generating functions indexed by m, where m is an infinite tuple of naturals. In
fact, we are interested in the infinite tuples m that are always 0, except a finite number of indices, in order
to compute F0ω (z), which corresponds to closed λ-terms. Let u stands for the infinite sequences of variables
m1
mn
0
(u0 , u1 , ...) and um stands for (um
0 , u1 , ..., un , ...) and tail (u) stand for (u1 , ...). We consider the series of
two variables z and u or double series associated with Fm (z):
X
F(z, u) =
Fm (z) um .
m∈Nω

Natural size
Lνm (z) is associated with the numbers of closed linear SwissCheeses for natural size:
Lν0:m (z)
Lν(h+1):m (z)

=

=

z

X

Lνm0 (z)Lνm00 (z) + z

m0 m00 =0:m
∞
^

[h = 0 +

∞
X
(mi + 1)z i Lνm↑i (z)
i=0

mi = 0] + z

X
m0 m00 =(h+1):m

i=0

6

Lνm0 (z)Lνm00 (z)

Lν0ω is the generating function for the closed linear λ-terms. Lν (z, u) is the double series associated with
Lνm (z) and is solution of the equation:
Lν (z, u)

∞
X

= u0 + z(Lν (z, u))2 +

zi

i=1
ν

∂Lν (z, tail (u))
∂ui

ω

L (z, 0 ) is the generating function of closed linear λ-terms.
For closed affine SwissCheeses we get:
Aν0:m (z)
Aν(h+1):m (z)

=

X

z

Aνm0 (z)Aνm00 (z) + z

m0 m00 =0:m
∞
^

=

[h = 0 +

i=0

X

mi = 0] + z

the generating function for the closed linear λ-terms. Aν (z, u) is the double series associated with
and is solution of the equation:
Aν (z, u)

= u0 + z(Aν (z, u))2 +

∞
X

zi

i=1
ν

Aνm0 (z)Aνm00 (z)

m0 m00 =(h+1):m

i=0

Aν0ω is
Aνm (z)

∞
X
(mi + 1)z i Aνm↑i (z) + z Aνm (z)

∂Aν (z, tail (u))
+ zAν (z, tail (u))
∂ui

ω

A (z, 0 ) is the generating function of closed affine λ-terms.

Variable size 0
L0m is associated with the numbers of closed linear SwissCheeses for variable size 0:
L00:m (z)

X

= z

L0m0 (z)L0m00 (z) + z

m0 m00 =m

L0(h+1):m (z)

=

[h = 0 +

∞
^

∞
X

(mi + 1)L0m↑i (z)

i=0

X

mi = 0] +

zL0m0 (z)L0m00 (z)

m0 m00 =m

i=0

L00ω is the generating function for the closed linear λ-terms. L0 (z, u) is the double series associated with
L0m (z) and is solution of the equation:
L0 (z, u)

= u0 + z(L0 (z, u))2 +

∞
X
∂L0 (z, tail (u)
i=1

∂ui

L0 (z, 0ω ) is the generating function of closed linear λ-terms.
For closed affine SwissCheeses we get:
A00:m (z)
A0(h+1):m (z)

=

=

z

X

A0m0 (z)A0m00 (z) + z

m0 m00 =0:m
∞
^

[h = 0 +

i=0

X

mi = 0] +

i=0

∞
X
(mi + 1)A0m↑i (z) + z A0m (z)

zA0m0 (z)A0m00 (z)

m0 m00 =(h+1):m

A00ω is the generating function for the affine linear λ-terms. A0 (z, u) is the double series associated with
A0m (z) and is solution of the equation:
A0 (z, u)

= u0 + z(A0 (z, u))2 +

∞
X
∂A0 (z, tail (u))
i=1

0

ω

A (z, 0 ) is the generating function of closed linear λ-terms.
7

∂ui

+ zA0 (z, tail (u))

Variable size 1
1
The generating functions for ln,m
are:

L10:m (z)
L1(h+1):m (z)

=

=

X

z

L1m0 (z)L1m00 (z) + z 2

m0 m00 =m
∞
^

[h = 0 +

∞
X

(mi + 1)L1m↑i (z)

i=0

X

mi = 0] +

zL1m0 (z)L1m00 (z)

m0 m00 =m

i=0

Then we get as associated double series :
L1 (z, u)

=

u0 + z(L1 (z, u))2 + z 2

∞
X
∂L1 (z, tail (u))
i=1

8

∂ui

6

Effective computations

The definition of the coefficients aνm and others is highly recursive and requires a mechanism of memoization.
In Haskell, this can be done by using the call by need which is at the core of this language. Assume we want
to compute the values of aνm until a value upBound for n. We use a recursive data structure:
data Mem = Mem [Mem] | Load [Integer]
in which we store the computed values of a function
a :: Int -> [Int] -> Integer
In our implementation the depth of the recursion of Mem is limited by upBound, which is also the longest
tuple m for which we will compute aνm . Associated with Mem there is a function
access :: Mem -> Int -> [Int] -> Integer access (Load l) n [] = l !! n
access (Mem listM) n (k:m) = access (listM !! k) n m
The leaves of the tree memory, corresponding to Load, contains the values of the function:
memory :: Int -> [Int] -> Mem
memory 0 m = Load [a n (reverse m) | n<-[0..]]
memory k m = Mem [memory (k-1) (j:m) | j<-[0..]]
The memory relative to the problem we are interested in is
theMemory = memory (bound) []
and the access to theMemory is given by a specific function:
acc :: Int -> [Int] -> Integer acc n m = access theMemory n m
Notice that a and acc have the same signature. This is not a coincidence, since acc accesses values of a
already computed. Now we are ready to express a:
a 0 m = iv (head m == 1 && all ((==) 0) (tail m))
a n m = aAPP n m + aABSwB n m + aABSnB n m
aAPP counts affine terms that are applications:
aAPP n m = sum (map (\((q,r),(k,nk))->(acc k q)*(acc nk r)) (allCombinations m (n-1)))
where allCombinations returns a list of all the pairs of pairs (m0 , m00 ) such m = m0  m00 and of pairs
(k, nk) such that k + nk = n. aABSwB counts affine terms that are abstractions with binding.
aABSwB n m
| head m == 0 = sum [aABSAtD n m i |i<-[1..(n-1)]]
| otherwise = 0
aABSAtD counts affine terms that are abstractions with binding at level i:
aABSAtD n m i = (fromIntegral (1 + m!!i))*(acc (n-i-1) (tail (inc i m) ++ [0]))
aABSnB counts affine terms that are abstractions with no binding:
aABSnB n m
| head m == 0 = (acc (n-1) (tail m ++ [0]))
| otherwise = 0
Anyway the efficiency of this program is limited by the size of the memory, since for computing aνn,0n , for
instance, we need to compute aνr for about n! values.
9

7

Generating affine and linear terms

By relatively small changes it is possible to build programs which generate linear and affine terms. For
instance for generating affine terms we get.
amg :: Int -> [Int] -> [SwissCheese]
amg 0 m = if (head m == 1 && all ((==) 0) (tail m)) then [Box 0] else []
amg n m = allAPP n m ++ allABSwB n m ++ allABSnB n m
allAPP :: Int -> [Int] -> [SwissCheese]
allAPP n m = foldr (++) [] (map (\((q,r),(k,nk))-> appSC (cartesian (accAG k q)
(accAG nk r))
(allCombinations m (n-1)))
allABSAtD :: Int -> [Int] -> Int -> [SwissCheese]
allABSAtD n m i = foldr (++) [] (map (abstract (i-1)) (accAG (n - i - 1)
(tail (inc i m) ++ [0])))
allABSwB :: Int -> [Int] -> [SwissCheese]
allABSwB n m
| head m == 0 = foldr (++) [] [allABSAtD n m i |i<-[1..(n-1)]]
| otherwise = []
allABSnB :: Int -> [Int] -> [SwissCheese]
allABSnB n m
| head m == 0 = map (AbsSC . raise) (accAG (n-1) (tail m ++ [0]))
| otherwise = []
memoryAG :: Int -> [Int] -> MemSC
memoryAG 0 m = LoadSC [amg n (reverse m) | n<-[0..]]
memoryAG k m = MemSC [memoryAG (k-1) (j:m) | j<-[0..]]
theMemoryAG = memoryAG (upBound) []
accAG :: Int -> [Int] -> [SwissCheese]
accAG n m = accessSC theMemoryAG n m
From this, we get programs for generating random affine terms or random linear terms as follows: if we want
a random closed linear term of a given size n, we throw a random number, say p, between 1 and ln,0n and
we look for the pth in the list of all the closed linear terms of size n. Haskell laziness mimics the unranking.
Due to high requests in space, we cannot go further than the random generation of closed linear terms of
size 23 and closed affine terms of size 19 . There are similar programs for generating all the terms of size n
for variable size 0 and variable size 1.

8

Normal forms

From the method used for counting affine and linear closed terms, it is easy to deduce method for counting
affine and linear closed normal forms. Like before, we use SwissCheeses. In this section we consider only
natural size.

10

8.1

Natural size

Affine closed normal forms
ν
Let us call anfn,m
the numbers of affine SwissCheeses with no β-redex and aneνn,m the numbers of neutral
affine SwissCheeses, i.e., affine SwissCheeses with no β-redexes that are sequences of applications starting
with a de Bruijn index. In addition we count:

• anf ν λwn,m the number of affine SwissCheeses with no β-redex which are abstraction with a binding
of a de Bruijn index,
• anf ν λnn,m the number of affine SwissCheeses with no β-redex which are abstraction with no binding.

ν
anf0,m
ν
anfn+1,m

= aneν0,m
= aneνn+1,m + anf ν λwn+1,m + anf ν λnn+1,m

where
aneν0,m
aneνn+1,m

= m0 = 1 ∧

j=1
n
X

X

=

p−1
^

mj = 0
ν
aneνk,q anfn−k,r

qr = 0:m k=0

and
ν

anf λwn+1,m

=

n
X
ν
(mi + 1) anfn−i,m
↑i
i=0

and
anf ν λnn+1,m

ν
= anfn,m

ν
ν
There are two generating functions, Anf and Ane , which are associated to anfn,m
and anfn,m
:

Anf (z, u)

= Ane (z, u) +

∞
X
i=1

ne

A (z, u)

zi

∂Anf (z, tail (u))
+ zAnf (z, tail (u))
∂ui

ne

= u0 + zA (z, u)Anf (z, u)

Linear closed normal forms
ν
Let us call lnfn,m
the numbers of linear SwissCheeses with no β-redex and lneνn,m the numbers of neutral
linear SwissCheeses, linear SwissCheeses with no β-redexes that are sequences of applications starting with a
de Bruijn index. In addition we count lnf ν λwn,m the number of linear SwissCheeses with no β-redex which
are abstraction with a binding of a de Bruijn index.

ν
lnf0,m
ν
lnfn+1,m

= lneν0,m
= lneνn+1,m + lnf ν λwn+1,m

11

where
lneν0,m
lneνn+1,m

= m0 = 1 ∧

j=1
n
X

X

=

p−1
^

mj = 0
ν
lneνk,q lnfn−k,r

qr = 0:m k=0

and
lnf ν λwn+1,m

p−1
X
ν
(mi + 1) lnfn−i,m
↑i

=

i=0

with the two generating functions:
Lnf,ν (z, u)

= Lne,ν (z, u) +

∞
X
i=1

ne,ν

L

(z, u)

= u0 + zL

ne,ν

zi

∂Lnf,ν (z, tail (u))
∂ui

(z, u)Lnf,ν (z, u)

We also deduce programs for generating all the closed affine or linear normal forms of a given size from
which we deduce programs for generating random closed affine or linear normal forms of a given size. For
instance, here are three randoms linear closed normal forms (using de Bruijn indices) of natural size 28:
λλλλ(2 λ((1 2) λ(0 (5 1))))

8.2

λ(0 λλ(1 λλ((0 (2 λλ((1 λ0) 0))) 1)))

λ((0 λ0) λλ((0((1 λ0)λλ(1 (0 λ0))))λ0))

Variable size 0

Linear closed normal forms
0
the numbers of linear SwissCheeses with no β-redex and lne0n,m the
A little like previously, let us call lnfn,m
numbers of neutral linear SwissCheeses, linear SwissCheeses with no β-redexes that are sequences of applications starting with a de Bruijn index. In addition we count lnf 0 λwn,m the number of linear SwissCheeses
with no β-redex which are abstraction with a binding of a de Bruijn index. We assume that the reader knows
now how to proceed.

0
lnf0,m
0
lnfn+1,m

= lne00,m
= lne0n+1,m + lnf 0 λwn+1,m

where
lne00,m
lne0n+1,m

= m0 = 1 ∧
=

p−1
^
j=1
n
X

X

mj = 0
0
lne0k,q lnfn−k,r

qr = 0:m k=0

lnf 0 λwn+1,m

=

n
X
i=0

12

0
(mi + 1) lnfn,m
↑i

and the two generating functions:
Lnf,0 (z, u)

= Lne,0 (z, u) +

∞
X
∂Lnf,0 (z, tail (u))
i=1

Lne,0 (z, u)

∂ui

= u0 + zLne,0 (z, u)Lnf,0 (z, u)

0
With no surprise we get for lnfn,0
n the sequence:

0, 1, 0, 3, 0, 26, 0, 367, 0, 7142, 0, 176766, 0, 5304356, ...
mentioned by Zeilberger in [19] and listing the coefficients of the generating function Lnf,0 (z, 0ω ).
We let the reader deduce how to count closed affine normal forms for variable size 0 and closed linear
and affine normal forms for variable size 1 alike. Notice that the Haskell programs are on the GitHub site.

9

Related works and Acknowledgement

There are several works on counting λ-terms, for instance on natural size [3, 2], on variable size 1 [5, 10, 18],
on variable size 0 [14], on affine terms with variable size 1 [7, 6], on linear λ-terms [21, 19, 20], also on a
size based binary representation of the λ-calculus [15] (see [12] for a synthetic view of both natural size and
binary size).
The basic idea of this work comes from a discussion with Maciej Bendkowski, Olivier Bodini, Sergey
Dovgal and Katarzyna Grygiel, I thank them as I thank Noam Zeilberger for interactions.

10

Conclusion

This presentation shares similarity with this of [14, 15, 4]. Instead of considering the size n and the bound
m of free indices like in expressions of the form:
Tn+1,m = Tn,m+1 +

n
X

Ti,m Tn−i,m

i=0

here we replace m by the characteristic m. We can imagine a common framework. On another hand, as
noticed by Paul Tarau, this approach has features of dynamic programming [9], which makes it somewhat
efficient.

References
[1] Henk P. Barendregt. The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1984. Second
edition.
[2] Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, and Marek Zaionc. Combinatorics of λ-terms:
a natural approach. CoRR, abs/1609.07593, 2016.
[3] Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, and Marek Zaionc. A natural counting of
lambda terms. In Rusins Martins Freivalds, Gregor Engels, and Barbara Catania, editors, SOFSEM
2016: Theory and Practice of Computer Science - 42nd International Conference on Current Trends in
Theory and Practice of Computer Science, Harrachov, Czech Republic, January 23-28, 2016, Proceedings, volume 9587 of Lecture Notes in Computer Science, pages 183–194. Springer, 2016.

13

[4] Maciej Bendkowski, Katarzyna Grygiel, and Paul Tarau. Boltzmann samplers for closed simply-typed
lambda terms. In Yuliya Lierler and Walid Taha, editors, Practical Aspects of Declarative Languages 19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017, Proceedings, volume
10137 of Lecture Notes in Computer Science, pages 120–135. Springer, 2017.
[5] Olivier Bodini, Danièle Gardy, and Bernhard Gittenberger. Lambda terms of bounded unary height. In
Proceedings of the Eighth Workshop on Analytic Algorithmics and Combinatorics, pages 23–32, 2011.
[6] Olivier Bodini, Danièle Gardy, Bernhard Gittenberger, and Alice Jacquot. Enumeration of generalized
BCI lambda-terms. Electr. J. Comb., 20(4):P30, 2013.
[7] Olivier Bodini, Danièle Gardy, and Alice Jacquot. Asymptotics and random sampling for BCI and BCK
lambda terms. Theor. Comput. Sci., 502:227–238, 2013.
[8] Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
[9] Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms, Third Edition. The MIT Press, 3rd edition, 2009.
[10] René David, Christophe Raffalli, Guillaume Theyssier, Katarzyna Grygiel, Jakub Kozik, and Marek
Zaionc. Some properties of random lambda terms. Logical Methods in Computer Science, 9(1), 2009.
[11] Nicolaas G. de Bruijn. Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Proc. Koninkl. Nederl. Akademie van Wetenschappen, 75(5):381–392, 1972.
[12] Bernhard Gittenberger and Zbigniew Golebiewski. On the number of lambda terms with prescribed size
of their de Bruijn representation. In Nicolas Ollinger and Heribert Vollmer, editors, 33rd Symposium
on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France,
volume 47 of LIPIcs, pages 40:1–40:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
[13] Katarzyna Grygiel, Pawel M. Idziak, and Marek Zaionc. How big is BCI fragment of BCK logic. J.
Log. Comput., 23(3):673–691, 2013.
[14] Katarzyna Grygiel and Pierre Lescanne. Counting and generating lambda terms. J. Funct. Program.,
23(5):594–628, 2013.
[15] Katarzyna Grygiel and Pierre Lescanne. Counting and generating terms in the binary lambda calculus.
J. Funct. Program., 25, 2015.
[16] J. Roger Hindley. BCK-combinators and linear lambda-terms have types. Theor. Comput. Sci., 64(1):97–
105, 1989.
[17] J. Roger Hindley. Basic Simple Type Theory. Number 42 in Cambridge Tracts in Theoretical Computer
Science. Cambridge University Press, 1997.
[18] Pierre Lescanne. On counting untyped lambda terms. Theor. Comput. Sci., 474:80–97, 2013.
[19] Noam Zeilberger.
Counting isomorphism classes of β-normal linear lambda terms.
abs/1509.07596, 2015.

CoRR,

[20] Noam Zeilberger. Linear lambda terms as invariants of rooted trivalent maps. J. Funct. Program.,
26:e21, 2016.
[21] Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar
lambda terms. Logical Methods in Computer Science, 11(3), 2015.

14

0
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

0
0
1
0
0
3
2
0
16
24
8
117
252
180
1024
2680
2952
10350
29420
42776
116768
335520
587424
1420053
3976424
7880376
18103936
48816576
104890704
237500826
617733708
1396750576
3171222464
8014199360
18688490336
42840683418
106063081288
251769197688
583690110208
1425834260080
3417671496432
8007221710652
19404994897976
46747189542384
110498345360800
266679286291872
644021392071840
1533054190557133
3693823999533360
8931109667692464
21375091547312128

51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100

51496022711337536
124591137939086496
299402908258405410
721839933329222924
1747307145272084192
4211741383777966592
10165998012602469888
24620618729658655936
59482734150603634286
143764591607556354344
348379929166234350008
843169238563254723200
2040572920613086128400
4948102905207104837424
11992521016286173712196
29059897435554891991144
70516464312280927105392
171105110698292441423968
415095704639682396539232
1008016383720573882885792
2448305474519849567597826
5945721872300885649415632
14449388516068567845838736
35125352062243788817753856
85382289240293493116120064
207650379931166057815603296
505172267243918348155299780
1229005880128485245247395000
2991079243470267667831893408
7281852742753184123608419712
17729171587798767750815341440
43177454620325445122944305984
105185452787117035266315446868
256273862465425158211948020048
624527413292252904584121980208
1522355057007327280427270436480
3711429775030704772089070886624
9050041253711022076275958636128
22073150301758857110072042919800
53844910909398928990641101351664
131371135544173914537076774932576
320588677238085642820920910555968
782465218885869813183863213231424
1910077425906069707804966102543936
4663586586924802791117231052636349
11388259565942452837717688743953504
27813754361897984543467478917223008
67941781284113201998645699501746176
165989485724048964272023600773271424
405588809305168453963137377442321728

Figure 3: Natural size: numbers of closed linear terms of size n from 0 to 100

Data
ν
ν
ν
In the appendix, we give the first values of ln,0
n , an,0n , and anfn,0n .

15

0
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

0
0
1
1
2
5
12
25
64
166
405
1050
2763
7239
19190
51457
138538
374972
1020943
2792183
7666358
21126905
58422650
162052566
450742451
1256974690
3513731861
9843728012
27633400879
77721141911
218984204904
618021576627
1746906189740
4945026080426
14017220713131
39784695610433
113057573020242
321649935953313
916096006168770
2611847503880831
7453859187221508
21292177500898858
60875851617670699
174195916730975850
498863759031591507
1429753835635525063
4100730353324163138
11769771167532816128
33804054749367200891
97151933333668422006
279385977720772581435

51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100

803928779462727941247
2314623127904669382002
6667810436356967142481
19218411059885449257096
55421020161661024650870
159899218321197381984561
461557020400062903560120
1332920908954281811200519
3851027068336583693412910
11131032444503136571789527
32186581221116996967632029
93108410048006285466998584
269446191702411420790402033
780043726186403167392453886
2259043189995515315930349650
6544612955390252336187266873
18966737218108971681014445025
54985236298270057405776629352
159455737350384637847783055311
462562848624435724964181323484
1342251884451664733064283251627
3896065622127200625653134100538
11312117748805772104795220337816
32853646116456632492645965741531
95442534633482460553801961967438
277342191547330839640289978813667
806125189457291902863848267463755
2343682130911232279285707290604156
6815564023736534208079367816340359
19824812322145727566417303371819466
57679033022808238913186144092831856
167851787082561392384648248846390041
488574368670832093243802790464796207
1422426342380883254459783410845365006
4142104564089044203901190817275864665
12064305885705003967881526911560653106
35145647815239737143373764367447378676
102406303052123097062053564818109468705
298446029598661205216170897850336550644
869935452705023302189031644932803990417
2536229492704354513309696228592784181158
7395518143425160073537967606298755947391
21568776408467701927134211542478146593789
62915493935623036562559989770249004382816
183553775888862113259168150130266362416356
535600661621556969155453544692826625532079
1563109720672526919899689366626240867515144
4562542818801138452310024131223304186909233
13319630286623965617386598746472280781972745
38890520391341859449843201188612375394153776

Figure 4: Natural size: numbers of closed affine terms of size n from 0 to 100

16

0
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

0
0
1
1
2
3
7
10
20
40
77
160
318
671
1405
2981
6312
13672
29399
63697
139104
304153
667219
1469241
3247176
7184288
15949179
35480426
79083472
176607519
395119875
885450388
1987289740
4466760570
10053371987
22656801617
51121124910
115478296639
261139629999
591138386440
1339447594768

41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

3037843646560
6895841598615
15666498585568
35620848278448
81052838239593
184564847153821
420564871255118
958975854646984
2188068392529104
4995528560788451
11411921511827547
26084524952754538
59654682828889245
136500653558490261
312496493161999851
715760763686417314
1640194881084692664
3760284787917366081
8624561382605096780
19789639944299656346
45427337308377290201
104320438668034814453
239656248361374562433
550769764273325683828
1266217774600330829940
2912050679107531357883
6699418399886008666265
15417663698156810292010
35492710197462925262295
81732521943462960197057
188270363628099910161436
433807135012774797924026
999851681931974600766994
2305129188866501774481545
5315847675735178072941600
12262083079763320881047944
28292248892584567512609357
65294907440089718078048829
150729070403767032817820543
348031015577337732605480908

Figure 5: Natural size: numbers of closed affine normal forms of size n from 0 to 80

17

