NORMALIZATION BY EVALUATION to simplify a term, run it — then read the answer back as syntax
Normalization by evaluation (NbE) computes the normal form of a term by a surprising detour: instead of rewriting the syntax step by step, it evaluates the term in a semantic domain (reflect), then reads the value back into syntax (reify). Running the term does the simplification; the read-back recovers a term in normal form. It reuses the meta-language's own evaluator as the normalizer — no explicit reduction rules to iterate. Berger & Schwichtenberg found this “inverse of the evaluation functional,” and it is the conversion-checker inside proof assistants like Agda (and MINLOG, its original home), where terms must be compared up to computation.
THE TECHNIQUE reflect (evaluate) then reify (read back) → normal form
Normalizing (λx. x) 9 by evaluating then reading back. The demo reflects to a value and reifies to the normal form 9: live demo
HISTORY & CREDIT Berger & Schwichtenberg, 1991
“To normalize a term you must rewrite it rule by rule.” — NbE just evaluates it and reads the value back; running the term is the normalization. The evaluator you already have becomes the normalizer. cited
1991 · Ulrich Berger & Helmut Schwichtenberg — “An inverse of the evaluation functional”: reflect/reify normalization. lineage · the reflect/reify pair; later named “normalization by evaluation” (Berger, Danvy). now · the conversion-checker in Agda (and MINLOG, its original setting); Coq and Lean kernels instead use lazy weak-head reduction (Coq also compiled reduction — vm_compute).
Evaluate to simplify, read back to recover syntax: the normal form falls out of running the term. The evaluator, inverted, is a normalizer. Berger-Schwichtenberg 1991
RECOMMEND FOR I-13 reflect/reify normal form, computed
On the canonical compiler, normalizing (λx. x) 9 reflects to the value 9 and reifies to the normal form 9:
$ i13 run m_nbe.i13 # normalize (\x.x) 9 via reflect/reify
RUN OK . 9 step(s) . peak stack 2 . call depth 1
reflected = 9
normal_form = 9
Recommend: NbE's move — run the term to simplify it — is one i13 makes constantly, just not for proofs. i13 has an evaluator (its IVM) but no separate rewrite engine and no notion of comparing terms up to computation, because it is not a proof assistant: it runs programs, it does not normalize them. Still, the deep idea resonates with i13's benchmark, whose JIT keys its cache on a semantic hash (two syntactically different programs with the same meaning are one cache entry) — a reflect-then-compare in spirit. NbE is the disciplined, typed version of “meaning, not syntax” that i13 already leans on informally.