What I’ve Learnt at Midlands Graduate School in the Foundations of Computer Science
Midlands Graduate School (MGS23) is an in-person conference held at the University of Birmingham in early April this year (2023). It features lectures on mathematics and its application to computer science. Before we proceed, I am a hobbyist math nerd but a software engineer by training first and foremost. Thus, my intuition for the following may differ from most mathematicians.
The courses I took for the conference were Domain Theory, Homotopy Type Theory, String Diagrams and Computational Models of Higher Categories, instructed by Tom de Jong, Eric Finster, Dan Marsden and Jamie Vicary, respectively.
The attendees I’ve met came from various backgrounds, from PhD students doing theoretical research such as categorical semantics of homotopy type theory, synthetic topology and even logic via the geometry of interaction. Some were also doing systems research, such as domain-specific language for hardware verification, separation logic for imperative language verification and graded linear type systems. Among them are also MSc students and software engineers from the industry like myself.
My main goal for attending the conference is to learn and contribute to using category theory to study the semantics of type theory and theories of computation in the future.
In this article, I will walk you through a high-level summary of each course I have taken and conclude with key takeaways that have shaped the way I look at the subject.
Domain Theory
In domain theory, we use lattice theory to model the semantics for programming languages. In the lectures, we used the programming language PCF as an example.
In most programming language implementation courses, we would define the syntax, dynamics, statics and denotational semantics rules of the language. Here domain theory is the study of the latter; denotational semantics.
After going through the formation rules of the PCF language, we attempted to give a denotational semantic to the constructs of the language. When defining the semantics for the function type:
σ => τWe can naively try to assign to it some function from the denotational semantic of the argument type to the denotational semantic of the return type. However, this will not be able to complete non-terminating terms as an element or for the fixed point term.
Thus we interpret types as some poset instead. For example, the natural numbers can be the following poset.
Let's give some definitions given a poset X
- An ω-chain in X is a sequence of x0 ≤ x1 ≤ x2 ≤ …
- An upper bound of S ⊆ X is an element y ∈ X such that ∀ s ∈ S, s ≤ y.
- A least upper bound y where for all upper bounds u, y ≤ u.
- X is chain complete (ω-cpo) if it has a least upper bound for all ω-chains.
- The least element ⊥ where for all elements x∈ X, ⊥ ≤ x.
- A ω-cpo is pointed (ω-cppo) if it has a least element.
- A function between two ω-cpos is ω-continuous if it is monotonic.
The Knaster-Tarski theorem then says every ω-continuous function has a least fixed point ∪fⁿ(⊥) which is the least upper bound of the following omega chain
⊥ <= f(⊥) <= f(f(⊥)) <= f(f(f(⊥))) <= ...We then explored the denotational semantics of contexts and product types, which we use to define the Scott Model of PCF, which is a complete denotational semantics for PCF.
With the Scott Model, we can express the Soundness Theorem and Computational Adequacy using a logical relation called the tate-computability, akin to proving soundness and completeness in logic. (but not exactly)
The key takeaway I got from Domain Theory is that:
- We can use lattice theory (or topology if we look at stone duality) to define denotational semantics for programming languages.
- Every element in the lattice corresponds to some program.
- Traversing the lattice corresponds to an inductive definition using the fix function in PCF.
- Knaster-Tarski theorem makes all inductive definitions terminate.
I would love to continue studying in this direction to use topology in domain theory. I was recommended the book “Synthetic Topology of Data Types and Classical Spaces” by a fellow student. Tom de Jong also suggests “Synthetic Domain Theory”.
Homotopy Type Theory (HoTT)
HoTT is an extension of Martin Löf Type theory (MLTT) that adds higher inductive types and the univalence axiom. It serves the following purpose.
- Clarifies equality in a constructive setting
- Types are geometric homotopical expressions
- Homotopy has its axiomatic definitions separate from topology
We first start by going through MLTT, such as the Curry-Howard correspondence. Where types correspond to propositions in logic and specification in computing, and terms correspond to proofs in logic and programs in computing.
Dependent types are then introduced, which can be seen as the following:
- Functions, terms on terms λx.E: A -> B
- Type Functions, terms on types λT.x: ΠT’. E
- Polymorphic Types, types on types λA.E: ΠA’. U
- Dependent Function, types on terms λx.E: Π(x’:A). B(x’)
If your type theory can perform induction, we can use it to express disjoint sum types, unit type, null type, finite types like bool and sigma, and the dependent pair type.
In MLTT there is also a notion of identity types where the proof that two terms of a type are equal is expressed as an identity type
refl_ab : a = bBut in HoTT, these proofs are not unique, meaning there can be more than one unique term in identity types. Moreover, proof of equality can also construct an identity type. Identity types with unique terms are defined as axiom K. In other words, in HoTT, axiom K does not hold.
Thus, there is a tower of identity types between proofs of equality, and there are symmetries or ways to be equal to themselves in many ways. We can visualise this naively as a tower of equality.
However, some identity types are unique or contractible, meaning if there are more than two proofs or equality, they are contractible to a single proof. Depending on which level this happens in the tower, it defines the truncation level or h level.
But what if we are identifying on types, i.e. A, B: U, thus p: A = B? This is where the univalence axiom comes in that says A = B ≃ A ≃ B. Here, A ≃ B is called an equivalence which can be seen as a form of function extensionality as follows
A ≃ B := Σ(g,h:B -> A)(Π(a:A) g(f a) = a) * (Π(b:B) f(h b) = b)With the univalence axiom, there is a map from identities to equivalences, and this map is precisely an equivalence.
These higher structures arise simply because identifications are now part of the data that the formalism can express. And this structure can be found in Homotopy Theory, a part of Algebraic Geometry. Thus types and constructions in the type theory correspond to some geometric meaning. This is known as the Curry-Howard-Voevodsky correspondence. You can check the table at the end of my previous blog post for more details.
We then defined the transport of a path, the unit circle S1, and the suspension of a type and using that on S1 allows us to define a function for the n-dimensional sphere Sn.
There is an operation called truncation, where a type with a specific h level can be truncated to another type with a smaller level. The truncation to n -1 or h level 1 will produce a type known as a mere proposition. It is akin to saying: “I have proof of a proposition” without specifying which exact proof it is. It thus corresponds to the unit type.
We also explored more exotic types, such as |S2|2 = K(Z2), equivalent to CP∞ or Eilenberg Maclane space. This shows that simply by going up one dimension from the unit circle, there is a rich geometric structure expressed in the identities.
The key takeaway I got from HoTT is that:
- Higher inductive types and univalence create a rich structure when terms of equality are part of the formalism.
- This structure can also be found in geometry (homotopy theory), creating a correspondence.
- We can use homotopical structures such as boundary and null homotopies to operate on our tower of identity types.
- Homotopical Interpretation does not just mean points and path corresponds to terms and identity terms, but dimensions, truncation, and connectedness also correspond to operations on higher inductive types.
- Complex types tend to be contractible at some point, whereas simpler types like S2 are rich in structure.
String Diagrams
When doing category theory in general, we can visualise or express categories using the following:
- Equational Expressions
Equations are linear syntax that can express any categorical construction. However, when we talk about complex constructions, it is hard to visualise how all the pieces interact with one another.
2. Commutative Diagrams
These diagrams help show how an expression is ‘equal’ or commute. Different confluent paths mean equivalent derivations. However, even in 2-categories, the diagrams can be rather complex too.
3. String Diagrams
String diagrams hide the messy details of a commutative diagram and instead let us reason the equivalences or commutative equations via isotopy reasoning, where we can slide and move parts of the diagram based on some rules.
The formalism of string diagrams for 2-categories is that
- 2D area regions are categories
- 1D lines are functors
- 0D points are natural transformations
Our notation is that functors are read from right to left. Thus in the example above, we can see that F: A → B as A is to the right of f with B to its left. And natural transformations are similarly read from top to bottom.
They obey some rules, such as functors that must come from the top of the diagram to the bottom unless connected to a natural transformation. And functors cannot bend backwards from where it comes from as that will have a different semantic meaning from functors.
One example of isotopy reasoning is how the interchange law can be derived from a string diagram.
Thus vertical and horizontal composition is simply appending diagrams next to one another, which implies the interchange law.
Another example of isotopy reasoning is the naturality of natural transformations.
Here we can see that dots sliding over other dots have some semantic meaning in the category, in this case, naturality.
We then explored some constructions in 2-categories.
Monad
The equational definition of a monad is simply the natural transformations η: Id → M and μ: M ○ M→ M that satisfy the unit and associativity axioms. Thus in string diagrams, it is visualised as such:
It should be noted that identities are left as blank spaces in the dimension below, i.e. identity functors are left blank in categories or areas; the line is omitted. Identity natural transformations are left blank in lines; the dot is omitted. This aids isotopy reasoning, as seen in the unit axiom.
Monad Morphisms
A monad morphism also gives meaning to the isotopy reasoning when sliding natural transformations over monads.
The same isotopy reasoning can be applied to monad morphism composition, where there are two monad morphism natural transformations (two or more points on the lines connected to the monad).
Kleisli Category
Given a monad, we can construct the Kleisli category of it.
In the string diagram, we are looking at the underlying category. Thus the Kleisli arrow or morphism can be seen as f: A → M B. This diagram does not view areas as categories but as objects. And lines not as functors but morphisms. And thus, the dot is a 2-cell construction of the Kleisli arrow. For ease of isotopy reasoning, we also use the third option for drawing Kleisli morphism, as shown in the figure above.
The laws or axioms of a Kleisli category can be done with isotopy reasoning by putting η and μ into the functor between M and f.
Likewise, for the monad axioms on a Kleisli category.
We then continued the exploration of other constructions such as F-Algebras, Eilenberg Moore Algebra (an F-algebra construction from a monad) and actions on a monad.
Adjunctions
Recall previously that functors cannot bend backwards from where they came from. This is because functors that do are called adjunctions.
The laws of adjunctions can be done with isotopy reasoning as well. These are called snake equations.
By isotopy reasoning, we can see that right adjoints are determined up to isomorphism. It takes time to equationally reason for new students to category theory, but we can see it clearly with isotopy reasoning.
We also explored adjunction composition and how using adjunctions in an underlying category is simply the bending of wires. This is called a transpose. This adjoint transposition is expressed as a box notation.
With this notation, the snake equations can be presented in another way.
We then went through even more complex constructions such as Huber Construction, Free Monads, and Resumption Monad.
The key takeaway I got from String Diagrams is that:
- 2-categories are not as scary if we can visualise them with string diagrams.
- We can use our geometric intuitions to do planar isotopy reasoning, which corresponds to some meaning in category theory.
- Learning category theory should be accompanied by string diagrams, just as commutative diagrams have.
Computational Models of Higher Categories
We start by defining 1-categories and 2-categories and observe how the definitional complexity increases exponentially as the dimension of the category increases. This leads us to the solution of Grothendieck’s disks and pasting schemes, which view paths as types.
At first glance, they may seem like ordinary commutative diagrams, but it is in fact, the representation of the structure of the category. In the diagram above, from left to right, it corresponds to the 0-category, 1-category, 2-category and 3-category.
We can then combinatorially glue these disks together. Pasting schemes can be expressed in four ways.
The k-cells (objects, and n-morphisms) are called words. They come in four kinds.
- Variables; primitively defined cells: x, y, z, w, f, g, h
- Composites; made by composing other words: f o g
- Equivalences; laws or defined by an equation: id_x, α_f,g,h
- Substituted; possibly composites with equivalences with variables possibly substituted for composites
Every pasting scheme has a source and target boundary, which can be seen as a subgraph of the disk representation that includes all objects. This itself is a pasting diagram and thus can be expressed as a word. The word for both boundaries must be the same dimension.
Grothendieck’s big idea is that the coherence of a pasting diagram is the path from the word of the source boundary to the word of the target boundary.
Thus coherence properties of pasting diagrams are yet another pasting diagram! This is the core idea of how the Catt proof assistant works.
In the second lecture, we explored again the idea of string diagrams as a graphical calculus for 2-categories. Then we generalized the idea for n-categories.
In general, the highest dimensional morphism is always the vertices. As the cell reduces in dimension, its geometric counterpart increases in dimension.
This representation of higher categories is the foundation for homotopy.io, a visual proof assistant that runs on the web.
As per isotopy reasoning, certain transformations on a graphical calculus do not change the definition of the category. This requires that those transformations are equivalent. This is permitted in a weak category and invalid in a strict category. However, homotopy as a mechanism for geometric reasoning lies somewhere in between.
The theory of pasting schemes is semistrict, whereas graphical calculus is semiweak. The proof assistant Catt based on pasting schemes thus are semistrict. However, we are still able to make it semiweak via three reductions:
- P Reduction: prune identity arguments
- D Reduction: simplify unary composites
- L Reduction: eliminate loops
Thus the class of pasting diagrams that normalize to the same pasting diagram after all of the reductions are equal in a semiweak sense. Thus we can compute our way to a semiweak theory in a semistrict one!
Lastly, we explore phenomena in higher categories using these formalisms.
Catastrophes in the theory of manifolds are critical points in local structures where their projection changes abruptly. In higher categories, this means a local transformation in a graphical calculus leads to an abrupt complex transformation in the higher dimensional calculus of coherences. In particular, we explored adjunctions.
In 2-category string diagrams, this corresponds to snake equations, but in 3-categories, the swallowtail; in 4-category the butterfly; and in 5-category, the wigwam.
We also explored the cobordism hypothesis and models of knot theory in higher categories.
The key takeaways are:
- Grothendieck’s pasting diagram innovates coherences and properties of higher categories as constructions in higher categories themselves
- Graphical calculus of higher categories allows geometric equivalences to correspond to the strict vs weak properties of the category
- Geometric structures can be modelled in higher categories
- Higher categories can be modelled in geometric structures
Conclusion
I enjoyed my first solo trip abroad to Birmingham and meeting many cool people working on foundational computer science and category theory.
MGS23 is a remarkable platform for expanding my understanding of the field. The engaging sessions, thought-provoking discussions and presentations by esteemed experts provided deep insight into the advancements shaping the future of theoretical computer science and category theory. The knowledge I gained during the conference will undoubtedly contribute to my personal and professional growth, fueling my passion for this ever-evolving discipline.
For more information and links to the slides for the conference, check out: https://www.cs.bham.ac.uk/~mhe/events/MGS23/
