[Prev][Next][Index][Thread]

Churchian integers in PER

There seems to be enough demand for a proof that the Churchian integers
in the PER model of polymorphism are the natural numbers to post the
proof that Martin Hyland showed to Edmund and me some time ago.

Let e be in \Pi X.[[X -> X] -> [X -> X]]. 

Denote the partial function coded by the number f with the same symbol f.
For any natural number a let f^n(a) be f applied n times to a (possibly
indefined). If for all n the value f^n(a) exists, we'll say that a has
f-orbit, and write O(f,a) = { f^n(a) : n in N } for the orbit. When we write
f:O(f,a) -> O(f,a) we mean the endofunction induced by f on the diagonal
relation on O(f,a) in PER.

If O(f,a) exists, then e(f)(a) exists and is in O(f,a): we aim to show
that it is uniformly  a |---> f^r(a)   for some fixed r.

Note that e acts on any (index for a) partial recursive function g as 
g: { a : O(g,a) exists } ->  { a : O(g,a) exists }.

CLAIM. If O(f,a) is infinite, then there is a number k such that for any
partial recursive function g with O(g,a) infinite such that 
       <a,g(a),...,g^k(a)> = <a,f(a),...,f^k(a)>
one has e(f)(a) = e(g)(a).

Proof: First take an enumeration of suitable basis functions: for any sequence
without repetions u = <u_0, u_1, ..., u_k> let u~ be the partial function
such that 
            u~ (u_i) = u_{i+1}      for i < k
            u~ (u_k) = u_k
and notice that a code for u~ can be effectively computed from u.
Given f,a as in the hypothesis of the claim, define f' by the second
recursion theorem
        / f(x)  if x=f^r(a) for r < least y [e(f)(a) and e(f')(a) converge in
        |                                    less than y steps and are equal]
        |
f'(x) = < u~(x) if x=f^r(a) for r >_ least y [     ''      ''    ] (call it z)
        |          and u is the least s.t.
        |          <a,f(a),...,f^{z-1}(a)> = <u_0,u_1,...,u_{z-1}>
        \          and     e(u~)(a) =/= e(f)(a).

First note that there must be y such that 
    [e(f)(a) and e(f')(a) converge in less than y steps and are equal].
Otherwise f and f' agree as maps on O(f,a); so are equivalent in 
[O(f,a) -> O(f,a)] and e(f)(a) = e(f')(a).
Second given the least such, z say,
(*) all basis functions u~ extending <a,f(a),...,f^{z-1}(a)> are such that
     e(u~)(a) = e(f)(a).
For if not, the first u~ extending <a,...,f^{z-1}(a)> with e(u~)(a) not equal
to e(f)(a) would be equivalent to f' on [O(f,a) -> O(f,a)], so
e(u~)(a) = e(f')(a). But e(f)(a) = e(f')(a).
Let k = z-1. Now, if g is as in the claim, for some h any basis function
u~ extending <a,g(a),...,g^h(a)> is such that e(g)(a) = e(u~)(a). By taking a
basis function u~ extending both segments, e(f)(a) = e(u~)(a) = e(g)(a).

We can deduce the following:

1. For any a,f with O(f,a) infinite, there is N such that
     e(f)(a) = f^r(a)  ==>  e(f)(f^M(a)) = f^{M+r}(a) , all M > N.

Proof: Let N = max(r,k), for k,r given by the claim. Let g be (an index for)
the function which agrees with f on O(f,a) except that g(f^N(a)) = f^N(a).
Then g on {a,...,f^N(a)} is equal to a basis function extending
<a,...,f^k(a)>. Hence by (*), we have e(f)(a) = e(g)(a). 
Take now M > N, and consider the least congruence relation R on O(f,a) with
respect to the single operation g: O(f,a) -> O(f,a) such that
    a R f^M(a)  (hence  f^{M+N}(a) R f^{M+N+1}(a) R f^{M+N+2}(a) R ...).
Then g: R -> R. So f^r(a) = e(g)(a) R e(g)(f^M(a)). The last term must be in
O(g,f^M(a)) = O(f,f^M(a)), and g is equivalent to f on O(f,f^M(a)).
Hence e(f)(f^M(a)) = e(g)(f^M(a)) = f^{M+r}(a).

2. For any a,f with O(f,a) infinite,
     e(f)(a) = f^r(a)  ==> e(f)(f^n(a)) = f^{n+r}(a) , all n.

Proof: Suppose e(f)(f^n(a)) = f^{n+s}(a). For a sufficiently large K
     f^{K+r}(a) = e(f)(f^K(a)) = e(f)(f^{K-m}(f^m(a))) 
                = f^{K-m+s}(f^m(a) = f^{K+s}(a).
Hence r = s.

3. Suppose O(f,a) and O(g,b) are infinite.
     e(f)(a) = f^r(a) and e(g)(b) = g^s(b)  ==> r = s.

Proof: Let N be as in 1. Suppose m is such that the intersection of the
infinite set {g^m(b), g^{m+1}(b),...} with {a, f(a),..., f^N(a)} is empty.
Let h be (an index for) the function

   a |-> f(a) |-> ... |-> f^N(a) |-> g^m(b) |-> g^{m+1}(b) |-> ...

Then e(h)(a) = e(f)(a) = f^r(a) = h^r(a) by (*). Also
e(h)(h^{N+1}(a)) = e(h)(g^m(b)) = e(g)(g^m(b)) = g^{m+s}(b) = h^{N+1+s}(a).
Hence r = s by 2 above.

4. Suppose O(g,b) is finite, O(f,a) is infinite, and e(f)(a) = f^r(a). Then
    e(g)(b) = g^r(b).

Proof: We can assume that O(f,a) and O(g,b) are disjoint since if they aren't
we replace a by f^n(a) for some n large enough. Let X be the union of O(f,a)
and O(g,b), and h: X -> X be (an index for) the function which is f on O(f,a)
and g on O(g,b). Then 
   e(h)(b) = e(g)(b), and e(h)(a) = e(f)(a) = f^r(a).
Consider the least congruence relation R on X with respect to the single
operation h: X -> X such that  a R b. Thus h: R -> R, and
e(h)(b) R e(h)(a) = f^r(a) R g^r(b). Hence e(h)(b) = g^r(b) as required.

Putting all together, there is a unique r such that for any a with f-orbit
       e(f)(a) = f^r(a).

Remark for the effective topos enthusiast: the whole argument can be
performed on the modest sets in the effective topos as it all depends
only on some of the constructive principles true in Eff. Notice that
the claim can also be proved with a continuity argument on
(essentially) the partial recursive functions.

Pino Rosolini