co-iteration?

co-iteration?

[Al Vilcius]

For many (categorical) notions,
there is a useful (often fantastic) dual notion.

What about iteration?

In a category with finite coproducts,
we have a notion of iteration   f:A-->A+B
(written A -f-> A+B here)
which in the case of sets and partial functions, for example,
is completely specified by the Elgot equation
   A -f-> A+B -f"+1-> B =  A -f"-> B  recursive in  f"
(plus one more little, quite natural condition - see [Manes '92])
This awful looking mess, written using the infix morphism notation,
actually looks quite neat when you draw the diagram.

Now without meaning to start the "co"-wars again,
- is there a useful notion of co-iteration?
- what could it do for us, say in the category of partial functions?
- is there a simple algebra/coalgebra context?

Reference:
[Manes '92] E.G.Manes, "Predicate Transformer Semantics", CUP 1992

Al Vilcius
personal: al.r@vilcius.com
business: avilcius@webpearls.com

Re: co-iteration?

[Peter Selinger]

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

Re: co-iteration?

[Dusko Pavlovic]

> In a category with finite coproducts,
> we have a notion of iteration   f:A-->A+B
> (written A -f-> A+B here)
> which in the case of sets and partial functions, for example,
> is completely specified by the Elgot equation
>    A -f-> A+B -f"+1-> B =  A -f"-> B  recursive in  f" [...]
> Now without meaning to start the "co"-wars again,
> - is there a useful notion of co-iteration?
> - what could it do for us, say in the category of partial functions?
> - is there a simple algebra/coalgebra context?

by reversing the arrows, and replacing coproducts by products, we get
that, for the function g:AxB->A holds

B--<g',id>-->AxB--g-->A = B--g'-->A, ie g(g'(y),y) = g'(y)

in words, the "coiterator" g' is just a fixpoint of g.

-- dusko

Re: co-iteration?

[Lengyel, Florian]

I consider these and related matters in Recursion categories of coalgebras,
available at http://xxx.lanl.gov/abs/math.CT/0105256

Regards,
Florian Lengyel