Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)
MacQueen, D., Plotkin, G., Sethi, R.: An ideal model for recursive polymorphic types. Information and Control 71, 95–130 (1986)
Cardone, F., Coppo, M.: Type inference with recursive types. Syntax and Semantics. Information and Computation 92, 48–80 (1991)
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)
Rutten, J.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249, 3–80 (2000)
Jones, S.: The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs (1987)
Statman, R.: Recursive types and the subject reduction theorem. Technical Report 94–164, Carnegie Mellon University (1994)
Marz, M.: An algebraic view on recursive types. Applied Categorical Structures 7(12), 147–157 (1999)
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)
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)
Ariola, Z., Klop, J.: Equational term graph rewriting. Fundamenta Informaticae 26, 207–240 (1996)
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)
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)
Milner, R.: A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17, 348–375 (1978)
Courcelle, B.: Fundamental properties of infinite trees. Theoretical Computer Science 25, 95–169 (1983)
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)
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)
Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey. Theoretical Computer Science 121, 279–308 (1993)
Cardone, F.: A coinductive completeness proof for the equivalence of recursive types. Theoretical Computer Science 275, 575–587 (2002)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cardone, F., Coppo, M. (2003). Decidability Properties of Recursive Types. In: Blundo, C., Laneve, C. (eds) Theoretical Computer Science. ICTCS 2003. Lecture Notes in Computer Science, vol 2841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45208-9_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-45208-9_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20216-5
Online ISBN: 978-3-540-45208-9
eBook Packages: Springer Book Archive