xorvoid / meson-brainfuck

A proof that Meson is actually Turing-Complete
20 stars 0 forks source link

Does not actually constitute a proof of Turing completeness #1

Open jpakkane opened 4 years ago

jpakkane commented 4 years ago

I'm glad you like the Meson build system, but this is not really a "proof" of Turing completeness. The mathematical definition of Turing completeness is very specific. It is not "takes a very, very, very long time to get to the result" but instead it ties to the Halting problem. Specifically, determining whether a program will exit for all possible inputs.

To prove that this is not the case, we need to show that we can prove that Meson execution will end in finite time for all possible inputs. If we can, the halting problem for this problem is not undecidable and thus the language is not Turing complete. The proof splits into two parts:

  1. All statemens that are not foreach take one step to execute and executing them will not cause a step that has already been executed to be re-executed.
  2. foreach statements are executed at most n times where n is the size of the array iterated over and since the array can not be altered while iterated over, this operation takes only a finite number of steps.

Therefore it follows that if the Meson build definition being processed has x regular operations, y foreach statements and the largest one of them has z suboperations, an upper bound on the total number of steps is tot = x + y*z. This is finite for all programs of finite size and Meson will terminate after executing a finite number of steps. Thus the system is not Turing complete.

The "flaw" in the original reasoning is this:

most programmers seem to agree that any language that can implement a brainfuck interpretor is turing-complete

This is true, but strictly speaking that script does not implement a Brainfuck interpreter. It implements an interpreter with a finite upper bound on the number of steps it can execute. Those are not Turing complete by the same reasoning as above.

The easier way of making the claim that Meson is Turing complete is that run_command can execute arbitrary programs. But even then the Turing completeness is outside of Meson. Or at least that is my excuse and I'm sticking with it. :)

xorvoid commented 4 years ago

Seems like a pretty flimsy, overly pedantic argument. If this is the logic, then we might as well conclude that no programming language is turing-complete (which is true). All practical computing is finitely-bounded (if only due to hardware eventually failing). But, either way this makes the claim that "Meson is not Turing-complete, and never will be" pretty pointless, and quite misleading. My point here is that avoiding "Turing-complete-ness" really isn't that interesting and in fact isn't even what you are trying to do. You're trying to design a good DSL for build definitions, while preventing the DSL from being used for more general-purpose tasks.

Volker-Weissmann commented 3 years ago

I'm a bit late to the party, but here is why what jpakkane says makes sense:

It is true that every finite bounded system is not turing complete. But there still is an important difference between e.g. the Meson DSL, which is turing incomplete by desing and e.g. Python, a language that would be Turing complete if it had infinite memory.

In a Turing complete system (e.g. Python with infinite RAM), the halting problem is insolvable. In e.g. Python with finite RAM, the halting problem is solvable, but it might take extreme amounts of memory and time to solve. even if the Python code does not look like analyzing it will take extreme computing power. In a by-desing-turing-incomplete language, the halting problem is solvable, and it will only take extreme amount of memory and time to solve it if the code looks like analyzing it will take extreme computing power.

Consider this Python code:

i = int(sys.argv[1])
while i != 1:
    if i % 2 == 0:
        i /= 2
    else:
        i = i * 3 + 1

this code does not look like it takes a lot of computing power to analyse, but it will take an EXTREME amount of computing power to solve the halting problem: To solve the halting problem for this code, you need to to simulate it for all integers that fit into memory. This means you will have to simulate a finite, but giant amount of cases. For all practical purposes, you cannot solve the halting problem for this simple python code, even if its turing incomplete due to finite memory.

If you want to write code in a by-desing-turing-incomplete-language where the halting problem takes a lot of time to solve, you cannot use smart "i *3 + 1" trickery like in the python example, because the meson dsl allows no such loops. The only thing you can use to drastically increase the time it takes to solve the halting problem is by nesting a lot of foreach _ : large_array loops. What does this mean in practice for meson:

I don't know much about meson, but I assume that in order to build your code, meson needs/wants to calculate some property of your meson.build script that is impossible to calculate if the meson.build language would be turing complete (Similar to calculating wheter your meson.build script halts.). If the meson.build language would be python this would mean that writing some innocent looking python code, might result in finite, but extreme (> 1 year) build times. If the meson.build language is the meson-dsl, writing some innocent looking code cannot greatly increase the build time. You can still greatly increase the build time by using large nested loops e.g.

foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
foreach _ : [0,1,2,3,4,5,6,7,8,9]
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach
endforeach

would takes about a thousand years (if my calculations are correct) to run $ meson setup on my machine. This is an inacceptable amount of time, but it is obvious to the user that this code is slow.

The difference is that if a user writes some innocent looking code and it takes years to build, he will be mad at meson, but if the writes some large nested for loops and it takes years to build, he will not be mad at meson (because lots of nested loops are slow in every language, its not a meson-specific problem), but he will try to cleanup his nested loops instead.

When jpakkane says: "We want to stay turing incomplete" he really means: We never want to be a million times slower than any other build tool. Your code with nested loops don't count, because nested loops are slow in every programming language. If meson would use python in its meson.build file, then situations would exist where meson is a million times slower than another build tool (e.g. if meson needs to simulate the i=i*3+1 algorithm for all numbers that fit into memory, but another build tool wouldn't need to).

If jpakkane says: "The meson dsl is turing incomplete and python is turing complete" he really means: If meson would use Python for its meson.build files, you could write innocent looking code, that result in $ meson setup taking years (but not forever). But if meson uses the meson-dsl for its meson.build files, you cannot write innocent looking code that results in $ meson setup taking years. You can still write heavy-to-calculate looking code that result in $ meson setup taking years (but not forever).

Because the argument above is very long and ugly, theoretical computer scientist usually just say that every computer got infinite amount of memory. Then the paragraphe above simplifies to:

If jpakkane says: "The meson dsl is turing incomplete and python is turing complete" he really means: If meson would use Python for its meson.build files, you could write code, that result in $ meson setup taking forever. But if meson uses the meson-dsl for its meson.build files, you cannot do this.

The reason meson, but not other build tools cares about not being turing complete is that meson tries to "analyse" the meson.build file more than other build tools "analyse" their config files. And turing complete languages are more difficult to "analyse" than non-turing complete languages.

I hope you can follow my explanation. Sometimes theorists fail to explain how their concepts translate into the praxis.

alexreinking commented 1 year ago

then we might as well conclude that no programming language is turing-complete (which is true).

Python, a language that would be Turing complete

@Volker-Weissmann @xorvoid -- This is not true.

Python as a language is Turing complete, but computers are not Turing machines. They're finite-memory approximations. The distinction between a Turing-complete language and a specific Turing machine matters. Python does not define its memory pool to be finite.

Meson is not Turing-complete even as a mathematical object, given infinite memory. As @jpakkane observes, there is no Halting problem for Meson since it is easy to show that all Meson programs terminate. Some Turing machines do not terminate. That ought to close the book on this argument right there.

To address the construction in this repo, and see why it does not constitute a proof of Turing-completeness, let's look at what is here. It's one member of a family of Meson programs that simulate a brainfuck interpreter to exponentially many (in the size of the program) steps. To actually "reach" infinitely many steps, you would need to include infinitely many nested foreach loops. Turing machine programs are not infinite in size by definition. So this shows you can do interesting finite things in Meson, but it falls short of being a proof of Turing completeness.

eli-schwartz commented 1 year ago

Added to that...

My point here is that avoiding "Turing-complete-ness" really isn't that interesting and in fact isn't even what you are trying to do. You're trying to design a good DSL for build definitions, while preventing the DSL from being used for more general-purpose tasks.

This is wrong, or debatably wrong, as well. The fact that Meson avoids Turing completeness by design, also has impacted what sort of things you can do with the DSL.

... At least, what you can reasonably do in a way that doesn't constitute outright obfuscation. Since no overtly Turing-complete functionality is available, even faking it with "really big loops" results in un-idiomatic meson.build files, suitable for having playful fun but not much else.

...

There's another project that also plays with this idea; appropriately, it was released on Halloween for that extra-spooky behavior: https://github.com/annacrombie/meson-raytracer/

It's directly based on the famous CMake raytracer, oft-cited as a reason why the CMake language is "bad". As you can see by looking at the Meson one, @annacrombie used a similar tactic of "loop with a really big number" and a flat main function (with an actual honest-to-goodness VM to try to hide as much from the main loop as possible and avoid repetition).

Once again, it falls short of true Turing completeness, because it mathematically fails to encounter the Halting problem.

But it does show what you need to be willing to do in order to have function-like behavior.

Also, fun fact: the meson raytracer takes a day to complete, because the fancy VM gets a clock speed of 381 Hz, which is probably tolerable for a build system but less so for a programming language. The c99 implementation can push 26,685 and completes in a mere 15 minutes.

The hidden benefit of being really slow in an academic sense? You decide.