alifib, the language of higher-dimensional diagrams

As part of ARIA’s Safeguarded AI programme, I have been leading the development of alifib, an experimental programming language and interactive proof assistant founded on higher-dimensional rewriting. In alifib, programs are diagrams: not illustrations of programs, but the syntax itself, the internal representation, the thing that is checked and run. This notebook post is an attempt to say what that means and what it is for. The proof assistant runs in a browser at http://compose.ee/alifib, with nothing to install, and the reader may want to keep it open beside the text.

From terms to diagrams

Nearly every programming language represents a program as a term, a tree-like structure. The tree records what the program is; how it runs is settled elsewhere—by reduction, by evaluation, by whatever mechanism an interpreter or compiler chooses—outside the syntax, and taken on faith.

Term syntax also makes a quiet assumption: that data may be copied and discarded at will. A variable may appear twice in a term, or never. Much of computation is not like that—a resource consumed cannot be reused, a message sent cannot be unsent—and category theory has long had a syntax for such situations: string diagrams for monoidal categories, that is, nodes joined by wires, each wire carrying a value, exactly once, from one operation into the next. Terms are the special case in which every wire comes with copying and discarding operations.

The second step is to go up in dimension. A string diagram is already a two-dimensional object, having besides its nodes and wires the regions of the plane that the wires bound. Once regions, wires, and nodes are counted as cells of dimension 0, 1, and 2, there is no reason to stop counting. A pasting diagram has cells of every dimension, each bounded by an input and an output face: a point, an arrow between points, a filled surface between two paths of arrows, a solid between two such surfaces. Each level, moreover, reads as a rewrite of the level below—an arrow carries its source to its target, a 2-cell carries one path of arrows into another—so that every storey of the tower, however high one climbs, is the same kind of object. (The counting is by role rather than by drawn shape: the string diagram is the Poincaré dual of a two-dimensional pasting diagram, with regions standing for points, and nodes for 2-cells.)

This is the entire ontology of the language: one kind of thing, the diagram, and one non-trivial operation upon it, subdiagram search, which finds a diagram sitting inside another. The whole rests on a single observation, the founding principle of higher-dimensional rewriting:

a computation on n-dimensional data is itself (n+1)-dimensional data.

In every other model of computation that I know of, a program and a run of that program are objects of different kinds: usually, a piece of syntax on one side, a sequence of machine configurations on the other. Here they are the same kind of object, one dimension apart, and the run is data again, ready in its turn to be computed on.

An alphabet of two letters

A type in alifib is a diagrammatic signature, a collection of building blocks of increasing dimension from which diagrams can be assembled. Let us look at a simple 2-dimensional example, essentially an encoding of a string rewrite system. Here is a type with a point pt, and two arrows a, b from the point to itself, so that words, that is, strings of as and bs, are one-dimensional diagrams. A rule of grammar for these words is nothing but a two-dimensional generator:

@Type
Letters <<= {
    pt,
    a: pt -> pt,
    b: pt -> pt,
    (* a rewrite rule is just a 2-dimensional generator *)
    swap: a b -> b a
}

swap rewrites the pattern a b, wherever it occurs inside a word, into b a. Note what is missing: there is no separate register in which “evaluation rules” are declared, no computation mechanism external to the type. The rule and the data it acts on are generators of one type, a dimension apart. A point, two letters, and one rule are very little, but they are enough to compute with.

Watching it run

Begin an interactive session on the word a b a b. The visualisation pane draws it as a string diagram, while the engine searches out every position at which swap matches, and lists them. This is subdiagram search at work; everything else in the system is bookkeeping around it, and everything one is ever asked to trust reduces to it.

Each click applies one rewrite. The session, however, is not mutating a string, as a text editor would: it is building a two-dimensional diagram, one swap cell pasted on at each step, and the word on screen is only the frontier of the construction. Stop at any point and switch the visualisation from the step view to the proof view: everything that has happened is there, as a single diagram.

It is worth pausing on that diagram. It is not a log of the computation; it is the computation, a first-class term of the language, which can be inspected, replayed, pasted into larger diagrams, and acted upon by higher-dimensional computations in its turn. If one only wants the answer, one asks for its output boundary.

Computational transparency

Recall the Curry–Howard correspondence, according to which programs are proofs: a well-typed term certifies, by existing, that the program it denotes is correctly formed. The correspondence, however, speaks only of the program. A term also carries an equational theory—a notion of when two terms are “the same”—and this theory, the very mechanism by which programs run, is meta-theoretical: assumed to exist, assumed to be computable, and in practice entrusted to the compiler. One may certify the program inside the language; to certify its execution, one must trust something outside it.

With diagrams, this boundary disappears. The rules by which a type computes are generators of the type itself, written down beside the ordinary ones, and a run of a program is a higher term—exactly the diagram built in the session above.

Well-typed terms are verified programs. Well-typed higher terms are verified executions.

I call this principle computational transparency, and it is alifib’s reason to exist. A verified program is not yet a verified run; between the two stands the whole tower of compilers and machines, and it is there that guarantees tend to evaporate. Our concern in this programme is with what a system did, rather than with what it was meant to do, and transparency is that concern made into syntax: the object one examines is the run itself, not a report of the run.

There is a consequence worth stating on its own. Since the rules by which a type computes are its own generators, each type is its own computational universe: its generators create, at the same time, the space in which computations happen, the data on which they act, and the computations themselves; nothing arrives from outside. A type expressive enough to house a Turing machine is still, in this sense, a sandbox, accounted for cell by cell by a kernel small enough to be read.

None of this is confined to two-letter alphabets. examples/TRS.ali sets up term rewriting systems in general, their terms two-dimensional diagrams and their runs three-dimensional ones, and examples/BinaryNat.ali instantiates it with binary arithmetic, so that

@BinaryNat
let d = (run auto on Eval.(run auto on parse "57 * (12 + 30)" end))

binds d not to the number 2394 but to a witness of the entire computation, whose output boundary is 2394. Since parsing, evaluation, and execution are all the same kind of diagram, parsing itself turns out to be functorial—the parse map sends parse traces of arithmetic expressions to the diagrams they denote—a remark that I will not develop here, beyond noting that those two files carry it out.

Eckmann–Hilton, by hand

Because equations are directed cells, equational reasoning in a higher-categorical structure is the same activity as running a machine. The classic Eckmann–Hilton argument says that two endomorphisms a, b of an identity must commute. In examples/EckmannHilton.ali the setting is built over a Bicategory module—itself written in ordinary alifib, its structural laws oriented into pairs of cells one dimension up—and the claim is stated as a map into the module’s type of equations, with two images withheld:

@EckmannHilton
let total Commutativity :: Equation = [
    lhs => a b,
    rhs => b a,
    dir => ?,
    inv => ?
]

Each ? is a hole: an image left open, to be filled interactively. The two fills are the proof: a pair of three-dimensional diagrams assembled by clicking through rewrites exactly as before, in which a and b slide past one another. Textbooks give this argument as a sequence of pictures, and the sequence built here is scarcely longer; the difference is that every move now exists as a cell, checked and retained, where the pictures rely on the reader’s goodwill to interpolate between them.

Four readings

Beneath the syntax, an alifib type is a finite directed complex: a finite family of cells graded by dimension, each carrying a partition of its boundary into an input half and an output half. The combinatorics—the molecules of my book, Combinatorics of higher-categorical diagrams—descend from far-sighted work of Richard Steiner in the early 1990s, in a lineage that runs back through Ross Street to the early days of higher category theory. What holds the construction together is topological soundness: every such complex is realised by an honest cell complex with exactly one cell per generator, so the combinatorics never drift from the geometry they claim to describe.

The reward is that one object may be read, faithfully, in four ways at once: as a piece of directed topology; as a presentation of a higher category; as a higher-dimensional rewrite system; and as a directed higher inductive type, with constructors between constructors. Each reading is a way of using the language—one may reason equationally in monoidal categories and bicategories, specify abstract machines whose every run is a witnessed trace, or describe a space and ask for its homology at the prompt—and the readings illuminate one another. In examples/Bicategory_examples.ali, the walking equivalence (a morphism invertible up to invertible 2-cells) sits beside the walking adjoint equivalence, which adds the two triangle equations of an adjunction. Asked for their homology, the interpreter reports $H_2 = \mathbb{Z}$ for the first and $H_2 = 0$ for the second: a hole in dimension two, witnessing topologically the classical fact that a bare equivalence is not coherent—and that promoting it to an adjoint equivalence is precisely what fills the hole.

What comes next

alifib today is a working system: a batch interpreter, a terminal REPL, the browser interface pictured throughout this post, a line-protocol daemon for editors, and an MCP server offering the same engine, tool by tool, to AI agents. The last deserves a word. In alifib, building a proof is search, and search is untrusted, whether a human is clicking or a model is calling; what is trusted is the kernel that accepts or rejects each step. It does not matter, then, how capable or how erratic the model is: nothing it produces enters a type except through the same check that governs a human hand. This division of labour—an inventive but untrusted proposer set against a small checker—will sound familiar to readers from the Safeguarded AI programme.

alifib can be tried at http://compose.ee/alifib, and its source lives at https://github.com/ahadziha/alifib. A paper giving a full account of the language and its interpreter is currently under review.

Further off, modules will acquire higher cells of their own (a module is already, in disguise, a complex whose points are types); a strategy language, where the effectful part of the runtime will live, I/O included, is being worked out with Wessel de Weijer; and a small family of type constructors—duals, suspensions, Gray products, joins—will make globes, oriented simplices, and oriented cubes available structurally, rather than as constructions made by hand.