Equational logic of circular data type specification

Iteration theories, introduced by Bloom, Elgot and Wright in (1980), formalize the equational properties of the strong behaviors of flowchart algorithms. We show that the same equational properties are shared by the functors used to specify circular data types. Lehmann and Smyth (1981) have shown how to specify circular data types, such as stacks, as fixed points of certain functors (the-called gw -functors). For example, the set of stacks of elements in the set A is a solution to the equation in the variable X , X = F ( A , X ) where F ( X , X ) ≔ = 1 + A × X is the functor on SET taking the pair ( A , X ) to the disjoint union of the singleton set 1 and the product A × X . Such equations have initial solutions, F † ( A ), which in turn determine a ‘solution functor’ F † . The equational properties of the operation F ↦ F † are precisely captured by the axioms for iteration theories. More precisely, we show how the structure Th ω ( C ) of all ω-functors C n → C p , n , p ⩾ 0, on the ω-category C , forms an iteration theory and, conversely, any identity valid in all such structures is valid in the class of all iteration theories.