3 ms·
That's basically what the winning entry does.
by defen 16y ago
That's basically what the winning entry does.
- Eliezer 16y agoNnnnnoooo... no, it does not. 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.
- Eliezer 16y agoE.g., it's possible (haven't checked) that TREE would defeat the winner: http://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem http://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem