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项$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))$ |
记$\Lambda(n)$为可以用至多$n$个符号表示的不同闭合lambda项的数目，其中$\alpha$-等价的lambda项只计算一次。已知$\Lambda(6)=1$，$\Lambda(9)=2$，$\Lambda(15)=20$以及$\Lambda(35)=3166438$。
求$\Lambda(2000)$，并将答案对$1000000007$取模。