Re: Refutation of Turing’s 1936 Halting Problem Proof Based on Self-Referential Conflation as a Category (Type) Error

On 21/04/2025 17:37, Mr Flibble wrote:

This document refutes Alan Turing’s 1936 proof of the undecidability of
the halting problem, as presented in “On Computable Numbers, with an
Application to the Entscheidungsproblem” (Proceedings of the London
Mathematical Society, 1936), by leveraging the assumption that self-
referential conflation of a halt decider and its input constitutes a
category (type) error. The refutation argues that Turing’s proof, which
relies on a self-referential construction, is invalid in a typed system
where such conflation is prohibited.
 ---
 1. Turing’s 1936 Halting Problem Proof
Turing’s proof demonstrates that no general algorithm (Turing machine) can
decide whether an arbitrary Turing machine halts on a given input. The
proof proceeds as follows:
 - Assume a universal Turing machine U that can simulate any Turing machine
M on input w.
- Assume a halt decider H, a Turing machine that takes as input the
description of a Turing machine M (denoted <M>) and an input w, and
outputs:
   - 1 if M halts on w.
   - 0 if M does not halt on w.
   Thus, H(<M>, w) determines whether M halts on w.
- Construct a Turing machine D (the “diagonal” machine) defined as:
   - D takes as input the description of a Turing machine <M>.
   - D runs H(<M>, <M>), i.e., it checks whether M halts when given its own
description as input.
   - If H(<M>, <M>) = 1 (M halts on <M>), D enters an infinite loop (does
not halt).
   - If H(<M>, <M>) = 0 (M does not halt on <M>), D halts.
- Apply D to its own description, i.e., evaluate D(<D>):
   - If H(<D>, <D>) = 1 (D halts on <D>), D loops infinitely (does not
halt).
   - If H(<D>, <D>) = 0 (D does not halt on <D>), D halts.
- This creates a contradiction: H’s output about D’s halting behavior
leads to the opposite behavior, implying that H cannot exist for all
Turing machines and inputs.
- Therefore, the halting problem is undecidable, as no such H can
consistently determine halting for all cases.
 Turing’s proof relies on self-reference, where D is defined in terms of
H’s evaluation of D’s own description, leading to the diagonalization
contradiction.

That's simply wrong.  D is defined in terms of H's description only.  (Specifically it does not require "H's evaluation of D's own description".)
You are trying to raise the spectre of "impredicativity" (circular definitions) but you have just misunderstood.  There nothing remotely circular in D's definition.  See [#####] below...

 ---
 2. Assumption: Self-Referential Conflation as a Type Error
The refutation assumes that the self-referential construction in Turing’s
proof—specifically, the evaluation H(<D>, <D>), where D calls H with its
own description as input—constitutes a category (type) error.

D is /derived/ from H.  D cannot "call H", but D does embed the logic of H internally.  At the point in the proof where D is defined, H is already a fixed TM.  The logic of H can certainly be incorporated inside a new TM - TMs (and algorithms generally) do that routinely.
As noted above, D's definition is not self-referential - you've just got this muddled! :)
Once D is properly defined (as in the proof), D will itself have a string description, and so can be called with that description.  (When running a TM with an input on its tape, that input can be any valid string of the appropriate input character set, such as the TM D's string description.
IOW there is no category (type) error.

A type error
occurs when an operation is applied to arguments of an inappropriate type,
resulting in undefined or invalid behavior.

Well, type errors like that would invalidate a mathematical proof.
Fortunately there is no such type error, because everything in the HP proof is of the correct type.

Here, conflating the halt
decider H with its input <D> (by allowing D to embed a call to H(<D>,
<D>)) is argued to violate type constraints, rendering D an ill-formed
Turing machine.

That's just nonsense.

 ---
 3. Refutation
The refutation demonstrates that Turing’s proof is invalid in a typed
computational model because the self-referential machine D is ill-formed
due to a type error, undermining the contradiction.

As explained above, D is a well defined TM, with a well defined TM-description.

 3.1. Type System
In a typed computational framework, the halt decider H can be assigned a
type signature:
   H: (TM_Description, Input) → {0, 1}
where:
- TM_Description is the type of valid Turing machine descriptions (e.g.,
encoded as strings or Gödel numbers).
- Input is the type of inputs accepted by the Turing machine.
- The output {0, 1} indicates whether the machine halts (1) or does not
halt (0).
The machine D, which takes a Turing machine description <M> and calls
H(<M>, <M>), must itself be a valid Turing machine with a description <D>
of type TM_Description. For H(<D>, <D>) to be well-typed, <D> must be a
fully defined TM_Description.
 3.2. Self-Reference as a Type Error
In Turing’s construction, D is defined such that it calls H(<D>, <D>),
meaning D’s behavior depends on H’s evaluation of D’s own description.
This self-reference introduces a circular dependency:
- D’s description <D> must be well-defined for H(<D>, <D>) to be a valid
computation.
- However, D’s definition includes the call to H(<D>, <D>), meaning <D> is
not fully defined until H’s computation is resolved.

[#####]
Ah, this seems to be where you've gone wrong!
D's definition does /not/ "include the call to H(<D>, <D>)".  It /couldn't/ do that, because D is not defined at this point in the proof.
H is already defined, so D's definition can embed the logic of H, which I'll refer to as embedded_H.   What D's definition actually says is that D effectively invokes embedded_H (my_input, my_input) where my_input is whatever is on D's tape.  This does not require <D> to be already defined, only H.   And once D is defined, <D> is well defined.
It is only later in the proof when considering D run with input <D> that we see embedded_H (<D>, <D>).  By this time in the proof D is properly defined.  I.e. D (and hence <D> is fully resolved before embedded_H's computation is introduced in the proof.

- This circularity creates a type error in a strict type system, as D’s
type (TM_Description) cannot be resolved without evaluating H(<D>, <D>),
which in turn requires a complete <D>.
In typed systems (e.g., typed lambda calculus or modern programming
languages), such self-referential definitions are often rejected at the
type-checking stage. For example, a program that uses its own source code
as an argument in a recursive manner may fail type checking if the type
system prohibits unresolved recursive dependencies. Thus, D is not a well-
formed Turing machine in a typed framework, as its description is invalid
due to the self-referential conflation.

No, this is your previous mistake coming out (there is no "self-referential conflation").  D is a well formed TM.
Regarding types generally, the HP proof is a mathematical proof, and mathematical proofs require appropriate use of types at all points in the proof although the terminology is usually different. E.g. proofs talk of entities being "well defined" which incorporates an idea of types.  Like say we define a function f: N ---> N  [a function f mapping natural numbers 0,1,2,3... to natural numbers] with f(n) = n+1 for all n.  When we subsequently use f, its argument must be a natural number.  An expression such as f(Pi) in the proof is not well defined and the proof would be broken - a "type error" we could say.
The HP proof has various types that must be adhered to, e.g. TM, TM-description, tape_input, tape_input_description and so on.  It seems to me that the HP proof uses entities of correct type at all points, and the examples you've raised so far have just been mistakes or misunderstandings on your part.  E.g. H(<D>,<D>) needs:
-  H to be a TM taking TM-description and input+description   [tick]
-  <D>,<D> to be a TM-description and input+description   [tick]
-  D to be a TM in order for <D> to be a valid TM_descriptioin   [tick]
-  and so on.
To be fair, these techie details are rather fiddly, and I recall thinking that the Linz proof had got the details munged somewhat - but it was a case of clearly fixable laziness/inattention rather than anything fundamental to the proof.

 3.3. Impact on Turing’s Proof
Turing’s proof assumes that D is a valid Turing machine whose description
<D> can be passed to H. If H(<D>, <D>) constitutes a type error, then D is
not a well-formed Turing machine, and the evaluation D(<D>) is undefined.
The contradiction derived from analyzing D’s behavior—halting if and only
if it does not halt—relies on D being a legitimate machine. Since D is
illformed due to the type error, the contradiction does not hold, and the
proof fails to demonstrate that H cannot exist.

H(<D>, <D>) does not constitute a type error etc.
[no further comments - I've not read any further]
Mike.

 3.4. Implications
By classifying self-referential constructions like D as type errors, the
proof’s generality is undermined. If self-referential Turing machines are
excluded from the set of valid machines due to type constraints, then H
might exist for non-self-referential machines in a typed system. This
suggests that Turing’s proof does not establish the undecidability of the
halting problem in computational models where self-reference is restricted
by type discipline.
 3.5. Critical Examination
- Counterargument: Turing’s proof operates in the untyped domain of Turing
machines, where any string can represent a valid machine description,
including self-referential ones like <D>. Type errors are irrelevant in
this context, and D is a legitimate construction.
- Response: While Turing machines are untyped, the assumption of a type
error can be applied by imposing a type discipline on the model of
computation. For example, in typed computational frameworks (e.g., typed
lambda calculus or formal systems with type safety), self-referential
definitions are restricted to ensure well-formedness. By reinterpreting
Turing’s proof in such a framework, H(<D>, <D>) is flagged as a type
error, rendering D invalid and the proof unsound.
- Limitation: This refutation specifically targets Turing’s
diagonalization argument and does not negate the undecidability of the
halting problem in general. Other proofs, such as those based on
reductions to other undecidable problems (e.g., the Post correspondence
problem), may avoid self-referential constructions and remain unaffected.
Additionally, the halting problem’s undecidability is well-established in
untyped systems, so the refutation is limited to typed contexts.
 ---
 4. Conclusion
Based on the assumption that self-referential conflation of a halt decider
and its input is a category (type) error, Turing’s 1936 proof of the
halting problem’s undecidability is refuted in a typed computational
framework. The diagonal machine D is ill-formed due to the type error in
H(<D>, <D>), as its self-referential definition violates type constraints.
Since the proof’s contradiction depends on D being a valid Turing machine,
the type error invalidates the argument. This refutation highlights the
significance of type systems in computational theory and suggests that
Turing’s proof does not hold in typed contexts where self-reference is
prohibited. However, it does not challenge the broader undecidability of
the halting problem in untyped systems or via alternative proofs.