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

Marcelo P. Fiore, Philip Saville · LICS · 2020 · category-theory metatheory · DOI
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.

Cite
Cite as @fiore_saville_2020 (helia, typst) · \cite{fiore_saville_2020} (LaTeX)
BibTeX
bibtex · 1 line
@inproceedings{fiore_saville_2020, series={LICS ’20}, title={Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure}, url={http://dx.doi.org/10.1145/3373718.3394769}, DOI={10.1145/3373718.3394769}, booktitle={Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science}, publisher={ACM}, author={Fiore, Marcelo and Saville, Philip}, year={2020}, month=jul, pages={425–439}, collection={LICS ’20} }
hayagriva YAML (typst)
yaml · 18 lines
fiore_saville_2020:
  type: article
  title: Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure
  author:
  - Fiore, Marcelo
  - Saville, Philip
  date: 2020-07
  page-range: 425-439
  url: http://dx.doi.org/10.1145/3373718.3394769
  serial-number:
    doi: 10.1145/3373718.3394769
  parent:
    type: proceedings
    title: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
    publisher: ACM
    parent:
      type: proceedings
      title: LICS ’20
Download: fiore_saville_2020.bib · fiore_saville_2020.yml
Cited by (1)

Coherence for bicategorical cartesian closed structure fiore-2021-coherenceMSCS · 2021
We prove a strictification theorem for cartesian closed bicategories. First, we adapt Power’s proof of coherence for bicategories with finite bilimits to show that every bicategory with bicategorical cartesian closed structure is biequivalent to a 2-category with 2-categorical cartesian closed structure. Then we show how to extend this result to a Mac Lane-style “all pasting diagrams commute” coherence theorem: precisely, we show that in the free cartesian closed bicategory on a graph, there is at most one 2-cell between any parallel pair of 1-cells. The argument we employ is reminiscent of that used by Čubrić, Dybjer, and Scott to show normalisation for the simply-typed lambda calculus (Čubrić et al., 1998). The main results first appeared in a conference paper (Fiore and Saville, 2020) but for reasons of space many details are omitted there; here we provide the full development.
DOI
Cites 67 works (6 here)
With notes (6)

Semantic analysis of normalisation by evaluation for typed lambda calculus fiore-2022-semanticMSCS · 2022
This paper studies normalisation by evaluation for typed lambda calculus from a categorical and algebraic viewpoint. The first part of the paper analyses the lambda definability result of Jung and Tiuryn via Kripke logical relations and shows how it can be adapted to unify definability and normalisation, yielding an extensional normalisation result. In the second part of the paper, the analysis is refined further by considering intensional Kripke relations (in the form of Artin–Wraith glueing) and shown to provide a function for normalising terms, casting normalisation by evaluation in the context of categorical glueing. The technical development includes an algebraic treatment of the syntax and semantics of the typed lambda calculus that allows the definition of the normalisation function to be given within a simply typed metatheory. A normalisation-by-evaluation program in a dependently typed functional programming language is synthesised.
DOI · arXiv

Normalization and the Yoneda embedding NormalizationAndTheYonedaEmbeddingMSCS · 1998
We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is 𝒫-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of 𝒫-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no use of traditional proof-theoretic or rewriting techniques. To show the robustness of our method, we give an extended treatment for more general λ-theories in the Appendix.
DOI

A general coherence result power_1989JPAA · 1989

Introduction to Higher-Order Categorical Logic lambek_scott_19861986
Web

Normalization by evaluation for typed lambda calculus with coproducts altenkirch_etal_ndLICS
Solves the decision problem for the simply typed lambda calculus with a strong binary sum, or, equivalently, the word problem for free Cartesian closed categories with binary co-products. Our method is based on the semantic technique known as “normalization by evaluation”, and involves inverting the interpretation of the syntax in a suitable sheaf model and, from this, extracting an appropriate unique normal form. There is no rewriting theory involved and the proof is completely constructive, allowing program extraction from the proof.
DOI

Abstract syntax and variable binding fiore_etal_ndLICS
We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one; besides compositionality, it automatically verifies the semantic substitution lemma.
DOI
External (61)
fiore_saville_2020 reference entries/refs/fiore_saville_2020/fiore_saville_2020.hel