Rice's Theorem comprehension check

A place to discuss the science of computers and programs, from algorithms to computability.

Formal proofs preferred.

Moderators: phlip, Moderators General, Prelates

User avatar
gmalivuk
GNU Terry Pratchett
Posts: 25789
Joined: Wed Feb 28, 2007 6:02 pm UTC
Location: Here and There
Contact:

Rice's Theorem comprehension check

Postby gmalivuk » Fri May 12, 2017 6:54 pm UTC

Refreshing my memory of the halting problem for the thread in the math forum led me to pages about Rice's Theorem, and it took me a while to wrap my head around that proof so I want to check here if I basically understand what's going on.

First of all, we know from the halting problem proof that there can be no program H(n) which always determines whether program N halts with input n. (I'm going to use capital letters for programs and lower case letters for the strings representing those programs. Also all programs take one input, which I don't always specify.)

So then suppose we have a program P(n) which determines whether (the partial function computed by) program N has some non-trivial property (i.e. a property that at least one program has and at least one program doesn't have). P outputs 1 for inputs with the property and 0 for inputs without the property.

We can assume wlog that P(n)=0 when N doesn't halt on any input. We can make this assumption because P(n) is equivalent to Q(n)=1-P(n) in the sense that they partition the set of programs into the same two subsets, so we can use whichever one outputs 0 for never-halting programs.

Because the property determined by P is non-trivial, let a be a string such that P(a)=1.

For any n, we can construct a program TN(m) which
1) Runs N(n)
2) Computes A(m)
(TN is a different program for each n, which takes m as its only input.)

But then if we define H(n) so it
1) Constructs tn as (the string corresponding to the program) described above
2) Outputs P(tn)
then H(n) is a halting oracle.
---
Is that basically correct?

I was getting confused by the first step of H, I think because I was picturing a Turing machine rather than a program written in a more human readable language. I think I get it now that I imagine H just concatenating the relevant strings of programming language.
Unless stated otherwise, I do not care whether a statement, by itself, constitutes a persuasive political argument. I care whether it's true.
---
If this post has math that doesn't work for you, use TeX the World for Firefox or Chrome

(he/him/his)

User avatar
Xanthir
My HERO!!!
Posts: 5215
Joined: Tue Feb 20, 2007 12:49 am UTC
Location: The Googleplex
Contact:

Re: Rice's Theorem comprehension check

Postby Xanthir » Fri May 12, 2017 10:26 pm UTC

I think so, yes. The proof sketch in Wikipedia makes it particularly clear to me - if you claim to have a program that can tell whether another program squares its numeric input, then I can feed it a program that does some arbitrary computation, throws the result away, then returns the square of its input. The only thing that can stop my program from returning the square of its input is if the arbitrary computation never halts; thus, your algorithm must be able to tell whether the arbitrary computation loops or halts in order to give a proper answer. It's thus trivially obvious that it must be a Halting Oracle, and is thus can't exist, per the Halting Theorem.
(defun fibs (n &optional (a 1) (b 1)) (take n (unfold '+ a b)))

User avatar
gmalivuk
GNU Terry Pratchett
Posts: 25789
Joined: Wed Feb 28, 2007 6:02 pm UTC
Location: Here and There
Contact:

Re: Rice's Theorem comprehension check

Postby gmalivuk » Sat May 13, 2017 1:35 am UTC

Yeah I saw the wiki page, but was still confused until I typed it up in my own words here.
Unless stated otherwise, I do not care whether a statement, by itself, constitutes a persuasive political argument. I care whether it's true.
---
If this post has math that doesn't work for you, use TeX the World for Firefox or Chrome

(he/him/his)


Return to “Computer Science”

Who is online

Users browsing this forum: No registered users and 4 guests