{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T03:22:27Z","timestamp":1761708147529},"reference-count":68,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2007,10,1]],"date-time":"2007-10-01T00:00:00Z","timestamp":1191196800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2007,10]]},"abstract":"<jats:p>It is an empirical observation arising from the study of higher type computability that a wide range of approaches to defining a class of (hereditarily) total functionals over<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129507006251_inline1\"><jats:alt-text>$\\nat$<\/jats:alt-text><\/jats:inline-graphic>leads in practice to a relatively small handful of distinct type structures. Among these are the type structure C of Kleene\u2013Kreisel<jats:italic>continuous functionals<\/jats:italic>, its effective substructure C<jats:sup><jats:italic>eff<\/jats:italic><\/jats:sup>and the type structure HEO of the<jats:italic>hereditarily effective operations<\/jats:italic>. 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.<\/jats:p><jats:p>In this paper we present some new results that go some way towards explaining this phenomenon. Our results show that a large class of<jats:italic>extensional collapse<\/jats:italic>constructions always give rise to C, C<jats:sup><jats:italic>eff<\/jats:italic><\/jats:sup>or HEO (as appropriate). We obtain versions of our results for both the \u2018standard\u2019 and \u2018modified\u2019 extensional collapse constructions. The proofs make essential use of a technique due to Normann.<\/jats:p><jats:p>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 three type structures under consideration are highly canonical mathematical objects.<\/jats:p>","DOI":"10.1017\/s0960129507006251","type":"journal-article","created":{"date-parts":[[2007,10,29]],"date-time":"2007-10-29T03:28:35Z","timestamp":1193628515000},"page":"841-953","source":"Crossref","is-referenced-by-count":8,"title":["On the ubiquity of certain total type structures"],"prefix":"10.1017","volume":"17","author":[{"given":"JOHN","family":"LONGLEY","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2007,10,1]]},"reference":[{"key":"S0960129507006251_ref46","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (revised)","author":"Milner","year":"1997"},{"key":"S0960129507006251_ref29","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.005"},{"key":"S0960129507006251_ref44","unstructured":"Longley J. R. (2007) Notions of computability at higher types II. (In preparation.)"},{"key":"S0960129507006251_ref42","first-page":"32","volume-title":"Lecture Notes in Logic","author":"Longley","year":"2005"},{"key":"S0960129507006251_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1291-0_2"},{"key":"S0960129507006251_ref15","first-page":"138","volume-title":"Proceedings of 6th Annual Symposium on Logic in Computer Science","author":"Bucciarelli","year":"1991"},{"key":"S0960129507006251_ref65","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(99)80017-2"},{"key":"S0960129507006251_ref36","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003663"},{"key":"S0960129507006251_ref43","first-page":"87","article-title":"On the ubiquity of certain total type structures \u2013 extended abstract. In: Proceedings of the Workshop on Domains VI, Birmingham, United Kingdom","volume":"73","author":"Longley","year":"2005","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"S0960129507006251_ref35","first-page":"290","volume-title":"Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam, 1957","author":"Kreisel","year":"1959"},{"key":"S0960129507006251_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"S0960129507006251_ref30","volume-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"S0960129507006251_ref4","volume-title":"The Lambda Calculus: Its syntax and semantics","author":"Barendregt","year":"1984"},{"key":"S0960129507006251_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF02284592"},{"key":"S0960129507006251_ref28","first-page":"165","volume-title":"The L. E. J. Brouwer Centenary Symposium","author":"Hyland","year":"1982"},{"key":"S0960129507006251_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(79)90006-8"},{"key":"S0960129507006251_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9"},{"key":"S0960129507006251_ref26","unstructured":"Hyland J. M. E. (1975) Recursion theory on the countable functionals, Ph.D. thesis, University of Oxford."},{"key":"S0960129507006251_ref50","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(99)80024-X"},{"key":"S0960129507006251_ref5","unstructured":"Bauer A. (2000) The Realizability Approach to Computable Analysis and Topology, Ph.D. thesis, Carnegie Mellon University. (Available as technical report CMU-CS-00-164.)"},{"key":"S0960129507006251_ref22","first-page":"378","article-title":"Effective operations and recursive functionals (abstract)","volume":"27","author":"Gandy","year":"1962","journal-title":"Journal of Symbolic Logic"},{"key":"S0960129507006251_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90038-F"},{"key":"S0960129507006251_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45465-9_42"},{"key":"S0960129507006251_ref6","doi-asserted-by":"publisher","DOI":"10.1002\/1521-3870(200210)48:1+<1::AID-MALQ11111>3.0.CO;2-7"},{"key":"S0960129507006251_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(97)00101-1"},{"key":"S0960129507006251_ref34","first-page":"101","volume-title":"Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam, 1957","author":"Kreisel","year":"1959"},{"key":"S0960129507006251_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BF01877480"},{"key":"S0960129507006251_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003675"},{"key":"S0960129507006251_ref32","first-page":"81","volume-title":"Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam, 1957","author":"Kleene","year":"1959"},{"key":"S0960129507006251_ref1","first-page":"1","volume-title":"Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School","author":"Abramsky","year":"1999"},{"key":"S0960129507006251_ref49","first-page":"1","article-title":"The continuous functionals: computations, recursions and degrees","volume":"21","author":"Normann","year":"1981","journal-title":"Annals of Pure and Applied Logic"},{"key":"S0960129507006251_ref24","doi-asserted-by":"crossref","first-page":"138","DOI":"10.4288\/jafpos1956.3.138","article-title":"A note on continuous functionals","volume":"3","author":"Hinata","year":"1969","journal-title":"Annals of the Japan Association for Philosophy of Science"},{"key":"S0960129507006251_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(82)80002-9"},{"key":"S0960129507006251_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/BF01463138"},{"key":"S0960129507006251_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08860-1_7"},{"key":"S0960129507006251_ref37","unstructured":"Longley J. R. (1995) Realizability Toposes and Language Semantics, Ph.D. thesis, University of Edinburgh. (Available as technical report ECS-LFCS-95-332.)"},{"key":"S0960129507006251_ref31","first-page":"1","article-title":"Recursive functionals and quantifiers of finite types I","volume":"91","author":"Kleene","year":"1959","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0960129507006251_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003638"},{"key":"S0960129507006251_ref55","first-page":"389","volume-title":"Models and Computability","author":"van","year":"1999"},{"key":"S0960129507006251_ref14","doi-asserted-by":"publisher","DOI":"10.2307\/2274222"},{"key":"S0960129507006251_ref39","doi-asserted-by":"crossref","unstructured":"Longley J. R. (1999b) Unifying typed and untyped realizability. (Unpublished note available at http:\/\/www.inf.ed.ac.uk\/home\/jrl\/unifying.txt.)","DOI":"10.1016\/S1571-0661(04)00105-7"},{"key":"S0960129507006251_ref56","unstructured":"Platek R. (1966) Foundations of recursion theory, Ph.D. thesis, Stanford University."},{"key":"S0960129507006251_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00110-5"},{"key":"S0960129507006251_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00105-7"},{"key":"S0960129507006251_ref23","first-page":"407","volume-title":"Logic Colloquium 1976","author":"Gandy","year":"1977"},{"key":"S0960129507006251_ref51","doi-asserted-by":"publisher","DOI":"10.2307\/2586691"},{"key":"S0960129507006251_ref33","volume-title":"The Foundations of Intuitionistic Mathematics","author":"Kleene","year":"1965"},{"key":"S0960129507006251_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF02219096"},{"key":"S0960129507006251_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129507006251_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_38"},{"key":"S0960129507006251_ref11","first-page":"39","volume-title":"Generalized Recursion Theory II","author":"Bergstra","year":"1978"},{"key":"S0960129507006251_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.topol.2004.02.011"},{"key":"S0960129507006251_ref52","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:4)2005"},{"key":"S0960129507006251_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983504"},{"key":"S0960129507006251_ref53","doi-asserted-by":"publisher","DOI":"10.2307\/2586626"},{"key":"S0960129507006251_ref57","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0960129507006251_ref58","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90006-5"},{"key":"S0960129507006251_ref63","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"S0960129507006251_ref59","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90094-A"},{"key":"S0960129507006251_ref60","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002692"},{"key":"S0960129507006251_ref61","first-page":"335","volume-title":"Kreiseliana: About and around Georg Kreisel","author":"Schwichtenberg","year":"1996"},{"key":"S0960129507006251_ref62","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0073967"},{"key":"S0960129507006251_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0098602"},{"key":"S0960129507006251_ref64","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"S0960129507006251_ref66","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139166386"},{"key":"S0960129507006251_ref67","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0960129507006251_ref20","first-page":"455","volume-title":"Logic Colloquium 1976","author":"Ershov","year":"1976"},{"key":"S0960129507006251_ref68","volume-title":"Computability","author":"Weihrauch","year":"2000"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129507006251","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:50:37Z","timestamp":1556923837000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129507006251\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10]]},"references-count":68,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,10]]}},"alternative-id":["S0960129507006251"],"URL":"https:\/\/doi.org\/10.1017\/s0960129507006251","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10]]}}}