---

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 $\mathrm{\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 $\mathrm{\Lambda }(6)=1$, $\mathrm{\Lambda }(9)=2$, $\mathrm{\Lambda }(15)=20$ and $\mathrm{\Lambda }(35)=3166438$.

Find $\mathrm{\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项$T$中出现过的所有变量$x$均包含于$T$中的某个抽象$(\lambda x.M)$，则称$T$为闭合的，并称包含$x$的抽象中最小的一个绑定了$x$。换言之，如果一个lambda项中出现的所有变量都被绑定为某个函数定义中的参数，则它是闭合的。例如，lambda项$(\lambda x.x)$是闭合的，而lambda项$(\lambda x.(xy))$则不是，因为$y$并未被绑定。

另外，只要不改变抽象的绑定关系，我们可以随意重命名变量。这意味着$(\lambda x.x)$和$(\lambda y.y)$应当被认为是等价的，因为我们只是重命名了一个参数。在这样的重命名中等价的两个lambda项被称为$\alpha$-等价。注意$(\lambda x.(\lambda y.(xy)))$和$(\lambda x.(\lambda x.(xx)))$并不是$\alpha$-等价的，因为前者中绑定第一个变量的抽象是外层的抽象，而后者中则变成了内层的抽象。不过，$(\lambda x.(\lambda y.(xy)))$和$(\lambda y.(\lambda x.(yx)))$是$\alpha$-等价的。

如下的表格展示了所有可以用至多$15$个符号表示的lambda项，这里的符号包括括号，$\lambda$，点号和变量名。

$(\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))$

记$\mathrm{\Lambda }(n)$为可以用至多$n$个符号表示的不同闭合lambda项的数目，其中$\alpha$-等价的lambda项只计算一次。已知$\mathrm{\Lambda }(6)=1$，$\mathrm{\Lambda }(9)=2$，$\mathrm{\Lambda }(15)=20$以及$\mathrm{\Lambda }(35)=3166438$。

求$\mathrm{\Lambda }(2000)$，并将答案对$1000000007$取模。

---