0%

# Problem 623

## Lambda Count

The lambda-calculus is a universal model of computation at the core of functional programming languages. It is based on lambda-terms, a minimal programming language featuring only function definitions, function calls and variables. Lambda-terms are built according to the following rules:

• Any variable $x$ (single letter, from some infinite alphabet) is a lambda-term.
• If $M$ and $N$ are lambda-terms, then $(MN)$ is a lambda-term, called the application of $M$ to $N$.
• If $x$ is a variable and $M$ is a term, then $(\lambda x.M)$ is a lambda-term, called an abstraction. An abstraction defines an anonymous function, taking $x$ as parameter and sending back $M$.

A lambda-term $T$ is said to be closed if for all variables $x$, all occurrences of $x$ within $T$ are contained within some abstraction $(\lambda x.M)$ in $T$. The smallest such abstraction is said to bind the occurrence of the variable $x$. In other words, a lambda-term is closed if all its variables are bound to parameters of enclosing functions definitions. For example, the term $(\lambda x.x)$ is closed, while the term $(\lambda x.(xy))$ is not because $y$ is not bound.

Also, we can rename variables as long as no binding abstraction changes. This means that $(\lambda x.x)$ and $(\lambda y.y)$ should be considered equivalent since we merely renamed a parameter. Two terms equivalent modulo such renaming are called $\alpha$-equivalent. Note that $(\lambda x.(\lambda y.(xy)))$ and $(\lambda x.(\lambda x.(xx)))$ are not $\alpha$-equivalent, since the abstraction binding the first variable was the outer one and becomes the inner one. However, $(\lambda x.(\lambda y.(xy)))$ and $(\lambda y.(\lambda x.(yx)))$ are $\alpha$-equivalent.

The following table regroups the lambda-terms that can be written with at most $15$ symbols, symbols being parenthesis, $\lambda$, dot and variables.

$(\lambda x.x)$ $(\lambda x.(x(xx)))$ $(\lambda x.(\lambda y.(yx)))$ $(\lambda x.((\lambda y.x)x))$
$(\lambda x.(x((xx)x)))$ $(\lambda x.(xx))$ $(\lambda x.((xx)x))$ $(\lambda x.(\lambda y.(yy)))$
$(\lambda x.((\lambda y.y)x))$ $(\lambda x.((xx)(xx)))$ $(\lambda x.(\lambda y.x))$ $(\lambda x.(\lambda y.(xx)))$
$(\lambda x.(x(\lambda y.x)))$ $((\lambda x.x)(\lambda x.x))$ $(\lambda x.((x(xx))x))$ $(\lambda x.(\lambda y.y))$
$(\lambda x.(\lambda y.(xy)))$ $(\lambda x.(x(\lambda y.y)))$ $(\lambda x.(x(x(xx))))$ $(\lambda x.(((xx)x)x))$

Let $\Lambda(n)$ be the number of distinct closed lambda-terms that can be written using at most $n$ symbols, where terms that are $\alpha$-equivalent to one another should be counted only once. You are given that $\Lambda(6)=1$, $\Lambda(9)=2$, $\Lambda(15)=20$ and $\Lambda(35)=3166438$.

Find $\Lambda(2000)$. Give the answer modulo $1000000007$.

## lambda计数

lambda演算是作为函数式编程语言核心的一种通用计算模型。这种模型基于lambda项，这是一种只包含函数定义、函数调用和变量的极简编程语言。lambda项根据如下的规则进行构建：

• 任意变量$x$（由单个字母表示，假定字母表的长度无穷）都是lambda项。
• 如果$M$和$N$是lambda项，那么$(MN)$也是lambda项，这被称为将$M$应用到$N$上。
• 如果$x$是一个变量而$M$是一个lambda项，那么$(\lambda x.M)$是一个lambda项，这被称为抽象。 一个抽象定义了一个匿名函数，其中$x$是参数并返回$M$。

$(\lambda x.x)$ $(\lambda x.(x(xx)))$ $(\lambda x.(\lambda y.(yx)))$ $(\lambda x.((\lambda y.x)x))$
$(\lambda x.(x((xx)x)))$ $(\lambda x.(xx))$ $(\lambda x.((xx)x))$ $(\lambda x.(\lambda y.(yy)))$
$(\lambda x.((\lambda y.y)x))$ $(\lambda x.((xx)(xx)))$ $(\lambda x.(\lambda y.x))$ $(\lambda x.(\lambda y.(xx)))$
$(\lambda x.(x(\lambda y.x)))$ $((\lambda x.x)(\lambda x.x))$ $(\lambda x.((x(xx))x))$ $(\lambda x.(\lambda y.y))$
$(\lambda x.(\lambda y.(xy)))$ $(\lambda x.(x(\lambda y.y)))$ $(\lambda x.(x(x(xx))))$ $(\lambda x.(((xx)x)x))$