`sd-visualiser`: interactive hypergraph visualisation for programs as string diagrams

Nick Hu

Alex Rice

Calin Tataru

Dan Ghica

25th April 2025

Programs and semantics

What is a program?

A program is a sequence of instructions which, when executed, performs a computation.

For example, consider the program which computes $7 + 7 + 7 + 7 = 28$.

Computations are ordered: \[ \underline {7 + 7} + 7 + 7 \to \underline {14 + 7} + 7 \to \underline {21 + 7} \to 28. \]

This program is compiled to the following ARM assembly machine code:

MOV R0, 7     // load 7 into register 0
ADD R1, R0, R0 // add register 0 to register 0 and store in register 1
ADD R1, R1, R0 // add register 1 to register 0 and store in register 1
ADD R2, R1, R0 // add register 1 to register 0 and store in register 2

Programming language theory studies the mathematical structure of programs and their semantics. First, we need to understand what a program is. A program is a sequence of instructions which computes something.

For example, consider the program which computes $7 + 7 + 7 + 7 = 28$. A computation is a sequence of steps which transform the program to its result, and we think of this as an ordered relationship. For example, instead of thinking of $7 + 7 = 14$ as an equation, we think of it as a directed step from left to right in the computation.

This sequence of instructions is with respect to some kind of algebraic theory, in the vaguest sense; here, we are just using simple arithmetic to represent our program for the addition of these 4 numbers. To be of any use, this needs to be turned into something a computer can understand, for example assembly code. Here is a fragment of ARM assembly code which does this arithmetic computation.

A compiler is a special program which translates a program from one language to another; typically, from a high-level source language (in this case, our language is arithmetic), to some low-level machine code (here, ARM assembly). We can imagine such a program that when given any arithmetic expression, it will produce the corresponding ARM assembly code.

What is a compiler optimisation?

Theory of arithmetic tells us that $x + x + x + x = x \times 4$.

An optimising compiler recognises $7 + 7 + 7 + 7$ fits this pattern: \[ \underline {7 * 4} \to 28. \]

We get a shorter, more efficient program:

MOV R0, 7     // load 7 into register 0
MOV R1, 4     // load 4 into register 1
MUL R2, R1, R0 // multiply register 1 to register 0 and store in register 2

In general, compiler optimisations are about finding semantic-preserving transformations on programs which make them more efficient.

We know certain things about the theory of arithmetic: for example, adding four copies of a number is equivalent to multiplying by four. This means that, doing our computation by hand, we can replace the previous computation by a multiplication. In particular, it is useful for a compiler to understand this fact, as it can make the generated code shorter and more efficient.

These kind of rules are called compiler optimisations. They are about finding transformations on programs which preserve the meaning (semantics), but make it more efficient.

Just as mathematicians (especially category theorists) like to find concise and elegant proofs, programmers like to wield abstraction and write concise and elegant programs. Highly abstract programming languages like Haskell are popular because they allow programmers to express their ideas and algorithms neatly, yet they are extremely far from the machine-level instructions. On the other hand, low-level programming languages like C are closer to the machine, so are more common choices for code where performance is absolutely critical. But using a low-level language is a trade-off: it is harder to write and reason about programs in C than in Haskell, and the amount of code necessary for comparable tasks is many multitudes higher. Compiler optimisations bridge this gap by allowing programmers to write in a high-level language and have the compiler automatically generate efficient machine code.

What does it mean?

Programs: terms of a type theory (e.g. arithmetic expressions, λ-calculus).

Denotations: mathematical objects associated to a term (e.g. numbers, functions).

Categorical semantics: \[ \begin {aligned} \text {type theory} &\cong \text {category}, \\ \text {types} &\cong \text {objects}, \\ \text {terms} &\cong \text {morphisms}. \end {aligned} \]

Curry-Howard-Lambek correspondence: \[ \begin {aligned} \text {simply typed $\lambda $-calculus} &\cong \text {cartesian closed category}, \\ \text {types} &\cong \text {objects}, \\ \text {terms} &\cong \text {morphisms}. \end {aligned} \]

How do you know a compiler optimisation is correct? First, we need to understand what it means for a program to be correct, which begins by understanding their semantics.

A narrow view, but the most typical among category theorists, is that programs are terms of a type theory. These are syntactic objects which can be manipulated by rules. For example, I showed earlier an arithmetic expression built out of some numbers and addition, and a computation which evaluates the addition.

Denotational, and categorical, semantics are about associating mathematical objects to these terms. Domain theory is a denotational semantics for the λ-calculus, where terms are interpreted as continuous functions on complete partial orders. Categorical semantics then generalises this by associating terms to morphisms in a category, where the ambient structure and property of the category determines the type theory of its internal language.

A particularly famous correspondence is the Curry-Howard-Lambek correspondence, which says that the simply typed λ-calculus corresponds to a cartesian closed category. More precisely, for any cartesian closed category, there is an associated theory of the simply typed λ-calculus given by its internal language, and every theory of the simply typed λ-calculus admits a syntactic category whose objects are types and morphisms are terms.

This allows us to establish an equivalence between programs and morphisms. Categories in particular define when two morphisms are equal, which in turn tells us what it means for programs to have the same meaning: when their denotations are equal.

What is a computer?

A computer is nothing more than a string processing machine.

Programs are always represented as strings.

We use encodings to represent fancier data structures, and it matters how we encode them.

Traditional abstract syntax trees are a way to represent programs as trees:

\[ ((7 + 7) + 7) + 7 \] \[ \leadsto \]

This talk: string diagrams give us a better way.

A reductionist view of a computer is that it is a string processing machine. It acts on sequences of 0s and 1s in its memory buffers, taking these strings as input and outputting more strings.

Every program that we type into a computer is ultimately encoded this way, as is every piece of data that a program manipulates. But we get to choose how we wish to encode information.

Unlike in mathematics, we do concern ourselves with specific encodings of data, as the choice matters for performance reasons, and any algorithm we give (if we want the computer to run it) must be with respect to whichever encoding is in use. For example, in scientific computing, data is often given by large matrices of which many cells are 0. To make computations tractable, we can use a sparse matrix encoding, which only stores the non-zero entries.

A compiler as a program needs to have a way of representing its input: other programs. The traditional way to do this is with an abstract syntax tree, which is a tree representation of the program that abstracts away from unnecessary details present in the token stream of the string representation of the program.

In this talk, we will see how string diagrams give us a better way to represent programs.

Crash course on λ-calculus

Fix a countably infinite set of variables $\mathcal {V}$.

λ-terms $\Lambda $ are generated inductively by:

$\lambda $ is a binder; variables which are not bound are free: \[ \forall t \in \Lambda . \text {FV} (t) \subset \mathcal {V}. \]

α-equivalence: terms are equivalent up to renaming of bound variables. \[ \lambda x. t \equiv _\alpha \lambda y. t[y/x]. \]

Captures the idea that the name of a variable doesn't matter.

I suspect that many of you are not familiar with the λ-calculus, so I will give a very brief introduction. The λ-calculus is a very simple language, giving a mathematical theory of functions and computation. It is Turing complete, which means that any computable function can be expressed in the λ-calculus.

The λ-calculus is a formal system for expressing computation based on function abstraction and application using λ-terms. A λ-term is either a variable, an abstraction, or an application.

Formally, we fix a set of variables, countably infinite so that we never run out. The set $\Lambda $ is the set of all λ-terms, which are generated inductively by these rules.

The λ symbol is a binder which binds a variable in an expression, similar to $\forall $ and $\exists $ in logic.

Variables are either bound, if under a λ, or free in a term. Two terms are α-equivalent if they are the same up to renaming of bound variables; that is, given a term $\lambda x. t$, then we can generate an equivalent term by performing a capture-avoiding substitution of $y$ for $x$ in the subterm $t$. This captures the idea that the choice of variable name doesn't matter.

String diagrams

String diagrams are a graphical notation for terms in different types of monoidal categories.

The term $(f \otimes \text {id}) \circ (\text {id} \otimes g)$ is represented by the string diagram:

Equations of terms arising from the monoidal structure are captured by isotopy of string diagrams.

Cartesian monoidal categories (i.e. $\otimes = \times $ and $I = 1$) admit a natural copy-delete comonoid:

\[ \forall f. \]

\[ = \]

String diagrams are a graphical notation for terms in different types of monoidal categories.

In most settings, including ours, they are a two-dimensional syntax which is remarkably capable of absorbing uninteresting complexity in their geometry.

They've been used in a variety of settings, including quantum computing, linguistics, and category theory:

In quantum computing, these ideas spawned the ZX-calculus, which is a highly successful framework for reasoning about qubits and linear maps.
In linguistics, they are used to give a compositional study of natural language semantics.

So far, they have not been heavily exploited in the context of programming languages, but there do exist success stories Reference [string-diagrams-for-lambda-calculi-and-functional-computation].

Reverse automatic differentiation is a powerful technique for gradient-descent-based optimisation, which is heavily used in modern machine learning. In the presence of higher order functions, the algorithm (Lambda the Ultimate Backpropagator) is notoriously hard to describe and reason about. Only recently has the algorithm been shown to be correct using string diagram reasoning Reference [functorial-string-diagrams-for-reverse-mode-automatic-differentiation].
Closure conversion is a technique used to efficiently compile partial function application in functional programming by lifting all functions to global scope, which is naturally described with the string diagram calculus.

String diagrams $\leftrightarrow $ hypergraphs

Hypergraphs

Definition

A hypergraph $H$ is given by a set of vertices $V$ and a family of sets of hyperedges $E_{k, l}$ for each $k, l \in \mathbb {N}$. That is, a hyperedge $e \in E_{k, l}$ has $k$ (ordered) source vertices and $l$ (ordered) target vertices: for any $0 \leq i < k$ and $0 \leq j < l$, there is an $i$th source map $s_i\colon E_{k, l} \to V$ and a $j$th target map $t_j\colon E_{k, l} \to V$.

A hypergraph is discrete if it has no hyperedges.

Example

Hypergraphs as presheaves

Definition

Let $\mathbf {I}$ denote the category generated by objects pairs $(k, l) \in \mathbb {N} \times \mathbb {N}$ and an additional object $\star $, with $k+l$ morphisms: $\{\star \xrightarrow {i} (k, l) : 0 \leq i < k + l\}$.

A hypergraph is precisely a (finite) presheaf $H\colon {\mathbf {I}}^{\mathrm {op}} \to \mathbf {Set} \in \hat {\mathbf {I}}$: $H \star $ gives the set of vertices, and $H (k, l)$ gives the set of hyperedges with $k$ (ordered) source vertices and $l$ (ordered) target vertices; each function $H (k, l) \xrightarrow {i} H \star $ gives the $i$th hyperedge source map if $i < k$ and the $(i-k)$th target map otherwise.

This determines a category $\mathbf {Hyp} \coloneqq \hat {\mathbf {I}}$.

Consequences:

we know what hypergraph homomorphism is;
all colimits exist, formalising 'gluing together' hypergraphs;
we can make a 'labelled/typed' version of hypergraphs $\mathbf {Hyp}_\Sigma $ with respect to some signature $\Sigma $.

Hypergraphs with interfaces

Definition

The category of hypergraphs with interfaces, $\mathrm {Csp}_D (\mathbf {Hyp})$, is the category whose objects are discrete hypergraphs and morphisms are isomorphism classes of cospans in $\mathbf {Hyp}$ of the form $S \xrightarrow {\mathsf {in}} H \xleftarrow {\mathsf {out}} T$, where $S$ and $T$ are discrete.

Example

Monogamy, acyclicity

Definition

A morphism $S \xrightarrow {\mathsf {in}} H \xleftarrow {\mathsf {out}} T$ of $\mathrm {Csp}_D (\mathbf {Hyp})$ is monogamous if $\mathsf {in}$ and $\mathsf {out}$ are injective as vertex mappings, and every vertex $v$ of $H$ has in/out-degree either 0 or 1, with in-degree 0 if and only if $v$ is in the image of $\mathsf {in}$, and symmetrically out-degree 0 if and only if $v$ is in the image of $\mathsf {out}$.

Definition

A hypergraph is acyclic if there is no path from a vertex to itself, where a path from $u$ to $v$ is a non-empty sequence of hyperedges such that the first hyperedge mentions $u$ on its source boundary and the last hyperedge mentions $v$ on its target boundary, and each consecutive pair of hyperedges $(e, e^\prime )$ shares a common vertex in the target boundary of $e$ and the source boundary of $e^\prime $. A cospan $S \xrightarrow {\mathsf {in}} H \xleftarrow {\mathsf {out}} T$ is acyclic if $H$ is.

Representation theorem

Proposition

The restriction of $\mathrm {Csp}_D (\mathbf {Hyp}_\Sigma )$ to monogamous acyclic cospans forms a symmetric monoidal category $\mathrm {MACsp}_D (\mathbf {Hyp}_\Sigma )$.

Theorem\[ \mathbf {S}_{\Sigma } \cong \mathrm {MACsp}_D (\mathbf {Hyp}_\Sigma ). \]

Free symmetric monoidal categories over $\Sigma $ are equivalent to monogamous acyclic cospans of discrete hypergraphs labelled by $\Sigma $.

Programs represented as string diagrams

`sd-lang`

Introducing sd-lang, a toy language for programs with let bindings.

syntax

essentially λ-calculus with arithmetic operations and recursive let:

e.g. bind x = v1 y = v2 … in v.

values are variables, thunks, or operations op(v1, v2, …):

plus(x, y), eq(x, y), if(cond, tb, fb), etc.

semantics

a model of string diagrams for traced cartesian closed categories.

We have a toy language for programs, which is essentially λ-calculus with arithmetic operations and recursive let Reference [a-robust-graph-based-approach-to-observational-equivalence].

Operations are all explicit, including λ abstraction and application.

As we are talking about compiler tooling, unlike when implementing a real compiler, we don't concern ourselves with evaluation: we are only interested in the structure of the program, hence our semantics as essentially a fancy version of the syntactic model.

In other words, we really think about sd-lang as a hypergraph description language.

sd-lang is a stand-in for an intermediate representation used inside of a compiler, which we will talk about later.

Nonetheless, we can still write programs and imagine what they mean.

Example: factorial

bind fact = lambda(x .
    if(eq(x, 0),
      1,
      times(x,
        app(fact,
          minus(x, 1)
        )
      )
    )
  )
  in app(fact, 5)

Here is a program which computes the factorial of 5.

factorial is defined as a lambda which recursively calls itself.

On the right, we have the string diagram representation of this program:

the nodes represent operations, and the edges represent dataflow;
the nested boxing (i.e. the hierarchical in hierarchical hypergraph) represents thunking;
the recursive call is represented by a loop, corresponding to traced structure.

There are a few non-obvious reasons for why we might want to represent this program this way, which will be one of the main focuses for this talk

`Factorial` as an AST

bind("fact",
    lambda("x",
      if(eq("x", 0),
        1,
        times("x",
          app("fact",
            minus("x", 1)
          )
        )
      )
    ),
    app("fact", 5)
  )

Compiler optimisations are described by semantic-preserving transformations on these ASTs given by rewrite rules.

First, let's look at how this program might be traditionally represented in a compiler.

We have a notion of abstract syntax tree, which is a tree representation of the program that abstracts away from unnecessary details present in the token stream of the string representation of the program. e.g. whitespace and indentation choice.

Rather than representing this AST textually, we can also draw it as a tree.

An optimising compiler might do some transformations on this tree to make the program more efficient, in a way that preserves the meaning of the program for soundness.

ASTs do not support sharing, or α-equivalence I

Consider the expression $(x + 1) + (x + 1)$ (where $x$ is free).

This is represented by the sd-lang expression: plus(plus(x, 1), plus(x, 1))

Its AST is:

ASTs do not support sharing, or α-equivalence II

Problem: The term obtained by the α-invariant substitution $[x \mapsto y]$ is represented by a different AST.

Consequence: The optimisation $\texttt {plus}(x_1, x_2) \to \texttt {times}(x_1, 2)$ needs to do a non-trivial computation to be valid, namely checking that $x_1 \equiv _\alpha x_2$.

Can leverage de Bruijn indices, nominal techniques…

This means that if our compiler wants to do a transformation to perform an optimisation, like replacing $x + x$ with $2x$, it needs to do a non-trivial computation to check that the two $x$'s are the same.

There are some techniques to manage this, such as de Bruijn indices, which force $\alpha $-equivalence to coincide with equality by using indices to refer to variables.

But these are not very pleasant to work with, as reindexing must happen often and is complicated, so this approach is completely divorced from compiler implementation in practice.

String diagrams do support sharing, and α-equivalence

Our string diagrams are equipped with a natural copy-delete comonoid.

This allows for a more meaningful representation of this program as the string diagram:

$(x + 1) + (x + 1)$ — observe that $x$ does not appear in the diagram!

Nodes represent operations, and edges represent dataflow (e.g. of values)!

ASTs do not support binding and shadowing

Another way to write this program: bind y = plus(x, 1) in plus(y, y)

AST:

\[ \neq \]

ASTs vs string diagrams

Program	AST	String diagram
plus(plus(x, 1), plus(x, 1))
bind y = plus(x, 1) in plus(y, y)

Compiler optimisations as string diagram rewriting

The optimisation we care about is:

\[ = \]

For $(x + 1) + (x + 1)$, derive:

\[ = \]

Here is the optimisation we wanted from before, in string diagram form.

This derivation works as follows:

First, we can box up the plus 1 to think of it as some endomorphism on this wire.
Then, we apply the naturality of the copy comonoid with respect to this endomorphism.
Next, we unbox.
Finally, we are in a position to directly apply our optimisation as a rewrite rule, and obtain the optimised term.

An aside on graphs

Graphs are also used in production compilers to sidestep these issues

✔ They also convey information efficiently, and naturally support sharing
✗ They are not algebraic: no inductive structure, hard to reason about and distil algorithms which preserve invariants

String diagrams can be thought of as an intermediate representation between ASTs and graphs

✔ Have enough graphical structure to support sharing and α-equivalence
✔ They are algebraic, as they represent terms of some kind of monoidal category
✔ Support a natural theory of rewriting via double-pushout graph rewriting (corresponding to equipping the monoidal category with equations)
✗ ( ✔ ?) Not very well studied, lack of tooling(!)

One might wonder why all this machinery is necessary, and why we can't just use graphs.

Graphs do feature in production compilers, and solve some of the problems I've talked about.

However, in the absence of some structure, the only reasonable notion of equivalence is graph isomorphism.

For instance, think again about the naturality of the copy comonoid.
Both sides of the equation can be thought of as graphs, but they are not isomorphic, so from a graph perspective there is no reason a priori to believe that this equation holds.

In some sense, string diagrams are the notion of fancy graphs with structure to make them more useful for reasoning about programs.

In part, this is because they are algebraic, as they represent terms of some kind of monoidal category — so really it should be like working with the internal language of this category, albeit with a topological flavour.

How to draw a string diagram

Hypergraphs quotient monoidal categories with copy-delete.

For each hypergraph, we need to pick a representative monoidal term:

involves (non-canonically) foliating the hypergraph into layers, and determining the order of operations (which determines how many 'swaps' are needed);
Aesthetically-pleasing diagram heuristic: minimise the number of layers, and the number of swaps (NP-hard).

Given a monoidal term, we can construct a big linear program to determine the coordinates of each node and positioning of edges [2].

A non-trivial problem is how to draw a string diagram.

As we are working with hypergraphs, we first need to pick a representative monoidal term.

This involves foliating the hypergraph into layers, and determining the order of operations.
This is a hard problem, and we have a heuristic which minimises the number of layers and the number of swaps to get nicer-looking diagrams.

Once we have a monoidal term, we can construct a big linear program to determine the coordinates of each node and positioning of edges.

This is then presented to the user of our tool in an interactive way.

LLVM and `sd-visualiser`

Anatomy of a modern compiler

It does this by providing an idealised kind of assembly language, called LLVM IR, which can be seen instructions for a kind of reduced instruction set computer with infinitely many registers. Compiler optimisations are performed at the level of LLVM IR, and a compiler itself is split into a language-specific frontend which turns a high-level programming language into this IR, and a target-specific backend which generates machine code. In effect, this solves the $m$-$n$ problem of adding support for a target to a specific programming language. Many modern programming languages are primarily compiled via LLVM.

Bug hunting `fibo.c`

Consider the following (buggy) Fibonacci program:

// fibo.c
#include <stdio.h>
int fib(int n) {
  int f, f0 = 1, f1 = 1;
  while (n > 1) {
    n = n - 1;
    f = f0 + f1;
    f0 = f1;
    f1 = f;
  }
  return f;
}
int main() {
  int n = 9;
  while (n > 0) {
    printf("fib(%d)=%dN", n, fib(n));
    n = n - 1;
  }
  return 0;
}

; clang -emit-llvm fibo.c -O1 -S
define i32 @fib(i32 %0) {
  %2 = icmp sgt i32 %0, 1
  br i1 %2, label %3, label %10

3:                    ; preds = %1, %3
  %4 = phi i32 [ %8, %3 ], [ 1, %1 ]
  %5 = phi i32 [ %4, %3 ], [ 1, %1 ]
  %6 = phi i32 [ %7, %3 ], [ %0, %1 ]
  %7 = add nsw i32 %6, -1
  %8 = add nsw i32 %4, %5
  %9 = icmp sgt i32 %6, 2
  br i1 %9, label %3, label %10

10:                   ; preds = %3, %1
  %11 = phi i32 [ undef, %1 ], [ %8, %3 ]
  ret i32 %11
}

LLVM IR is a good place to perform some program analysis in a way that is somewhat programming-language independent.

We will go through an example C program; there's an issue with this implementation of Fibonacci, can anyone see? Hint: what happens if $n \leq 0$, which is a perfectly valid int range; we return the uninitialised f, which is undefined behaviour.

We can compile this C program using the clang frontend to LLVM, generating this LLVM IR. It looks a bit like assembly language, and there are three blocks, corresponding to the start of the function, the body of the while loop, and what follows.

Using sd-visualiser, we can render this IR as a string diagram. Hopefully, here it is clearer what the issue is!

Demo

Also available at https://sd-visualiser.github.io/sd-visualiser.

Next, I will demo our tool. Our example use-case is the following: imagine you are a compiler developer, on a language which uses string diagrams as IR. Now, you want to write an optimisation pass, which is a rewrite rule on string diagrams, but you're not sure if it's correct, and you want to test it on some examples and see how it interacts with the other optimisations in the compiler. There is no option other than to check the compiler output, with and without the optimisation. In a traditional compiler, this is already pretty hellish to do on an AST level; with string diagrams coming from machine-generated compiler output, it's even worse. This is where our tool comes in: you want to be able to effectively visualise the string diagrams, and interactively explore the compiler output.

References

Dan Ghica , Fabio Zanasi, String Diagrams for \lambda -calculi and Functional Computation, October 2023
Calin Tataru , Jamie Vicary , A layout algorithm for higher-dimensional string diagrams, May 2023
Mario Alvarez-Picallo , Dan Ghica , David Sprunger , Fabio Zanasi , Functorial String Diagrams for Reverse-Mode Automatic Differentiation, 2023
Dan Ghica , Koko Muroya, Todd Waugh Ambridge, A robust graph-based approach to observational equivalence, September 2021
Chris Lattner, Vikram Adve, LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation, March 2004

sd-visualiser: interactive hypergraph visualisation for programs as string diagrams

Programs and semantics

What is a program?

What is a compiler optimisation?

What does it mean?

What is a computer?

Crash course on λ-calculus

String diagrams

String diagrams \(\leftrightarrow \) hypergraphs

Hypergraphs

Hypergraphs as presheaves

Hypergraphs with interfaces

Monogamy, acyclicity

Representation theorem

Programs represented as string diagrams

sd-lang

Example: factorial

Factorial as an AST

ASTs do not support sharing, or α-equivalence I

ASTs do not support sharing, or α-equivalence II

String diagrams do support sharing, and α-equivalence

ASTs do not support binding and shadowing

ASTs vs string diagrams

Compiler optimisations as string diagram rewriting

An aside on graphs

How to draw a string diagram

LLVM and sd-visualiser

Anatomy of a modern compiler

Bug hunting fibo.c

Demo

References

`sd-visualiser`: interactive hypergraph visualisation for programs as string diagrams

`sd-lang`

`Factorial` as an AST

LLVM and `sd-visualiser`

Bug hunting `fibo.c`