CONTENTS
========
1 Introduction
1.1 The contents
1.2 Accompanying texts
1.2.1 Textbooks on category theory
1.2.2 ML references and availability
1.2.3 A selection of textbooks on functional programming
1.3 Acknowledgements
2 Functional Programming in ML
2.1 Expressions, values and environments
2.2 Functions
2.2.1 Recursive definitions
2.2.2 Higher order functions
2.3 Types
2.3.1 Primitive types
2.3.2 Compound types
2.3.3 Type abbreviation
2.4 Type polymorphism
2.5 Patterns
2.6 Defining types
2.7 Abstract types
2.8 Exceptions
2.9 Other facilities
2.10 Exercises
3 Categories and Functors
3.1 Categories
3.1.1 Diagram chasing
3.1.2 Subcategories, isomorphisms, monics and epis
3.2 Examples
3.2.1 Sets and finite sets
3.2.2 Graphs
3.2.3 Finite categories
3.2.4 Relations and partial orders
3.2.5 Partial orders as categories
3.2.6 Deductive systems
3.2.7 Universal algebra: terms, algebras and equations
3.2.8 Sets with structure and structure-preserving arrows
3.3 Categories computationally
3.4 Categories as values
3.4.1 The category of finite sets
3.4.2 Terms and term substitutions: the category T_tau^Fin
3.4.3 A finite category
3.5 Functors
3.5.1 Functors computationally
3.5.2 Examples
3.6 Duality
3.7 An assessment*
3.8 Conclusion
3.9 Exercises
4 Limits and Colimits
4.1 Definition by universality
4.2 Finite colimits
4.2.1 Initial objects
4.2.2 Binary coproducts
4.2.3 Coequalizers and pushouts
4.3 Computing colimits
4.4 Graphs, diagrams and colimits
4.5 A general construction of colimits
4.6 Colimits in the category of finite sets
4.7 A calculation of pushouts
4.8 Duality and limits
4.9 Limits in the category of finite sets
4.10 An application: operations on relations
4.11 Exercises
5 Constructing Categories
5.1 Comma categories
5.1.1 Representing comma categories
5.2 Colimits in comma categories
5.3 Calculating colimits of graphs
5.4 Functor categories
5.4.1 Natural transformations
5.4.2 Functor categories
5.5 Colimits in functor categories
5.6 Duality and limits
5.7 Abstract colimits and limits*
5.7.1 Abstract diagrams and colimits
5.7.2 Category constructions
5.7.3 Indexed colimit structures
5.7.4 Discussion
5.8 Exercises
6 Adjunctions
6.1 Definitions of adjunctions
6.2 Representing adjunctions
6.3 Examples
6.3.1 Floor and ceiling functions: converting real numbers to integers
6.3.2 Components of a graph
6.3.3 Free algebras
6.3.4 Graph theory
6.3.5 Limits and colimits
6.3.6 Adjunctions and comma categories
6.3.7 Examples from algebra and topology
6.4 Computing with adjunctions
6.5 Free algebras
6.5.1 Constructing free algebras
6.5.2 A program
6.5.3 An example: transitive closure
6.5.4 Other constructions of free algebras
6.6 Exercises
7 Toposes
7.1 Cartesian closed categories
7.1.1 An example: the category of finite sets
7.2 Toposes
7.2.1 An example: the topos of finite sets
7.2.2 Computing in a topos
7.2.3 Logic in a topos
7.2.4 An example: a three-valued logic
7.3 Conclusion
7.4 Exercises
8 A Categorical Unification Algorithm
8.1 The unification of terms
8.2 Unification as a coequalizer
8.3 On constructing coequalizers
8.4 A categorical program
9 Constructing Theories
9.1 Preliminaries
9.2 Constructing theories
9.3 Theories and institutions
9.4 Colimits of theories
9.5 Environments
9.6 Semantic operations
9.7 Implementing a categorical semantics
10 Formal Systems for Category Theory
10.1 Formal aspects of category theory
10.2 Category theory in OBJ
10.3 Category theory in a type theory
10.4 Categorical data types
A ML Keywords
B Index of ML Functions
C Other ML Functions
D Answers to Programming Exercises 231
Author(s): D.E. Rydeheard, R.M. Burstall
Series: Prentice-Hall International Series in Computer Science
Edition: 1
Publisher: Prentice-Hall
Year: 1988
Language: English
Commentary: Vector PDF, 3-level bookmarks, pagination
Pages: 268
Front Cover......Page 1
Contents......Page 7
Foreword......Page 11
Preface......Page 15
1 Introduction......Page 17
1.1 The contents......Page 20
1.2.1 Textbooks on category theory......Page 22
1.2.3 A selection of textbooks on functional programming......Page 23
1.3 Acknowledgements......Page 24
2 Functional Programming in ML......Page 25
2.1 Expressions, values and environments......Page 27
2.2 Functions......Page 29
2.2.2 Higher order functions......Page 30
2.3 Types......Page 31
2.3.2 Compound types......Page 32
2.4 Type polymorphism......Page 33
2.5 Patterns......Page 36
2.6 Defining types......Page 37
2.7 Abstract types......Page 40
2.8 Exceptions......Page 42
2.10 Exercises......Page 43
3.1 Categories......Page 51
3.1.1 Diagram chasing......Page 54
3.1.2 Subcategories, isomorphisms, monics and epis......Page 55
3.2.2 Graphs......Page 56
3.2.4 Relations and partial orders......Page 57
3.2.6 Deductive systems......Page 58
3.2.7 Universal algebra: terms, algebras and equations......Page 59
3.2.8 Sets with structure and structure-preserving arrows......Page 62
3.3 Categories computationally......Page 63
3.4.1 The category of finite sets......Page 65
3.4.2 Terms and term substitutions: the category T_tau^Fin......Page 66
3.4.3 A finite category......Page 68
3.5 Functors......Page 69
3.5.2 Examples......Page 70
3.6 Duality......Page 71
3.7 An assessment......Page 73
3.9 Exercises......Page 76
4 Limits and Colimits......Page 81
4.1 Definition by universality......Page 83
4.2 Finite colimits......Page 84
4.2.1 Initial objects......Page 85
4.2.2 Binary coproducts......Page 86
4.2.3 Coequalizers and pushouts......Page 88
4.3 Computing colimits......Page 90
4.4 Graphs, diagrams and colimits......Page 95
4.5 A general construction of colimits......Page 98
4.6 Colimits in the category of finite sets......Page 104
4.7 A calculation of pushouts......Page 106
4.8 Duality and limits......Page 109
4.9 Limits in the category of finite sets......Page 111
4.10 An application: operations on relations......Page 113
4.11 Exercises......Page 116
5 Constructing Categories......Page 119
5.1 Comma categories......Page 120
5.1.1 Representing comma categories......Page 121
5.2 Colimits in comma categories......Page 123
5.3 Calculating colimits of graphs......Page 125
5.4.1 Natural transformations......Page 129
5.4.2 Functor categories......Page 130
5.5 Colimits in functor categories......Page 132
5.6 Duality and limits......Page 134
5.7 Abstract colimits and limits......Page 136
5.7.1 Abstract diagrams and colimits......Page 137
5.7.2 Category constructions......Page 138
5.7.4 Discussion......Page 139
5.8 Exercises......Page 140
6 Adjunctions......Page 143
6.1 Definitions of adjunctions......Page 144
6.2 Representing adjunctions......Page 146
6.3 Examples......Page 147
6.3.2 Components of a graph......Page 148
6.3.3 Free algebras......Page 150
6.3.4 Graph theory......Page 152
6.3.6 Adjunctions and comma categories......Page 154
6.3.7 Examples from algebra and topology......Page 155
6.4 Computing with adjunctions......Page 156
6.5 Free algebras......Page 158
6.5.1 Constructing free algebras......Page 159
6.5.2 A program......Page 160
6.5.3 An example: transitive closure......Page 162
6.5.4 Other constructions of free algebras......Page 165
6.6 Exercises......Page 168
7 Toposes......Page 171
7.1 Cartesian closed categories......Page 172
7.1.1 An example: the category of finite sets......Page 173
7.2 Toposes......Page 175
7.2.1 An example: the topos of finite sets......Page 177
7.2.2 Computing in a topos......Page 178
7.2.3 Logic in a topos......Page 180
7.2.4 An example: a three-valued logic......Page 182
7.3 Conclusion......Page 186
7.4 Exercises......Page 187
8 A Categorical Unification Algorithm......Page 189
8.1 The unification of terms......Page 190
8.2 Unification as a coequalizer......Page 191
8.3 On constructing coequalizers......Page 192
8.4 A categorical program......Page 196
9 Constructing Theories......Page 203
9.1 Preliminaries......Page 204
9.2 Constructing theories......Page 206
9.3 Theories and institutions......Page 210
9.4 Colimits of theories......Page 213
9.5 Environments......Page 215
9.6 Semantic operations......Page 216
9.7 Implementing a categorical semantics......Page 217
10 Formal Systems for Category Theory......Page 219
10.1 Formal aspects of category theory......Page 220
10.2 Category theory in OBJ......Page 223
10.3 Category theory in a type theory......Page 232
10.4 Categorical data types......Page 234
A ML Keywords......Page 239
B Index of ML Functions......Page 241
C Other ML Functions......Page 245
D Answers to Programming Exercises......Page 247
Back Cover......Page 268
