Abstract
In this paper we present a theorem for defining fixed-points in categories of sheaves. This result gives a unifying and general account of most techniques used in computer science in order to ensure convergency of circular definitions, such as (but not limited to) well-founded recursion and contractivity in complete ultra metric spaces. This general fixed-point theorem encompasses also a similar set theoretic result presented in previous work, based on the notion of ordered family of equivalences, and implemented in the Coq proof assistant.
Work supported by italian MIUR project COFIN 2001013518 CoMeta.
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
Balaa, A., Bertot, Y.: Fix-point equations for well-founded recursion in type theory. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 1–16. Springer, Heidelberg (2000)
Bove, A.: General recursion in type theory. In: [5], pp. 39–58
de Bakker, J.W., Zucker, J.I.: Processes and the denotational semantics of concurrency. Information and Control 54, 70–120 (1982)
Di Gianantonio, P., Miculan, M.: A unifying approachto recursive and corecursive definitions. In: [5], pp. 148–161
Geuvers, H., Wiedijk, F. (eds.): Proceedings of TYPES 2002. LNCS, vol. 2646. Springer, Heidelberg (2003)
Giménez, E.: Codifying guarded recursion definitions withrecursiv e schemes. In: Smith, J., Dybjer, P., Nordström, B. (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1995)
Gimenez, E.: A tutorial on recursive types in Coq. RT-0221, INRIA (1998)
INRIA. The Coq Proof Assistant (2003), http://coq.inria.fr/doc/main.html
Kelley, J.L.: General Topology. Springer, Heidelberg (1975)
Lambek, J., Scott, P.J.: Introduction to higher order categorical logic. Cambridge studies in advanced mathematics, vol. 7. Cambridge University Press, Cambridge (1986)
Matthews, J.: Recursive function definition over coinductive types. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 73–90. Springer, Heidelberg (1999)
Nordström, B.: Terminating general recursion. BIT 28, 605–619 (1988)
Paulin-Mohring, C.: Inductive definitions in the system Coq; rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Di Gianantonio, P., Miculan, M. (2004). Unifying Recursive and Co-recursive Definitions in Sheaf Categories. In: Walukiewicz, I. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2004. Lecture Notes in Computer Science, vol 2987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24727-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-24727-2_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21298-0
Online ISBN: 978-3-540-24727-2
eBook Packages: Springer Book Archive