A proper disproof disallows any instance. If I disprove that bachelors are married, you can be sure there are no married bachelors. If I prove Hume's guillotine, you can be sure there are no moral facts. If I disprove nonexistence, then existence definitely exists; there are no instances of nonexistence.
While = true.
This program doesn't halt. Proof by inspection.
Whoops. How can there be no general algorithm to determine if a program halts if every particular program has a particular proof? What do you think a general algorithm is except the most compressed version of [every particular poof]?
Do you remember the six simple machines? The ramp, the screw, the pulley, the lever, etc? In reality, computer programs likewise have a set of simple digital machines. Some of their relationships result in non-halting, and you can just list these relationships if you want, because there's like six simple machines and thus like 15 binary relationships between machines,
Sure halting is likely NP-complete, but you can just brute force it, the same way you solve a travelling salesman problem. If the trinary relationships matter, I think there's 90 of them. Goes up quick. Still finite though. (Plus the designer can control this. If you haven't checked a relationship for halting yet, don't use it.)
Second empirical disproof: physics is a formal system. Here's my algorithm to determine if a program halts: run it and see what happens. How does physics know whether physics halts or not? Physics has to run an algorithm, because physics is simply the greatest algorithm. Turing's proof should demonstrate that physics itself doesn't know whether a program will halt or not. (Ref: uncertainty principle.) All programs should enter an incollapsible superposition of both halting and not-halting. In reality all programs that halt in under t hours will be proven to halt by running them until time t.
Godel's and Turing's proofs are isomorphic. They both commit a grammatical solecism. They are not valid.
The actual form is basically [G = G is not provable]. This would mean [G = G is provable] is also grammatically allowed. Or [G = G is true = is true]. [3 = 3 is true] = is true, 3 = G = 2 = 0. You also can't prove or disprove 3 = +, because + is an operator, not a number. If 3 = + then 9 + 2 = 9 [3] 2. If 3 != +, then some number does, and you get the same nonsense. 3 = = amuses me more, to be fair. 9 + 2 [3] 11.The equation is just malformed, like 3/0 = ?.
"True" isn't a number, it's a meta-property. Get this: [system + ε] has elements that are non-provable using only [system]. Amazing. Stating things about [system + ε] without using ε is inconsistent. Inconceivable.
Bonus round: every program halts. Are you watching? Look ma, no brain: it's called the second law of thermodynamics. The machine is itself a program which is running your explicit program as a proper subset, and the machine is going to break down. The program halts at t < ∞, for all programs.
Reminder that Godel numbers are absolute genius brilliance, which is presumably why nobody talks about them and fewer use them. See also: Xeno was likely the best philosopher after Socrates, yet he's considered a footnote.
P.S. Speaking of doing things the easy* way rather than the hard way, rather than trying to use (n-1)n/2 with odd numbers, you can remember it's equivalent to n * (n/2-0.5). [5 => 5 * 2]. [9 => 9 * 4]. Etc. This formula always has an integer-only form as long as n is an integer.
Really, why would you factor out the n/2 instead of the n/1? WTF?
Technically the formula is n!/2(n-2)! ( n=5 => 120 / 2*6 ) you could use that instead if you wanted...
*In the above case, the possible way instead of the impossible way.
10 comments:
> How can there be no general algorithm to determine if a program halts if every particular program has a particular proof?
Do you define an algorithm to be the same thing as a program?
A program is nothing more than a series of algorithms. If all parts of a construct are clay, it is a clay construct.
> A program is nothing more than a series of algorithms. If all parts of a construct are clay, it is a clay construct.
Okay. Are all algorithms finite in length?
> If the trinary relationships matter, I think there's 90 of them.
I can see how you can enumerate all programs with a program. But how do you determine whether a program halts or not based on this?
There seems to be a hidden hypothesis here - namely that it's possible to determine if a program of size N halts based on the behaviour of smaller programs.
> Here's my algorithm to determine if a program halts: run it and see what happens.
This will say that the program halts for all halting programs. However, for non halting programs it will not halt. It's supposed to output "it will not halt".
It's not a hidden hypothesis, I said it straight out: "Some of their relationships result in non-halting, and you can just list these relationships if you want, because there's like six simple machines and thus like 15 binary relationships between machines"
Don't use the non-halting relationships, don't get infinite loops. You can pack as many halting algorithms together as you want and they'll still halt. If you're not sure, then check.
How will you predict the behaviour of two nested whiles using just the behaviour of one while? I.e.
While (test1) {
While (test2) {
...
}
...
}
Using just
While(test) {
...
}
& ...?
(... represents non looping code)
I don't. I investigate each while individually. Then I investigate the [nesting] relationship. The program has three components, and I need to understand three components. If I don't know the components then I don't use them.
However, I don't have to investigate every instance of nesting as if it were some unique species. I can investigate nesting per se, once, and then understand it for all programs.
It turns out nesting doesn't affect the issue unless it breaks certain rules of variable ownership, in which case the problem isn't [nesting] it's spaghetti code. I consider the latter a distinct kind of relationship.
If the while inside halts, and the while outside halts, then the program halts. No amount of nesting finite programs will get you an infinite program.
Okay, I think I finally understood the flaw in the proof of the lack of any solutions to halting problem.
From wikipedia:
"For any program f that might determine if programs halt, a "pathological" program g, called with some input, can pass its own source and its input to f and then specifically do the opposite of what f predicts g will do. No f can exist that handles this case."
If f cannot be represented by any program, then g is not a program. f, which takes as input only programs, cannot be expected to tackle the case of g.
Is this the case you are making?
Possibly. You weren't entirely unambiguous.
That said yes that's the keystone and I myself understand better what I'm saying now you've highlighted it.
For the proof to work, program g has to actually exist. Ideally you would be able to physically write program g in C++ or python.
Program g is a function of f, which is a function of g, which is a function of f...
This function does not converge. You definitely absolutely cannot write this in C++. Even if you somehow pseudocoded it properly, it would fail to compile.
Turing has instead proven the opposite of what he's alleged to prove. "Halting is undecidable if program g exists. Program g does not exist. Modus tollens: halting is decidable."
Since Godel's first incompleteness and Turing's halting are isomorphic, Turing has likewise proven that formal systems are complete.
You're explaining something everyone else here already knows. You're the one who doesn't get it. You're probably crazy and should be in an asylum.
Post a Comment