Liste des Groupes | Revenir à theory |
On 5/3/2025 7:20 PM, Mike Terry wrote:But "Termination analyzers" are not "partial halt deciders", in fact the Termination Analyzation problem is a tougher problem than Halt Deciding because it needs to decide if the given algorithm will halt for *ALL* inputs.On 03/05/2025 20:45, Richard Heathfield wrote:Not so much programming background?On 03/05/2025 19:50, Mike Terry wrote:>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).
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.Or we could call them their software engineering name
>>>
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?
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.
of "termination analyzers".
I cover what a partial HD isAnd since it doesn't get it one input correctly, it isn't even that.
below, and why it is enough for his argument [..if HHH/DD worked as originally claimed..]
>
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! 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.
>
----------------------
>
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!
>
Say I give you a halt decider H. H is a TM, and following the mechanical instructions in Linz, you would be able to create from H a new TM H^. Basically you start with the H I gave, and edit it:
>
1) add some initial code that runs before my H gets control - that code duplicates whatever input is on the tape when it is invoked, so that if the initial tape contained "hello\0" the modified tape needs to end up "hello\0hello\0".
>
2) modify the halt states that my H used to indicate halt/non-halting when deciding its input:
- the state H uses to indicate its input halts is replaced with a tight loop
- the state H uses to indicate its input fails to halt is replaced with halt state.
Hmm, that state was a halt state in the H I gave you, so actually there's no change
for that state.
>
So, I gave you H, and you've modified it to produce a new TM H^. The essence of the Linz proof is that the logic of how H^ works / guarantees/ that when we ask my H whether your H^ halts when run against a tape containing the TM-description of H^, my H will give the wrong answer! So, my H never was a halt decider after all, because it gets a wrong answer for this particular input. Halt deciders must decide halting correctly for /every/ input i.e. every combination of P,I [P is the TM, I the input tape].
>
[I'm not explaining the proof of /why/ H will get the answer wrong. That's important of course and is in Linz and other accounts of the proof, but it's not really relevant to understanding what PO is trying to achieve.]
>
This next bit might be a missing key for you... Looking at the above, we started by me giving you a "halt decider" H. What if I only gave you a lesser achievement: a "partial halt decider" that correctly decides halting for certain (P,I) inputs, but fails to halt for all the rest? The answer is the same logic still applies, but the conclusion is slightly different:
>
- I give you a /partial/ HD H
- You follow the same instructions to create the new TM, H^
- The same reasoning of the Linz proof shows that my H does not correctly decide halting
for the case of TM H^ running against input <H^>
a) If H decides HALTS, we can show H^(<H^>) never halts
b) If H decides NEVER_HALTS, we can show H^(<H^>) halts
c) If H fails to decide (i.e. it loops) then H^(<H^>) never halts
This last possibility is new, because H is only a partial halt decider
>
Now we can look at what PO claims to have: a *partial* halt decider H, which CORRECTLY decides its corresponding input (<H^>,<H^>). Specifically, he claims his H decides NEVER_HALTS, and that indeed H^(<H^>) never halts. This contradicts the Linz proof /reasoning/ which lead to (b) above.
>
Since the Linz proof reasoning would have been shown to reach a false conclusion [in the case of PO's HHH/DD programs], the reasoning must be wrong somewhere, and if the reasoning is wrong it can't be used in the Linz proof. It is ok here that H is only a partial halt decider - in fact the above only requires that PO's H correctly decides the one H^(<H^>) case to get the contradiction.
>
Er, that's it!
>
Just as a reminder I'll repeat the final outcome of all this:
>
- PO's H does decide NEVER_HALTS for TM H^ running with input <H^>.
- PO's H^ running with input <H^> in fact halts, in line with Linz logic (b) above.
>
A final observation - nothing in this post is anything to do with "simulation". That comes later looking at how PO's H supposedly works...
>
Mike.
>
Les messages affichés proviennent d'usenet.