Daniël Otten

@zyang That makes a lot of sense and further explains the motivation for the steps in nf7 for me. Thank you for your quick reply!

@zyang (cc, @AndrasKovacs) Thank you for the interesting blog post! It really helped me to understand the optimizations that NbE applies.

After reading the original blog post I also tried thinking about ways to simplify nf7 and I worked out one alternative (https://github.com/DDOtten/NbE-cached/blob/main/NbE.hs)

I implemented a further variation (nf8 at the end of the file) that avoids the need for the forceShifts function. This change is based on storing the number of shifts at the root of the cached normal forms: instead of storing a ~TmS with lazy weakenings we store a ~Tm and the number of shifts that need to be applied to the normal form for this specific occurrence.

I hope the computational complexity of nf8 is the same as nf7, since both have to traverse every cached normal form once per occurrence to apply the needed shifts (which depend on the number of additional binders encountered before substituting this occurrence), but I have not worked this out in detail yet.

I did compare the output and performance of (both the original and newly updated) nf7 and nf8 on the original adversarial example and two new large adversarial examples, and they match, with nf8 being slightly faster on my computer. However, a more detailed analysis of computational behavior is needed, so please let me know if I made any mistakes!