Path: news.eternal-september.org!eternal-september.org!feeder3.eternal-september.org!news.quux.org!news.nk.ca!rocksolid2!i2pn2.org!.POSTED!not-for-mail
From: Richard Damon <richard@damon-family.org>
Newsgroups: comp.theory
Subject: Re: Refutation of Linz's Halting Problem Proof
Date: Sun, 20 Apr 2025 19:35:23 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <cc9713578e2f4d302b525abd44aef0311f50b882@i2pn2.org>
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: Sun, 20 Apr 2025 23:35:42 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="1196511"; mail-complaints-to="usenet@i2pn2.org";
	posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
X-Spam-Checker-Version: SpamAssassin 4.0.0
In-Reply-To: <cmeNP.2703008$nb1.2107160@fx01.ams4>
Content-Language: en-US

On 4/20/25 6:15 PM, 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.
> 
> --------------------------------------------------------------------------------
> 1. Background: Linz's Proof
> --------------------------------------------------------------------------------
> Linz demonstrates the halting problem's undecidability using a
> diagonalization

This is not a "diagonalizeation" argument. There is no need to order the 
possible deciders into a list.

> argument. He assumes a hypothetical halting oracle H(P, I), which decides
> 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.
> 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.

The proof does NOT use "self-referece", as nothing needs to "refer" to 
itself, and in fact, "reference" is a concept foreign to the domain of 
Turing Machines.

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

Or problem has no "oracles" in it. Just Programs.

>    - Type Input: The type of inputs to programs, which may include encoded
> programs
>      but excludes deciders.

Why does it exclude deciders? Why can't we give the encoding of a 
decider to a decider to decide on?

Isn't that a violation of the defintion of the decider to be able to 
decide on ALL inputs.

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

But we can't have a halting oracle, as that isn't in the domain of valid 
answers.

If you are starting by assuming H is an oracle machine, then you have 
left the domain of the problem.

Yes, Inputs can't be based on Oracle Machies, but Oracle Machines are 
not answers to the problem, which must be an actual program.

> 
> --------------------------------------------------------------------------------
> 3. Refutation of Linz's Proof
> --------------------------------------------------------------------------------
> The following arguments demonstrate that Linz's proof fails under the type
> error
> assumption:
> 
> 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.

And this is just repeating your error, H is of type PROGRAM, as your 
type "decider" is outside the bounds of the theory, allowing non-program 
oracle machines.

This just breaks the rest of your logic, and shows that you just don't 
understand what you are talking about.

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