Handbook of Logic in Computer Science. Volume 5: Logic and Algebraic Methods

Martin-L6f s type theory 1
B. Nordstrtim, K. Petersson and J. M. Smith
1 Introduction 1
1.1 Different formulations of type theory 3
1.2 Implementations 4
2 Propositions as sets 4
3 Semantics and formal rules 7
3.1 Types 7
3.2 Hypothetical judgements 9
3.3 Function types 12
3.4 The type Set 14
3.5 Definitions 15
4 Prepositional logic 16
5 Set theory 19
5.1 The set of Boolean values 20
5.2 The empty set 21
5.3 The set of natural numbers 21
5.4 The set of functions
(Cartesian product of a family of sets) 23
5.5 Prepositional equality 26
5.6 The set of lists 28
5.7 Disjoint union of two sets29
5.8 Disjoint union of a family of sets 29
5.9 The set of small sets 30
6 The ALF series of interactive editors for type theory 32

Categorial logic 39
Andrew M. Pitts
1 Introduction 40
2 Equational logic 43
2.1 Syntactic considerations 44
2.2 Categorical semantics 45
2.3 Internal languages 48
3 Categorical datatypes 50
3.1 Disjoint union types 52
3.2 Product types 57
3.3 Function types 60
3.4 Inductive types 62
3.5 Computation types 65
4 Theories as categories 67
4.1 Change of category 68
4.2 Classifying category of a theory 68
4.3 Theory-category correspondence 73
4.4 Theories with datatypes 75
5 Predicate logic 77
5.1 Formulas and sequents 77
5.2 Hyperdoctrines 78
5.3 Satisfaction 82
5.4 Prepositional connectives 84
5.5 Quantification 89
5.6 Equality 93
5.7 Completeness 97
6 Dependent types 100
6.1 Syntactic considerations 101
6.2 Classifying category of a theory 107
6.3 Type-categories 109
6.4 Categorical semantics 114
6.5 Dependent products 119
7 Further reading 123

A uniform method for proving lower bounds
on the computational complexity of
logical theories 129
K. Compton and C. Ward Henson
1 Introduction 129
2 Preliminaries 135
3 Reductions between formulas 140
4 Inseparability results for first-order theories 151
5 Inseparability results for monadic second-order theories 158
6 Tools for NTIME lower bounds 164
7 Tools for linear ATIME lower bounds 173
8 Applications 180
9 Upper bounds 196
10 Open problems 204

Algebraic specification of abstract data types 217
J. Loeckx, H.-D. EhrichandM. Wolf
1 Introduction 219
2 Algebras 220
2.1 The basic notions 220
2.2 Homomorphisms and isomorphisms 223
2.3 Abstract data types 224
2.4 Subalgebras 225
2.5 Quotient algebras 225
3 Terms 227
3.1 Syntax 227
3.2 Semantics 228
3.3 Substitutions 229
3.4 Properties 229
4 Generated algebras, term algebras 230
4.1 Generated algebras 230
4.2 Freely generated algebras 233
4.3 Term algebras 234
4.4 Quotient term algebras 235
5 Algebras for different signatures 235
5.1 Signature morphisms 235
5.2 Reducts 237
5.3 Extensions 238
6 Logic 239
6.1 Definition 239
6.2 Equational logic 240
6.3 Conditional equational logic 241
6.4 Predicate logic 241
7 Models and logical consequences 243
7.1 Models 243
7.2 Logical consequence 244
7.3 Theories 245
7.4 Closures 246
7.5 Reducts 248
7.6 Extensions 248
8 Calculi 249
8.1 Definitions 249
8.2 An example 250
8.3 Comments 251
9 Specification 252
10 Loose specifications 253
10.1 Genuinely loose specifications 253
10.2 Loose specifications with constructors 255
10.3 Loose specifications with free constructors 256
11 Initial specifications 257
11.1 Initial specifications in equational logic 257
11.2 Examples 258
11.3 Properties 260
11.4 Expressive power of initial specifications 260
11.5 Proofs 261
11.6 Term rewriting systems and proofs 263
11.7 Rapid prototyping 265
11.8 Initial specifications in conditional equational 266
logic
11.9 Comments 266
12 Constructive specifications 267
13 Specification languages 270
13.1A simple specification language 271
13.2 Two further language constructs 274
13.3 Adding an environment 278
13.4 Flattening 281
13.5 Properties and proofs 282
13.6 Rapid prototyping 282
13.7 Further language constructs 282
13.8 Alternative semantics description 283
14 Modularization and parameterization 284
14.1 Modularized abstract data types 284
14.2 Atomic module specifications 285
14.3 A modularized specification language 287
14.4 A parameterized specification language 290
14.5 Comments 294
14.6 Alternative parameter mechanisms 295
15 Further topics 297
15.1 Behavioural abstraction 297
15.2 Implementation 299
15.3 Ordered sorts 301
15.4 Exceptions 302
15.5 Dynamic data types 304
15.6 Objects 306
15.7 Bibliographic notes 308
16 The categorical approach 309
16.1 Categories 309
16.2 Institutions 309

Computable functions and semicomputable sets
on many-sorted algebras 397
J. V Tucker and J. I. Zucker
1 Introduction 319
1.1 Computing in algebras 322
1.2 Examples of computable and non-computable functions 325
1.3 Relations with effective algebra 329
1.4 Historical notes on computable functions on algebras 335
1.5 Objectives and structure of the chapter 340
1.6 Prerequisites 343
2 Signatures and algebras 344
2.1 Signatures 344
2.2 Terms and subalgebras 349
2.3 Homomorphisms, isomorphisms and abstract data types 350
2.4 Adding Booleans: Standard signatures and algebras 351
2.5 Adding counters: V-standard signatures and algebras 353
2.6 Adding the unspecified value u; algebras Au of signature Su 355
2.7 Adding arrays: Algebras A* of signature £_* 356
2.8 Adding streams: Algebras A of signature £ 359
3 While computability on standard algebras 360
3.1 Syntax of While(£)361
3.2 States 363
3.3 Semantics of terms 363
3.4 Algebraic operational semantics 364
3.5 Semantics of statements for While(E,) 366
3.6 Semantics of procedures 368
3.7 Homomorphism invariance theorems 371
3.8 Locality of computation 372
3.9 The language While Proc(S) 374
3.10 RelativeWhile computability 375
3.11 For(E) computability 376
3.12 WhileN and ForN computability 377
3.13 While* and For* computability 378
3.14 Remainder set of a statement; snapshots 380
3.15 E*/E conservativity for terms 383
4 Representations of semantic functions; universality 387
4.1 Godel numbering of syntax 388
4.2 Representation of states 389
4.3 Representation of term evaluation 389
4.4 Representation of the computation step function 390
4.5 Representation of statement evaluation 392
4.6 Representatipn of procedure evaluation 393
4.7 Computability of semantic representing functions; term 394
evaluation property
4.8 Universal WhileN procedure for While 397
4.9 Universal WhileN procedure for While* 401
4.10 Snapshot representing function and sequence 402
4.11 Order of a tuple of elements 404
4.12 Locally finite algebras 405
4.13 Representing functions for specific terms or programs 406
5 Notions of semicomputability 407
5.1 While semicomputability 408
5.2 Merging two procedures: Closure theorems 409
5.3 Projective While semicomputability: semicomputability 413
with search
5.4 WhileN semicomputability 414
5.5 Projective WhileN semicomputability 416
5.6 Solvability of the halting problem 416
5.7 While* semicomputability 420
5.8 Projective While* semicomputability 421
5.9 Homomorphism invariance for semicomputable sets 422
5.10 The computation tree of a While statement 423
5.11 Engeler\'s lemma 425
5.12 Engeler\'s lemma for While* semicomputabitity 429
5.13 £1* definability: Input/output and halting formulae 431
5.14 The projective equivalence theorem 434
5.15 Halting sets of While procedures with random assignments 435
6 Examples of semicomputable sets of real and complex numbers 438
6.1 Computability on R and C 439
6.2 The algebra of reals; a set which is projectively While 441
semicomputable but not While* semicomputable
6.3 The ordered algebra of reals; sets of reals which are While 443
semicomputable but not While* computable
6.4 A set which is projectively While* semicomputable but not 445
projectively WhileN semicomputable
6.5 Dynamical systems and chaotic systems on R; sets which 447
are WhileN semicomputable but not While* computable
6.6 Dynamical systems and Julia sets on C; sets which are 449
WhileN semicomputable but not While* computable
7 Computation on topological partial algebras 451
7.1 The problem 452
7.2 Partial algebras and While computation 453
7.3 Topological partial algebras 455
7.4 Discussion: Two models of computation on the reals 458
7.5 Continuity of computable functions 460
7.6 Topological characterisation of computable sets in compact 464
algebras
7.7 Metric partial algebra 465
7.8 Connected domains: computability and explicit definability 465
7.9 Approximable computability 470
7.10 Abstract versus concrete models for computing on the real 475
numbers
8 A survey of models of computability 479
8.1 Computability by function schemes 479
8.2 Machine models 484
8.3 High-level programming constructs; program schemes 488
8.4 Axiomatic methods 490
8.5 Equational definability 490
8.6 Inductive definitions and fixed-point methods 492
8.7 Set recursion 493
8.8 A generalised Church-Turing thesis for computability 493
8.9 A Church-Turing thesis for specification 496
8.10 Some other applications 500
Index 525