Timeline for Will this Turing machine find a proof of its halting?
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 31, 2023 at 5:27 | comment | added | Akiva Weinberger | If anyone wishes to republish this problem somewhere, they should call this machine $C$ for "compliant," to distinguish from what OP calls $M'$ and what I think should be called $R$ for "rebellious." | |
| Aug 4, 2022 at 14:58 | comment | added | Oscar Cunningham | A bounded version of this problem is considered here: lesswrong.com/posts/TNfx89dh5KkcKrvho/…. It's bounded in the sense that M only searches proofs up to some maximum length. They also consider the case with two programs that each search for a proof the other halts. This is eventually used to construct agents which achieve mutual cooperation in the Prisoner's Dilemma, while still defecting against exploitable opponents. arxiv.org/abs/1401.5577 | |
| Aug 4, 2022 at 13:05 | comment | added | Akiva Weinberger |
@SamHopkins Here's a simple way to construct $M$. As it stands, $M$ is a zero-input program. Define $M_1$ to be a 1-input program, with the following behavior: if the input is $P$, then $M_1(P)$ interprets $P$ as a 1-input program and searches for a proof that $P(P)$ halts, and halts when it does. Then OP's $M$ is $M_1(M_1)$ (that is, $M_1$ run on itself). Similarly, in my answer, we can construct $N_1$ on similar lines, and let $N$ be $N_1(N_1)$. I leave actually writing the pseudocode (for p in proofs etc) to someone else.
|
|
| Aug 4, 2022 at 11:05 | vote | accept | Henry Yuen | ||
| Aug 4, 2022 at 8:04 | history | became hot network question | |||
| Aug 4, 2022 at 2:18 | comment | added | paul garrett | This is a hilariously interesting question! :) :) | |
| Aug 4, 2022 at 1:44 | answer | added | Akiva Weinberger | timeline score: 83 | |
| Aug 4, 2022 at 0:37 | answer | added | Joel David Hamkins | timeline score: 80 | |
| Aug 4, 2022 at 0:12 | comment | added | Joe Bebel | @SamHopkins It seems at least to me to be unambiguous, since it is clear that there exists at least one $M$ that meets the informal description of enumerating and checking ZFC proofs, and Kleene's recursion theorem guarantees that it can encode the statement "M halts" in ZFC language | |
| Aug 4, 2022 at 0:04 | comment | added | Sam Hopkins | I'm not sure you have really described $M$ unambiguously. Doesn't it have to "know how it is coded"? | |
| Aug 4, 2022 at 0:01 | history | asked | Henry Yuen | CC BY-SA 4.0 |