Enriched Lawvere Theories

My grad student Christian Williams and I finished this paper just in time for him to talk about it at SYCO:

• John Baez and Christian Williams, Enriched Lawvere theories for operational semantics.

Abstract. Enriched Lawvere theories are a generalization of Lawvere theories that allow us to describe the operational semantics of formal systems. For example, a graph-enriched Lawvere theory describes structures that have a graph of operations of each arity, where the vertices are operations and the edges are rewrites between operations. Enriched theories can be used to equip systems with operational semantics, and maps between enriching categories can serve to translate between different forms of operational and denotational semantics. The Grothendieck construction lets us study all models of all enriched theories in all contexts in a single category. We illustrate these ideas with the SKI-combinator calculus, a variable-free version of the lambda calculus, and with Milner’s calculus of communicating processes.

When Mike Stay came to U.C. Riverside to work with me about ten years ago, he knew about computation and I knew about category theory, and we started trying to talk to each other. I’d heard that categories and computer science were deeply connected: for example, people like to say that the lambda-calculus is all about cartesian closed categories. But we soon realized something funny was going on here.

Computer science is deeply concerned with processes of computation, and category theory uses morphisms to describe processes… but when cartesian closed categories are applied to the lambda calculus, their morphisms do not describe processes of computation. In fact, the process of computation is effectively ignored!

We decided that to fix this we could use 2-categories where

• objects are types. For example, there could be a type of integers, INT. There could be a type of pairs of integers, INT × INT. There could also be a boring type 1, which represents something there’s just one of.

• morphisms are terms. For example, a morphism f: 1 → INT picks out a specific natural number, like 2 or 3. There could also be a morphism +: INT × INT → INT, called ‘addition’. Combining these, we can get expressions like 2+3.

• 2-morphism are rewrites. For example, there could be a rewrite going from 2+3 to 5.

Later Mike realized that instead of 2-categories, it can be good to use graph-enriched categories: that is, things like categories where instead of a set of morphisms from one object to another, we have a graph.

In other words: instead of hom-sets, a graph-enriched category has ‘hom-graphs’. The objects of a graph-enriched category can represent types, the vertices of the hom-graphs can represent terms, and the edges of the hom-graphs can represent rewrites.

Mike teamed up with Greg Meredith to write a paper on this:

• Mike Stay and Greg Meredith, Representing operational semantics
with enriched Lawvere theories
.

Christian decided to write a paper building on this, and I’ve been helping him out because it’s satisfying to see an old dream finally realized—in a much more detailed, beautiful way than I ever imagined!

The key was to sharpen the issue by considering enriched Lawvere theories. Lawvere theories are an excellent formalism for describing algebraic structures obeying equational laws, but they do not specify how to compute in such a structure, for example taking a complex expression and simplifying it using rewrite rules. Enriched Lawvere theories let us study the process of rewriting.

Maybe I should back up a bit. A Lawvere theory is a category with finite products T generated by a single object t, for ‘type’. Morphisms t^n \to t represent n-ary operations, and commutative diagrams specify equations these operations obey. There is a theory for groups, a theory for rings, and so on. We can specify algebraic structures of a given kind in some ‘context’—that is, in some category C with finite products—by a product-preserving functor \mu: T \to C. For example, if T is the theory of groups and C is the category of sets then such a functor describes a group, but if C is the category of topological space then such a functor describes a topological group.

All this is a simple and elegant form of what computer scientists call denotational semantics: roughly, the study of types and terms, and what they signify. However, Lawvere theories know nothing of operational semantics: that is, how we actually compute. The objects of our Lawvere are types and the morphisms are terms. But there are no rewrites going between terms, only equations!

This is where enriched Lawvere theories come in. Suppose we fix a cartesian closed category V, such as the category of sets, or the category of graphs, or the category of posets, or even the category of categories. Then V-enriched category is a thing like a category, but instead of having a set of morphisms from any object to any other object, it has an object of V. That is, instead of hom-sets it can have hom-graphs, or hom-posets, or hom-categories. If it has hom-categories, then it’s a 2-category—so this setup includes my original dream, but much more!

Our paper explains how to generalize Lawvere theories to this enriched setting, and how to use these enriched Lawvere theories in operational semantics. We rely heavily on previous work, especially by Rory Lucyshyn-Wright, who in turn built on work by John Power and others. But we’re hoping that our paper, which is a bit less high-powered, will be easier for people who are familiar with category theory but not yet enriched categories. The novelty lies less in the math than its applications. Give it a try!

Here is a small piece of a hom-graph in the graph-enriched theory of the SKI combinator calculus, a variable-free version of the lambda calculus invented by Moses Schönfinkel and Haskell Curry back in the 1920s:

SKI

You can use Markdown or HTML in your comments. You can also use LaTeX, like this: $latex E = m c^2 $. The word 'latex' comes right after the first dollar sign, with a space after it.

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.