The equational properties of iteration, when combined with composition and pairing, are captured by the notion of 'iteration theory'. We believe that every iterative construction satisfies at least the properties of iteration theories. Axiomatizations are given for several varieties of iteration theories which occur naturally in the semantics of programming languages, i.e., those generated by theories of trees, theories of sequacious functions, theories of partial functions, and theories of both sequacious and partial functions with distinguished predicates. We show which additional equations must be added to the axioms for iteration theories in order to obtain a set of axioms for these subvarieties. Concrete descriptions of the free theories in each variety are given.
ASJC Scopus subject areas
- Computer Science(all)