Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: =?utf-8?Q?Re:_Flibble=E2=80=99s_Leap:_Why_Behavioral_Divergence_Implies_a_Type_Distinction_in_the_Halting_Problem?=
Date: Tue, 13 May 2025 11:27:17 +0300
Organization: -
Lines: 110
Message-ID: <vvuvp5$1n44a$1@dont-email.me>
References: <vv1UP.77894$JJT6.54808@fx16.ams4> <vvscu1$10mib$1@dont-email.me> <vvt3bm$14pca$7@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 13 May 2025 10:27:18 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="70f604bba1da44c1dffb957c0b3101a2";
	logging-data="1806474"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18Guv/+hZLjW4M/8MheNlxK"
User-Agent: Unison/2.2
Cancel-Lock: sha1:g/kOXObzRQVF+9rnN5imBrv24ak=

On 2025-05-12 15:16:05 +0000, olcott said:

> On 5/12/2025 3:53 AM, Mikko wrote:
>> On 2025-05-11 13:21:31 +0000, Mr Flibble said:
>> 
>>> Flibble’s Leap: Why Behavioral Divergence Implies a Type Distinction in
>>> the Halting Problem
>>> =========================================================================================== 
>>> 
>>> 
>>> Summary
>>> -------
>>> Flibble argues that the Halting Problem's undecidability proof is built on
>>> a category (type) error: it assumes a program and its own representation
>>> (as a finite string) are interchangeable. This assumption fails under
>>> simulating deciders, revealing a type distinction through behavioral
>>> divergence. As such, all deciders must respect this boundary, and
>>> diagonalization becomes ill-formed. This reframing dissolves the paradox
>>> by making the Halting Problem itself an ill-posed question.
>>> 
>>> 1. Operational Evidence of Type Distinction
>>> -------------------------------------------
>>> - When a program (e.g., `DD()`) is passed to a simulating halt decider
>>> (`HHH`), it leads to infinite recursion.
>>> - This behavior differs from direct execution (e.g., a crash due to a
>>> stack overflow).
>>> - This divergence shows that the program (as code) and its representation
>>> (as data) are operationally distinct.
>>> - Therefore, treating them as the same "type" (as Turing's proof does)
>>> leads to inconsistency.
>>> 
>>> 2. Generalization to All Deciders
>>> ---------------------------------
>>> - If simulation reveals this type mismatch, then no valid decider can rely
>>> on conflating program and representation.
>>> - Diagonalization (e.g., defining D(x) = if H(x,x) then loop else halt)
>>> necessarily crosses the type boundary.
>>> - The contradiction in the Halting Problem arises from this type error,
>>> not from inherent undecidability.
>>> - Hence, the Halting Problem is ill-defined for self-referential input.
>>> 
>>> 3. Comparisons to Other Formal Systems
>>> --------------------------------------
>>> - In type-theoretic systems (like Coq or Agda), such self-reference is
>>> disallowed:
>>>   - Programs must be well-typed.
>>>   - Self-referential constructs like `H(x, x)` are unrepresentable if they
>>> would lead to paradox.
>>> - In category theory, morphisms must respect domain/codomain boundaries:
>>>   - Reflexive constructions require stratification to avoid logical
>>> inconsistency.
>>> 
>>> 4. Conclusion
>>> -------------
>>> - The Halting Problem depends on self-reference and diagonalization.
>>> - If these constructs are blocked due to type/category errors, the proof
>>> breaks down.
>>> - Thus, the Halting Problem isn’t undecidable—it’s malformed when it
>>> crosses type boundaries.
>>> - This is not a refutation of Turing, but a reformulation of the problem
>>> under more disciplined typing rules.
>>> 
>>> This model mirrors how Russell’s Paradox was avoided in modern logic: not
>>> by solving the contradiction, but by redefining the terms that made the
>>> contradiction possible.
>> 
>> The halting problem has very simple types: the input is two strings
>> and the output is a bit. The same input can be given to a UTM, so
>> the input type of the halting problem is the input type of a UTM.
>> There is no divergence of behaviour: a UTM has only one behaviour for
>> each input and no other UTM needs be considered.
> 
> That ignores a key fact

None of the several facts and other claims mentioned below is identifed
as a key fact.

> _DDD()
> [00002172] 55         push ebp      ; housekeeping
> [00002173] 8bec       mov ebp,esp   ; housekeeping
> [00002175] 6872210000 push 00002172 ; push DDD
> [0000217a] e853f4ffff call 000015d2 ; call HHH(DDD)
> [0000217f] 83c404     add esp,+04
> [00002182] 5d         pop ebp
> [00002183] c3         ret
> Size in bytes:(0018) [00002183]
> 
> One or more instructions of the above function
> are correctly emulated by different instances of
> pure x86 emulators at machine address 000015d2.

None of them is completely emulated.

> None of these correctly emulated DDD instances halts.

The (correctly or othewise or not at all) emulated DDD
halts but HHH does not emulate the halting of DDD.

> It is stupidly incorrect to simply assume that the
> pathological relationship between HHH and DDD does
> not change the behavior of DDD when it is proven
> that is does change the behavior.

The pathologial relationship is there either alweys or
never. The relationship does not change. Therefore its
consequences, if any, don't change, either.

-- 
Mikko