TY - JOUR
T1 - Fixpoint operators for domain equations
AU - Power, John
AU - Rosolini, Giuseppe
N1 - Mathematical foundations of programming semantics (Boulder, CO, 1996)
PY - 2002/5/6
Y1 - 2002/5/6
N2 - We investigate previous termfixpointnext termprevious termoperatorsnext term for previous termdomainnext termprevious termequationsnext term. It is routine to verify that if every endofunctor on a category has an initial algebra, then one can construct a previous termfixpointnext termprevious termoperatornext term from the category of endofunctors to the category. That construction does not lift routinely to enriched categories, using the usual enriched notion of initiality of an endofunctor. We show that by embedding the 2-category of small enriched categories into the 2-category of internal categories of a presheaf topos, we can recover the previous termfixpointnext term construction elegantly. Also, we show that in the presence of cotensors, an enriched category allows the previous termfixpointnext term construction.
AB - We investigate previous termfixpointnext termprevious termoperatorsnext term for previous termdomainnext termprevious termequationsnext term. It is routine to verify that if every endofunctor on a category has an initial algebra, then one can construct a previous termfixpointnext termprevious termoperatornext term from the category of endofunctors to the category. That construction does not lift routinely to enriched categories, using the usual enriched notion of initiality of an endofunctor. We show that by embedding the 2-category of small enriched categories into the 2-category of internal categories of a presheaf topos, we can recover the previous termfixpointnext term construction elegantly. Also, we show that in the presence of cotensors, an enriched category allows the previous termfixpointnext term construction.
UR - http://dx.doi.org/10.1016/S0304-3975(00)00341-8
U2 - 10.1016/S0304-3975(00)00341-8
DO - 10.1016/S0304-3975(00)00341-8
M3 - Article
SN - 0304-3975
VL - 278
SP - 323
EP - 333
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 1-2
ER -