Sujet : Re: Annotated Breakdown: Linz's Halting Problem Proof and the Category Error Perspective
De : acm (at) *nospam* muc.de (Alan Mackenzie)
Groupes : comp.theoryDate : 21. Apr 2025, 00:45:45
Autres entêtes
Organisation : muc.de e.V.
Message-ID : <vu40v9$2pec$1@news.muc.de>
References : 1
User-Agent : tin/2.6.4-20241224 ("Helmsdale") (FreeBSD/14.2-RELEASE-p1 (amd64))
Mr Flibble <
flibble@red-dwarf.jmc.corp> wrote:
This is a step-by-step outline of Linz's classical proof of the
undecidability of the Halting Problem, with commentary from the
perspective of a category-theoretic critique.
It's not even clear you understand what category-theoretic even means.
This perspective suggests that certain steps in the proof involve
category errors, where roles and types of entities are improperly mixed
— for example, treating a program and a meta-level decider as
interchangeable.
You haven't said what you mean by a meta-level decider. It seems you
mean a program.
1. Assume a Halting Decider Exists Linz begins by assuming the
existence of a function H(P, x) that can determine whether program P
halts on input x.
Category-Theoretic View: This assumption does not yet involve any category
error. It describes a standard computational decider working over ordinary
program-input pairs.
Ordinary? The assumption of the existence of a halting decider is that
it applies to ALL program/input pairs. Otherwise it's not interesting.
2. Define a Contradictory Program D(P)
Construct a new program D such that:
if H(P, P) reports 'halts', then D(P) loops forever;
if H(P, P) reports 'loops', then D(P) halts.
Category-Theoretic View: This step begins to introduce potential category
confusion.
I don't think you understand what category confusion means. You haven't,
as yet, defined any categories to get confused by.
The function D is now being constructed specifically to act in
contradiction to H's analysis of P on itself, blending the role of
program and predicate. This blurs the boundary between object-level and
meta-level semantics.
There is no such boundary.
3. Invoke D on Itself
Evaluate D(D), which leads to the contradiction:
- If H(D, D) says D halts → D(D) loops
- If H(D, D) says D loops → D(D) halts
Contradiction of what, exactly? The program runs successfully and
either returns or fails to return as you indicate.
Category-Theoretic View: Here the category error is fully exposed. The
object D is passed into H and simultaneously defined in terms of H’s
result on itself.
There is no category error, here. The category is programs, and D is a
program.
This self-referential construct crosses semantic layers:
If you read up on Turing machines a bit, you'll see there's no such thing
as "self-reference" there.
a program is both subject and evaluator.
This is an essential facet of the halting problem, namely that a
purported decider has to decide ANY program/input combination.
In type-theoretic terms, this is akin to an ill-formed expression — a
form of circular logic not grounded in a well-defined semantic domain.
You haven't justified that at all, yet. There's nothing ill formed about
the program D. It's just a program. As for the rest of that paragraph,
you're just being pompous; it's not clear you understand what
"well-defined semantic domain" means.
4. Conclude H Cannot Exist
The contradiction implies that no such universal halting decider H can
exist.
Category-Theoretic View: From this perspective, the contradiction arises
not from an inherent limitation of deciders per se, ....
Correction: PURPORTED deciders. The contradiction very much exposes
their limitations.
.... but from allowing semantically invalid constructs. D(D) is seen as
undefined or outside the valid domain of discourse — not a legitimate
program-input pair, but a malformed self-referential statement.
D(D) is just an ordinary program invocation, perfectly well defined.
From the set of all program/input combinations, this just happens to be
one which the purported halting decider H gets wrong. There are many
cases where a program has itself as its input. Many compilers are
written in their own language and compile themselves, for example. A
purported halting decider which couldn't decide if a development version
of a compiler compiling itself is going to terminate wouldn't be all that
useful.
5. Interpretation
The standard interpretation is that the Halting Problem is undecidable —
there is no algorithm that can determine for all programs and inputs
whether the program halts.
Not at all. "Undecidable" means something else. The correct
interpretation is that the termination status of a program/input pair is
incomputable. That status is perfectly well defined.
Category-Theoretic View: The undecidability arises only when the system
permits semantically malformed constructions.
Who said anything about undecidability? A purported halting decider
always gives a definite result, by its definition. It's just the wrong
result a lot of the time. Such a purported halting decider doesn't just
get it's specially selected program D wrong, it gets lots of other
program/input combinations wrong too.
If the language of computation is refined to exclude category errors —
such as programs that attempt to reference or reason about their own
evaluation in this way — then within that well-formed subset, halting
may be decidable or at least non-contradictory.
You might think so, but it's not. Halting's been proven non computable
in several different ways, the proof you've outlined being just one of
them.
-- Alan Mackenzie (Nuremberg, Germany).