Algebraic and Coalgebraic Methods in the Mathematics of Program Construction

International Summer School and Workshop, Oxford, UK, April 10-14, 2000, Revised Lectures

By: Roland Backhouse (Editor), Roy Crole (Editor), Jeremy Gibbons (Editor)

Write A Review

Paperback | 17 April 2002

At a Glance

Paperback
408 Pages

Dimensions(cm)
22.86 x 15.24 x 2.54

Paperback

$84.99

or 4 interest-free payments of $21.25 with

Ships in 5 to 7 business days

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.

Shipping

	Standard Shipping	Express Shipping
Metro postcodes:	$9.99	$14.95
Regional postcodes:	$9.99	$14.95
Rural postcodes:	$9.99	$14.95

Orders over $79.00 qualify for free shipping.

How to return your order

At Booktopia, we offer hassle-free returns in accordance with our returns policy. If you wish to return an item, please get in touch with Booktopia Customer Care.

Additional postage charges may be applicable.

Defective items

If there is a problem with any of the items received for your order then the Booktopia Customer Care team is ready to assist you.

For more info please visit our Help Centre.

You Can Find This Book In

Non-Fiction Mathematics Algebra Discrete Mathematics Computing & I.T.Computer Programming & Software Development Programming & Scripting Languages Medicine Medicine in General Software Engineering Computer Science Mathematical Theory of Computation

Mathematical Foundation Mathematical Logic Computer Architecture & Logic Design

Introduction	p. 1
Preliminaries	p. 1
Assumed Knowledge	p. 1
Volume Overview	p. 2
A Mathematical History Tour	p. 3
Fixed Points	p. 3
Induction and Coinduction	p. 7
Types and Categories	p. 8
Algebras and Coalgebras	p. 9
Mathematics in ACMMPC	p. 13
Chapter 2: Ordered Sets and Complete Lattices	p. 14
Chapter 3: Introducing Algebras and Coalgebras	p. 14
Chapter 4: Galois Connections and Fixed Point Calculus	p. 15
Chapter 5: Calculating Functional Programs	p. 15
Chapter 6: Algebra of Program Termination	p. 16
Chapter 7: Exercises in Coalgebraic Specification	p. 17
Chapter 8: Algebraic Methods for Optimization Problems	p. 17
Chapter 9: Temporal Algebra	p. 18
Ordered Sets and Complete Lattices	p. 21
Introduction	p. 21
From Binary Relations to Diagrams	p. 23
A Fundamental Example: Powersets	p. 23
Input-Output Relations Pictorially	p. 24
Exercise	p. 25
Binary Relations and Their Polars	p. 26
Exercise	p. 27
Summing Up So Far	p. 27
Order, Order, Order	p. 28
Partial Order	p. 28
Information Orderings	p. 29
Diagrams	p. 30
Duality: Buy One, Get One Free	p. 31
Bottom and Top	p. 31
Lifting	p. 32
New Posets from Old: Sums and Products	p. 32
Maps between Posets	p. 33
Pointwise Ordering of Maps	p. 34
Up-Sets: An Inbred Example	p. 35
Monotone Maps and Up-Sets	p. 35
Exercise (More on Monotone Maps and Up-Sets)	p. 36
Down Is Nice Too	p. 36
Exercise (Turning Things Upside Down)	p. 36
The Down-Set Operator, ↓, and the Up-Set Operator, ↑	p. 37
Exercise (A Context Explored)	p. 38
Maximal and Minimal Elements	p. 38
Stocktaking	p. 38
Lattices in General and Complete Lattices in Particular	p. 39
Lattices	p. 39
Examples of Lattices	p. 41
Distributive Lattices	p. 41
Boolean Algebras	p. 42
Lattices in Logic	p. 42
Upper Bounds and Sups, Lower Bounds and Infs	p. 43
Much Ado about Nothing, and about Everything	p. 44
Complete Lattices	p. 45
Completeness on the Cheap	p. 45
A Special Class of Complete Lattices	p. 45
Suprema, Infima, and Monotone Maps	p. 46
Complete Lattices, Concretely: Closure Systems and Closure Operators	p. 47
A Useful Technical Remark	p. 47
Complete Lattices of Sets	p. 47
Closure Systems	p. 47
Closure Systems	p. 48
Examples	p. 49
From a Complete Lattice to a Closure System	p. 49
Defining Closure Operators	p. 49
New Complete Lattices from Old: From a Closure Operator to a Complete Lattice	p. 50
Closure Operators more Concretely	p. 51
Galois Connections: Basics	p. 51
Introduction	p. 51
Lattice Representation via Galois Connections	p. 52
Galois Connections from Binary Relations: Method I	p. 53
Galois Connections and Algebras-A Fleeting Glimpse	p. 54
Galois Connections by Sectioning	p. 54
Galois Connections from Binary Relations: Method II	p. 55
Galois Connections: Basic Properties	p. 55
<$>{}^\triangleright<$> and <$>{}^\triangleleft<$> Have Isomorphic Images	p. 56
Equivalent Definitions for Galois Connections	p. 57
The Good (and Less Good) Behaviour of Galois Maps	p. 58
Uniqueness of Adjoints: <$>{}^\triangleright<$> from <$>{}^\triangleleft<$> and <$>{}^\triangleleft<$> from <$>{}^\triangleright<$>	p. 59
Exercise (Surjective and Injective Galois Maps)	p. 60
A Look Ahead	p. 60
Existence of Adjoints: A Technical Lemma	p. 61
Existence Theorem for Adjoints	p. 61
Postscript	p. 62
Making Connections, Conceptually	p. 62
From a Galois Connection to a Closure Operator	p. 62
From a Closure Operator to a Galois Connection	p. 63
Contexts and Concepts: Re-setting the Scene	p. 63
Ordering Concepts	p. 63
Three for the Price of One: A Trinity of Complete Lattices	p. 64
Manufacturing Concepts	p. 65
Density: Generating all Concepts via ¿ or ¿	p. 65
From a Complete Lattice to a Concept Lattice	p. 66
The Case for the Defence	p. 66
Summing Up	p. 67
The Existence of Fixed Points	p. 67
Fixed Points and Least Fixed Points: Definitions	p. 68
Characterizing Least Fixed Points via Least Prefix Points	p. 68
The Knaster-Tarski Fixed Point Theorem	p. 69
Exercise	p. 69
Exercise	p. 69
From Complete Lattices to CPOs	p. 69
A Sense of Direction	p. 70
Exercise (Sups and Directed Sups Related)	p. 70
CPOs	p. 71
Directed Sets and Continuity	p. 71
New CPOs from Old	p. 72
Fixed Point Theorem for a Continuous Function on a CPO	p. 72
From Continuity to Monotonicity	p. 72
An Assumption: Zorn's Lemma (ZL), CPO Form	p. 73
The Fixed Point Theorem for a Monotone Endofunction on a CPO	p. 73
Exercise	p. 74
Exercise	p. 74
Concluding Remarks	p. 74
Speaking Categorically	p. 75
Categories	p. 75
Algebras and Coalgebras	p. 79
Introduction	p. 79
Terms	p. 80
Variable-Free Terms	p. 80
Terms as Set Theoretical Objects	p. 81
Terms with Variables	p. 82
Initial (F,X)-Algebras	p. 83
Substitution	p. 83
Trees	p. 84
Variable-Free Trees	p. 84
Representing Terms as Well-Founded Trees	p. 84
Corecursion	p. 85
Set Theoretical Representation of Trees	p. 85
Trees with Variables	p. 87
Substitution	p. 87
Solution Property	p. 87
The Monad of a Substitution System	p. 88
Galois Connections and Fixed Point Calculus	p. 89
Introduction	p. 89
Fixed Point Equations	p. 89
Languages	p. 89
Functions	p. 90
Datatypes	p. 91
Galois Connections	p. 91
Basic Assumptions	p. 92
Issues and Applications	p. 93
Galois Connections - Introductory Examples	p. 93
Simple Examples	p. 94
The Floor Function	p. 96
Identifying Galois Connections	p. 100
Symmetric Definitions	p. 101
Universal Property	p. 102
Commutativity Properties	p. 103
Pair Algebras	p. 105
Infima and Suprema	p. 107
Extremum Preservation Properties	p. 109
Existence Theorem	p. 111
Fixed Points	p. 115
Prefix Points	p. 115
A First Example	p. 119
Kleene Algebra	p. 122
Fixed Point Calculus	p. 127
Basic Rules	p. 128
Fusion	p. 129
Uniqueness	p. 134
Parameterised Prefix Points	p. 136
Mutual Recursion	p. 141
An Illustration - Arithmetic Expressions	p. 143
Further Reading	p. 146
Calculating Functional Programs	p. 149
Introduction	p. 149
Why Calculate Programs?	p. 149
Functional Programming	p. 150
Universal Properties	p. 150
The Categorical Approach to Datatypes	p. 153
The Pair Calculus	p. 155
Bibliographic Notes	p. 158
Exercises	p. 159
Recursive Datatypes in the Category Set	p. 160
Overview	p. 160
Monomorphic Datatypes	p. 160
Folds	p. 161
Polymorphic Datatypes	p. 163
Properties of Folds	p. 165
Co-datatypes and Unfolds	p. 166
... and Never the Twain Shall Meet	p. 169
Bibliographic Notes	p. 169
Exercises	p. 170
Recursive Datatypes in the Category Cpo	p. 173
The Category Cpo	p. 173
Continuous Algebras	p. 175
The Pair Calculus Again	p. 176
Hylomorphisms	p. 177
Bibliographic Notes	p. 180
Exercises	p. 180
Applications	p. 183
A Simple Compiler	p. 183
Monads andComonads	p. 186
Breadth-First Traversal	p. 191
Bibliographic Notes	p. 193
Exercises	p. 193
Appendix: Implementation in Haskell	p. 197
Products	p. 197
Sums	p. 197
Functors	p. 198
Datatypes	p. 198
Folds and Unfolds	p. 198
Lists	p. 198
Trees	p. 200
Quicksort	p. 200
Algebra of Program Termination	p. 203
Introduction	p. 203
Imperative Programming and Well-Founded Relations	p. 203
Relation Algebra	p. 204
Imperative Programming	p. 206
Domains and Division	p. 208
Well-Foundedness Defined	p. 210
Totality of While Statements	p. 214
Induction Principles	p. 215
Admits-Induction Implies Well-Founded	p. 217
Hylo Equations	p. 218
Relators and Hylos	p. 219
Hylo Programs	p. 220
Intermediate Data Structures	p. 227
The Hylo Theorem	p. 229
Reducing Problem Size	p. 230
A Calculus of F-Reductivity	p. 232
Exercises in Coalgebraic Specification	p. 237
Introduction	p. 237
Mathematical Preliminaries	p. 239
Specification of Groups and Vector Spaces	p. 241
A First Coalgebraic Specification: Binary Trees	p. 244
Elements of Binary Trees	p. 247
Bisimulations and Bisimilarity	p. 248
Invariants	p. 253
Temporal Logic for Coalgebras	p. 255
A Concrete Description of <$>\box<$> and <$>\diamondsuit<$> for Binary Trees	p. 256
Using <$>\box<$> and <$>\diamondsuit<$> for Specification and Verification of Binary Trees	p. 259
Towards a ¿-Calculus for Coalgebras	p. 261
A Case Study: Peterson's Mutual Exclusion Algorithm	p. 265
Peterson's Solution for Mutual Exclusion	p. 265
Dealing with Time in Coalgebraic Specification	p. 267
Class-Valued Methods	p. 269
Peterson's Algorithm in Coalgebraic Specification	p. 270
Refinements between Coalgebraic Specifications	p. 275
Conclusion	p. 277
Algebraic Methods for Optimization Problems	p. 281
Introduction	p. 281
Bibliographic Notes	p. 283
The Algebra of Relations	p. 283
Relations	p. 283
Special Kinds of Relation	p. 286
Breadth	p. 287
Folds	p. 287
BibliographicNotes	p. 290
Exercises	p. 290
Optimization Problems	p. 291
The Eilenberg-Wright Lemma	p. 292
Preorders	p. 292
Monotonicity	p. 293
Minimum	p. 293
The GreedyTheorem	p. 294
Thinning	p. 295
Bibliographic Notes	p. 297
Exercises	p. 297
Optimal Bracketing	p. 299
Representation	p. 300
The Converse-of-a-Function Theorem	p. 300
Spines	p. 301
An Application of Thinning	p. 302
An Application of Greediness	p. 303
Refinement of the Greedy Algorithm to a Program	p. 304
Summary	p. 304
The Haskell Program	p. 305
Bibliographic Notes	p. 305
Exercises	p. 305
Temporal Algebra	p. 309
Introduction	p. 309
Preliminaries	p. 311
Lattices	p. 311
Galois Connections	p. 312
Boolean Algebra	p. 314
Fixed Points	p. 318
Regular Algebra	p. 320
Iteration	p. 320
Repetition	p. 322
Galois Algebra	p. 322
Definition and Basic Properties	p. 323
New Algebrasfrom Old	p. 327
Diamonds and Boxes	p. 327
`Until' and `Since'	p. 330
Confluence	p. 332
Linearity	p. 335
Infinity	p. 337
Sequential Algebra	p. 337
Observations	p. 339
Lifting to Sets	p. 343
Sequential Set Algebras	p. 346
Abstract Sequential Algebras	p. 352
Time-Wise Duality	p. 354
Relational Laws of Sequential Algebra	p. 355
Basic Laws	p. 356
Predicates	p. 359
Left and Right Domain	p. 361
Interval Calculi	p. 364
Somewhere and Everywhere	p. 365
Importability	p. 368
Engineer's Induction	p. 371
Finite and Infinite Observations	p. 373
Measuring Time	p. 375
Phase Calculus	p. 377
Duration Calculus	p. 381
Conclusion	p. 382
Author Index	p. 387
Table of Contents provided by Publisher. All Rights Reserved.

Algebraic and Coalgebraic Methods in the Mathematics of Program Construction

International Summer School and Workshop, Oxford, UK, April 10-14, 2000, Revised Lectures

At a Glance

Paperback

Shipping

How to return your order

Defective items

You Can Find This Book In

More in Computer Programming & Software Development

Coding For Dummies, All New Edition

For Dummies (Computer/Tech)

Python Crash Course

3rd Edition - A Hands-On, Project-Based Introduction to Programming

Python Automation For Dummies

For Dummies (Computer/Tech)

The C Programming Language

Prentice Hall Software

Addiction by Design

Machine Gambling in Las Vegas

The Legend of Zelda(tm) Tears of the Kingdom - The Complete Official Guide

Collector's Edition

Coding For Kids For Dummies

For Kids for Dummies

Teach Yourself VISUALLY iPhone 17 and iPhone Air

Teach Yourself VISUALLY (Tech)

Python All-in-One For Dummies

3rd Edition

Python Workout, Second Edition

200 ten-minute exercises

Effective Modern C++

42 Specific Ways to Improve Your Use of C++11 And C++14

Fundamentals of Software Architecture

A Modern Engineering Approach

Windows 11 For Seniors For Dummies, 2nd Edition

For Dummies (Computer/Tech)

Head First Design Patterns

Building Extensible and Maintainable Object-Oriented Software 2nd Edition

The Pragmatic Programmer 2nd edition

your journey to mastery, 20th Anniversary Edition

The Man Who Solved the Market

How Jim Simons Launched the Quant Revolution SHORTLISTED FOR THE FT & MCKINSEY BUSINESS BOOK OF THE YEAR AWARD 2019

Web Engineering

Theory and Practice

The Essence of Software Engineering

Parallel Computing

Design and Analysis of Algorithms

Introduction to Programming Languages

Typesetting Mathematics With Latex

Semantics With Applications

Advanced Topics in Computer Science

Practical Probabilistic Programming

Practical Probabilistic Programming

This product is categorised by