research-article

Open access

Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure

Authors:

Philip SavilleAuthors Info & Claims

LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 425 - 439

https://doi.org/10.1145/3373718.3394769

Published: 08 July 2020 Publication History

Abstract

We present two proofs of coherence for cartesian closed bicategories. Precisely, we show that in the free cartesian closed bicategory on a set of objects there is at most one structural 2-cell between any parallel pair of 1-cells. We thereby reduce the difficulty of constructing structure in arbitrary cartesian closed bicategories to the level of 1-dimensional category theory. Our first proof follows a traditional approach using the Yoneda lemma. For the second proof, we adapt Fiore's categorical analysis of normalisation-by-evaluation for the simply-typed lambda calculus. Modulo the construction of suitable bicategorical structures, the argument is not significantly more complex than its 1-categorical counterpart. It also opens the way for further proofs of coherence using (adaptations of) tools from categorical semantics.

References

[1]

M. G. Abbott. 2003. Categories of containers. Ph.D. Dissertation. University of Leicester.

[2]

A. Abel, T. Coquand, and P. Dybjer. 2007. Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements. In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS '07). IEEE Computer Society, Washington, DC, USA, 3--12. https://doi.org/10.1109/LICS.2007.33

Digital Library

[3]

D. Ahman and S. Staton. 2013. Normalization by Evaluation and Algebraic Effects. Electronic Notes in Theoretical Computer Science (ENTCS) 298 (2013), 51--69.

Digital Library

[4]

M. Alimohamed. 1995. A Characterization of Lambda Definability in Categorical Models of Implicit Polymorphism. Theor. Comput. Sci. 146, 1-2 (July 1995), 5--23. https://doi.org/10.1016/0304-3975(94)00283-O

Digital Library

[5]

T. Altenkirch, P. Dybjer, M. Hofmannz, and P. Scott. 2001. Normalization by Evaluation for Typed Lambda Calculus with Coproducts. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01). IEEE Computer Society, Washington, DC, USA, 303-. http://dl.acm.org/citation.cfm?id=871816.871869

[6]

T. Altenkirch, M. Hofmann, and T. Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science, 6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995, Proceedings, Vol. 953. 182--199.

[7]

T. Altenkirch and A. Kaposi. 2016. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) (Leibniz International Proceedings in Informatics (LIPIcs)), D. Kesner and B. Pientka (Eds.), Vol. 52. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 6:1--6:16. https://doi.org/10.4230/LIPIcs.FSCD.2016.6

[8]

T. Altenkirch and A. Kaposi. 2017. Normalisation by Evaluation for Type Theory, in Type Theory. Logical Methods in Computer Science Volume 13, Issue 4 (Oct. 2017). https://doi.org/10.23638/LMCS-13(4:1)2017

[9]

S. Awodey. 2010. Category Theory (2nd ed.). Number 52 in Oxford Logic Guides. Oxford University Press.

[10]

V. Balat, R. Di Cosmo, and M. Fiore. 2004. Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Venice, Italy) (POPL '04). Association for Computing Machinery, New York, NY, USA, 64--76. https://doi.org/10.1145/964001.964007

[11]

J.Bénabou. 1967. Introduction to bicategories. In Reports of the Midwest Category Seminar. Springer Berlin Heidelberg, Berlin, Heidelberg, 1--77. https://doi.org/10.1007/BFb0074299

[12]

U. Berger and H. Schwichtenberg. 1991. An inverse of the evaluation functional for typed lambda-calculus. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science (LICS '91). 203--211. https://doi.org/10.1109/LICS.1991.151645

[13]

F. Borceux. 1994. Bicategories and distributors. Encyclopedia of Mathematics and its Applications, Vol. 1. Cambridge University Press, 281--324. https://doi.org/10.1017/CBO9780511525858.009

[14]

A. Carboni, G. M. Kelly, R. F. C. Walters, and R.J. Wood. 2008. Cartesian bicategories II. Theory and Applications of Categories 19, 6 (2008), 93--124. http://www.tac.mta.ca/tac/volumes/19/6/19-06abs.html

[15]

A. Carboni, S. Lack, and R. F. C. Walters. 1993. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra 84, 2 (Feb. 1993), 145--158. https://doi.org/10.1016/0022-4049(93)90035-r

[16]

A. Carboni and R. F. C. Walters. 1987. Cartesian bicategories I. Journal of Pure and Applied Algebra 49, 1 (1987), 11--32. https://doi.org/10.1016/0022-4049(87)90121-6

[17]

S. Castellan, P. Clairambault, S. Rideau, and G. Winskel. 2017. Games and Strategies as Event Structures. Logical Methods in Computer Science 13 (2017).

[18]

T. Coquand and P. Dybjer. 1997. Intuitionistic Model Constructions and Normalization Proofs. Mathematical. Structures in Comp. Sci. 7, 1 (Feb. 1997), 75--94. https://doi.org/10.1017/S0960129596002150

[19]

R. L. Crole. 1994. Categories for Types. Cambridge University Press. https://doi.org/10.1017/CBO9781139172707

[20]

D. Čubrić, P. Dybjer, and P. Scott. 1998. Normalization and the Yoneda embedding. Mathematical Structures in Computer Science 8, 2 (1998), 153--192. https://doi.org/10.1017/S0960129597002508

Digital Library

[21]

P-E. Dagand and C. McBride. 2013. A Categorical Treatment of Ornaments. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '13). IEEE Computer Society, Washington, DC, USA, 530--539. https://doi.org/10.1109/LICS.2013.60

[22]

B. Day. 1970. On closed categories of functors. In Reports of the Midwest Category Seminar IV, S. Mac Lane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, and S. Swierczkowski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1--38. https://doi.org/10.1007/BFb0060438

[23]

B. Day and R. Street. 1997. Monoidal Bicategories and Hopf Algebroids. Advances in Mathematics 129, 1 (1997), 99--157. https://doi.org/10.1006/aima.1997.1649

[24]

M. Fiore. 2002. 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 (Pittsburgh, PA, USA) (PPDP '02). ACM, New York, NY, USA, 26--37. https://doi.org/10.1145/571157.571161

Digital Library

[25]

M. Fiore. 2011. Algebraic Foundations for Type Theories. 18th Types for Proofs and Programs workshop. Slides available at https://www.cl.cam.ac.uk/~mpf23/talks/Types2011.pdf.

[26]

M. Fiore. 2016. An Algebraic Combinatorial Approach to Opetopic Structure. https://www.mpim-bonn.mpg.de/node/6586. Talk at the Seminar on Higher Structures, Program on Higher Structures in Geometry and Physics, Max Planck Institute for Mathematics, Bonn (Germany).

[27]

M. Fiore, N. Gambino, M. Hyland, and G. Winskel. 2007. The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society 77, 1 (2007), 203--220. https://doi.org/10.1112/jlms/jdm096

[28]

M. Fiore, N. Gambino, M. Hyland, and G. Winskel. 2017. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica New Series 24 (2017), 2791--2830. https://doi.org/10.1007/s00029-017-0361-3

[29]

M. Fiore and A. Joyal. 2015. Theory of para-toposes. Talk at the Category Theory 2015 Conference. Departamento de Matematica, Universidade de Aveiro (Portugal).

[30]

M. Fiore, G. Plotkin, and D. Turi. 1999. Abstract Syntax and Variable Binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS '99). IEEE Computer Society, Washington, DC, USA, 193-. http://dl.acm.org/citation.cfm?id=788021.788948

[31]

M. Fiore and P. Saville. 2017. List Objects with Algebraic Structure. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK. 16:1--16:18. https://doi.org/10.4230/LIPIcs.FSCD.2017.16

[32]

M. Fiore and P. Saville. 2019. A type theory for cartesian closed bicategories. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '19). https://doi.org/10.1109/LICS.2019.8785708

[33]

M. Fiore and P. Saville. 2020. Relative Full Completeness for Bicategorical Cartesian Closed Structure. In Foundations of Software Science and Computation Structures, J. Goubault-Larrecq and B. König (Eds.). Springer International Publishing, Cham., 277--298. https://doi.org/10.1007/978-3-030-45231-5_15

[34]

T. Fiore. 2006. Pseudo limits, biadjoints, and pseudo algebras: categorical foundations of conformal field theory. Memoirs of the AMS, Vol. 860. American Mathematical Society.

[35]

S. Forest and S. Mimram. 2018. Coherence of Gray Categories via Rewriting. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD '18) (Leibniz International Proceedings in Informatics (LIPIcs)), H. Kirchner (Ed.), Vol. 108. 15:1--15:16. https://doi.org/10.4230/LIPIcs.FSCD.2018.15

[36]

N. Gambino and A. Joyal. 2017. On operads, bimodules and analytic functors. Memoirs of the AMS, Vol. 249. American Mathematical Society.

[37]

N. Gambino and J. Kock. 2013. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society 154, 1 (2013), 153--192. https://doi.org/10.1017/S0305004112000394

[38]

J.-Y. Girard. 1972. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Ph.D. Dissertation. Université Paris Diderot - Paris 7.

[39]

J.-Y. Girard, P. Taylor, and Y. Lafont. 1989. Proofs and Types. Cambridge University Press, New York, NY, USA.

[40]

G.L. Cattani, M. Fiore, and G. Winskel. 1998. A theory of recursive domains with applications to concurrency. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS '98). IEEE Computer Society, 214--225. https://doi.org/10.1109/LICS.1998.705658

[41]

R. Gordon, A. J. Power, and R. Street. 1995. Coherence for tricategories. Memoirs of the AMS, Vol. 558. American Mathematical Society.

[42]

J. W. Gray. 1974. Formal Category Theory: Adjointness for 2-Categories. Lecture Notes in Mathematics, Vol. 391. Springer. https://doi.org/10.1007/BFb0061280

[43]

N. Gurski. 2013. Coherence in Three-Dimensional Category Theory. Cambridge University Press. https://doi.org/10.1017/CBO9781139542333

[44]

B.P. Hilken. 1996. Towards a proof theory of rewriting: the simply typed 2λ-calculus. Theoretical Computer Science 170, 1 (1996), 407--444. https://doi.org/10.1016/S0304-3975(96)80713-4

Digital Library

[45]

T. Hirschowitz. 2013. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science 9 (Sept. 2013), 1--22. https://doi.org/10.2168/LMCS-9(3:10)2013

[46]

R. Houston. 2007. Linear Logic without Units. Ph.D. Dissertation. University of Manchester.

[47]

A. Joyal and R. Street. 1993. Braided tensor categories. Advances in Mathematics 102, 1 (11 1993), 20--78. https://doi.org/10.1006/aima.1993.1055

[48]

S. Lack. 2010. A 2-Categories Companion. Springer New York, New York, NY, 105--191. https://doi.org/10.1007/978-1-4419-1524-5_4

[49]

S. Lack, R. F. C. Walters, and R. J. Wood. 2010. Bicategories of spans as cartesian bicategories. Theory and Applications of Categories 24, 1 (2010), 1--24. http://www.tac.mta.ca/tac/volumes/24/1/24-01.pdf

[50]

J. Lambek and P. J. Scott. 1986. Introduction to Higher Order Categorical Logic. Cambridge University Press, New York, NY, USA.

[51]

T. Leinster. 1998. Basic Bicategories. (May 1998). Available at https://arxiv.org/abs/math/9810017.

[52]

T. Leinster. 2004. Higher operads, higher categories. Number 298 in London Mathematical Society Lecture Note Series. Cambridge University Press.

[53]

Q. M. Ma and J. C. Reynolds. 1992. Types, abstraction, and parametric polymorphism, part 2. In Mathematical Foundations of Programming Semantics, S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1--40.

[54]

S. Mac Lane. 1963. Natural associativity and commutativity. Rice University Studies (1963). https://hdl.handle.net/1911/62865

[55]

S. Mac Lane. 1998. Categories for the Working Mathematician (second ed.). Graduate Texts in Mathematics, Vol. 5. Springer-Verlag New York. https://doi.org/10.1007/978-1-4757-4721-8

[56]

S. Mac Lane and R. Paré. 1985. Coherence for bicategories and indexed categories. Journal of Pure and Applied Algebra 37 (1985), 59--80. https://doi.org/10.1016/0022-4049(85)90087-8

[57]

M. Makkai. 1996. Avoiding the axiom of choice in general category theory. Journal of Pure and Applied Algebra 108, 2 (1996), 109--173. https://doi.org/10.1016/0022-4049(95)00029-1

[58]

Federico Olimpieri. 2020. Intersection Type Distributors. arXiv (2020). arXiv:2002.01287v2 [cs.LO]

[59]

J. Ouaknine. 1997. A two-dimensional extension of Lambek's categorical proof theory. Master's thesis. McGill University. http://digitool.library.mcgill.ca/R/?func=dbin-jump-full&object_id=20277&local_base=GEN01-MCG02

[60]

H. Paquet. 2020. Probabilistic concurrent game semantics. Ph.D. Dissertation. University of Cambridge.

[61]

A. M. Pitts. 1987. An elementary calculus of approximations (extended abstract). (1987). Unpublished manuscript, University of Sussex, December 1987.

[62]

A. M. Pitts. 2000. Categorical Logic. In Handbook of Logic in Computer Science. Oxford University Press, Oxford, UK, Chapter 2, 39--123. http://dl.acm.org/citation.cfm?id=373919.373928

Digital Library

[63]

A. J. Power. 1989. Coherence for Bicategories with Finite Bilimits I. In Categories in Computer Science and Logic: Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference Held June 14-20, 1987 with Support from the National Science Foundation, J. W. Gray and A. Scedrov (Eds.). Vol. 92. American Mathematical Society, 341--349.

[64]

A. J. Power. 1989. A general coherence result. Journal of Pure and Applied Algebra 57, 2 (1989), 165--173. https://doi.org/10.1016/0022-4049(89)90113-8

[65]

E. Ritter and V. de Paiva. 1997. On explicit substitutions and names (extended abstract). In Automata, Languages and Programming, P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 248--258. https://doi.org/10.1007/3-540-63165-8_182

[66]

P. Saville. forthcoming. Cartesian closed bicategories: type theory and coherence. Ph.D. Dissertation. University of Cambridge.

[67]

R. A. G. Seely. 1987. Modelling computations: a 2-categorical framework. In Proceedings of the 2nd Annual IEEE Symp. on Logic in Computer Science (LICS '87) (Ithaca, NY, USA), D. Gries (Ed.). IEEE Computer Society Press, 65--71.

[68]

R. Statman. 2014. Near semi-rings and lambda calculus. In Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, G. Dowek (Ed.). Springer International Publishing, Cham., 410--424. https://doi.org/10.1007/978-3-319-08918-8_28

[69]

S. Staton. 2013. An algebraic presentation of predicate logic. In Foundations of Software Science and Computation Structures, F. Pfenning (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 401--417. https://doi.org/10.1007/978-3-642-37075-5_26

[70]

R. Street. 1972. The formal theory of monads. Journal of Pure and Applied Algebra 2, 2 (1972), 149--168. https://doi.org/10.1016/0022-4049(72)90019-9

[71]

R. Street. 1980. Fibrations in bicategories. Cahiers de Topologie et Géométrie Différentielle Catégoriques 21, 2 (1980), 111--160. http://eudml.org/doc/91227

[72]

R. Street. 1995. Categorical Structures. In Handbook of Algebra, M. Hazewinkel (Ed.). Vol. 1. Elsevier, Chapter 15, 529--577. http://maths.mq.edu.au/~street/45.pdf

[73]

W. Tait. 1967. Intensional Interpretations of Functionals of Finite Type I. The Journal of Symbolic Logic 32, 2 (1967), 198--212. http://www.jstor.org/stable/2271658

[74]

T. Uustalu. 2014. Coherence for Skew-Monoidal Categories. Electronic Proceedings in Theoretical Computer Science 153 (June 2014). https://doi.org/10.4204/EPTCS.153.5

Cited By

Kerinec AManzonetto GOlimpieri F(2023)Why Are Proofs Relevant in Proof-Relevant Models?Proceedings of the ACM on Programming Languages10.1145/35712017:POPL(218-248)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571201
Galal Z(2023)Fixpoint operators for 2-categorical structures2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175688(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175688
Olimpieri FGorla D(2021)Intersection type distributorsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470617(1-15)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470617
Show More Cited By

Index Terms

Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure
1. Theory of computation
  1. Logic
    1. Type theory
  2. Semantics and reasoning
    1. Program semantics
      1. Categorical semantics

Recommendations

Relative Full Completeness for Bicategorical Cartesian Closed Structure
Foundations of Software Science and Computation Structures
Abstract
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 ...
A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions

We present a simply-typed λ-calculus with explicit substitutions and we give a fully formalised proof of its soundness and completeness with respect to Kripke models. We further give conversion rules for the calculus and show also for them that they are ...
Observationally-induced Effects in Cartesian Closed Categories

Alex Simpson has suggested an observationally-induced approach towards obtaining monads for computational effects in denotational semantics. The underlying idea of this approach is to use a single observation algebra as computational prototype and to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

July 2020

986 pages

ISBN:9781450371049

DOI:10.1145/3373718

Conference Chairs:
Holger Hermanns,
Lijun Zhang,
Naoki Kobayashi,
General Chair:
Dale Miller

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 July 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

LICS '20

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science

July 8 - 11, 2020

Saarbrücken, Germany

Acceptance Rates

LICS '20 Paper Acceptance Rate 69 of 174 submissions, 40%;

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
361
Total Downloads

Downloads (Last 12 months)96
Downloads (Last 6 weeks)12

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kerinec AManzonetto GOlimpieri F(2023)Why Are Proofs Relevant in Proof-Relevant Models?Proceedings of the ACM on Programming Languages10.1145/35712017:POPL(218-248)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571201
Galal Z(2023)Fixpoint operators for 2-categorical structures2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175688(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175688
Olimpieri FGorla D(2021)Intersection type distributorsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470617(1-15)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470617
Fiore MSaville P(2021)Coherence for bicategorical cartesian closed structureMathematical Structures in Computer Science10.1017/S0960129521000281(1-28)Online publication date: 18-Oct-2021
https://doi.org/10.1017/S0960129521000281
Fiore MSaville P(2020)Relative Full Completeness for Bicategorical Cartesian Closed StructureFoundations of Software Science and Computation Structures10.1007/978-3-030-45231-5_15(277-298)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45231-5_15

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents