Decidability Properties of Recursive Types

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, we describe an algorithm showing that the natural equivalence generated by finitely many steps of folding and unfolding of 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. From these results invertibility is easily proved for both equivalences.