Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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.
R. Amadio. Recursion over realizability structures. Information and Computation, 91(1):55–85, 1991.
J.A. Bergstra and J.W. Klop. A convergence theorem in process algebra. Technical Report CS-R8733, CWI, Amsterdam, 1987.
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.
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.
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.
K. Bruce and J.C. Mitchell. PER models of subtyping recursive types and higher-order polymorphism. 1991. To appear, POPL 1992.
L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988.
L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. ACM Computing Surveys, 17:471–522, 1985.
F. Cardone. Recursive types for Fun. Theoretical Computer Science, 83:29–56, 1991.
F. Cardone and M. Coppo. Type inference with recursive types. Syntax and Semantics. Information and Computation, 92(1):48–80, 1991.
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.
B. Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.
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.
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.
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.
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.
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.
C. Gunter. Universal profinite domains. Information and Computation, 72:1–30, 1987.
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.
D. MacQueen, G.D. Plotkin, and R. Sethi. An ideal model for recursive polymorphic types. Information and Control, 71((1/2)):95–130, 1986.
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.
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.
D.S. Scott. Lectures on a mathematical theory of computation. Lecture notes, Merton College, Oxford, Michaelmas Term, 1980.
M. Smyth and G.D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal of Computing, 11:761–783, 1982.
J. Tiuryn. Unique fixed points vs. least fixed points. Theoretical Computer Science, 12:229–254, 1980.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cardone, F. (1992). An algebraic approach to the interpretation of recursive types. In: Raoult, J.C. (eds) CAAP '92. CAAP 1992. Lecture Notes in Computer Science, vol 581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55251-0_4
Download citation
DOI: https://doi.org/10.1007/3-540-55251-0_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55251-2
Online ISBN: 978-3-540-46799-1
eBook Packages: Springer Book Archive