Lambda Count
Problem 623
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:
A lambda-term is said to be closed if for all variables , all occurrences of within are contained within some abstraction in . The smallest such abstraction is said to bind the occurrence of the variable . In other words, a lambda-term is closed if all its variables are bound to parameters of enclosing functions definitions. For example, the term is closed, while the term is not because is not bound.
Also, we can rename variables as long as no binding abstraction changes. This means that and should be considered equivalent since we merely renamed a parameter. Two terms equivalent modulo such renaming are called -equivalent. Note that and are not -equivalent, since the abstraction binding the first variable was the outer one and becomes the inner one. However, and are -equivalent.
The following table regroups the lambda-terms that can be written with at most symbols, symbols being parenthesis, , dot and variables.
Let be the number of distinct closed lambda-terms that can be written using at most symbols, where terms that are -equivalent to one another should be counted only once. You are given that , , and .
Find . Give the answer modulo .