Skip to content


Fabian edited this page Oct 18, 2021 · 5 revisions
Clone this wiki locally

From syntax to semantics and back: Demystifying NbE

by Nachi


Traditional normalization techniques transform a term to normal form by repeatedly applying syntactic transformations specified by a reduction relation. Normalization by Evaluation (NbE), on the other hand, normalizes a term by evaluating it in a host language, and then reifying the resulting value back into term syntax. But why is the resulting term in normal form? And what reduction steps were applied to produce it? The involvement of semantics (host language) complicates understanding NbE for those of us who understand normalization as a syntactic transformation procedure.

In this talk, I intend to motivate a syntactic explanation for this semantic procedure. Concretely, we will implement NbE for a simple combinator language with primitive recursion (combinatorial System T) on the whiteboard (then Agda). To expose the underlying reduction sequence, we will then enhance this implementation with the ability to "log" the reduction steps. Furthermore, we will package the ability to produce a normal form with a reduction trace to show that NbE yields a proof of weak normalization.

All the ideas in this talk are based on the paper "Intuitionistic model constructions and normalization proofs" by Dybjer and Coquand. If time permits, I will also briefly discuss the glueing construction from this paper in the context of NbE.

Code and Exercises


  1. Intuitionistic model constructions and normalization proofs. T Coquand and P Dybjer
  2. Normalization and Partial Evaluation. P Dybjer and A Filinski