<p>Sequence <a href="https://oeis.org/A333479" rel="noreferrer">https://oeis.org/A333479</a> in the On-Line Encyclopedia of Integer Sequences mostly answers your question. The question of shortest term for which lack of a normal form cannot be proven in ZFC remains open, but one candidate is the 213 bit Laver program presented in <a href="https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc">https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc</a></p>

CC BY-SA 4.0
2020-04-23T20:27:34.537Z
2020-04-23T20:27:34.537Z
John Tromp
<p>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:</p>

<p>Over all terms in the ULC composed of <code>n</code> abstractions, variables and applications, which has the longest normal form?</p>

<p>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.</p>

<p>Clearly, this function is not computable for arbitrarily large <code>n</code>, 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 <code>n</code>. What values is it known for? What bounds exists for higher <code>n</code>? For what <code>n</code> is the value known to be independent of ZFC?</p>

CC BY-SA 4.0
2019-01-01T19:36:45.327Z
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](https://www.scottaaronson.com/blog/?p=2725).
Marzio De Biasi
CC BY-SA 4.0
2019-01-04T15:58:06.910Z
@MarzioDeBiasi Not that relevant, but people have taken this question pretty seriously, and code golfed it down to 1919 states: https://github.com/sorear/metamath-turing-machines
cody
CC BY-SA 4.0
2019-01-04T16:14:04.930Z
Also, see this: http://googology.wikia.com/wiki/Xi_function
cody
CC BY-SA 4.0
2019-01-04T19:07:10.647Z
@cody: Nice "race"! :-) ...
Marzio De Biasi
CC BY-SA 4.0
2020-02-26T04:35:50.797Z
Just found this thread after posting a similar question at https://mathoverflow.net/questions/353514/whats-the-smallest-lambda-calculus-term-not-known-to-have-a-normal-form
John Tromp
<lo.logic><pl.programming-languages><lambda-calculus>
Busy Beaver Equivalent for the Untyped Lambda Calculus
isaacg
# Busy Beaver Equivalent for the Untyped Lambda Calculus

(Asked by: username_0 on 2019-01-01)

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?

**Tags:** lo.logic, pl.programming-languages, lambda-calculus

> **Comments:**
> **username_1**: 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](https://www.scottaaronson.com/blog/?p=2725).  
> **username_2**: @MarzioDeBiasi Not that relevant, but people have taken this question pretty seriously, and code golfed it down to 1919 states: https://github.com/sorear/metamath-turing-machines  
> **username_2**: Also, see this: http://googology.wikia.com/wiki/Xi_function  
> **username_1**: @username_2: Nice "race"! :-) ...  
> **username_3**: Just found this thread after posting a similar question at https://mathoverflow.net/questions/353514/whats-the-smallest-lambda-calculus-term-not-known-to-have-a-normal-form  

---

## 1 answers

### Answer by username_3 on 2020-04-23. Score: 7 | Accepted answer

Sequence <https://oeis.org/A333479> in the On-Line Encyclopedia of Integer Sequences mostly answers your question. The question of shortest term for which lack of a normal form cannot be proven in ZFC remains open, but one candidate is the 213 bit Laver program presented in <https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc>


---

