Задача 623
Лямбда-счет

Лямбда-исчисление - это универсальная модель вычисления, находящаяся в основе функциональных языков программирования. Она основана на лямбда-термах, минимальных языках программирования, содержащих только определения функций, вызовы функций и переменные. Лямбда-термы построены в соответствии со следующими правилами:

  • Любая переменная $x$ (одна буква из какого-то бесконечного алфавита) является лямбда-термом.
  • Если $M$ и $N$ являются лямбда-термами, тогда $(M N)$ - это лямбда-терм, называющийся аппликацией $M$ к $N$.
  • Если $x$ - переменная и $M$ - терм, тогда $(\lambda x. M)$ - лямбда-терм, называющийся абстракцией. Абстракция определяет анонимную функцию, принимая $x$ как параметр и возвращая $M$.

Лямбда-терм $T$ называется закрытым, если для всех переменных $x$, все возникновения $x$ внутри $T$ содержатся в какой-то абстракции $(\lambda x. M)$ в $T$. Наименьшая такая абстракция связывает возникновение $x$. Другими словами, лямбда-терм закрыт, если все его переменные связаны с параметрами определений окружающих функций. Например, терм $(\lambda x. x)$ закрыт, однако, терм $(\lambda x. (x y))$ - нет, так как $y$ не связан.

Однако, мы можем переименовывать переменные, если это не изменит никакую связывающую абстракцию. Это обозначает, что $(\lambda x. x)$ и $(\lambda y. y)$ стоит считать эквивалентными, так как мы всего лишь переименовали параметр. Два терма, эквивалентные по модулю такого переименования, называются $\alpha$-эквивалентными. Заметим, что $(\lambda x. (\lambda y. (x y)))$ и $(\lambda x. (\lambda x. (x x)))$ не являются $\alpha$-эквивалентными, так как абстракция, связывающая первую переменную, была внешней и стала внутренней. Однако, $(\lambda x. (\lambda y. (x y)))$ и $(\lambda y. (\lambda x. (y x)))$ $\alpha$-эквивалентны.

Следующая таблица перегруппировывает лямбда-термы, которые могут быть записаны не больше, чем $15$ символами, где символами считаются скобки, $\lambda$, точка и переменные.

\[\begin{array}{|c|c|c|c|} \hline (\lambda x.x) & (\lambda x.(x x)) & (\lambda x.(\lambda y.x)) & (\lambda x.(\lambda y.y)) \\ \hline (\lambda x.(x (x x))) & (\lambda x.((x x) x)) & (\lambda x.(\lambda y.(x x))) & (\lambda x.(\lambda y.(x y))) \\ \hline (\lambda x.(\lambda y.(y x))) & (\lambda x.(\lambda y.(y y))) & (\lambda x.(x (\lambda y.x))) & (\lambda x.(x (\lambda y.y))) \\ \hline (\lambda x.((\lambda y.x) x)) & (\lambda x.((\lambda y.y) x)) & ((\lambda x.x) (\lambda x.x)) & (\lambda x.(x (x (x x)))) \\ \hline (\lambda x.(x ((x x) x))) & (\lambda x.((x x) (x x))) & (\lambda x.((x (x x)) x)) & (\lambda x.(((x x) x) x)) \\ \hline \end{array}\]

Пусть $\Lambda(n)$ будет количеством различных закрытых лямбда-термов, которые могут быть записаны, используя не больше $n$ символов, где термы, которые $\alpha$-эквивалентны друг другу, считаются только один раз. Известно, что $\Lambda(6) = 1$, $\Lambda(9) = 2$, $\Lambda(15) = 20$ и $\Lambda(35) = 3166438$.

Найдите $\Lambda(2000)$. В качестве ответа дайте остаток от деления полученного числа на $1\,000\,000\,007$.

Оригинал
 
© Проект Эйлера | Translated problems from ProjectEuler.net