Iteration theories. The equational logic of iterative processes.

*(English)*Zbl 0773.03033
EATCS Monographs on Theoretical Computer Science. Berlin: Springer- Verlag. xv, 630 p. (1993).

Being the result of a great deal of experience and synthesis, the present monograph provides a detailed investigation of the structures involving fixed point properties in the process of computation. Many of the fixed point questions met in theoretical computer science can be stated as follows: for an appropriate category \(C\) and endofunctor \(F: C\to C\), find the least (unique, initial, canonical etc.) point \(x\) such that \(x=F(x)\). The natural framework to study such a problem is provided by iteration theories since they describe the equational properties of the fixed point operation, in combination with other operations like composition, coproducts, orderings, sums etc. The book is organized in 14 chapters as follows: The first four chapters introduce the necessary background and results: posets, 2-categories, \(\Sigma\)-trees and \(\Sigma\)-algebras, theories, sequacious relations, the categories of \(T\)(theory)-algebras and their formal properties. Chapters 5-8 contain a first half of the fundamental results: iterative theories (Ch. 5), iteration theories (Ch. 6), iteration algebras (Ch. 7), and continuous theories (Ch. 8). The results of Ch. 8 are to be applied in Ch. 13 to parallelism semantics. Chapters 9 and 10 are devoted to matrix iteration theories and, respectively, matricial iteration theories as regular languages. Chapter 11 introduces the notion of presentation, necessary to characterize an iteration theory as being a coproduct of an iteration theory and of a free iteration theory, and is applicable to interpreting the sequential (Ch. 12 – Flowchart behaviors) and parallel (Ch. 13 – Synchronization trees) algorithms. Finally, Chapter 14 (Floyd-Hoare logic) presents a system of partial correctness logic for all flowchart programs, as being a special case of the equational logic of iteration theories.

Reviewer: N.Curteanu (Iaşi)

##### MSC:

03D75 | Abstract and axiomatic computability and recursion theory |

03-02 | Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations |

68-02 | Research exposition (monographs, survey articles) pertaining to computer science |

68Q55 | Semantics in the theory of computing |

03B70 | Logic in computer science |

03G30 | Categorical logic, topoi |