Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:On the ubiquity of certain total type structures
Authors: John Longley
Date: 2005
Publication Title:Mathematical Structures in Computer Science
Publication Type:Conference Paper Publication Status:Published
Volume No:17 (5) Page Nos:841-953
DOI:10.1017/S0960129507006251 ISBN/ISSN:1469-8072
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 CF of Kleene-Kreisel continuous functionals, its recursive substructure RCF, 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 extensional collapse constructions always give rise to CF, RCF or HEO (as appropriate). We obtain versions of our results for both the ``standard'' and ``modified'' extensional collapse constructions. The proofs make essential use of a technique due to Normann. Many new results, as well as 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.
Links To Paper
1st Link
Bibtex format
author = { John Longley },
title = {On the ubiquity of certain total type structures},
book title = {Mathematical Structures in Computer Science},
year = 2005,
volume = {17 (5)},
pages = {841-953},
doi = {10.1017/S0960129507006251},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh