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.
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)