- Артикул:00-01092023
- Автор: R. Nederpelt, H. Geuvers
- ISBN: 978-1-107-03650-5
- Обложка: Твердая обложка
- Издательство: Cambridge University Press (все книги издательства)
- Город: Cambridge
- Страниц: 436
- Формат: А4 (210x290 мм)
- Год: 2014
- Вес: 1241 г
Развернуть ▼
Книга на английском языке
Type theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This gentle step-by-step introduction is ideal for graduate students and researchers who need to understand the ins and outs of the mathematical machinery, the role of logical rules therein, the essential contribution of definitions and the decisive nature of well-structured proofs.
The authors begin with untyped lambda calculus and proceed to several fundamental type systems, including the well-known and powerful Calculus of Constructions. The book also covers the essence of proof checking and proof development, and the use of dependent type theory to formalise mathematics.
The only prerequisite is a basic knowledge of undergraduate mathematics. Carefully chosen examples illustrate the theory throughout. Each chapter ends with a summary of the content, some historical context, suggestions for further reading and a selection of exercises to help readers familiarise themselves with the material.
Contents
Foreword, by Henk Barendregt
Preface
Acknowledgements
Greek alphabet
1 Untyped lambda calculus
1.1 Input-output behaviour of functions
1.2 The essence of functions
1.3 Lambda-terms
1.4 Free and bound variables
1.5 Alpha conversion
1.6 Substitution
1.7 Lambda-terms modulo ?-equivalence
1.8 Beta reduction
1.9 Normal forms and confluence
1.10 Fixed Point Theorem
1.11 Conclusions
1.12 Further reading Exercises
2 Simply typed lambda calculus
2.1 Adding types
2.2 Simple types
2.3 Church-typing and Curry-typing
2.4 Derivation rules for Church’s lambda ?
2.5 Different formats for a derivation in lambda ?
2.6 Kinds of problems to be solved in type theory
2.7 Well-typedness in lambda ?
2.8 Type Checking in lambda ?
2.9 Term Finding in lambda ?
2.10 General properties of lambda ?
2.11 Reduction and lambda ?
2.12 Consequences
2.13 Conclusions
2.14 Further reading Exercises
3 Second order typed lambda calculus
3.1 Type-abstraction and type-application
3.2 П-types
3.3 Second order abstraction and application rules
3.4 The system lambda 2
3.5 Example of a derivation in lambda 2
3.6 Properties of lambda 2
3.7 Conclusions
3.8 Further reading Exercises
4 Types dependent on types
4.1 Type constructors
4.2 Sort-rule and var-rule in lambda ?
4.3 The weakening rule in lambda ?
4.4 The formation rule in lambda ?
4.5 Application and abstraction rules in lambda ?
4.6 Shortened derivations
4.7 The conversion rule
4.8 Properties of lambda ?
4.9 Conclusions
4.10 Further reading Exercises
5 Types dependent on terms
5.1 The missing extension
5.2 Derivation rules of lambda P
5.3 An example derivation in lambda P
5.4 Minimal predicate logic in lambda P
5.5 Example of a logical derivation in lambda P
5.6 Conclusions
5.7 Further reading Exercises
6 The Calculus of Constructions
6.1 The system lambda C
6.2 The A-cube
6.3 Properties of lambda C
6.4 Conclusions
6.5 Further reading Exercises
7 The encoding of logical notions in lambda C
7.1 Absurdity and negation in type theory
7.2 Conjunction and disjunction in type theory
7.3 An example of propositional logic in lambda C
7.4 Classical logic in lambda C
7.5 Predicate logic in lambda C
7.6 An example of predicate logic in lambda C
7.7 Conclusions
7.8 Further reading Exercises
8 Definitions
8.1 The nature of definitions
8.2 Inductive and recursive definitions
8.3 The format of definitions
8.4 Instantiations of definitions
8.5 A formal format for definitions
8.6 Definitions depending on assumptions
8.7 Giving names to proofs
8.8 A general proof and a specialised version
8.9 Mathematical statements as formal definitions
8.10 Conclusions
8.11 Further reading Exercises
9 Extension of lambda C with definitions
9.1 Extension of lambda C to the system lambda D0
9.2 Judgements extended with definitions
9.3 The rule for adding a definition
9.4 The rule for instantiating a definition
9.5 Definition unfolding and ?-conversion
9.6 Examples of ?-conversion
9.7 The conversion rule extended with lambda D0
9.8 The derivation rules for lambda D0
9.9 A closer look at the derivation rules of lambda D0
9.10 Conclusions
9.11 Further reading Exercises
10 Rules and properties of lambda D
10.1 Descriptive versus primitive definitions
10.2 Axioms and axiomatic notions
10.3 Rules for primitive definitions
10.4 Properties of lambda D
10.5 Normalisation and confluence in lambda D
10.6 Conclusions
10.7 Further reading Exercises
11 Flag-style natural deduction in lambda D
11.1 Formal derivations in lambda D
11.2 Comparing formal and flag-style lambda D
11.3 Conventions about flag-style proofs in lambda D
11.4 Introduction and elimination rules
11.5 Rules for constructive propositional logic
11.6 Examples of logical derivations in lambda D
11.7 Suppressing unaltered parameter lists
11.8 Rules for classical propositional logic
11.9 Alternative natural deduction rules for V
11.10 Rules for constructive predicate logic
11.11 Rules for classical predicate logic
11.12 Conclusions
11.13 Further reading Exercises
12 Mathematics in lambda D: a first attempt
12.1 An example to start with
12.2 Equality
12.3 The congruence property of equality
12.4 Orders
12.5 A proof about orders
12.6 Unique existence
12.7 The descriptor l
12.8 Conclusions
12.9 Further reading Exercises
13 Sets and subsets
13.1 Dealing with subsets in AD
13.2 Basic set-theoretic notions
13.3 Special subsets
13.4 Relations
13.5 Maps
13.6 Representation of mathematical notions
13.7 Conclusions
13.8 Further reading Exercises
14 Numbers and arithmetic in AD
14.1 The Peano axioms for natural numbers
14.2 Introducing integers the axiomatic way
14.3 Basic properties of the ‘new‘ N
14.4 Integer addition
14.5 An example of a basic computation in AD
14.6 Arithmetical laws for addition
14.7 Closure under addition for natural and negative numbers
14.8 Integer subtraction
14.9 The opposite of an integer
14.10 Inequality relations on Z
14.11 Multiplication of integers
14.12 Divisibility
14.13 Irrelevance of proof
14.14 Conclusions
14.15 Further reading Exercises
15 An elaborated example
15.1 Formalising a proof of Bezout’s Lemma
15.2 Preparatory work
15.3 Part I of the proof of Bezout’s Lemma
15.4 Part II of the proof
15.5 Part III of the proof
15.6 The holes in the proof of Bezout’s Lemma
15.7 The Minimum Theorem for Z
15.8 The Division Theorem
15.9 Conclusions
15.10 Further reading Exercises
16 Further perspectives
16.1 Useful applications of AD
16.2 Proof assistants based on type theory
16.3 Future of the field
16.4 Conclusions
16.5 Further reading
Appendix A Logic in lambda D
A.l Constructive propositional logic
A.2 Classical propositional logic
A.3 Constructive predicate logic
A.4 Classical predicate logic
Appendix В Arithmetical axioms, definitions and lemmas
Appendix C Two complete example proofs in lambda D
C.l Closure under addition in N
C.2 The Minimum Theorem
Appendix D Derivation rules for AD
References
Index of name
Index of definitions
Index of symbols
Index of subjects
Рекомендуем
