On constructive operators of finite types

V. P. Chernov

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part V, Tome 32 (1972), pp. 140-147

Résumé

Finite types and the spaces of finite type are defined as follows: the space of type $0$ is $N$; the spaces of types $(c\times d)$ and $(c\to d)$ are respectively the product of the spaces of types $c$ and $d$ and the space of constructive mappings (effective operations) from the space of type $c$ into the space of type $d$. Strong sheaf-spaces (s.s.s.) are introduced and the spaces of finite types are proved (with the help of Myhill–Shepherdson theorem) to be s.s.s. The theorem about the universal constructive mapping and the normal form theorem are proved for the mappings of s.s.s. The notion of a minimal element of s.s.s. is introduced,minimal elements of the space of partial recursive functions being general recursive functions. The structure of the set of minimal elements of s.s.s. is investigated and Ceitin–Ereisel–Lacombe–Shoenfield theorem is generalized to embeddings of arbitrary s.s.s.