Abstract
We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via simulation and bisimulation, respectively. The main novelty of the axiomatization is the fixpoint rule (or coinduction principle), which has the form where P is either a type equality τ=τ′ or type containment τ≤τ′. We define what it means for a proof (formal derivation) to be formally contractive and show that the fixpoint rule is sound if the proof of the premise A, P ⊢ P is contractive. (A proof of A, P ⊢ P using the assumption axiom is, of course, not contractive.) The fixpoint rule thus allows us to capture a coinductive relation in the fundamentally inductive framework of inference systems.
The new axiomatizations are “leaner” than previous axiomatizations, particularly so for type containment since no separate axiomatization of type equality is required, as in Amadio and Cardelli's axiomatization. They give rise to a natural operational interpretation of proofs as coercions. In particular, the fixpoint rule corresponds to definition by recursion. Finally, the axiomatization is closely related to (known) efficient algorithms for deciding type equality and type containment. These can be modified to not only decide type equality and type containment, but also construct proofs in our axiomatizations efficiently. In connection with the operational interpretation of proofs as coercions this gives efficient (O(n 2) time) algorithms for constructing efficient coercions from a type to any of its supertypes or isomorphic types.
This research was partially supported by the Danish Research Council, Project DART.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Martín Abadi. Personal communication, September 1996. ACM State of the Art Summer School on Functional and Object-Oriented Programming in Sobotka, Poland, September 8–14, 1996.
Samson Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65–117. Addison-Wesley, 1990. Also available by anonymous ftp from theory.doc.ic.ac.uk.
R. Amadio and L. Cardelli. Subtyping recursive types. In Proc. 18th Annual ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, pages 104–118. ACM Press, January 1991.
Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems (TOPLAS), 15(4):575–631, September 1993.
Martín Abadi and Marcelo P. Fiore. Syntactic considerations on recursive types. In Proc. 1996 IEEE 11th Annual Symp. on Logic in Computer Science (LICS), New Brunswick, New Jersey. IEEE Computer Society Press, June 1996.
Zena M. Ariola and Jan Willem Klop. Equational term graph rewriting. Technical report, University of Oregon, 1995. To appear in Acta Informatica.
V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93(1):172–221, July 1991. Presented at LICS '89.
Ch. Ben-Yelles. Type assignment in the lambda-calculus: Syntax and semantics. Technical report, Department of Pure Mathematics, University College of Swansea, September 1979. Author's current address: Univérsité des Sciènces et dé la Technologie Houari Boumediene, Institut D'Informatique, El-Alia B.P. No. 32, Alger, Algeria.
Luca Cardelli. Algorithm for subtyping recursive types (in Modula-3). http://www.research.digital.com/SRC/personal/Luca.Cardelli/Notes/RecSub.txt, 1993. Originally implemented in Quest and released in 1990.
F. Cardone and M. Coppo. Type inference with recursive types: Syntax and semantics. Information and Computation, 92(1):48–80, May 1991.
P. Curien and G. Ghelli. Coherence of subsumption. In A. Arnold, editor, Proc. 15th Coll. on Trees in Algebra and Programming, Copenhagen, Denmark, pages 132–146. Springer, May 1990.
Thierry Coquand. Infinite objects in type theory. In Proc. Int'l Workshop on Types for Proofs and Programs, Lecture Notes in Computer Science (LNCS), pages 62–78. Springer-Verlag, 1993.
B. Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.
Andrew Gordon. Bisimilarity as a theory of functional programming. In Proceedings of the Eleventh Conference on the Mathematical Foundations of Programming Semantics (MFPS), New Orleans, March 29 to April 1, 1995, Elsevier Electronic Notes in Theoretical Computer Science, volume 1, 1995.
Fritz Henglein. Dynamic typing: Syntax and proof theory. Science of Computer Programming (SCP), 22(3):197–230, 1994.
R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc., 146:29–60, December 1969.
Furio Honsell and Marina Lenisa. Final semantics for untyped lambdacalculus. In Proc. Int'l Conf. on Typed Lambda Calculi and Applications (TLCA), volume 902 of Lecture Notes in Computer Science (LNCS), pages 249–265. Springer-Verlag, 1995.
Jesper Jørgensen. A Calculus for Boxing Analysis of Polymorphically Typed Languages. PhD thesis, DIKU, University of Copenhagen, October 1995.
Dexter Kozen, Jens Palsberg, and Michael Schwartzbach. Efficient recursive subtyping. In Proc. 20th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 419–428. ACM, ACM Press, January 1993.
Dexter Kozen, Jens Palsberg, and Michael Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science (MSCS), 5(1), 1995.
Marina Lenisa. Final semantics for a higher order concurrent language. In H. Kirchner, editor, Proc. Coll. on Trees in Algebra and Programming (CAAP), volume 1059 of Lecture Notes in Computer Science (LNCS), pages 102–118. Springer-Verlag, 1996.
Robin Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science (TCS), 4(1):1–22, February 1977.
Robin Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences (JCSS), 28:439–466, 1984.
J. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, MIT, 1968.
Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87(1):209–220, 1991. Note.
Andrew M. Pitts. A co-inducion principle for recursively defined domains. Theoretical Computer Science (TCS), 124:195–219, 1994.
Andrew M. Pitts. Relational properties of domains. Information and Computation, 127(2):66–90, June 1996.
J. Rehof. Polymorphic dynamic typing — aspects of proof theory and inference. Master's thesis, DIKU, University of Copenhagen, March 1995.
A. Salomaa. Two complete axiom systems for the algebra of regular events. Journal of the Association for Computing Machinery (JACM), 13(1):158–169, 1966.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brandt, M., Henglein, F. (1997). Coinductive axiomatization of recursive type equality and subtyping. In: de Groote, P., Roger Hindley, J. (eds) Typed Lambda Calculi and Applications. TLCA 1997. Lecture Notes in Computer Science, vol 1210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62688-3_29
Download citation
DOI: https://doi.org/10.1007/3-540-62688-3_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62688-6
Online ISBN: 978-3-540-68438-1
eBook Packages: Springer Book Archive