Fail of contracting an isolated singularity III #119
Comments
HdXu
changed the title
|
Thanks Hao. Was this related to the issue we experienced in the meeting
today?
…On Mon, 19 Jul 2021, 13:50 HdXu, ***@***.***> wrote:
I cannot contract the following type of singularity in the current UI
setting.
*Screenshot*
[image: Screenshot 2021-07-19 at 13 49 29]
<https://user-images.githubusercontent.com/35509721/126162148-651d9fa0-5512-42b8-989f-1af8152e0230.png>
*Demo File*
bug-isolated singularity3.hom.zip
<https://github.com/homotopy-io/homotopy-rs/files/6840958/bug-isolated.singularity3.hom.zip>
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<#119>, or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACQ4OHX2W7BASUB4N2YWU3LTYQNQDANCNFSM5ATULR3Q>
.
|
|
I am not really sure, as there is slight difference in behavior of homotopy.io. If we can find a stable way to resolve singularities shown in demos, these problems should all be solved. |
|
Here try to contract the top two vertices to see the issue |
|
The problematic diagram appears to be constructed somewhere in the restriction code of the type checker. I couldn't localize it any further yet. |
|
Thanks for the report Lukas, hopefully it won't be too hard to find.
…On Wed, 28 Jul 2021, 16:57 Lukas Heidemann, ***@***.***> wrote:
The problematic diagram appears to be constructed somewhere in the
restriction code of the type checker. I couldn't localize it any further
yet.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#119 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACQ4OHQ6ZW2D4BS7J2VWKIDT2ASE7ANCNFSM5ATULR3Q>
.
|
|
Similar panic report: Demo Screenshot Log Stack: https://beta.homotopy.io/index-62c53504a5ec64bb.js:292:28 wasm-stub@[native code] [Error] RuntimeError: Unreachable code should not be executed (near '...e__hbbfcef5a03f88217(arg0, arg1, addBorr...') |
|
Demo file Error Log Stack: https://beta.homotopy.io/index-5e3d90191231d939.js:482:28 wasm-stub@[native code] [Error] RuntimeError: Unreachable code should not be executed (near '...e__h39d61493df4fb466(arg0, arg1, addBorr...') |
|
It looks like the restriction code itself does exactly what it's supposed to do, but it is asked to restrict to a subdiagram which is non-globular. Consequently the sanity checks triggered by building the non-globular diagram complain. I wonder how the original JS implementation deals with this. |
|
Could this be a difference between the old-style and new-style
normalization, with your non-globular rewrites?
…On Mon, Aug 23, 2021 at 4:09 PM Lukas Heidemann ***@***.***> wrote:
It looks like the restriction code itself does exactly what it's supposed
to do, but it is asked to restrict to a subdiagram which is non-globular.
Consequently the sanity checks triggered by building the non-globular
diagram complain. I wonder how the original JS implementation deals with
this.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#119 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACQ4OHTGIUKK3RTZYGFTM6LT6JQCPANCNFSM5ATULR3Q>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>
.
|
|
Is it definitely correct, that it is being asked to restrict to a
non-globular subdiagram? That sounds weird.
…On Mon, Aug 23, 2021 at 5:15 PM Jamie Vicary ***@***.***> wrote:
Could this be a difference between the old-style and new-style
normalization, with your non-globular rewrites?
On Mon, Aug 23, 2021 at 4:09 PM Lukas Heidemann ***@***.***>
wrote:
> It looks like the restriction code itself does exactly what it's supposed
> to do, but it is asked to restrict to a subdiagram which is non-globular.
> Consequently the sanity checks triggered by building the non-globular
> diagram complain. I wonder how the original JS implementation deals with
> this.
>
> —
> You are receiving this because you commented.
> Reply to this email directly, view it on GitHub
> <#119 (comment)>,
> or unsubscribe
> <https://github.com/notifications/unsubscribe-auth/ACQ4OHTGIUKK3RTZYGFTM6LT6JQCPANCNFSM5ATULR3Q>
> .
> Triage notifications on the go with GitHub Mobile for iOS
> <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
> or Android
> <https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>
> .
>
|
|
I think that is correct. My current theory is that the JS implementation also restricts to a non-globular diagram but regular normalisation makes it globular and happens to be fine with non-globular inputs. The new-style normalisation (in the way it is implemented) expects a globular input diagram and hence crashes. |
|
That's very interesting. Can you now construct a smaller example of the
phenomenon, i.e. a scenario where restriction will be asked to restrict to
a non-globular diagram.
…On Mon, Aug 23, 2021 at 5:18 PM Lukas Heidemann ***@***.***> wrote:
I think that is correct. My current theory is that the JS implementation
also restricts to a non-globular diagram but regular normalisation makes it
globular and happens to be fine with non-globular inputs. The new-style
normalisation (in the way it is implemented) expects a globular input
diagram and hence crashes.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#119 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACQ4OHT5AIWM5TGUAESFVX3T6JYHHANCNFSM5ATULR3Q>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>
.
|
|
Looking at the original diagram which produced the non-globular restriction, it looks like the original itself was non-globular to begin with: |
|
Thanks Lukas this is great. So we should write a globularity checker and
hook it into the diagram rewrite constructor, and have some sort of debug
mode where this executes at runtime to detect malformed diagrams. Hopefully
this is caused by a bug in some other code and we'll be able to find it
quickly.
Calin maybe you might like to do this? It's similar to the other checker
you wrote.
…On Tue, 24 Aug 2021, 12:03 Lukas Heidemann, ***@***.***> wrote:
Looking at the original diagram which produced the non-globular
restriction, it looks like the original itself was non-globular to begin
with:
[image: IMG20210824004848]
<https://user-images.githubusercontent.com/357669/130604737-7e6ae403-a698-4f47-89ca-7c2135952d29.jpg>
The two rows of diagrams in this picture are alternating regular and
singular slices of two 3-diagrams and there is a rewrite between the upper
one to the lower. The rewrite is of the shape indicated in the upper left
corner in white: the first two singular levels of the lower diagram are
created from nothing, and the last from the entirety of the original
diagram. This makes the rewrite non-globular since the second regular level
of the bottom diagram does not agree with the first regular level of the
top one. The problematic subdiagram is indicated by the yellow boxes and is
non-globular precisely because the bigger diagram is.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#119 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACQ4OHW5ZXKP5WRRZ44OYMLT6N37VANCNFSM5ATULR3Q>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>
.
|
|
Last week there was a bugfix to typechecking. It's possible that this disallows for the creation of @HdXu's diagram in the first place. Previously we had been assuming that it was well-formed, but this is evidence to suggest that it's not. |
|
Yes worth a try but we need to make sure we never get into this situation
again. A runtime diagram consistency checker will make sure of that.
…On Tue, 24 Aug 2021, 12:28 Nick Hu, ***@***.***> wrote:
Last week there was a bugfix to typechecking. It's possible that this
disallows for the creation of @HdXu <https://github.com/HdXu>'s diagram
in the first place. Previously we had been assuming that it was
well-formed, but this is evidence to suggest that it's not.
If it's simple to recreate, that would be the first step.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#119 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACQ4OHVPTIZX26AGC6VK6XTT6N64NANCNFSM5ATULR3Q>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>
.
|
|
I will write the globularity checker now. @jamievicary would it make sense to check for globularity in the same method as the commutativity checker I wrote last week, or should it be a different method? |
|
Actually, never mind that doesn't make sense. The globularity checker needs to know the source and target diagrams as well as the rewrite, so it should be a different method. |
|
It would certainly make sense to have a generic well-formed diagram
consistency checker that can be on during runtime, that checks all aspects
of diagram validity.
This particular check would make most sense in the rewrite constructor I
think, I'm not sure how consistent that is with the previous one you wrote.
Where is that being called?
…On Tue, 24 Aug 2021, 13:01 Calin Tataru, ***@***.***> wrote:
I will write the globularity checker now. @jamievicary
<https://github.com/jamievicary> would it make sense to check for
globularity in the same method as the commutativity checker I wrote last
week, or should it be a different method?
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#119 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACQ4OHQN4XIILTSP4K5H2FLT6OC3JANCNFSM5ATULR3Q>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>
.
|
|
The previous one is only called in factorisation, as that is the only place (as far as I know) where you may produce malformed diagrams/rewrites. It makes sense for the diagram validity checker (i.e. |
|
So filename_todo-19 is malformed and was caused by a bug in factorisation. That was fixed by #150 so it's not reproducible anymore. |
|
I checked all the diagrams in this bug again to figure out if there is still anything left to fix:
|
|
Since the original issue has been fixed by smoothing, I'm going to close this. I have started another issue to investigate the remaining malformed diagram (singularityIII). |
|
I don't think the first singularity is resolved by the smoothing?
…________________________________
From: Calin Tataru ***@***.***>
Sent: Wednesday, August 25, 2021 4:47:54 PM
To: homotopy-io/homotopy-rs ***@***.***>
Cc: HdXu ***@***.***>; Mention ***@***.***>
Subject: Re: [homotopy-io/homotopy-rs] Fail of contracting an isolated singularity III (#119)
Closed #119<#119>.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub<#119 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AIO5LWKDMISYLKCBDT5JQ53T6UGCVANCNFSM5ATULR3Q>.
Triage notifications on the go with GitHub Mobile for iOS<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android<https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>.
|
|
It should be, I tried it earlier. Just click on regular level 0 and drag upwards. |
|
Sorry, I misspoke. You cannot do smoothing in that example because you would end up with a diagram that has no singular levels. But if you have the same example within a larger diagram, it's fine. |
|
It's ok to have a diagram with no singular levels!
…On Wed, 25 Aug 2021, 22:25 Calin Tataru, ***@***.***> wrote:
Sorry, I misspoke. You cannot do smoothing in that example because you
would end up with a diagram that has no singular levels. But if you have
the same example within a larger diagram, it's fine.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#119 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACQ4OHQ4KKDDVOMOOA2IO6LT6VNWHANCNFSM5ATULR3Q>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>
.
|
I cannot contract the following type of singularity in the current UI setting.
Screenshot
Demo File
bug-isolated singularity3.hom.zip
Addition:
screenshots
singularity
regular levels
another demo file
bug-isolated singularity4.hom.zip
Now, if we create a pair of braids at the singular level like this
and then try to contract the top two nodes, this causes a panic.
error report
panicked at 'assertion failed:
(left == right)left:
[Cospan { forward: RewriteN { dimension: 1, cones: [] }, backward: RewriteN { dimension: 1, cones: [] } }, Cospan { forward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: Cospan { forward: Rewrite0(0:0, 1:2), backward: Rewrite0(0:0, 1:2) }, slices: [] } }] }, backward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: Cospan { forward: Rewrite0(0:0, 1:2), backward: Rewrite0(0:0, 1:2) }, slices: [] } }] } }],right:
[Cospan { forward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: Cospan { forward: Rewrite0(0:0, 1:2), backward: Rewrite0(0:0, 1:2) }, slices: [] } }] }, backward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: Cospan { forward: Rewrite0(0:0, 1:2), backward: Rewrite0(0:0, 1:2) }, slices: [] } }] } }, Cospan { forward: RewriteN { dimension: 1, cones: [] }, backward: RewriteN { dimension: 1, cones: [] } }]', homotopy-core/src/diagram.rs:265:13The text was updated successfully, but these errors were encountered: