Syntax and semantics in higher-type recursion theory

Author:
David P. Kierstead

Journal:
Trans. Amer. Math. Soc. **276** (1983), 67-105

MSC:
Primary 03D65

DOI:
https://doi.org/10.1090/S0002-9947-1983-0684494-7

MathSciNet review:
684494

Full-text PDF Free Access

Abstract | References | Similar Articles | Additional Information

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}p$.

In this paper, we complement the syntactic structure with a syntax-free definition of recursion over $\hat {T}p$, and show that the two notions are equivalent. This system admits an enumeration theorem, in spite of the fact that the presence of partial objects complicates the coding of finite sequences. Indeed, it is not possible to code all finite sequences from type $\hat {\jmath }$ as type-$\hat {\jmath }$ objects. We use the combination of the syntactic and semantic systems to prove that, for any $\varphi : Tp^{(\sigma )} \underset {p}{\to }\mathbf {N}$, the following are equivalent:

A. $\varphi$ is recursive in the sense of Kleene [**1959**],

B. $\varphi$ is recursive in the sense of Kleene [**1978**], and

C. $\varphi$ is the pull-back in $Tp$ of some recursive $\psi :\hat {T} p^{(\sigma )} \underset {p}{\to } \mathbf {N}$. Using these equivalences, we give a necessary and sufficient condition on $\theta :T{p^{(\sigma )}} \underset {p}{\to } \mathbf {N}$, under which the substitution principle mentioned above will hold for any recursive $\varphi :T{p^{(\tau )}} \underset {p}{\to } {\mathbf {N}}$. With one trivial exception, the condition is that if $j \geqslant 1$, then $\mathfrak {A}$ must contain a variable of type greater than $j$. We feel that this result is particularly natural in the current setting.

*Handbook of mathematical logic*, Studies in Logic and the Foundations of Mathematics, vol. 90, North-Holland Publishing Co., Amsterdam, 1977. With the cooperation of H. J. Keisler, K. Kunen, Y. N. Moschovakis and A. S. Troelstra. MR**457132**- Stephen Cole Kleene,
*Introduction to metamathematics*, D. Van Nostrand Co., Inc., New York, N. Y., 1952. MR**0051790** - S. C. Kleene,
*Recursive functionals and quantifiers of finite types. I*, Trans. Amer. Math. Soc.**91**(1959), 1â€“52. MR**102480**, DOI https://doi.org/10.1090/S0002-9947-1959-0102480-9 - S. C. Kleene,
*Recursive functionals and quantifiers of finite types. II*, Trans. Amer. Math. Soc.**108**(1963), 106â€“142. MR**153557**, DOI https://doi.org/10.1090/S0002-9947-1963-0153557-4 - S. C. Kleene,
*Recursive functionals and quantifiers of finite types revisited. I*, Generalized recursion theory, II (Proc. Second Sympos., Univ. Oslo, Oslo, 1977) Stud. Logic Foundations Math., vol. 94, North-Holland, Amsterdam-New York, 1978, pp. 185â€“222. MR**516936** - S. C. Kleene,
*Recursive functionals and quantifiers of finite types revisited. II*, The Kleene Symposium (Proc. Sympos., Univ. Wisconsin, Madison, Wis., 1978), Stud. Logic Foundations Math., vol. 101, North-Holland, Amsterdam-New York, 1980, pp. 1â€“29. MR**591873**
---[to appear] - David P. Kierstead,
*A semantics for Kleeneâ€™s $j$-expressions*, The Kleene Symposium (Proc. Sympos., Univ. Wisconsin, Madison, Wis., 1978), Stud. Logic Foundations Math., vol. 101, North-Holland, Amsterdam-New York, 1980, pp. 353â€“366. MR**591890**
A. Platek [1966]

*Recursive functionals and quantifiers of finite types revisited*. III.

*Foundations of recursion theory*, Ph.D. Thesis, Stanford University, Stanford, Calif.

Retrieve articles in *Transactions of the American Mathematical Society*
with MSC:
03D65

Retrieve articles in all journals with MSC: 03D65

Additional Information

Article copyright:
© Copyright 1983
American Mathematical Society