@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...)