## 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} }