Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

December 17, 2016

Globular for Higher-Dimensional Knottings (Part 2)

Posted by John Baez

guest post by Scott Carter

This is the second post in a series about Globular. To load Globular, open a new tab in a Chrome browser window and have a a 3-button mouse plugged into your computer. The papers to read about Globular are Data structures for quasistrict higher categories by Jamie Vicary and Krzysztof Bar, and Globular: an online proof assistant for higher-dimensional rewriting in which Aleks Kissinger joins Jamie and Krzysztof to explain further and give some nice examples of globular’s potential.

Back when John Baez was still a proto-blogger, Masahico Saito and I were initiating a study of knotted surfaces from a movie point of view. The entire study of embedded surfaces in 4-dimensional space has a rather brief history. It started in 1925 when Emil Artin demonstrated that higher dimensional knotted spheres exist. Artin’s construction is called spinning, and the spin of a knot has the same fundamental group and hence the same Alexander polynomial as the knot that was spun.

Most results about knotted surfaces, and indeed most examples were discovered in the period 1960 through 1980. In a 1965 paper, by Sir Christopher Zeeman (not yet knighted at that point) gave a construction of twist spinning. This was generalized both by Ralph Fox and Rick Litherland. Recently at a conference, a colleague bemoaned the fact that that there is an paucity of examples of knotted surfaces. That colleague and I are of the same mathematical age (mathematical birth 1982), and his dissertation involved questions about twist-spinning. Here is your chance to do something about this. First, let me describe the movie move template. Please click the last link! Also disable the “Allow undo” button on the lower right.

As before, background space is black, empty, and codimension 2. It is constructed as the identity on the identity of a single 0-cell that is named, cell 1. Within this space, we have a white object, cell 1, that is a morphism from the identity on cell 1 to itself. I will collapse the categorical description and call this small white point an object. Morphisms in the category are constructed from \cup, \cap, XX, and X¯\overline{X}. As before, you can construct an X or Xbar. by means of composing a white dot with itself, hitting the identity key, switching to a project 1, and left-clicking/ right or left swishing with your mouse at the bottom or top of an arc. I’d advocate turning off “Allow undo” on the lower right before beginning.

Those who are familiar with the 2-category of 2-tangles will recognize that Reidemeister type I, type II, type III, ysp/psy, zig-zag moves, and interchanges of distant critical points are invertible 2-morphisms in this 2-category. Births, deaths, saddles, and crotches are non-invertible 2-morphisms. Among the 4-cells listed, type II and type III moves are not listed because they are categorical. Bear in mind that often there are two different types of type III moves because there are two different proofs that the Yang-Baxter move follows from naturality.

Oh yeah, you are probably still cringing at the word choice “crotch.” There is a distinction if only because, as critical points, they can be of different indices. When you sit upon a horse, your crotch fits in the saddle. The crotch and saddle allign in different directions. Horizontal cusps can interchange crotches and saddles. Meanwhile, I don’t have an alternative synonym in English. Other Romance languages use words that roughly mean bifurcation. The term crotch stands for now.

Let us look at one of the 5-cells. These are the movie moves that are not intrinsic to globular, although some follow from globular’s isotopy moves. Left click on R birth/crotch cancel. Change the projection to 2. There are 2 possible slices. In the zeroth slice you’ll see a black rectangle separated by a lime green line from a white rectangle. It looks like this:

With more experience you’ll imagine this as a vertical parabolic cylinder opening to the right of the screen. The lime green vertical line indicates the identity on a cup. But don’t take my word for it: change to project 1 to see this:

There are now two slice indices. Increment the slice on the right. Nothing happens! That’s why it is an identity. Now go back to project 2 slice 1:

A black region on the left and bottom is separated from a white region on the right and top by a pendulous dichromatic line. Hover the mouse over the lower greenish vertex at the lower left. It indicates birth at t[0]:


The purplish upper right vertex indicates a crotch at t[1]. Let’s slice this. So change the view to project 1, slice 1,0. Again this is a cup. Hover the mouse to the right most box at the slice and move your right hand to the up arrow key on your keyboard. A yellow rectangle appears below the minimal point of the cup:


Click on the up arrow. A circle is born. A second hover/click indicates that a crotch will occur between the lower pants leg (circle) and the cup. Switch back and forth between the various projections and slices until you understand this.

Obviously, most of this article is self-serving, so it won’t be any more self-serving to refer you to this book. Please examine the 5-cells in the signature, and compare them to the moves on page 52–54 of our book. Also check out the movie representations that (mostly) begin on page 79. As I pointed out earlier, any move that is not explicitly listed in the signature (and some that are listed) are consequences of the axioms of globular.

Now we’ll work through an exercise to create the most basic of knotted surfaces. Left click on the birth element of the signature:

Then left click again to reveal a set of five options for the new birth. We want a birth to the right of the given birth, so click on the fourth menu item.

Now within the workspace, change the projection to 1. Click up to slice 1. You should see an oval on the left and a circle on the right:


Hover the mouse to the left strand of the circle; left click and quickly drag so that this arc crosses over the arc to its left:


Replicate this move two more times:


Just below the third crossing from the top and at the third segment from the left, left click to produce a menu. Attach a saddle:


This is my fourth menu item. Now hover to the reddish maximal point that you just created and left click to get a menu. The last menu item is a crotch. Add this.


Move the mouse to the above crossing at which a type II move can occur. Left click and drag down. Do this twice more. Left click to the minimum point on the circle to get a menu, and click on the death. Then kill the remaining circle in a similar fashion. Change the view to project 2. You see the trace of the set of moves that you achieved. This is the spun trefoil whose image adorns David’s book Towards a Philosophy of Real Mathematics:


Can you prove that this is knotted? You can hit the identity button on the right and start to manipulate it.

In the next post, I’ll demonstrate the braided form of knotted surfaces. Meanwhile, see what other knotted surfaces you can construct.

Posted at December 17, 2016 2:15 AM UTC

TrackBack URL for this Entry:

14 Comments & 0 Trackbacks

Re: Globular for Higher-Dimensional Knottings (Part 2)

I’m sorry if this is too off-topic but reading these posts encouraged me to try out Globular so I attempted to implement the very simple SKI combinator calculus in Globular. It took me a few iterations to realize what’s actually needed (initially I had way too many extra elements to needlessly saveguard execution) but eventually I came up with this:

How to Mock a Mockingbird, Graphically

Posted by: kram1032 on December 19, 2016 2:49 PM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

Hi kram1032, that’s nice! Can you explain a bit how this worksheet implements the SKI calculus?

Posted by: Jamie Vicary on December 19, 2016 5:45 PM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

If you want you can try following along. Let’s try the following: All the elements you need to build any SKI combinator expression can be found in the 3-Cells. Specifically, only the first four, S, K, I and Branch will be needed. The other two occur automatically during evaluation.

Let’s build a simple test-case expression:
- Click on “Branch”. A t-junction with one end on top and two on the bottom will appear. Click on the bottom left end just inside the border of the image. Select “S Combinator”. The t-junction will now have a blue leaf. Next, click on the right branch and find an I-combinator to add a green leaf. After that, by clicking on the right side of the image, you can add another wire. Click between the two wires on the top and select branch. Click on the lose end on the bottom and add another I combinator. Click on the right end again to add another wire and at the top to connect the top two wires with another Branch.
At this point you are looking at a Mockingbird. It will repeat what ever you put into it. It’s just waiting for another bird to mock. And what better bird to mock than another Mockingbird?
Click on the bottom loose end to add a Branch. On its left end, add another Branch. And on the three loose ends, from left to right, add an S-, I- and I-combinator.

What you are looking at here is the famous infinite loop of two Mockingbirds about to mock each other:

Two Mockingbirds

This is already in evaluation order. When hovering over individual pieces you can confirm that: - the blue vertices are S combinators. - the green vertices are I(dentity) combinators. In this particular diagram there are no K combinators. They would be red.

  • the grey vertices are branching points. You can also think of these as parentheses, sort of. They force the evaluation order and also are crucial for applying S-, K-, and I-moves. Evaluation order is depth-first from left to right, if you bring the diagram into the standard form as seen in the image. So what you are looking at in this tree is: a Mockingbird SII acting on a Mockingbird SII like so: SII(SII).

I combinators take a single input that they return unchanged. Effectively all they do is remove the branch they are attached to.
K combinators take two inputs and return the first (so they delete the second.)
S combinators take three inputs, copy the third and apply it to the first and then the second.

At this point, just to get a history of what’s happened, it might be a good idea to click on Identity or just press I on your keyboard.

So, since in the above diagram this is going to be the first move that happens, let’s look at how an S move looks like in this diagram:

First, how things need to look to apply the move: S-move start

You can see here how the move can be applied whenever an S combinator is directly next to three branches at once. These are its three inputs. Now let’s apply this move. (This can be done simply by clicking on the S-combinator. If it happens to not work, make sure your tree is arranged in precisely this form! Globular doesn’t know isomorphisms. Gotta put the work of rearranging in yourself.)

S-move done

Okay, this looks a bit messy. But remember, the bottom three lines are the inputs. So just follow along upwards and see what happens. Go back and forth in time (click up and down in the second Slice field) to get a feeling for what just changed.
First, look at the right-most wire. That upside-down branch is actually a copy node. It will copy what ever is below it. Crucially, it is NOT an inverse of the Branch node and as such will NOT cancel out. It wouldn’t work if that was the case. Its right copy stays on the right side. Its left copy, however, crosses over the second input. If you remember the evaluation order that means, first the left input is evaluated, then the left copy of the right input:
Sxyz = xz(yz) - that’s exactly what’s going on here!

Furthermore you have the two remaining I combinators, but look, one of them is all tangled up! So let’s first move the left I combinator all the way (three times) up to the branch vertex, then click it. In accordance to its rule, it will have deleted its branch. Once again, if you need more time to appreciate the change, go back and forth on the Slice counter.

Next, let’s move the other I combinator up. At the crossing, drag it to the top-right. At that point it will once again be in position to be applied, so let’s do that.

At this point you get what looks kind of weird, but it really is where the magic happens. Once you have an intuitive understanding of these graphs you’ll see exactly what’s going to happen from hereon out. First, a branch and a copy node come directly together, forming a loop. You might be tempted to assume the two could cancel out, but no, the copy node only ever moves down and can’t interact at all with any vertex above it.
So when you click on it, it will actually copy the branch below it. The result is a little messy if you aren’t used to it, though not nearly as bad as the mess the S-combinator initially caused. Once again go back and forth in time and also follow the wires carefully to really see what’s happening: The copy vertex turned our one branch into two along each of which flows another copy branch. The left branch’s right copy crosses over to become the right branch’s left copy and vice versa. This way, once copy is done, there will be a perfect copy of the entire initial branch.

So let’s go on moving the left copy process along. Once again it copies a branch, spawning two more copy nodes in the process. Next you could copy the S combinator and finally finish one of the branches. After that, move the left remaining copy down twice and click it once more. Only one copy process to go but let’s untangle the the wires on the left first. Move the intersection down and the S-combinator across.
After that, let’s drag the copy node all the way down to copy. From here on out all that’s left is some untangling and you’ll soon be back to where it all began. The second mockingbird was perfectly mocked by the first which, thus, turned into yet another mockingbird. It can repeat the process all over.

Since this process didn’t feature K-nodes at all, for completeness sake I will also show you what happens with there. First, the setup when it can be applied: In the 4-cells, find the cell called “apply K”. What you get will look nothing like what the two pictures suggest. The reason for that is that the Projection level is automatically set to 2 (so 2 dimensions are dropped.) To fix that, lower it to 1.

K-move setup

By advancing the Slice-counter by 1 you can see what happens if you apply the move.

K-move applied

Technically, at the end of that right wire, there is a vertex but it is black. I thought that works well given that it symbolizes what’s happening: This wire is now dead. Every time you click on its end when right above another node, it will delete what follows below. That’s what K does: Given two inputs, it returns the first. The second one is just discarded.
If you’d rather be able to actually see the Eat vertex, you can easily change its color by finding “Eat” in the 3-Cells and click on the color field reading 000000. Pick your favorite color. I’ll ask for more feedback first but if I find this to be a common concern I’ll just upload a new version with such a change myself.

And finally, if you want to play around with this some more, say, if you want to start simulating untyped lambda calculus or the like, or if you want to recreate all the species in the book “How to Mock a Mockingbird”, there is plenty of literature available online. Just search for that title or SKI combinator calculus. It won’t take long to find some examples to try and replicate.

Posted by: kram1032 on December 19, 2016 11:24 PM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

Yes, this is quite nice, but I would urge changing colors here and there. In particular, you have morphisms such as “eat” that are black on a black background. If you click on the color pallet and then click a color choice, this will change all instances of that color.

Posted by: Scott Carter on December 19, 2016 6:24 PM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

I added an extra rule (eating copied branches) and while I was at it I reworked the colors a bit. Do you like this better? updated version

Posted by: kram1032 on December 22, 2016 12:35 AM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

I hadn’t seen the comment that eat was black since it was a type of ground state. So yeah, I like it better now. I am unfamiliar with the SKI calculus. I think I saw something on the arXiv about it recently, but only skimmed the paper. can you say a few words about it?

Posted by: Scott Carter on December 22, 2016 2:14 AM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

Well, to be honest, I’m hardly an expert. Really I just wanted to do something simple to test out / learn Globular and having seen another demo somebody did (“Arithmetic” somewhere in the Gallery) I thought this might work out nicely. Currently I’m also working on something slightly more sophisticated, SF-calculus, directly based on a paper. I’ll publish that once I’m content with it. In any case, I think I learned about as much about Combinators as about Globular while doing this.

That being said, let me try: Combinator calculi and combinatory logic are able to do (untyped - though from what I understand you can add typing to it) intutionistic logic without ever mentioning quantified variables, i.e. in point-free style. For instance, and to show that it is Turing complete, you can easily boolean logic in the most common flavors. They are very minimal systems though. Kind of an assembly language of logic with at minimum just as few as two symbols (the so-called iota-combinator and an application symbol) though usually more are used. The most common flavors are the SK and SKI calculi with the following rules:

  • Ix = x (it’s often called the “Idiot bird”)
  • Kxy = x (it’s called a “Kerstel”)
  • Sxyz = xz(yz) (this one is referred to as “Sterling”)

First, note that “I”, the identity operator, is merely a convenience addition. You get the same behavior by substituting I for SKK:

SKKx = Kx(Kx) = x

Next, let’s try Boolean logic: As you saw, K returns the first of its two arguments. That makes it very useful for this purpose. You can write another function (two slightly different ones in fact) that rather returns the second argument.

  • KIxy = Iy = y
  • SKxy = Ky(xy) = y

Either choice works just fine.

You can use this in multiple ways: K takes the role of True, KI (in SKI calculus that tends to be the default choice) the role of false, and you can use this to build if then else:

KK(KI) says “if true = true, then true, else false” and results in true. KIK(KI) says “if true = false, then true, esle false” and results in false.

Furthermore, let’s find and, or and not:

  • not x = x(KI)K
  • x and y = xy(KI)
  • x or y = xKy

if you substitute our truth values in there, you can see that this works as desired. For instance, for not:

K(KI)K = KI KI(KI)K = IK = K

Finally, you can also define arbitrary recursive loops in SKI calculus. There is a combinator, typically called the Mockingbird, that repeats anything you throw at it:

SIIx = IxIx = xx

and if you throw it at itself, you just might be able predict what’s going to happen:


This combinator often gets its own symbol, M for Mockingbird.

Using it and a bunch of other useful constructs you can define another combinator, typically called the Why-bird and abreviated Y, and it returns anything you throw at it indefinitely: Yx =x(Yx) - so it’s a fixed point combinator.

All these silly bird names come from Raymond Smullyan’s 1985 classic “To Mock a Mockingbird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic” which is freely available online.

Now, if you check my published Globular workbook, you’ll find that there are three more building blocks: Branch, Copy and Eat. Copy and Eat are technically not combinators, rather they only occur as in-between steps while evaluating combinators:
K deletes its second input, so it caps that branch with Eat which then consumes everything below one by one
S copies its third input, so it spawns Copy which runs down the wire symbol by symbol like a zipper and, well, copies each vertex.
Incidentally S also reorders the wires which is why I had to go to level 3 to implement this. The wire crossover move, as far as I can tell, would have been impossible to do on level 2.
Finally, Branch is there to start parentheses or, equivalently, it’s the application operator. Each of the combinators only can be applied if the appropriate number of Branch vertices are adjacent. For I that’s just one, but K needs two and S needs three.

If you’d like to experiment a bit with it, you can try implementing your own combinators and seeing how they act. I actually ended up doing that a lot in the upcoming SF-combinator version. (F is a rather new combinator which allows the combinators to express equality within the system rather than resorting to metatheory. This was not possible in the older systems like SK and BCKW calculi)

To implement your own combinators you can either implement their behavior directly (adding them to your base set) or you can add substitution rules and then prove the results. For instance, take the Mockingbird M:

  • Add a new combinator (click on the 0-cell, press I(dentity) twice, press S(ource), click on the 1-cell, press T(arget))

First, let’s look at the base element approach:

  • check what behavior M has:
  • Mx = xx
  • First, observe that it takes just one input
  • so click on the M-combinator to get a copy of it,
  • then click to the right of it to add another wire,
  • and designate it as input by connecting the two wires with a Branch.
  • take this as Source
  • now let’s think about how to replicate the behavior:
  • it takes one input and returns it twice
  • therefore, Copy is a good candidate
  • but copy gives two outputs. We only want one.
  • simplest solution: cap with a Branch
  • Set as target.
  • also add the abilities to Eat and Copy the combinator in the obvious ways.

This turns out to be the correct behavior, but you can also prove that this it was it does if you instead specify substitution rules:

  • Remember that M = SII
  • Set a lone M as Source
  • Click on S
  • Add two wires to the right
  • first on the middle, then on the right wire, add an I
  • add a Branch to the left pair
  • add a Branch to the remaining pair
  • Set as target
  • optionally make it invertible

Once you did that you can prove all three M-rules, application, copy and eat, just from this substitution. All of them work in the same basic way. Let’s go through the application case:

  • Click on M
  • add a wire to its right
  • add a Branch on top
  • Press I(dentity)
  • Click on the M in the frame to apply your substitution move
  • Click on the resulting S to evaluate
  • Rearrange the wires until you can apply each I combinator
  • At that point you should be at the same configuration as we previously defined directly. If not, keep rearranging (and find superfluous moves one Projection level higher)
  • QED. Press Theorem

So to summarize, we just proved that, given the basic behaviors of our predefined S and I combinators, M behaves by taking a wire and inserting a loop (a Branch and a Copy) into it. The same can be done to prove that M can be consumed by Eat and copied by Copy.

For suggestions for useful combinators, try This (especially useful are the Bluebird, Cardinal, Mockingbird, Lark and Why Bird - though it’s easier to define them hierarchically rather than going with the lenghty base forms in SK-combinators)

or check out To Mock a Mockingbird, starting at chapter 9

And finally, Here is an first attempt by Conor McBride to rewrite an inconsistent version of Martin Löf’s Type Theory into Combinator Calculus Not sure if that ever went anywhere though. I couldn’t find any followup from the following 4 years.

Posted by: kram1032 on December 23, 2016 1:34 PM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

In case this analogy helps anyone:

combinatory logic (SKI) : Hilbert system :: lambda-calculus : natural deduction

It was kind of a revelation to me when I realized it.

Posted by: Mike Shulman on January 1, 2017 12:11 PM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

The explanation is in the abstract of the project though if you want more details I can try explaining it better. Check out the 5-cell on projection level 1 and step through it to see an example of how it works. The colors are actually on purpose like they are: I thought it’s kind of appropriate for “Eat” to look like it’s, well, “eating” the wire. But it’s easy enough to change. If you think it’d be better having it, say, dark gray, or something else entirely, I’ll upload a third version. (By the way, there already is a second version but the only difference is that I fixed a few typos in the abstract. There doesn’t seem to be a way to modify an abstract after it’s saved for some reason)

Posted by: kram1032 on December 19, 2016 9:34 PM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

oops, that was meant as a reply…

Posted by: kram1032 on December 19, 2016 9:35 PM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

Hi Scott,

It’s great to read these posts of yours, and to revisit that spun trefoil whose image you kindly let me use.

I remember you telling me it could take up to 3 hours to generate some of your diagrams. I wonder if Globular can speed things up.

Can you prove that this is knotted?

I was posing the question on the nForum as to what kinds of result Globular can establish. I was thinking that equality of knots is possible, but not inequality.

More generally, I wonder what there is to say about the strength of Globular as a system in which to prove results about some algebraic entity (e.g., kind of monoidal category) via manipulation of the initial topological term model.

Posted by: David Corfield on December 20, 2016 11:49 AM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

Hi David,

Certainly, now globular speeds things up immensely. Since I have created knotted and braided surface templates, I expect that not only new 2-knots, but also higher dimensional knots can be created quite quickly. The aesthetics are not within globular yet, but I anticipate that they will come with time. Also since globular automatically creates the cross sections of a movie, I can then import them into a drawing program and then use them to trace the knots that I want. Still my drawing technology was fast converging with Jamie’s globular technology. In particular, I was starting to draw things in standard sizes, using atomic pieces. Globular does exactly this!

Posted by: Scott Carter on December 22, 2016 1:50 AM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

That’s interesting, since what I had always liked about your pictures is how naturalistic and unlike Globular’s pictures they are!

Posted by: Jamie Vicary on January 4, 2017 10:17 PM | Permalink | Reply to this

Re: Globular for Higher-Dimensional Knottings (Part 2)

My question, “Can you show that this is knotted?” currently requires human intervention. Jamie and I had discussions about how to create within some globular worksheets a way of computing invariants, but the discussions were in a very short basement at a very loud party.

Posted by: Scott Carter on December 22, 2016 1:52 AM | Permalink | Reply to this

Post a New Comment