Abstract
This paper describes a theory of second-order trees, that is, finite and infinite trees where nodes of the tree can bind variables that appear further down in the tree. Such trees can be used to provide a natural and intuitive interpretation for type systems with equirecursive types and binding constructs like universal and existential quantifiers. The paper defines the set of binding trees, and a subset of these called regular binding trees. These are similar to the usual notion of regular trees, but generalised to take into account the binding structure. Then the paper shows how to interpret a second-order type system with recursive quantifiers as binding trees, and gives a sound and complete axiomatisation of when two types map to the same tree. Finally the paper gives a finite representation for trees called tree automata, and gives a construction for deciding when two automata map to the same tree. To tie everything together, the paper defines a mapping from types to automata, thus giving a decision procedure for when two types map to the same tree.
The notation x y := z denotes the capture avoiding substitution of z for y in x.
A type coercion changes the type of an expression but has no runtime effect.
Chapter PDF
Similar content being viewed by others
References
Roberto Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Progamming Languages and Systems, 15(4):575–631, September 1993.
N. De Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Mat., 34:381–392, 1972.
Dario Colazzo and Giorgio Ghelli. Subtyping recursive types in kernel fun. In 1999 Symposium on Logic in Computer Science, pages 137–146, Trento, Italy, July 1999.
Jean-Yves Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination de coupures dans l’analyse et la théorie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63–92. North-Holland Publishing Co., 1971.
Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.
Neal Glew. A theory of second-order trees. Technical Report TR2001-1859, Department of Computer Science, Cornell University, 4130 Upson Hall, Ithaca, NY 14853-7501, USA, January 2002.
Irving Kaplansky. Set Theory and Metric Spaces. Chelsea Pub Co, 2nd edition, June 1977.
Dexter Kozen, Jens Palsberg, and Michael Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5(1):113–125, March 1995.
Benjamin Pierce. Bounded quantification is undecidable. Information and Computation, 112:131–165, 1994.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Glew, N. (2002). A Theory of Second-Order Trees. In: Le Métayer, D. (eds) Programming Languages and Systems. ESOP 2002. Lecture Notes in Computer Science, vol 2305. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45927-8_11
Download citation
DOI: https://doi.org/10.1007/3-540-45927-8_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43363-7
Online ISBN: 978-3-540-45927-9
eBook Packages: Springer Book Archive