1 Mathematical Motivation.- 2 Why Iteration Theories?.- 3 Suggestions for the Impatient Reader.- 4 A Disclaimer.- 5 Numbering.- 1 Preliminary Facts.- 1 Sets and Functions.- 2 Posets.- 3 Categories.- 4 2-Categories.- 4.1 Cellc is a 2-Category, Too.- 5 ?-Trees.- 2 Varieties and Theories.- 1 S-Algebras.- 2 Terms and Equations.- 3 Theories.- 4 The Theory of a Variety..- 3 Theory Facts.- 1 Pairing and Separated Sum.- 2 Elementary Properties of TH.- 3 Theories as N x N-Sorted Algebras.- 4 Special Coproducts.- 5 Matrix and Matricial Theories.- 5.1 Matrix Theories.- 5.2 Theories of Relations.- 5.3 Matricial Theories.- 5.4 Sequacious Relations.- 5.5 Sequacious Functions.- 6 Pullbacks and Pushouts of Base Morphisms.- 7 2-Theories.- 4 Algebras.- 1 T-algebras.- 1.1 An Example: Algebras of Matrix Theories.- 2 Free Algebras in Tb.- 2.1 The T-algebras Tn.- 2.2 Infinitely Generated Free Algebras in Tb.- 3 Subvarieties of Tb.- 4 The Categories TH and var.- 5 Notes.- 5 Iterative Theories.- 1 Ideal Theories.- 2 Iterative Theories Defined.- 3 Properties of Iteration in Iterative Theories.- 4 Free Iterative Theories.- 5 Notes.- 6 Iteration Theories.- 1 Iteration Theories Defined.- 2 Other Axiomatizations of Iteration Theories.- 2.1 Scalar Axiomatizations.- 3 Theories with a Functorial Dagger.- 4 Pointed Iterative Theories.- 5 Free Iteration Theories.- 6 Constructions on Iteration Theories.- 7 Feedback Theories.- 8 Summary of the Axioms.- 8.1 Axioms for Iteration Theories.- 8.2 Axioms for Conway Theories.- 9 Notes.- 7 Iteration Algebras.- 1 Definitions.- 2 Free Algebras in T+.- 3 The Retraction Lemma.- 4 Some Categorical Facts.- 5 Properties of T+.- 6 A Characterization Theorem.- 7 Strong Iteration Algebras.- 8 Notes.- 8 Continuous Theories.- 1 Ordered Algebraic Theories.- 1.1 Free Ordered Theories.- 2 ?-Continuous Theoriesx.- 2.1 Free ?-Continuous Theories.- 3 Rational Theories.- 4 Initiality and Iteration in 2-Theories.- 5 ?-Continuous 2-Theories.- 5.1 The Definition, with Examples.- 5.2 Initial Algebras Exist.- 5.3 ?-Continuous 2-Theories are Iteration Theories.- 6 Notes.- 9 Matrix Iteration Theories.- 1 Notation.- 2 Properties of the Star Operation.- 3 Matrix Iteration Theories Defined.- 4 Presentations in Matrix Iteration Theories.- 5 The Initial Matrix Iteration Theory.- 6 An Extension Theorem.- 7 Matrix Iteration Theories of Regular Sets.- 8 Notes.- 10 Matricial Iteration Theories.- 1 From Dagger to Star and Omega, and Back.- 2 Matricial Iteration Theories Defined.- 3 Examples.- 3.1 SeqRel(inA).- 3.2 L(X*; X?).- 3.3 RL(X*;X?).- 3.4 CL(X*; X?).- 3.5 RCL(X*;X?).- 3.6 More Commutative Identities.- 4 Additively Closed Subiteration Theories.- 4.1 An A.C. Subiteration Theory of C(X*; X?).- 5 Presentations in Matricial Iteration Theories.- 6 The Initial Matricial Iteration Theory.- 7 The Extension Theorem.- 8 Additively Closed Theories of Regular Languages.- 9 Closed Regular (?-Languages.- 10 Notes.- 11 Presentations.- 1 Presentations in Iteration Theories.- 2 Simulations of Presentations.- 3 Coproducts Revisited.- 4 Notes.- 12 Flowchart Behaviors.- 1 Axiomatizing Sequacious Functions.- 2 Axiomatizing Partial Functions.- 3 Diagonal Theories.- 4 Sequacious Functions with Predicates.- 4.1 The Theory of One Predicate.- 4.2 Several Binary Predicates.- 5 Partial Functions with Predicates.- 6 Notes.- 13 Synchronization Trees.- 1 Theories of Synchronization Trees.- 2 Grove Iteration Theories.- 3 Axiomatizing Synchronization Trees.- 4 Bisimilarity.- 5 Notes.- 14 Floyd-Hoare Logic.- 1 Guards.- 2 Partial Correctness Assertions.- 2.1 An Alternative Definition of n-Guards.- 3 The Standard Example.- 4 Rules for Partial Correctness.- 4.1 Formalization.- 4.2 Formal Rules.- 5 Soundness.- 6 The Standard Example, Continued.- 7 A Floyd-Hoare Calculus for Iteration Theories.- 8 The Standard Example, Again.- 9 Completeness.- 9.1 The Invariant Guard Property.- 9.2 Completeness of Floyd-Hoare Rules.- 9.3 Guarantees of Completeness.- 9.4 Weakest Liberal Preconditions and Completeness.- 9.5 The Cook Completeness Theorem.- 9.6 The Unwinding Property.- 10 Examples.- 10.1 An Example of a Correctness Proof.- 10.2 The Interpolation Property Does Not Imply the Invariant Guard Property.- 10.3 A Non-Expressive Structure with Weakest Liberal Preconditions.- 11 Notes.- List of Symbols.