On 9/5/2025 11:06 AM, Ben Bacarisse wrote:
Richard Heathfield <rjh@cpax.org.uk> writes:
On 04/09/2025 02:17, Andr‚ G. Isaak wrote:
I think this is a simple case of terminological confusion. A decider is a >>> TM which determines membership in a particular set. It ACCEPTS inputs
which belong to the set and REJECTS input which doesn't belong to the
set. Accepting or rejecting is how it decides.
Fine by me, as long as it's clear which set is being tested. May I presume >> that ACCEPT means that DD halts? So HHH REJECTs when it should ACCEPT?
Well, PO has long ago abandoned the notion of a TM determining set membership. It's simple and clear (so used in the theory) but way too abstract and clear for PO to waffle about.
Not at all, I have just been very terrible at
communicating my position. Now that I use
conventional terms in their conventional way
my position should be much more clear.
HHH(DD) reports on the semantic (halting) property
of its input finite string that includes that DD
calls HHH(DD) in recursive emulation.
HHH accepts this finite string if DD simulated
by HHH reaches its own *SIMULATED* final halt
state and rejects it if DD correctly simulated
by any HHH cannot possibly reach its own *SIMULATED*
final halt state.
The DD() caller of HHH(DD) has never been any sort
of input to HHH(DD) thus has always been totally out
of the scope of HHH.
This exact same thing equally applies to the Linz proof
*From the bottom of page 319 has been adapted to this*
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
Machine M contains simulating halt decider H based on a UTM
M.q0 ⟨M⟩ ⊢* M.H ⟨M⟩ ⟨M⟩ ⊢* M.∞ // accept state
M.q0 ⟨M⟩ ⊢* M.H ⟨M⟩ ⟨M⟩ ⊢* M.qn // reject state
In the specific case of the Halting Problem, it seems to me to be an
utterly unnecessary abstraction.
The halting problem is entirely abstract! There is a set of encodings
(often just tapes representing natural numbers) and a halting decider
splits the set into two -- the numbers that represent finite
computations and the numbers that do not. This level of abstraction
allows the whole theory to be built in a formal manner.
It's ironic, but in PO's non-abstract model of computation (roughly
speaking C programs that do no I/O) halting is TM decidable!
And likewise the Linz proof where
M.H ⟨M⟩ ⟨M⟩ transitions to M.qn // reject state
based on the fact that
*Repeats until aborted proving non-halting*
(a) M copies its input ⟨M⟩
(b) M invokes M.H ⟨M⟩ ⟨M⟩
(c) M.H simulates ⟨M⟩ ⟨M⟩
--
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
--- MBSE BBS v1.1.2 (Linux-x86_64)
* Origin: A noiseless patient Spider (3:633/280.2@fidonet)