M. Coppo and F. Cardone
Decidability properties of recursive
types
In ICTCS'03, volume 2841 of LNCS, pages 242-255
Springer-Verlag, 2003
In this paper we study decision problems and invertibility for
two notions of equivalence of recursive types. In particular,
for recursive types presented by means of a recursion operator mu,
we describe an algorithm showing that the natural equivalence generated
by finitely many steps of folding and unfolding of mu-types is
decidable. For recursive types presented by finite systems of recursive
equations, we give a thoroughly coinductive characterization of the
equivalence induced by their interpretation as infinite (regular)
trees, from which the decidability of this equivalence follows.
A formal proof of the former result, to our knowledge, has never
appeared in the literature. The latter result, on the contrary,
is well known but we present here a new proof obtained as an
application of general coalgebraic facts to the theory of recursive
types. From these results invertibility is easily proved
for both equivalences.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43