🚀 go-pugleaf

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