Path: ...!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: wij <wyniijj5@gmail.com>
Newsgroups: comp.theory
Subject: Re: Another Halting Problem Question (very difficult)
Date: Wed, 29 May 2024 10:04:15 +0800
Organization: A noiseless patient Spider
Lines: 53
Message-ID: <2db54a94832639405021f300652e0b6690a9dea9.camel@gmail.com>
References: <e59d06e61850db2c77d1a784abce13dc84067079.camel@gmail.com>
	 <19b48c13e1abe0c0c68ece8114535d43a771cd3c.camel@gmail.com>
	 <47d52c4babb83d32286f6bf597b415151d3e4fda.camel@gmail.com>
	 <1f231ededa977e799945496518d7aa8e2f7efc4a.camel@gmail.com>
	 <DO2dnck8JrFdGcv7nZ2dnZfqn_WdnZ2d@brightview.co.uk>
MIME-Version: 1.0
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Injection-Date: Wed, 29 May 2024 04:04:16 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="356615fa2e3e10e4de8b1fb8357c2248";
	logging-data="1021935"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/xcMXZCw8XrC7eRQf0Yco5"
User-Agent: Evolution 3.50.2 (3.50.2-1.fc39)
Cancel-Lock: sha1:H2txpES3FspoyBj5aSEdW8zPXqM=
In-Reply-To: <DO2dnck8JrFdGcv7nZ2dnZfqn_WdnZ2d@brightview.co.uk>
Bytes: 2889

On Wed, 2024-05-29 at 02:28 +0100, Mike Terry wrote:
> On 29/05/2024 01:31, wij wrote:
> [..snip..]
> >=20
> > Revision:
> > Does there exist a decision function sat that determines whether or not=
 a
> > terminating function bool f() (given as the argument of sat) returns tr=
ue or
> > not? IOW, sat(f)=3D=3Dtrue iff f()=3D=3Dtrue.
> >=20
> Yes.=C2=A0 A UTM meets your requirement, given that the input domain is l=
imited to terminating functions=20
> f().
>=20
> > Is Rice's theorem (or GUR if you like) refuted?
> >=20
> No.=C2=A0 You may be thinking that identifying functions that return true=
 is identifying a "semantic=20
> property of functions" as required for Rice.=C2=A0 But your requirement a=
bove is restricted to a domain=20
> containing only halting programs, so does not match Rice's theorem requir=
ements.
>=20
>=20
> Mike.
>=20

Rice's theorem: Any nontrivial property about the language recognized by a =
Turing machine is
undecidable.=20
http://kilby.stanford.edu/~rvg/154/handouts/Rice.html

The above translated me: Any nontrivial property about a computation functi=
on
is undecidable.

typedef bool (*Func)();
bool sat(Func f);

1. Func includes lots of nontrivial functions.
2. sat(f) can't be proved undecidable by Halting Problem like method. I gue=
ss
   Rice's theorem is based on the same method for its claim.

   E.g. This typical example won't work. Because whenever u is proven=20
        undecidable, u is an Invalid Input (Olcott 2024).

        bool u() {
          return sat(u);
        }