Zhixuan Yang

@DDOtten Thank you so much for the feedback! I am very happy to know you liked the post!

I think your nf8 computes the normal form correctly, but I am worrying about the cost when arguments are repetitively reified. When you cache the normal form of an argument, shift 0 i is applied to the normal form, but the normal form may become a part of the normal form of another argument, which needs reification and shift 0 again.

In particularly, for the following term

-- t = (\x. \y. y x) ((\x. \y. y x) (...))
t :: Int -> Tm
t 0 = Abs (Var 0)
t n = Abs (Abs (Var 0 `App` Var 1)) `App` t (n-1)

where the cached normal form of the argument contains the cached normal form of the argument of the cached normal form of the argument.... nf8 is slow on my machine:

-- >>> fv (nf8 (t 10000))

but nf5 is fast:

-- >>> fv (nf5 (t 10000)) -- -1

(By the way, embarrassingly, the updated nf7 in the current version of my post is in fact incorrect... I am still thinking about if it can be saved...)

Just edited the post because I came up with the right way to lazy shifting of de Bruijn indices for the very last normaliser (apart from using freshly named variables that @AndrasKovacs told me yesterday). Also fixed a strictness bug. I had to duplicate the definition of some functions only for different strictness/laziness annotations. Is "strictness polymorphism" a thing?

@AndrasKovacs thanks so much for the pointers! I am quite ignorant about the existing literature on efficient normalisation so these pointers are extremely useful to me

https://yangzhixuan.github.io/NbE.html

My (rather long) blog post on normalisation by evaluation is online now. In this post I show how we can optimise a naive substitution-based applicative-order normaliser of untyped calculus step by step, leading us to reconstruct NbE as "weak-applicative-order normalisation with meta-level laziness, lazy substitution, and de Bruijn levels". We will also examine some "adversarial exploit" that makes NbE slow and use the insights gained from our reconstruction of NbE to optimise NbE.