Abstract
It is natural to present subtyping for recursive types coinductively. However, Gapeyev, Levin and Pierce have noted that there is a problem with coinductive definitions of non-trivial transitive inference systems: they cannot be “declarative”—as opposed to “algorithmic” or syntax-directed—because coinductive inference systems with an explicit rule of transitivity are trivial.
We propose a solution to this problem. By using mixed induction and coinduction we define an inference system for subtyping which combines the advantages of coinduction with the convenience of an explicit rule of transitivity. The definition uses coinduction for the structural rules, and induction for the rule of transitivity. We also discuss under what conditions this technique can be used when defining other inference systems.
The developments presented in the paper have been mechanised using Agda, a dependently typed programming language and proof assistant.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Abel, A.: Mixed inductive/coinductive types and strong normalization. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 286–301. Springer, Heidelberg (2007)
Abel, A., Altenkirch, T.: A predicative analysis of structural recursion. Journal of Functional Programming 12(1), 1–41 (2002)
The Agda Team. The Agda Wiki (2010), http://wiki.portal.chalmers.se/agda/
Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)
Barthe, G., Frade, M.J., Giménez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Mathematical Structures in Computer Science 14(1), 97–141 (2004)
Barwise, J.: Mixed Fixed Points. In: The Situation in Logic. CSLI Lecture Notes, vol. 17, Center for the Study of Language and Information, Leland Stanford Junior University (1989)
Bradfield, J., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier, Amsterdam (2007)
Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae 33(4), 309–338 (1998)
Capretta, V.: General recursion via coinductive types. Logical Methods in Computer Science 1(2), 1–28 (2005)
Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994)
Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretations. In: POPL ’92, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 83–94 (1992)
Danielsson, N.A.: Code accompanying the paper (2010a), http://www.cs.nott.ac.uk/~nad/
Danielsson, N.A.: Beating the productivity checker using embedded languages. Draft (2010b)
Danielsson, N.A., Altenkirch, T.: Mixing induction and coinduction. Draft (2009)
de Vries, E.: Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof). Message to the Coq-Club mailing list (August 2009)
Gapeyev, V., Levin, M.Y., Pierce, B.C.: Recursive subtyping revealed. Journal of Functional Programming 12(6), 511–548 (2002)
Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Fundamenta Informaticae 66(4), 353–366 (2005)
Giménez, E.: Un Calcul de Constructions Infinies et son Application à la Vérification de Systèmes Communicants. PhD thesis, Ecole Normale Supérieure de Lyon (1996)
Gordon, A.D.: Bisimilarity as a theory of functional programming. Theoretical Computer Science 228(1-2), 5–47 (1999)
Hagino, T.: A Categorical Programming Language. PhD thesis, University of Edinburgh (1987)
Hancock, P., Pattinson, D., Ghani, N.: Representations of stream processors using nested fixed points. Logical Methods in Computer Science 5(3:9) (2009)
Hensel, U., Jacobs, B.: Proof principles for datatypes with iterated recursion. In: Moggi, E., Rosolini, G. (eds.) CTCS 1997. LNCS, vol. 1290, pp. 220–241. Springer, Heidelberg (1997)
Hughes, J., Moran, A.: Making choices lazily. In: FPCA ’95, Proceedings of the seventh international conference on Functional programming languages and computer architecture, pp. 108–119 (1995)
Kozen, D., Palsberg, J., Schwartzbach, M.I.: Efficient recursive subtyping. Mathematical Structures in Computer Science 5(1), 113–125 (1995)
Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation 207(2), 284–304 (2009)
Levy, P.B.: Infinitary Howe’s method. In: Proceedings of the Eighth Workshop on Coalgebraic Methods in Computer Science (CMCS 2006). ENTCS, vol. 164, pp. 85–104 (2006)
Mendler, P.F.: Inductive Definition in Type Theory. PhD thesis, Cornell University (1988)
Milner, R.: Operational and algebraic semantics of concurrent processes. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics. The MIT Press and Elsevier (1990)
Milner, R., Tofte, M.: Co-induction in relational semantics. Theoretical Computer Science 87(1), 209–220 (1991)
Müller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming 9(2), 191–223 (1999)
Nakata, K., Uustalu, T.: Trace-based coinductive operational semantics for While; Big-step and small-step, relational and functional styles. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol. 5674, pp. 375–390. Springer, Heidelberg (2009)
Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and Göteborg University (2007)
Park, D.: On the semantics of fair parallelism. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 504–526. Springer, Heidelberg (1980)
Raffalli, C.: L’Arithmétique Fonctionnelle du Second Ordre avec Points Fixes. PhD thesis, Université Paris VII (1994)
Sangiorgi, D., Milner, R.: The problem of “weak bisimulation up to”. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 32–46. Springer, Heidelberg (1992)
Turner, D.A.: Total functional programming. Journal of Universal Computer Science 10(7), 751–768 (2004)
Wadler, P., Taha, W., MacQueen, D.: How to add laziness to a strict language, without even being odd. In: Proceedings of the 1998 ACM SIGPLAN Workshop on ML (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Danielsson, N.A., Altenkirch, T. (2010). Subtyping, Declaratively. In: Bolduc, C., Desharnais, J., Ktari, B. (eds) Mathematics of Program Construction. MPC 2010. Lecture Notes in Computer Science, vol 6120. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13321-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-13321-3_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13320-6
Online ISBN: 978-3-642-13321-3
eBook Packages: Computer ScienceComputer Science (R0)