Well, I know how I would solve this problem if I was sufficiently good at packing really complicated damn programs into 512 characters of C, or if I were allowed, say, 10 kilobytes of code. Start with a large number X, a larger number Y, and a powerful proof system. For all programs of size X, search through all proofs of length Y to see if they prove that X terminates. Multiply the runtimes of all the Xs together, or pick the largest one, it won't make any difference.
In this case it doesn't matter much whether you use second-order logic or first-order logic, because what you can prove syntactically in second-order logic is no different from what you can prove in a many-sorted first-order logic. But you do want to pick a powerful proof system like ZFC that can prove the consistency of whole ordinal hierarchies of weaker systems, rather than something weak like Peano Arithmetic; that will make a rather large difference, because it means you'll be able to prove the termination of large recursive structures of programs that do their own searches through all possible proofs etc.
If anyone can come up with a method of producing substantially larger numbers than this using bounded finite runtimes and programs guaranteed to terminate, I'd be quite interesting in hearing it.
It takes programs from a restricted language in which all programs provably terminate. It doesn't take arbitrary programs and search for termination proofs relative to a powerful proof system. There's, um... a really really really LARGE difference.
Based on the way that sort of termination proof usually works, I'd guess there are some simple tree ordinals which grow faster than that language, and that a program based on them would defeat the winner, but I haven't looked into it in detail so it's only a guess.
This is really deja vu all over again. Over 45 years ago I read a "largest number that can be computed with expressions on a postcard" competition in a publication of some college (details escape me as to which college). This was held over a number of issues, and much of this discussion echoes (as far as I remember) that competition. Then, as now, the difficult part was comparing two values computed in completely different ways.
the difficult part was comparing two values computed in completely different ways
I think this is a lot of the fun. But if you wanted to make a similar contest that resolved more easily, what would you do?
Off the top of my head, maybe a contest to most closely approximate a huge non-Mersenne prime in n characters? (Edit: now that I think about it, I’m not sure that the computational complexity of numbers of c. largest-prime size would make that challenging enough for reasonable n. For example, the largest known non-Mersenne prime is apparently 19249·2^13018586+1 … boring.) Or maybe the best PRNG (under a given set of tests) in n characters?
What a weird problem. You're writing in C for a turing machine. Your program has to terminate but you can't use any real-world boundary like CPU time or memory, despite the fact that the most efficient ways of doing this sort of thing in C is to hack binary memory and cast a variable.
It seems like the people writing these programs had a much better idea of the problem definition than the description on the linked page.
Do we need to explain every joke? Of course it doesn't finish. But its output is still very well defined: an infinite string of 9... So my argument was that in a suitable language, I should be able to call atoi() on that string.
I concede this hypothetical language would be somewhat abstract. Maybe it's called maths?
In this case it doesn't matter much whether you use second-order logic or first-order logic, because what you can prove syntactically in second-order logic is no different from what you can prove in a many-sorted first-order logic. But you do want to pick a powerful proof system like ZFC that can prove the consistency of whole ordinal hierarchies of weaker systems, rather than something weak like Peano Arithmetic; that will make a rather large difference, because it means you'll be able to prove the termination of large recursive structures of programs that do their own searches through all possible proofs etc.
If anyone can come up with a method of producing substantially larger numbers than this using bounded finite runtimes and programs guaranteed to terminate, I'd be quite interesting in hearing it.