×

Equilogical spaces. (English) Zbl 1059.18004

The paper studies the category \({\mathcal E}qu\) of equivalence relations and equivalence-preserving continuous mappings over the standard category of topological \(T_0\)-spaces. An equivalent definition, in terms of algebraic lattices and partial equivalence relations, is used to prove cartesian closure by using well-known theorems in domain theory, related to injective properties of algebraic lattices treated as topological spaces. Later, the focus is on expressiveness of \({\mathcal E}qu\), in particular, its capability to represent type theory and logic, and develop notions of modest sets and assemblies in order to justify that a model of dependent type theory is obtained. Finally, some comparisons are made to other known models.

MSC:

18C50 Categorical semantics of formal languages
68Q55 Semantics in the theory of computing
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
03G30 Categorical logic, topoi
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amadio, R. M.; Curien, P.-L., Domains and Lambda-Calculi, Cambridge Tracts in Theoretical Computer Science, Vol. 46 (1998), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0962.03001
[2] M. Barr, Exact categories, in: M. Barr, P.A. Grillet, D.H. van Osdol (Eds.), Exact Categories and Categories of Sheaves, Lecture Notes in Mathematics, Vol. 236, Spinger, Berlin, 1971, pp. 1-120.; M. Barr, Exact categories, in: M. Barr, P.A. Grillet, D.H. van Osdol (Eds.), Exact Categories and Categories of Sheaves, Lecture Notes in Mathematics, Vol. 236, Spinger, Berlin, 1971, pp. 1-120. · Zbl 0223.18009
[3] A. Bauer, The Realizability Approach to Computable Analysis and Topology, Ph.D. Thesis, Carnegie Mellon University, 2000, available as CMU Tech. Report and at .; A. Bauer, The Realizability Approach to Computable Analysis and Topology, Ph.D. Thesis, Carnegie Mellon University, 2000, available as CMU Tech. Report and at .
[4] A. Bauer, L. Birkedal, Continuous functionals of dependent types and equilogical spaces, in: P. Clote, H. Schwichtenberg (Eds.), Computer Science Logic, 14th Ann. Conf. of the EACSL, Fischbachau, Germany, August 21-26, 2000, Lecture Notes in Computer Science, Vol. 1862, Springer, Berlin, August 2000.; A. Bauer, L. Birkedal, Continuous functionals of dependent types and equilogical spaces, in: P. Clote, H. Schwichtenberg (Eds.), Computer Science Logic, 14th Ann. Conf. of the EACSL, Fischbachau, Germany, August 21-26, 2000, Lecture Notes in Computer Science, Vol. 1862, Springer, Berlin, August 2000. · Zbl 0973.03036
[5] Berger, U., Total sets and objects in domain theory, Ann. Pure Appl. Logic, 60, 91-117 (1993) · Zbl 0776.03031
[6] U. Berger, Continuous Functionals of Dependent and Transitive Types, Habilitationsschrift, Ludwig-Maximilians-Universität München, 1997.; U. Berger, Continuous Functionals of Dependent and Transitive Types, Habilitationsschrift, Ludwig-Maximilians-Universität München, 1997.
[7] L. Birkedal, Developing theories of types and computability via realizability, Electronic Notes in Theoretical Computer Science, 34:viii+282, 2000 (book version of Ph.D. Thesis).; L. Birkedal, Developing theories of types and computability via realizability, Electronic Notes in Theoretical Computer Science, 34:viii+282, 2000 (book version of Ph.D. Thesis). · Zbl 0947.68049
[8] L. Birkedal, A general notation of realizability, in: Proc. 15th Ann. IEEE Symp. on Logic in Computer Science, Santa Barbara, CA, IEEE Computer Society, Silver Spring, MD, June 2000, pp. 7-17.; L. Birkedal, A general notation of realizability, in: Proc. 15th Ann. IEEE Symp. on Logic in Computer Science, Santa Barbara, CA, IEEE Computer Society, Silver Spring, MD, June 2000, pp. 7-17.
[9] L. Birkedal, A. Carboni, G. Rosolini, D.S. Scott, Type theory via exact categories, in: Proc. 13th Ann. IEEE Symp. on Logic in Computer Science, IEEE Computer Society, Indianapolis, Indiana, June 1998, pp. 188-198.; L. Birkedal, A. Carboni, G. Rosolini, D.S. Scott, Type theory via exact categories, in: Proc. 13th Ann. IEEE Symp. on Logic in Computer Science, IEEE Computer Society, Indianapolis, Indiana, June 1998, pp. 188-198. · Zbl 0945.03542
[10] Borceux, F., Handbook of Categorical Algebra I. Basic Category Theory, Encyclopedia of Mathematics and Its Applications, Vol. 51 (1994), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0803.18001
[11] A. Carboni, P.J. Freyd, A. Scedrov, A categorical approach to realizability and polymorphic types, in: Mathematical Foundations of Programming Semantics, Proc. New Orleans, Louisiana, Lecture Notes in Computer Science, Vol. 298, Springer, Berlin, 1988, pp. 23-42.; A. Carboni, P.J. Freyd, A. Scedrov, A categorical approach to realizability and polymorphic types, in: Mathematical Foundations of Programming Semantics, Proc. New Orleans, Louisiana, Lecture Notes in Computer Science, Vol. 298, Springer, Berlin, 1988, pp. 23-42. · Zbl 0651.18004
[12] J. Cartmell, Generalized algebraic theories and contextual categories, Ph.D. Thesis, University of Oxford, 1978.; J. Cartmell, Generalized algebraic theories and contextual categories, Ph.D. Thesis, University of Oxford, 1978.
[13] Davey, B. A.; Priestley, H. A., Introduction to Lattices and Order (1990), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0701.06001
[14] Th. Ehrhard, A categorical semantics of constructions, in: Proc. 3rd Ann. IEEE Symposium on Logic in Computer Science, Computer Society Press, Washington, 1988, pp. 264-273.; Th. Ehrhard, A categorical semantics of constructions, in: Proc. 3rd Ann. IEEE Symposium on Logic in Computer Science, Computer Society Press, Washington, 1988, pp. 264-273.
[15] Y.L. Ershov, Model C for partial continuous functionals, in: Logic Colloquium 1976, North-Holland, Amsterdam, 1977, pp. 455-467.; Y.L. Ershov, Model C for partial continuous functionals, in: Logic Colloquium 1976, North-Holland, Amsterdam, 1977, pp. 455-467.
[16] Gierz, G.; Hofmann, K. H.; Keimel, K.; Lawson, J. D.; Mislove, M.; Scott, D. S., A Compendium of Continuous Lattices (1980), Springer: Springer Berlin · Zbl 0452.06001
[17] M. Hofmann, On the interpretation of type theory in locally cartesian closed categories, in: J. Tiuryn, L. Pacholski (Eds.), Proc. of Computer Science Logic, Lecture Notes in Computer Science, Springer, Berlin, 1994.; M. Hofmann, On the interpretation of type theory in locally cartesian closed categories, in: J. Tiuryn, L. Pacholski (Eds.), Proc. of Computer Science Logic, Lecture Notes in Computer Science, Springer, Berlin, 1994.
[18] M. Hofmann, A simple model for quotient types, in: Proceedings of Typed Lamda Calculus and Applications, Lecture Notes in Computer Science, Vol. 902, Springer, Berlin, 1995 pp. 216-234.; M. Hofmann, A simple model for quotient types, in: Proceedings of Typed Lamda Calculus and Applications, Lecture Notes in Computer Science, Vol. 902, Springer, Berlin, 1995 pp. 216-234. · Zbl 1063.68602
[19] Hyland, J. M.E., The effective topos, (Troelstra, A. S.; van Dalen, D., The L.E.J. Brouwer Centenary Symp. The L.E.J. Brouwer Centenary Symp, Studies in Logic and The Foundations of Mathematics, Vol. 110 (1982), North-Holland: North-Holland Amsterdam), 165-216 · Zbl 0522.03055
[20] Hyland, J. M.E.; Johnstone, P. T.; Pitts, A. M., Tripos theory, Math. Proc. Cambridge Philos. Soc., 88, 205-232 (1980) · Zbl 0451.03027
[21] Hyland, J. M.E.; Pitts, A. M., The theory of constructions: categorical semantics and topos theoretical models, (Gray, J. W.; Scedrov, A., Categories in Computer Science and Logic. Categories in Computer Science and Logic, Contemporary Mathematics, Vol. 92 (1989), American Mathematical Society: American Mathematical Society Providence, RI), 137-199 · Zbl 0721.03048
[22] Hyland, J. M.E.; Robinson, E. P.; Rosolini, G., The discrete objects in the effective topos, Proc. London Math. Soc., 3, 60, 1-36 (1990) · Zbl 0703.18002
[23] B. Jacobs, Categorical type theory, Ph.D. Thesis, University of Nijmegen, 1991.; B. Jacobs, Categorical type theory, Ph.D. Thesis, University of Nijmegen, 1991.
[24] B. Jacobs, Quotients in simple type theory, unpublished Manuscript, available at , June 1991.; B. Jacobs, Quotients in simple type theory, unpublished Manuscript, available at , June 1991.
[25] Jacobs, B., Comprehension categories and the semantics of type dependency, Theoret. Comput. Sci., 107, 169-207 (1993) · Zbl 0804.18007
[26] Jacobs, B., Categorical Logic and Type Theory (1999), Elsevier Science: Elsevier Science Amsterdam · Zbl 0911.03001
[27] S.C. Kleene, Countable functionals, in: A. Heyting (Ed.), Constructivity in Mathematics, Proc. of the Colloquium, Amsterdam, 1957, North-Holland, Amsterdam, 1959, pp. 81-100.; S.C. Kleene, Countable functionals, in: A. Heyting (Ed.), Constructivity in Mathematics, Proc. of the Colloquium, Amsterdam, 1957, North-Holland, Amsterdam, 1959, pp. 81-100.
[28] J.R. Longley, Realizability toposes and language semantics, Ph.D. Thesis, University of Edinburgh, 1994.; J.R. Longley, Realizability toposes and language semantics, Ph.D. Thesis, University of Edinburgh, 1994.
[29] Luo, Z., Computation and Reasoning, A Type Theory for Computer Science, International Series of Monographs on Computer Science, Vol. 11 (1994), Oxford University Press: Oxford University Press Oxford · Zbl 0823.68101
[30] Moggi, E., A category theoretic account of program modules, Math. Struct. Comput. Sci., 1, 103-139 (1991) · Zbl 0747.18009
[31] E. Moggi, Metalanguages and applications, Notes for Summer School on Semantics and Logics of Computation, University of Cambridge, Isaac Newton Institute for Mathematical Sciences, September 1995.; E. Moggi, Metalanguages and applications, Notes for Summer School on Semantics and Logics of Computation, University of Cambridge, Isaac Newton Institute for Mathematical Sciences, September 1995.
[32] D. Pavlović, Predicates and fibrations, Ph.D. Thesis, University of Utrect, 1990.; D. Pavlović, Predicates and fibrations, Ph.D. Thesis, University of Utrect, 1990.
[33] W. Phoa, An introduction to fibrations, topos theory, the effective topos and modest sets, Tech. Report, University of Edinburgh, 1993.; W. Phoa, An introduction to fibrations, topos theory, the effective topos and modest sets, Tech. Report, University of Edinburgh, 1993.
[34] A.M. Pitts, Categorical logic, unpublished manuscript, available at , May 1995.; A.M. Pitts, Categorical logic, unpublished manuscript, available at , May 1995.
[35] B. Reus, Program verification in synthetic domain theory, Ph.D. Thesis, Ludwig-Maximilians-Universität München, November 1995.; B. Reus, Program verification in synthetic domain theory, Ph.D. Thesis, Ludwig-Maximilians-Universität München, November 1995. · Zbl 0869.68037
[36] Robinson, E. P.; Rosolini, G., Colimit completions and the effective topos, J. Symbolic Logic, 55, 678-699 (1990) · Zbl 0713.18003
[37] J. Rosický, Cartesian closed exact completions, available from the Hypatia Electronic Library: , 1997.; J. Rosický, Cartesian closed exact completions, available from the Hypatia Electronic Library: , 1997.
[38] D.S. Scott, A new category? unpublished manuscript, available at .; D.S. Scott, A new category? unpublished manuscript, available at .
[39] Stoltenberg-Hansen, V.; Lindström, I.; Griffor, E. R., Mathematical Theory of Domains, Cambridge Tracts in Computer Science, Vol. 22 (1994), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0828.06001
[40] P. Taylor, Recursive domains, indexed categories and polymorphism, Ph.D. Thesis, University of Cambridge, 1986.; P. Taylor, Recursive domains, indexed categories and polymorphism, Ph.D. Thesis, University of Cambridge, 1986.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.