On 20/04/2025 23:15, Mr Flibble wrote:
================================================================================
Refutation of Linz's Halting Problem Proof
Based on Type Error Assumption
================================================================================
Date: April 20, 2025
This document refutes Peter Linz's proof of the undecidability of the
halting
problem, as presented in "An Introduction to Formal Languages and
Automata," under
the assumption that self-referential input conflating deciders with
programs
constitutes a category (type) error. By enforcing a type system that
separates
deciders from programs, the diagonalization argument central to Linz's
proof is
invalidated, challenging the claim of universal undecidability.
I think you genuinely mean well with this argument, but IMO you have completely missed what's going on with the Linz proof.
Linz is proving a result specifically about *TMs*, as are other similar proofs by other authors. The reason TMs are chosen as the model of computing is:
a) that it is the best model we know of for representing "algorithms" in the real world.
b) the various other computing model candidates that have been proposed such as lambda-calculus
and the likes are all easily seen to be equivalent to TMs
c) we need to fix on some mathematical framework in order to make mathematical claims about
e.g. the /non-existence/ of "algorithms" with certain properties. We all know
(Turing/Church thesis) that we cannot prove
mathematically that no other real-world computation method exists, but nobody knows of
such and the general belief is that TMs adequately cover what we mean by "algorithm"
[accepting that that is not something provable mathematically].
If instead of fixing on a mathematically precise model of computing [such as TMs], we
just talk about "effective computing" [which is more of a philosophical idea for "what
can be calculated by some means or other"] then we could argue that certain things
can be "effectively calculated", but we would have nowhere to start if we want to
argue that something /wasn't/ effectively calculable - that needs a precise definition
of calculation.
So that is /why/ all these proofs focus on TMs or TM equivalents. We can talk mathematically about entities like oracles or infinite (non-terminating) computations, but we have no belief that such oracles exist in the real world in a way that can actually calulate anything - hence we ask whether *A TM* halt decider exists.
Anyhow, regardless of /why/ we do this, THIS IS WHAT IS DONE IN LINZ AND SIMILAR HP PROOFS. And what we are all doing here in comp.theory in the PO threads. Of course, PO talks in terms of x86 architectures and so on, but ultimately everything relates back to the TM computing model as in the Linz proof, which he claims to have refuted. Forget talk of oracles and the likes!
If we acknowledge we are dealing with TMs only (as we are for HP proof), then
a) an algorithm/program means a *TM*
b) a decider is also a *TM* (obviously not all TMs are deciders)
c) TMs and input tapes can be encoded as finite strings which can appear on a TM
input tape (for suitably specified TMs supporting the required symbol set).
We can fix the representation so that a TM supporting the right
input/tape symbol set etc. can process /any/ (TM+input tape) correctly coded as
a finite string.
d) in particular ALL deciders, *being TMs* can be so encoded as a valid input tape
for any putative halt decider TM - they are all just TMs.
e) all TM + input tape combinations either halt or do not halt, so asking whether
a halt decider exists that decides for a valid string representation of the
(TM + input) becomes a well defined question mathematical question.
f) There is no "category/type" error anywhere, SINCE ALL DECIDERS ARE ALSO TMS.
IF we were considering mathematical oracles which report TM halting (as mathematcians can and have investigated) then "deciders" would NOT necessarily be TMs and trying to apply the TM HP proof in such a scenario would not work, due in effect to the sort of type errors you talk of below.
BUT JUST TO MAKE IT ABSOLUTELY CLEAR - LINZ AND OTHERS (INCLUDING PO) ARE TALKING ONLY ABOUT TMS, and the Linz proof is valid in that setting.
I've highlighted below where your argument goes off the rails for the Linz (TM based) proof.
--------------------------------------------------------------------------------
1. Background: Linz's Proof
--------------------------------------------------------------------------------
Linz demonstrates the halting problem's undecidability using a
diagonalization
argument. He assumes a hypothetical halting oracle H(P, I), which decides
NO - he assumes a *TM* H, no oracles or TM extensions etc. just a plain TM.
whether
program P halts on input I. A program D is constructed such that:
- D uses H to check if D(D) halts.
- If H(D, D) says D(D) halts, D loops; otherwise, it halts.
Right. H is one particular fixed TM.
D is a modification of H, and is also a particular TM. Any TM, including D, can be represented as a finite string suitable for running with any halt decider TM, including H. No type error here, and nothing invalid or remotely dodgy in running H with the string representation of D on its tape.
This creates a contradiction: D(D) halts if and only if it does not,
implying no
such H exists. The proof relies on self-reference, where D is both the
program and
input to H.
If we accept this as a kind of self-reference, it is not of a "dodgy" kind, like circular definitions where a new entity is defined in terms of itself. Nothing circular like that is happening.
First H is /given/ (fixed), and D is then uniquely defined in terms of H, being guaranteed to exist if H exists. The string version of D is then properly defined, and H can certainly be run with that string (indeed, with /any/ string of the conforming tape symbol set) as its input. No circular definitions here.
--------------------------------------------------------------------------------
2. Assumption: Self-Reference as a Type Error
--------------------------------------------------------------------------------
The refutation assumes that self-referential input, where a decider (e.g.,
H) is
conflated with the program being decided (e.g., D), is a category error in
a typed
computational model. We define:
- Type Program: The type of executable programs (e.g., Turing machines).
- Type Decider: The type of decision procedures (e.g., oracles deciding
properties of programs).
- Type Input: The type of inputs to programs, which may include encoded
programs
but excludes deciders.
The HP proof is specifically concerning TMs, and deciders are a specialisation of TMs. Input to deciders does not exclude (encoded) deciders - all are just enoded TMs and encoded tape data, i.e. exactly the correct sort of data for feeding to a halt decider.
In this system, the halting oracle has signature H: Program x Input ->
{halt, loop}.
Self-referential cases, where P = H or I encodes H, are ill-typed because
H is of > type Decider, not Program.
In HP proof, Decider is a specialisation of Program and is valid input for other deciders. No type errors / category errors.
--------------------------------------------------------------------------------
3. Refutation of Linz's Proof
--------------------------------------------------------------------------------
The following arguments demonstrate that Linz's proof fails under the type
error
assumption:
Incorrect assumption for Linz proof.
3.1 Type Restriction Invalidates Self-Reference
------------------------------------------------
Constructing D such that D(D) queries H(D, D) commits a type error. Since
H is of
type Decider, it cannot be passed as a Program to itself, nor can D
(derived from H)
be a valid input to H. The type system enforces that inputs to H are of
type Input,
excluding Decider or programs embedding H. Thus, H(D, D) is undefined, and
D's
construction is invalid.
3.2 Collapse of Diagonalization Argument
------------------------------------------------
Linz's proof depends on H being applicable to all pairs (P, I), including
(D, D).
By disallowing self-referential inputs, the diagonalization step—where
D(D) halts
if and only if it does not—cannot be derived. Without this contradiction,
the proof
fails to show that H cannot exist.
Incorrect assumption has (unsurprisingly) led to incorrect conclusion.
3.3 Decidability in a Typed Model
------------------------------------------------
In a typed system, a halting oracle H could decide halting for well-typed
inputs
(where P ≠ H and I does not encode H). Linz's proof assumes a type-free
model, but
in a typed model, the halting problem may be decidable for restricted
cases,
undermining the claim of universal undecidability.
Yes, but within the "TM type system", Decider is a specialisation of TM, so there is no type error. You are just saying that OTHER systems can exist where Decider is NOT a specification of TM, and in those other systems, the HP proof does not apply. [Also note that D is not actually a decider]
We all know that - search for "TM halting oracles" and the likes and you will find this is all well understood.
Meanwhile, nothing in the (TM specific) Linz proof is invalidated by what you say because there are no type errors or improperly defined entities (self referential or otherwise).
It seems to me that with the clarification that Linz is dealing ONLY WITH TMs, and that deciders are TMs, that you ought to recognise that [FOR THIS SCENARIO] the Linz proof is valid, and that no TM halt decider for TM halting exists. But knowing how this sort of thread generally goes I won't put any money on it! :)
Regards,
Mike.
Re: Refutation of Linz's Halting Problem Proof