Algebraic and Coalgebraic Methods in the Mathematics of Program Construction: International Summer School and Workshop, Oxford, UK, April 10-14, 2000, Revised LecturesRoland Backhouse, Roy Crole, Jeremy Gibbons Springer, 31/07/2003 - 390 من الصفحات Program construction is about turning specifications of computer software into implementations. Recent research aimed at improving the process of program construction exploits insights from abstract algebraic tools such as lattice theory, fixpoint calculus, universal algebra, category theory, and allegory theory. This textbook-like tutorial presents, besides an introduction, eight coherently written chapters by leading authorities on ordered sets and complete lattices, algebras and coalgebras, Galois connections and fixed point calculus, calculating functional programs, algebra of program termination, exercises in coalgebraic specification, algebraic methods for optimization problems, and temporal algebra. |
من داخل الكتاب
النتائج 1-5 من 51
الصفحة xi
... Functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198 5.4. Datatypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
... Functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198 5.4. Datatypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
الصفحة 9
... functor. The key point is that if f : X → Y, then [f] : [X] → [Y]—the image of the morphism f under the functor is a morphism between the images of the source and target of f. Some other conditions must be satisfied: the morphism ...
... functor. The key point is that if f : X → Y, then [f] : [X] → [Y]—the image of the morphism f under the functor is a morphism between the images of the source and target of f. Some other conditions must be satisfied: the morphism ...
الصفحة 10
... functor from the category X to itself. Moreover, the least prefixed point has a special property, namely, given any ... functors. 10 Roy Crole.
... functor from the category X to itself. Moreover, the least prefixed point has a special property, namely, given any ... functors. 10 Roy Crole.
الصفحة 11
... functors. They are useful because many datatypes of interest in computing have models which arise as initial algebras. An example is the set of natural numbers. Let 1 = {∗} be a singleton set, and + denote disjoint union of sets. Then ...
... functors. They are useful because many datatypes of interest in computing have models which arise as initial algebras. An example is the set of natural numbers. Let 1 = {∗} be a singleton set, and + denote disjoint union of sets. Then ...
الصفحة 13
... functors; fixed points of monotone functions are simple examples. 3. Mathematics. in. ACMMPC. In this section we give a sketch of the contents of each chapter, and in particular we indicate where the underpinning mathematics described in ...
... functors; fixed points of monotone functions are simple examples. 3. Mathematics. in. ACMMPC. In this section we give a sketch of the contents of each chapter, and in particular we indicate where the underpinning mathematics described in ...
المحتوى
1 | |
13 | |
21 | |
28 | |
Lattices in General and Complete Lattices in Particular | 39 |
Closure Systems and Closure Operators | 47 |
Speaking Categorically | 75 |
Trees | 84 |
EverMind Westerkade 154 9718 AS Groningen | 202 |
Hylo Equations | 218 |
Department of Computer Science University of Nijmegen | 237 |
Binary Trees | 244 |
Invariants | 253 |
Towards a μCalculus for Coalgebras | 261 |
Refinements between Coalgebraic Specifications | 275 |
Algebraic Methods for Optimization Problems | 281 |
Identifying Galois Connections | 100 |
Fixed Points | 115 |
Fixed Point Calculus | 127 |
Further Reading | 146 |
Calculating Functional Programs | 149 |
Recursive Datatypes in the Category Set | 160 |
Recursive Datatypes in the Category Cpo | 173 |
Applications | 183 |
Implementation in Haskell | 197 |
The Algebra of Relations | 283 |
Optimization Problems | 291 |
Optimal Bracketing | 299 |
Temporal Algebra | 309 |
Relational Laws of Sequential Algebra | 355 |
Interval Calculi | 364 |
Conclusion | 382 |
طبعات أخرى - عرض جميع المقتطفات
عبارات ومصطلحات مألوفة
admits induction Algebraic and Coalgebraic algorithm apply arbitrary arrows axioms binary relation binary trees category theory Chapter closure operator coalgebraic specification coalgebras complete lattice composition Computer Science concat cons constructors coreflexive datatype defined definition denote domain down-sets dual element equivalent example Exercise exists expressions F-algebra finite fixed point equation fold foldL foldT f function f functional programming functor fusion Galois algebra Galois connection given hylo initial algebra integers IntList isomorphism Kleene algebra least fixed point least prefix point Lemma linear List lower adjoint map f mathematical Mini-exercise monotonic natural numbers node non-empty notion ordered sets pair partial order point of f poset powerset predicate Prod programming languages proof Proposition Prove recursion relation algebra rule satisfies semantics solution structure subset supremum tail temporal logic theorem tion unfold unique universal property upper adjoint well-founded