This monograph contains the results of our joint research over the last ten years.…This book provides a detailed investigation of the properties of the fixed point or iteration operation.…It is shown that in all structures that have been used as semantic models, the equational properties of the fixed point operation are captured by the axioms describing iteration theories. (From the preface.)
After an introduction, the first four chapters of this monograph set up the algebraic and categorical machinery in which the work is to be presented. Program operations are represented as functions (morphisms) from p variables to n variables, written f : n → p. (In this notation, a p-ary term t ( x 1 ,..., x p ) would be a morphism t : 1 → p .)
The fifth chapter introduces iterative theories, where certain morphisms f have a unique solution f t for an iteration equation for f. The next chapter defines iteration theories as those iterative theories where all morphisms f have an iteration operation f t defined. Iteration becomes a functor. These ideas are then applied to regular languages (finite and infinite) [1], flowchart behaviors (which the authors call sequacious functions) [2], and synchronization trees [3]. Finally, the authors show how Floyd-Hoare logic [4] can be viewed as a special case of equational logic in theories that admit guard expressions.
The dagger operation is nonstandard. For example, in regular languages, it corresponds to the operation A * B. Consequently, it requires some thinking to relate the authors’ equational axioms to others that the reader might be familiar with, such as those of Salomaa or Kozen.
The treatment is formal and rigorous, but leisurely. Required concepts are defined, but a familiarity with the way languages are related to semirings will help the reader. Although a toy example is treated (verification of an algorithm by John Reynolds), direct application to program verification is not really the goal of the book; rather, the authors intend to give the reader a theoretical understanding of the iteration operation.
I found the introduction a bit casual. I would have liked to read a good survey on the subject of iteration in equational logic and the difficulties in treating recursion--something that I have not come across yet.
Most of the material has appeared or is to appear in papers (as cited above). As such, the book becomes a long compendium of the authors’ work. Readers interested in a specific application area would probably want to refer to the paper directly rather than investing in an expensive book. Researchers in equational logic might want a useful collection of the results, however.
This monograph could have had a wider appeal if the authors had devoted more space to explaining the connection to related work, such as dynamic algebras [5], relation algebras with star [6], action algebras [7], and process algebras with guards [8], in all of which iteration is an important operation.
