Foundations for programming languages / John C. Mitchell.

CONTENIDO
1. Introduction 1
Model Programming Languages 1
Lambda Notation 3
Equations, Reduction, and Semantics 5
Axiomatic Semantics 6
Operational Semantics 7
Denotational Semantics 8
Types and Type Systems 9
Notation and Mathematical Conventions 11
Set-theoretic Background 13
Fundamentals 13
Relations and Functions 17
Syntax and Semantics 21
Object Language and Meta-language 21
Grammars 21
Lexical Analysis and Parsing 23
Example Mathematical Interpretation 25
Induction 27
Induction on the Natural Numbers 27
Induction on Expressions and Proofs 32
Well-founded Induction 38
2. The Language PCF 45
Introduction 45
Syntax of PCF 46
Overview 46
Booleans and Natural Numbers 47
Pairing and Functions 51
Declarations and Syntactic Sugar 57
Recursion and Fixed-point Operators 60
PCF Syntax Summary and Collected Examples 65
PCF Programs and Their Semantics 67
Programs and Results 67
Axiomatic Semantics 69
Denotational Semantics 73
Operational Semantics 75
Equivalence Relations Defined by Each Form of Semantics 76
PCF Reduction and Symbolic Interpreters 79
Nondeterministic Reduction 79
Reduction Strategies 84
The Left-most and Lazy Reduction Strategies 86
Parallel Reduction 91
Eager PCF 92
PCF Programming Examples, Expressive Power and Limitations 96
Records and n-tuples 96
Searching the Natural Numbers 98
Iteration and Tail Recursion 101
Total Recursive Functions 105
Partial Recursive Functions 109
Nondefinability of Parallel Operations 113
Variations and Extensions of PCF 122
Summary of Extensions 122
Unit and Sum Types 122
Recursive Types 126
Lifted Types 132
3. Universal Algebra and Algebraic Data Types 145
Introduction 145
Preview of Algebraic Specification 146
Algebras, Signatures and Terms 148
Algebras 148
Syntax of Algebraic Terms 149
Algebras and the Interpretation of Terms 151
The Substitution Lemma 156
Equations, Soundness and Completeness 157
Equations 157
Term Algebras and Substitution 159
Semantic Implication and an Equational Proof System 161
Forms of Completeness 171
Congruence, Quotients and Deductive Completeness 173
Nonempty Sorts and the Least Model Property 177
Homomorphisms and Initiality 179
Homomorphisms and Isomorphisms 179
Initial Algebras 181
Algebraic Data Types 188
Specification and Data Abstraction 188
Initial Algebra Semantics and Datatype Induction 191
Examples and Error Values 196
Alternative Approaches to Error Values 202
Rewrite Systems 203
Basic Definitions 203
Confluence and Provable Equality 207
Termination 210
Critical Pairs 216
Left-linear Non-overlapping Rewrite Systems 222
Local Confluence, Termination and Completion 227
Applications to Algebraic Datatypes 230
4. Simply-typed Lambda Calculus 235
Introduction 235
Types 237
Syntax 237
Interpretation of Types 237
Terms 239
Context-sensitive Syntax 239
Syntax of Terms 241
Terms with Product, Sum and Related Types 248
Formulas-as-types Correspondence 250
Typing Algorithm 257
Proof Systems 257
Equations and Theories 257
Reduction Rules 267
Reduction with Additional Rules 271
Proof-theoretic Methods for Consistency and Conservativity 273
Henkin Models, Soundness and Completeness 279
General Models and the Meanings of Terms 279
Applicative Structures, Extensionality and Frames 280
Environment Model Condition 283
Type and Equational Soundness 288
Completeness for Henkin Models Without Empty Types 293
Completeness with Empty Types 295
Combinators and the Combinatory Model Condition 297
Combinatory and Lambda Algebras 300
Henkin Models for Other Types 301
5. Models of Typed Lambda Calculus 305
Introduction 305
Domain-theoretic Models and Fixed Points 306
Recursive Definitions and Fixed Point Operators 306
Complete Partial Orders, Lifting and Cartesian Products 308
Continuous Functions 312
Fixed Points and the Full Continuous Hierarchy 318
CPO Model for PCF 327
Fixed-point Induction 333
Computational Adequacy and Full Abstraction 339
Approximation Theorem and Computational Adequacy 339
Full Abstraction for PCF with Parallel Operations 345
Recursion-theoretic Models 354
Introduction 354
Modest Sets 357
Full Recursive Hierarchy 360
Partial Equivalence Relations and Recursion 364
Partial Equivalence Relation Interpretation of Types 364
Generalization to Partial Combinatory Algebras 368
Lifting, Partial Functions and Recursion 373
Recursion and the Intrinsic Order 375
Lifting, Products and Function Spaces of Effective CPOs 382
6. Imperative Programs 387
Introduction 387
While Programs 389
L--values and R--values 389
Syntax of While Programs 390
Operational Semantics 392
Basic Symbols in Expressions 392
Locations and Stores 392
Evaluation of Expressions 394
Execution of Commands 395
Denotational Semantics 401
Typed Lambda Calculus with Stores 401
Semantic Functions 405
Equivalence of Operational and Denotational Semantics 410
Before-after Assertions about While Programs 412
First-order and Partial Correctness Assertions 412
Proof Rules 415
Soundness 421
Relative Completeness 423
Semantics of Additional Program Constructs 429
Overview 429
Blocks with Local Variables 429
Procedures 438
Combining Blocks and Procedure Declarations 440
7. Categories and Recursive Types 445
Introduction 445
Cartesian Closed Categories 446
Category Theory and Typed Languages 446
Categories, Functors and Natural Transformations 446
Definition of Cartesian Closed Category 458
Soundness and the Interpretation of Terms 468
Henkin Models as CCCs 484
Categorical Characterization of Meaning Function 487
Kripke Lambda Models and Functor Categories 490
Overview 490
Possible Worlds 491
Applicative Structures 491
Extensionality, Combinators and Functor Categories 493
Environments and Meanings of Terms 497
Soundness and Completeness 499
Kripke Lambda Models as Cartesian Closed Categories 501
Domain Models of Recursive Types 505
A Motivating Example 505
Diagrams, Cones and Limits 509
F-algebras 512
Omega-Chains and Initial F-algebras 514
O-categories and Embeddings 518
Colimits and O-colimits 521
Locally Continuous Functors 526
Examples of the General Method 528
8. Logical Relations 535
Introduction to Logical Relations 535
Logical Relations over Applicative Structures 536
Definition of Logical Relation 536
The Basic Lemma 538
Partial Functions and Theories of Models 544
Logical Partial Equivalence Relations 545
Quotients and Extensionality 546
Proof-Theoretic Results 550
Completeness for Henkin Models 550
Normalization 553
Confluence and Other Reduction Properties 556
Reduction with Fix and Additional Operations 562
Partial Surjections and Specific Models 573
Partial Surjections and the Full Classical Hierarchy 574
Full Recursive Hierarchy 576
Full Continuous Hierarchy 578
Representation Independence 580
Motivation 580
Example Language 581
General Representation Independence 585
Generalizations of Logical Relations 586
Introduction 586
Motivating Examples: Complete Partial Orders and Kripke Models 588
Sconing and Relations 595
Comparison with Logical Relations 600
General Case and Applications to Specific Categories 603
9. Polymorphism and Modularity 607
Introduction 607
Overview 607
Types as Function Arguments 608
General Products and Sums 613
Types as Specifications 614
Predicative Polymorphic Calculus 617
Syntax of Types and Terms 617
Comparison with Other Forms of Polymorphism 624
Equational Proof System and Reduction 628
Models of Predicative Polymorphism 630
ML-Style Polymorphic Declarations 635
Impredicative Polymorphism 639
Introduction 639
Expressiveness and Properties of Theories 640
Termination of Reduction 657
Summary of Semantic Models 663
Models Based on Universal Domains 665
Partial Equivalence Relation Models 670
Data Abstraction and Existential Types 679
General Products, Sums and Program Modules 685
The ML Module Language 685
Predicative Calculus with Products and Sums 692
Representing Modules with Products and Sums 697
Predicativity and the Relationship between Universes 698
10. Subtyping and Related Concepts 703
Introduction 703
Simply Typed Lambda Calculus with Subtyping 706
Records 713
General Properties of Record Subtyping 713
Typed Calculus with Records and Subtyping 714
Semantic Models of Subtyping 718
Overview 718
Conversion Interpretation of Subtyping 718
Subset Interpretation of Types 727
Partial Equivalence Relations as Types 734
Recursive Types and a Record Model of Objects 739
Polymorphism with Subtype Constraints 750
11. Type Inference 765
Introduction to Type Inference 765
Type Inference for with Type Variables 769
The Language 769
Substitution, Instances and Unification 771
An Algorithm for Principal Curry Typings 777
Implicit Typing 782
Equivalence of Typing and Unification 784
Type Inference with Polymorphic Declarations 790
ML Type Inference and Polymorphic Variables 790
Two Sets of Implicit Typing Rules 791
Type Inference Algorithms 795
Equivalence of ML1 and ML2 802
Complexity of ML Type Inference 805
Bibliography 817
Index 837