by S. Abramsky, Dov. M. Gabbay and T. S. E. Maibaum
ISBN: 9780198537816
Logic is now widely recognized as one of the foundational disciplines of computing, and its applications reach almost every aspect of the subject, from software engineering and hardware to programming languages and AI. The Handbook of Logic in Computer Science is a multi-volume work covering all the major areas of application of logic to theoretical computer science. The handbook comprises six volumes, each containing five or six chapters giving an in-depth overview of one of the major topics in field. It is the result of many years of cooperative effort by some of the most eminent frontline researchers in the field, and will no doubt be the standard reference work in logic and theoretical computer science for years to come. Volume 5: Algebraic and Logical Structures covers all the fundamental topics of semantics in logic and computation. The extensive chapters are the result of several years of coordinated research, and each have thematic perspective. Together, they offer the reader the latest in research work, and the book will be indispensable.
List of contributors p. xvii
Martin-Lof's type theory p. 1
Introduction p. 1
Different formulations of type theory p. 3
Implementations p. 4
Propositions as sets p. 4
Semantics and formal rules p. 7
Types p. 7
Hypothetical judgements p. 9
Function types p. 12
The type Set p. 14
Definitions p. 15
Propositional logic p. 16
Set theory p. 19
The set of Boolean values p. 20
The empty set p. 21
The set of natural numbers p. 21
The set of functions (Cartesian product of a family of sets) p. 23
Propositional equality p. 26
The set of lists p. 28
Disjoint union of two sets p. 29
Disjoint union of a family of sets p. 29
The set of small sets p. 30
The ALF series of interactive editors for type theory p. 32
Categorial logic p. 39
Introduction p. 40
Equational logic p. 43
Syntactic considerations p. 44
Categorical semantics p. 45
Internal languages p. 48
Categorical datatypes p. 50
Disjoint union types p. 52
Product types p. 57
Function types p. 60
Inductive types p. 62
Computation types p. 65
Theories as categories p. 67
Change of category p. 68
Classifying category of a theory p. 68
Theory-category correspondence p. 73
Theories with datatypes p. 75
Predicate logic p. 77
Formulas and sequents p. 77
Hyperdoctrines p. 78
Satisfaction p. 82
Propositional connectives p. 84
Quantification p. 89
Equality p. 93
Completeness p. 97
Dependent types p. 100
Syntactic considerations p. 101
Classifying category of a theory p. 107
Type-categories p. 109
Categorical semantics p. 114
Dependent products p. 119
Further reading p. 123
A uniform method for proving lower bounds on the computational complexity of logical theories p. 129
Introduction p. 129
Preliminaries p. 135
Reductions between formulas p. 140
Inseparability results for first-order theories p. 151
Inseparability results for monadic second-order theories p. 158
Tools for NTIME lower bounds p. 164
Tools for linear ATIME lower bounds p. 173
Applications p. 180
Upper bounds p. 196
Open problems p. 204
Algebraic specification of abstract data types p. 217
Introduction p. 219
Algebras p. 220
The basic notions p. 220
Homomorphisms and isomorphisms p. 223
Abstract data types p. 224
Subalgebras p. 225
Quotient algebras p. 225
Terms p. 227
Syntax p. 227
Semantics p. 228
Substitutions p. 229
Properties p. 229
Generated algebras, term algebras p. 230
Generated algebras p. 230
Freely generated algebras p. 233
Term algebras p. 234
Quotient term algebras p. 235
Algebras for different signatures p. 235
Signature morphisms p. 235
Reducts p. 237
Extensions p. 238
Logic p. 239
Definition p. 239
Equational logic p. 240
Conditional equational logic p. 241
Predicate logic p. 241
Models and logical consequences p. 243
Models p. 243
Logical consequence p. 244
Theories p. 245
Closures p. 246
Reducts p. 248
Extensions p. 248
Calculi p. 249
Definitions p. 249
An example p. 250
Comments p. 251
Specification p. 252
Loose specifications p. 253
Genuinely loose specifications p. 253
Loose specifications with constructors p. 255
Loose specifications with free constructors p. 256
Initial specifications p. 257
Initial specifications in equational logic p. 257
Examples p. 258
Properties p. 260
Expressive power of initial specifications p. 260
Proofs p. 261
Term rewriting systems and proofs p. 263
Rapid prototyping p. 265
Initial specifications in conditional equational logic p. 266
Comments p. 266
Constructive specifications p. 267
Specification languages p. 270
A simple specification language p. 271
Two further language constructs p. 274
Adding an environment p. 278
Flattening p. 281
Properties and proofs p. 282
Rapid prototyping p. 282
Further language constructs p. 282
Alternative semantics description p. 283
Modularization and parameterization p. 284
Modularized abstract data types p. 284
Atomic module specifications p. 285
A modularized specification language p. 287
A parameterized specification language p. 290
Comments p. 294
Alternative parameter mechanisms p. 295
Further topics p. 297
Behavioural abstraction p. 297
Implementation p. 299
Ordered sorts p. 301
Exceptions p. 302
Dynamic data types p. 304
Objects p. 306
Bibliographic notes p. 308
The categorical approach p. 309
Categories p. 309
Institutions p. 309
Computable functions and semicomputable sets on many-sorted algebras p. 397
Introduction p. 319
Computing in algebras p. 322
Examples of computable and non-computable functions p. 325
Relations with effective algebra p. 329
Historical notes on computable functions on algebras p. 335
Objectives and structure of the chapter p. 340
Prerequisites p. 343
Signatures and algebras p. 344
Signatures p. 344
Terms and subalgebras p. 349
Homomorphisms, isomorphisms and abstract data types p. 350
Adding Booleans: Standard signatures and algebras p. 351
Adding counters: N-standard signatures and algebras p. 353
Adding the unspecified value u; algebras A[superscript u] of signature [Sigma superscript u] p. 355
Adding arrays: Algebras A* of signature [Sigma]* p. 356
Adding streams: Algebras A of signature [Sigma] p. 359
While computability on standard algebras p. 360
Syntax of While([Sigma])361
States p. 363
Semantics of terms p. 363
Algebraic operational semantics p. 364
Semantics of statements for While([Sigma]) p. 366
Semantics of procedures p. 368
Homomorphism invariance theorems p. 371
Locality of computation p. 372
The language While Proc([Sigma]) p. 374
RelativeWhile computability p. 375
For([Sigma]) computability p. 376
While[superscript N] and For[superscript N] computability p. 377
While* and For* computability p. 378
Remainder set of a statement; snapshots p. 380
[Sigma]*/[Sigma] conservativity for terms p. 383
Representations of semantic functions; universality p. 387
Godel numbering of syntax p. 388
Representation of states p. 389
Representation of term evaluation p. 389
Representation of the computation step function p. 390
Representation of statement evaluation p. 392
Representation of procedure evaluation p. 393
Computability of semantic representing functions; term evaluation property p. 394
Universal While[superscript N] procedure for While p. 397
Universal While[superscript N] procedure for While* p. 401
Snapshot representing function and sequence p. 402
Order of a tuple of elements p. 404
Locally finite algebras p. 405
Representing functions for specific terms or programs p. 406
Notions of semicomputability p. 407
While semicomputability p. 408
Merging two procedures: Closure theorems p. 409
Projective While semicomputability: semicomputability with search p. 413
While[superscript N] semicomputability p. 414
Projective While[superscript N] semicomputability p. 416
Solvability of the halting problem p. 416
While* semicomputability p. 420
Projective While* semicomputability p. 421
Homomorphism invariance for semicomputable sets p. 422
The computation tree of a While statement p. 423
Engeler's lemma p. 425
Engeler's lemma for While* semicomputability p. 429
[Sigma]*[subscript 1] definability: Input/output and halting formulae p. 431
The projective equivalence theorem p. 434
Halting sets of While procedures with random assignments p. 435
Examples of semicomputable sets of real and complex numbers p. 438
Computability on R and C p. 439
The algebra of reals; a set which is projectively While semicomputable but not While* semicomputable p. 441
The ordered algebra of reals; sets of reals which are While semicomputable but not While* computable p. 443
A set which is projectively While* semicomputable but not projectively While[superscript N] semicomputable p. 445
Dynamical systems and chaotic systems on R; sets which are While[superscript N] semicomputable but not While* computable p. 447
Dynamical systems and Julia sets on C; sets which are While[superscript N] semicomputable but not While* computable p. 449
Computation on topological partial algebras p. 451
The problem p. 452
Partial algebras and While computation p. 453
Topological partial algebras p. 455
Discussion: Two models of computation on the reals p. 458
Continuity of computable functions p. 460
Topological characterisation of computable sets in compact algebras p. 464
Metric partial algebra p. 465
Connected domains: computability and explicit definability p. 465
Approximable computability p. 470
Abstract versus concrete models for computing on the real numbers p. 475
A survey of models of computability p. 479
Computability by function schemes p. 479
Machine models p. 484
High-level programming constructs; program schemes p. 488
Axiomatic methods p. 490
Equational definability p. 490
Inductive definitions and fixed-point methods p. 492
Set recursion p. 493
A generalised Church-Turing thesis for computability p. 493
A Church-Turing thesis for specification p. 496
Some other applications p. 500
Index p. 525
Another Logic Books
Download
No comments:
Post a Comment