Malformed diagrams being created

[jamievicary]

Unfortunately within in an hour or so of playing with the labelled version I have twice created an invalid diagram, which has not been noticed by the wellformedness checker. The attached workspace is an example, contract the two heights to generate a crash. (This diagram was formed by some complex process that I can't reproduce; if you just create this diagram directly it contracts without any issue.)

Presumably the wellformedness checker is currently switched on in alpha?

So I think this is a very good reason to implement labelled typechecking #703. Luckily as recently discussed this should be easy.

[jamievicary]

We can close this issue once we discover what feature of the tool is generating the malformed diagrams.

[jamievicary]

Here is the example I meant to attach to the OP: homotopy_io_export (7).zip

[calintat]

Yes, the wellformedness checks are turned on (in both beta and alpha). It looks like contraction or expansion is generating something malformed.

[calintat]

However, I don't see why typechecking would help with this. This is worse than the diagram not typechecking, it means something has gone wrong.

[jamievicary]

Yes I completely agree Calin. My point it is that it is not clear at what point the diagram is being corrupted. We need to implement typechecking so that (as a temporary debug mode) we typecheck the entire diagram after every interaction. That will allow us to immediately detect the problem when it occurs, and hence isolate the code responsible. Does that make sense?

[calintat]

Yes, it's weird that the diagram gets corrupted and we don't catch that, I will look into that. It could be we're using the "unsafe" versions of the constructors which don't run the checks.

[calintat]

However, the really weird thing is that the diagram in the attached workspace should be wellformed, because otherwise the import wouldn't work.

[jamievicary]

Ah so we run a one-off wellformedness check on import?

[jamievicary]

In that case the most likely thing is that the diagram is wellformed, but just doesn't typecheck, e.g. because a framing label is wrong somewhere. Hence my proposal to implement typechecking.

[calintat]

Yes we do a deep wellformedness check on every diagram in the signature and workspace when we import.

[calintat]

In that case the most likely thing is that the diagram is wellformed, but just doesn't typecheck, e.g. because a framing label is wrong somewhere. Hence my proposal to implement typechecking.

I see, that makes sense. Still I would expect contraction to just fail if the framing is wrong, rather than produce something malformed. We should never make malformed diagrams.

[calintat]

I tracked down the panic to this code in contract_base: https://github.com/homotopy-io/homotopy-rs/blob/02ff8d32d206eecd51a3b2912293e2e623711eff/homotopy-core/src/contraction.rs#L175-L184

[jamievicary]

Calin can you summarize for me exactly what the wellformedness checks do for all the fundamental structures (Diagrams, Rewrites, Cones, etc)?

[calintat]

For a cone, it checks the commutativity conditions. For a rewrite, it checks that all cones are wellformed. For a diagram, it checks that all cospan rewrites are wellformed and compatible (i.e. you can start with the source and repeatedly rewrite it forwards or backwards along the rewrites without issue).

[calintat]

This panic in particular says that the cone in that contraction rewrite above fails the commutativity condition on the first square, so singular_slices[0] $\circ$ cospan0.forward $!=$ cospan.forward.

[jamievicary]

That's interesting. Here are some other things we could maybe easily check in addition:

• a cone should never be an identity cone
• for a rewrite, its cones should be correctly ordered
• for a diagram, when you say rewrite the source without issue, this should involve verifying that when we cut out the corresponding source diagram part it matches the given source data for the cones

[jamievicary]

It is very very very surprising that contracting a wellformed nonwelltyped diagram should produce a nonwellformed diagram. However it appears that is what is happening.

[jamievicary]

Hence why I want us to forensically double-check we are not accidentally omitting any well-formedness checks.

[calintat]

I agree, I will add the extra checks you suggested.

But I am afraid the best way forward is to sit down and tediously check the diagram you attached and figure out exactly why it's contracting to a malformed diagram. Since Nick is on holiday, I guess I will do that.

[jamievicary]

Those checks I suggested, are we already doing any of them?

I agree we may ultimately just have to check this example by hand, but ensuring we have all possible well-formedness checks first does not hurt.

[calintat]

We're not checking that a rewrite doesn't contain identity cones or that the cones are sorted by index. The third one we're already doing.

Something else I just realised we don't check is that the source and target cospans of a cone are wellformed, though that would be caught by the check for the diagram which that cone is a part of.

[jamievicary]

If that is not currently checked we certainly need to do that!! Surely it's already being checked by the recursive structure of the well-formedness checker?

[calintat]

I have added all the extra checks and the diagram is still well-formed. I think it's time to check the example by hand.

[calintat]

OK I figured out what's different about the attached diagram. It contains some "directed identities" (i.e. rewrites that are the same as identities except for the orientation labels). It's nothing to do with typechecking, the diagram is well-typed.

I still don't understand why that causes contraction to create a malformed diagram which is still bad.

@jamievicary perhaps we could have a meeting to talk about this? I am not really sure what the best solution is.

[jamievicary]

Hi Calin thanks for this! Are you saying the only difference between this diagram and its "correct version" is in the orientation labels?

My sister and her family are visiting today so it's hard to have a meeting, can you maybe sketch a couple of decorated scaffold pictures showing the difference between the attached diagram and what it's supposed to be like?

[calintat]

Hi Jamie, no worries!

It's more subtle than that. On paper, this diagram and its correct version are identical (including the orientation labels on the generators). The only difference is in the encoding. The "bad version" contains some extra cones which are these "directed identities". It still passes my "are there any identity cones" check because these cones are not real identities

Also I am very very confused why contraction doesn't work on this.

[calintat]

This fundamentally comes down to the problem of how we store the orientation labels as that can have unexpected side-effects due to our sparse encoding of diagrams and rewrites and this concept of "directed identities". This is completely an implementation problem.

[jamievicary]

Thanks that is interesting. Perhaps there is nonetheless some way this data can be indicated in a picture, e.g. by decorating the edges of the scaffold with appropriate data showing what is being stored sparsely vs non-sparsely?

[jamievicary]

We need a firm decision on how the orientation labels should be handled with respect to sparseness, and then rigorously enforce this with our wellformedness checker. We discussed this exact point recently. Can you remind me what decision we came to. I remember there was a minor multiplicity of opinion. I think my proposal was that we label a 0-diagram with a pair (g,s) of generator name and sign, that a 0-rewrite (g,s)-->(g',s') stores all the data g,s,g',s' as part of the 0-rewrite, and that a rewrite (g,s)-->(g',s') is an identity (discarding the data) if and only if g=g' and s=s'.

[calintat]

So that is what I was doing until recently. The problem with that idea is that it lets you have "directed identities", i.e. rewrites of the form $(g, +) \to (g, 0)$. That always felt a bit wrong to me. But more importantly it broke the cospan bubbling that Nick wrote.

So then I implemented this new idea (which is what is currently implemented): a 0-diagram is a generator $g$, and 0-rewrite $g_0 \to g_1$ is a triple $(g_0, g_1, s)$ where $s$ is the orientation of $g_1$. That fixed cospan bubbling and I thought it meant we can never have directed identities, but I now realise I was wrong. For example, the diagram above contains the following cone which is not discarded as the source and target cospans are different:

[jamievicary]

Thanks for explaining that. Sorry if I'm being dense, but does that clarify why the tool is crashing? I.e. I don't yet see the problem with the existence of such directed identities as you have drawn in your picture.

[calintat]

It doesn't clarify why contraction crashes tbh. It's probably because we're not being consistent about which directed identities we discard or not.

Which is why I think it's safer if we just store them all like we did before. So I propose I just revert to the original implementation (i.e. your proposal) as that never caused any crashes like this. It will be fairly easy to revert the commit which changes the way we store orientations, but that will break cospan bubbling unfortunately, so I will have to find a way to fix that.

[jamievicary]

Ok, let's try that. Meanwhile can you please make a new issue for diagram bubbling where we can discuss how to fix that. We had at least 2 ideas I think.

On Fri, 19 Aug 2022, 12:05 Calin Tataru, @.***> wrote:

It doesn't clarify why contraction crashes tbh. It's probably because we're not being consistent about which directed identities we discard or not.

Which is why I think it's safer if we just store them all like we did before. So I propose I just revert to the original implementation (i.e. your proposal) as that never caused any crashes like this. It will be fairly easy to revert the commit which changes the way we store orientations, but that will break cospan bubbling unfortunately, so I will have to find a way to fix that.

— Reply to this email directly, view it on GitHub https://github.com/homotopy-io/homotopy-rs/issues/702#issuecomment-1220544004, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACQ4OHUSDP5K5EOWK7BBPJDVZ5TABANCNFSM563C4RJA . You are receiving this because you were mentioned.Message ID: @.***>

[calintat]

Done. I reverted the commit and disabled bubbling for now. That happened to fix #713 which is a good sign. Unfortunately since we don't know the steps to reproduce the diagram in this bug, I can't tell if that is still reproducible or not. Importing the attached workspace won't work as the data structures are different.

[jamievicary]

Regarding the well-formedness checks: we have both regular and singular slice data. Can you clarify precisely how the well-formedness checks work with respect to these? We should be verifying commutative triangles not squares (as we would if the regular slices weren't there.)

[jamievicary]

Here I am talking about well-formedness for cones.

[calintat]

Yes, we check triangles instead of squares.

[calintat]

Is it okay to close this? With the recent changes, I think it's impossible to reproduce this diagram.

[jamievicary]

Yes definitely close this boys

[jamievicary]

Oops weird typo from swype input, meant to write close this now!