An algebraic approach to the interpretation of recursive types

  • Felice Cardone
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)


We present an algebraic framework for the interpretation of type systems including type recursion, where types are interpreted as partial equivalence relations over a Scott domain. We use the notion of iterative algebra, introduced by J. Tiuryn [26] as a counterpart to the categorical notion of iterative algebraic theory by C.C. Elgot [15]. We show that a suitable collection of partial equivalence relations is closed under type constructors and forms an iterative algebra. The existence of type interpretations follows from the initiality, in the class of iterative algebras, of the algebra of regular infinite trees obtained by infinitely unfolding recursive types.


Regular Tree Type Environment Denotational Semantic Type Constructor Infinite Tree 
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]
    M. Abadi and G.D. Plotkin. A per model of polymorphism and recursive types. In Proc. Symposium on Logic and Computer Science, pages 355–365. IEEE, 1990.Google Scholar
  2. [2]
    R. Amadio. Recursion over realizability structures. Information and Computation, 91(1):55–85, 1991.Google Scholar
  3. [3]
    J.A. Bergstra and J.W. Klop. A convergence theorem in process algebra. Technical Report CS-R8733, CWI, Amsterdam, 1987.Google Scholar
  4. [4]
    S.L. Bloom, C.C. Elgot, and J.B. Wright. Solutions of the iteration equation and extensions of the scalar iteration operation. SIAM Journal on Computing, 9(1):25–45, 1980.Google Scholar
  5. [5]
    S.L. Bloom, C.C. Elgot, and J.B. Wright. Vector iteration in pointed iterative theories. SIAM Journal on Computing, 9(3):525–540, 1980.Google Scholar
  6. [6]
    K. Bruce and G. Longo. A modest model of records, inheritance and bounded quantification. In Proc. Symposium on Logic and Computer Science, pages 38–50. IEEE, 1988.Google Scholar
  7. [7]
    K. Bruce and J.C. Mitchell. PER models of subtyping recursive types and higher-order polymorphism. 1991. To appear, POPL 1992.Google Scholar
  8. [8]
    L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988.Google Scholar
  9. [9]
    L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. ACM Computing Surveys, 17:471–522, 1985.Google Scholar
  10. [10]
    F. Cardone. Recursive types for Fun. Theoretical Computer Science, 83:29–56, 1991.Google Scholar
  11. [11]
    F. Cardone and M. Coppo. Type inference with recursive types. Syntax and Semantics. Information and Computation, 92(1):48–80, 1991.Google Scholar
  12. [12]
    M. Coppo. A completeness theorem for recursively defined types. In W. Brauer, editor, Proc. 12th International Colloquium on Automata, Languages and Programming, LNCS 194, pages 120–129. Springer, 1985.Google Scholar
  13. [13]
    B. Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.Google Scholar
  14. [14]
    H. Ehrig, F. Parisi-Presicce, P. Boehm, C. Rieckhoff, C. Dimitrovici, and M. Grosse-Rhode. Algebraic data type and process specification based on projection spaces. In Recent trends in data type specification, LNCS 332, pages 23–43. Springer, 1988.Google Scholar
  15. [15]
    C.C. Elgot. Monadic computation and iterative algebraic theories. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium 73, pages 175–318, Amsterdam, 1975. North Holland.Google Scholar
  16. [16]
    C.C. Elgot, S.L. Bloom, and R. Tindell. The algebraic structure of rooted trees. Journal of Computer and System Sciences, 16(3):362–399, 1978.Google Scholar
  17. [17]
    J. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright. Initial algebra semantics and continuous algebras. Journal of the ACM, 24:68–95, 1977.Google Scholar
  18. [18]
    M. Grosse-Rhode and H. Ehrig. Transformation of combined data type and process specifications using projection algebras. In Stepwise refinement of distributed systems, LNCS 430, pages 301–339. Springer, 1989.Google Scholar
  19. [19]
    C. Gunter. Universal profinite domains. Information and Computation, 72:1–30, 1987.Google Scholar
  20. [20]
    C.A. Gunter and D.S. Scott. Semantic domains. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, pages 633–674, Amsterdam, 1990. North Holland.Google Scholar
  21. [21]
    D. MacQueen, G.D. Plotkin, and R. Sethi. An ideal model for recursive polymorphic types. Information and Control, 71((1/2)):95–130, 1986.Google Scholar
  22. [22]
    A.R. Meyer. Semantical paradigms: Notes for an invited lecture, with two appendices by Stavros S. Cosmadakis. In 3rd Symposium on Logic in Computer Science, pages 236–255. IEEE, 1988.Google Scholar
  23. [23]
    J.C. Mitchell. A type inference approach to reduction properties and semantics of polymorphic expressions. In Proc. ACM Conference on LISP and Functional Programming, pages 308–319, 1986.Google Scholar
  24. [24]
    D.S. Scott. Lectures on a mathematical theory of computation. Lecture notes, Merton College, Oxford, Michaelmas Term, 1980.Google Scholar
  25. [25]
    M. Smyth and G.D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal of Computing, 11:761–783, 1982.CrossRefGoogle Scholar
  26. [26]
    J. Tiuryn. Unique fixed points vs. least fixed points. Theoretical Computer Science, 12:229–254, 1980.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Felice Cardone
    • 1
  1. 1.Dipartimento di Scienze dell'InformazioneUniversità di MilanoMilano

Personalised recommendations