Decidability Properties of Recursive Types

  • Felice Cardone
  • Mario Coppo
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)


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. A formal proof of the former result, to our knowledge, has never appeared in the literature. The latter result, on the contrary, is 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.


Type Structure Decidability Property Recursion Operator Type Constraint Lambda Calculus 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)zbMATHGoogle Scholar
  2. 2.
    MacQueen, D., Plotkin, G., Sethi, R.: An ideal model for recursive polymorphic types. Information and Control 71, 95–130 (1986)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Cardone, F., Coppo, M.: Type inference with recursive types. Syntax and Semantics. Information and Computation 92, 48–80 (1991)zbMATHMathSciNetGoogle Scholar
  4. 4.
    Fiore, M.: A coinduction principle for recursive data types based on bisimulation. In: Proceedings Eighth Symposium on Logic in Computer Science, IEEE, Los Alamitos (1993)Google Scholar
  5. 5.
    Rutten, J.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249, 3–80 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Jones, S.: The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs (1987)zbMATHGoogle Scholar
  7. 7.
    Statman, R.: Recursive types and the subject reduction theorem. Technical Report 94–164, Carnegie Mellon University (1994)Google Scholar
  8. 8.
    Marz, M.: An algebraic view on recursive types. Applied Categorical Structures 7(12), 147–157 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Coppo, M.: Type inference with recursive type equations. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 184–198. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. 10.
    Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 63–81. Springer, Heidelberg (1997)Google Scholar
  11. 11.
    Ariola, Z., Klop, J.: Equational term graph rewriting. Fundamenta Informaticae 26, 207–240 (1996)zbMATHMathSciNetGoogle Scholar
  12. 12.
    Scott, D.: Some philosophical issues concerning theories of combinators. In: Böhm, C. (ed.) Lambda-Calculus and Computer Science Theory. LNCS, vol. 37, pp. 346–366. Springer, Heidelberg (1975)CrossRefGoogle Scholar
  13. 13.
    Breazu-Tannen, V., Meyer, A.: Lambda calculus with constrained types. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 23–40. Springer, Heidelberg (1985)Google Scholar
  14. 14.
    Milner, R.: A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17, 348–375 (1978)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Courcelle, B.: Fundamental properties of infinite trees. Theoretical Computer Science 25, 95–169 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Courcelle, B., Kahn, G., Vuillemin, J.: Algorithmes d’équivalence et de réduction à des expressions minimales, dans une classe d’équations récursives simples. In: Loeckx, J. (ed.) ICALP 1974. LNCS, vol. 14, pp. 200–213. Springer, Heidelberg (1974)Google Scholar
  17. 17.
    Klop, J.: Term rewriting systems. In: Abramsky, S., Gabby, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, pp. 1–116. Oxford University Press, New York (1992)Google Scholar
  18. 18.
    Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey. Theoretical Computer Science 121, 279–308 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Cardone, F.: A coinductive completeness proof for the equivalence of recursive types. Theoretical Computer Science 275, 575–587 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Turi, D., Rutten, J.: On the foundations of final semantics: Non-standard sets, metric spaces, partial orders. Mathematical Structures in Computer Science 8, 481–540 (1998)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Felice Cardone
    • 1
  • Mario Coppo
    • 2
  1. 1.DISCoUniversità di Milano-BicoccaMilano
  2. 2.Dipartimento di InformaticaUniversità di TorinoTorino

Personalised recommendations