Re: co-iteration?

[Peter Selinger <selinger@Theory.Stanford.EDU>]

To put it in a nutshell, the dual of iteration is recursion. You start
with a function f:AxB-->A, and you obtain a function f":B-->A
satisfying B -f"x1-> AxB -f-> A = B -f"-> A. This is precisely dual to
the situation you describe. 

In a programming language context, much more can be said. Andrzej
Filinski observed in his 1989 Master's thesis that call-by-*name*
recursion is dual to call-by-*value* iteration. In the presence of
certain control operators, call-by-value iteration is in turns
inter-definable with call-by-value recursion. The typing of these
statements is as follows:

1) Call-by-name recursion:   AxB -> A
                            ----------
                              B -> A

2) Call-by-value iteration:  A -> A+B
                            ----------
                              A -> B

3) Call-by-value recursion:  (A->C)xB -> (A->C)
                            --------------------
                                 B -> (A->C)

Here, in 1), AxB stands for a categorical product. In 2), A+B is a
categorical co-product. However, in 3), the "product" type AxB is not
a categorical product (not even a tensor product - in fact it is a
premonoidal structure). And the "function space" A->C is not that of a
cartesian (or monoidal) closed structure. Thus, there is a bit more to
call-by-value recursion than meets the eye.

All this is explained very nicely (both categorically and from a
lambda calculus point of view) in a recent paper by Masahito Hasegawa
and Yoshihiko Kakutani. The paper appeared in FoSSaCS 2001, and it is
available from Hasegawa's website
(http://www.kurims.kyoto-u.ac.jp/~hassei/papers/). In particular, this
paper discusses precisely which axioms to require of the operations
1), 2), and 3), and it details the duality between 1) and 2) and the
equivalence of 2) and 3). 

I may add, although it is not directly in response to the original
question, that the duality between call-by-name and call-by-value can
already be observed even in languages that don't have recursion or
iteration. The duality requires the presence of a certain kind of
control operator. This duality also appears in Filinski's master's
thesis, and its category theoretic meaning is explained in my
paper "Control Categories and Duality"
(http://theory.stanford.edu/~selinger/papers.html).

-- Peter