Abstract:

recursion in higher types was introduced by S. C. Kleene in 1959. Since that time, it has come to be recognized as a natural and important generalization of ordinary recursion theory. Unfortunately, the theory contains certain apparent anomalies, which stem from the fact that higher type computations deal with the intensions of their arguments, rather than the extensions. This causes the failure of the substitution principle (that if $\varphi ({\alpha ^{j + 1}},\mathfrak {A})$ and $\theta ({\beta ^j},\mathfrak {A})$ are recursive, then there should be a recursive $\psi (\mathfrak {A})$ such that $\psi (\mathfrak {A}) \simeq \varphi (\lambda {\beta ^j}\theta ({\beta ^j},\mathfrak {A}),\mathfrak {A})$ at least whenever $\lambda {\beta ^j}\theta ({\beta ^j},\mathfrak {A})$ is total), and of the first recursion principle (that if ${\mathbf {F}}(\zeta ;\mathfrak {A})$ is a recursive functional, then the minimal solution $\zeta$ of the equation ${\mathbf {F}}(\zeta ;\mathfrak {A}) \simeq \zeta (\mathfrak {A})$ should be recursive as well). In an effort to remove—or at least explain—these anomalies, Kleene, in 1978, developed a system for computation in higher types which was based entirely on the syntactic manipulation of formal expressions, called $j$-expressions. As Kleene pointed out, no adequate semantics for these expressions can be based on the classical (total) type structure $Tp$ over ${\mathbf {N}}$. In a paper to appear in The Kleene Symposium (North-Holland), we showed that an appropriate semantics could be based on the type structure $\hat {T}p$, which is obtained by adding a new object $\mathfrak {u}$ at level $0$ and, at level $(j + 1)$, allowing all monotone, partial functions from type $\hat {\jmath }$ into ${\mathbf {N}}$. Over $\hat {T}p$, both of the principles mentioned above do hold. There is a natural embedding to $Tp$ into $\hat {T