Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail From: Mikko 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: References: 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