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 من 58
الصفحة 4
... subsets of a set S. If T is the set of all rooted binary trees, we can define a function Φ : P(T) → P(T) which maps a subset S of T to the set consisting of all integers, all variables, and all those finite trees with root + and ...
... subsets of a set S. If T is the set of all rooted binary trees, we can define a function Φ : P(T) → P(T) which maps a subset S of T to the set consisting of all integers, all variables, and all those finite trees with root + and ...
الصفحة 14
... subset order. It is often easier to reason about a lattice when it is presented in such a concrete way, and many examples of program models are based on similar representations [19]. Galois connections are defined, together with some ...
... subset order. It is often easier to reason about a lattice when it is presented in such a concrete way, and many examples of program models are based on similar representations [19]. Galois connections are defined, together with some ...
الصفحة 23
... subsets of some given set X, that is, they are members of the powerset of X. This powerset carries a natural ordering, namely set inclusion, ⊆. We denote the set of all subsets of X by. ℘(X),. and always regard this as equipped with the ...
... subsets of some given set X, that is, they are members of the powerset of X. This powerset carries a natural ordering, namely set inclusion, ⊆. We denote the set of all subsets of X by. ℘(X),. and always regard this as equipped with the ...
الصفحة 24
... subsets of a set X—not necessarily the full powerset—is also ordered by inclusion. For an example, see the diagram in Figure 8(b). Mini-exercise (i) Draw a diagram for the family {{3}, {1,3}, {1, 3, 4}} in 9({1,2,3,4}). (ii) Draw a ...
... subsets of a set X—not necessarily the full powerset—is also ordered by inclusion. For an example, see the diagram in Figure 8(b). Mini-exercise (i) Draw a diagram for the family {{3}, {1,3}, {1, 3, 4}} in 9({1,2,3,4}). (ii) Draw a ...
الصفحة 26
... subsets of G to subsets of M—it takes a set A of objects to the set of attributes common to all the objects in A; likewise, ⊲ maps subsets of M to subsets of G, taking a set of attributes B to the set of all objects which possess all ...
... subsets of G to subsets of M—it takes a set A of objects to the set of attributes common to all the objects in A; likewise, ⊲ maps subsets of M to subsets of G, taking a set of attributes B to the set of all objects which possess all ...
المحتوى
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