5
$\begingroup$

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?

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ 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. $\endgroup$
    – Marzio De Biasi
    Jan 1, 2019 at 19:36
  • $\begingroup$ @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 $\endgroup$
    – cody
    Jan 4, 2019 at 15:58
  • $\begingroup$ Also, see this: googology.wikia.com/wiki/Xi_function $\endgroup$
    – cody
    Jan 4, 2019 at 16:14
  • $\begingroup$ @cody: Nice "race"! :-) ... $\endgroup$
    – Marzio De Biasi
    Jan 4, 2019 at 19:07
  • $\begingroup$ Just found this thread after posting a similar question at mathoverflow.net/questions/353514/… $\endgroup$
    – John Tromp
    Feb 26, 2020 at 4:35

1 Answer 1

Reset to default
5
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.