Last Time : Using the QIIT Framework for Meta-Theoretic Reasoning on Type Theory

Our exploration will focus on how to use categorical methods for meta-theoretic reasoning.

Motivation: Why Categorical Semantics?

We have heard that “Free CCC is the syntax for Simply Typed Lambda Calculus.” To serve as syntax, it needs an eliminator so that we can reason and compute with it — defining pretty-printers, evaluators, etc. We claim the universal property of Free CCC acts as such an eliminator.

Why use this? The universal property gives an extensional, syntax-invariant characterization of data.

Consider boolean. Its universal property (non-rigorously):

Inductive boolean : Set := true : boolean | false : boolean
Definition UP_boolean :
  ∀ {R : Set}, R → R → boolean → R :=
  fun rt rf b ⇒ match b with true ⇒ rt | false ⇒ rf

(The real formulation also demands uniqueness of this morphism.)

A key insight of category theory: the universal property determines the type up to isomorphism. Suppose an arbitrary type X has the same universal property:

Axiom UP_X : ∀ {R : Set}, R → R → X → R.

Then X is isomorphic to boolean, yet X carries no concrete intensional definition. Whatever we prove about X using only UP_X ports back to boolean — and to any other type satisfying the same property. We say such reasoning is syntax-invariant.

Applied to our meta-theory: different formulations of STLC (meta-level substitution vs. explicit substitution vs. extrinsic vs. intrinsic) all satisfy the Free CCC universal property. Proving things directly about Free CCC reuses across all concrete formulations.

This extensional characterization and syntax-invariance makes categorical semantic more mathematical to some extent — and justifies why so many people want to work with categorical semantic! Instead of only about a concrete syntax, they want their meta-theorem to be more generalized.

The real question: is your concrete syntax good enough to prefer over the initial model? QIIT comes close, but there are cases QIIT cannot handle — e.g., Kavvos’s modality where a ≡ b does not imply box a ≡ box b — for which a (2-)categorical semantics still exists. The key advantage remains syntax-invariance.

Free CCC as Syntax: Why?

If a given object is to serve as syntax, we need a strong enough mapping-out arrow acting as an elimination principle, so that we can do induction on it to reason (just like with QIIT). Why does Free CCC have such an “elimination principle”?

  1. How is it defined?
  • Following Lambek 1988, we can see there is an adjunction between Free CCC and Graph, $\mathcal{F} \dashv \mathcal{U}: \mathbf{CCC} \to \mathbf{Graph}$, and the universal property is defined therein.
    • Basically, the universal property says any arrow $F: X \to U(Y)$ is (co)unit-factorized via $X \to U(F(X)) \to U(Y)$.
  • So if we generate Free CCC from the empty graph (an initial object in the Graph category), we will also obtain an initial object in the category of CCCs, due to this adjunction. This initiality should act as an elimination principle.
  • Thus once we prove a given model is a CCC, due to this initiality, we should have a unique arrow from this Free CCC to the given model, acting as an elimination principle. This should suffice to formulate the denotational semantic.

Another notion is Free SCWF.

Free SCWF

  1. Roughly, it can be considered as the data of a QIIT with an STLC signature, just as a CWF corresponds to a QIIT with an MLTT signature.
  2. In the original text, free SCWF doesn’t explicitly mention its freeness, but we do have initiality, which is enough for us to see the existence of an elimination principle.
  3. However, free SCWF can be shown to be really free.
  4. The idea is formally stated in Proposition 1.10 here.
    1. Why does the initial object of the comma category lead to the factorization?
    2. Why does the above factorization imply the object is initial in the comma category?
      1. These two hold trivially because the comma category consists of objects of the form $(c, f, R(?))$.
    3. Then Prop 1.10 holds trivially.
  5. Going back: we want to show there is an adjunction $F \dashv U : \mathbf{Set} \to \mathbf{SCwf}$. Here we know $F$ maps a base-type set $B$ to the initial object in $B$-SCwf. To show adjunction, we need to show $(B, ?, U(F(B)))$ is the initial object of the comma category $(B, ?, U(?))$.
    1. Consider the definition of $B$-SCwf — basically an SCwf with an interpretation $\llbracket \cdot \rrbracket_B : B \to Ty$. Thus each object $(C, Ty, Tm, \llbracket \cdot \rrbracket_B)$ in $B$-SCwf is an object in $(B, ?, U(?))$, of the form $(B, \llbracket \cdot \rrbracket_B, U((C, Ty, \dots)))$.
    2. So now it is clear that $F$ is the construction mentioned in Prop 4 of free SCWF.
    3. and $F \dashv U$ where $U$ simply returns the $Ty$ set of the SCWF.
  6. But syntactically, this SCWF is even weaker than CCC.

However, Free CCC / SCWF is too weak to be helpful. Basically, we cannot impose customized intro/elim rules at all. We need to use another framework (e.g., QIIT). But is QIIT “categorical” enough to be considered a proper “syntax-invariant” notion? Unknown to the author. But we do know QIIT can induce a good notion of category and morphisms, and each QIIT syntax is the initial object.

Ending Thoughts

  1. Categorical semantics/syntax is extensional and syntax-invariant, and thus more mathematical for sure.
  2. Categorical semantics/syntax is, at the end of the day, describing a bunch of equations, and thus very axiomatic.
    1. Thus it has many advantages when describing STLC, categorical logic, and dependent (algebraic) type theory, because they can easily be described in a “reduction-free” (absence of operational semantics) style.
      1. Note that these, without operational semantics (or execution behavior), are not really PL but type theory.
      2. They become PL once we have a runnable denotational interpreter.
      3. Or for dependent types, we need a normalization-by-evaluation algorithm that does type-checking and evaluation at the same time. At least we need canonicity to ensure that computation yields canonical forms.
    2. But for general-purpose PLs described using operational semantics, categorical semantics becomes a bit less useful (since they don’t really have equations, they are rather non-logical, and their definition relies on dynamic transitions).
      1. We can still have contextual equivalence in these general-purpose PLs, so category theory can still come in to help.
      2. For example, Levy’s CBPV thesis uses category theory to describe the equational theory of CBPV.
      3. But to be honest, I don’t see the advantage of using category theory in that case, because it is too axiomatic to be useful for practical CS.
      4. And contextual equivalence still requires operational semantics as the “root of evidence” for the equations in category theory — so how does categorical semantics help?
      5. But truly, Levy did find some adjunction models in this context for his CBPV model, so it is possible to bring insight.
      6. In these cases, I would suggest turning to denotational semantics, then polishing the denotational equality back into categorical semantics.
  3. To summarize: a. If a system requires equations from the very beginning (like dependent type theory), or the developer cares greatly about the equational theory, and it has a strong logical flavor — there is no reason to be against categorical semantics. b. If a system is described from the beginning in a dynamic style (very operational) without a clear idea of contextual equivalence from the start, then the definition of categorical semantics is harder to come by a priori.
  4. The topic of categorical semantics, or categorical logic, is mainly about finding theory-model equivalences. (See Levy’s adjunction models for Call-by-Push-Value with stacks.) The gluing model (roughly the model used to prove canonicity/termination) and presheaf models should be situated here.