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 من 52
الصفحة 3
... notion of an algebra of which groups, rings, natural numbers and lists are examples. It is this notion that embodies our so-called algebraic methods. Many computing concepts, not just natural numbers and lists, are instances of algebras ...
... notion of an algebra of which groups, rings, natural numbers and lists are examples. It is this notion that embodies our so-called algebraic methods. Many computing concepts, not just natural numbers and lists, are instances of algebras ...
الصفحة 7
... notion of the set coinductively defined by Φ, namely the greatest fixed point ν Φ of Φ, has been studied intensively and shown to arise in a variety of applications. We discuss the ideas briefly, because inductive and coinductive ...
... notion of the set coinductively defined by Φ, namely the greatest fixed point ν Φ of Φ, has been studied intensively and shown to arise in a variety of applications. We discuss the ideas briefly, because inductive and coinductive ...
الصفحة 8
... notion of a category. We begin with type theory. A crude definition of a type is a set, together with a collection of operations on the set. The key point is that from the programmer's point of view, a type σ should behave as a ...
... notion of a category. We begin with type theory. A crude definition of a type is a set, together with a collection of operations on the set. The key point is that from the programmer's point of view, a type σ should behave as a ...
الصفحة 12
... notion of coalgebraic specification, analogous to that of algebraic specification. The details can be found in Chapter 7. There is also a notion of categorical final coalgebra, which we illustrate by example. Let N∞ be the set N ...
... notion of coalgebraic specification, analogous to that of algebraic specification. The details can be found in Chapter 7. There is also a notion of categorical final coalgebra, which we illustrate by example. Let N∞ be the set N ...
الصفحة 16
... notion of least and greatest fixed point, and these yield initial and final coalgebras. Various examples of (models of) datatypes are given, all expressed as (co)algebras. Equations useful for calculations are derived by using the ...
... notion of least and greatest fixed point, and these yield initial and final coalgebras. Various examples of (models of) datatypes are given, all expressed as (co)algebras. Equations useful for calculations are derived by using the ...
المحتوى
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