# Busy Beaver Equivalent for the Untyped Lambda Calculus

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?

• I think that research on Busy Beavers focused only on the Turing machine model (as introduced by T.Rado in 1962). Switching to an equivalent (Turing complete) model probably (who knows?:) cannot lead to new insights about the problem ( undecidability is not affected, small things can become very large, and so on ...). Nevertheless it would be fun to see if independency of ZFC could be achieved in less space than the space used to describe the 7,918 states Turing Machine independent of ZFC. – Marzio De Biasi Jan 1 at 19:36
• @MarzioDeBiasi Not that relevant, but people have taken this question pretty seriously, and code golfed it down to 1919 states: github.com/sorear/metamath-turing-machines – cody Jan 4 at 15:58
• Also, see this: googology.wikia.com/wiki/Xi_function – cody Jan 4 at 16:14
• @cody: Nice "race"! :-) ... – Marzio De Biasi Jan 4 at 19:07