-
Notifications
You must be signed in to change notification settings - Fork 134
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Normalizing proof of commutativity +-comm #149
Comments
That is very strange! There seems to be an exponential blow-up. This does not happen for +-suc, so I think the problem must come from the use of compPath which builds a bunch of hcomp's. The number of them should be linear though, so I would expect this to be linear as well. @Saizan Thoughts? |
I think you are right that the culprit is compPath, it seems more expensive to increase the second argument, which is the one creating more compositions. Also, using |
Ok, it's a problem of sharing for partial elements, basically hcomp has to look at the partial elements to decide if they are a constructor and then recurse. However, because of how partial elements are manipulated, the recusive call has to reduce the original partial element from scratch. The reason for this inefficiency is that there isn't a good way to generate partial elements during reduction at the moment. Currently the only way to produce non-trivial partial elements on the fly is For naturals and other builtin types with literals we should also have custom implementations that take advantage of the compact representation available for closed terms. E.g., for Nat, |
I noticed a massive speed-up in cubicaltt when computing hcomp as you suggest for closed terms of datatypes. It's not clear to me how we can utilize this in the presence of open terms though... But if we write an efficient closed term evaluator we should definitely use this optimization. |
In agda's internals, 100 is represented as |
Won't this force the sides to always be evaluated? I tried this in cubicaltt and it made things extremely slow because we couldn't rely on laziness to avoid unfolding things |
For open computation we have to reduce the sides to WHNF anyway. For compositions that are known to be closed we can just use the base, that would be a different optimization. |
I see. Please try to optimization then! A good benchmark is: https://github.com/agda/cubical/blob/master/Cubical/Experiments/Problem.agda#L69 It should evaluate to refl at pos 0. I cubicaltt it is instant (with the optimization for hcomp in nat) but in Cubical Agda it never terminated for me. |
Might be good, but unless I'm missing something it's not a benchmark involving |
Optimized Normalizing @wvhulle would you like to test it out? |
I will close this as my testing indicates it's much better now. |
Normalizing the application of
+-comm
to cubical numerals fails for relatively low values such as for example in+-comm 4 6
. Is this normal expected behaviour? Normalization works for any number when the implementation of the numerals in the standard library is used.The text was updated successfully, but these errors were encountered: