Part I Background and General Theory |
|
|
1 Introduction and Motivations |
|
|
3 | (32) |
|
|
4 | (17) |
|
|
4 | (3) |
|
1.1.2 Computable Operations |
|
|
7 | (1) |
|
1.1.3 Examples of Computability Models |
|
|
8 | (5) |
|
1.1.4 Simulating One Model in Another |
|
|
13 | (3) |
|
1.1.5 Equivalences of Computability Models |
|
|
16 | (2) |
|
1.1.6 Higher-Order Models |
|
|
18 | (3) |
|
1.2 Motivations and Applications |
|
|
21 | (6) |
|
1.2.1 Interpretations of Logical Systems |
|
|
21 | (3) |
|
1.2.2 Extracting Computational Content from Proofs |
|
|
24 | (1) |
|
1.2.3 Theory of Programming Languages |
|
|
25 | (2) |
|
1.2.4 Higher-Order Programs and Program Construction |
|
|
27 | (1) |
|
1.3 Scope and Outline of the Book |
|
|
27 | (8) |
|
|
28 | (2) |
|
1.3.2 Chapter Contents and Interdependences |
|
|
30 | (2) |
|
1.3.3 Style and Prerequisites |
|
|
32 | (3) |
|
|
35 | (16) |
|
2.1 Formative Ingredients |
|
|
35 | (3) |
|
2.1.1 Combinatory Logic and λ-Calculus |
|
|
35 | (2) |
|
2.1.2 Relative Computability and Second-Order Functionals |
|
|
37 | (1) |
|
2.1.3 Proof Theory and System T |
|
|
38 | (1) |
|
2.2 Full Set-Theoretic Models |
|
|
38 | (4) |
|
|
39 | (1) |
|
|
40 | (1) |
|
|
41 | (1) |
|
2.3 Continuous and Effective Models |
|
|
42 | (6) |
|
|
42 | (2) |
|
|
44 | (2) |
|
2.3.3 LCF as a Programming Language |
|
|
46 | (1) |
|
2.3.4 The Quest for Sequentiality |
|
|
47 | (1) |
|
|
48 | (2) |
|
2.4.1 A Unifying Framework |
|
|
48 | (1) |
|
2.4.2 Nested Sequential Procedures |
|
|
49 | (1) |
|
|
50 | (1) |
|
3 Theory of Computability Models |
|
|
51 | (64) |
|
3.1 Higher-Order Computability Models |
|
|
52 | (16) |
|
3.1.1 Computability Models |
|
|
52 | (2) |
|
3.1.2 Examples of Computability Models |
|
|
54 | (2) |
|
3.1.3 Weakly Cartesian Closed Models |
|
|
56 | (2) |
|
3.1.4 Higher-Order Models |
|
|
58 | (3) |
|
3.1.5 Typed Partial Combinatory Algebras |
|
|
61 | (3) |
|
|
64 | (2) |
|
|
66 | (2) |
|
3.2 Further Examples of Higher-Order Models |
|
|
68 | (14) |
|
3.2.1 Kleene's Second Model |
|
|
68 | (2) |
|
3.2.2 The Partial Continuous Functionals |
|
|
70 | (3) |
|
|
73 | (3) |
|
3.2.4 The van Oosten Model |
|
|
76 | (2) |
|
3.2.5 Nested Sequential Procedures |
|
|
78 | (4) |
|
3.3 Computational Structure in Higher-Order Models |
|
|
82 | (11) |
|
3.3.1 Combinatory Completeness |
|
|
82 | (3) |
|
|
85 | (1) |
|
|
86 | (1) |
|
|
87 | (2) |
|
3.3.5 Recursion and Minimization |
|
|
89 | (2) |
|
3.3.6 The Category of Assemblies |
|
|
91 | (2) |
|
3.4 Simulations Between Computability Models |
|
|
93 | (6) |
|
3.4.1 Simulations and Transformations |
|
|
93 | (4) |
|
3.4.2 Simulations and Assemblies |
|
|
97 | (2) |
|
3.5 Examples of Simulations and Transformations |
|
|
99 | (7) |
|
3.5.1 Effective and Continuous Models |
|
|
105 | (1) |
|
3.6 General Constructions on Models |
|
|
106 | (8) |
|
|
106 | (2) |
|
3.6.2 The Subset Construction |
|
|
108 | (2) |
|
3.6.3 Partial Equivalence Relations |
|
|
110 | (3) |
|
|
113 | (1) |
|
|
114 | (1) |
|
|
115 | (52) |
|
|
116 | (17) |
|
4.1.1 Interpretations of λ-Calculus |
|
|
116 | (3) |
|
4.1.2 The Internal Interpretation |
|
|
119 | (2) |
|
4.1.3 Categorical λ-Algebras |
|
|
121 | (6) |
|
4.1.4 The Karoubi Envelope |
|
|
127 | (4) |
|
4.1.5 Retraction Subalgebras |
|
|
131 | (2) |
|
4.2 Types and Retractions |
|
|
133 | (17) |
|
|
135 | (3) |
|
|
138 | (4) |
|
4.2.3 Further Type Structure in Total Settings |
|
|
142 | (2) |
|
4.2.4 Partiality, Lifting and Strictness |
|
|
144 | (5) |
|
|
149 | (1) |
|
|
150 | (6) |
|
4.4 Prelogical Relations and Their Applications |
|
|
156 | (11) |
|
4.4.1 Prelogical and Logical Relations |
|
|
157 | (2) |
|
4.4.2 Applications to System T |
|
|
159 | (4) |
|
4.4.3 Pure Types Revisited |
|
|
163 | (4) |
Part II Particular Models |
|
|
5 Kleene Computability in a Total Setting |
|
|
167 | (44) |
|
5.1 Definitions and Basic Theory |
|
|
169 | (19) |
|
5.1.1 Kleene's Definition via S1-S9 |
|
|
169 | (5) |
|
|
174 | (4) |
|
5.1.3 A λ-Calculus Presentation |
|
|
178 | (6) |
|
5.1.4 Models Arising from Kleene Computability |
|
|
184 | (2) |
|
5.1.5 Restricted Computability Notions |
|
|
186 | (2) |
|
5.2 Computations, Totality and Logical Complexity |
|
|
188 | (15) |
|
5.2.1 Logical Complexity Classes |
|
|
188 | (4) |
|
5.2.2 Top-Down Computation Trees |
|
|
192 | (6) |
|
5.2.3 Totality and the Maximal Model |
|
|
198 | (5) |
|
5.3 Existential Quantifiers and Effective Continuity |
|
|
203 | (5) |
|
5.4 Computability in Normal Functionals |
|
|
208 | (3) |
|
6 Nested Sequential Procedures |
|
|
211 | (68) |
|
6.1 The NSP Model: Basic Theory |
|
|
212 | (22) |
|
6.1.1 Construction of the Model |
|
|
212 | (4) |
|
6.1.2 The Evaluation Theorem |
|
|
216 | (9) |
|
6.1.3 Interpretation of Typed λ-Calculus |
|
|
225 | (4) |
|
6.1.4 The Extensional Quotient |
|
|
229 | (1) |
|
6.1.5 Simulating NSPs in B |
|
|
230 | (2) |
|
6.1.6 Call-by-Value Types |
|
|
232 | (1) |
|
6.1.7 An Untyped Approach |
|
|
232 | (2) |
|
6.2 NSPs and Kleene Computability |
|
|
234 | (5) |
|
6.2.1 NSPs and Kleene Expressions |
|
|
234 | (1) |
|
6.2.2 Interpreting NSPs in Total Models |
|
|
235 | (4) |
|
|
239 | (22) |
|
6.3.1 Finite and Well-Founded Procedures |
|
|
239 | (3) |
|
6.3.2 Left-Well-Founded Procedures |
|
|
242 | (4) |
|
6.3.3 Left-Bounded Procedures |
|
|
246 | (4) |
|
6.3.4 Expressive Power of T + min and Klexmin |
|
|
250 | (9) |
|
6.3.5 Total Models Revisited |
|
|
259 | (2) |
|
6.4 Kleene Computability in Partial Models |
|
|
261 | (18) |
|
6.4.1 Three Interpretations of Kleene Computability |
|
|
262 | (5) |
|
|
267 | (5) |
|
6.4.3 Relating Partial and Total Models |
|
|
272 | (4) |
|
6.4.4 Kleene Computability via Inductive Definitions |
|
|
276 | (3) |
|
|
279 | (70) |
|
7.1 Interpretations of PCF |
|
|
281 | (23) |
|
|
282 | (3) |
|
7.1.2 Mathematical Structure in Models of PCF |
|
|
285 | (2) |
|
7.1.3 Soundness and Adequacy |
|
|
287 | (2) |
|
7.1.4 Observational Equivalence and Full Abstraction |
|
|
289 | (4) |
|
7.1.5 Completeness of PCFΩ + byval for Sequential Procedures |
|
|
293 | (7) |
|
7.1.6 Relationship to Kleene Expressions |
|
|
300 | (1) |
|
7.1.7 Interpretation of NSPs Revisited |
|
|
301 | (3) |
|
7.2 Variants and Type Extensions of PCF |
|
|
304 | (5) |
|
7.2.1 Further Type Structure in Models of PCF |
|
|
304 | (2) |
|
|
306 | (3) |
|
7.3 Examples and Non-examples of PCF-Definable Operations |
|
|
309 | (14) |
|
7.3.1 Counterexamples to Full Abstraction |
|
|
310 | (2) |
|
7.3.2 The Power of Nesting |
|
|
312 | (1) |
|
|
313 | (3) |
|
|
316 | (3) |
|
7.3.5 Selection Functions and Quantifiers |
|
|
319 | (4) |
|
|
323 | (6) |
|
7.5 Sequential Functionals |
|
|
329 | (13) |
|
|
330 | (2) |
|
7.5.2 Some Partial Characterizations |
|
|
332 | (6) |
|
7.5.3 Effective Presentability and Loader's Theorem |
|
|
338 | (4) |
|
7.6 Order-Theoretic Structure of the Sequential Functionals |
|
|
342 | (4) |
|
7.7 Absence of a Universal Type |
|
|
346 | (3) |
|
8 The Total Continuous Functionals |
|
|
349 | (82) |
|
8.1 Definition and Basic Theory |
|
|
352 | (15) |
|
8.1.1 Construction via PC |
|
|
352 | (2) |
|
8.1.2 The Density Theorem |
|
|
354 | (5) |
|
8.1.3 Topological Aspects |
|
|
359 | (4) |
|
8.1.4 Computability in Ct |
|
|
363 | (4) |
|
8.2 Alternative Characterizations |
|
|
367 | (17) |
|
8.2.1 Kleene's Construction via Associates |
|
|
367 | (5) |
|
8.2.2 The Modified Associate Construction |
|
|
372 | (2) |
|
|
374 | (7) |
|
8.2.4 Compactly Generated Spaces |
|
|
381 | (1) |
|
|
382 | (1) |
|
8.2.6 Ct as a Reduced Product |
|
|
383 | (1) |
|
8.3 Examples of Continuous Functionals |
|
|
384 | (6) |
|
|
384 | (2) |
|
|
386 | (2) |
|
|
388 | (2) |
|
|
390 | (9) |
|
8.4.1 Characterizations of Compact Sets |
|
|
390 | (6) |
|
8.4.2 The Kreisel Representation Theorem |
|
|
396 | (3) |
|
8.5 Kleene Computability and tt-Computability over Ct |
|
|
399 | (22) |
|
8.5.1 Relative Kleene Computability |
|
|
399 | (12) |
|
8.5.2 Relative µ-Computability |
|
|
411 | (6) |
|
8.5.3 Computably Enumerable Degrees of Functionals |
|
|
417 | (4) |
|
8.6 Computing with Realizers |
|
|
421 | (10) |
|
8.6.1 Sequential Computability and Total Functionals |
|
|
423 | (5) |
|
8.6.2 The Ubiquity Theorem |
|
|
428 | (3) |
|
9 The Hereditarily Effective Operations |
|
|
431 | (32) |
|
9.1 Constructions Based on Continuity |
|
|
432 | (8) |
|
9.1.1 Hereditarily Effective Continuous Functionals |
|
|
432 | (3) |
|
|
435 | (5) |
|
9.2 Alternative Characterizations |
|
|
440 | (11) |
|
9.2.1 The Kreisel-Lacombe-Shoenfield Theorem |
|
|
440 | (6) |
|
9.2.2 The Modified Extensional Collapse of K1 |
|
|
446 | (4) |
|
|
450 | (1) |
|
9.3 Some Negative Results |
|
|
451 | (3) |
|
|
454 | (4) |
|
9.5 Other Relativizations of the Continuous Functionals |
|
|
458 | (5) |
|
10 The Partial Continuous Functionals |
|
|
463 | (26) |
|
10.1 Order-Theoretic and Topological Characterizations |
|
|
464 | (5) |
|
10.1.1 Definition and Order-Theoretic Structure |
|
|
464 | (3) |
|
10.1.2 Topological and Limit Characterizations |
|
|
467 | (2) |
|
|
469 | (3) |
|
10.3 PCF with Parallel Operators |
|
|
472 | (9) |
|
10.3.1 Finitary Parallel Operators |
|
|
473 | (4) |
|
10.3.2 Infinitary Parallel Operators |
|
|
477 | (3) |
|
10.3.3 Degrees of Parallelism |
|
|
480 | (1) |
|
10.4 Realizability over K2 and K1 |
|
|
481 | (4) |
|
10.5 Enumeration and Its Consequences |
|
|
485 | (3) |
|
10.6 Scott's Graph Model pω |
|
|
488 | (1) |
|
11 The Sequentially Realizable Functionals |
|
|
489 | (16) |
|
11.1 Basic Structure and Examples |
|
|
490 | (3) |
|
|
493 | (5) |
|
11.3 SR as a Maximal Sequential Model |
|
|
498 | (2) |
|
11.4 The Strongly Stable Model |
|
|
500 | (3) |
|
11.5 Order-Theoretic Structure |
|
|
503 | (1) |
|
11.6 The Stable Model and Its Generalizations |
|
|
504 | (1) |
|
12 Some Intensional Models |
|
|
505 | (30) |
|
12.1 Sequential Algorithms and van Oosten's B |
|
|
506 | (20) |
|
12.1.1 Sequential Data Structures |
|
|
507 | (2) |
|
12.1.2 A Category of Sequential Algorithms |
|
|
509 | (5) |
|
12.1.3 Simply Typed Models |
|
|
514 | (1) |
|
12.1.4 B as a Reflexive Object |
|
|
515 | (2) |
|
12.1.5 A Programming Language for Sequential Algorithms |
|
|
517 | (3) |
|
12.1.6 An Extensional Characterization |
|
|
520 | (5) |
|
12.1.7 Relation to Other Game Models |
|
|
525 | (1) |
|
12.2 Kleene's Second Model K2 |
|
|
526 | (6) |
|
12.2.1 Intensionality in K2 |
|
|
529 | (3) |
|
12.3 Kleene's First Model K1 |
|
|
532 | (3) |
|
13 Related and Future Work |
|
|
535 | (12) |
|
13.1 Deepening and Broadening the Programme |
|
|
535 | (4) |
|
13.1.1 Challenges and Open Problems |
|
|
536 | (1) |
|
13.1.2 Other Higher-Order Models |
|
|
536 | (2) |
|
13.1.3 Further Generalizations |
|
|
538 | (1) |
|
|
539 | (6) |
|
13.2.1 Computability over Non-discrete Spaces |
|
|
539 | (2) |
|
13.2.2 Computability in Analysis and Physics |
|
|
541 | (1) |
|
13.2.3 Normal Functionals and Set Recursion |
|
|
541 | (1) |
|
13.2.4 Complexity and Subrecursion |
|
|
542 | (1) |
|
|
543 | (1) |
|
13.2.6 Abstract and Generalized Computability Theories |
|
|
544 | (1) |
|
|
545 | (2) |
|
13.3.1 Metamathematics and Proof Mining |
|
|
545 | (1) |
|
13.3.2 Design and Logic of Programming Languages |
|
|
545 | (1) |
|
13.3.3 Applications to Programming |
|
|
546 | (1) |
References |
|
547 | (14) |
Index |
|
561 | |