Open 3abc opened 5 years ago
I made some tests and this doesn't seem to make things faster... I ran testShortcut4To5 (after applying https://github.com/mortberg/cubicaltt/commit/7d70bea5a8d9c540c6b0a765a62e4f43f612ff7b) and the timing is actually 1s slower.
@ecavallo has some alternative definition of this map that completely avoids the lemmas that this patch affects, however this doesn't seem to make things faster either. So the strange slowdown in the latter maps doesn't seem to come from this.
@ecavallo has some alternative definition of this map that completely avoids the lemmas that this patch affects, however this doesn't seem to make things faster either. So the strange slowdown in the latter maps doesn't seem to come from this.
I think the most time consuming part is from the map h
sending test0To4
to test0To5
? At least on my computer I can't have cubicaltt to compute normal form of test0To5
. For that I think we either need to greatly simplify the proof of decodeEncode
or find a direct proof of a special case of isSet loopS1
setLoopRefls : (r : Path loopS1 refl refl) → r ≡ refl
The part that using g2TruncElim
is f7
sending test0To6
to test0To7
, I think it's already kinda fast in cubicaltt if the input is not too complicated? Like testShortcut3To6
shows. However this version of g2TruncElim
can be really useful in Agda, at least it greatly simplifies normal form of things like multTwoTilde base2 (g2squashC x y p q r s u v i j k l)
. For the version using J
it was 400k lines and 20 min, for this version it's almost instant.
Yeah, test0To5 definitely needs to get faster. However f8 (kappaTwo) seems to cause a massive combinatorial explosion. Try the following:
> :n f7 (f6 (f3 test0To2))
...
> :n f8 (f7 (f6 (f3 test0To2)))
...
> :n f8 (f7 (f6 (f3 (f6 (f3 test0To2)))))
...
This map seems very innocent so I wonder what is going on. I think the problem might be that we are running truncPath2
to compute the path that we are transporting in, and this might end up being extremely complex. Another definition of this map could speed things up a lot in the latter part of the computation.
I think the problem might be that we are running
truncPath2
to compute the path that we are transporting in, and this might end up being extremely complex. Another definition of this map could speed things up a lot in the latter part of the computation.
Oh yeah a direct definition of kappaTwo
will be awesome.
Oh yeah a direct proof of
kappaTwo
will be awesome.
The map is defined in B.10 (page 155) of https://arxiv.org/pdf/1606.05916.pdf
Maybe someone can come up with a more efficient definition? @ecavallo @loic-p
The case we need here is n=2 and A=S^2.
Oh yeah a direct proof of
kappaTwo
will be awesome.The map is defined in B.10 (page 155) of https://arxiv.org/pdf/1606.05916.pdf
Maybe someone can come up with a more efficient definition? @ecavallo @loic-p
The case we need here is n=2 and A=S^2.
Evan seems to have figured it out: https://github.com/mortberg/cubicaltt/pull/110
Those new maps seem to have linear complexity in the number of hcomps in the input. This is a huge improvement to f8-f10 that were seemingly at least exponential.
The next step is to optimize f5. I have some ideas for how to do it, but I really have to work on a grant proposal so it might be a few weeks before I work on it
PS: the idea to hopefully optimize f5 is to use Loic's definition of the map from the total space of the Hopf fibration to S1 * S1 instead of the "tee" map (https://github.com/mortberg/cubicaltt/blob/pi4s3_nobug/examples/brunerie2.ctt#L925):
https://github.com/agda/cubical/blob/master/Cubical/HITs/Hopf.agda#L60
As Loic's map is defined for the Hopf fibration defined using the suspension of S1 we will have to change a bunch of other things in f5 as well. One way to quickly test it might be to insert the map:
https://github.com/mortberg/cubicaltt/blob/pi4s3_nobug/examples/brunerie2.ctt#L927
somewhere but I'm not sure where. If someone experiments with this please keep me posted.
Evan seems to have figured it out: #110
Those new maps seem to have linear complexity in the number of hcomps in the input. This is a huge improvement to f8-f10 that were seemingly at least exponential.
Just one observation: I just did :n (g9 (g8 (f7 (f6 (f3 test0To2)))))
and there's a lot of empty systems. However it doesn't cause much problem since after applying g10
they all disappear.
NORMEVAL: hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z) (hcomp (sTrunc Z)
[...] (the full term has 13.3K characters, use option -f to print it)
]) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []) []
#hcomps: 604
Time: 0m0.065s
Wow, this should be better in Cubical Agda then... Once we have a perfected version of f5 it should be fairly straightforward to port the definition and try it there.
PS: the idea to hopefully optimize f5 is to use Loic's definition of the map from the total space of the Hopf fibration to S1 * S1 instead of the "tee" map (https://github.com/mortberg/cubicaltt/blob/pi4s3_nobug/examples/brunerie2.ctt#L925):
https://github.com/agda/cubical/blob/master/Cubical/HITs/Hopf.agda#L60
Is there any heuristic for one to believe this new map is better than the one defined by tee
?
Is there any heuristic for one to believe this new map is better than the one defined by
tee
?
I seems simpler and shorter. But this is very hard to judge without trying, so we will have to see empirically :)
Wow, this should be better in Cubical Agda then... Once we have a perfected version of f5 it should be fairly straightforward to port the definition and try it there.
I used -f
and it turns out to be just (sinc (pos (suc zero)))
with 604 empty systems...
Is there any heuristic for one to believe this new map is better than the one defined by
tee
?I seems simpler and shorter. But this is very hard to judge without trying, so we will have to see empirically :)
I ported it now:
https://github.com/mortberg/cubicaltt/blob/pi4s3_nobug/examples/brunerie2.ctt#L972
It doesn't seem faster... But more testing and experimenting is necessary.
I used a lemma called
g2TruncFib
similar tosetTruncFib
.Just one remark, for
g2TruncFib
(and similarlysetTruncFib
) to work we don't need thatgP x
is a 2-groupoid for allx
. We actually only need it to be a 2-groupoid at the fiber overb
. However I choose to keep the type unchanged. But this could be useful at some point where not all fibers are known to be 2-groupoid.