Path: news.eternal-september.org!eternal-september.org!feeder3.eternal-september.org!news.szaf.org!news.karotte.org!news.space.net!news.muc.de!.POSTED.news.muc.de!not-for-mail
From: Alan Mackenzie <acm@muc.de>
Newsgroups: comp.theory
Subject: Re: Annotated Breakdown: Linz's Halting Problem Proof and the Category Error Perspective
Date: Sun, 20 Apr 2025 23:45:45 -0000 (UTC)
Organization: muc.de e.V.
Message-ID: <vu40v9$2pec$1@news.muc.de>
References: <_cdNP.1582076$Xb1.667097@fx05.ams4>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Injection-Date: Sun, 20 Apr 2025 23:45:45 -0000 (UTC)
Injection-Info: news.muc.de; posting-host="news.muc.de:2001:608:1000::2";
	logging-data="91596"; mail-complaints-to="news-admin@muc.de"
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=20
> undecidability of the Halting Problem, with commentary from the=20
> 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
> =E2=80=94 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 categ=
ory=20
> error. It describes a standard computational decider working over ordin=
ary=20
> 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 catego=
ry=20
> 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 =E2=86=92 D(D) loops
>     - If H(D, D) says D loops =E2=86=92 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=20
> object D is passed into H and simultaneously defined in terms of H=E2=80=
=99s=20
> 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:=20

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 =E2=80=
=94 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=20
> exist.

> Category-Theoretic View: From this perspective, the contradiction arise=
s=20
> 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 =E2=80=94 not a legi=
timate
> 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 =
=E2=80=94=20
> there is no algorithm that can determine for all programs and inputs=20
> 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=
=20
> 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 =E2=
=80=94
> such as programs that attempt to reference or reason about their own
> evaluation in this way =E2=80=94 then within that well-formed subset, h=
alting
> 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.

--=20
Alan Mackenzie (Nuremberg, Germany).