NetNews Usenet Archive 1992 #23/NN_1992_23.iso/spool/sci/logic/1683

Internet Message Format | 1992-10-09 | 1.3 KB

Path: sparky!uunet!mcsun!uknet!comlab.ox.ac.uk!oxuniv!loader
From: [e-mail]
Newsgroups: sci.logic
Subject: Kreisel Lacombe Shoenfield and HEO
Message-ID: <[e-mail]>
Date: 8 Oct 92 14:15:56 GMT
Organization: Oxford University VAX 6620
Lines: 26

The Kreisel-Lacombe-Shoenfield theorem states that any partial recursive
function f that gives a well defined functional on recursive functions ( ie
if {a} and {b} are total and equal then f(a)=f(b) ) is recursively continuous
( i.e. If {a} is total then there is recursive n(a) such that f(a)=f(b)
whenever {b} is total with {a}(x)={b}(x), x=0 ... n(a) )

(For a proof see eg 'Foundations of Constructive Math.', M Beeson, 1985)

It is not hard to see that the conclusion is equivalent to saying that there
is a recursive functional F with F({a})=f(a) whenever {a} is total.

Thus in terms of the model HEO, the KLS theorem states that:

   Any equivalence class of (N -> N) -> N is                         (*)
   given by a recusive functional of this type.

Question: What happens to (*) at other finite types?

For types of rank 1, this is the trivial statement that a recursive functional
with no function parameters is a recursive function.

For types of rank 2, the question can be reduced to (*).

What happens at higher types???

R Loader, Oxford