Logic in Computer Science (LICS 1990)

Paper: Recursive types reduced to inductive types (at LICS 1990)

Authors: Freyd, P.

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

BibTeX

  @InProceedings{Freyd-Recursivetypesreduc,
    author = 	 {Freyd, P.},
    title = 	 {Recursive types reduced to inductive types},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {498--507},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }