Re: A qn on primitive recursive functions

From: peter_douglass (baisly_at_gis.net)
Date: 08/31/04 

Date: Tue, 31 Aug 2004 13:08:13 GMT

"Peter Smith" <ps218@cam.ac.uk> wrote in message
news:ps218-5624F5.09593031082004@pegasus.csx.cam.ac.uk...

> The following is true:

> There is no effective way of deciding, of some arbitrary primitive
> recursive function f(x), whether there are values x such that
> f(x) = 0.

> You can prove that readily if you already know about Turing machines and
> halting problems, or already know that the total recursive functions are
> not effectively enumerable [for if we can effectively tell which p.r.
> functions are regular, we could effectively enumerate the total
> recursive function, because we could tell which recipes for functions
> involved regular minization].
>
> But how about a more direct proof that doesn't go via results about
> Turing machines or recursive functions?

This request seems to appear somewhat regularly. I have attached
such a proof that is not depend upon Turing machines at the end of this
post. The proof is also "direct" in another sense, in that it does not
involve reductio ad absurdum.

The definitions that I give before the proof are somewhat "long".
IMHO, this helps to clarify exactly what is needed to make the
proof go through. If you are not concerned with water-tightness,
you may get away with some unexpressed assumptions. Suggestions
for making the proof shorter, without sacrificing formality
are welcome.

> Ideally, I'd like a proof that could be presented to students early on
> (just after the diagonal proof that there are computable but not p.r.
> functions and before minimization, recursive functions or Turing
> machines have entered the scene). Any offers? (And I stand prepared to
> kick myself for being really dim about this ....).

I would definitely like some feedback on whether you think this
proof is understandable to beginning students. I would also
welcome any critiques from other angles.

** An abstract proof of the halting theorem **

Assume as given the following:

A Countable Set of Machines M;
A Countable Set of Values V (not containing _|_);

A Predicate which we shall call Test
Test :: V -> Boolean
satisfying the requirement that
Exists v in V such that Test(v) is True, and
Exists v' in V such that Test(v') is False.

An injection from Machines to Values written #:
# :: M -> V ;

Pairing:
<_,_> :: V x V -> V ;

A Function Eval:
Eval :: M x V -> V + _|_
Eval gives the "result" of of running machine m in M on the input x.
If the machine halts, the result if V. If the machine does not
halt, the result is _|_ ;

(Rule of Composition)
For every pair of Machines m1 and m2 in M we can construct
a machine (m1;m2) which satisfies the following:
If m1 halts on input x, then
  Eval( (m1;m2),x) = Eval( m2, Eval(m1,x) )
Otherwise
  Eval( (m1;m2),x) = _|_

(Rule of Conditional)
For every pair of Machines m1 and m2 in M we can construct
a machine (m1 | m2) which satisfies the following:
If Test(x) then
  Eval( (m1 | m2),x) = Eval( m1, x)
 else
  Eval( (m1 | m2),x) = Eval( m2, x) ;

(Existence of non-terminating Machine)
There exists a Machine m in M such that
  forall x, Eval(m,x) = _|_
We refer such a machine satisfying
this property as LoopForever ;

(Existence of Double Machine)
There is a machine m in M
such that
   forall x, Eval(m,x) = <x,x>
We refer to such a machine as Double ;

(Existence of a Machine invariantly returning False values)
There is a machine m in M
such that
   forall x, Eval(m,x) != _|_
   and
   forall x, Test(Eval(m,x)) = False ;
We refer to such a machine as False ;

Definitions:

(Totality) Machine m in M is total
iff forall x, Eval(m,x) != _|_

(Partiality) Machine m in M is partial
 iff There exists an x such that Eval(m,x) = _|_

(Halts)
Halts :: M x V -> Bool .
Halts(m,x) = ( Eval(m,x) != _|_ )
(Note that Halts(m,x) is a well defined function.
It is not the hypothetical Turing machine "Halts" that
is proven not to exist by reductio ad absurdum in most
popular proofs of the Halting Theorem.)

(Implements)
Machine m in M partially implements Halts
iff forall x,y in V,
    Eval(m,<x,y>) != _|_ <=> Eval(m,<x,y>) = Halts(#x, y)
(That is, if m halts on input <x,y> then the value returned is
Halts(#x, y)

CLAIM:
Our claim is that for any Machine m in M,
either m does not partially compute Halts, or m is not total.
Thus, there is no Machine in M which totally computes
Halts. (This is a restatement of the Halting Theorem)

PROOF:

Construct the Machine m' given by

m' = (Double ; m ; (False | LoopForever) )

Lemma 1:
  forall x,
      !Halt(m',x) =>
           !Halts((Double ; m), x) \/
            (Halts((Double; m), x) /\ !Test(Eval((Double ; m), x)))
(proof omitted)

Let z = Eval(m',#m')

By cases,
     z is an element of V or
     z = _|_

Case 1. z is an element of V

     Eval(m',#m') != _|_ =>
     Halts(m',#m') = True =>
     Halts((Double; m ; (False | LoopForever)),#m')

     Halts(m',x) =>
     Eval(m',x) = True =>
     Test(Eval((Double ; m) , x)))

     Halts(m',#m') =>
     Test(Eval((Double ; m), #m'))) =>
     Test(Eval(m,<#m',#m'>))

     Halts(m',#m') /\ Test(Eval(m,<#m',#m'>) =>
     m does not partially implement Halts

Case 2. z = _|_

  By Lemma 1
     !Halts((Double ; m), #m') \/ (Halts((Double ; m), #m') /\
!Test(Eval((Double ; m), #m')) )

Case 2a. z = _|_ and !Halts((Double ; m), #m')
     !Halts((double ; m), #m') =>
     Eval(m,<#m',#m'>) = _|_ =>
     m is not total

Case 2b. z = _|_ and (Halts((Double ; m), #m') and !Test(Eval((Double ;
m), #m'))
      z = _|_ =>
     !Halts(m',#m')

    !Halts(m',#m') /\ !Test(Eval(m,<#m',#m'>) =>
    m does not partially implement Halts

QED

Relevant Pages

  • Re: A qn on primitive recursive functions
    ... or already know that the total recursive functions are ... If the machine halts, the result if V. ... forall x, Test) = False; ...
    (sci.logic)
  • Re: All panduks are green
    ... *If* you can represent all primitive recursive functions, ... and your theory is consistent, and your theory is r.e., ... But T cannot prove the statement "forall x, ...
    (sci.logic)
  • Re: All panduks are green
    ... *If* you can represent all primitive recursive functions, ... and your theory is consistent, and your theory is r.e., ... But T cannot prove the statement "forall x, ...
    (sci.logic)
  • Re: All panduks are green
    ... *If* you can represent all primitive recursive functions, ... and your theory is consistent, and your theory is r.e., ... But T cannot prove the statement "forall x, ...
    (sci.logic)