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
I consider these and related matters in Recursion categories of coalgebras, available at http://xxx.lanl.gov/abs/math.CT/0105256 Regards, Florian Lengyel
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
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
participants (4)
-
Al Vilcius -
Dusko Pavlovic -
Lengyel, Florian -
Peter Selinger