Path: ...!eternal-september.org!feeder3.eternal-september.org!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: Mon, 12 May 2025 11:53:21 +0300
Organization: -
Lines: 72
Message-ID: <vvscu1$10mib$1@dont-email.me>
References: <vv1UP.77894$JJT6.54808@fx16.ams4>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 12 May 2025 10:53:22 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="972afbe06a2d38ad56daf31aa26024ca";
	logging-data="1071691"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX180860ZSuDAaoWLOsyHlRqm"
User-Agent: Unison/2.2
Cancel-Lock: sha1:lTNbbnSgfUIx8ECsgqHD7NYoeGQ=
Bytes: 4217

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.

-- 
Mikko