mei

putting this on my reading list: https://yangzhixuan.github.io/NbE.html

Normalisation by evaluation is known to be more efficient in practice than substitution-based normalisers. Glueing proofs nicely explains why normalisation by evaluation is correct, but I find that they don’t tell us much about why normalisation by evaluation is fast. In this article, I will try to shed some light on the latter question by showing how we can spot the sources of inefficiency in a naive substitution-based normaliser, optimise these inefficiency problems with some standard algorithmic tricks, and eventually obtain NbE. In fact, through this process we will also see some inefficiency problems in NbE, and in the end we will end up with a normaliser that is asymptotically better than a standard NbE normaliser on some input (and never worse on all input).