Invalid contraction is allowed

[calintat]

The following contraction is now allowed:

I think this is wrong and it definitely didn't use to be the case. I suppose we could fix this with typechecking, but we should investigate why our new contraction algorithm allows this to go through and whether that's avoidable.

[NickHu]

I think I understand why this is happening. This contraction happens in two steps. Consider the first step: a contraction between an endomorphism $e$ next to an identity on some generator $f$, and a cup which also has its tip marked by the generator $f$. In this contraction, $e$ has dimension 2, and $f$ has dimension 1, so $e$ is going to be computed as the colimit, and you end up with a cup with tip $e$ with the $f$ folded into it (I think in the theories we care about, this is not well typed). The second contraction will proceed similarly. My guess is that neither contraction would work if instead you had an algebraic cup and cap instead, because then $e$ would not be the unique maximal dimension generator and no colimit would be computed. This kind of suggests that when $f$ appears as the tip of the cup or cap it should have dimension 2.

[calintat]

This used to be an invalid contraction, so it can't be because of the dimension.

[calintat]

Also the labels should not allow this contraction to go through, because this is a valid oriented contraction but an invalid framed contraction.

[NickHu]

Here's a thought which might justify why such a contraction should exist: if instead you had the endomorphism wedged in the middle of the snake, instead of this bubble, then these two contractions would be how you construct the transpose.

[calintat]

I don't agree that this should contract (for framed generators). The example you just described is different and that's always used to contract. This used be an invalid contraction until recently, and I think that's the correct behaviour.

Also I remember you describing this as unsound when I discovered it for oriented generators 🤔

[NickHu]

Yes I think you're right, the framing should preclude the second contraction but the first one is valid.

[jamievicary]

I think I have a clear understanding of why this is happening. It is directly related to the nondeterministic edge collapse that we discussed before in issue #798.

Let $E$ be the set of edges at a particular depth, and let $a,b \in E$ be two collapsible edges, with the property that collapsing $a$ makes $b$ non-collapsible. Then if we choose to collapse $a$, it follows immediately that the resulting collapse homotopy will not type-check, since the type-checking algorithm would try to collapse that triangle involving $b$, but we already know it does not collapse.

So, what do we need to do instead. Well at the moment, for a fixed depth, we collect all the collapsible edges, and then try to collapse them one by one. We keep checking each time if the edge is not collapsible, and if we find a non-collapsible edge, we skip over it and try the next one. Here is what we must do instead: if we discover one of the edges is no longer collapsible, we fail and declare the diagram non-contractible.

I suspect this will rescue all these examples Calin discovered in the early hours of this morning, where diagrams contract which shouldn't. However it may cause the example from #798 to not contract. But at least it will be a failure to contract rather than a crash, and we can then manually examine that example in detail to understand what needs to change in the algorithm. For example, maybe we need a more refined view of what the "depth" of an edge is.

This should be a very quick change to the algorithm, so if you guys are happy, could we please do this and then evaluate the results.

Nick or Calin, could you also post a very clear explanation of the current definition of "depth", and how we currently decide in what order to group the collapsible edges.

[jamievicary]

By the way, a very nice example of this phenomenon (two collapsible edges of the same depth, where collapsing one makes the other non-collapsible) arises from trying to collapse this second contraction above.

[calintat]

The definition of depth is very simple. We do it based on the coordinates. An edge from coordinate $x$ to coordinate $y$ has depth $i$ iff $i$ is the first index at which $x$ and $y$ differ (i.e. $x_j = y_j$ for $j < i$ and $x_i \neq y_i$).

Another way to think about this is the explode graph. The depth of an edge represents the step of the iterated explosion at which that edge was introduced for the first time. When you explode a rewrite into its subslices, the subslices will have the same depth as the original rewrite. I hope that makes sense.

In a 2D example, vertical edges have depth 0 and horizontal edges have depth 1 and we always collapse the edges in the reverse order of the depths.

[jamievicary]

Thanks Calin. What do you think about my comment this morning, does it make sense to you?

There clearly are ways we could refine the depth ordering on edges (lexicographic by start and end depth?) but it would be good to be motivated by an example rather than trying to do it arbitrarily.

[calintat]

It makes some sense, but I will need to sketch this example to really understand what's going on.

I agree there are many ways we could group the edges. Previously we had a single group, now we have one group per depth. It seems reasonable to say that if two collapsible edges in the same group exhibit this phenomenon where collapsing one makes the other non-collapsible, we should fail. Something I'm wondering is why did the previous algorithm work correctly? Was it because we were doing this accidentally because there was only one group?

[calintat]

And if we wanted to experiment with a different strategy to group edges, I have another idea.

Inside each depth group, we can further group the edges into subgroups which correspond to subslices of the whole diagram. For example, in the second contraction above, we can group the horizontal edges into five subgroups corresponding to the five heights of the diagram.

This is already what we do for calculating the orientation. Maybe by splitting the groups into more subgroups, we can fix this while also not breaking #798.

[jamievicary]

Yes using the subdiagram (ie the actual coordinate value) is a good idea for refining the groups.

The earlier algorithm we were using was not tested on such complex examples.

[calintat]

Well I have definitely tested the old algorithm on this particular example and it worked correctly, which is why I'm a bit confused.

[NickHu]

Fixed by 1bdf7cea5e785cf635a0058dfb736a8f5a3c3d2e