On the Ubiquity of Certain Total Type Structures: (Extended Abstract)

Research output: Contribution to journalArticlepeer-review


It is a fact of experience from the study of higher type computability that a wide range of plausible approaches to defining a class of (hereditarily) total functionals over N results in a surprisingly small handful of distinct type structures. Among these are the type structure C of Kleene-Kreisel continuous functionals, its recursive substructure RC, and the type structure HEO of the hereditarily effective operations. However, the proofs of the relevant equivalences are often non-trivial, and it is not immediately clear why these particular type structures should arise so ubiquitously.

In this paper we present some new results which go some way towards explaining this phenomenon. Our results show that a large class of realizability-style constructions always give rise to C, RC or HEO (as appropriate). The proofs make essential use of a technique due to Dag Normann. In this extended abstract, we content ourselves with giving precise statements of our theorems, and a brief outline of the method of proof.

Several new results, and some previously known ones, can be obtained as instances of our theorems, but more importantly, the proofs apply uniformly to a whole family of constructions, and provide strong evidence that the above three type structures are highly canonical mathematical objects
Original languageEnglish
Pages (from-to)87-109
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 2004

Fingerprint Dive into the research topics of 'On the Ubiquity of Certain Total Type Structures: (Extended Abstract)'. Together they form a unique fingerprint.

Cite this