Abstract
This article has two parts: in the first part, we present some general results about fixpoint objects. The minimal categorical structure required to model soundly the equational type theory which combines higher order recursion and computation types (introduced by Crole and Pitts (1992)) is shown to be precisely a let-category possessing a fixpoint object. Functional completeness for such categories is developed. We also prove that categories with fixpoint operators do not necessarily have a fixpoint object.
In the second part, we extend Freyd's gluing construction for cartesian closed categories to cartesian closed let-categories, and observe that this extension does not obviously apply to categories possessing fixpoint objects. We solve this problem by giving a new gluing construction for a limited class of categories with fixpoint objects; this is the main result of the paper. We use this category-theoretic construction to prove a type-theoretic conservative extension result.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Barr, M. and Wells, C.: Category Theory for Computing Science, International Series in Computer Science, Prentice Hall, 1990.
Crole, R. L.: Categories for Types, Cambridge Mathematical Textbooks, Cambridge University Press, 1993.
Crole, R. L.: Programming metalogics with a fixpoint type, PhD thesis, Computer Laboratory, University of Cambridge, 1991.
CroleR. L. and PittsA. M.: New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, Information and Computation 98 (1992), 171–210.
Freyd, P. J. and Scedrov, A.: Categories, Allegories, North-Holland, 1990.
Jacobs, B.: Categorical type theory, PhD thesis, University of Nijmegen, 1991.
Johnstone, P. T.: Topos Theory, Academic Press, 1977.
KockA.: Monads on symmetric monoidal closed categories, Archiv der Mathematik 21 (1970), 1–10.
Lafont, Y.: Logiques, catégories et machines, PhD thesis, Univ. Paris VII, 1988.
LambekJ. and ScottP. J.: Intuitionist type theory and the free topos, J. Pure Appl. Algebra 19 (1980), 215–257.
Lambek, J. and Scott, P. J.: Introduction to Higher Order Categorical Logic, Cambridge Studies in Advanced Mathematics, Cambridge University Press, 1986.
Mac Lane, S.: Categories for the Working Mathematician 5, Graduate Texts in Mathematics, Springer-Verlag, 1971.
MoggiE.: Notions of computation and monads, Theoretical Computer Science 93 (1989), 55–92.
Pitts, A. M.: Categorical logic, to appear in S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (eds), Handbook of Logic in Computer Science, Oxford University Press, 1995. Technical Report No. 367, University of Cambridge Computer Laboratory.
Plotkin, G. D.: Post-graduate lecture notes in advanced domain theory (incorporating the “Pisa Notes”), Dept. of Computer Science, Univ. of Edinburgh, 1981.
Semantics of Programming Languages: Structures and Techniques, Foundations of Computing, MIT Press, 1992.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Crole, R.L. On fixpoint objects and gluing constructions. Appl Categor Struct 4, 251–281 (1996). https://doi.org/10.1007/BF00122256
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF00122256