8 ms·

Can you give a specific finite program which is undecidable?

• pron 2mo ago
  A program that enumerates all theorems in ZFC and stops when it proves a contradiction (e.g. true = false). Encoding a program that is equivalent to that directly as a Turing Machine in merely 748 states: https://www.scottaaronson.com/papers/bb.pdf https://www.scottaaronson.com/papers/bb.pdf (meaning that we cannot prove an upper bound on the 748th Busy-Beaver number, but there are probably even smaller undecidable TMs). But my favourite example (shown here in Java) demonstrates the difficulty of analysing simple, realistic programs without necessarily being undecidable: long foo(long x) { if (x <= 2 || (x & 1) != 0) return 0; for (var i = x; i > 0; i--) if (bar(i) && bar(x - i)) return i; throw new Error(); } boolean bar(long x) { for (var i = x - 1; i >= 2; i--) for (var s = x; s >= 0; s -= i) if (s == 0) return false; return true; } Even in this case where even the input space is finite (and so everything here is definitely decidable), we simply don't yet know whether there is some x for which foo(x) throws, let alone if we made the input unbounded by using BigInteger instead of long.