دانلود کتاب Computational Category Theory

CONTENTS========1 Introduction1.1 The contents1.2 Accompanying texts1.2.1 Textbooks on category theory1.2.2 ML references and availability1.2.3 A selection of textbooks on functional programming1.3 Acknowledgements2 Functional Programming in ML2.1 Expressions, values and environments2.2 Functions2.2.1 Recursive definitions2.2.2 Higher order functions2.3 Types2.3.1 Primitive types2.3.2 Compound types2.3.3 Type abbreviation2.4 Type polymorphism2.5 Patterns2.6 Defining types2.7 Abstract types2.8 Exceptions2.9 Other facilities2.10 Exercises3 Categories and Functors3.1 Categories3.1.1 Diagram chasing3.1.2 Subcategories, isomorphisms, monics and epis3.2 Examples3.2.1 Sets and finite sets3.2.2 Graphs3.2.3 Finite categories3.2.4 Relations and partial orders3.2.5 Partial orders as categories3.2.6 Deductive systems3.2.7 Universal algebra: terms, algebras and equations3.2.8 Sets with structure and structure-preserving arrows3.3 Categories computationally3.4 Categories as values3.4.1 The category of finite sets3.4.2 Terms and term substitutions: the category T_tau^Fin3.4.3 A finite category3.5 Functors3.5.1 Functors computationally3.5.2 Examples3.6 Duality3.7 An assessment*3.8 Conclusion3.9 Exercises4 Limits and Colimits4.1 Definition by universality4.2 Finite colimits4.2.1 Initial objects4.2.2 Binary coproducts4.2.3 Coequalizers and pushouts4.3 Computing colimits4.4 Graphs, diagrams and colimits4.5 A general construction of colimits4.6 Colimits in the category of finite sets4.7 A calculation of pushouts4.8 Duality and limits4.9 Limits in the category of finite sets4.10 An application: operations on relations4.11 Exercises5 Constructing Categories5.1 Comma categories5.1.1 Representing comma categories5.2 Colimits in comma categories5.3 Calculating colimits of graphs5.4 Functor categories5.4.1 Natural transformations5.4.2 Functor categories5.5 Colimits in functor categories5.6 Duality and limits5.7 Abstract colimits and limits*5.7.1 Abstract diagrams and colimits5.7.2 Category constructions5.7.3 Indexed colimit structures5.7.4 Discussion5.8 Exercises6 Adjunctions6.1 Definitions of adjunctions6.2 Representing adjunctions6.3 Examples6.3.1 Floor and ceiling functions: converting real numbers to integers6.3.2 Components of a graph6.3.3 Free algebras6.3.4 Graph theory6.3.5 Limits and colimits6.3.6 Adjunctions and comma categories6.3.7 Examples from algebra and topology6.4 Computing with adjunctions6.5 Free algebras6.5.1 Constructing free algebras6.5.2 A program6.5.3 An example: transitive closure6.5.4 Other constructions of free algebras6.6 Exercises7 Toposes7.1 Cartesian closed categories7.1.1 An example: the category of finite sets7.2 Toposes7.2.1 An example: the topos of finite sets7.2.2 Computing in a topos7.2.3 Logic in a topos7.2.4 An example: a three-valued logic7.3 Conclusion7.4 Exercises8 A Categorical Unification Algorithm8.1 The unification of terms8.2 Unification as a coequalizer8.3 On constructing coequalizers8.4 A categorical program9 Constructing Theories9.1 Preliminaries9.2 Constructing theories9.3 Theories and institutions9.4 Colimits of theories9.5 Environments9.6 Semantic operations9.7 Implementing a categorical semantics10 Formal Systems for Category Theory10.1 Formal aspects of category theory10.2 Category theory in OBJ10.3 Category theory in a type theory10.4 Categorical data typesA ML KeywordsB Index of ML FunctionsC Other ML FunctionsD Answers to Programming Exercises 231