4 ms·
The proof that the Z3 is turing complete is pretty funny: https://news.ycombinator.com/item?id=1945455 https://news.ycombinator.com/item?id=1945455 http://www
by 7373737373 6y ago
The proof that the Z3 is turing complete is pretty funny:
https://news.ycombinator.com/item?id=1945455 https://news.ycombinator.com/item?id=1945455
http://www.inf.fu-berlin.de/inst/ag-ki/rojas_home/documents/1997/Universal_Computer.pdf http://www.inf.fu-berlin.de/inst/ag-ki/rojas_home/documents/...
- pmiller2 6y agoI clicked through the first link because I wanted to see what was "funny" about it. Turns out, the way you simulate a Turing machine on the Z3 is very similar to the execution model of AWS step functions. https://aws.amazon.com/step-functions/ https://aws.amazon.com/step-functions/
- codeflo 6y agoI 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 agoZ4/ETH-Edition has conditional jumps, which makes it much less contentious.
- cameldrv 6y agoUltimately 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 agoWouldn'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.
- kens 6y agoHistorians say: the "argument that Konrad Zuse's 1943 Z3 computer was universal was an impressive party trick, but diverged entirely from the way the machine was designed, how it was actually used, or indeed from anything that would have made sense in the 1940s... To us, the real lesson of his analysis is that the Z3 could have been Turing complete with only minor design changes, but that it wasn't because the concept and its benefits were not yet widely understood." I agree with that analysis and think Turing-completeness is overrated.