In the same way that the Busy Beaver function is defined for Turing Machines, we could define a similar function for the untyped lambda calculus:
Over all terms in the ULC composed of
n abstractions, variables and applications, which has the longest normal form?
This could be defined in a couple ways: we could consider only strongly normalizing ULC terms, or we could look for the longest normal form over all replacements.
Clearly, this function is not computable for arbitrarily large
n, for the same reason as for the standard Busy Beaver function. However, I am interested in whether anything is known about this function for small values of
n. What values is it known for? What bounds exists for higher
n? For what
n is the value known to be independent of ZFC?