Syntax and semantics in higher-type recursion theory
David P. Kierstead · Transactions of the American Mathematical Society · 1983
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 φ ( α j + 1 , A ) \varphi ({\alpha ^{j + 1}},\mathfrak {A}) and θ ( β j , A ) \theta ({\beta ^j},\mathfrak {A}) are recursive, then there should be a recursive ψ ( A ) \psi (\mathfrak {A}) such that ψ ( A ) ≃ φ ( λ β j θ ( β j , A ) , A ) \psi (\mathfrak {A}) \simeq \varphi (\lambda {\beta ^j}\theta ({\beta ^j},\mathfrak {A}),\mathfrak {A}) at least whenever λ β j θ ( β j , A ) \lambda {\beta ^j}\theta ({\beta ^j},\m