Liste des Groupes | Revenir à c theory |
On 03/05/2025 20:45, Richard Heathfield wrote:The two proofs are isomorphic to each other.On 03/05/2025 19:50, Mike Terry wrote:I generally think I post way too much, and tend to wander off topic with unnecessary background and so on, and probably I write too much from a "maths" perspective, because that's my background. Not sure if I can change any of that! :) Just ask if I use obscure notation or let me know if I'm going too fast/slow. Part of the problem is I don't know your background and what things you're super familiar with.On 03/05/2025 06:47, Richard Heathfield wrote:>
>
<snip>
>>In passing, when I nailed down "TL;DR" I felt mildly guilty for scoring so few tersinosity points, but in return I must accuse you of undue obscurity.>
>
TL;DR appears to have attracted a certain currency, so okay, but... NTLFM? Really? "Seek and ye shall find", so I sought but shall findethed not. Most of my best guesses started 'Now The' and ended rhyming with RTFM, but none of those guesses jumped out as being self-evidently right. Would you care to translate?
I admit to making it up, but all these (usenet?) abbreviations have to start somewhere, so I thought I would start a much needed new one!
>
TL;DR = too long, didn't read,
Yes, that chimes with my research, but...
>introducing a short summary for someone who hasn't the inclination/ time to read a long (probably overly) verbose explanation. At least that's how I've seen it used. But then, how to introduce the verbose explanation? I couldn't find anything for that, so I invented NTLFM; which means "Not Too Long For Me" !>
Ach! Of course.
>I'm looking forward to being a footnote in history when it catches on...>
In a footnote to the footnote for NTLFM I would add TOAST --- Too Obscure And Startlingly Terse.
>>>I kind of disagree with your mild denigration of the Linz (and similar) proofs.>
I wish to clarify that denigration was most certainly not my intent. There is, however, no doubt in my mind that while Linz is undoubtedly a worthy and indeed admirable computer scientist, his proof stands on giant shoulders. All I meant to say was that, were Linz's proof to lose its balance and take a tumble, it would not be the fault of the shoulders.
Yeah, denigration was really the wrong word, as I know there was no bad intent anywhere. Perhaps "downplaying" would have been what I was looking for.
<nod />
>Ben pointed out there was confusion in the Linz proof with the labelling of states, and when I looked closely at the proof I a few years ago I recall thinking Linz had munged the conversion of (general) TM tape inputs to "H inputs" (which in Linz are binary representations of those tapes) when duplicating D's input. Now I'm not sure about that, but can't motivate myself to get to the bottom of it, since either way, if it is a problem it's clear how it should be fixed, and the basis for the proof is not affected.>
>
The proof is both "very easy" conceptually [as witnessed by how many people join in here, quickly understanding how it works if they've not come across it before], and slightly fiddly due to the TM H needing to have a fixed tape alphabet which must be able to represent any TM as well as any tape input for that TM. So there are certainly opportunities to miss details especially with a book aimed at those with a minimal maths background. Really, the only aspect of the proof requiring careful thought is convincing yourself that the fiddliness has been handled ok, along with understanding the notation used...
>
I don't see any scope for the proof actually being invalid, and PO certainly does not present any argument for it being invalid. He simply believes his H can give the right answer for his D, and that's the beginning and end of it all. When he developed his x96utm, it became possible to actually run his code, and it became /manifestly/ clear his H gets the wrong answer for D. But PO just doubles down and comes up with bizarre explanations for why he still thinks it is right when it is obviously wrong.
As I re-read Linz /again/, two points stick out:
>
"We cannot find the answer by simulating the action of M on w, say by performing it on a universal Turing machine, because there is no limit on the length of the computation. If M enters an infinite loop, then no matter how long we wait, we can never be sure that M is in fact in a loop. It may simply be a case of a very long computation. What we need is an algorithm that can determine the correct answer for any M and w by performing some
analysis on the machine's description and the input. But as we
now show, no such algorithm exists."
>
"It is important to keep in mind what Theorem 12.1 says. It does not preclude solving the halting problem for specific cases; often we can tell by an analysis of M and w whether or not the Turing machine will halt. What the theorem says is that this cannot always be done; there is no algorithm that can make a correct decision for all WM and w."
>
>
Both of these statements are self-evidently true, and both would appear to knock Mr O's HHH completely out of the water.
>
I am conscious that you have already explained to me (twice!) that Mr O's approach is aimed not at overturning the overarching indecidability proof but a mere detail of Linz's proof. Unfortunately, your explanations have not managed to establish a firm root in what passes for my brain. This may be because I'm too dense to grok them, or possibly it's because your explanations are TOAST (see above).
>Yes. PO is aiming to refute the /proof method/ that Linz (and similar) proofs use, i.e. to attack the /reasoning/ behind the proof. In effect, he is saying that his HHH/DD provide a counter-example to that reasoning. His HHH/DD are not full halt deciders - they're /partial/ halt deciders but that would be enough. I cover what a partial HD is below, and why it is enough for his argument [..if HHH/DD worked as originally claimed..]
You have said, I think, that Olcott doesn't need a universal decider in order to prove his point. But a less ambitious decider doesn't contradict Linz's proof, surely? So once more for luck, what exactly would PO be establishing with his non-universal and impatient simulator if he could only get it to work?
If he was successful with his HHH/DD programs, it would mean the Linz proof contained some logical error, and so the conclusion of the proof (the HP theorem) would not be warranted /by that proof/, We would have to cross that proof out of our Master Book Of Mathematical Theorems And Their Proofs! As there are other proofs of the theorem, the theorem itself could remain.
It would be like the following scenario: there are many alternative proofs of Pythagorus' Theorem, but let's imagine that one of them - the "MikeT" proof - is the first one taught to all school children across the world, and it's been that way for the last 50 years. Suddenly PO finds a flaw in that proof! Sure, there are other proofs without that flaw so we still trust Pythagorus' Theorem, but we're not going to continue teaching children an incorrect proof of it, right. So finding such a flaw would force many changes on our education system and be highly interesting in its own right.
This doesn't explain exactly how PO's HHH/DD would "refute" the Linz proof, so that's what the rest of the post tries to do.
BTW, when I refer to "the Linz proof" it is purely because the Linz book is apparently the one that PO has access to, and when he started posting here he claimed to have refuted the "Linz" proof that appears in that book. As you suspect, the proof is nothing to do with Linz other than appearing in his book!That Linz uses explicit state transitions transforms
It also appears I expect in some form in most computer science books covering computation theory, because it's so well known. Hmm, not sure who discovered it, but it would be one of the big guys like Turing, Church, Kleene,... all doing related work in the early days of the field.When Ĥ is applied to ⟨Ĥ⟩
----------------------
So to say what PO's code would refute, I need to explain exactly how the Linz proof works. Sorry if you already perfectly clear on that!
Les messages affichés proviennent d'usenet.