3 ms·

Am I missing something? The author says that a solution to the Post Correspondence Problem with infinite dominoes in finite time is impossible. He then writes a

Am I missing something? The author says that a solution to the Post Correspondence Problem with infinite dominoes in finite time is impossible. He then writes a bunch of C++ code that can solve the PCP for any arbitrary list of dominoes. Did he realize that this list must be finite since it’s written into the C++ code? If the list had infinitely many dominoes it would require infinite space to store and infinite time to compile anyways, PCP or not. That’s like saying Java is undecidable because you can write List<List<List<List<...>>>> and have something take infinitely long to compile.

ben509 6y ago
> The author says that a solution to the Post Correspondence Problem with infinite dominoes in finite time is impossible. He doesn't say an infinite set, though: > Turns out, there exists no algorithm that says “yes” or “no” to the Post Correspondence Problem in finite time, given any set of dominoes as input. That means any finite set of dominos. It's similar to the idea behind the halting problem, it's not checking whether an infinitely long program will halt, but whether any possible finite program will halt.
roywiggins 6y ago
It may take an infinite amount of time to solve the Post Correspondence Problem even with a finite number of dominoes, but you can't know whether it really will hang forever or whether you just haven't run your program long enough to find the answer. You don't need infinite space or time for the ones that are solveable, just an unknowably large amount. So if you make a C++ program that compiles if the equivalent arbitrary Post Correspondence Problem is solvable, and compiles forever otherwise, you've proven that C++ compilation is not decidable.
jlebar 6y ago
There is a finite set of Domino "prototypes" (a pair of strings), and you are allowed to use as many of each prototype as you like.
btilly 6y ago
What you are missing is that in the Post Correspondence Problem you have an unlimited supply of each type of domino. So a finite list of domino types could require an unlimited number of dominos to decide. Now we can write programs that attempt some sort of clever reasoning to figure out whether or not there is a solution at all. But given any specific program that does that, there is a finite arrangement of dominos such that either the program produces the wrong answer, or cannot possibly finish. In other words, for any algorithm there is a finite problem that cannot be properly decided by that algorithm. Given an axiom system such as ZFC, we can write a program that searches through all proofs in ZFC for a proof or disproof that a particular case of the Post Correspondence Problem is solvable. This, being an algorithm, has a finite input that it will either produce a wrong answer for (meaning that ZFC contradicts itself) or else will never finish. Whether or not that case has an answer is not decidable within ZFC! Ideally we want the answer to be "there is no solution" in this case. But if we introduce the axiom that there is a solution, we will never find a contradiction and never be aware of any disturbing conclusion beyond, "That solution must be really, really big." It turns out that, no matter how hard we try, first order logic cannot correctly encode the concept of "finite". This is what we mean by "undecidable".

ben509 6y ago

> The author says that a solution to the Post Correspondence Problem with infinite dominoes in finite time is impossible. He doesn't say an infinite set, though: > Turns out, there exists no algorithm that says “yes” or “no” to the Post Correspondence Problem in finite time, given any set of dominoes as input. That means any finite set of dominos. It's similar to the idea behind the halting problem, it's not checking whether an infinitely long program will halt, but whether any possible finite program will halt.

roywiggins 6y ago

It may take an infinite amount of time to solve the Post Correspondence Problem even with a finite number of dominoes, but you can't know whether it really will hang forever or whether you just haven't run your program long enough to find the answer. You don't need infinite space or time for the ones that are solveable, just an unknowably large amount. So if you make a C++ program that compiles if the equivalent arbitrary Post Correspondence Problem is solvable, and compiles forever otherwise, you've proven that C++ compilation is not decidable.

jlebar 6y ago

There is a finite set of Domino "prototypes" (a pair of strings), and you are allowed to use as many of each prototype as you like.

btilly 6y ago

What you are missing is that in the Post Correspondence Problem you have an unlimited supply of each type of domino. So a finite list of domino types could require an unlimited number of dominos to decide. Now we can write programs that attempt some sort of clever reasoning to figure out whether or not there is a solution at all. But given any specific program that does that, there is a finite arrangement of dominos such that either the program produces the wrong answer, or cannot possibly finish. In other words, for any algorithm there is a finite problem that cannot be properly decided by that algorithm. Given an axiom system such as ZFC, we can write a program that searches through all proofs in ZFC for a proof or disproof that a particular case of the Post Correspondence Problem is solvable. This, being an algorithm, has a finite input that it will either produce a wrong answer for (meaning that ZFC contradicts itself) or else will never finish. Whether or not that case has an answer is not decidable within ZFC! Ideally we want the answer to be "there is no solution" in this case. But if we introduce the axiom that there is a solution, we will never find a contradiction and never be aware of any disturbing conclusion beyond, "That solution must be really, really big." It turns out that, no matter how hard we try, first order logic cannot correctly encode the concept of "finite". This is what we mean by "undecidable".