Section. Adversarial Exploit of NbE [nbe-adversarial-example]

We shall not stop at NbE. With our knowledge gained in the reconstruction of NbE, let's push NbE further. Recall that the reason that led to using weak-applicative-order normalisation is that when we normalise App f a, the optimal thing to do for the function f is to normalise it just enough to expose its outermost lambda abstraction. However, for the argument a we chose to also normalise it to expose the outermost lambda abstraction because the argument a may be used as a function in the body of f. Our strategy for f is good, but our strategy for a is based on the assumption that a will be used as a function inside f later.

Of course this assumption doesn't always hold. For an extreme example, we can have a term (with a free variable x)

(\y. x y y y y y ... y) (expensiveTm 100)

where the argument expensiveTm 100 is used as arguments in the function body 1000000 times. NbE would be very slow on this term because the term expensiveTm 100 would be normalised to weak normal forms before (lazy) substitution, and then in the function body it would be duplicated 1000000 times, and the NbE would reify the weak normal form of expensiveTm 100 1000000 times, one time for each occurrence of y.

nbeAdversarialExploit :: Tm
nbeAdversarialExploit =
  Abs (foldr (\_ r -> r `App` Var 0) (Var 1) [1..1000000]) `App` expensiveTm 100

On this term, our naive normaliser nf0 takes a few seconds to compute on my laptop:

-- >>> fv (nf0 nbeAdversarialExploit)
-- 0

But our best NbE normaliser nf5 takes a much longer time:

-- >>> fv (nf5 nbeAdversarialExploit)
-- ProgressCancelledException

Let's fix this problem in the rest of this article. The plan is simple: when we (weakly) normalise App f a, we create a lazy thunk of the full normal form of a and pass it to the function body of f. Later when we reify a value and see a thunk of a full normal form in a spine, we can just force this thunk. In this way, if the argument a is used in the function body f many times as arguments in a spine, they would share the same thunk of the full normal form.

The plan is simple, but a technical difficulty is that when we weakly normalise App f a and creates the thunk of the full normal form a' of a, the de Bruijn level where a' is created will be different from the de Bruijn level where a' will be used inside the function body f. This highlights the disadvantage of de Bruijn levels over de Bruijn indices: a closed term with de Bruijn indices is stable if we move this term to some other locations, while a closed term with de Bruijn levels is not stable. For example, consider the following term in the context of one free variable x:

(\z. x (\w. z)) (\y. y y)

Using de Bruijn levels, the free variable x is represented by 0, and y is represented by 1. However, if we substitute \y. y y for z, we obtain x (\w. (\y. y y)), where y should be shifted to 2 (because w is 1).

To fix this problem, we shall revert back to use de Bruijn indices instead of de Bruijn levels. Recall that previously we switched from de Bruijn indices to levels when optimising nf3 to nf5 to save the time of shifting de Bruijn indices. But we mentioned that we had another solution to do this: lazy tagging. Therefore let's first do another optimised version of nf3 using lazy shifting of de Bruijn indices.