Computable Models (eBook)
240 Seiten
Springer London (Verlag)
978-1-84882-052-4 (ISBN)
Computational models can be found everywhere in present day science and engineering. In providing a logical framework and foundation for the specification and design of specification languages, Raymond Turner uses this framework to introduce and study computable models. In doing so he presents the first systematic attempt to provide computational models with a logical foundation.
Computable models have wide-ranging applications from programming language semantics and specification languages, through to knowledge representation languages and formalism for natural language semantics. They are also implicit in computer modelling in many areas of physical and social science.
This detailed investigation into the logical foundations of specification and specification languages and their application to the definition of programming languages, coupled with a clear exposition of theories of data and computable models as mathematical notions will be welcomed by researchers and graduate students.
Computational models can be found everywhere in present day science and engineering. In providing a logical framework and foundation for the specification and design of specification languages, Raymond Turner uses this framework to introduce and study computable models. In doing so he presents the first systematic attempt to provide computational models with a logical foundation.Computable models have wide-ranging applications from programming language semantics and specification languages, through to knowledge representation languages and formalism for natural language semantics. They are also implicit in computer modelling in many areas of physical and social science.This detailed investigation into the logical foundations of specification and specification languages and their application to the definition of programming languages, coupled with a clear exposition of theories of data and computable models as mathematical notions will be welcomed by researchers and graduate students.
Preface 5
Contents 6
1 What is a Computable Model? 11
Mathematical Models 11
Specifications, Programs, and Models 12
Data Types and Programming Languages 13
Theories of Data 14
Recursive Models 15
Intensional Models 16
A Logical Foundation for Specification 17
Implementable Models 17
The Logical Setting 18
References 19
2 Typed Predicate Logic 20
Judgments and Contexts 20
Structural Rules 22
Types 22
Relations and Functions 24
Equality 24
Propositional Rules 25
Quantifier Rules 26
TPL Derivations 27
Type Inference 29
References 32
3 Data Types 34
Booleans 34
Products 36
Stacks 38
Terms 39
Numbers 39
Lists 41
A Type of Types 42
Theories of Data Types 42
References 44
4 Definability 46
Semidecidable Relations 47
Decidable Relations 48
References 50
5 Specification 52
A Logical Perspective 53
Some Specifications 54
Operations on Schema 57
Conservative Extensions 60
References 61
6 Functions 62
Totality and Functionality 62
Functional Application 63
Explicit Functions 66
The Elimination of Application 68
References 71
7 Preconditions 72
Specifications with Preconditions 72
Totality and Functionality 74
Functional Application 76
Application Elimination 78
Partial Functions 78
References 79
8 Natural Numbers 80
A Theory of Numbers 80
Numerical Specification 83
Recursive Specifications 88
Enriched Arithmetic 91
Arithmetic Interpretation 92
References 93
9 Typed Set Theory 94
CST 94
Elementary Properties 97
Subsets and Extensionality 98
New Sets from Old 99
Set-Theoretic Relations 106
Arithmetic Interpretation 109
References 111
10 Systems Modeling 112
The Requirements 112
The State 113
Operations 116
A Mathematical Model 117
References 120
11 A Type of Types 121
The Type type 122
Dependent Types 123
Dependent Specifications 124
Polymorphic Specifications 125
Polymorphic Set Theory 128
Specifications and Types 130
Arithmetic Interpretation 132
References 133
12 Schemata 134
A Theory of Relations 134
A Minimal Theory 137
Operations on Schemata 139
Arithmetic Interpretation 146
References 147
13 Separation Types 149
Theories with Separation 149
Subtypes in Specification 151
Preconditions and Functions 152
Polymorphism and Subtypes 154
The Elimination of Subtypes 155
References 159
14 Recursive Schemata 160
Closure and Induction 160
Simultaneous Recursion 163
Arithmetic Interpretation 167
Sets and Schemata 167
References 171
15 Inductive Types 172
The General Form 172
Some Inductive Types 173
Conservative Extensions 175
Finite Schemata 176
References 180
16 Recursive Functions 181
General Form 181
Numerical Recursion 184
Recursive Functions and Inductive Types 185
References 187
17 Schema Definitions 188
Schema Definitions 188
Refinement 191
Implementable Definitions 194
The Limits of Refinement 195
Properties of Schemata 196
References 197
18 Computable Ontology 198
Implementable Models 198
A Type of Events 199
Arithmetic Interpretation 200
Instants 201
Implementation 202
References 202
19 Classes 203
Classes and Judgments 203
Class Elimination 206
References 207
20 Classes of Functions 208
Function Application 208
Specifications and Function Classes 210
Partial Functions 213
Polymorphism 214
References 216
21 Computable Analysis 217
Cauchy Sequences 217
Operations on the Real Numbers 219
Implementation 220
References 222
22 Programming Language Specification 223
The Abstract Machine 223
A Programming Language and Its Specification 226
Implementation 228
References 229
23 Abstract Types 230
Axiomatic Specifications 230
Polymorphism and Data Abstraction 233
References 235
24 Conclusion 236
Index 237
| Erscheint lt. Verlag | 21.4.2009 |
|---|---|
| Sprache | englisch |
| Themenwelt | Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge |
| Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik | |
| Mathematik / Informatik ► Mathematik | |
| Technik | |
| ISBN-10 | 1-84882-052-6 / 1848820526 |
| ISBN-13 | 978-1-84882-052-4 / 9781848820524 |
| Informationen gemäß Produktsicherheitsverordnung (GPSR) | |
| Haben Sie eine Frage zum Produkt? |
Kopierschutz: Adobe-DRM
Adobe-DRM ist ein Kopierschutz, der das eBook vor Mißbrauch schützen soll. Dabei wird das eBook bereits beim Download auf Ihre persönliche Adobe-ID autorisiert. Lesen können Sie das eBook dann nur auf den Geräten, welche ebenfalls auf Ihre Adobe-ID registriert sind.
Details zum Adobe-DRM
Dateiformat: PDF (Portable Document Format)
Mit einem festen Seitenlayout eignet sich die PDF besonders für Fachbücher mit Spalten, Tabellen und Abbildungen. Eine PDF kann auf fast allen Geräten angezeigt werden, ist aber für kleine Displays (Smartphone, eReader) nur eingeschränkt geeignet.
Systemvoraussetzungen:
PC/Mac: Mit einem PC oder Mac können Sie dieses eBook lesen. Sie benötigen eine
eReader: Dieses eBook kann mit (fast) allen eBook-Readern gelesen werden. Mit dem amazon-Kindle ist es aber nicht kompatibel.
Smartphone/Tablet: Egal ob Apple oder Android, dieses eBook können Sie lesen. Sie benötigen eine
Geräteliste und zusätzliche Hinweise
Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook-orders from other countries.
aus dem Bereich