Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: wij <wyniijj5@gmail.com>
Newsgroups: comp.theory
Subject: Re: Can Moving the Paradox Code into the SHD Layer Reintroduce the
 Halting Problem?
Date: Sun, 25 May 2025 21:08:40 +0800
Organization: A noiseless patient Spider
Lines: 81
Message-ID: <d4fc479722fcc73b0ba822beaebd049b457d7898.camel@gmail.com>
References: <XtBYP.501017$wBVe.207428@fx06.ams4>
MIME-Version: 1.0
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Injection-Date: Sun, 25 May 2025 15:08:42 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="5d64dd4dba03fd5772c2b57948096626";
	logging-data="1445910"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX187MiJP46o6b5QSYm3453E6"
User-Agent: Evolution 3.54.3 (3.54.3-1.fc41)
Cancel-Lock: sha1:J31MoBaGZQNaxo4nj8xamzJc+Kc=
In-Reply-To: <XtBYP.501017$wBVe.207428@fx06.ams4>

On Sun, 2025-05-25 at 09:33 +0000, Mr Flibble wrote:
> Can Moving the Paradox Code into the SHD Layer Reintroduce the Halting=
=20
> Problem?
> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D
>=20
> Question:
> ---------
> In the neos solution (Flibble's typed SHD model), programs are split into=
=20
> two layers:
> - The SHD layer (meta-level) that analyzes programs.
> - The program layer that cannot reference the SHD.
>=20
> What happens if you move the paradoxical construction (e.g., D() =3D if H=
(D)=20
> then loop) into the SHD layer itself?
>=20
> Analysis:
> ---------
>=20
> 1. Stratification Prevents Self-Reference (If Enforced)
> --------------------------------------------------------
> - Typed SHD systems (like Coq, Agda, or neos with layered semantics) can=
=20
> prevent self-reference by using type stratification.
> - In this setup, the SHD layer cannot analyze itself.
> - The construction of `D'` within the SHD layer, which calls `H(D')`,=20
> would be semantically ill-typed and rejected.
>=20
> 2. If SHDs Can Analyze Themselves, the Paradox Returns
> -------------------------------------------------------
> - If SHDs are allowed to analyze other SHDs or themselves, you can=20
> reintroduce the diagonal construction:
> =C2=A0=C2=A0=C2=A0 D': if H(D') then loop forever; else halt;
> - This results in the same contradiction as in the classical halting=20
> problem proof.
>=20
> Conclusion:
> -----------
> - Moving the paradox into the SHD layer only prevents the contradiction i=
f=20
> the SHD layer is **itself** stratified and prevents self-analysis.
> - The paradox is not avoided merely by code relocation=E2=80=94it is avoi=
ded by=20
> **semantic restriction**.
> - The issue is not *where* the paradox is written, but *what is allowed*=
=20
> in the system.
>=20
> Final Verdict:
> --------------
> You can't escape the Halting Problem paradox simply by shifting the code=
=20
> to a different layer. You must redefine your system's rules to prevent an=
y=20
> form of self-reference in all layers, including the SHD meta-level.

CSCall++ already solved the 'self-reference' problem >20 years ago from the=
 very
beginning of the project: Self-reference is inenevitable.

"... This guideline (of CSCall++ library) has no strong opinion on how this=
 self-ops
 should be handled, yet (it is like divided by zero error). Implement may c=
heck the
 self-ops (not generally doable) and return ELOOP. Working around might be =
needed=C2=A0
 since the intent mostly assumes the argument is passed by value, nonethele=
ss a
 theoretical bug might be thus hidden..."

Whatever you "SHD" is=C2=A0(assuming you are one genius who can hit the tar=
get no one can see),
it suffers the same basic problem as POOH: No one can reproduce what you sa=
y, even yourself.