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 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: 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 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).