What Computers Cannot Do: The Consequences of Turing-Completeness
yzena.com
yzena.com
> This was “easy” because the other major thing about UTM’s is how well they generalize to proving that just about any property of an algorithm is not computable, in the general case.
This paraphrasing of Rice's theorem is good enough, but the mathematical result is meaningless in the practical Turing Complete sense. Rice's theorem is misused often on the internet to put limits on static analysis, but in most cases you can successfully prove that a given program terminates. And by proving that, Rice's theorem no longer prevents you from proving anything.
> That looks like an unprovable property, which is exactly what you would have in a Turing-complete language.
> ...
> In essence, your language is still Turing-complete in practice.
The implication of this statement is that because it is not obvious how to prove a given statement, it must be impossible to prove ANY statements in the general case. No additional argument beyond Rice's theorem has been given to explain why proving other properties would be impossible in the general case.
It is exactly this thought process that makes me strongly dislike Rice's theorem. It is easy to decide that "I must not be able to prove this because its impossible" even when it is practically provable.
Strong static typing? It's generally possible to write valid programs (i.e., that would run successfully without runtime errors) that don't type-check successfully. So the set of type-safe programs is smaller than the set of useful programs. Is that an argument for discarding type safety? No, because the vast majority of programs we want to write can be type-checked and it's useful to do so.
Termination checking? This post has a nice example of an effectively-non-terminating loop in Bazel. Bazel's control language doesn't have unbounded loops, so the author just nests a bunch of very long loops. It's fun, but "it's possible to write a Bazel build script that takes an infeasibly long time to run, effectively infinite" doesn't seem like a problem in practice. It's still hard to write such a thing accidentally!
No, I do not.
The real world consequences of this problem are something we have become desensitized to. I didn’t quite understand the impact of the halting problem until I started working in security, specifically for a company that made a SAST product and I had to support the scanner for companies across the globe. There will always be a 0-day market because of Halting problem.
If you think down the road 20 years. Virtually everything we touch will have internet. It will all depend on a program checking a program. Since no computer can guarantee its correctness on its own. Exploits will always be able to chained, and everything will always be exploitable. Including AI systems.
A book I read had a quote that said if you want to make a product that will generate infinite profit, create a static analysis scanner.
I’m not a mathematician but the Halting problem always reminds me of the Godels incompleteness theorem in a way.
I think these are the greatest gifts humanity has ever discovered.
It means there is always hope for humanity as long as oppression depends on technology, because the technology will always be flawed.
There is always a undiscovered theorem that has to potential to change everything we know.
Good point. Also, discovering exploits is also equivalent to the halting problem. So both things are impossible in the general case.
ISBN is 3423300175.
I really appreciate your comment. That book has been sitting behind me on my bookshelf for years blending into background. I just pulled it off the shelf.
I just graduated a few weeks ago after working on my BS for 10 years. The fact that you brought this book up, the piece that inspired me to go back to school in the first place… is something Hofstadter would probably refer as my minds I recursive loop of existence. Something of that sentiment at least
This is relevant for security, because entire operating systems have been formally proven to adhere to their specification/free of all bugs: https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
2. Even proving anything about finite state machines is NP hard so the problem is harder than just using weaker model of computation.
3. Proofs are not reuable: proving something about one program does not tell us anything about other programs.
See excellent https://pron.github.io/posts/correctness-and-complexity for more details.
> 1. Unfortunately the set of "some" programs is unknown and most probably really small.
Many useful algorithms can be proven to terminate. Compare against the situation in mathematics: many theorems are not be provable, but that does not stop us from trying to prove useful theorems, or recognizing that a given theorem has already been proven.
> 3. Proofs are not reuable: proving something about one program does not tell us anything about other programs.
This is true in the sense that a proof of arbitrary program A does not tell us anything about many other programs. But it is clear for example that if, say a program is recognized by inspection as the concatenation (splicing the final states and initial states together) of two programs that terminate, then this program terminates.
Even the link you provide gives optimism and claims that
> Now we know why writing correct programs is hard: because it has to be. But while we cannot verify all programs all the time – regardless of how they’re written – there’s nothing stopping us from verifying some programs some of the time for some properties.
I would say that one small piece of software (Sel4 is only 9,400 SLOC!) always cited as an example is actually a very small set of programs that can be formally verified. I haven't heard of a formally verified web browser...
> Many useful algorithms can be proven to terminate.
Proving that a program terminates is not that much interesting. Lack of security vulnerabilities would be much better.
> But it is clear for example that if, say a program is recognized by inspection as the concatenation (splicing the final states and initial states together) of two programs that terminate, then this program terminates
But it does not tell us anything about real programs? We don't compose software by concatenating their state machines.
> Even the link you provide gives optimism and claims that
This is a call for empiricism (aka testing) and ad-hoc heuristics exactly because the problem is not solvable in general using formal methods.
> Proving that a program terminates is not that much interesting. Lack of security vulnerabilities would be much better.
My bad, I dare make the stronger claim that most algorithms that you see in an undergrad algorithms textbook are useful and mathematically known to be correct.
> But it does not tell us anything about real programs?
I agree that most software today are extremely complicated. Most software today don't even have a proper target specification all in one place, which is kind of a prerequisite for being proven to adhere to a specification. Furthermore, most software today is so complex that attempts at a rigorous specification is likely to have bugs at the level of stating the property itself. Not to mention completely missing properties that one is unaware of that are relevant to attacks that one is unaware of.
But core parts of real software is composed of those undergrad algorithms that are proven to be correct. You can create useful libraries of useful algorithms that have guarantees, and small programs that have guarantees. For this reason I disagree that the class of useful programs is as small as you think.
> We don't compose software by concatenating their state machines.
Structured programming without loops can be modeled as concatenation of turing machines (branching composes different machines to the accept and reject states); and it is trivial that it terminates once the component machines terminate.
When you introduce a loop that is when you need to identify a nontrivial property that guarantees that the loop terminates, and this is done work for many useful algorithms.
They are reusable to some degree when the proofs are made with type systems, via Curry-Howard.
There's several very dubious claims that are stated way too confidently like this in the article, like "Yep, virus scanners are almost completely useless"
Yes, the lambda calculus can. They are equivalent.
But Turing's machines gave us the model to think that way. In my opinion.
Btw: I think your site would look better with left justified text. Right justified looks best only for long paragraphs (books).
> Universal Turing Machines The idea of UTM’s is that you can have Turing Machines running other Turing Machines.
Just like you can have lambda terms running other lambda terms [1] [2]. In fact an additvely optimal [3] universal lambda term can be as simple as
┬─┬ ────────────────────────────────────────────────────┬─┬── ┬────────
└─┤ ────────────────────────────────────────────────────┼─┼─┬ │ ┬─┬ ┬─┬
│ ┬───────────────────────────────────────────────────┼─┼─┼ │ └─┤ ├─┘
│ │ ──┬────────────────────────────────────────────── ├─┘ │ │ ├─┘
│ │ ┬─┼─────────────────────────────────────────────┬ │ │ ├───┘
│ │ ┼─┼─┬─────────────┬───────────────────┬─────────┼ │ │ │
│ │ ┼─┼─┼───┬─────────┼─┬───────────┬─────┼─┬───────┼ │ │ │
│ │ │ ┼─┼─┬─┼─────────┼─┼─────────┬─┼───┬─┼─┼─────┬─┼ │ │ │
│ │ │ │ │ ┼─┼─┬───────┼─┼─┬────── │ │ ┬─┼ ┼─┼─────┼─┼ │ │ │
│ │ │ │ │ │ │ ┼─────┬ │ ┼─┼───┬── │ │ ├─┘ │ ┼─┬───┼ │ │ │ │
│ │ │ │ │ │ │ ┼───┬─┼ │ │ ┼─┬─┼─┬ │ ├─┘ │ │ ┼─┬─┼ │ │ │ │
│ │ │ │ │ │ │ │ ┬─┼─┼ │ │ └─┤ ├─┘ └─┤ │ │ │ ├─┘ │ │ │ │
│ │ │ │ │ │ │ │ └─┤ │ │ │ ├─┘ │ │ │ ├─┘ │ │ │ │
│ │ │ │ │ │ │ │ ├─┘ │ ├───┘ │ │ ├─┘ │ │ │ │
│ │ │ │ │ │ │ ├───┘ ├─┘ │ └─┤ │ │ │ │
│ │ │ │ │ │ ├─┘ │ │ ├───────┘ │ │ │
│ │ │ │ │ └─┤ │ ├───────┘ │ │ │
│ │ │ │ │ ├─────────┘ │ │ │ │
│ │ │ │ ├───┘ │ │ │ │
│ │ │ └─┤ │ │ │ │
│ │ │ ├───────────────────────────┘ │ │ │
│ │ ├───┘ │ │ │
│ └─┤ │ │ │
│ └─────────────────────────────────────────────────┤ │ │
│ ├───┘ │
└─────────────────────────────────────────────────────┤ │
└─────┘
[1] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d8...
[2] https://rosettacode.org/wiki/Universal_Lambda_Machine
[3] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d8...
Regardless, I'd still consider your 'additively optimal' to be a strange definition, given that BLT programs get to have their input bits pre-expanded as a valid sequence of boolean terms for free. If all it means is that the input format accepted by D is a subset of the input format accepted by U, then many existing small UTMs could easily meet it just by restricting D's input format.
[0] https://doi.org/10.1016/j.tcs.2006.06.002
[1] https://mural.maynoothuniversity.ie/12416/1/Woods_FourSmall_...
Could you construct a 2-symbol UTM whose own encoding is under, say, 10,000 bits in size? If it takes 10,000 bits then it would not seem as easy as the 232 bit universal lambda machine.
> you could add a few states extra to expand new input on the fly, shifting any existing data to the left as necessary.
That would be more than "a few" states, and could easily add thousands of bits to the UTM size.
> given that BLT programs get to have their input bits pre-expanded as a valid sequence of boolean terms for free.
I guess you mean BLC programs. That criticism seems unfair, since the lambda machine model has no primitive notion of bits. Thus there is no expansion, only representation of bits in the lambda calculus.
> If all it means is that the input format accepted by D is a subset of the input format accepted by U
The input format for D can be all binary strings, e.g. if D is identity (assuming the delimited input model).
> many existing small UTMs could easily meet it just by restricting D's input format.
I don't know what this means. A UTM should parse the description of a TM from its input, and simulate that TM on the remainder of input. If it does that, then it would be additively optimal. It cannot assume any restriction on that remainder of input.
Ah, if you're specifically talking about self-encoding size as a yardstick, then you've got me: I spent yesterday afternoon adapting an existing UTM construction to take a look at this. While I managed to get most of the way there within ~40 states, it would take ~4 megabits to encode itself, by my estimation. Though it's difficult to tell just what the lower bound is, since the more states you allow in the UTM, the shorter you can make the encoding. I still suspect that 5 kilobits should be more than enough for someone actually good at TM golfing.
> That criticism seems unfair, since the lambda machine model has no primitive notion of bits. Thus there is no expansion, only representation of bits in the lambda calculus.
> The input format for D can be all binary strings, e.g. if D is identity (assuming the delimited input model).
> A UTM should parse the description of a TM from its input, and simulate that TM on the remainder of input. If it does that, then it would be additively optimal. It cannot assume any restriction on that remainder of input.
Having played with the UTM problem, I have a better understanding of the point I was trying to make. Consider a thought experiment, where you try to construct a UTM by making a TM that simply evaluates a BLC term on the tape. This TM by itself would still not be 'additively optimal' by your rules! It would also need an incremental input encoder to convert packed bits into BLC terms, as well as a lazy evaluation model to trigger it only when needed.
Thus, I think your UTM rules are a bit unfairly strict. A UTM that abides by those rules, as well as being additively optimal, must further be 'concatenatively optimal', in that for any description D, bit string s, and bit stream t, there must exist an encoding <D, s>, no longer than <D> + s, such that <D, s> + t is equivalent to <D> + s + t. (That is, adding a fixed prefix before the input cannot extend the encoding by more than the length of the prefix.)
But by itself, the language of BLC programs is not and cannot be concatenatively optimal! This is the expansion I was talking about: a given bitstring can't be represented as efficiently inside the BLC encoding as it can outside the encoding. To get a concatenatively optimal language, you'd have to formulate it as a (term, input) pair, where the input is a raw binary string that must be encoded before feeding it into the actual program. (This isn't an issue entirely unique to BLC: a TM model mandating an empty initial tape also couldn't be concatenatively optimal.)
So then, one might ask, where is the implementation of this input encoding within your 232-bit BLC term? Nowhere! Its only task is to 'interrogate' the first several input bits (as already encoded) to parse the description D. And when it finishes constructing the term corresponding to D, its job is done, since the remaining input bits are already encoded in a form it can use. So if we try to trace the point where the encoding actually happens, we can only conclude that it occurs wholly outside the lambda calculus. But the encoding step is entirely necessary for concatenative optimality to hold.
That is all to say, self-encoding size is an easily gameable metric (in the trivial case, you could make a universal machine that's also a quine, so that it can encode itself in 1 bit), and your idea of additive optimality is tied very closely to the power of the input model defined outside the system. (The input model can also be easily gamed: imagine that each cons term of the input, alongside the head and tail, also supplied a universal program. Under that input model, the program within the system would be trivial.) By saying that a UTM only gets 2 symbols and has to accept dense input, you mandate a very weak input model, so of course it will be tough to get it to accept arbitrary data.
---
But in the bigger picture, I'd like to note that I'm not trying to dunk on BLC here, nor on the lambda calculus in general: clearly, it's very efficient at representing and simulating itself, and no simple TM model can simulate itself nearly as easily. And that's all well and good if you want a model where you can treat code as data and do other stuff like that. But I maintain that this self-representation doesn't make it more universal, or otherwise more fundamental, than the TM model, which aims to use as simple a rule as possible for transitioning from one configuration to the next, at the cost of having heterogeneous code and data. (Imperatively speaking, lambda-calculus reductions would seem closer in power to a random-access machine, or perhaps a TM on a branching tape.) So being generous, I'd say that both are equally as fundamental, they're just trying to excel at two different goals.
Coincidentally, that is about the size of Penrose's UTM [1] which takes 5495 bits in its own encoding. I suspect that one is only linearly optimal, so it might take another few thousand bits to make it additively optimal.
> Consider a thought experiment, where you try to construct a UTM by making a TM that simply evaluates a BLC term on the tape. This TM by itself would still not be 'additively optimal' by your rules! It would also need an incremental input encoder to convert packed bits into BLC terms, as well as a lazy evaluation model to trigger it only when needed.
Yes; that's what it means to evaluate BLC programs. If the UTM does that, then it's additively optimal. It would be a TM implementation of the Universal Lambda Machine [2]. Most implementations you find there also have subroutines doing the conversion from bits to terms and back.
> for any description D, bit string s, and bit stream t, there must exist an encoding <D, s>, no longer than <D> + s, such that <D, s> + t is equivalent to <D> + s + t. (That is, adding a fixed prefix before the input cannot extend the encoding by more than the length of the prefix.)
I'm not quite understanding this. In my write-up, D is not a description but a description method, i.e. a computable mapping from binary strings (descriptions) to outputs (some set that includes binary strings). What is your D and what does <D> mean?
> a given bitstring can't be represented as efficiently inside the BLC encoding as it can outside the encoding
By "inside the BLC encoding", do you mean as part of the lambda term encoding prefix of the BLC program? Indeed, that is why we equip BLC programs with pure binary input so that k bits of data only add k bits to program length. Which is what allows additive optimality.
> where is the implementation of this input encoding within your 232-bit BLC term?
It's part of the BLC machine model, i.e. of the description method. We can agree that BLC is a computable mapping from bitstrings to outputs including bitstrings.
> Its only task is to 'interrogate' the first several input bits (as already encoded) to parse the description D.
If by D you mean an encoded lambda term, then the 232 bits definitely include the parser of that binary encoding.
[1] R. Penrose, The Emperor's New Mind, Oxford University press, 1989.
Einstein, Gödel, and a few others verified work means the majority of us are coloring within the lines they drew until we die.
Also, the whole, "we make this other program that does the opposite" argument implies the test of `is_halting` is actually a test of some other function "do_opposite" that wraps "is_halting" and does the opposite. That's not exactly fair, that's a test of the opposite function, not the "is_halting" function. Furthermore, the inner "do_opposite" evaluated by is_halting, is a different invocation of the do_opposite source. (I.E. Fregeian Sense and Reference, a different referent for the same sense).
Just because somebody outside the is_halting function can do something counterproductive, doesn't necessarily mean the specific invocation of do_opposite within the closure of is_halting is impossible to classify. Furthermore, is_halting could theoretically refuse to play ball and crash the program at runtime, or induce a compile error before the game can even begin, if we try to create a paradox. Has anyone actually even witnessed a real paradox in real life? Maybe the universe is deeply anti-paradox and the whole argument is a bunch of humbug.
Can someone please tell me how I'm fooling myself? Cuz I'm neck deep in coding this thing and building all the helper functions and it would save a bunch of time to know why it's wrong. Every proof seems to boil down to "muh contradiction" which feels like, ok, so what? If the caller wants to do_opposite, that's their problem, not on is_opposite. A function which can decide halting for all the non_opposite functions (which is, every one that matters in practice, right?)
Plus, who knows what an anti-paradox machine can accomplish? Maybe there's one weird trick quantum scientists or thermodynamic reversible computer engineers hate, and you can solve hard problems by finding the ones which both halt and don't.
Just feels weird how we all accept this quasi-religious belief that we shouldn't even try to decide if programs halt simply because you can't categorize every single program into 2 buckets. What about 3 buckets i.e. 3-decidability of the ternary halting problem?
sorry for long comment, fuck it, ill post code, it sucks and doesn't run, just tinkering, but https://github.com/bionicles/halts published for your pleasure. No promise it will ever actually work.
def foo(n):
if n <= 1:
return
elif n & 1:
return foo(3*n+1)
else:
return foo(n//2)Would you give an engineer an infinitely large project, criticize them for being unable to complete it, and use their 'failure' to support cancellation of a finite, smaller project with potential benefit?
Seems like just another lame argument to me.
Or, how about this one:
def foo(n):
if n <= 1:
return
elif n & 1:
return foo(n//3)
else:
return foo(n//2)
> (I.E. Fregeian Sense and Reference, a different referent for the same sense).
For the traditional halting problem, all of the programs are encodings for some particular UTM and therefore we are only talking about referents. The halting problem is the statement that there does not exist a referent for the sense that is "Does referent P halt on input I?"
> Just because somebody outside the is_halting function can do something counterproductive, doesn't necessarily mean the specific invocation of do_opposite within the closure of is_halting is impossible to classify.
The problem is the inner call and the outer call are definitionally the same. The input to `halts` is an encoding a of turing machine and an input. The construction of the `do_opposite` function is possible no matter what the encoding of `halts` would be. So if `halts` has a valid encoding, there is a corresponding `do_opposite` that totally confuses it and forces the inner and outer eval to be the same.
> Every proof seems to boil down to "muh contradiction" which feels like, ok, so what?
I think you may misunderstand why everyone is like "muh contradiction". They are doing a proof by contradiction so as soon as they get to a contraction, the proof is complete. I will give a proof of the halting problem for python programs.
Theorem: There does not exist a function `halts(program, inputs)` that correctly determines if a given program halts for EVERY input.
For the sake of contraction, assume such a function `halts` exists. Then carefully construct a program `do_opposite` that intends to befuddle `halts` as follows:
def do_opposite(inputs):
if halts(do_opposite,inputs):
while True:
"Loop"
else:
return
if `halts(do_opposite, inputs) == False` then `do_opposite` must immediately return because the else statement will be executed.
For any return value of `halts(do_opposite, inputs)` it must contradict the definition because it does not correctly behave on this particular input. Because this is a contradiction with the only assumption we have made, that assumption must be wrong. QED.
Would "halts" be useless if it only decided every function except the ones that invoke it and do the opposite? If not, maybe it's worth building, even if we know it's not possible to classify everything into 2 buckets, because the majority of real world functions don't have that opposite property and could be useful to decide halting for that subset.
Also, I'd point out, there is a difference between the inner and outer invocations of the same turing machine. They are different executions of the same machine, on different layers. A decision about an inner machine might be truly correct, independent of whatever happens outside.
The real question is, how small can you make the set of instances that results in "maybe", and how small can you make the intersection of that set, and the set of instances we actually care about.
And, it turns out, you can typically make that intersection pretty small.
Regarding the question as you stated it. If you define "paradox" as whatever situation your algorithm cannot handle, then it us trivial. If you define "paradox" as the smallest possible set of "maybe", then determining what instances belong in paradox is equivalent to solving the halting problem.
def do_opposite(): if is_halting(do_opposite): loop_forever()
That's the paradox function which allegedly proves it's not worth attempting to decide {halt, loop} and so that (and other functions with the same behavior) would belong in the paradox category.
For example you can't have a general program that you feed in any 2 mathematical statements and tells you if they're equal. From what I understand this is proven for "regular math" but not all formal systems.
As a counterpoint, there are many algorithms these days that can do theorem proving better than anything before in history (partly thanks to AI, and partly thanks to the massive efforts that went into symbolic computation engines over the past decades). I think in a few years theorem proving will be done elegantly by computers instead of humans. Not all theorems, sure, but this is the world we got to live in.
> I still had the mainstream belief that AI would be just as capable as humans.
Roger Penrose is one of the more authoritative, for lack of other arguments, voices for humans being more capable than AIs. Still not sure if it implies an existence of God, a class of ability higher than Turing machine or something else.
Yes it does, it would mean that your brain can somehow exploit quantum gravity to turn itself into an oracle machine. How a wet blob significantly hotter than room temperature (in the superconductor definition) is supposed to do that I don't know.
If there is any quantum effect either used directly or measured within our brains, it might provide a speed advantage.
That's what I was getting at with the temp. comment, as I suppose an oracle machine could theoretically be classical.