Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: =?utf-8?Q?Re:_Refutation_of_Strachey=E2=80=99s_1965_Proof_Based_on_Self-Referential_Conflation_as_a_Category_(Type)_Error?=
Date: Thu, 24 Apr 2025 11:19:46 +0300
Organization: -
Lines: 204
Message-ID: <vucs72$167ao$2@dont-email.me>
References: <3%oNP.2703666$nb1.805417@fx01.ams4> <130c384bc4881eb654343d0ccf3ced6905a90fbb@i2pn2.org> <3QpNP.1081604$B61.671277@fx02.ams4> <vu7kke$7o3q$1@dont-email.me> <BTLNP.1469340$dBr6.1183611@fx04.ams4>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 24 Apr 2025 10:19:47 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="8b323bd0b35eb59ebd32e9261de22c1e";
	logging-data="1252696"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/lLbhSdngZx9n+tFUlLPQv"
User-Agent: Unison/2.2
Cancel-Lock: sha1:+zLCS/e8XT12n3bgDym48aR1n4w=
Bytes: 9900

On 2025-04-22 12:24:01 +0000, Mr Flibble said:

> On Tue, 22 Apr 2025 11:39:42 +0300, Mikko wrote:
> 
>> On 2025-04-21 11:18:23 +0000, Mr Flibble said:
>> 
>>> On Mon, 21 Apr 2025 06:54:33 -0400, Richard Damon wrote:
>>> 
>>>> On 4/21/25 6:21 AM, Mr Flibble wrote:
>>>>> Refutation of Strachey’s 1965 Proof Based on Self-Referential
>>>>> Conflation as a Category (Type) Error
>>>>> 
>>>>> This document refutes Christopher Strachey’s 1965 argument in “An
>>>>> Impossible Program” by leveraging the assumption that
>>>>> self-referential conflation of a halt decider and its input
>>>>> constitutes a category (type) error. The refutation demonstrates that
>>>>> Strachey’s proof, which relies on a self-referential program
>>>>> construction, is invalid in a typed system where such conflation is
>>>>> prohibited.
>>>>> 
>>>>> ---
>>>>> 
>>>>> 1. Strachey’s 1965 Argument In “An Impossible Program” (The Computer
>>>>> Journal, Vol. 7, No. 4, p. 313,
>>>>> 1965), Strachey presents a proof of the undecidability of the halting
>>>>> problem. The argument assumes a halt decider T, which determines
>>>>> whether any program P halts on a given input. Strachey constructs a
>>>>> program Strachey_P as follows:
>>>>> 
>>>>> void Strachey_P() {
>>>>> L: if (T(Strachey_P)) goto L; return;
>>>>> }
>>>>> 
>>>>> 
>>>>> Here, T(Strachey_P) checks whether Strachey_P halts. The proof
>>>>> analyzes Strachey_P’s behavior:
>>>>> - If T(Strachey_P) returns true (Strachey_P halts), Strachey_P loops
>>>>> infinitely (does not halt).
>>>>> - If T(Strachey_P) returns false (Strachey_P does not halt),
>>>>> Strachey_P halts.
>>>>> This contradiction implies that T cannot exist, proving the halting
>>>>> problem undecidable.
>>>>> 
>>>>> ---
>>>>> 
>>>>> 2. Assumption: Self-Referential Conflation as a Type Error The
>>>>> refutation assumes that the self-referential call T(Strachey_P)
>>>>> within Strachey_P constitutes a category (type) error. A type error
>>>>> occurs when an operation is applied to arguments of an inappropriate
>>>>> type.
>>>>> Here, conflating the halt decider T with its input Strachey_P (by
>>>>> allowing Strachey_P to embed T(Strachey_P)) is argued to violate type
>>>>> constraints, rendering Strachey_P ill-formed.
>>>> 
>>>> And where do you get that assumption from? It is valid logic to
>>>> temporarily assume a statement true to prove that it leads to a
>>>> contradiction and thus can't be true.
>>>> 
>>>> It is NOT valid to just assume it to be true and then use its Truth to
>>>> prove something else is true.
>>>> 
>>>> You are just showing your ignorance of the topic.
>>>> 
>>>> 
>>>>> ---
>>>>> 
>>>>> 3. Refutation The refutation proceeds by demonstrating that
>>>>> Strachey_P is invalid in a typed system due to a type error,
>>>>> undermining the contradiction in Strachey’s proof.
>>>> 
>>>> But only by an unproven assumption.
>>>> 
>>>> 
>>>>> 3.1. Type System In a typed context, the halt decider T has a type
>>>>> signature:
>>>>> T: (Program, Input) → Boolean where Program is the type of valid
>>>>> program descriptions, and Input is the type of program inputs.
>>>>> Strachey_P, as a program, must be of type Program to be a valid
>>>>> argument to T. The call T(Strachey_P) requires Strachey_P to be a
>>>>> well-defined program description.
>>>> 
>>>> Which it is, at least if T is.
>>>> 
>>>> 
>>>>> 3.2. Self-Reference as a Type Error Strachey_P’s definition includes
>>>>> T(Strachey_P), meaning Strachey_P depends on its own description as
>>>>> an argument to T. This self-reference creates a circular dependency:
>>>>> - Strachey_P’s type cannot be resolved without evaluating
>>>>> T(Strachey_P).
>>>> 
>>>> Your "type" was that it was a program. That is not a dynamically
>>>> determined category, but a statically determined one.
>>>> 
>>>> Note, that if T was a program, its actual response is solely
>>>> determined by the input it is given.
>>>> 
>>>>> - T(Strachey_P) requires Strachey_P to be a fully defined Program.
>>>>> In a strict type system, such circular definitions are rejected as
>>>>> type errors, as they violate referential transparency. Strachey_P is
>>>>> thus not a well-formed program, as its type is undefined due to the
>>>>> self-referential conflation.
>>>> 
>>>> And it is, as program definition is based on fully defining the code
>>>> of said program, and the code of Strachey_P is fully defined and built
>>>> by legal processes.
>>>> 
>>>> Your "Type System" is not "strictly" defined, but improperly defined.
>>>> 
>>>> 
>>>>> 3.3. Impact on Strachey’s Proof Strachey’s proof assumes Strachey_P
>>>>> is a valid program. If T(Strachey_P) is a type error, Strachey_P is
>>>>> ill-formed and cannot be used to derive a contradiction. The proof’s
>>>>> logic collapses, as the contradictory behavior (halting or not
>>>>> halting) depends on an invalid program. Therefore, the argument fails
>>>>> to demonstrate that T cannot exist.
>>>> 
>>>> But it IS a valid program, as the definition of a valid program is
>>>> being built on valid construction processes.
>>>> 
>>>> What "Error" was made in the construction of Strachey_P?
>>>> 
>>>> The only way for Strachey_P to be an invalid program is for T to not
>>>> be a valid one.
>>>> 
>>>> 
>>>>> 3.4. Implications By excluding self-referential programs like
>>>>> Strachey_P due to type errors, the proof’s universality is
>>>>> challenged. A halt decider T might exist for non-self-referential
>>>>> programs in a typed system, suggesting that Strachey’s proof does not
>>>>> establish undecidability in such contexts.
>>>> 
>>>> But you didn't prove your point, as there was no type error of the
>>>> types defined by the problem.
>>>> 
>>>> 
>>>>> 3.5. Critical Examination - Counterargument: Turing machines, as used
>>>>> by Strachey, are untyped, allowing self-referential programs without
>>>>> type errors.
>>>> 
>>>> Actually, Turing Machines don't support "references" at all, so there
>>>> can't BE a self-refeential program. We just are allowed to give
>>>> programs descriptions of themselves as part of "for any input".
>>>> 
>>>> And since Halt Deciders are DEFINED to answer about any program
>>>> described to them, you can't limit that domain with a type that
>>>> doesn't cover ALL programs.
>>>> 
>>>>> - Response: Imposing a type discipline on the computational model
>>>>> (e.g., typed lambda calculus) restricts self-reference. In such
>>>>> systems, Strachey_P is invalid, and the proof does not hold.
>>>> 
>>>> But you need to impose a VALID type system. A Prgram defined to take
>>>> as an input *ALL* programs (via their description) must still take in
>>>> *ALL*
>>>> programs to be valid for its definition.
>>>> 
>>>>> - Limitation: This refutation targets Strachey’s specific
>>>>> construction and does not disprove the halting problem’s
>>>>> undecidability, which is supported by other proofs (e.g., Turing
>>>>> 1936).
>>>> 
>>>> Whch means you really are admitting you aren't doing anything,
>>>> 
>>>> 
>>>>> ---
>>>>> 
>>>>> 4. Conclusion Based on the assumption that self-referential
>>>>> conflation is a type error, Strachey’s 1965 proof is refuted. The
>>>>> program Strachey_P is ill-formed due to the type error in
>>>>> T(Strachey_P), invalidating the contradiction. This highlights the
>>>>> role of type systems in computational arguments and shows that
>>>>> Strachey’s proof fails in typed contexts where self-reference is
>>>>> restricted.
>>>> 
>>>> Right, based on a false assumption you can prove a false claim.
>>>> 
>>>> Congradulations, you just proved that bad logic leads to bad
>>>> conclusions, and that your "type system" just isn't a useful tool the
>>>> way you are using it.
>>>> 
>>>> It seems you only have a hammer, and thus see everything as a Nail,
========== REMAINDER OF ARTICLE TRUNCATED ==========