Normalisation by evaluation とは

プログラミング言語のセマンティクスでは、評価による正規化(NBE)は、その意味論的セマンティクスをアピールして、λ計算の用語の正規形を得るスタイルです。まず、用語をλ項構造の記号モデルに解釈し、その正規表現(βノーマルとηロング)の代表を抽出する。このような本質的な意味論的アプローチは、正規化のより伝統的な構文的記述と異なり、βリダクションがλ項の中で深く許される項書き換えシステムの削減である。
NBEは、単純にタイプされたラムダ計算について最初に記述された。それ以来、ドメイン理論的アプローチを用いたタイプのないラムダ計算や、Martin-Löf型理論のいくつかの変形などのより豊かなタイプのシステムにまで拡張されてきた。