3 ms·

I knew that there was a proof, but never read the paper before. Now that I did, I think that proof is garbage tbh. For Turing completeness, a fixed, constant-s

I knew that there was a proof, but never read the paper before. Now that I did, I think that proof is garbage tbh. For Turing completeness, a fixed, constant-sized program needs to be able to handle arbitrary inputs and use arbitrary amounts of memory. It's important to distinguish the model from the implementation here. Theoretically, a language like Python is Turing complete. (And BTW you don't need infinite precision integers or anything fancy: you can simply simulate the tape with an object graph.) Practically, every Python program running on a real computer will run out of memory eventually. Anyway, the translated Z3 programs in this paper contain one case statement for every possible memory location. This means that for a given program size, you're limited to run in O(1) space. That's only as powerful as a finite state machine, not a Turing machine. I see nothing in the paper that convincingly addresses this limitation. There are some arguments to the effect that practical CPUs have limited address space as well. Which is true, but that argument only shows that those aren't Turing complete either, not that the Z3 magically is. Maybe there's a subtle point that I overlooked, but at the moment, I'm simply not convinced.

formerly_proven 6y ago
Z4/ETH-Edition has conditional jumps, which makes it much less contentious.
cameldrv 6y ago
Ultimately there is no real computer that is Turing complete, because all real computers are finite. Ultimately, you can represent any real computer with a (very large) DFA. The two things missing from what would normally be considered a universal computer are conditionals and indirect addressing. The Z3 is also limited in that it executes a specific finite set of instructions in linear order, with no branching. In the proof, they get around the finite length of a program by literally creating a loop -- they glue one end of the paper tape of the program to the other so that the computer can keep executing the same instruction stream forever. Then they get around the lack of indirect addressing by accessing every memory location in every loop. I agree that it's very much a stretch to call the Z3 Turing complete.
- formerly_proven 6y ago
  Wouldn't a DFA for a computer have to have 2^n states for n bits of memory, so it's size would be exponential to memory size of the computer? So even for a pedestrian 640K of memory, that's like 10^10^7 states. Sounds a lot like trying to simulate a non-deterministic Turing machine on a deterministic machine; the state space explodes exponentially making it intractable.

formerly_proven 6y ago

Z4/ETH-Edition has conditional jumps, which makes it much less contentious.

cameldrv 6y ago

Ultimately there is no real computer that is Turing complete, because all real computers are finite. Ultimately, you can represent any real computer with a (very large) DFA. The two things missing from what would normally be considered a universal computer are conditionals and indirect addressing. The Z3 is also limited in that it executes a specific finite set of instructions in linear order, with no branching. In the proof, they get around the finite length of a program by literally creating a loop -- they glue one end of the paper tape of the program to the other so that the computer can keep executing the same instruction stream forever. Then they get around the lack of indirect addressing by accessing every memory location in every loop. I agree that it's very much a stretch to call the Z3 Turing complete.

formerly_proven 6y ago
Wouldn't a DFA for a computer have to have 2^n states for n bits of memory, so it's size would be exponential to memory size of the computer? So even for a pedestrian 640K of memory, that's like 10^10^7 states. Sounds a lot like trying to simulate a non-deterministic Turing machine on a deterministic machine; the state space explodes exponentially making it intractable.