I read through it, I think the idea of having regular attention checks is quite interesting. (Personally I found them to be a bit too frequent).
But there are also things like:
>If you implement halts using canBeRegex, you’ve got a proof by contradiction that canBeRegex can’t exist.
This is plainly false. I can also implement halts using addition, that does not imply that addition can not exist.
The author is clearly writing for a more general audience and I know what he means. But I think that if you are writing for a more general audience you should be more careful in your language and I think the article is sonewhat lacking there.
It does not matter at a high level but I think the distinction is that there should be only one black box in the proof, which is precisely the thing being reduced. Every other instruction/call used n the algorithm must be known to be computable (in this case, addition).
Here is a solution of the halting problem which is implemented using addition:
function haltWithAdd(code) {
var a = 1 + 2;
return halt(code);
}
This clearly solves the halting problem (we assumed the existence of halt as the first step of our proof by contradiction). And it clearly uses addition (surely you can find where it does). By the logic (as written) of the article the implication is that '+' does not exist.
If you assume that halt does exist to make your solution valid, then you can derive any statement (including that addition does not exist), because that assumption is false.
In general:
Let P be a statement. Lets assume that the Turing Machine T solves the halting problem - let's call this assumption H.
Now we assume P is false. Now we have a contradiction - H says that T solves the halting problem, but we know that there is not Turing machine that can solve the halting problem!
Thus P must be true!
Notice that P is arbitrary.
Plainly speaking:
If you assume that the halting problem can be solved, I can formally prove you that addition does not exist (i.e. there is no operation +, such that it forms a group on Z)
> By the logic (as written) of the article the implication is that '+' does not exist.
This is actually true. With that strong assumption, + does not exist.
As a reminder: a proof by contradiction works by assuming first the negation of a given statement. If from that you can deduce a falsehood you know that statement is true.
In the article the author says:
"If you implement halts using canBeRegex, you’ve got a proof by contradiction that canBeRegex can’t exist."
Which is plainly a false statement. What he means is the following statement:
"If you show that if canBeRegex is computable then halts is computable, you’ve got a proof by contradiction that canBeRegex can’t exist."
Those two statements are clearly not equivalent. And only the second one is true.
>that the implementation is required to be correct?
No. "Implemented" is in fact irrelevant, it is clearly not the term to use here. Because what the implementation uses is irrelevant, the question is about whether computability in one can be derived from computability of the other.
In his example the implementation also uses ".length", whether it does or doesn't is irrelevant though. Since it is not a question of implementation.
Implemented in this context means exactly the type of reduction that is needed. If halt can be implemented by using X that means you can reduce X to halt. This is similar to polynomial time reductions in complexity.
Standard practice in mathematics would apply here if what was said is wrong. This time it is about an interpretation that no one shares with you.
[edit] After reading again your comment I realized that maybe you are not applying the logic correctly. If the reduction "implementation" uses both length and foo, then the conclusion is that at least one of length or foo cannot be computable. Since length is trivial, then it must be foo that is not computable.
You would need to show how to use length to implement halt and that is the part you will not be able to do. If you did, then yes, length would not be computable.
Reductions in complexity theory work like this. An explicit algorithm invokes a black box and this shows that either the black box does not exist or you can solve the original problem. Typically you care about the complexity of the reduction to establish that the problem is inside a given complexity class (e.g. NP complete).
The statement is obviously false by the way, as you can see in the article where the author does exactly that. You rephrasing the statement to make it true, is just ignoring the point.
I would encourage you to engage in some studying of reading comprehension. It is an important skill in mathematics and related disciplines.
You are arguing against a completely fictional point which you have made up in your head.
None of what you are saying is even remotely a response to my criticism. You can tell me that I failed basic logic all you want, but your reading comprehension sucks so much that you still have not been able to figure out what I am even talking about.
I think you still haven't understood that I never said his intended reasoning was wrong. But that his statement as written is plainly false. There is no argument against the logic by me, so the fact that you keep going on and on about "logic" just shows that you haven't even understood yet that nobody disagrees with the logic. I know how a proof by contradiction works, you do not seem to want to understand that "computes" and "implements" are different words. And that by repeatedly arguing that the authors reasoning is valid if you change the statement to make it correct you are proving my point again and again.
I'll bite, what is the false statement that you keep alluding to? Because the vacuous "if" statement that you claimed to be false is absolutely a truth in logic.
Compute and implements are different words, nobody is arguing that. To me and everyone literate in math/cs, the role of "implementing" here is in the proof by reduction, which in the case of computability is used to establish by contradiction that some other problem is not computable by reducing a known incompatible problem to it.
Just like when you show an algorithmic implementation that maps any SAT instance to another problem using a polynomial time algorithm, then it follows that this other problem is NP-complete.
> This clearly solves the halting problem (we assumed the existence of halt as the first step of our proof by contradiction).
Implementing the halting problem using addition does not assume the existence of halt. It assumes the existence of addition, and you use that to show that halt must also exist. And that's not possible to do.
To implement halts using addition, you need to:
- Take the input to halts, namely the source code to a program.
- Convert that into an input to addition, namely two numbers.
- Call into addition, which adds the numbers.
- Use the result of that addition to infer whether the original program halts or not.
Why are you debating the validity of the argument?
The code very clearly:
- is an implementation of the halting problem. If halt existed it would undoubtly solve the halting problem
- it uses '+'
You are prentending I didn't know what the author meant. The point is that what the author says is simply not true, if you take the statement as written.
What he wants to show is that if canBeRegex is computable then halt is computable, but that isn't what he is saying.
You're not getting it. A "CanBeRegex" function which (always) correctly indicates whether a code block could be replaced by a regex MUST be able to solve the halting problem. The same is not true for addition.
>If you implement halts using canBeRegex, you’ve got a proof by contradiction that canBeRegex can’t exist.
This is plainly false. I can also implement halts using addition, that does not imply that addition can not exist.
The author is clearly writing for a more general audience and I know what he means. But I think that if you are writing for a more general audience you should be more careful in your language and I think the article is sonewhat lacking there.