• DocumentCode
    2719167
  • Title

    Recursive types reduced to inductive types

  • Author

    Freyd, Peter

  • Author_Institution
    Pennsylvania Univ., Philadelphia, PA, USA
  • fYear
    1990
  • fDate
    4-7 Jun 1990
  • Firstpage
    498
  • Lastpage
    507
  • Abstract
    A setting called complete partial ordering (CPO) categories and the notion of dialgebra are described. Free dialgebras on CPO-categories are shown to be the same as minimal invariant objects. In the case that the bifunctor is independent of its contravariant variable (hence construable as a covariant functor), it is shown that minimal invariant objects serve simultaneously as initial algebras and final coalgebras. The reduction to inductive types is shown in a two-step process. First let T be a bifunctor contravariant in its first variable, convariant in the second. For each A it is possible to consider the convariant functor that sends X to TAX. If FA denotes a minimal invariant object of this covariant functor, one for each A, then F becomes a contrainvariant functor. It is shown that the minimal invariant objects of F are minimal invariant objects of the original bifunctor T. Secondly, let T be a contrainvariant functor. It is shown that the square of the functor (necessarily covariant) has the same minimal invariant objects
  • Keywords
    data structures; formal logic; CPO-categories; bifunctor; complete partial ordering; contravariant variable; covariant functor; dialgebras; final coalgebras; inductive types; initial algebras; minimal invariant object; minimal invariant objects; Algebra; Upper bound;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e
  • Conference_Location
    Philadelphia, PA
  • Print_ISBN
    0-8186-2073-0
  • Type

    conf

  • DOI
    10.1109/LICS.1990.113772
  • Filename
    113772