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 من 82
الصفحة x
... Pair Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 4.1. Infima and Suprema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
... Pair Algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 4.1. Infima and Suprema . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
الصفحة xi
... Pair Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 1.6. Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
... Pair Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 1.6. Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
الصفحة 9
... pair (A, B) into A × B is part of the definition of a functor. These ideas are exploited in Chapter 5. 2.4 Algebras and Coalgebras We often find type definitions in programming languages similar to the following example nats = Zero ...
... pair (A, B) into A × B is part of the definition of a functor. These ideas are exploited in Chapter 5. 2.4 Algebras and Coalgebras We often find type definitions in programming languages similar to the following example nats = Zero ...
الصفحة 12
... x) Our “system” is a computer which can run the program above. The system state at any given time is the pair (n, x) or HALT. If p is any positive integer, given a starting state of (p, p) then the system will halt, 12 Roy Crole.
... x) Our “system” is a computer which can run the program above. The system state at any given time is the pair (n, x) or HALT. If p is any positive integer, given a starting state of (p, p) then the system will halt, 12 Roy Crole.
الصفحة 27
... pair of polar maps, forming what is known as a Galois connection. In a way we have yet fully to explore, these maps in turn give rise to an ordered set of objects we call concepts, and this encodes the original binary relation. But we ...
... pair of polar maps, forming what is known as a Galois connection. In a way we have yet fully to explore, these maps in turn give rise to an ordered set of objects we call concepts, and this encodes the original binary relation. But we ...
المحتوى
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