Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Can we make an n-category of "towers and instructions"?

David Egolf (Oct 07 2023 at 18:05):

I was watching "This Week's Finds 12: the periodic table of n-categories" (see also #general: events > This Week's Finds seminar ). A few minutes in, there is a question from the audience along the lines of "What are some examples of n-categories?". Trying to think of some additional example (besides the ones that John Baez gives in his answer during the seminar), I had what seems like a fun idea - and I'm curious if we can actually get an $n$-category (hopefully for $n \geq 2$) from it.

Here's the idea. The objects of our n-category are to be towers made out of building blocks. The blocks are square, 2-dimensional, and are all the same size. Every block must be on top of another block, or resting on "the ground". Some examples of towers look like this:

three towers

For convenience, we might wish to label the blocks, so that we can easily talk about a specific one. A labelled block tower might look like this:
a labelled tower

Note that for any block, a tower contains the information that can be used to answer the following questions:

• Is there a block directly above this block?
• Is there a block directly to the left of this block?
• Is there a block directly to the right of this block?
• Is there a block directly below this block?

So, a tower of blocks is more than just a way to draw a set: we have "spatial" relationships between the different blocks of a tower.

Next, I roughly describe what 1-morphisms are to be between our block towers. A 1-morphism $f: a \to b$ is a list (ordered set) of instructions, that tells us how to build the tower $b$ from the tower $a$. We don't require this list of building instructions to respect labelling of the blocks - the labelling is just for convenience. Intuitively, the list of instructions provides a way to "adjust" tower $a$ to form tower $b$: we don't require the instructions to build tower $b$ from scratch.

Each list of instructions is (roughly) of the following form: take a block currently not under any block, and move it to a position specified relative to another block, so that it rests on a block or on the ground. We also allow for empty lists of instructions (which I think provide the identity 1-morphisms). Here is an example list of instructions, which builds the tower on the right from the tower on the left:

start and finish towers

Here is one possible list of instructions to build the tower on the right from the one on the left:

1. place block $c$ on top of block $a$

Here is another possible list of instruction:

1. place block $a$ on top of block $c$
2. place block $b$ on top of block $a$

Composition of 1-morphisms is to be by concatenation of lists. I think this should be associative, so that we get a 1-category.

To define two-morphisms, the rough idea is to consider list of instructions (which I will call "edits") so that an edit $e: f \to g$ modifies the list of instructions $f$ until it becomes the list of instructions in $g$. I'm not sure what kind of "editing commands" should be allowed so that we get a 2-category (e.g. we need the interchange law to hold). But the rough idea I had in mind is that we could possibly have editing commands along these lines:

• rearrange building commands (e.g. do what used to be step 3 after what used to be step 4)
• delete building commands (e.g. don't do what used to be step 2)
• change the destination of a block in a building command (if possible)
• change the source of a block in a building command (if possible)
• add a new building command

The idea is then to continue upwards in this fashion. So a 3-morphism would be a list of commands that gradually changes one edit to another edit. And a 4-morphisms would be a list of commands that gradually changes one 3-morphism to another 3-morphism.

Can we actually get an $n$-category (for some arbitrarily large $n$) along these lines? More broadly, is there some kind of $n$-category of things, lists of instructions, lists of instructions between lists of instructions, lists of instructions between (lists of instructions between lists of instructions) and so on?

Morgan Rogers (he/him) (Oct 08 2023 at 09:58):

I like this idea @David Egolf ! Categories whose morphisms are "algorithms" of some kind are common in computer science contexts, but I love the constrained nature of these block manipulation recipes; they're almost like puzzles. It seems to me that you should indeed be able to make a higher category out of these, but it's not clear yet whether it's possible for arbitrary $n$ (or at least, possible in an interesting way - after all, any $n$-category is also an $(n+1)$-category where the $(n+1)$-morphisms are all identities). In case you've heard of lambda calculus, in that context we can think of lambda-terms as 1-morphisms, $\beta$-reductions as 2-morphisms, and re-orderings of $\beta$-reductions as 3-morphisms, and there might even be some $4$-morphism structure, but that structure gets progressively less complex as we go higher.

To understand whether the morphisms 'keep going up' in your context, you need to compare the 2-morphism level with the 1-morphism level. Did you notice that the instructions are constrained in a similar way that the blocks are? In your simple example, we can't move block $b$ until we have moved block $a$, so it's like the former instruction is trapped underneath the latter. Can you present a 1-morphism as some variant of a block tower? Do the 2-morphisms correspond to rearrangements of these?

A hard part when thinking about this might be choosing coordinates and defining boundary constraints. Do the instructions select a specific block, or a block in a specific position in the tower (in the context of rearranging instructions)? When moving your block labelled $c$, am I allowed to move it to any column, or only one adjacent to a block? Am I allowed to have disconnected blocks? If not, am I not allowed to move a block which connects two towers?

I think you could tune the choices of answer here to make a bunch of different, related categories - and your idea extends to more dimensions (cube, hypercube...) too! It's a cool idea, I encourage you to keep digging :star_struck:

David Egolf (Oct 08 2023 at 19:34):

Thanks @Morgan Rogers (he/him) for your encouraging and interesting response! Today I need to take a rest from math (for health reasons), but hopefully in the coming days I can think a bit more about this.

John Baez (Oct 10 2023 at 08:51):

David Egolf said:

To define 2-morphisms, the rough idea is to consider list of instructions (which I will call "edits") so that an edit $e: f \to g$ modifies the list of instructions $f$ until it becomes the list of instructions in $g$. I'm not sure what kind of "editing commands" should be allowed so that we get a 2-category (e.g. we need the interchange law to hold). But the rough idea I had in mind is that we could possibly have editing commands along these lines:

• rearrange building commands (e.g. do what used to be step 3 after what used to be step 4)
• delete building commands (e.g. don't do what used to be step 2)
• change the destination of a block in a building command (if possible)
• change the source of a block in a building command (if possible)
• add a new building command.

Nice idea. One problem I see is that in a 2-category a 2-morphism $\alpha : f \Rightarrow g$ can only go between morphisms with the same source and same target: $f, g : x \to y$. If you 'edit' a sequence of commands corresponding to some morphism $f: x \to y$ in the ways you describe, you'll typically get some morphism $f: x \to y'$ with $y' \ne y$. Right?

John Baez (Oct 10 2023 at 08:51):

You may wind up wanting to use a double category instead of a 2-category.

David Egolf (Oct 11 2023 at 18:45):

John Baez said:

Nice idea. One problem I see is that in a 2-category a 2-morphism $\alpha : f \Rightarrow g$ can only go between morphisms with the same source and same target: $f, g : x \to y$. If you 'edit' a sequence of commands corresponding to some morphism $f: x \to y$ in the ways you describe, you'll typically get some morphism $f: x \to y'$ with $y' \ne y$. Right?

Thanks for your response!

Let's assume that $f: x \to y$ is a 1-morphism. So, it is a sequence of instructions that adjust the tower $x$ until it becomes the tower $y$. If we then "edit" this sequence of commands, we are in general going to get a sequence of instructions that produce a different tower $y' \neq y$. However, as you note, in a 2-category a 2-morphism can only go only between two morphisms with the same source and target. I think the 2-morphisms I had in mind were "edits" that take a morphism $f: x \to y$ and produce a morphism $g: x \to y$. So, we take one way of adjusting tower $x$ to form tower $y$, and modify it to get another way of adjusting tower $x$ to form tower $y$. In this case, the "edit" is going between two 1-morphsims with the same source and target.

Depending on what one wanted to do, one could consider more general edits, that convert a 1-morphism to a new 1-morphism with potentially a different target. But that sounds more complex!

David Egolf (Oct 11 2023 at 19:17):

Morgan Rogers (he/him) said:

I like this idea David Egolf ! Categories whose morphisms are "algorithms" of some kind are common in computer science contexts, but I love the constrained nature of these block manipulation recipes; they're almost like puzzles.

I did not know that categories having morphisms as "algorithms" are common in computer science. That is very interesting to learn!

Regarding the constrained nature of the block manipulation recipes, I felt I had to introduce some constraints based on relative block positions. Otherwise, the nature of the block towers (where blocks have relative positions) would not be reflected in the way that the morphisms compose. And it does feel puzzle like, as I discovered when trying to provide some examples in my post above!

It seems to me that you should indeed be able to make a higher category out of these, but it's not clear yet whether it's possible for arbitrary $n$ (or at least, possible in an interesting way - after all, any $n$-category is also an $(n+1)$-category where the $(n+1)$-morphisms are all identities). In case you've heard of lambda calculus, in that context we can think of lambda-terms as 1-morphisms, $\beta$-reductions as 2-morphisms, and re-orderings of $\beta$-reductions as 3-morphisms, and there might even be some $4$-morphism structure, but that structure gets progressively less complex as we go higher.

I have heard of lambda calculus, and $\beta$-reduction, although I haven't worked with them enough to understand them properly.

I'm trying to remember roughly how this goes, to try and roughly understand what you are saying:

• A $\lambda$-term is like(?) a function. For example, we might have a $\lambda$-term $\lambda x [x^2 + 3]$, which I think denotes some function $x \mapsto x^2+3$. Although it feels like we might need to specify the source and target of this function? Or maybe the this function just produces a syntactic expression that we don't necessarily "collapse" to a single number by carrying out arithmetic operations?
• $\beta$-reduction I think is intuitively the process of taking a $\lambda$-term and "plugging" in some value. I see that people write $(\lambda x[M])N = M[x \coloneqq N]$. I think the idea is we have some expression $M$ in $x$, and we can provide the input $N$ to get the expression $M[x \coloneqq N]$ where every occurrence of $x$ has been replaced by an occurrence of $M$.

Clearly I would need to do more work to understand these concepts properly. However, with my current level of understanding, I don't quite see how a particular $\beta$-reduction can be viewed as a morphism between two $\lambda$-terms. Is the idea to view the output of $\beta$-reduction as a $\lambda$-term, somehow?

I'm also unsure how this (interesting) mention of lambda calculus relates to the block towers. A $\lambda$-term (which I'm thinking as a function) seems rather different than a sequence of building instruction! But I'm guessing you have some connection in mind.

To understand whether the morphisms 'keep going up' in your context, you need to compare the 2-morphism level with the 1-morphism level. Did you notice that the instructions are constrained in a similar way that the blocks are? In your simple example, we can't move block $b$ until we have moved block $a$, so it's like the former instruction is trapped underneath the latter. Can you present a 1-morphism as some variant of a block tower? Do the 2-morphisms correspond to rearrangements of these?

I agree that we can only do certain instructions under certain conditions. Sometimes, we might have to perform a certain instruction before we can perform another one. I'm trying to understand how you are connecting this idea to the idea that we can view a 1-morphism as a sort of block tower. I guess the idea is that a 1-morphism is a sequence of commands, and we can consider which of those commands are "trapped" under other commands - in the sense that they can't be executed until other commands in that sequence are executed. This seems interesting, but I think I'm not quite following what you have in mind. For example, when trying to view a 1-morphism as a sort of block tower, I'm not sure how one would incorporate the fact that a 1-morphism is a sequence of instructions, not just a set of instructions.

A hard part when thinking about this might be choosing coordinates and defining boundary constraints. Do the instructions select a specific block, or a block in a specific position in the tower (in the context of rearranging instructions)? When moving your block labelled $c$, am I allowed to move it to any column, or only one adjacent to a block? Am I allowed to have disconnected blocks? If not, am I not allowed to move a block which connects two towers?

I think you could tune the choices of answer here to make a bunch of different, related categories - and your idea extends to more dimensions (cube, hypercube...) too! It's a cool idea, I encourage you to keep digging :star_struck:

Yes, there are many variants possible! Honestly, it seems a bit overwhelming. I find it dissatisfying to have to make an arbitrary choice to narrow down a collection of possible constructions to one particular one. But to think more about this idea, one would have to make some choices to get a specific category! As you indicate, it could also be interesting to see how the resulting categories under different choices are related to one another.

Jean-Baptiste Vienney (Oct 11 2023 at 19:26):

I'll try to answer some of your questions on $\lambda$-calculus. But I'm not an expert so I'll let others correct me or give more details.

Jean-Baptiste Vienney (Oct 11 2023 at 19:38):

David Egolf said:

A $\lambda$-term is like(?) a function. For example, we might have a $\lambda$-term $\lambda x [x^2 + 3]$, which I think denotes some function $x \mapsto x^2+3$. Although it feels like we might need to specify the source and target of this function?

The category-theoretic understanding of $\lambda$-calculus is mainly the understanding of typed $\lambda$-calculus and not all $\lambda$-calculus (although it is also related to category theory, but in a more complicated way as far as I know).

You can specify the source and the target of $\lambda$-terms, sometimes but not always. The terms such that you can specify the source and the target are named typable. For instance $\lambda x.x$ is typable with type $A \rightarrow A$ or $B \rightarrow B$ etc... So it can have several types. This is the Curry-style typing.

You also have the Church-style typing. In this philosophy, you precise the type of the variables, and then a $\lambda$-term has at most one type. For instance you write $\lambda x^A.x$ and this $\lambda$-term has only on type which is $A \rightarrow A$. Here you speak of typed $\lambda$-terms.

Jean-Baptiste Vienney (Oct 11 2023 at 19:39):

Let's use the Curry-style. So that we will speak of typable and non-typable $\lambda$-terms.

Jean-Baptiste Vienney (Oct 11 2023 at 19:39):

Some $\lambda$-terms are not typable.

Jean-Baptiste Vienney (Oct 11 2023 at 19:41):

For instance $(\lambda x.(x)x)(\lambda x.(x)x)$ is not typable

Jean-Baptiste Vienney (Oct 11 2023 at 19:45):

David Egolf [said]

$\beta$-reduction I think is intuitively the process of taking a $\lambda$-term and "plugging" in some value. I see that people write $(\lambda x[M])N = M[x \coloneqq N]$.

>
>

Jean-Baptiste Vienney (Oct 11 2023 at 19:46):

People don't exactly write that. They write $(\lambda x[M])N =_\beta M[x \coloneqq N]$ or better $(\lambda x[M])N \rightarrow_\beta M[x \coloneqq N]$.

Jean-Baptiste Vienney (Oct 11 2023 at 19:48):

$\lambda$-terms are programs, when they are executed, the execution consist of steps which are ordererd in the time. The notion of computation is oriented contrary to equality. The execution consists in using $\rightarrow_\beta$ as much as you can until there is no longer any reduction to perform.

Jean-Baptiste Vienney (Oct 11 2023 at 19:49):

Of course it doesn't always finish, sometimes the program doesn't terminate. But hopefully, if the $\lambda$-term is typed, then the program always terminate.

Jean-Baptiste Vienney (Oct 11 2023 at 19:51):

That's a reason why typed functional programming language are useful. By using types, it's easier to ensure that your programs are going to terminate.

Jean-Baptiste Vienney (Oct 11 2023 at 19:52):

David Egolf said:

Clearly I would need to do more work to understand these concepts properly. However, with my current level of understanding, I don't quite see how a particular $\beta$-reduction can be viewed as a morphism between two $\lambda$-terms. Is the idea to view the output of $\beta$-reduction as a $\lambda$-term, somehow?

>
>

Jean-Baptiste Vienney (Oct 11 2023 at 19:53):

Here is how you obtain a $2$-category from $\lambda$-terms:

Jean-Baptiste Vienney (Oct 11 2023 at 19:54):

I'm sorry but now I'm going to use the Church-Style so that types are assigned to the variables $x,y...$

Jean-Baptiste Vienney (Oct 11 2023 at 19:55):

It will be easier because like this, hom-sets will be disjoints if the input and output are different.

Jean-Baptiste Vienney (Oct 11 2023 at 19:56):

First let's precise what is a type.

Jean-Baptiste Vienney (Oct 11 2023 at 19:56):

A type is something obtained by starting with letters $A,B,C...$ and then using a connector $\rightarrow$

Jean-Baptiste Vienney (Oct 11 2023 at 19:57):

For instance $A$, $A \rightarrow A$ or $(A \rightarrow A) \rightarrow (A \rightarrow A)$ are types.

Jean-Baptiste Vienney (Oct 11 2023 at 19:58):

In the basic typed $\lambda$-calculus this is all the types you have

Jean-Baptiste Vienney (Oct 11 2023 at 19:59):

People often say "typed $\lambda$-calculus" = "cartesian closed categories" but this is a bit wrong because you don't have products in the basic typed $\lambda$-calculus" (although you could add them)

Jean-Baptiste Vienney (Oct 11 2023 at 20:01):

Clearly you want that the homset $\mathcal{C}[A,B]$ where $A$ and $B$ are two types to be the set of all lambda terms of type $A \rightarrow B$

Jean-Baptiste Vienney (Oct 11 2023 at 20:02):

You need a bit more than a mere category to be able to deal with your types.

Jean-Baptiste Vienney (Oct 11 2023 at 20:02):

First how to interpret a $\lambda$-terms of type $A$ ?

Jean-Baptiste Vienney (Oct 11 2023 at 20:02):

It looks loke something with an output type but without an input type.

Jean-Baptiste Vienney (Oct 11 2023 at 20:03):

That's why we need a terminal object $\top$.

Jean-Baptiste Vienney (Oct 11 2023 at 20:03):

We will interpret a $\lambda$-term of type $A$ as a morphism in $\mathcal{C}[\top,A]$

Jean-Baptiste Vienney (Oct 11 2023 at 20:04):

Now hoe to interpret a $\lambda$-term of type $A \rightarrow (A \rightarrow B)$?

Jean-Baptiste Vienney (Oct 11 2023 at 20:05):

We need an internal hom-set

Jean-Baptiste Vienney (Oct 11 2023 at 20:05):

ie. a way of obtaining an object of type $A \rightarrow B$ from two objects $A,B$

Jean-Baptiste Vienney (Oct 11 2023 at 20:06):

That's why the good categorical structure is a closed category (I will use $\rightarrow$ for the internal hom-set)

Jean-Baptiste Vienney (Oct 11 2023 at 20:07):

And we will interpret a $\lambda$-term of type $A \rightarrow (A \rightarrow B)$ as a morphism in $\mathcal{C}[\top,A \rightarrow (A \rightarrow B)]$ for instance

Jean-Baptiste Vienney (Oct 11 2023 at 20:11):

Now, the $2$-morphisms correspond to $\beta$-reduction

Jean-Baptiste Vienney (Oct 11 2023 at 20:14):

For instance there is a $2$-morphism $(\lambda x^A.x)y^A \in \mathcal{C}[\top,A] \Rightarrow y^A \in \mathcal{C}[\top,A]$

Jean-Baptiste Vienney (Oct 11 2023 at 20:16):

Types don't change when you $\beta$-reduce so that you really obtain a $2$-category

Jean-Baptiste Vienney (Oct 11 2023 at 20:17):

I gave you the main ideas I think...

Jean-Baptiste Vienney (Oct 11 2023 at 20:47):

Ooh, what I said is a bit incomplete, you need to add products.

Jean-Baptiste Vienney (Oct 11 2023 at 20:48):

In fact "typed $\lambda$-calculus" (the basic one) = "cartesian closed categories" is really true.

John Baez (Oct 11 2023 at 22:46):

David Egolf said:

• A $\lambda$-term is like(?) a function.

It is like a function, but - to connect up with another aspect of this conversation - it's even more like an algorithm, or program, that computes a given function. Different $\lambda$-terms can compute the same function... and some $\lambda$-terms can fail to "halt", and don't compute anything.

John Baez (Oct 11 2023 at 22:49):

A nice motto is that "Turing machines are a simple model of hardware, while the lambda-calculus is a simple model of software". They were both developed at roughly the same time by people trying to understand what it means to compute. Turing developed Turing machines (obviously) and Church developed the lambda-calculus. Once it was discovered they compute the same class of functions, the Church-Turing thesis claimed that these were all the functions that could be computed by any systematic method whatsoever.

John Baez (Oct 11 2023 at 22:50):

Later the lambda-calculus was found to have deep connections to category theory - in particular, cartesian closed categories.

Mike Shulman (Oct 11 2023 at 23:05):

John Baez said:

and some $\lambda$-terms can fail to "halt", and don't compute anything.

But, importantly, all the typed $\lambda$-terms (in ordinary typed $\lambda$-calculus, anyway) do halt and compute something.

Mike Shulman (Oct 11 2023 at 23:09):

Jean-Baptiste Vienney said:

People often say "typed $\lambda$-calculus" = "cartesian closed categories" but this is a bit wrong because you don't have products in the basic typed $\lambda$-calculus" (although you could add them)

While hoping not to confuse the people still learning about this stuff, I feel obliged to quibble with this a bit. You may not have product types in the basic typed $\lambda$-calculus (although I think there's room for quibbling about what "basic" means too), but products are implicitly present in the fact that there can be multiple typed variables in the context. So you can set up a syntax-semantics correspondence between STLC and CCCs, and people often do. Although I agree that it's more faithful to the syntax to consider instead some categorical structure that distinguishes product types from concatenation of contexts, such as a cartesian multicategory.

David Egolf (Oct 12 2023 at 01:10):

Thanks @Jean-Baptiste Vienney for your explanation!

Jean-Baptiste Vienney said:

Let's use the Curry-style. So that we will speak of typable and non-typable $\lambda$-terms.

I guess this is pointing out that I don't really know exactly what it means to "type" something. It seems surprising (to me) to talk about a non-typable program, which I am intuitively trying to understand as a program where one can't talk about the "kind" of things that are inputs or outputs of a program. If nothing else, I would have thought we could assign some kind of minimally descriptive type like "thing" to the input and output, so we can say that a program always takes "things" as inputs and provides "things" as outputs.

David Egolf (Oct 12 2023 at 01:13):

Jean-Baptiste Vienney said:

$\lambda$-terms are programs, when they are executed, the execution consist of steps which are ordererd in the time. The notion of computation is oriented contrary to equality. The execution consists in using $\rightarrow_\beta$ as much as you can until there is no longer any reduction to perform.

Ah, understanding $\lambda$-terms as programs helps me better understand why @Morgan Rogers (he/him) was mentioning these in the context of the 1-morphisms described above. (The 1-morphisms above are a sequence of instructions to move blocks around - and this sounds a lot like a program).

David Egolf (Oct 12 2023 at 01:21):

Jean-Baptiste Vienney said:

We will interpret a $\lambda$-term of type $A$ as a morphism in $\mathcal{C}[\top,A]$

This is interesting, but I would have thought that a morphism in $\mathcal{C}[\top,A]$ should have type $\top \to A$, not a type of $A$. I'm also wondering what makes the terminal object $\top$ special, so that we use it when viewing $\lambda$-terms of type $A$ as morphisms (e.g. why not use any other object, or say an initial object?).

On a related note, imagine we have a $\lambda$-term of type $A \to B$. Then do we model this as a morphism from type $A$ to type $B$, and also as a morphism from type $\top$ to type $A \to B$?

Jean-Baptiste Vienney (Oct 12 2023 at 01:24):

David Egolf said:

Thanks Jean-Baptiste Vienney for your explanation!

Jean-Baptiste Vienney said:

Let's use the Curry-style. So that we will speak of typable and non-typable $\lambda$-terms.

I guess this is pointing out that I don't really know exactly what it means to "type" something.

To type a $\lambda$-term, you must use logic! Actually, a very simple logic, whose inference rules can be presented like this:
Screenshot-2023-10-11-at-9.23.17-PM.png

Jean-Baptiste Vienney (Oct 12 2023 at 01:26):

You start by using (Ax), where $\Gamma$ is a list of variables with a type for instance $\Gamma = x:A, y:B, z:B$

Jean-Baptiste Vienney (Oct 12 2023 at 01:27):

And you build your proof by using also the other rules

Jean-Baptiste Vienney (Oct 12 2023 at 01:28):

For instance, you can prove $x:A \vdash \lambda x.x : A \rightarrow A$

Jean-Baptiste Vienney (Oct 12 2023 at 01:28):

It means: if $x$ is of type $A$, then $\lambda x.x$ is of type $A \rightarrow A$

Jean-Baptiste Vienney (Oct 12 2023 at 01:29):

It's easier to write proofs by starting from the conclusion.

Jean-Baptiste Vienney (Oct 12 2023 at 01:29):

My conclusion will be $x:A \vdash \lambda x.x : A \rightarrow A$

Jean-Baptiste Vienney (Oct 12 2023 at 01:30):

If you look at the three rules, to obtain this this only solution is to use $\rightarrow_{intro}$ as the last step

Jean-Baptiste Vienney (Oct 12 2023 at 01:32):

and thus the previous conclusion will be $x:A, x:A \vdash x : A$

Jean-Baptiste Vienney (Oct 12 2023 at 01:32):

which is proved by using $(Ax)$

Jean-Baptiste Vienney (Oct 12 2023 at 01:35):

So finally my proof is this:

Jean-Baptiste Vienney (Oct 12 2023 at 01:35):

Screenshot-2023-10-11-at-9.35.33-PM.png

Jean-Baptiste Vienney (Oct 12 2023 at 01:37):

You can prove that $(\lambda x.(x)x)(\lambda x.(x)x)$ is not typable by proving that you can't write any proof which type this term!

Jean-Baptiste Vienney (Oct 12 2023 at 01:39):

The problem intuitively is that when you run this program, the only step that you can perform is $(\lambda x.(x)x)(\lambda x.(x)x) \rightarrow_{\beta} (\lambda x.(x)x)(\lambda x.(x)x)$

Jean-Baptiste Vienney (Oct 12 2023 at 01:40):

Nothing has changed when you have done this step and the only thing you can do is repeating it indefinitely

Jean-Baptiste Vienney (Oct 12 2023 at 01:40):

The program doesn't terminate

Jean-Baptiste Vienney (Oct 12 2023 at 01:41):

If you try to write a proof to type it, you realize that the last rule must be $\rightarrow_{elim}$

Jean-Baptiste Vienney (Oct 12 2023 at 01:41):

And must be of this form:

Jean-Baptiste Vienney (Oct 12 2023 at 01:44):

Screenshot-2023-10-11-at-9.48.35-PM.png

Jean-Baptiste Vienney (Oct 12 2023 at 01:45):

So if this term was typable then $\lambda x.(x)x$ should be at the same time of some type $\alpha \rightarrow \beta$ and of the type $\alpha$... in some context $\Gamma$

Jean-Baptiste Vienney (Oct 12 2023 at 01:55):

And I guess that one can proves that it is not possible by thinking a bit

Mike Shulman (Oct 12 2023 at 03:20):

David Egolf said:

If nothing else, I would have thought we could assign some kind of minimally descriptive type like "thing" to the input and output, so we can say that a program always takes "things" as inputs and provides "things" as outputs.

This is absolutely correct! In fact the so-called "untyped" $\lambda$-calculus is arguably better thought of as a "uni-typed" $\lambda$-calculus, where all terms have the same type. The weird thing though is that in that case a "thing" has to be essentially the same as a function from things to things, since any un(i)typed $\lambda$-term can be applied as a function to any other such term and produces another such term. So unityped $\lambda$-calculus corresponds semantically to categories having one object $T$ such that $T^T = T$.

David Egolf (Oct 12 2023 at 15:44):

Jean-Baptiste Vienney said:

David Egolf said:

Thanks Jean-Baptiste Vienney for your explanation!

Jean-Baptiste Vienney said:

Let's use the Curry-style. So that we will speak of typable and non-typable $\lambda$-terms.

I guess this is pointing out that I don't really know exactly what it means to "type" something.

To type a $\lambda$-term, you must use logic! Actually, a very simple logic, whose inference rules can be presented like this:
Screenshot-2023-10-11-at-9.23.17-PM.png

Thanks for explaining! I don't follow the details (I'm not comfortable with the syntax), but it's great to know - at a high level - that:

• one can accept certain inference rules for reasoning about typing (which is called a "logic", it sounds like)
• using these rules, (and some context $\Gamma$ specifying the types of some basic "variables") one can sometimes prove that a (potentially complex) given $\lambda$-term has a specific type
• using these rules, and our context $\Gamma$, you can also show that some $\lambda$-terms can never be proven to have a specific type using our inference rules

Morgan Rogers (he/him) (Oct 12 2023 at 16:29):

To complete the higher category structure I sketched earlier, you note that some $\lambda$-terms have several beta reductions that can be applied to them, so that there can be several formally different sequences of beta reductions between two terms. A suitably presented way of re-ordering those beta reductions could give you a class of 2-morphisms.

David Egolf (Oct 12 2023 at 17:30):

Morgan Rogers (he/him) said:

To complete the higher category structure I sketched earlier, you note that some $\lambda$-terms have several beta reductions that can be applied to them, so that there can be several formally different sequences of beta reductions between two terms. A suitably presented way of re-ordering those beta reductions could give you a class of 2-morphisms.

Ah, I think I understand now. Sufficiently complicated $\lambda$-terms can require multiple beta reductions to completely "simplify" them. After applying some sequence of beta reductions, we get a $\lambda$-term (I think) as output. Thinking of a $\lambda$-term as a program, doing one beta reduction I think might correspond to computing part of the program. But the remaining un-computed parts can still be further beta reduced, so we still have a program (and so - intuitively - a $\lambda$-term).

From what you are saying, it sounds like we can beta reduce a $\lambda$-term in different ways, and still get the same result. So we can get multiple distinct sequences of beta reductions that reduce one $\lambda$-term to another (fixed) $\lambda$-term. To make one of these sequences of beta reductions from another, I think you are saying we can just reorder one beta reduction to get another one (so each sequence of beta reductions involves the same steps, just in a different order).

Mike Shulman (Oct 12 2023 at 17:39):

It's a little more subtle than that because if you can reduce one term in two ways, say X and Y, then it could be that after reducing X you have to do more than one further reduction to achieve the effect of Y. For instance, in $(\lambda x. xx)((\lambda y.y)z)$, if you reduce the outer argument first to get $(\lambda x.xx)z$ you can then get $zz$, but if you reduce the outer application first you get $((\lambda y.y)z)((\lambda y.y)z)$ and then you have two more reductions to do to get to $zz$.

Mike Shulman (Oct 12 2023 at 17:39):

The fact that you can always get to the same thing eventually is called a "diamond property" or "Church-Rosser property", I believe. Or sometimes "confluence".

Morgan Rogers (he/him) (Oct 12 2023 at 17:59):

Returning to your blocks @David Egolf, I could treat an individual instruction as a cube resting in the plane, with position in one dimension and height determined by the source block and position in the other dimension determined by the destination. We have to allow the cubes to float here so that we can keep track of the constraints... does that kind of picture make any sense? I don't know how you would handle a sequence of instructions that moves a cube back to a previous position and then moves it again in this geometric picture, so maybe it can't be made to work literally as a higher-dimensional version of the block towers.

Simon Burton (Oct 12 2023 at 21:17):

It seems like all these block instruction rewrites are invertible, so this looks like a kind of n-groupoid to me..

David Egolf (Oct 13 2023 at 16:46):

Morgan Rogers (he/him) said:

Returning to your blocks David Egolf, I could treat an individual instruction as a cube resting in the plane, with position in one dimension and height determined by the source block and position in the other dimension determined by the destination. We have to allow the cubes to float here so that we can keep track of the constraints... does that kind of picture make any sense? I don't know how you would handle a sequence of instructions that moves a cube back to a previous position and then moves it again in this geometric picture, so maybe it can't be made to work literally as a higher-dimensional version of the block towers.

If I understand correctly, the idea is to try and associate a cube that sits in three dimensions to each building instruction. And you are (I think) indicating there are three pieces of data associated to a building instruction:

• the horizontal position of the block to be moved
• the vertical position of the block to be moved
• the destination position of that block

I'm not sure if we want to talk about "absolute" positions of these blocks (relative to some origin), or if we would prefer to talk about displacements between blocks. I'll talk about displacements below, just because I want to think of two towers as basically the same if one is a laterally shifted copy of the other.

For example, consider this tower:
a labelled tower

Then we could describe a building instruction by three pieces of data:

• block $c$ is directly to the left of $b$
• block $c$ is at the same height as $b$
• put block $c$ two blocks above block $b$

Then - I think - the idea is to understand constraints between different building instructions by associating cubes to each building instruction, and seeing if one cube is "stuck under" the other cube.

By the way, it seems to me that the destination position of a block can be thought of as two pieces of data:

• the horizontal position of the destination block (relative to some block in the destination tower)
• the vertical position of the destination block (again relative to some block in the destination tower)

So, perhaps we could instead view a building instruction as comprised of four pieces of data:

• the horizontal position of the block to be moved, relative to some block
• the vertical position of the block to be moved, relative to some block
• the horizontal position of the destination of the block moved, relative to some block
• the vertical position of the destination of the block moved, relative to some block

However, to avoid having to consider four dimensional objects when representing building instructions by geometric things, we could make use of the fact that there should be a bijection $\mathbb{Z} \cong \mathbb{Z} \times \mathbb{Z}$, so that a position in a 2D grid uniquely specifies a position in a single "gridded" direction. So, I guess we can "compress" the destination position of the block to a position in a single coordinate direction. I'll call this compression ("squeezing") operation $s: \mathbb{Z} \times \mathbb{Z} \cong \mathbb{Z}$.

Then we can represent building instructions by (constant size) cubes with displacements in 3D space as follows:

• The horizontal displacement between two cubes is the horizontal displacement between the blocks they move
• The vertical displacement between two cubes is the vertical displacement between the blocks they move
• The "depth-wise" displacement (displacement in the remaining direction) between two cubes is $s(d_f)$, where $d_f \in \mathbb{Z} \times \mathbb{Z}$ is the (two dimensional) displacement between the destinations of the two blocks moved by the two instructions, and $s: \mathbb{Z} \times \mathbb{Z} \cong \mathbb{Z}$ is our compression operation mentioned above.

Am I following you so far? I'm not sure this is quite the picture you hand in mind. I do think that in this setup, one instruction cube $A$ gets stuck under another one $B$ if the block moved by $B$ rests on top of the block $A$. (Intuitively, we can just look at our instruction cubes from the depth-wise direction; then the observed displacement between them is just the displacement between the blocks that they move).

Morgan Rogers (he/him) (Oct 13 2023 at 16:58):

I was imagining that since you always place a block on top of the destination tower that you could drop the vertical position of the destination to simplify things, even though that might make other things more complicated.

Mike Stay (Oct 13 2023 at 18:12):

The approach explained by Lambek and Scott uses a variant of simply-typed lambda calculus that includes explicit product types and pairs, projections, and a constant of type 1 as terms.

Objects are types. We start with a set of base types $\{A, B, C, ...\}$, a terminal type $1$, and construct the complete set of types by adjoining the types $(A \to B)$ and $(A \times B)$ whenever $A$ and $B$ are types.

Morphisms are $(\alpha\beta\eta)$-equivalence classes of terms with one free variable; the source of the morphism is the type of the variable, and the target of the morphism is the type of the term. Two terms are $\alpha$-equivalent if you can get one from the other by renaming parameters (aka dummy variables): $\lambda x.xz \equiv_\alpha \lambda y.yz$. Two terms are $\beta$ equivalent if they eventually reduce to the same result. So a program that does some massive computation and outputs 42 (in some encoding) is $\beta$-equivalent to the number 42 itself. Any term $M$ is $\eta$-equivalent to $\lambda x.Mx$. Composition of morphisms is substituting one into the other; since the one you're substituting in has one free variable and the other's free variable got replaced, the result also has one free variable. The identity morphism is the equivalence class of the term consisting of just the free variable.

As you can see, this approach completely ignores the process of computation. To avoid that, R. A. G. Seely constructed a 2-category of computations that treats beta and eta as 2-morphisms. @John Baez and @Christian Williams did some lovely related work using enriched categories instead of 2-categories.

David Egolf (Oct 15 2023 at 21:00):

Morgan Rogers (he/him) said:

I was imagining that since you always place a block on top of the destination tower that you could drop the vertical position of the destination to simplify things, even though that might make other things more complicated.

I think I see what you mean. So then there are only three pieces of data that determine a single building instruction: the horizontal and vertical positions of the block we are moving, and the horizontal position of where to "release" the block (it will get placed on top of whatever blocks are already at that horizontal position).

(I wonder if it could also be interesting to ignore the vertical position of the source block, so that a single building instruction is determined by two pieces of data: the horizontal position of the source block, and the horizontal position of the destination).

David Egolf (Oct 15 2023 at 21:04):

Morgan Rogers (he/him) said:

Returning to your blocks David Egolf, I could treat an individual instruction as a cube resting in the plane, with position in one dimension and height determined by the source block and position in the other dimension determined by the destination. We have to allow the cubes to float here so that we can keep track of the constraints... does that kind of picture make any sense?

I'm not sure I understand why we need to allow the cubes to float, though. If one instruction cube $A$ is at some non-ground height, that means it corresponds to moving a block from a non-ground height. That means that there is a block underneath the source block of $A$, so that there exists a valid building instruction cube that sits underneath $A$.

I don't know how you would handle a sequence of instructions that moves a cube back to a previous position and then moves it again in this geometric picture, so maybe it can't be made to work literally as a higher-dimensional version of the block towers.

It's not clear to me how one would handle sequences of instructions in this cube picture, in general. If we make a tower of instruction cubes, there in general will be different orders that we can carry out all those instructions in. So, it seems like we need some additional information to describe a particular sequence of building instructions, besides the cube tower (which is - as far as I can tell - just a set of building instructions, together with some information about constraints on the order in which the instructions can be carried out).

David Egolf (Oct 15 2023 at 21:12):

I guess this sort of comes down to the tension between these two concepts:

• a block tower is just a collection of blocks together with their relative locations: it doesn't have some total ordering on its blocks
• but a sequence of building instructions is a totally ordered collection of building instructions

So it's going to be tough, I think, to model a sequence of building instructions with an "unordered" block tower. I suppose we could consider a "ordered" block tower though - where we say which block is first, second, ..., and last. (Or alternatively, maybe we could relax the ordering we put on our building instructions).

David Egolf (Oct 17 2023 at 15:53):

Morgan Rogers (he/him) said:

Returning to your blocks David Egolf, I could treat an individual instruction as a cube resting in the plane, with position in one dimension and height determined by the source block and position in the other dimension determined by the destination. We have to allow the cubes to float here so that we can keep track of the constraints... does that kind of picture make any sense?

I think I understand better what you were saying here, now:
While it is true that there is always an instruction cube that can exist (if that makes sense) under any instruction cube not on the ground, that instruction cube is not necessarily included in a sequence of instructions that involves the instruction cube not on the ground. So, if we want to visualize - for example - the single building instruction that moves a block not on the ground, we are naturally led to consider instruction cubes that float in the air.

I don't know how you would handle a sequence of instructions that moves a cube back to a previous position and then moves it again in this geometric picture, so maybe it can't be made to work literally as a higher-dimensional version of the block towers.

I also misunderstood what you were saying here. I was thinking about concatenating sequences of building instructions with common source $A$ and target $B$ , so that their composite specifies a more complex sequence of building instruction from $A$ to $B$. However, I now believe you are talking about composing a building instruction from $A$ to $B$ with a building instruction from $B$ to $C$, so that our composite building instruction is from $A$ to $C$.

I think you are indicating the problem is as follows. We have two situations:

1. We move a block from a starting position to a final position.
2. We move a block somewhere, then back to its starting position, and then to a final position.

In each case, the block starts and ends at the same place, but the sequence of instructions involved in each case is different. So, the method of visualizing instructions as cubes (which only keeps track of starting and ending positions) wouldn't distinguish these two sequences of instructions.

David Egolf (Oct 17 2023 at 16:16):

Just for fun, I did have another geometric idea for visualizing this setup :upside_down::

• we don't change how we visualize block towers
• individual building instructions can be visualized as "paths" that travel in space from a starting position to an ending position
• building instructions that move a block somewhere, and then move it somewhere else can be composed (by composing the two paths)
• If we have a sequence of building instructions (with common source and target), it's like we have a sequence of paths. To visualize this geometrically, we can draw a path that visits each of the building instruction paths in a specified order. So, a sequence of building instructions is like "a path on paths". I'm wondering if this can be thought of as some kind of "directed surface" that moves through each building instruction path in order.

Anyways, I'm not sure what my goal is with any of this (besides thinking about fun geometric things)! I just wanted to share a geometric visualization idea, since you (@Morgan Rogers (he/him) ) went to the effort of sharing one with me.

Morgan Rogers (he/him) (Oct 18 2023 at 21:13):

Fantastic, it seems you figured out exactly what I was trying to describe! And your suggestion of keeping track of paths rather than just start and end positions is a great idea: these paths are a kind of discrete homotopy, and with that point of view it might become easier to think about what higher morphisms look like. What's especially interesting about your set-up is that the constraints on the blocks ensure that some operations that seem like they should be homotopic to the identity that aren't.
Think about a stack of two blocks, and the operation which moves the top block into an adjacent column and then moves the other block on top of it. If we repeat that operation, it seems like we get back to where we started (since the blocks arrive in the same position relative to one another and block towers are invariant under translation), but if I'm thinking about this correctly there is no way to completely eliminate the moves in the middle.

If what you're aiming to do is understand higher categories better, thinking about this some more is not going to be wasted effort, it's already a category which has some interesting features ;)

David Egolf (Oct 20 2023 at 19:24):

@Morgan Rogers (he/him) It's great to hear I was able to figure out what you were describing!

It's going to take me some time to think about your most recent comment. I'm planning to respond to it properly once I've managed to organize and develop my thoughts a bit more!

David Egolf (Oct 23 2023 at 21:23):

Morgan Rogers (he/him) said:

And your suggestion of keeping track of paths rather than just start and end positions is a great idea: these paths are a kind of discrete homotopy, and with that point of view it might become easier to think about what higher morphisms look like.

The term "discrete homotopy" is new to me! I found an interesting paper Foundations of a Connectivity Theory for Simplicial Complexes that talks about a kind of discrete homotopy.

Using the ideas from that paper, I think we can start to organize the above rough ideas a bit. I think this gives a natural way to define 2-morphisms between between our 1-morphisms, which are sequences of building instructions.

I'll explain the ideas below in probably a couple posts (I find it easier to edit and render shorter posts).

David Egolf (Oct 23 2023 at 21:29):

I want to visualize each sequence of building instructions as a kind of path. To do this, I think we can consider a sort of "space" that I am calling "tower space". Each point in tower space is a block tower. So far, "tower space" is just a set, but I want to define a notion of adjacency between towers, so that we have a kind of "distance" in tower space. I'll also want to talk about "paths" in tower space.

So, each point in tower space corresponds to an object of the category we roughly described above, which is just a block tower. I want morphisms between these block towers to be "paths" in tower space. To define a "path" (which I will actually call a "chain", imitating the terminology from the paper I mentioned), I will first define what it means for two towers to be adjacent.

Two block towers $A$ and $B$ are adjacent if we can make tower $B$ from tower $A$ by either moving zero blocks or moving one block in tower $A$, while obeying the restriction that we can't move blocks that have another block resting on top of them. So, $A$ and $B$ are adjacent if we can "adjust" one tower into the other in (at most) a single move.

So, for example, here are two adjacent block towers:
two adjacent towers

And here are two more adjacent block towers:
two more adjacent towers

David Egolf (Oct 23 2023 at 21:33):

Next, we define a "path" of towers, which I will actually call a "chain", to follow the terminology in the paper I linked above. A chain is a sequence of towers, where any two consecutive towers are adjacent. The idea is we are gradually walking through tower space from tower to another, where with each step we have to move between adjacent towers.

Here is an example of a tower chain:
a tower chain

Note that, for any tower $A$, we can make the tower to the left of $A$ or the tower to the right of $A$ by moving a single block in $A$.

I believe that tower chains correspond closely to what I've been calling "sequences of building instructions" above. In the category outlined earlier, sequences of building instructions that make tower $A$ into tower $B$ were our 1-morphisms (from $A$ to $B$). We can now visualize these 1-morphisms as chains in tower space, I believe. So, all the 1-morphisms from tower $A$ to tower $B$ correspond to all the tower chains between $A$ and $B$ in tower space.

To compose chains, we stick them end to end. To have identity morphisms, I suppose this means we need to allow for empty chains? (I'm not quite sure how to think about identity morphisms.)

David Egolf (Oct 23 2023 at 21:42):

Now, using the setup, we want to define 2-morphisms. Above, I indicated that I wanted 2-morphisms to be a way to edit one sequence of building instructions to get a different sequence of building instructions. Translating this concept to tower space, I believe we want a 2-morphism to be a "homotopy" from one chain to another. That is, it should be a way of gradually turning one tower chain (from $A$ to $B$) into another tower chain (also from $A$ to $B$).

Following the paper I linked above, I think we should allow for two kinds of operations that turn one chain into another chain:

1. The kind of operation that repeats a given tower multiple consecutive times in a given chain (so a tower chain $a,b,c$ might become $a,b,b,b,c$). This operation allows us to make a chain longer by "adding in slack". Upon reflection, I think we also want to allow for deletions of consecutive repeated towers in a chain.
2. The kind of operation which takes a chain $\sigma: A \to B$, and then produces a new chain $\tau: A \to B$ with the same number of towers, such that the $i_{th}$ tower in the first sequence $\sigma_i$ is adjacent to the $i_{th}$ tower in the new sequence $\tau_i$, and that this is true for all $i$. The idea is that we "dragging" the chain around in tower space, so that adjacent points stay adjacent, and we move each point in the chain to an adjacent point.

A homotopy of chains is then a sequence of operations of the two kinds listed above that changes one chain from $A$ to $B$ to another chain from $A$ to $B$. (I think we need to allow for empty sequences, so that we have identity morphisms, as composition is to be by concatenation of sequences).

Here is a visualization of a very short homotopy of chains:
homotopy of chains

The first chain is the sequence of towers in the first row, and the second chain is the sequence of towers in the second row. Note that for any tower $A$ in this drawing, the tower above/below/left/right is adjacent to $A$. So, we have a homotopy with a single operation (of the second kind) that changes the first chain to the second chain.

David Egolf (Oct 23 2023 at 22:02):

Morgan Rogers (he/him) said:

Think about a stack of two blocks, and the operation which moves the top block into an adjacent column and then moves the other block on top of it. If we repeat that operation, it seems like we get back to where we started (since the blocks arrive in the same position relative to one another and block towers are invariant under translation), but if I'm thinking about this correctly there is no way to completely eliminate the moves in the middle.

So, two chains are described here:
do the operation once

and

do the operation twice

We have a homotopy from the first chain to the second chain as follows:
a homotopy

(Note that these chains don't keep track of how we are changing one block tower into an adjacent one. I'm not sure if it would be good to keep track of this or not.)

I'm not quite sure if this is what you had in mind, but hopefully it's related! It could be that too many 1-morphisms are homotopic in this setup, relative to what you had in mind.

David Egolf (Oct 23 2023 at 22:04):

Morgan Rogers (he/him) said:

If what you're aiming to do is understand higher categories better, thinking about this some more is not going to be wasted effort, it's already a category which has some interesting features ;)

That seems like a reasonable goal to have, and so that's great to hear! :smile:

Morgan Rogers (he/him) (Oct 24 2023 at 07:33):

David Egolf said:

I'm not quite sure if this is what you had in mind, but hopefully it's related! It could be that too many 1-morphisms are homotopic in this setup, relative to what you had in mind.

I like the simplicity of your construction, since it makes it easy to generalize to 3-morphisms and beyond. But comparing with what I tried to describe, this identifies more 1-morphisms than I was expecting. That's because there are actually two ways to go between the two-block towers which your presentation doesn't distinguish: from the vertical position I can move the top block to the left or to the right to get the horizontal tower, and I was expecting those to be distinct :face_with_monocle: but if a morphism is just a sequence of block towers, that information is discarded.

Morgan Rogers (he/him) (Oct 24 2023 at 07:34):

Isn't it funny that things can already be complicated with just two blocks :rolling_on_the_floor_laughing:

David Egolf (Oct 24 2023 at 18:01):

Morgan Rogers (he/him) said:

But comparing with what I tried to describe, this identifies more 1-morphisms than I was expecting. That's because there are actually two ways to go between the two-block towers which your presentation doesn't distinguish: from the vertical position I can move the top block to the left or to the right to get the horizontal tower, and I was expecting those to be distinct :face_with_monocle: but if a morphism is just a sequence of block towers, that information is discarded.

I'm all for hanging on to more information! Keeping track of where the individual blocks move I think is more in the spirit of what I had in mind earlier, too. Now that I've worked out a notion of 2-morphism when a 1-morphism is a just a sequence of block towers, I think I have an idea of how to work out a notion of 2-morphism when 1-morphism is a sequence of block moves.

To carry out the construction above, the key thing was to define a notion of adjacency between block towers. I think now we want to extend this notion of adjacency to "block moves", which say how to move one block to make one tower from another tower. We can draw a single "block move" like this:
a block move

I could also draw in arrows for all the other blocks, but they just stay in place - so I don't draw arrows for them, to reduce clutter.

David Egolf (Oct 24 2023 at 18:07):

Now I want define a notion of adjacency between two block moves. If we have a block move $f: A \to B$ and a block move $g: C \to D$, then let us say that $f$ is adjacent to $g$ if there are block moves $h$ and $h'$ so that this square commutes:
two adjacent block moves f and g

Notice that this implies that $A$ is adjacent to $C$ and $B$ is adjacent to $D$ as block towers. In the previous construction, we basically were requiring squares like this to exist, but not necessarily to be commutative.

We can draw a block move adjacency like this:
a block move adjacency

The top block move is adjacent to the bottom block move. That's because this square is commutative in the sense that if you track any block around the bottom left path or the top right path, it ends up in the same place. I again don't draw arrows for blocks that don't move, with exception of the arrow pointing down on the left, which I've drawn to emphasize commutativity.

Morgan Rogers (he/him) (Oct 24 2023 at 18:13):

That's perfect! Now if you draw the two-block tower flipping a couple of times, the block move arrows will form a braid. My claim was that this braid is not homotopic to the identity, even though the blocks end up back where they started :wink:

Morgan Rogers (he/him) (Oct 24 2023 at 18:14):

Another interesting thing to observe is that since all of the moves are reversible, this is actually a higher groupoid!

Morgan Rogers (he/him) (Oct 24 2023 at 18:18):

By the way @David Egolf , I don't know if you have seen the discussion about Curry-Howard-Lambek in another stream. It's quite technical, but there are some further details of how people have formalized dynamics of computation using higher categories. If that's ever something you want to explore further based on our conversation earlier in the thread, there are some good references in that discussion.

Morgan Rogers (he/him) (Oct 24 2023 at 18:22):

(How are you drawing your pictures, by the way? I like them a lot!)

David Egolf (Oct 24 2023 at 18:25):

I think we also want to define a notion of "horizontal adjacency" for block moves, to imitate the previous construction and eventually define 2-morphisms. Let us say that an ordered pair of block moves $(f: A \to B, g: C \to D)$ are horizontally adjacent exactly when $B=C$. Since we want the composition of two 1-morphisms to be a 1-morphism, we now define a 1-morphism to be a sequence of block moves, where each pair of consecutive block moves $(f,g)$ are horizontally adjacent. Since I want identity morphisms to exist, I think we actually have to allow a "block move" to consist of either (1) moving one block or (2) moving zero blocks. So, the identity 1-morphism on a tower $A$ is the empty sequence of block moves that produces $A$ from $A$. Composition of 1-morphisms is by concatenation of sequences.

Now we define two operations that let us turn 1-morphism into another 1-morphism:

1. Add in repeated identity morphisms. This amounts to inserting extra copies of a block tower in a sequence, with the identity block move between each copy.
2. Turn a 1-morphism $\tau$ into a 1-morphism $\sigma$ where, for each $i$, $\tau_i$ and $\sigma_i$ are "vertically adjacent" (adjacent in the sense above, with a commutative square) as block-moves. (Here $\tau_i$ is the $i_{th}$ block move of the sequence $\tau$).

Then a 2-morphism from $f: A \to B$ to $g: C \to D$ is a sequence of operations of the two kinds listed above that turns $f$ into $g$.

David Egolf (Oct 24 2023 at 18:26):

Morgan Rogers (he/him) said:

(How are you drawing your pictures, by the way? I like them a lot!)

Thanks!

I wrote a program to draw the blocks for me (using the Makie package in Julia), and then I've been manually drawing in the arrows in Inkscape. Probably it would be possible to extend the program to draw arrows as well, but that sounded like too much work at the moment!

David Egolf (Oct 24 2023 at 18:36):

Morgan Rogers (he/him) said:

That's perfect! Now if you draw the two-block tower flipping a couple of times, the block move arrows will form a braid. My claim was that this braid is not homotopic to the identity, even though the blocks end up back where they started :wink:

Here is this picture!
braiding

I've drawn in some extra arrows to track how each block gets moved around, and to try and visualize the two paths of the different blocks getting "tangled up".

David Egolf (Oct 24 2023 at 18:50):

Interestingly, I think doing this flipping operation once and doing it twice are still homotopic under the current construction. Although it gets a little complicated!

I start out by adding in several copies of the identity block move between the central block tower in the "do the operation once" sequence of block towers. Then I think I show below that this is homotopic to the "do the operation twice" sequence of block moves (that is, there is a 2-morphism from the first sequence of block moves to the second sequence of block moves):
a homotopy, I think

The red and blue paths are drawn in to illustrate commutativity of the last square.

And here's that drawing again, with a few more arrows drawn in:
a homotopy with more arrows

David Egolf (Oct 24 2023 at 19:06):

Morgan Rogers (he/him) said:

That's perfect! Now if you draw the two-block tower flipping a couple of times, the block move arrows will form a braid. My claim was that this braid is not homotopic to the identity, even though the blocks end up back where they started :wink:

Ah, I notice now that your claim is that the "flipping the tower over twice" operation is not homotopic to the identity. That's different than what I was investigating in the drawing above (where I think I showed that "flipping once" is homotopic to "flipping twice").

David Egolf (Oct 24 2023 at 19:48):

I think "flipping twice" and even just "flipping once" is probably not homotopic to the identity in this case. If we start by "stretching out the identity" and then try to transform this to the "flipping once" operation, we run into a problem, as pictured below:
not a homotopy

The top row is the "stretched out" version of leaving the tower untouched. The bottom row is the operation that flips the two-block tower upside down.

The dashed arrow needs to be chosen so that both the blue and red squares commute. But this is impossible!

If we flipped the blocks twice, then we'd have an even bigger diagram where we'd need to make all the squares commutative. The diagram above would be a sub-diagram of this bigger diagram, and so I suspect that flipping the blocks twice will also not be homotopic to the identity.

Morgan Rogers (he/him) (Oct 25 2023 at 09:17):

David Egolf said:

Interestingly, I think doing this flipping operation once and doing it twice are still homotopic under the current construction. Although it gets a little complicated!

This is really unexpected for me, because I hadn't considered that for the horizontal arrangement, the translation invariance means that moving the left block to the right or moving the right block to the left (i.e. the horizontal swap) are actually identical transformations! This makes me suspect that there might be a way to construct a homotopy to the identity after all.
I want to highlight the fact that you were able to intuitively extend the notion of 2-morphism/homotopy that you proposed for the adjacency definition to a sensible notion for the version of this category with arrows. This exercise is already building your understanding of at least one shape that higher morphisms can take, and besides exploring this specific example, watching you develop that has been a cool experience too.

David Egolf (Oct 25 2023 at 20:04):

Morgan Rogers (he/him) said:

This is really unexpected for me, because I hadn't considered that for the horizontal arrangement, the translation invariance means that moving the left block to the right or moving the right block to the left (i.e. the horizontal swap) are actually identical transformations! This makes me suspect that there might be a way to construct a homotopy to the identity after all.

It is interesting how the translation invariance for the towers means that we can't distinguish moving the left block to the right, or the right block to the left. That's a good point.

I think we can prove that the "flip the tower once" operation is not homotopic to the identity, by the way! Here's an outline of a possible argument:

• to construct a homotopy from the identity to the "flip the tower once" operation involves two steps: extending the two sequence of block moves to be the same length (by insertion of identities) and then transforming one sequence to the other while respecting horizontal and vertical adjacency
• at the end of our construction of this homotopy, we get a diagram illustrating how the blocks are moved around, where each square has to commute (in the sense that one can follow a single block around the square on the top right path or on the bottom left path)
• in our top row of this diagram, we have the identity block move repeated several times: this always moves the top block to the top block
• in our outermost vertical columns we also have the identity block move repeated several times
• in our bottom row, we have some sequence of block moves that eventually moves to the block on the top to be at the bottom of the two-block stack (because this row corresponds to the "flip the tower once" operation)
• So, if we track the block on the top around the outside of this diagram on the top right path, it ends up on the top. But if we track it around the outside of this diagram on the bottom left path, it ends up on the bottom. Thus, the diagram doesn't commute: we don't have a homotopy. (If each individual square commutes, the outermost rectangle must commute; so if the outermost rectangle doesn't commute, there must be at least one individual square that doesn't commute).

To illustrate, here's an example of an attempt I made to construct a homotopy. This helps illustrate why all such attempts must (I believe) fail:
not a homotopy

Notice that the blue sequence of block moves and red sequence of block moves don't send the top block to the same place, as would be required for this to be a homotopy.

David Egolf (Oct 25 2023 at 20:14):

Morgan Rogers (he/him) said:

David Egolf said:

Interestingly, I think doing this flipping operation once and doing it twice are still homotopic under the current construction. Although it gets a little complicated!

I want to highlight the fact that you were able to intuitively extend the notion of 2-morphism/homotopy that you proposed for the adjacency definition to a sensible notion for the version of this category with arrows. This exercise is already building your understanding of at least one shape that higher morphisms can take, and besides exploring this specific example, watching you develop that has been a cool experience too.

Yes, this has been both fun and interesting! I feel like I've learned some good things. For example, I feel like I've managed to understand the concept of homotopy a bit better. This example also helped me realize that the intuition I have for 1-morphisms - namely, that they can often be viewed as data witnessing a way to turn one object into another object - can be extended to 2-morphisms between 1-morphisms. I feel like this might help me construct new categories (e.g. for applications) in the future.

Thanks for exploring these ideas with me! I got a lot further with the help of your insights than I would have on my own.

Nathaniel Virgo (Oct 26 2023 at 02:34):

I'm curious about something - I hope it doesn't throw too much of a spanner into the works if I bring it up.

Let $V$ be the set of all towers, and let $E$ be the set of block moves. Each block move goes 'from' one tower 'to' another, so we can define two functions, $s,t:E \to V$, where $s$ sends a block move to its 'source' tower and $t$ sends a block move to its 'target' tower.

So then we have this situation:

image.png

which is (what category theorists call) a graph, aka a directed multigraph or quiver. In this case the vertices are towers and the edges are block moves.

It seems like your construction only really depends on the graph structure. It seems like your construction only really depends on this graph structure. So can this same notion of homotopy be defined for any graph?

Morgan Rogers (he/him) (Oct 26 2023 at 12:17):

David Egolf said:

I think we can prove that the "flip the tower once" operation is not homotopic to the identity, by the way! Here's an outline of a possible argument:

• to construct a homotopy from the identity to the "flip the tower once" operation involves two steps: extending the two sequence of block moves to be the same length (by insertion of identities) and then transforming one sequence to the other while respecting horizontal and vertical adjacency
• at the end of our construction of this homotopy, we get a diagram illustrating how the blocks are moved around, where each square has to commute (in the sense that one can follow a single block around the square on the top right path or on the bottom left path)
• in our top row of this diagram, we have the identity block move repeated several times: this always moves the top block to the top block
• in our outermost vertical columns we also have the identity block move repeated several times
• in our bottom row, we have some sequence of block moves that eventually moves to the block on the top to be at the bottom of the two-block stack (because this row corresponds to the "flip the tower once" operation)
• So, if we track the block on the top around the outside of this diagram on the top right path, it ends up on the top. But if we track it around the outside of this diagram on the bottom left path, it ends up on the bottom. Thus, the diagram doesn't commute: we don't have a homotopy. (If each individual square commutes, the outermost rectangle must commute; so if the outermost rectangle doesn't commute, there must be at least one individual square that doesn't commute).

I like this argument, but uh-oh! doesn't that also apply when comparing the 1-flip and 2-flip transformations? (I've actually spotted the mistake in your diagrams from earlier, so indeed it does :wink: ) That leaves open the question of whether the 2-flip operation is homotopic to the identity. Thanks to your last diagram, I have an idea of the answer, but I won't spoil it.

Morgan Rogers (he/him) (Oct 26 2023 at 12:18):

Nathaniel Virgo said:

It seems like your construction only really depends on the graph structure. It seems like your construction only really depends on this graph structure. So can this same notion of homotopy be defined for any graph?

Beware that the operations we've considered on block towers don't correspond to graph homomorphisms, but a certain constrained type of transformation of graphs. Beyond that, defining homotopies of this discrete type between such transformations seems like it should be possible.

David Egolf (Oct 26 2023 at 16:32):

Morgan Rogers (he/him) said:

I like this argument, but uh-oh! doesn't that also apply when comparing the 1-flip and 2-flip transformations? (I've actually spotted the mistake in your diagrams from earlier, so indeed it does :wink: )

Ah, good point! Using the idea of the argument above, I was able to also spot the mistake in my diagram from before as well:
a mistake found

I've circled the place where I made a mistake. If the top row is really going to be the "flip once" operation, the block that was on the top at the start needs to end up on the bottom. Instead, I put the block back on the top again!

So, using this argument above, I think we can conclude that the 1-flip and the 2-flip are not homotopic. And in general, flipping an odd number of times will never be homotopic to flipping an even number of times.

David Egolf (Oct 26 2023 at 17:15):

Morgan Rogers (he/him) said:

That leaves open the question of whether the 2-flip operation is homotopic to the identity. Thanks to your last diagram, I have an idea of the answer, but I won't spoil it.

If I haven't made another mistake (easier said than done with these block diagrams!), I think I have constructed a homotopy from the identity to the 2-flip operation:
a homotopy, I think

I've drawn arrows that keep track of where a single block goes under all the block moves involved.

It's key to have the middle step here (the middle row). If we try and go directly from the top row (the stretched-out identity operation) to the bottom row (the 2-flip operation), we encounter a problem similar to what prevents the 1-flip from being homotopic to the identity.

David Egolf (Oct 26 2023 at 17:26):

Nathaniel Virgo said:

I'm curious about something - I hope it doesn't throw too much of a spanner into the works if I bring it up.

Let $V$ be the set of all towers, and let $E$ be the set of block moves. Each block move goes 'from' one tower 'to' another, so we can define two functions, $s,t:E \to V$, where $s$ sends a block move to its 'source' tower and $t$ sends a block move to its 'target' tower.

So then we have this situation:

image.png

which is (what category theorists call) a graph, aka a directed multigraph or quiver. In this case the vertices are towers and the edges are block moves.

It seems like your construction only really depends on the graph structure. It seems like your construction only really depends on this graph structure. So can this same notion of homotopy be defined for any graph?

That's really interesting! It reminds me of what is done in the paper I mentioned above, Foundations of a Connectivity Theory for Simplicial Complexes. In that paper, they define "chains" on simplicial complexes, as follows:

q-chain definition

They also define when two q-chains are homotopic, and it is this definition I was imitating above when I defined homotopies between sequences of block moves.

If we consider the case when the simplicial complex in question only contains 1D simplices (and their 0D endpoints), we get a sort of undirected graph as our setting for talking about q-chains and their homotopies. Maybe the ideas considered in that paper for undirected simplicial complexes can be adapted to directed simplicial complexes, which I think start to look like directed graphs (if we have only 1D simplices and 0D simplices in our directed simplicial complex).

I suppose this is still different from what you are describing, because - if I understand correctly - a directed simplicial complex still has at most one directed 1D simplex from one 0D point to another, while a graph (in the sense you describe above) can have multiple edges from one vertex to another.

David Egolf (Oct 26 2023 at 17:36):

All that being said, I think we probably could define this same notion of homotopy for any graph; I think a graph contains the key information we need. (Below, I think I realize we actually need a bit more information). We will call two vertices "adjacent" if there is a directed edge that connects them.

I guess we get a category where:

• the objects are the vertices of the graph
• a 1-morphism from $A$ to $B$ is roughly a composable sequence of directed edges that go from $A$ to $B$ (by "composable", I mean that the target of one directed edge in the sequence is the source of the next directed edge in the sequence) (I'm not quite sure how to handle identities morphisms though...)
• a 2-morphism (or "homotopy") is a sequence of steps that transforms a 1-morphism to another 1-morphism using (1) "stretching" of a 1-morphism, which involves adding in identity directed edges and (2) "adjacent transformation" where we change a 1-morphism $\sigma$ to another $\tau$ of the same length with the same endpoints, while requiring $\sigma_i$ and $\tau_i$ (the $i_{th}$ vertices associated to these 1-morphisms) to be adjacent for all $i$, and we also require the below square to commute for each $i$ (where the diagram is defined), where the arrows drawn are all edges in the graph:

adjacent transformation diagram

By $e_i^\sigma$ I mean the $i_{th}$ directed edge of the 1-morphism $\sigma$. And by $e_i^\tau$ I mean the $i_{th}$ directed edge of the 1-morphism $\tau$. The $\alpha_i$ and $\alpha_{i+1}$ are directed edges and they describe how to transform one edge into an "adjacent" directed edge.

However, staring at this last diagram, I'm not sure we necessarily know what it means for this diagram to commute in an arbitrary graph. In our block tower example, commutativity of this kind of square means that each block ends up going to the same destination whether you use the top right path or the bottom left path. In other words, we can compose two block moves to get a more complicated building instruction, and that allows us to determine if the square commutes. But I believe that a graph by itself doesn't come with a way to compose its directed edges.

David Egolf (Oct 26 2023 at 17:55):

If we can compose directed edges in our graph, then we can assess whether the square indicated above commutes or not. So maybe we can define a similar notion of homotopy on any "graph with composition"? (A "graph with composition" starts to sound a lot like a category...)

If we did consider a graph that supports composition of its directed edges, we might also want to label special directed edges as the ones providing "adjacency", similar to how the "block moves" that move a single block (or zero blocks) define a notion of adjacency between block towers. In that case, we would say that two vertices are adjacent if they are connected by a directed edge that is an adjacency.

So, in summary, maybe we can define a similar notion of homotopy for any graph where we can compose any two compatible directed edges to get another directed edge, and certain special directed edges are labelled as "adjacencies".