Iteration theories: the equational logic of iterative processes
Written both for graduate students and research scientists in theoretical computer science and mathematics, this book provides a detailed investigation of the properties of the fixed point or iteration operation. Iteration plays a fundamental role in the theory of computation: for example, in the theory of automata, in formal language theory, in the study of formal power series, in the semantics of flowchart algorithms and programming languages, and in circular data type definitions. It is shown that in all structures that have beenused as semantic models, the equational properties of the fixed point operation are captured by the axioms describing iteration theories. These structures include ordered algebras, partial functions, relations, finitary and infinitary regular languages, trees, synchronization trees, 2-categories, and others. The book begins with a gentle introduction to the study of universal algebra in the framework of algebraictheories. A remarkably useful calculus is developed for manipulating algebraic theory terms. The reader is then guided through a vast terrain of theorems and applications by means of detailed proofs,examples, and exercises, with the emphasis on equational proofs. The last chapter shows that the familiar topic of correctness logic is a special caseof the equational logic of iteration theories. Several significant open problems are scattered throughout the text.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Why Iteration Theories?
The Theory of a Variety
32 other sections not shown
Other editions - View all
2-category 2-theory algebraic theory base matrix base morphism base surjections bisimulation Boolean coaccessible colimit Conway matricial theory Conway theory coproduct Corollary dagger congruence define Definition denote distinguished morphism EAAtr equivalence equivalence relation Example Exercise feedback finite flowchart follows free algebra functorial dagger implication functorial star GA-implication hom-set homomorphism horizontal morphisms ideal morphisms idempotent induction initial algebra injective base integers isomorphic iteration equation iteration semiring iteration theory morphism left zero identity Lemma matricial iteration theory matrix theory Mats n-guard n-tuple ordered theory parameter identity partial function permutation identity phism preiteration theory morphism Proof Proposition prove pushout regular language satisfies the functorial scalar morphisms Section star and omega star operation subiteration theory subtheory Suppose surjective base matrices surjective base morphism synchronization tree T-algebra T-iteration algebra Theorem theory congruence tupling unique morphism vertex vertical morphism weakest liberal preconditions