Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mike Terry <news.dead.person.stones@darjeeling.plus.com>
Newsgroups: comp.theory
Subject: Re: Refutation of Linz's Halting Problem Proof
Date: Mon, 21 Apr 2025 03:43:09 +0100
Organization: A noiseless patient Spider
Lines: 202
Message-ID: <vu4bbt$19f07$1@dont-email.me>
References: <cmeNP.2703008$nb1.2107160@fx01.ams4>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 21 Apr 2025 04:43:10 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="1290843d3454ebcce1c683cda01aeea6";
	logging-data="1358855"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+i4UjL65QkDyD4Jvye1j3g5Y1uugmfl1k="
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.18.2
Cancel-Lock: sha1:7PP03eyIsc/ujjJNq2Hk6sj5mfk=
In-Reply-To: <cmeNP.2703008$nb1.2107160@fx01.ams4>

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
========== REMAINDER OF ARTICLE TRUNCATED ==========