Liste des Groupes | Revenir à c theory |
On 5/12/2025 11:15 AM, dbush wrote:In other words, you can't identify a specific instruction that HHH emulated differently from HHH1, as Mike proved when he recently posted a side-by-side trace, and as you have previously admitted on the record:On 5/12/2025 12:09 PM, olcott wrote:When HHH emulates itself emulating DDD that callsOn 5/12/2025 10:21 AM, dbush wrote:>On 5/12/2025 11:16 AM, olcott wrote:>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
>
_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 these correctly emulated DDD instances halts.
>
In other words, you change the input.
>
Changing the input is not allowed.
>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.
Because you're changing the input.
>
Changing the input is not allowed.
>>>
HHH1(DDD) has no pathological relationship thus HHH1
never emulates itself emulating DDD.
>
HHH(DDD) has a pathological relationship thus HHH
emulates itself emulating DDD.
>
It is pretty stupid to think that above two
behaviors are identical.
>
>
False, as you have admitted on the record that both are identical up to the point that HHH aborts:
>
I never said that and that is false.
>
The behavior of DDD emulated by HHH1 and the behavior
of DDD emulated by HHH are different as soon as either
DDD calls HHH(DDD).
>
In other words, you're claiming each emulates the "call HHH" instruction differently.
>
When HHH1 emulates "call HHH", it does the following:
- pushes return address 0000217f onto the stack
- sets EIP to 000015d2, i.e. the starting address of function HHH
>
How exactly does HHH emulate that instruction differently?
>
HHH(DDD) in recursive emulation the behavior is
different in that this call cannot possibly return.
HHH1 never gets to the point of emulating itself
emulated DDD because DDD does not call HHH1(DDD)
in recursive emulation. This call returns because
there is no recursive emulation involved.
Les messages affichés proviennent d'usenet.