Fixpoint operators for domain equations

John Power, Giuseppe Rosolini

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

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.
Original languageEnglish
Pages (from-to)323-333
Number of pages11
JournalTheoretical Computer Science
Volume278
Issue number1-2
DOIs
Publication statusPublished - 6 May 2002

Fingerprint

Fixpoint
Enriched Category
Operator
Term
Algebra
Presheaves
Topos
Verify
Internal

Cite this

Fixpoint operators for domain equations. / Power, John; Rosolini, Giuseppe.

In: Theoretical Computer Science, Vol. 278, No. 1-2, 06.05.2002, p. 323-333.

Research output: Contribution to journalArticle

Power, John ; Rosolini, Giuseppe. / Fixpoint operators for domain equations. In: Theoretical Computer Science. 2002 ; Vol. 278, No. 1-2. pp. 323-333.
@article{3edf475ce23c43afa212f9e34a9fef6d,
title = "Fixpoint operators for domain equations",
abstract = "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.",
author = "John Power and Giuseppe Rosolini",
note = "Mathematical foundations of programming semantics (Boulder, CO, 1996)",
year = "2002",
month = "5",
day = "6",
doi = "10.1016/S0304-3975(00)00341-8",
language = "English",
volume = "278",
pages = "323--333",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1-2",

}

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

VL - 278

SP - 323

EP - 333

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-2

ER -