An iteration theory is an algebraic theory that supports iteration on its operators.
In particular, in an iteration theory, any equation
has a well behaved solution, $t^\dagger$, such that $t[t^\dagger/x]=t^\dagger$. More generally, any finite sequence of equations has a solution,
In general, $t_i$‘s may have other free variables too.
Keeping it simple for a moment, suppose for a second that $n=1$ and $t$ has just one free variable, $x$. For any algebra $A$, the term is interpreted as a function $\llbracket t\rrbracket:A\to A$, and the solution $t^\dagger$ is interpreted as a constant in $\llbracket t^\dagger\rrbracket\in A$, which is a fixed point for the function $\llbracket t\rrbracket$. Thus an iteration theory provides canonical fixed points for equations, in every algebra.
Let $T$ be an abstract clone. It is a Conway theory when it is equipped with a family of operations
such that, for $f\in T(m+n)^m$, (omitting subscripts):
and satisfying axioms:
parameter identity: $((1_n \oplus g) \circ f)^\dagger = g \circ f ^\dagger$ where $f:n \to n+p, \ g:p \to q$
composition identity: $\langle (\langle f , \ 0_m \oplus 1_p \rangle \circ g)^\dagger , 1_p \rangle \circ f = (\langle g , \ 0_n \oplus 1_p \rangle \circ f)^\dagger$ where $f:n \to m+p, \ g:m \to n+p$
double dagger identity: $(\langle 1_n , \ 1_n \rangle \oplus 1_p) \circ f)^\dagger = (f^\dagger)^\dagger$ where $f: n \to n+n+p$
in its Kleisli category.
It is an iteration theory if the operations also satisfy:
where $f: n \to m+p, \ \rho: m \to n$ is a surjective base morphism and $\rho_i: m \to m$ are base with $\rho \circ \rho_i = \rho$ for every i.
This connects with the basic idea, because $f\in T(m+n)^m$ can be thought of as a sequence of $m$ terms with $m+n$ variables, and the solution $f^\dagger$ comprises $m$ terms just having the $n$ free variables.
To equip an abstract clone $T$ with the structure of a Conway theory is to equip the corresponding Lawvere theory with the structure of a traced monoidal category for the categorical product structure.
An abstract clone $T$ is continuous if each set $T(n)$ is equipped with the structure of a cpo, and the clone operations are continuous.
If $T$ is also pointed, i.e. each $T(n)$ has a least element $\bot$, then $T$ has a canonical structure of a Conway theory.
For any $f\in T(m+n)^m$, we define an endofunction $F_f : T(n)^m \to T(n)^m$ by
and then use Tarski‘s fixed point theorem to define
The ideas originated in the work by Calvin C. Elgot in the 1970s. A textbook reference is:
The connection with traced monoidal categories is due to Masahito Hasegawa and Martin Hyland, see Theorem 3.1 of:
This setting is further studied by Alex Simpson and Gordon Plotkin in
Last revised on October 27, 2022 at 15:12:33. See the history of this page for a list of all contributions to it.