HVM eats all my RAM and then segfaults about hvm HOT 4 CLOSED

I ran some tests measuring the number of rewrites HVM does to compute (sub big big) using this script and got this:

plot rewrites × big

It seems the rewrites grow quadratically with respect to big, not linearly. Perhaps this is related to #60? I'll run the tests again on the quadratic_fix branch and see if anything changes.

from hvm.

Huh, I guess let big = (double (inc (double zero)) doesn't work in quadratic_fix? It keeps reducing until it segfaults. (double, inc and zero are defined in the script)

Changing the representation of big to let big = λs λz (s (s (s ... (s z)))) fixes this segfault, but the runtime is still apparently quadratic, a bit worse than the other representation, and the number of rewrites doesn't change at all between master and quadratic_fix. (note: I'm not sure if this representation changes the complexity of sub...? hopefully my analysis is correct)

plot

from hvm.

It could be related to that issue, yes. Probably is. I don't have the time to troubleshoot right now, but if anyone voluntaries, it is possible to trace the entire reduction with hvm -d your_term and manually inspect. This is very laborious, but can give us an insight on exactly where and why HVM is losing its asymptotic advantage. As I commented on the other thread, an easy fix would be to just add references, but that is also an extreme solution which would bring several disadvantages. Sadly Andrea Asperti didn't answer my question regarding this issue; I'd highly appreciate a clarification from a related researcher. HVM is just implementing the optimal evaluation algorithm, so, if this isn't a bug on HVM (which may be the case!), this program counts as a counter-example to its asymptotical optimality.

from hvm.

If I may ask, could you move this information to #60? This definitely should be on the pinned thread.

from hvm.