Post by @zyang@mathstodon.xyz

2026-04-22 00:08 UTC

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 &quot;weak-applicative-order normalisation with meta-level laziness, lazy substitution, and de Bruijn levels&quot;. We will also examine some &quot;adversarial exploit&quot; that makes NbE slow and use the insights gained from our reconstruction of NbE to optimise NbE.

Replies (2)

@zyang@mathstodon.xyz 2026-04-24 01:23

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?

Open ##2127769
@AndrasKovacs@mathstodon.xyz 2026-04-22 13:12

@zyang Cool stuff! - This paper is about NbE with term sharing: https://arxiv.org/pdf/2603.21949 Based on this, I attempted a simple Haskell implementation: https://gist.github.com/AndrasKovacs/0e1bc2532e071cef5974ca582f8090ad I'm not completely sure about the correctness of my version, but in the case it's wrong it would be fixed by using global "gensym", like in the paper. - This paper uses a similar evaluator, but since it's a conversion checker, it's quite a bit more complicated: https://hal.science/hal-05322705/document - Another direction of NbE optimization is to reduce space usage by "trimming" environments; this is well-known in closed evaluators but it's been used in normalizers too, e.g. in https://depositonce.tu-berlin.de/items/512ba4cd-ff0c-4f33-a5c2-a8fdc66dc03c and probably in the Rocq VM (not sure).

Open ##2127770