Last Time : Use QIIT Framework for meta-theory reasoning on Type Theory

Our exploration will focus on how to use categorical method to do meta-theory reasoning.

But first,

Motivation : Why Categorical Semantic (and Syntax)?

For example, we heard that “Free CCC is the syntax for Simply Typed Lambda Calculus”.

To be a syntax, it is at least need to be equipped with an eliminator, like QIIT type, so that user can do reasoning/computation about it – like defining pretty printer and evaluators on it. We claim that the universal property of Free CCC can act like an eliminator.

Even if CCC does equip the universal property to do all kinds of reasoning and computation. What is the motivation of doing so, instead of using our former way of QIIT framework?

The reason is mainly due to the fact that, universal property gives an extensional(syntax-invariant) characteristic of data.

For example, let’s say the eliminator of boolean is the universal property for boolean. Here we (in a irrigorous way) formulate the intensional(concrete computational) information of the universal property.

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

Note that, the real formulation universal property is more extensional, (i.e. there should be a unique morphism from boolean to R with certain computational information).

Recall, one of the key insight of category theory is that, this universal property describes this type upto isomorphism (in certain category), i.e. say we have an arbitrary type X with this universal property:

Axiom UP_X : ∀ {R : Set}， R → R → X → R.
(* With other naturality condition (computational information)  *)

Then according to category theory (and universal property), in certain category, X is isomorphic (and thus consider equivalent) to boolean. However, this X is totally generic/parametric/free from any intensional information/no concrete definition specified — this means what we prove about X using only UP_X can be port back to boolean (the intensional datatype with concrete syntactic definition).

For example, if we then have

Inductive odd-even := 
  | 0 : odd-even 
  | S : odd-even -> odd-even 
  | h : x = S S x

For sure, (in usual extensional UIP setting), this odd-even has only two elements and thus must satisfy the universal property, but we have a totally different intensional definition compared to ‘boolean’ so the proof about ‘boolean’ is not usable here. But any proof about UP_X can be ported back to odd-even due to the same universal property. Thus we can say any reasoning using UP_X is syntax-invariant. This categorical definition of X can be considered as the syntax-invariant version of boolean.

This is one small example of data-generic programming in mathmatical reasoning.

We can have more related examples to our meta-theory – consider different formulation of STLC in equational theory, we can either use meta-level substitution to formulate them (the classic style in Coq), or using explicit substitution to formulate them (the QIIT style we introduced). However, if we use Free CCC as the syntax and prove things about it, since any concrete syntax (intensional) formulation should satisfy this universal property, the proof can be reused.

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.

Note: Since each intensional/concrete syntax is usually (isomorphic to) the initial object of the certain category, the reader can argue that, they can still work with this intensional/concrete syntax to do reasoning as it is already “initial” and suffice to be data-generic reasoning.

But the key point here is that, to really consider a intensional/concrete syntax is initial, you usually have to come up with the definition of the category of models and morphism of that syntax, and prove your syntax is initial in that category – and if you have gone through these considerations, then you are pretty much already working with cat semantic.

The key problem here is that, is your intensional/concrete syntax really that good so that you rather work with it than the initial model? I think QIIT might be one example that is good enough and I would rather work with it than to think of a very categorical flavour initial model.

To be honest, I consider cat semantic as a fancy way to write down the (syntax of an) equational theory, which to me is all QIIT is about (I am not saying QIIT is the best representation of cat semantic, I am saying QIIT seems a good enough intensional definition tool), but there are definitely cases where QIIT cannot handle well — for example, G. A. Kavvos’s thesis provide a modality that doesn’t respect equality, i.e. a ≡ b not implying box a ≡ box b, in this case, QIIT cannot handle well. But they still provide a (2-)cat semantic. Thus the key is still “syntax-invariant” here.

Now that we sort out the motivation for categorical semantic/syntax, we can now jump into the technical details.

Free CCC is syntax, Why?

Again,

To be a syntax, it is at least need to be equipped with an eliminator, like QIIT type, so that user can do reasoning/computation about it – like defining pretty printer and evaluators on it. We claim that the universal property of Free CCC can act like an eliminator.

We need to see why the universal property of Free CCC can be considered as eliminator.

Connection between Free-ness, Initiality and Elimination Principle.

Definition of Free
- Adjunction between two functors $F : C \to D$ and $G : D \to C$ has three formulations.
  - Two of them are Hom-Iso
  - and (co)unit factorization
  - These two combined can give you clearest understanding of the definition.
- Free functor is left adjoint to forgetful functors.
  - Usually forgetful functors are just functors forgetting some structures, and thus there is no official definition of forgetful functors
- As we know The Initial Object is exactly Elimination principle,
  - and we have initiality in these algebra using free-ness to generate upon the initial object
Is the existence of inductive type exactly some sort of free-ness?
- if we only consider W-type, where does free-ness come from for W-type?
Syntactical Model is usually free?
- Is free model always “equivalent to” syntactical model?
  - we have three notion here, free, initial and syntactical
    - free-ness is defined by the adjoint functor
    - initiality, which is basically implied by free-ness
    - syntactical model is defined by generator? Or Defined by quotient of something?
      - We need extra effort to prove a syntactic model is a free model, and it usually is
  - I think since free-ness subsume initiality to some extent, we only talk about the difference between term model and free models
    - what’s more, by Proposition 1.10 here we know certain collection of initiality implies is equivalent to free-ness
  - term model is one concrete intensional/syntactic construction of free model, and free model is described by adjoint functor thus extensional

Free CCC

If a given object is syntax, we need to have a strong enough mapping out arrow acting like elimination principle, so that we can do induction on it to reason (Just like dealing with QIIT)! Why Free CCC have elimination principle?

How is it defined?

Following Lambek 1988, we can see there is an adjoint functor between free CCC and graph $\mathcal{F} \dashv \mathcal{U}$: CCC $\to$ Graph and the universal property is defined in the book
- basically the universal property is saying any arrow $F: X \to U(Y)$ is (co)unit factorized by $X \to U(F(X)) \to U(Y)$.
So if we generate Free CCC using empty graph (an initial object in Graph category), then we will also have an initial object in the category of CCC, due to this adjunction. This initiality should be acting like elimination principle.
Thus once we prove a model is a CCC, due to this initiality, we should have a unique arrow from this free CCC to the given model, acting like elimination

Another notion is Free SCWF.

Free SCWF

Roughly it can be considered as the data of a QIIT with STLC signature, just like how CWF corresponds to QIIT using MLTT signature.
In the original text, free scwf doesn’t mention its free-ness, but we do have initiality, which is enough for us to see the existence of elimination principle
However, free SCWF can be really free,
the idea is formally formulated at Proposition 1.10 here.
1. Why initial object of the comma category leads to the factorization?
2. Why the above factorization means initial object of the comma category?
  1. These two hold trivially because that comma category is full of objects of the form $(c, f, R(?))$
3. Then Prop 1.10 holds trivially
Let’s go back, basically we want to show there should be an adjoint between $F \dashv U :$ Set $\to$ SCwf, here we know $F$ will map 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 category of $(B, ?, U(?))$.
1. Consider the definition of $B$-SCwf – basically SCwf with interpretation $\llbracket ?\rrbracket_B : B \to Ty$, thus each object $(C, Ty, Tm, \llbracket ?\rrbracket_B)$ in $B$-SCwf is an objet in $(B, ?, U(?))$, in the form of $(B, \llbracket ?\rrbracket_B, U((C, Ty, …)))$
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$ in scwf
But syntactically, this SCWF is even weaker than CCC

Lindenbaum-Tarski+algebra,

I should run some examples here but I am too lazy
Write out the definition Lindenbaum-Tarski algebra
Prove Lindenbaum-Tarski algebra is “free algebra” (present an adjoint functor)
Specify the initiality conjecture (and the proof here)
Indicate the same game of term model, initial model, free algebra for dependent type theory and Generalized Algebraic Theory
We have following related example about free/forgetful pair
- Graph $\dashv$ cartesian closed category
- ? $\dashv$ Free algebra of Lawvere Theory

However, Free CCC/SCwf is tooo weak to be helpful. Basically we cannot impose customized intro-elimination rules at all. We need to use “Sketch on CCC” or back to using QIIT about it. But is QIIT ‘categorical’ enough to be considered as a proper ‘syntax-invariant’ notion? Unknown to the author. But we do know QIIT can lead to some good notion of category and morphism and each QIIT syntax is the initial object.

However, that sketching paper is totally out of reach. The 2-monad and sketch is brand new for us…

Modern way of dealing with syntax is to use categorical syntax instead of the real syntax. For example, for STLC, using Coq’s Inductive type to define syntax is the real syntax, but using Free CCC instead is the categorical syntax.

Generally, we know in categorical setting, we will usually make one particular category (as a representation of an equational theory) as the syntax of the language we focus on. In that case, what is the semantic?

It must be confusing: Isn’t a category itself a “semantic”? i.e. Other category in the same category as the syntax category(initial object) should be the semantic, right?

Functorial Semantic

Lawvere suggested otherwise about the definition of semantic — once we have a given category as syntax (say translating a theory into a category and consider it as a syntax), then we consider a functor from this category to another (instead of the category) as a model (truly using the codomain category as the interpretation). Simply because model is actually a proof-relevant concept — two functors go to the same category should be considered as two different models because they map differently. Then model homomorphism is the natural transformation between functors. This is functorial semantic.

We need to review more according to:

References : Categorical Logic by Andrej Bauer + Awodey

Summary

Take away is

Categorical Semantic/Syntax is extensional and syntax-invariant and thus more mathematical for sure
Categorical Semantic/Syntax is at-the-end describing a bunch of equations, and thus very axiomatic
1. thus it has a lot of advantages when describing STLC, (Categorical)-Logic stuff and depednent type theory, because they can easily be described in a “reduction-free” (absence of operational semantic) style
  1. note that, these without operational semantic, are not really PL but type theory
  2. they become PL once we have a runnable denotational interpreter
  3. or for dependent type, we need a normalization-by-evaluation algorithm that is doing type-checking and running at the same time
2. But for general-purposed PL described using operational semantic, cat semantic becomes a bit useless (since they don’t really have equations, and they are pretty non-logic and the definition relies on the dynamic transitioning)
  1. We can still have contextual equivalence in these general-purposed PL, thus category theory can still come up to help
  2. for example, Levy’s CBPV thesis uses category theory to describe the equational theory of the CBPV
  3. but to be honest, I don’t see any advantage of using category theory in that case, because that is too axiomatic to be useful for a practical CS
  4. and the contextual equivalence still requires operational semantic as the “root of evidence” of the equation in category theory, so why cat semantic helpful?
  5. but truely, Levy finds out some adjunction model in this context for his CBPV model, so it is possible to bring some insight
  6. In these case, I would suggest turn into denotational semantic, then polish the denotation’s equality back to categorical semantic
To summarize –
1. if a system requires equation from the very beginning (like dependent type) or the developer wants the equational theory a lot, and has a strong logic flavour, there is no reason to be against cat semantic
2. If a system is described from the beginning in a dynamic style (very operational) without clear idea of contextual equivalence from the beginning, then (definition of) cat semantic is a bit hard to get for them in prior
The biggest problem for cat semantic:
1. cat semantic will consider (contextual) equivalent term as equal, but for an interpreter(normalizer), a concrete syntax representation is important
2. for example, (λ x. x)y is equal to y (after quotient) in our syntax and for cat semantic. A normalizer will expect to return y which is also exactly (λ x. x)y. This is unacceptable. So to do things correctly, a normalizer will return representation of equivalence class of the quotient. In other words, we need to define another datatype for representation. These are usually called Nf or Ne in the context of NbE
  1. to some extent, Nf and Ne is the classical notion of syntax that PL people will use
3. this problem is solvable, also in a very sophisticated way (2-cat, P-cat)
The topic of categorical semantic, or categorical logic, is mainly about finding theory-model equivalence. (Check Levy’s adjunction models for call-by-push-value With stacks), where the gluing model (roughly the model used to prove computability/halting) and presheaf model should locates.
This doesn’t cover topos stuff, just about the discussion of categorical semantic/syntax.

EDJ's Garage

Free CCC as Syntax for STLC