The equational logic of fixed points (Q1391734)

This is a well-written and extensive survey of the universal algebraic approach to the study of fixed points in mathematics generally, and theoretical computer science more particularly. While no proofs of theorems are presented, there are many references to the current literature (175 bibliographic entries), and many examples are given in detail. The remainder of this review is quoted from the authors' Introduction: ``Most computer scientists realize that just about every aspect of their subject involves fixed points. To list but a few familiar examples, context-free grammars are nothing but a system of fixed-point equations over the semiring of languages; circular data type specifications and recursive program schemes are also explicit fixed-point equations; the semantics of flowchart and higher type languages require the existence of certain fixed points; indeed, a ``recursive solution'' is a special kind of ``fixed point''. An entire industry has developed in order to answer questions such as: In what settings can one find solutions of this or that particular fixed-point equation? (The equation \(D=[D \to D]\) comes to mind.) ``This paper is not concerned with questions of the existence or the construction of fixed points. We are concerned with the properties of fixed-point solutions, especially equational properties. We want to emphasize the fact that there is a complete axiomatization of the valid fixed-point identities, namely the axioms for iteration theories. Knowledge of these identities is useful in deriving properties of fixed points. In fact, we think it is just as useful to computer scientists as the knowledge of rings is for students pondering such equations as \((x+a)(x-a)= x^2-a^2\). The fixed-point calculus, consisting of the axioms for fixed points and standard (many-sorted) equational logic ought to be a part of the standard toolkit of theoreticians. The point of this tutorial is to describe several kinds of models for fixed points, discuss some alternative sets of axioms, and give a pointer to the literature for proofs and related results. ``The study of the fixed-point operation in computer science has been greatly influenced by the pioneering work of Calvin Elgot and the ADJ group (Joe Goguen, Jim Thatcher, Eric Wagner, and Jess Wright) at IBM Yorktown Heights, and that of the French school of Theoretical Informatics led by Maurice Nivat. It is an interesting fact that despite the existence of many fixed-point theorems, there has been no axiomatic treatment of the fixed-point operation in classical mathematics''.