On 8/2/25 3:06 PM, olcott wrote:
On 8/2/2025 1:47 PM, joes wrote:
Am Fri, 01 Aug 2025 19:21:39 -0500 schrieb olcott:
On 8/1/2025 7:10 PM, Ben Bacarisse wrote:
Mr Flibble <flibble@red-dwarf.jmc.corp> writes:
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Proven what? And why can't halt deciders be decided?
Type constraints:
(B) cannot encode (A) due to uni-directionality.
WDYM "encode"?
*There is a violated type constraint in the Linz proof*
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.∞,
if Ĥ applied to ⟨Ĥ⟩ halts, and
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
if Ĥ applied to ⟨Ĥ⟩ does not halt.
The "if" statements are incorrect because Ĥ is not of the finite string >>> type.
Why should it? It is just a constraint expressed using variables.
Strings can't be applied or run.
The Linz proof requires Ĥ.embedded_H to report on its own behavior
instead of the behavior of its input.
Aren't those the same?
No Turing machine can even directly look at another
Turing machine because no TM takes another actual TM as input.
And no Turing Macine can even directly look at a number. or letter.
But they can take a representation of them.
And similarly, they can take the representation of a Turing Machine,
If you don't beleive in representation, I suggest you need to turn off
your computer, as everything you use to interface to it uses
representations.
Even the "text" you type, as all computers use are sets of 0s and 1s,
and only directly see text as arbitrary patterns of those.
Sorry, you are just proving your stupidity and that you have no problem
with lying about things you do not understand, which seems to be most thing.
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)