Liste des Groupes | Revenir à theory |
On 23/05/2025 19:37, Keith Thompson wrote:Ben Bacarisse <ben@bsb.me.uk> writes:>Mike Terry <news.dead.person.stones@darjeeling.plus.com> writes:[...]And the big picture is that this can be done because false is theHmm. I don't read that the way you do. Did I miss something?
correct halting decision for some halting computations. He has said
this explicitly (as I have posted before) but he has also explained it
in words:
>
| When-so-ever a halt decider correctly determines that its input would
| never halt unless forced to halt by this halt decider this halt
| decider has made a correct not-halting determination.
It assumes that the input is a non-halting computation ("its input
would never halt") and asserts that, in certain circumstances,
his mythical halt decider correctly determines that the input
is non-halting.
When his mythical halt decider correctly determines that its input
doesn't halt, it has made a correct non-halting determination.
It's just a tautology.
You're reading it the way most people would, and in the way I said Sipser
would be interpreting the oft-quoted "Sipser quote". I don't think you've
missed anything particularly.
I suppose Ben quoted PO saying this, because PO /uses/ it to justify that a
particular /halting/ computation will never halt,
Les messages affichés proviennent d'usenet.