MIT 6.044J/18.423J                                        Handout 26
6.044 Fall 1996                                           15 December, 1996
A. R. Meyer
                        Relativized Computability


EXTENDING SCHEME WITH AN ORACLE

Let script-A be any set of S-expressions, and define Scheme^{script-A} to
be Scheme with some designated <variable>, ORACLE?, now specified to be a
<primitive procedure id> with rewrite rules

(ORACLE? V) --> #t
       if V is the value of 'S for some S in script-A,

(ORACLE? V) --> #f
       if V is the value of 'S for some S not in script-A.

A partial function on S-expressions is said to be script-A-computable iff
it can be computed by some procedure definable in Scheme^{script-A}.
Similarly, a set script-S of S-expressions is script-A decidable iff there
is a decider for it in Scheme^{script-A}; we define script-A
HALF-decidability similarly .  Another way of saying that script-S is
script-A is to say that "script-S is decidable RELATIVE TO script-A."

For example, we might want to make use of the obvious fact that if a set
script-A were decidable, then so is its complement not-script-A, i.e.,
not-script-A is the set of S-expressions not in script-A.  We prove this
obvious fact by assuming that D_A is a decider for script-A.  Then
                        (lambda (s) (not (D_A s)))
is a decider for not-script-A.

This proof is fine, but the statement of what we have proved is a little
garbled.  For example, let script-H be the Halting Problem for Scheme,
i.e., the set of Scheme expressions which halt.  Then supposing "script-H
were decidable" allows us to conclude that the moon is made of green
cheese, because a FALSE HYPOTHESIS logically implies any assertion at all,
and we know that the hypothesis that script-H is decidable is indeed
false.

The proper way to state what we have proved is:

LEMMA 1.  not-script-A is decidable relative to script-A.

Proof: (lambda (s) (not (ORACLE? s))) is a Scheme^{script-A} decider for
not-script-A.  QED.


TURING REDUCIBILITY

The notion that a set script-B is decidable relative to script-A is due to
the logician and pioneer Computer Scientist, Alan Turing.  Another way to
of expressing the fact that script-B is decidable relative to script-A is
to say script-B is "Turing reducible" to script-A, written,
                          script-B <=_T script-A.

This notation reflects the fact that Turing reducibility in transitive:

LEMMA 2.  If
                         script-C <=_T script-B,
and
                         script-B <=_T script-A,
then
                         script-C <=_T script-A.

Proof: Let D_C be a script-B decider for C, and D_B be a script-A decider
for B.  Let D'_C be the result of replacing all occurrences of the
<primitive procedure id> ORACLE? in D_C by a fresh VARIABLE, say,
"b-oracle?".  Then a script-A decider for script-C is
                (let ((b-oracle? D_B)) D'_C).                         QED


We think of Scheme^{script-A} as Scheme extended with the ability to
decide script-A.  So any set script-B which is decidable -- that is,
decidable in "real", unextended Scheme -- will certainly be decidable when
Scheme is extended.  In fact, the Scheme decider for script-B will also be
a Scheme^{script-A} decider for script-B, subject to one quibble: the
Scheme <variable> ORACLE? is re-specified to be a <primitive procedure id>
in Scheme^{script-A}, so real Scheme expressions should not use the
<variable> ORACLE? in order to behave the same way in Scheme^{A}.


LEMMA 3.  If script-B is a decidable set of S-expressions, then
                         script-B <=_T script-A,
for ANY set script-A of S-expressions.

Proof.  Let D_B be a decider for script-B.  Let D'_B be the result of
replacing all occurrences of the Scheme <variable> ORACLE? in D_B by a
fresh variable, say, FRESH?.  Then D'_B is a Scheme^{A} decider for
script-B.                       QED


A crucial property of Turing reducibility is that "decidability inherits
downwards":


LEMMA 4.  If script-B <=_T script-A, and script-A is decidable, then
script-B is decidable.

Proof: Suppose D_A is a (real Scheme) decider for script-A, and D_B is a
Scheme^{script-A} decider for script-B.  Then
                        (let ((ORACLE? D_A)) D_B)
is a decider (in real Scheme) for script-B.                QED


LEMMAS 3 and 4 together immediately imply:


COROLLARY 1.  A set script-B is decidable iff script-B  <=_T  the-empty-set.


Taking the contrapositive of LEMMA 4, we immediately conclude that
"undecidability inherits upwards" through Turing reducibility:


LEMMA 5.  If script-B <=_T script-A, and script-B is undecidable, then
script-A is undecidable.


For example, we proved in Quiz 2 that the set script-H_0 of Scheme
expressions M such that (M `M) halts is undecidable.  We did this by
showing that
                script-H  <=_T  script-H_0,
(although we didn't say it this way on the quiz).  Then, since
undecidability inherits upwards, the undecidability of the script-H
immediately implies the undecidability of script-H_0.

So LEMMA 5 captures the reasoning we have used repeatedly to prove that
problems are undecidable.


DEFINITION.  A set script-B is STRICTLY Turing reducible to script-A iff
                         script-B  <=_T  script-A
and it is NOT the case that  script-A  <=_T  script-B.

For example, we conclude directly from LEMMA's 3 and 4 that every
decidable set is strictly Turing reducible to every undecidable set.


EXERCISE 1.  Show that half-decidability does NOT inherit downwards
through Turing reducibility.  HINT: LEMMA 1.


If we could decide the Halting Problem, then we can turn half-deciders
into deciders.  The proper way to express this is


THEOREM 1.  Every half-decidable set is Turing reducible to the Scheme
Halting Problem.

Proof:  Let script-B be half-decidable with half-decider D_B.  Then
a Scheme^{script-H} decider for script-B is
         (let ((make-apply (lambda (s t) (list s t))))
           (lambda (s) (ORACLE? (make-apply 'D_B s)))).   QED


RELATIVIZATION

Many of the properties of Scheme computability hold for computability
relative to any set script-A.  For example, in Handout 17 we proved that
decidable sets are closed under union, intersection, and set-difference,
and that a set is decidable iff it and its complement are half-decidable.
The proofs of these theorems apply without any change (except for the
quibble above about not using the identifier ORACLE? as a variable) for
sets decidable relative to script-A.  So we have

THEOREM 2.  The script-A decidable sets are closed under union,
intersection, and set-theoretic difference.  A set is script-A decidable
iff it and its complement are script-A half-decidable.

In general, when a theorem about Scheme computability in fact holds for
Scheme^{script-A} computability for all sets script-A, we say that the
theorem "relativizes."  Theorems usually relativize follow because their
proofs relativize: the proofs of the original theorem apply essentially
without change when Scheme is replaced by Scheme^{script-A}.  The most
important examples of theorems and proofs which relativize are Scott's
Rice's Theorem's and the existence of meta-circular interpreters, as the
reader should verify.  As a consequence we have:

DEFINITION.  Let Halts^{script-A} be the halting problem for
Scheme^{script-A}.  That is,

Halts^{script-A} ::= {M | M is a Scheme^{script-A} expression which halts}.


THEOREM 3.  Halts^{script-A} is script-A half-decidable, but not script-A
decidable.


Someetimes our proofs of results not only relativize, but yield stronger
"partially relativized" results.  An example is Theorem 1 above.  A "full"
relativization of it would say that "Every script-A half-decidable set is
script-A Turing reducible to Halts^{script-A}."  
-------------------------

But in fact the proof does not require that we relativize
Turing-reducibility as in the underlined phrase above.  So we get a
stronger theorem by relativizing half-decidability and the halting
problem, but not Turing reducibility:

THEOREM 4.  Every script-A half-decidable set is Turing reducible to
Halts^{script-A}.

Proof: The proof is exactly that of THEOREM 1, with suitable insertions of
the bracketed phrases [script-A]:

Let script-B be [script-A] half-decidable with half-decider D_B.  Then
a Scheme^{[Halts^{script-A}]} decider for script-B is
         (let ((make-apply (lambda (s t) (list s t))))
           (lambda (s) (ORACLE? (make-apply 'D_B s)))).   QED


DEFINITION.  Halts^{script-A} is sometimes called the JUMP of script-A and
written using the alternative notation (script-A)'.

Now script-A is trivially script-A decidable -- ORACLE? is its decider --
and hence by THEOREM 2 is script-A half-decidable.  Then by THEOREM 4,
script-A is Turing reducible to Halts^{script-A}, and by Theorem 3
Halts^{script-A} is not Turing reducible to script-A.  In other words, we
have concluded:

THEOREM 5:  For any set script-A of S-expressions,
                       script-A  <_T  (script-A)' .


In particular, script-H is strictly Turing reducible to (script-H)'.  In
this way it makes precise sense to say that the halting problem for
script-H-extended Scheme is "more undecidable" than the halting problem
for ordinary Scheme, even though both problems are undecidable.

And then, since (script-H)' <_T (script-H)'', we realize that there is a
still more undecidable problem than the halting problem for
script-H-extended Scheme.  There is, of course, no end to this hierachy,
because by THEOREM 5 we have

script-H  <_T  (script-H)'  <_T  (script-H)''  <_T  (script-H)'''  <_T ....


A set of S-expressions which is Turing reducible to some set in this
sequence is called, for historical reasons, an ARITHMETIC SET.  The
"height" of an arithmetic set script-A is defined to be the least n such
that
            script-A  <=_T  (script-H)''...' .
                                       \__/   
                                       n jumps

The sequence of sets of height 0, 1, 2, ... is called the ARITHMETIC HIERARCHY.
It provides an informative way to classify undecidable sets.  

EXERCISE 2.  Let script-J be { (n S) |  S is in (script-H)''...' }.
                                                           \__/   
                                                           n jumps
Prove that script-J is not arithmetic.