Fail of contracting an isolated singularity III

[HdXu]

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:13

Stack: Error at x (https://beta.homotopy.io/235.js:1:9598) at console_error_panic_hook::hook::h6aba13f31c7bca6d (https://beta.homotopy.io/a42196c9b2dfd942658e.module.wasm:wasm-function[915]:0x1485fe) at core::ops::function::Fn::call::h042126be8e13bf49 (https://beta.homotopy.io/a42196c9b2dfd942658e.module.wasm:wasm-function[2620]:0x197219) at std::panicking::rust_panic_with_hook::hbdbceb5cd158bf19 (https://beta.homotopy.io/a42196c9b2dfd942658e.module.wasm:wasm-function[1676]:0x18523b) at std::panicking::begin_panic_handler::{{closure}}::h9995bb2f0de4bb38 (https://beta.homotopy.io/a42196c9b2dfd942658e.module.wasm:wasm-function[1851]:0x18d0f1) at std::sys_common::backtrace::__rust_end_short_backtrace::hc7608161a467c002 (https://beta.homotopy.io/a42196c9b2dfd942658e.module.wasm:wasm-function[2189]:0x194ce5) at rust_begin_unwind (https://beta.homotopy.io/a42196c9b2dfd942658e.module.wasm:wasm-function[2133]:0x194154) at core::panicking::panic_fmt::h3ab5417155b7ba3b (https://beta.homotopy.io/a42196c9b2dfd942658e.module.wasm:wasm-function[2190]:0x194d1b) at core::panicking::assert_failed::inner::h67d89b54e013299d (https://beta.homotopy.io/a42196c9b2dfd942658e.module.wasm:wasm-function[1161]:0x162036) at core::panicking::assert_failed::h4f5d05a13e1f913a (https://beta.homotopy.io/a42196c9b2dfd942658e.module.wasm:wasm-function[1962]:0x1907c1)

B @ 235.js:1 console_error_panic_hook::hook::h6aba13f31c7bca6d @ a42196c9b2dfd942658e.module.wasm:0x1486e0 core::ops::function::Fn::call::h042126be8e13bf49 @ a42196c9b2dfd942658e.module.wasm:0x197219 std::panicking::rust_panic_with_hook::hbdbceb5cd158bf19 @ a42196c9b2dfd942658e.module.wasm:0x18523b std::panicking::begin_panic_handler::{{closure}}::h9995bb2f0de4bb38 @ a42196c9b2dfd942658e.module.wasm:0x18d0f1 std::sys_common::backtrace::__rust_end_short_backtrace::hc7608161a467c002 @ a42196c9b2dfd942658e.module.wasm:0x194ce5 rust_begin_unwind @ a42196c9b2dfd942658e.module.wasm:0x194154 core::panicking::panic_fmt::h3ab5417155b7ba3b @ a42196c9b2dfd942658e.module.wasm:0x194d1b core::panicking::assert_failed::inner::h67d89b54e013299d @ a42196c9b2dfd942658e.module.wasm:0x162036 core::panicking::assert_failed::h4f5d05a13e1f913a @ a42196c9b2dfd942658e.module.wasm:0x1907c1 homotopy_core::diagram::DiagramN::rewrite_forward::hef4eaa01bb2bf0d4 @ a42196c9b2dfd942658e.module.wasm:0xfbdf4

::next::h33ed9f69e684013c @ a42196c9b2dfd942658e.module.wasm:0xfb59f as alloc::vec::spec_from_iter::SpecFromIter>::from_iter::hd03e121cb9cc271b @ a42196c9b2dfd942658e.module.wasm:0x11aace homotopy_core::normalization::normalize_relative::he599385955ac9988 @ a42196c9b2dfd942658e.module.wasm:0x20198 homotopy_core::normalization::normalize_relative::he599385955ac9988 @ a42196c9b2dfd942658e.module.wasm:0x21333 homotopy_core::normalization::normalize_relative::he599385955ac9988 @ a42196c9b2dfd942658e.module.wasm:0x2031f homotopy_core::normalization::normalize::h9d19b43f4f659bb7 @ a42196c9b2dfd942658e.module.wasm:0x13f49a homotopy_core::typecheck::typecheck_cospan::hb56978f2b1f85bff @ a42196c9b2dfd942658e.module.wasm:0x91961 homotopy_core::contraction::::contract::{{closure}}::h2e5ac828cba3f32c @ a42196c9b2dfd942658e.module.wasm:0xe30de homotopy_core::attach::attach_worker::hca690786e1c574ea @ a42196c9b2dfd942658e.module.wasm:0xb43af homotopy_web::model::proof::ProofState::update::he9d3f357ecde8691 @ a42196c9b2dfd942658e.module.wasm:0x9cf2 homotopy_web::model::State::update::hc534deb828780a5f @ a42196c9b2dfd942658e.module.wasm:0x2c66c ::update::h2c8328a44d0ecb9a @ a42196c9b2dfd942658e.module.wasm:0x11a7d4 as yew::scheduler::Runnable>::run::h39ba2e481bf20f77 @ a42196c9b2dfd942658e.module.wasm:0x9336f yew::scheduler::Scheduler::start::h49a9c034775ead2e @ a42196c9b2dfd942658e.module.wasm:0x10c026 yew::html::component::scope::Scope::process::ha0ec65fa04fc1879 @ a42196c9b2dfd942658e.module.wasm:0x18caff ::view::{{closure}}::hf972da02dd28c302 @ a42196c9b2dfd942658e.module.wasm:0x18e513 ::attach::{{closure}}::h0a48eb8113e6d213 @ a42196c9b2dfd942658e.module.wasm:0x186ebf +Output = R as wasm_bindgen::closure::WasmClosure>::describe::invoke::h1864696aafdd1a77 @ a42196c9b2dfd942658e.module.wasm:0x1940cf H @ 235.js:1 r @ 235.js:1 a42196c9b2dfd942658e.module.wasm:0x197469 Uncaught RuntimeError: unreachable at __rust_start_panic (a42196c9b2dfd942658e.module.wasm:0x197469) at rust_panic (a42196c9b2dfd942658e.module.wasm:0x195422) at std::panicking::rust_panic_with_hook::hbdbceb5cd158bf19 (a42196c9b2dfd942658e.module.wasm:0x18525f) at std::panicking::begin_panic_handler::{{closure}}::h9995bb2f0de4bb38 (a42196c9b2dfd942658e.module.wasm:0x18d0f1) at std::sys_common::backtrace::__rust_end_short_backtrace::hc7608161a467c002 (a42196c9b2dfd942658e.module.wasm:0x194ce5) at rust_begin_unwind (a42196c9b2dfd942658e.module.wasm:0x194154) at core::panicking::panic_fmt::h3ab5417155b7ba3b (a42196c9b2dfd942658e.module.wasm:0x194d1b) at core::panicking::assert_failed::inner::h67d89b54e013299d (a42196c9b2dfd942658e.module.wasm:0x162036) at core::panicking::assert_failed::h4f5d05a13e1f913a (a42196c9b2dfd942658e.module.wasm:0x1907c1) at homotopy_core::diagram::DiagramN::rewrite_forward::hef4eaa01bb2bf0d4 (a42196c9b2dfd942658e.module.wasm:0xfbdf4) __rust_start_panic @ a42196c9b2dfd942658e.module.wasm:0x197469 rust_panic @ a42196c9b2dfd942658e.module.wasm:0x195422 std::panicking::rust_panic_with_hook::hbdbceb5cd158bf19 @ a42196c9b2dfd942658e.module.wasm:0x18525f std::panicking::begin_panic_handler::{{closure}}::h9995bb2f0de4bb38 @ a42196c9b2dfd942658e.module.wasm:0x18d0f1 std::sys_common::backtrace::__rust_end_short_backtrace::hc7608161a467c002 @ a42196c9b2dfd942658e.module.wasm:0x194ce5 rust_begin_unwind @ a42196c9b2dfd942658e.module.wasm:0x194154 core::panicking::panic_fmt::h3ab5417155b7ba3b @ a42196c9b2dfd942658e.module.wasm:0x194d1b core::panicking::assert_failed::inner::h67d89b54e013299d @ a42196c9b2dfd942658e.module.wasm:0x162036 core::panicking::assert_failed::h4f5d05a13e1f913a @ a42196c9b2dfd942658e.module.wasm:0x1907c1 homotopy_core::diagram::DiagramN::rewrite_forward::hef4eaa01bb2bf0d4 @ a42196c9b2dfd942658e.module.wasm:0xfbdf4 ::next::h33ed9f69e684013c @ a42196c9b2dfd942658e.module.wasm:0xfb59f as alloc::vec::spec_from_iter::SpecFromIter>::from_iter::hd03e121cb9cc271b @ a42196c9b2dfd942658e.module.wasm:0x11aace homotopy_core::normalization::normalize_relative::he599385955ac9988 @ a42196c9b2dfd942658e.module.wasm:0x20198 homotopy_core::normalization::normalize_relative::he599385955ac9988 @ a42196c9b2dfd942658e.module.wasm:0x21333 homotopy_core::normalization::normalize_relative::he599385955ac9988 @ a42196c9b2dfd942658e.module.wasm:0x2031f homotopy_core::normalization::normalize::h9d19b43f4f659bb7 @ a42196c9b2dfd942658e.module.wasm:0x13f49a homotopy_core::typecheck::typecheck_cospan::hb56978f2b1f85bff @ a42196c9b2dfd942658e.module.wasm:0x91961 homotopy_core::contraction::::contract::{{closure}}::h2e5ac828cba3f32c @ a42196c9b2dfd942658e.module.wasm:0xe30de homotopy_core::attach::attach_worker::hca690786e1c574ea @ a42196c9b2dfd942658e.module.wasm:0xb43af homotopy_web::model::proof::ProofState::update::he9d3f357ecde8691 @ a42196c9b2dfd942658e.module.wasm:0x9cf2 homotopy_web::model::State::update::hc534deb828780a5f @ a42196c9b2dfd942658e.module.wasm:0x2c66c ::update::h2c8328a44d0ecb9a @ a42196c9b2dfd942658e.module.wasm:0x11a7d4 as yew::scheduler::Runnable>::run::h39ba2e481bf20f77 @ a42196c9b2dfd942658e.module.wasm:0x9336f yew::scheduler::Scheduler::start::h49a9c034775ead2e @ a42196c9b2dfd942658e.module.wasm:0x10c026 yew::html::component::scope::Scope::process::ha0ec65fa04fc1879 @ a42196c9b2dfd942658e.module.wasm:0x18caff ::view::{{closure}}::hf972da02dd28c302 @ a42196c9b2dfd942658e.module.wasm:0x18e513 ::attach::{{closure}}::h0a48eb8113e6d213 @ a42196c9b2dfd942658e.module.wasm:0x186ebf +Output = R as wasm_bindgen::closure::WasmClosure>::describe::invoke::h1864696aafdd1a77 @ a42196c9b2dfd942658e.module.wasm:0x1940cf H @ 235.js:1 r @ 235.js:1

[jamievicary]

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 https://github.com/homotopy-io/homotopy-rs/issues/119, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACQ4OHX2W7BASUB4N2YWU3LTYQNQDANCNFSM5ATULR3Q .

[HdXu]

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.

[jamievicary]

simpler.zip

[jamievicary]

Here try to contract the top two vertices to see the issue

[zrho]

The problematic diagram appears to be constructed somewhere in the restriction code of the type checker. I couldn't localize it any further yet.

[jamievicary]

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 https://github.com/homotopy-io/homotopy-rs/issues/119#issuecomment-888425944, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACQ4OHQ6ZW2D4BS7J2VWKIDT2ASE7ANCNFSM5ATULR3Q .

[HdXu]

Similar panic report:

Demo singularityIII.zip

Screenshot

Log [Error] panicked at 'assertion failed: (left == right) left: [GenericCospan { forward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: GenericCospan { forward: Rewrite0(0:0, 1:2), backward: Rewrite0(0:0, 1:2) }, slices: [] } }], payload: () }, backward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: GenericCospan { forward: Rewrite0(0:0, 1:2), backward: Rewrite0(0:0, 1:2) }, slices: [] } }], payload: () } }, GenericCospan { forward: RewriteN { dimension: 1, cones: [], payload: () }, backward: RewriteN { dimension: 1, cones: [], payload: () } }], right: [GenericCospan { forward: RewriteN { dimension: 1, cones: [], payload: () }, backward: RewriteN { dimension: 1, cones: [], payload: () } }, GenericCospan { forward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: GenericCospan { forward: Rewrite0(0:0, 1:2), backward: Rewrite0(0:0, 1:2) }, slices: [] } }], payload: () }, backward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: GenericCospan { forward: Rewrite0(0:0, 1:2), backward: Rewrite0(0:0, 1:2) }, slices: [] } }], payload: () } }]', homotopy-core/src/diagram.rs:263:13

Stack:

https://beta.homotopy.io/index-62c53504a5ec64bb.js:292:28 wasm-stub@[wasm code] <?>.wasm-function[1527]@[wasm code] <?>.wasm-function[1040]@[wasm code] <?>.wasm-function[1348]@[wasm code] <?>.wasm-function[1361]@[wasm code] <?>.wasm-function[657]@[wasm code] <?>.wasm-function[278]@[wasm code] <?>.wasm-function[302]@[wasm code] <?>.wasm-function[349]@[wasm code] <?>.wasm-function[115]@[wasm code] <?>.wasm-function[115]@[wasm code] <?>.wasm-function[115]@[wasm code] <?>.wasm-function[561]@[wasm code] <?>.wasm-function[156]@[wasm code] <?>.wasm-function[261]@[wasm code] <?>.wasm-function[183]@[wasm code] <?>.wasm-function[247]@[wasm code] <?>.wasm-function[168]@[wasm code] <?>.wasm-function[1034]@[wasm code] <?>.wasm-function[939]@[wasm code] <?>.wasm-function[1106]@[wasm code] <?>.wasm-function[1336]@[wasm code] wasm-stub@[native code] __wbg_adapter_30@https://beta.homotopy.io/index-62c53504a5ec64bb.js:230:139 real@https://beta.homotopy.io/index-62c53504a5ec64bb.js:187:21

(anonymous function) (index-62c53504a5ec64bb.js:304)
wasm-stub
<?>.wasm-function[1527]
<?>.wasm-function[1040]
<?>.wasm-function[1348]
<?>.wasm-function[1361]
<?>.wasm-function[657]
<?>.wasm-function[278]
<?>.wasm-function[302]
<?>.wasm-function[349]
<?>.wasm-function[115]
<?>.wasm-function[115]
<?>.wasm-function[115]
<?>.wasm-function[561]
<?>.wasm-function[156]
<?>.wasm-function[261]
<?>.wasm-function[183]
<?>.wasm-function[247]
<?>.wasm-function[168]
<?>.wasm-function[1034]
<?>.wasm-function[939]
<?>.wasm-function[1106]
<?>.wasm-function[1336]
wasm-stub
__wbg_adapter_30 (index-62c53504a5ec64bb.js:230:140)
real (index-62c53504a5ec64bb.js:187)

[Error] RuntimeError: Unreachable code should not be executed (near '...ehbbfcef5a03f88217(arg0, arg1, addBorr...') <?>.wasm-function[1040] (index-62c53504a5ec64bb.js:230:140) <?>.wasm-function[1348] <?>.wasm-function[1361] <?>.wasm-function[657] <?>.wasm-function[278] <?>.wasm-function[302] <?>.wasm-function[349] <?>.wasm-function[115] <?>.wasm-function[115] <?>.wasm-function[115] <?>.wasm-function[561] <?>.wasm-function[156] <?>.wasm-function[261] <?>.wasm-function[183] <?>.wasm-function[247] <?>.wasm-function[168] <?>.wasm-function[1034] <?>.wasm-function[939] <?>.wasm-function[1106] <?>.wasm-function[1336] wasm-stub wbg_adapter_30 (index-62c53504a5ec64bb.js:230:140) real (index-62c53504a5ec64bb.js:187)

[HdXu]

Demo file filename_todo-19.hom.zip

Error Log [Error] panicked at 'assertion failed: (left == right) left: [GenericCospan { forward: RewriteN { dimension: 1, cones: [], payload: () }, backward: RewriteN { dimension: 1, cones: [], payload: () } }, GenericCospan { forward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: GenericCospan { forward: Rewrite0(0:0, 2:2), backward: Rewrite0(0:0, 2:2) }, slices: [] } }], payload: () }, backward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: GenericCospan { forward: Rewrite0(0:0, 2:2), backward: Rewrite0(0:0, 2:2) }, slices: [] } }], payload: () } }], right: [GenericCospan { forward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: GenericCospan { forward: Rewrite0(0:0, 2:2), backward: Rewrite0(0:0, 2:2) }, slices: [] } }], payload: () }, backward: RewriteN { dimension: 1, cones: [Cone { index: 0, internal: ConeInternal { source: [], target: GenericCospan { forward: Rewrite0(0:0, 2:2), backward: Rewrite0(0:0, 2:2) }, slices: [] } }], payload: () } }, GenericCospan { forward: RewriteN { dimension: 1, cones: [], payload: () }, backward: RewriteN { dimension: 1, cones: [], payload: () } }]', homotopy-core/src/diagram.rs:263:13

Stack:

https://beta.homotopy.io/index-5e3d90191231d939.js:482:28 wasm-stub@[wasm code] <?>.wasm-function[1448]@[wasm code] <?>.wasm-function[996]@[wasm code] <?>.wasm-function[1290]@[wasm code] <?>.wasm-function[1298]@[wasm code] <?>.wasm-function[743]@[wasm code] <?>.wasm-function[202]@[wasm code] <?>.wasm-function[392]@[wasm code] <?>.wasm-function[442]@[wasm code] <?>.wasm-function[116]@[wasm code] <?>.wasm-function[116]@[wasm code] <?>.wasm-function[116]@[wasm code] <?>.wasm-function[482]@[wasm code] <?>.wasm-function[167]@[wasm code] <?>.wasm-function[207]@[wasm code] <?>.wasm-function[190]@[wasm code] <?>.wasm-function[121]@[wasm code] <?>.wasm-function[473]@[wasm code] <?>.wasm-function[1099]@[wasm code] <?>.wasm-function[1060]@[wasm code] <?>.wasm-function[1287]@[wasm code] wasm-stub@[native code] __wbg_adapter_18@https://beta.homotopy.io/index-5e3d90191231d939.js:211:139 real@https://beta.homotopy.io/index-5e3d90191231d939.js:187:21

(anonymous function) (index-5e3d90191231d939.js:494)
wasm-stub
<?>.wasm-function[1448]
<?>.wasm-function[996]
<?>.wasm-function[1290]
<?>.wasm-function[1298]
<?>.wasm-function[743]
<?>.wasm-function[202]
<?>.wasm-function[392]
<?>.wasm-function[442]
<?>.wasm-function[116]
<?>.wasm-function[116]
<?>.wasm-function[116]
<?>.wasm-function[482]
<?>.wasm-function[167]
<?>.wasm-function[207]
<?>.wasm-function[190]
<?>.wasm-function[121]
<?>.wasm-function[473]
<?>.wasm-function[1099]
<?>.wasm-function[1060]
<?>.wasm-function[1287]
wasm-stub
__wbg_adapter_18 (index-5e3d90191231d939.js:211:140)
real (index-5e3d90191231d939.js:187)

[Error] RuntimeError: Unreachable code should not be executed (near '...eh39d61493df4fb466(arg0, arg1, addBorr...') <?>.wasm-function[996] (index-5e3d90191231d939.js:211:140) <?>.wasm-function[1290] <?>.wasm-function[1298] <?>.wasm-function[743] <?>.wasm-function[202] <?>.wasm-function[392] <?>.wasm-function[442] <?>.wasm-function[116] <?>.wasm-function[116] <?>.wasm-function[116] <?>.wasm-function[482] <?>.wasm-function[167] <?>.wasm-function[207] <?>.wasm-function[190] <?>.wasm-function[121] <?>.wasm-function[473] <?>.wasm-function[1099] <?>.wasm-function[1060] <?>.wasm-function[1287] wasm-stub wbg_adapter_18 (index-5e3d90191231d939.js:211:140) real (index-5e3d90191231d939.js:187)

[zrho]

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.

[jamievicary]

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 https://github.com/homotopy-io/homotopy-rs/issues/119#issuecomment-903860126, 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 .

[jamievicary]

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 https://github.com/homotopy-io/homotopy-rs/issues/119#issuecomment-903860126, 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 .

[zrho]

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.

[jamievicary]

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 https://github.com/homotopy-io/homotopy-rs/issues/119#issuecomment-903920457, 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 .

[zrho]

Looking at the original diagram which produced the non-globular restriction, it looks like the original itself was non-globular to begin with: 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.

[jamievicary]

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 https://github.com/homotopy-io/homotopy-rs/issues/119#issuecomment-904540948, 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 .

[NickHu]

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. If it's simple to recreate, that would be the first step.

[jamievicary]

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 https://github.com/homotopy-io/homotopy-rs/issues/119#issuecomment-904556136, 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 .

[calintat]

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?

[calintat]

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.

[jamievicary]

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 https://github.com/homotopy-io/homotopy-rs/issues/119#issuecomment-904576291, 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 .

[calintat]

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. Diagram::is_well_formed) to also check that every rewrite in the diagram is globular. Currently, it only checks that the rewrites are well-formed and compatible with the slices of the diagram.

[calintat]

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.

[calintat]

I checked all the diagrams in this bug again to figure out if there is still anything left to fix:

• bug-isolated singularity3 is well-formed. I don't see what the issue was here @HdXu?
• bug-isolated singularity4 is well-formed and the panic can no longer be reproduced (fixed by #150)
• simpler is malformed and can no longer be reproduced (fixed by #150)
• singularityIII is malformed but I can't tell if it's reproducible. @HdXu do you remember how you constructed this?
• filename_todo-19 is malformed and can no longer be reproduced (fixed by #150)

[calintat]

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).

[HdXu]

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 #119https://github.com/homotopy-io/homotopy-rs/issues/119.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://github.com/homotopy-io/homotopy-rs/issues/119#event-5207771071, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AIO5LWKDMISYLKCBDT5JQ53T6UGCVANCNFSM5ATULR3Q. Triage notifications on the go with GitHub Mobile for iOShttps://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Androidhttps://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email.

[calintat]

It should be, I tried it earlier. Just click on regular level 0 and drag upwards.

[calintat]

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.

[jamievicary]

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 https://github.com/homotopy-io/homotopy-rs/issues/119#issuecomment-905887039, 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 .