There's no way this is an argument that humans can do things AIs can't do. Weird quantum nonsense won't help, because quantum computers aren't oracle machines.
I'm not sure what is more mainstream - belief that AIs are as capable as humans, or belief that they are not.
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.
All it implies is that brains are immensely complicated and have kajillions of connections, which don't work the same as anything branded AI. Consciousness can be an emergent property AND AI capability can be largely oversold at the same time.
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.
that's a good question, but the electron transport chain and photosynthesis are both postulated/(known?) to exploit quantum effects at room temperature.
I haven’t seen anything yet that a Turing machine can’t do that we do. A better question might be: Can we do things “faster” than a Turing machine theoretically can?
If there is any quantum effect either used directly or measured within our brains, it might provide a speed advantage.
Quite a comprehensive summary of the implications of Turing-Completeness. There aren't any outright errors that pop out to me which is high bar if other articles are anything to judge by.
> 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.
I don't believe only turing machines are capable of executing other turing machines... Surely lambda calculus can do the same? I was under the impression, lambda calculus can indeed execute itself with even less code than turing machines
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"
I will never understand how people think like that. Sure, there are things computers cannot compute, but that's because those things are _uncomputable_ in general
It's obvious to you because of people like Church and Turing. Until their work on the Entscheidungsproblem was published, it was not only common, but mainstream to believe that nothing was inherently incomputable. They not only demonstrated that there were things that weren't, they did so by proving that the set of everything computable was the same set of things their approaches could compute and that certain problems were outside that set.
Yeah, that's definitely fair. What I'm annoyed about is the "checkmate, computers" stance, pretending like the problems computers cannot solve could be solved by other means
I'm confused by your 'additively optimal' definition. Suppose that the objects we want to describe are strings of bits, and the description method D is just "listing the bits out in a sequence". Then surely no BLC term can describe the same sequence of bits with only a constant amount of overhead.
If a 'description' of an 'object' is defined to always be a valid term or program that operates on provided input, then I don't see why Turing machines wouldn't nearly as easily be 'additively optimal' in your sense. For most universal Turing machines that represent an input bit as a constant-sized word (such as Neary & Woods' 8-state 4-symbol UTM [0], which represents each input bit as two symbols, or even their 15-state 2-symbol UTM [1], which uses a slightly trickier encoding), you could add a few states extra to expand new input on the fly, shifting any existing data to the left as necessary. The only precondition is that the existing data has a boundary recognizable by a finite-state machine; this condition can always be met with O(n) extra states by adding an extra symbol to the UTM's description to represent the boundary, then converting it back to a 2-symbol machine.
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.
> I don't see why Turing machines wouldn't nearly as easily be 'additively optimal' in your sense.
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.
> 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.
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 mand...
> I still suspect that 5 kilobits should be more than enough for someone actually good at TM golfing.
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.
To quickly summarize: A Turing machine program or method can't solve the Entscheidungsproblem, which means you can't have a general algorithm to prove all possible statements true or or false (or equivalent) within a formal system.
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.
(noob rant warning) What bugs me about the decidability thing, is Turing proved 2-undecidability in the action space {halt, loop}, but I still feel like we miss an opportunity to try 3-decidability {halt, loop, paradox} and throw out the functions upon which his proof hinged, namely, the ones that invoke the is_halting function and do the opposite.
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.
Collatz is not "theoretically undecidable" because of a paradox, it's "practically undecidable" because it has an infinite domain, so "is_halting" implemented via simulation would take infinite time to try every number.
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?
Okay. So you acknowledge that your approach will never solve the hard part of the halt/loop/paradox problem that your code hopes to solve. But instead of recognizing this as a fundamental limitation to your approach, you've gone on to create a new class of algorithm: lame. Do you suppose you can come up an algorithm to classify programs as halt/loop/paradox/lame in finite time?
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 can trivially prove this halts for all n. Can your code?
It is not clear to me what you would define as the reason to return paradox from `halts`. It is pretty clear you can make a `halts` function that returns halts, loop or unsure. Renaming unsure to paradox would give a valid version of your 3-decidable `halts`. A concrete definition in terms of turing machines is necessary if you want to displace the halting problem.
> (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) == True` then `do_opposite` must loop forever because the if statement will be followed leading to the inner loop.
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.
Thank you for the reply! I certainly don't intend to put forward a claim that 3-decidability, if possible, would invalidate the 2-undecidability result; Rather, I believe it worth investigation to see if we allow ourselves a middle road of a paradox category, it's a different theorem and might be provable or at least practically useful.
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 more tractable problem is {halt, loop, unknown}. That problem us trivially solvable, and solved by every static analysis tool and optimizing compiler. Or at least, the generalized {yes, no, maybe} problem for various properties is.
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.
I would define paradox specifically as the case involved in the proof of the 2-undecidability halting problem, namely, functions of this kind:
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.
I don't quite understand what big point this is trying to make. It's very down on formal verification, but does that mean all formal verification should be thrown away?
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!
Hot take, it's an author who wants total power over computers and is upset that Turing completeness impedes that power. If they were thinking pragmatically they wouldn't have gotten into the argument linked in the post about Zig comptime.
I love this. I’m in appsec and bring up the halting problem all the time to developers to get them to think about the security landscape. The halting problem is why security is a unsolvable problem at its core.
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.
If you haven't already, read "Gödel, Escher, Bach". It sounds like you would enjoy it. For me its more of a "pick it up somewhere in the middle and get inspired" than "front-to-back" title but iirc it considers the halting problem and the incompleteness theorem to be two sides of the same coin.
Funny you recommended this book. It what inspired me to go back to school and enroll in compsci. I forgot that’s where this seed was planted. I think it’s safe to say it really resonated with me lol.
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
I think you misunderstand the halting problem. An algorithm that can prove any program halts or doesn't is impossible. But it's possible to prove it for some programs.
I don't think your reply is particularly effective when you are replying to a comment that exhibits a formally verified microkernel.
> 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 don't think your reply is particularly effective when you are replying to a comment that exhibits a formally verified microkernel.
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.
I misunderstood the goalposts because you had seemed to be talking about theoretical CS notions like complexity and computability (we were talking about the halting problem), and now you are talking about proving properties motivated outside TCS.
> 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.
The author cites this https://news.ycombinator.com/item?id=35683634 as evidence that his interlocutor doesn't understand the halting problem. But the halting problem is a hard limit that is of concern only for computers with infinite memory. In practice we are unable to compile (and run) many perfectly valid programs due to RAM constraints, and some systems are able to compile programs that others cannot. People looking to compile useful programs already accept these inevitable limits, yet the author seems to think that some notion of fuel in compilation time makes a compiler terribly compromised.
Any sufficiently expressive type system is undecidable anyway (including Rust's), so it is futile to limit the practical Turing completeness as opposed to the theoretical Turing completeness.
60 comments
[ 3.6 ms ] story [ 136 ms ] thread> 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.
> 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.
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).
Einstein, Gödel, and a few others verified work means the majority of us are coloring within the lines they drew until we die.
> 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
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 mand...
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.
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.
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.
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:
I can trivially prove this halts for all n. Can your code?> (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:
if `halts(do_opposite, inputs) == True` then `do_opposite` must loop forever because the if statement will be followed leading to the inner loop.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.
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.
https://news.ycombinator.com/item?id=35707565