×

Relative full completeness for bicategorical Cartesian closed structure. (English) Zbl 07250943

Goubault-Larrecq, Jean (ed.) et al., Foundations of software science and computation structures. 23rd international conference, FOSSACS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12077, 277-298 (2020).
Summary: The glueing construction, defined as a certain comma category, is an important tool for reasoning about type theories, logics, and programming languages. Here we extend the construction to accommodate “2-dimensional theories” of types, terms between types, and rewrites between terms. Taking bicategories as the semantic framework for such systems, we define the glueing bicategory and establish a bicategorical version of the well-known construction of Cartesian closed structure on a glueing category. As an application, we show that free finite-product bicategories are fully complete relative to free cartesian closed bicategories, thereby establishing that the higher-order equational theory of rewriting in the simply-typed lambda calculus is a conservative extension of the algebraic equational theory of rewriting in the fragment with finite products only.
For the entire collection see [Zbl 1440.68008].

MSC:

68Nxx Theory of software
68Qxx Theory of computing
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abbott, M.G.: Categories of containers. Ph.D. thesis, University of Leicester (2003) · Zbl 1029.68096
[2] Abramsky, S., Jagadeesan, R.: Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic 59(2), 543-574 (1994). doi:10.2307/2275407 · Zbl 0822.03007
[3] Alimohamed, M.: A characterization of lambda definability in categorical models of implicit polymorphism. Theoretical Computer Science 146(1-2), 5-23 (1995). doi:10.1016/0304-3975(94)00283-O · Zbl 0873.68015
[4] Balat, V., Di Cosmo, R., Fiore, M.: Extensional normalisation and typed-directed partial evaluation for typed lambda calculus with sums. In: Proceedings of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 64-76 (2004) · Zbl 1325.68045
[5] Bénabou, J.: Introduction to bicategories. In: Reports of the Midwest Category Seminar. pp. 1-77. Springer Berlin Heidelberg, Berlin, Heidelberg (1967) · Zbl 1375.18001
[6] Bloom, S.L., Ésik, Z., Labella, A., Manes, E.G.: Iteration 2-theories. Applied Categorical Structures 9(2), 173-216 (2001). doi:10.1023/a:1008708924144 · Zbl 0981.18005
[7] Borceux, F.: Bicategories and distributors, Encyclopedia of Mathematics and its Applications, vol. 1, pp. 281-324. Cambridge University Press (1994). doi:10.1017/CBO9780511525858.009 · Zbl 0843.18001
[8] Carboni, A., Kelly, G.M., Walters, R.F.C., Wood, R.J.: Cartesian bicategories II. Theory and Applications of Categories 19(6), 93-124 (2008), http://www.tac.mta.ca/tac/volumes/19/6/19-06abs.html · Zbl 1146.18300
[9] Carboni, A., Lack, S., Walters, R.F.C.: Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra 84(2), 145-158 (1993). doi:10.1016/0022-4049(93)90035-r · Zbl 0784.18001
[10] Carboni, A., Walters, R.F.C.: Cartesian bicategories I. Journal of Pure and Applied Algebra 49(1), 11-32 (1987). doi:10.1016/0022-4049(87)90121-6 · Zbl 0637.18003
[11] Castellan, S., Clairambault, P., Rideau, S., Winskel, G.: Games and strategies as event structures. Logical Methods in Computer Science 13 (2017) · Zbl 1459.68111
[12] Crole, R.L.: Categories for Types. Cambridge University Press (1994). doi:10.1017/CBO9781139172707 · Zbl 0837.68077
[13] Dagand, P.E., McBride, C.: A categorical treatment of ornaments. In: Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 530-539. IEEE Computer Society, Washington, DC, USA (2013). doi:10.1109/LICS.2013.60 · Zbl 1366.68021
[14] Fiore, M.: Axiomatic Domain Theory in Categories of Partial Maps. Distinguished Dissertations in Computer Science, Cambridge University Press (1996) · Zbl 0979.68549
[15] Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. pp. 26-37. ACM, New York, NY, USA (2002). doi:10.1145/571157.571161
[16] Fiore, M., Di Cosmo, R., Balat, V.: Remarks on isomorphisms in typed lambda calculi with empty and sum types. In: Proceedings of the 28th Annual IEEE Symposium on Logic in Computer Science. pp. 147-156. IEEE Computer Society Press (2002). doi:10.1109/LICS.2002.1029824 · Zbl 1099.03011
[17] Fiore, M., Gambino, N., Hyland, M., Winskel, G.: The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society 77(1), 203-220 (2007). doi:10.1112/jlms/jdm096 · Zbl 1137.18003
[18] Fiore, M., Gambino, N., Hyland, M., Winskel, G.: Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica New Series (2017) · Zbl 1427.18012
[19] Fiore, M., Joyal, A.: Theory of para-toposes. Talk at the Category Theory 2015 Conference. Departamento de Matematica, Universidade de Aveiro (Portugal)
[20] Fiore, M., Saville, P.: A type theory for cartesian closed bicategories. In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (2019). doi:10.1109/LICS.2019.8785708
[21] Fiore, M., Saville, P.: Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure. Preprint (2020) · Zbl 1498.18030
[22] Fiore, M., Simpson, A.: Lambda definability with sums via Grothendieck logical relations. In: Girard, J.Y. (ed.) Typed lambda calculi and applications: 4th international conference. pp. 147-161. Springer Berlin Heidelberg, Berlin, Heidelberg (1999) · Zbl 0929.18004
[23] Freyd, P.: Algebraically complete categories. In: Lecture Notes in Mathematics, pp. 95-104. Springer Berlin Heidelberg (1991). doi:10.1007/bfb0084215 · Zbl 0815.18005
[24] Freyd, P.J., Scedrov, A.: Categories, Allegories. Elsevier North Holland (1990) · Zbl 0698.18002
[25] Gambino, N., Joyal, A.: On operads, bimodules and analytic functors. Memoirs of the American Mathematical Society 249(1184), 153-192 (2017) · Zbl 1393.18007
[26] Gambino, N., Kock, J.: Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society 154(1), 153-192 (2013). doi:10.1017/S0305004112000394 · Zbl 1278.18013
[27] Ghani, N.: Adjoint rewriting. Ph.D. thesis, University of Edinburgh (1995)
[28] Gibbons, J.: Conditionals in distributive categories. Tech. rep., University of Oxford (1997)
[29] G.L. Cattani, Fiore, M., Winskel, G.: A theory of recursive domains with applications to concurrency. In: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science. pp. 214-225. IEEE Computer Society (1998) · Zbl 0945.68521
[30] Gurski, N.: An Algebraic Theory of Tricategories. University of Chicago, Department of Mathematics (2006)
[31] Hasegawa, M.: Logical predicates for intuitionistic linear type theories. In: Girard, J.Y. (ed.) Typed lambda calculi and applications: 4th international conference. pp. 198-213. Springer Berlin Heidelberg, Berlin, Heidelberg (1999) · Zbl 0931.03036
[32] Hilken, B.: Towards a proof theory of rewriting: the simply typed \(2 \lambda \)-calculus. Theoretical Computer Science 170(1), 407-444 (1996). doi:10.1016/S0304-3975(96)80713-4 · Zbl 0874.03017
[33] Hirschowitz, T.: Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science 9, 1-22 (2013) · Zbl 1272.68184
[34] Jay, C.B., Ghani, N.: The virtues of eta-expansion. Journal of Functional Programming 5(2), 135-154 (1995). doi:10.1017/S0956796800001301 · Zbl 0833.68072
[35] Johann, P., Polonsky, P.: Higher-kinded data types: Syntax and semantics. In: 34th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE (2019). doi:10.1109/lics.2019.8785657
[36] Jung, A., Tiuryn, J.: A new characterization of lambda definability. In: Bezem, M., Groote, J.F. (eds.) Typed Lambda Calculi and Applications. pp. 245-257. Springer Berlin Heidelberg, Berlin, Heidelberg (1993) · Zbl 0795.03021
[37] Lack, S.: A 2-Categories Companion, pp. 105-191. Springer New York, New York, NY (2010) · Zbl 1223.18003
[38] Lack, S., Walters, R.F.C., Wood, R.J.: Bicategories of spans as cartesian bicategories. Theory and Applications of Categories 24(1), 1-24(2010) · Zbl 1315.18003
[39] Lafont, Y.: Logiques, catégories et machines. Ph.D. thesis, UniversitéParis VII (1987)
[40] Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge University Press, New York, NY, USA (1986) · Zbl 0596.03002
[41] Leinster, T.: Basic bicategories (May 1998), https://arxiv.org/pdf/math/9810017.pdf
[42] Leinster, T.: Higher operads, higher categories. No. 298 in London Mathematical Society Lecture Note Series, Cambridge University Press (2004) · Zbl 1160.18001
[43] Ma, Q.M., Reynolds, J.C.: Types, abstraction, and parametric polymorphism, part 2. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) Mathematical Foundations of Programming Semantics. pp. 1-40. Springer Berlin Heidelberg, Berlin, Heidelberg (1992)
[44] Mac Lane, S.: Categories for the Working Mathematician, Graduate Texts in Mathematics, vol. 5. Springer-Verlag New York, second edn. (1998). doi:10.1007/978-1-4757-4721-8 · Zbl 0906.18001
[45] Mac Lane, S., Paré, R.: Coherence for bicategories and indexed categories. Journal of Pure and Applied Algebra 37, 59-80 (1985). doi:10.1016/0022-4049(85)90087-8 · Zbl 0567.18003
[46] Marmolejo, F., Wood, R.J.: Kan extensions and lax idempotent pseudomonads. Theory and Applications of Categories 26(1), 1-29 (2012) · Zbl 1254.18005
[47] Mitchell, J.C., Scedrov, A.: Notes on sconing and relators. In: Börger, E.,J., G., Kleine Büning, H., Martini, S., Richter, M.M. (eds.) Computer Science Logic. pp. 352-378. Springer Berlin Heidelberg, Berlin, Heidelberg (1993) · Zbl 0795.03100
[48] Ouaknine, J.: A two-dimensional extension of Lambek’s categorical proof theory. Master’s thesis, McGill University (1997)
[49] Paquet, H.: Probabilistic concurrent game semantics. Ph.D. thesis, University of Cambridge (2020)
[50] Plotkin, G.D.: Lambda-definability and logical relations. Tech. rep., University of Edinburgh School of Artificial Intelligence (1973), memorandum SAI-RM-4
[51] Power, A.J.: An abstract formulation for rewrite systems. In: Pitt, D.H., Rydeheard, D.E., Dybjer, P., Pitts, A.M., Poigné, A. (eds.) Category Theory and Computer Science. pp. 300-312. Springer Berlin Heidelberg, Berlin, Heidelberg (1989) · Zbl 1493.68178
[52] Power, A.J.: Coherence for bicategories with finite bilimits I. In: Gray, J.W., Scedrov, A. (eds.) Categories in Computer Science and Logic: Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference, vol. 92, pp. 341-349. AMS (1989) · Zbl 0677.18006
[53] Power, A.J.: A general coherence result. Journal of Pure and Applied Algebra 57(2), 165-173 (1989). doi:10.1016/0022-4049(89)90113-8 · Zbl 0668.18010
[54] Rydeheard, D.E., Stell, J.G.: Foundations of equational deduction: A categorical treatment of equational proofs and unification algorithms. In: Pitt, D.H., Poigné, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. pp. 114-139. Springer Berlin Heidelberg, Berlin, Heidelberg (1987) · Zbl 0664.03041
[55] Saville, P.: Cartesian closed bicategories: type theory and coherence. Ph.D. thesis, University of Cambridge (Submitted) · Zbl 1498.18030
[56] Seely, R.A.G.: Modelling computations: A 2-categorical framework. In: Gries, D.(ed.) Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science. pp. 65-71. IEEE Computer Society Press (June 1987)
[57] Statman, R.: Logical relations and the typed \(\lambda \)-calculus. Information and Control 65, 85-97 (1985) · Zbl 0594.03006
[58] Stell, J.: Modelling term rewriting systems by sesqui-categories. In: Proc. Catégories, Algèbres, Esquisses et Néo-Esquisses (1994)
[59] Street, R.: Fibrations in bicategories. Cahiers de Topologie et Géométrie Différentielle Catégoriques 21(2), 111-160 (1980), https://eudml.org/doc/91227
[60] Street, R.: Categorical structures. In: Hazewinkel, M. (ed.) Handbook of Algebra, vol. 1, chap. 15, pp. 529-577. Elsevier (1995) · Zbl 0854.18001
[61] Tabareau, N.: Aspect oriented programming: A language for 2-categories. In: Proceedings of the 10th International Workshop on Foundations of Aspect-oriented Languages. pp. 13-17. ACM, New York, NY, USA (2011).doi:10.1145/1960510.1960514
[62] Taylor, P.: Practical Foundations of Mathematics, Cambridge Studies in Advanced Mathematics, vol. 59. Cambridge University Press (1999) · Zbl 0939.18001
[63] Troelstra, A.S., Schwichtenberg, H.: Basic proof theory. No. 43 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, second edn. (2000) · Zbl 0957.03053
[64] Verity, D.: Enriched categories, internal categories and change of base. Ph.D. thesis, University of Cambridge (1992), TAC reprint available at http://www.tac.mta.ca/tac/reprints/articles/20/tr20abs.html · Zbl 1254.18001
[65] Weber, M.: Yoneda structures from 2-toposes. Applied Categorical Structures 15(3), 259-323 (2007). doi:10.1007/s10485-007-9079-2 · Zbl 1125.18001
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.