A collection of things that are Turing-complete by accident (2013)
beza1e1.tuxen.de
beza1e1.tuxen.de
Great when you want to try and create a computer while trying to fend off goblin attacks and zombies.
Technically, it's not Turing Complete, as the "tape" is not unlimited, but other Turing Complete games have the same issue.
"In this paper, we answer computational complexity questions by unveiling a fundamental mapping between BGP configurations and logic circuits. Namely, we describe simple networks containing routers with elementary BGP configurations that simulate logic gates, clocks, and flip-flops, and we show how to interconnect them to simulate arbitrary logic circuits."
Okay, with some script...
>Here is a video, where a human (not a script!) creates a playable Flappy Bird clone this way.
Wait, what?!
Also the mod community's epScript compiler is itself a very clever feat, especially its use of self-modifying "code".
I was momentarily confused by this until I realized there shouldnt be any commas in that sentence.
(Except maybe the template / type system examples - I hear that's a lot like programming in Haskell)
Surely the point is that this stuff is possible at all. If you really wanted to program something meaningful using BGP hacks, you could build a compiler.
(0) Parsers for context-free grammars
(1) Relational algebra, and the subset of SQL that maps to it
(2) Hindley-Milner type inference
You start with simple and not too-powerful languages (rules systems, regexes, parsing stuff), note they are insufficient for some real-word use case, add one or two features, and bam!, that mess becomes turing complete.
Not only that, but you can also apply more tools onto it, treating the code as data and having a chance to use that as input data for totally different purposes.
Another classic example is structured text. If you want to aggregate facts from that, this is totally easy when the data is available in a simple JSON structure. If it is a simple HTML site, this is slightly more involved: you need to scrape the site and recognize irrelevant stuff ( navigation bars, tables only used for layouting, etc.). But if it is a blob of Flash code that happens to display the text in some shiny way, you are essentially becoming a reverse engineer, and your tool will almost certainly break apart with every change / new version of that structured text.
1. What makes reasoning hard is not quite the halting theorem as normally stated, but a generalization of it that's sometimes called "bounded halting", and was used in the proof of the time-hierarchy theorem, possibly the most important theorem in theoretical computer science. Bounded halting roughly states that it's impossible to know in under N steps whether an arbitrary program P would halt when operating on input X in fewer than N steps. A simple corollary also shows the impossibility of generalizing the program's operation from one input to another. In short, this theorem means that it's impossible to know what a program would do for any input any faster than running it for every input. It can roughly be stated as saying that the verification or "reasoning" complexity for a program with a state space S of size |S| is θ(|S|) (where theta is like big-O, except it roughly means "no more and no less than", whereas big-O means "no more than"). Most importantly, this theorem does not require the programming model to be Turing complete. For example, it applies directly -- using the same proof -- to programming models that only allow primitive recursive functions.
2. Even the simplest computational model -- the barely useful finite-state machine -- is already too complicated for arbitrary reasoning. Its verification complexity also happens to be θ(|S|) (but with a different proof than that of the bounded halting theorem), where |S| is usually at least exponential in the size of the program. In general it can very easily be shown that if your programming languages has nothing more than boolean variables and the ability to write loops of length of no more than 2 or, alternatively, it has subroutines even if they cannot be recursive and there are no first-class subroutines -- reasoning is also infeasible (it's PSPACE-complete) and you might as well be Turing complete, as that won't make the worst-case any harder in practice (it makes no difference if the worst case is truly infinite or "just" much longer than the expected lifespan of the universe). The above fact means it is provably impossible to create a programming language -- no matter how limited -- where every program would be easily verifiable. To make a language feasibly verifiable in all/most cases, its state space must grow slowly (polynomially) with program size; this means that not only must the programming model be weak (basically just FSM), but the language exceptionally inexpressive. Regular expressions are pretty much the farthest we can go, and even then some simple questions about regexps are infeasible (such as whether two regexps are equivalent; I believe that problem is PSPACE complete, even though there are heuristic algorithms that work in many instances).
For further discussion and complete results, see my post: https://pron.github.io/posts/correctness-and-complexity
If you limit it explicitly to models powerful enough to run arbitrary computation, then that sounds reasonable.
But there are a whole lot of situations where a sufficient set of useful algorithms for that given context are computable using models that we can reason much better about if you are willing to throw out the requirement to be able to run arbitrary computations.
A simple example is that you can easily define a model of computation that "solves" the halting problem the crude way: Just add an upper bound to the number of steps, and halt the problem after that number of steps. Now you know any program halts. Make the limit low enough and it actually makes a difference. Of course this model can not compute arbitrary programs. But depending on your needs it may be able to compute sufficiently complex programs.
More reasonable examples would be specialized domain languages like Sieve for filtering e-mail, that address reasoning by having no branching or loops or writable state.
The challenge is that accidentally expanding such a model in ways that accidentally adds back enough power to cause problems in reasoning about the programs is very easy.
This is not true, and precisely the point of my comment. There are no computational models of any wide utility -- no matter how limited -- that we can feasibly reason about in the general case. When I said "arbitrary" I meant arbitrary in whatever restricted model you give me. We can reason about many special cases, but we can (and do) do that for Turing complete languages, too.
> Make the limit low enough and it actually makes a difference. Of course this model can not compute arbitrary programs. But depending on your needs it may be able to compute sufficiently complex programs.
Again, this is not true. Knowing that your algorithm is bounded by some number, gives you no additional information usable in verifying it. There is still no faster way of answering questions than running the program on all inputs up to that number.
> that address reasoning by having no branching or loops or writable state.
If you have no loops (even bounded by a depth of 2) and no subroutines or no variables -- then verification is feasible, otherwise it is at least PSPACE-hard. Such languages may be useful for something, but obviously the vast majority of tasks cannot be done in them.
> The challenge is that accidentally expanding such a model in ways that accidentally adds back enough power to cause problems in reasoning about the programs is very easy.
This is provably impossible unless your don't mind your programs being as long as the worst-case time complexity that they solve. For almost any computational model (barring a couple of very special exceptions), the verification complexity is θ(|S|). As we know the minimum number of states for algorithms, the verification cost is known. The only thing you can do is make the languages so inexpressive that programs increase polynomially or exponentially in size, and so the verification complexity would decrease.
In general, the idea that a weaker computational model makes reasoning easy is a myth (obviously not one shared among researchers). The myth is probably because many practitioners know about the halting theorem but not about more significant computational complexity results, and mistakenly believe that it is that result which is the cause of the difficulty of verification.
I gave you an example: Sieve.
> If you have no loops (even bounded by a depth of 2) and no subroutines or no variables -- then verification is feasible, otherwise it is at least PSPACE-hard. Such languages may be useful for something, but obviously the vast majority of tasks cannot be done in them.
Sieve, as I mentioned fits in this category (though I'd not be surprised if there are extensions that break this; there are many, but the basic language is sufficiently constrained and still useful).
The point is not to do "the vast majority of tasks" in them, but that a wide range of tasks are constrained enough to achievable within different sets of such models, and this is a common way of seeking to contain computational complexity that works well when it is done by care.
(... but leads to unexpected Turing completeness now and again when people don't take care, as the article points out)
E.g. aforementioned Sieve is constrained this way explicitly to be safe to let end-users -- or scripts on their behalf -- construct Sieve filters to run during delivery on mail servers without e.g. having to impose any other restrictions than a size limit.
> This is provably impossible unless your don't mind your programs being as long as the worst-case time complexity that they solve.
I think you misunderstood what I wrote. The sentence you quoted here is arguing that people make mistakes when defining the kind of restricted languages I'm discussing all the time so that verification gets harder. You seem to think it was talking about making verification easier.
> In general, the idea that a weaker computational model makes reasoning easy is a myth
And again: This is flat out wrong without adding the caveat that you're talking about arbitrary computation rather than languages that are specifically and intentionally constructed to prevent arbitrary computation.
Here's one:
Consider a machine whose only instruction is "halt", which halts execution.
I said "of wide utility". BTW, I don't know Sieve, but if it has regular expressions then reasoning about it is also infeasible (e.g. checking whether two filters based on regular expressions are equivalent).
> but that a wide range of tasks are constrained enough to achievable within different sets of such models, and this is a common way of seeking to contain computational complexity that works well when it is done by care.
I don't know what "a wide range of tasks" means, but even regular expressions are not limited enough for general reasoning. Anything that requires regular expressions and beyond is already infeasibly verified in the general case.
> This is flat out wrong without adding the caveat that you're talking about arbitrary computation rather than languages that are specifically and intentionally constructed to prevent arbitrary computation.
No. I'm talking about arbitrary programs in whatever language you give me. If your language has regular expressions -- game over. If it has variables and subroutines/limited loops -- game over. And those are just the PSPACE-hard cases. If all you have in your language is boolean connectives (i.e., it's a propositional calculus) -- no subroutines, no loops and no mutable variables -- verifying it is "just" NP-hard. Special cases, on the other hand, are often possible to reason about even automatically even in Turing complete languages.
> You may intend a "useful" in there somewhere, in which case I point you again to Sieve, which is still trivial enough unless you carelessly add extensions.
I did say useful, and either Sieve is not very widely applicable and/or, if it has regular expressions it cannot be feasibly reasoned about.
And they are of wide utility, even though they may not satisfy your expectations to just how wide utility you want. But that is exactly the point - they're not meant to.
The claim I made, and that others here have made, that you've been arguing against is not about general purpose languages. I've pointed that out several times.
On the contrary the point is explicitly that there are benefits in isolating parts of problems and explicitly avoiding general purpose languages exactly because I agree that you won't gain much from trying to find weaker models for general purpose languages.
So when you keep bringing up more general computation, you keep arguing against a point I at least have not made.
I've never disputed that there is little to gain from trying to weaken the computational models for general purpose computation.
What we can do, and often do is to reduce the practical problems of working on these systems by lifting subsets of problems out of general purpose languages and into much weaker special purpose environments.
Since you keep bringing up regular expressions, for example:
> but if it has regular expressions then reasoning about it is also infeasible
... this is exactly one of the reasons why Sieve doesn't have them (at least not the base language) - it's limited to basic wildcards ("","?", specific strings). On top of that the implementation is allowed to terminate execution after an implementation defined number of execution steps, so it does not need to even deal with the worst case for a wildcard engine if someone tries to feed it pathological strings.
> I don't know what "a wide range of tasks" means, but even regular expressions are not limited enough for general reasoning. Anything that requires regular expressions and beyond is already infeasibly verified in the general case.
I've repeatedly pointed out that the entire goal of these languages is to prevent* general reasoning. That is a feature, not a flaw.
> No. I'm talking about arbitrary programs in whatever language you give me.
... in which case you're not addressing the comments of mine that you've replied to, and we're in violent agreement about something that is irrelevant to my argument.
A language that has no variables, no loops and no subroutines (and no regexps) is as far as you can go while remaining feasibly verifiable. There aren't many other options. What portion of our applications can be written in such languages? That people add extensions to Sieve only shows that its trusted portion isn't widely-enough useful even for the task of filtering email.
It's not a question of general-purpose vs. DSL. Regardless of what the language is for, with no loop, subroutines and variables there is very little you can do.
> I've repeatedly pointed out that the entire goal of these languages is to prevent* general reasoning. That is a feature, not a flaw.
It's not important, but that's not what I meant by general reasoning or arbitrary computation. What I meant is that no matter the language you give me (assuming it's useful enough etc.), answering arbitrary questions about arbitrary programs in that language is not feasible. For example, regular expressions do not allow "arbitrary computation" in the Turing completeness sense, yet it is infeasible to feasibly answer arbitrary questions about arbitrary regular expressions, such as the question "are two regular expressions equivalent?" This is a very important question about regular expressions, but it cannot be feasibly answered for arbitrary regular expressions.
Most extensions to Sieve still retain the same constraints. A few don't, sometimes because peoples needs are different: E.g. someone using it for their own mail server or a corporate mail server where it is possible to yell at the person who turned their mail script into a fork bomb has very different requirements from one that lets "anyone" sign up, for example. That's a good reason for why the extension mechanism is there.
As for examples of other things you can do: There are a number of templating languages, for example, that can be demonstrated to always terminate and otherwise be feasible to reason about. I've personally written such template engines also because it was a useful way of preventing the developers from doing stupid things (the ingrates then tried to sneak in a directive to embed a perl interpreter behind my back at one point).
You can do a lot more than you might think in such engines by e.g. providing primitives for filtering and iteration over nodes in input graphs (as long as you can't mutate the collections, and there are appropriate termination guarantees e.g. by preventing loops)
Another highly useful example that springs to mind is BPF, which while it started as a basic packet filter (e.g. for tcpdump) is increasingly powering much more functionality on Linux for e.g. tracing, and such as for example kernel level enforcement of system call constraints (you can define filters to apply to subsequent code that e.g. outright rejects certain system calls, or applies comparisons to the system call arguments to decide whether to allow or reject them).
But I'd say the question you're asking is the wrong one, though. The original point was that when approaching a problem, there is substantial value to be had by asking "how can I subdivide this problem so that as much as possible can be restricted to a less powerful subset?" The Rule of Least Power, basically.
Often you will end up with dynamic subsets that are hard to reason about, but as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the problem, and gain the ability to reason about the rest.
You don't even need to create full blown languages to get this effect - changing the way you write code and effectively create a DSL in the form of API's can often achieve the same effect, but isolating "dangerous" functionality to separate languages often makes it harder to violate the requirements.
> It's not important, but that's not what I meant by general reasoning or arbitrary computation. What I meant is that no matter the language you give me (assuming it's useful enough etc.), answering arbitrary questions about arbitrary programs in that language is not feasible
That'd be reasonable apart for setting it up for a No True Scotsman with your "assuming it's useful enough etc.". As we've seen with your objections to Sieve, the languages I'm talking about appears to be languages you don't find "useful enough." Since your objections applies to a different set of languages than those I'm talking about, your objections are moot.
Alas, this was proven wrong for verification in 2005. See https://pron.github.io/posts/correctness-and-complexity#corr...
> Since your objections applies to a different set of languages than those I'm talking about, your objections are moot.
1. I reject your examples on the ground that they're considered insufficient for their own domains, and in any case are so restricted that you could not compose the lion share of an application from them even without the theorem showing that you cannot reduce the cost of composition by verifying simple components.
2. While I'm happy to further ponder the utility of the languages you listed, you should bear in mind that, say, a Java program using similar constructs to a Sieve program can be reasoned about automatically by current tools, and with relative ease. In other words, a program so simple is easy to reason about whether it's written in a restricted or a non-restricted language, so using those DSLs just increases the cost of verification. However, that does not mean they are not useful. For example, I read that the main design object of Sieve is to allow servers to run untrusted code.
Take SAT solvers, for example. Since propositional logic encoded in CNF is so restrictive, we can find and implement relatively simple heuristics that solve huge, real-world problem instances in a reasonable time. The same propositional formula can also be represented by a C program which is much, much smaller [1], yet the best heuristic to determine whether the C program outputs 1 for any of its possible inputs, might be to run it once for each input combination (which would take longer than the age of the universe for even 10k variables).
[1] "Proof": the CNF is typically generated from a hand-written program in a practical programming language; therefore, the program represents the propositional formula.
Do you have any evidence for that? I have not seen this claim made anywhere. The reason is that heuristics apply in cases where the problem at hand can be stated in terms of a lower-complexity problem, and that happens regardless of model. Is there empirical data showing this is happens more often in restricted models? Intuitively, I see no reason why it should.
> Take SAT solvers, for example.
SAT is NP-complete, which is (well, we don't know for sure, but that's the working hypothesis) much easier than even verification of FSMs (PSPACE-complete). We don't have any similar working heuristics for, say, TQBF (PSPACE-complete), and even SAT solvers fail often.
> yet the best heuristic to determine whether the C program outputs 1 for any of its possible inputs, might be to run it once for each input combination (which would take longer than the age of the universe for even 10k variables).
Most autoamtic software verification doesn't work like that at all, but through a process called abstract interpretation which can conservatively project the problem onto a much smaller state space (that is basically one way to look at how type systems work). The beauty of SAT solvers is that they require no such semantic approximations, and appear to work on arbitrarily difficult problems (except when they don't). So far, they work by magic -- we don't know why they're so effective in practice. But the hope of finding such a general algorithm that happens to work on many real-world instances of problems that are at least PSPACE- or 2EXP-hard problems are not great. It all comes down to studying special cases, and I don't see a particularly good reason (and I haven't encountered any research to that effect) for how to make such "good" instances more likely using some restricted language.
Are you asking for studies? How would you even rigorously define the hypothesis?
> SAT is NP-complete, which is [...] much easier than even verification of FSMs (PSPACE-complete).
So? How does that invalidate my example?
> The beauty of SAT solvers is that they require no such semantic approximations, and appear to work on arbitrarily difficult problems (except when they don't). So far, they work by magic -- we don't know why they're so effective in practice.
But that's the point! For real-world problem instances, you'll find that automatically SAT solving a CNF model works much better than applying an automatic theorem prover to the C program that generated the CNF model. That's because in practice, it's easier to design heuristics that work on a propositional formula than it is to design heuristics that work on CNF-generating C programs. If that were not true, then we wouldn't need SAT solver – we'd just run the automatic theorem provers on the C programs that generate the CNF model.
> I don't see a particularly good reason (and I haven't encountered any research to that effect) for how to make such "good" instances more likely using some restricted language.
And yet it works extremely well in the case of the CNF-generating program vs. SAT solving the generated CNF model. That is a pretty strong argument, you cannot just dismiss it because PSPACE harder then NP.
Preferably studies, but even intuition would do at this point. You don't need to rigorously define the hypothesis, just demonstrate which kinds of patterns susceptible to commonly applied automated reasoning occur more frequently when the same application is written in a TC or non-TC language. The thing is that it's often easy to recognize special cases even in TC languages (e.g., deducing that a function is total in a TC language is easy in those cases where the function resembles those used in non-TC languages).
I'm not saying languages can't make verification easier. For example, recognizing a terminating loop may be a bit easier in a language with `for` loops than in a language that only has a `goto` construct, and a language with less/no aliasing makes local reasoning much easier; I'm saying that that help does not stem from restricting the computational model (just as removing `goto` does not reduce the computational power). Turing-completeness in itself is a red herring when it comes to the question of how languages can help verification.
But I don't understand even the general line of your argument. Even supposing that SATing a CNF formula automatically generated from C is easier than other approaches (it isn't), this does not show that writing CNF directly is more advantageous than writing C. After all, a simple mechanical translation exists, so why should I write CNF formulas if writing equivalent C code is easier?
> you'll find that automatically SAT solving a CNF model works much better than applying an automatic theorem prover to the C program that generated the CNF model.
It doesn't, though. Many automatic problems are easier to verify using abstract interpretation than SMT.
> So? How does that invalidate my example?
That a magical 50-year-old algorithm that no one understands to this day happens to exist for the very simplest of intractable problems does not mean that we can hope for similar success for much, much harder problems. When it comes to program verification, SAT (used in SMT) is effective only in a very controlled and limited way (I know because I use formal verification). No one believes SMT solvers could be extended to verify full programs.
Maybe this example helps: I should be easier to write analysis heuristics for a language that only allows loops of the form "for i = 1...n" than for one which also has while-loops, gotos, and unrestricted C-style loops. Maybe not from a theoretical point of view – after all, both languages are equally Turing-complete – but from a practical one, since there are more language constructs that have to be covered by the analysis. Sure, you can mechanically translate all loops from the second language to "for i = 1...n" loops, but that transformation is not trivial and has to be implemented first.
> But I don't understand even the general line of your argument. Even supposing that SATing a CNF formula automatically generated from C is easier than other approaches (it isn't), this does not show that writing CNF directly is more advantageous than writing C. After all, a simple mechanical translation exists, so why should I write CNF formulas if writing equivalent C code is easier?
My point isn't that we should hand-write CNF formulas. What I'm saying is, that automatically solving CNF formulas is easier than automatically solving a C program that expresses the same thing.
Example: a Sudoku solver. Given a partially filled 9x9 matrix,
* ) Program 1 takes as input an assignment for the unfilled fields (free variables). It outputs yes/no indicating whether the input satisfies the Sudoku rules.
* ) Program 2 generates a CNF instance which encodes the Sudoku rules and the partially filled matrix. The variables represent the unfilled fields.
Program 1 and the output of program 2 are equivalent in the sense that they encode the same problem instance, but the CNF generated by program 2 is in a much more restricted language than program 1. You can write a decent (although not state-of-the-art) CNF parser and SAT solver in a few 100 lines of code, but you will be hard-pressed to write even the parser for a general C program in that space, let alone something that can understand C's semantics, an automatic solver using abstract interpretation, and some heuristics to speed things up (only those heuristics are allowed to be somewhat tailored to this type of problem, everything else has to be general-purpose – just like the SAT solver, which is general purpose and has a few heuristics that speed up many practical instances).
Quite possibly, and that's exactly what I said. Languages may assist formal reasoning (although how is not always clear[1] and your example may or may not be valid -- the transformation in the well-behaved cases may be quite easy; compilers and static analyzers do such analysis all the time), but that's not due to a weakening of the computational model.
> What I'm saying is, that automatically solving CNF formulas is easier than automatically solving a C program that expresses the same thing.
Right, but as the transformation is mechanical, there is no reason to prefer one language over the other. They're equivalent -- in this particular scenario -- from both a theoretical and a practical point of view. Static analyzers commonly perform transformations -- from the programming language to SMT-LIB and/or using abstract interpretation.
> but you will be hard-pressed to write even the parser for a general C program in that space
Writing a compiler for Pascal is much harder than writing an assembler. That's not an argument for writing assembly by hand over writing Pascal.
[1]: One example is a pure-functional language like Haskell vs. an imperative one like Java. Well-behaved Haskell allows for equational reasoning while Java "only" allows for assertional reasoning, but the common use of higher-order functions makes some automatic reasoning methods much harder than the familiar and powerful assertional reasoning approaches.
Most SQL variants [1] and map-reduce [2] are Turing complete. They are easier to optimize in practice because they tend to be small and simple (compilers often make similar optimizations for similarly-sized general purpose programs) and because they express the parts that are important to optimize for that particular problem (data-dependence and parallelism) in a direct way -- not because of the computational model.
You could argue that because SQL is cumbersome for general-purpose programming it helps ensure programs are small and simple, but most people would rather not write their application in SQL, and if they did, it would no longer be small and simple.
[1]: https://stackoverflow.com/questions/900055/is-sql-or-even-ts...
[2]: https://www.quora.com/Theoretically-can-any-algorithm-be-imp...
Perhaps a better example is the humble Regex. If we have a true regular language, we can optimise it via a DFA to have O(N) runtime. The weak computational model is enabling this optimisation.
Termination and exponential (or super-exponential) running times are about equally bad. Avoiding either is done on a case-by-case basis. Restricting the language can save you from one and not the other.
> If we have a true regular language, we can optimise it via a DFA to have O(N) runtime. The weak computational model is enabling this optimisation.
I'm not an expert on regex by any means, but I believe this optimization is exponential (a DFA can be exponential in the size of the regex), and so infeasible in practice. Regardless, as I said, regex is about as far down as we can take computation, and regexps make for a very poor generally useful computational construct.
That's a significant improvement then
(Apologies if this is me-too ism)