Path: 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: Tue, 22 Apr 2025 11:39:42 +0300
Organization: -
Lines: 189
Message-ID: <vu7kke$7o3q$1@dont-email.me>
References: <3%oNP.2703666$nb1.805417@fx01.ams4> <130c384bc4881eb654343d0ccf3ced6905a90fbb@i2pn2.org> <3QpNP.1081604$B61.671277@fx02.ams4>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 22 Apr 2025 10:39:42 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="958cb6175161903e9793602f5c1d3304";
	logging-data="254074"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19hRDMBHO+gviuK53HE/xAR"
User-Agent: Unison/2.2
Cancel-Lock: sha1:1b2qE1xCa8rEzC1iNpJXCKY/Kys=

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, even
>> if it is actually a screw.
> 
> A circular dependency is like a circular argument or circular reasoning:
> not logically sound.

A circular argument is not like a circular argument. A circular argument
means either that there is an unjustified assumption and thus the argument
is fallacious or that the proof is redundant and therefore not needed.

Dependency is not a logical concept. Statements of dependency always involve
========== REMAINDER OF ARTICLE TRUNCATED ==========