Muutke küpsiste eelistusi

Higher-Order Computability 1st ed. 2015 [Kõva köide]

  • Formaat: Hardback, 571 pages, kõrgus x laius: 235x155 mm, kaal: 9989 g, 2 Illustrations, color; XVI, 571 p. 2 illus. in color., 1 Hardback
  • Sari: Theory and Applications of Computability
  • Ilmumisaeg: 17-Nov-2015
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • ISBN-10: 3662479915
  • ISBN-13: 9783662479919
  • Kõva köide
  • Hind: 150,61 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Tavahind: 177,19 €
  • Säästad 15%
  • Raamatu kohalejõudmiseks kirjastusest kulub orienteeruvalt 2-4 nädalat
  • Kogus:
  • Lisa ostukorvi
  • Tasuta tarne
  • Tellimisaeg 2-4 nädalat
  • Lisa soovinimekirja
  • Formaat: Hardback, 571 pages, kõrgus x laius: 235x155 mm, kaal: 9989 g, 2 Illustrations, color; XVI, 571 p. 2 illus. in color., 1 Hardback
  • Sari: Theory and Applications of Computability
  • Ilmumisaeg: 17-Nov-2015
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • ISBN-10: 3662479915
  • ISBN-13: 9783662479919
This book offers a self-contained exposition of the theory of computability in a higher-order context, where "computable operations" may themselves be passed as arguments to other computable operations. The subject originated in the 1950s with the work of Kleene, Kreisel and others, and has since expanded in many different directions under the influence of workers from both mathematical logic and computer science. The ideas of higher-order computability have proved valuable both for elucidating the constructive content of logical systems, and for investigating the expressive power of various higher-order programming languages.In contrast to the well-known situation for first-order functions, it turns out that at higher types there are several different notions of computability competing for our attention, and each of these has given rise to its own strand of research. In this book, the authors offer an integrated treatment that draws together many of these strands within a unify

ing framework, revealing not only the range of possible computability concepts but the relationships between them.The book will serve as an ideal introduction to the field for beginning graduate students, as well as a reference for advanced researchers

Introduction and Motivation.- Historical Survey.- Theory of Computability Models.- Theory of Lambda Algebras.- Kleene Computability in a Total Setting.- Nested Sequential Procedures.- PCF and Its Models.- Total Continuous Functionals.- Hereditarily Effective Operations.- Partial Continuous Functionals.- Sequentially Realizable Functionals.- Some Intensional Models.- Related and Future Work.- References.- Index.

Arvustused

This book is a true tour de force. The content is both mathematics and computer science; it is simultaneously an introductory textbook for students, a tutorial for seasoned researchers, a reference work, and a research monograph; ... The references to the literature are thorough. The writing is technical mathematics, and is good by that standard: there is ample intuitive explanation, and it is overall readable. (Robert S. Lubarsky, Mathematical Reviews, April 2018)

Part I Background and General Theory
1 Introduction and Motivations
3(32)
1.1 Computability Models
4(17)
1.1.1 Data and Datatypes
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)
1.3.1 Scope of the Book
28(2)
1.3.2
Chapter Contents and Interdependences
30(2)
1.3.3 Style and Prerequisites
32(3)
2 Historical Survey
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)
2.2.1 Kleene
39(1)
2.2.2 Platek
40(1)
2.2.3 Kleene Again
41(1)
2.3 Continuous and Effective Models
42(6)
2.3.1 Kleene-Kreisel
42(2)
2.3.2 Scott-Ershov
44(2)
2.3.3 LCF as a Programming Language
46(1)
2.3.4 The Quest for Sequentiality
47(1)
2.4 The Third Millennium
48(2)
2.4.1 A Unifying Framework
48(1)
2.4.2 Nested Sequential Procedures
49(1)
2.5 Summary
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)
3.1.6 Lax Models
64(2)
3.1.7 Type Worlds
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)
3.2.3 Typed A-Calculi
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)
3.3.2 Pairing
85(1)
3.3.3 Booleans
86(1)
3.3.4 Numerals
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)
3.6.1 Quotients
106(2)
3.6.2 The Subset Construction
108(2)
3.6.3 Partial Equivalence Relations
110(3)
3.6.4 Type Structures
113(1)
3.7 Prospectus
114(1)
4 Theory of λ-Algebras
115(52)
4.1 Typed λ-Algebras
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)
4.2.1 Pure Types
135(3)
4.2.2 Product Types
138(4)
4.2.3 Further Type Structure in Total Settings
142(2)
4.2.4 Partiality, Lifting and Strictness
144(5)
4.2.5 Universal Types
149(1)
4.3 Partial λ-Algebras
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)
5.1.2 Basic Properties
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)
6.3 Substructures of SP°
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)
6.4.2 Least Fixed Points
267(5)
6.4.3 Relating Partial and Total Models
272(4)
6.4.4 Kleene Computability via Inductive Definitions
276(3)
7 PCF and Its Models
279(70)
7.1 Interpretations of PCF
281(23)
7.1.1 Models of PCF
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)
7.2.2 Call-by-Value PCF
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)
7.3.3 Bar Recursion
313(3)
7.3.4 The Fan Functional
316(3)
7.3.5 Selection Functions and Quantifiers
319(4)
7.4 Game Models
323(6)
7.5 Sequential Functionals
329(13)
7.5.1 Basic Properties
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)
8.2.3 Limit Spaces
374(7)
8.2.4 Compactly Generated Spaces
381(1)
8.2.5 Filter Spaces
382(1)
8.2.6 Ct as a Reduced Product
383(1)
8.3 Examples of Continuous Functionals
384(6)
8.3.1 Bar Recursion
384(2)
8.3.2 The Fan Functional
386(2)
8.3.3 The Γ Functional
388(2)
8.4 Fine Structure of Ct
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)
9.1.2 The Kleene Tree
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)
9.2.3 Ubiquity of HEO
450(1)
9.3 Some Negative Results
451(3)
9.4 Logical Complexity
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)
10.2 A Universal Domain
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)
11.2 A Universal Type
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)
13.2 Neighbouring Areas
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)
13.2.5 Transfinite Types
543(1)
13.2.6 Abstract and Generalized Computability Theories
544(1)
13.3 Applications
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