XPost: comp.theory, sci.logic, sci.math

Proof that the embedded copy of Linz H in Linz Ĥ does correctly
determines the halt status of its input

CORRECT DEFINITION OF HALT DECIDING CRITERIA

(1) All deciders compute the mapping of their input finite strings to an
accept or reject state.

(2) The direct execution of a Turing machine is computationally
equivalent to the UTM simulation of its Turing machine description.

(3) Halt deciders compute the mapping of their input finite strings to
an accept or reject state on the basis of the actual behavior specified
by their input.

(4) The actual behavior specified by the input is measured by the
behavior of a UTM simulation of this input at the same point in the
execution trace as the simulating halt decider. (defined in (2) above)

Simplified Ĥ directly calls H --- infinite loop has been removed.
Ĥ.q0 ⟨Ĥ⟩ ⊢* H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qy
Ĥ.q0 ⟨Ĥ⟩ ⊢* H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qn

In other words every H remains in pure UTM mode until the outermost H
has complete proof that its simulated input would never reach its own
final state.

A simulating halt decider is in UTM mode while the behavior of its input remains computationally equivalent to the behavior of this same input
when simulated by a UTM.

(5) Linz: computation that halts … the Turing machine will halt whenever
it enters a final state. (Linz:1990:234)

(6) A correct simulation of a Turing machine description that would
never reach its final state is computationally equivalent to the direct execution of this same Turing machine never reaching its final state and
thus specifies a non-halting sequence of configurations.

Halting problem undecidability and infinitely nested simulation (V4) https://www.researchgate.net/publication/359349179_Halting_problem_undecidability_and_infinitely_nested_simulation_V4


--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)