This handbook with exercises reveals in formalisms, hitherto mainly used for hardware and software design and verification, unexpected mathematical beauty. The lambda calculus forms a prototype universal programming language, which in its untyped version is related to Lisp, and was treated in the first author's classic The Lambda Calculus (1984). The formalism has since been extended with types and used in functional programming (Haskell, Clean) and proof assistants (Coq, Isabelle, HOL), used in designing and verifying IT products and mathematical proofs. In this book, the authors focus on three classes of typing for lambda terms: simple types, recursive types and intersection types. It is in these three formalisms of terms and types that the unexpected mathematical beauty is revealed. The treatment is authoritative and comprehensive, complemented by an exhaustive bibliography, and numerous exercises are provided to deepen the readers' understanding and increase their confidence using types.
Author(s): Henk Barendregt, Wil Dekkers, Richard Statman
Series: Perspectives in Logic
Publisher: Cambridge University Press
Year: 2013
Language: English
Pages: 703
Tags: Математика;Дискретная математика;
Preface......Page 2
Contributors......Page 8
Contents in short......Page 9
Contents......Page 11
Introduction......Page 15
Part 1. Simple Types λ^A_→......Page 21
Untyped lambda calculus......Page 25
Simple types......Page 27
Assigning simple types......Page 28
The minimal and maximal systems λ^0_→ and λ^∞_→......Page 31
Different versions of λ^A_→......Page 33
Properties of λ^Cu_→......Page 36
Properties of λ^Ch_→......Page 38
Properties of λ^dB_→......Page 39
Equivalence of the systems......Page 40
Comparing λ^Cu_→ and λ^Ch_→......Page 41
Comparing λ^Ch_→ and λ^dB_→......Page 44
The three systems compared......Page 45
C. Normal inhabitants......Page 46
Inhabitation machines......Page 48
Booleans......Page 51
Natural numbers......Page 52
Words over a finite alphabet......Page 53
Trees......Page 54
Free algebras with a handicap......Page 55
Finite algebras......Page 57
Pairing......Page 58
E. Exercises......Page 60
A. Normalization......Page 65
Applications of normalization......Page 70
B. Proofs of strong normalization......Page 72
An elementary proof......Page 73
C. Checking and finding types......Page 75
For λ^dB_→ and λ^Ch_→......Page 76
For λ^Cu_→......Page 77
Complexity......Page 81
The Boolean model......Page 82
Intuitionistic propositional logic......Page 84
Kripke models......Page 85
Set-theoretic models......Page 87
E. Exercises......Page 89
Semantics for type assignment a la Church......Page 95
Operations on typed λ-models......Page 101
Semantics for type assignment a la Curry......Page 104
B. Lambda theories and term models......Page 106
Term models......Page 107
Constructing theories......Page 109
Syntactic logical relations......Page 111
Semantic logical relations......Page 118
Relating syntactic and semantic logical relations......Page 123
D. Type reducibility......Page 127
Applications of the reducibility theorem......Page 141
E. The five canonical term models......Page 143
Arbitrary finite sets of constants D......Page 150
Infinite sets of constants......Page 157
Term models......Page 158
Proof of proposition 3D.11......Page 161
F. Exercises......Page 162
The finite standard models......Page 171
B. Undecidability of unification......Page 180
Undecidability of unification......Page 183
C. Decidability of matching of rank 3......Page 185
Relevant solution......Page 186
An example......Page 187
Tree automata for relevant solutions......Page 189
Decidability of rank 3 matching: a particular case......Page 191
Decidability of rank 3 matching: the general case......Page 195
D. Decidability of the maximal theory......Page 197
The non-redundancy of the enumeration......Page 200
E. Exercises......Page 201
A. Lambda delta......Page 205
Higher order logic......Page 206
Logic of order n......Page 213
B. Surjective pairing......Page 214
The system λ_SP......Page 215
Cartesian monoids......Page 217
The free Cartesian monoid F[x_1...x_n]......Page 220
Cartesian monoids inside λ_SP......Page 226
Hilbert-Post completeness of λ_→SP......Page 227
Diophantine relations......Page 229
C. Goedel's system T: higher order primitive recursion......Page 235
Syntax of λ_T......Page 237
Semantics of λ_T......Page 239
Computational strength......Page 240
Syntax of λ_B......Page 249
Semantics of λ_B......Page 254
E. Platek's system Y: fixed point recursion......Page 256
Semantics of λ_Y......Page 257
F. Exercises......Page 258
Computing on data types......Page 265
Development of functional programming......Page 270
Other aspects of functional programming......Page 278
The Curry-de Bruijn-Howard correspondence......Page 279
Illative λ-calculus......Page 286
λ-terms for natural deduction, sequent calculus and cut elimination......Page 287
The logical system N, L and L^cf......Page 288
The type assignment systems λN, λL and λL^cf......Page 291
Relating λN, λL and λL^cf......Page 293
Discussion......Page 295
D. Grammars, terms and types......Page 296
Part 2. Recursive Types λ^A_=......Page 309
Type assignment a la Curry......Page 311
Quotients and syntactic type-algebras and morphisms......Page 313
Constructing type-algebras by equating elements......Page 314
Type assignment in a syntactic algebra......Page 316
Explicitely typed systems......Page 317
Subalgebras, quotients and morphisms......Page 320
Invertible type algebras and prime elements......Page 322
Enriched type algebras......Page 323
Sets of equations over type algebras......Page 324
C. Recursive types via simultaneous recursion......Page 325
Satisfying existential equations......Page 326
Simultaneous recursions......Page 327
Folding and unfolding......Page 330
Justifying sets of equations by an sr......Page 332
D. Recursive types via μ-abstraction......Page 333
Avoiding α-conversion on μ-types......Page 336
Identifying types equal up to renaming......Page 342
E. Recursive types as trees......Page 346
Bisimulation......Page 348
Tree unfolding for invertible general type algebras......Page 349
Tree unfolding for invertible syntactic type algebras......Page 350
Tree equivalence for μ-types......Page 353
Types as regular trees......Page 354
Notations for type assignment systems......Page 355
Trees as metric spaces......Page 356
Trees as coalgebras......Page 358
G. Exercises......Page 361
From sr to μ-types......Page 369
From μ-type to sr......Page 371
B. Properties of μ-types......Page 372
Decidability and axiomatization of strong equivalence......Page 380
Other systems......Page 387
Decidability of weak equivalence for an sr......Page 388
Strong equivalence for an equational theory......Page 391
Axiomatization of strong equivalence for sr......Page 393
Justifying type equations by an sr......Page 394
D. Exercises......Page 400
A. First properties of λ^A_=......Page 403
B. Finding and inhabiting types......Page 405
Principal type scheme in λ^A_=......Page 406
Type reconstruction......Page 409
The typability problem......Page 410
Finding inhabitants......Page 411
Finding μ-types and their inhabitants......Page 412
Strong normalization for μ-types......Page 413
Strong normalization for simultaneous recursion......Page 419
Type inference......Page 420
D. Exercises......Page 421
A. Interpretations of type assignments in λ^A_=......Page 423
Some notions of domain theory......Page 424
Approximating λ-models......Page 427
Complete uniform sets......Page 428
Approximate interpretations of μ-types......Page 431
Soundness and completeness for interpreting T_μ and T*_μ......Page 434
Applications of soundness......Page 436
Completeness......Page 438
C. Type interpretations in systems with explicit typing......Page 439
Domain models......Page 440
D. Exercises......Page 445
A. Subtyping......Page 451
Type structures from type theories......Page 452
Subject reduction......Page 454
Subtyping recursive types......Page 456
Soundness......Page 458
Completeness......Page 459
B. The principal type structure......Page 461
Extending the language......Page 463
Imperative programming......Page 464
Object-oriented programming......Page 465
Type inference and equivalence of recursive types......Page 466
Subtyping......Page 467
E. Exercises......Page 468
Part 3. Intersection Types λ^S_∩......Page 469
12. An Exemplary System......Page 471
A. The type assignment system λ^BCD_∩......Page 472
B. The filter model F^BCD......Page 477
C. Completeness of type assignment......Page 478
13. Type Assignment Systems......Page 481
A. Type theories......Page 483
Some properties about specific TTs......Page 490
Assignment of types from type theories......Page 493
Admissable rules......Page 495
Intersection type structures......Page 496
Categories of meet semi-lattices and type structures......Page 499
D. Filters......Page 500
E. Exercises......Page 501
14. Basic Properties......Page 503
A. Inversion lemmas......Page 505
β-conversion......Page 510
η-conversion......Page 512
C. Exercises......Page 515
15. Type and λ Structures......Page 521
Categories of algebraic lattices......Page 524
Equivalence between MSL^U and ALG_a......Page 528
Equivalence between MSL^-U and ALG^S_a......Page 532
B. Natural type structures and λ structures......Page 533
C. Type and zip structures......Page 538
Equivalences between type and zip structures......Page 539
Equivalences between TS^U and ZS......Page 540
Justifying morphisms in LS......Page 542
Various categories of λ structures......Page 543
Isomorphism between LZS and LLS......Page 544
Equivalences between type and λ structures......Page 547
E. Exercises......Page 549
16. Filter Models......Page 553
A. λ-models......Page 555
Isomorphisms of λ-models......Page 558
B. Filter models......Page 560
Representability of continuous functions......Page 564
The theory ABD......Page 568
D_∞ models......Page 569
D_∞ as a filter λ-model......Page 573
Specific models D_∞ as filter models......Page 578
Other domain equations......Page 581
The λI-calculus......Page 582
A filter model equating an arbitrary closed term to Ω......Page 583
Engeler's model......Page 586
Scott's P(ω) model......Page 587
E. Exercises......Page 588
17. Advanced Properties and Applications......Page 591
A. Realizability interpretation of types......Page 593
Completeness......Page 595
B. Characterizing syntactic properties......Page 597
Stable sets......Page 598
C. Approximation theorems......Page 602
Approximate normal forms......Page 603
Approximation theorem - part 1......Page 605
Approximation theorem - part 2......Page 606
D. Applications of the approximation theorem......Page 614
E. Undecidability of inhabitation......Page 617
Game contexts......Page 619
Tree games......Page 621
Typewriters......Page 627
Remarks......Page 632
Undecidability of inhabitation in λ^CDV_∩ vs. λ-definability in M_X......Page 633
F. Exercises......Page 637
A......Page 643
B......Page 645
C......Page 649
D......Page 652
E......Page 653
FG......Page 654
H......Page 657
IJ......Page 659
K......Page 660
L......Page 662
M......Page 663
N......Page 665
OP......Page 666
R......Page 668
S......Page 669
T......Page 672
UV......Page 673
XZ......Page 674
Indices......Page 677
Index of Definitions......Page 678
Index of Names......Page 689
Index of Symbols......Page 695
