\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Normalization by Evaluation

Table of Contents

1. Overview

A common project for functional programming courses is to implement a typed lambda calculus. There are a variety of ways to do this, but we will focus on the technique of Normalization by Evaluation. Basically, we encode the object language as syntactic objects, then we translate it into the implementing language for evaluation (or evaluate it through some other means), and finally translate back to the object language. Amazingly enough, this works.

To be clear, by "evaluate it by some means", what we really mean is we will use the denotational semantics of the language to evaluate expressions.

2. Example: Simply-Typed Lambda Calculus

Suppose we had simply-typed lambda calculus with some set of base types, products, and function types. We encode these using an algebraic data type: 

(* Syntactic types *)
datatype Type = Basic of string
              | Fun of Type * Type
              | Pair of Type * Type;

Now, terms in the object language are then encoded using syntactic terms, as distinguished from terms in the metalanguage used for evaluation. We have the syntactic terms: 

datatype Term = var of string
              | lam of string * Term (* lam (var_name, body) *)
              | app of Term * Term
              | pair of Term * Term
              | fst of Term
              | snd of Term;

It may prove useful to use de Bruijn indices or locally nameless variables, when encoding syntactic terms. I'm not sure whether I'll do it or not.

The semantic terms are precisely interpretations of the syntactic terms as elements of the metalanguage. We have 

datatype Sem = LAM of (Sem -> Sem)
             | PAIR of Sem * Sem
             | SYN of Term;

We need to move back-and-forth from the "syntactic level" and the "semantic level". The terminology used for translations moving from one level to the other are standardized as:

  • Reification (intuitively "evaluation"), denoted \(\downarrow^{\tau}\), constructs a syntactic representation of a "well-behaved" semantic value, and
  • Reflection, denoted \(\uparrow_{\tau}\) constructs "well-behaved" semantic values from pieces of syntax.

These are mutually recursive functions defined by the following equations:

\begin{align} \uparrow_{\alpha} t &= \mathbf{SYN}\ t \\ \uparrow_{\tau_1 \to \tau_2} v &= \mathbf{LAM} (\lambda S.\ \uparrow_{\tau_2} (\mathbf{app}\ (v, \downarrow^{\tau_1} S))) \\ \uparrow_{\tau_1 \times \tau_2} v &= \mathbf{PAIR} (\uparrow_{\tau_1} (\mathbf{fst}\ v), \uparrow_{\tau_2} (\mathbf{snd}\ v)) \\[1ex] \downarrow^{\alpha} (\mathbf{SYN}\ t) &= t \\ \downarrow^{\tau_1 \to \tau_2} (\mathbf{LAM}\ S) &= \mathbf{lam}\ (x, \downarrow^{\tau_2} (S\ (\uparrow_{\tau_1} (\mathbf{var}\ x)))) \text{ where } x \text{ is fresh} \\ \downarrow^{\tau_1 \times \tau_2} (\mathbf{PAIR}\ (S, T)) &= \mathbf{pair}\ (\downarrow^{\tau_1} S, \downarrow^{\tau_2} T) \end{align}

For any well-typed syntactic term \(s\) of type \(\tau\), its semantic value \(S\) can be reified into the ($β$-normal $η$-long) normal form of \(s\). The process of obtaining the "meaning" of \(s\) we denote by \(\|s\|_{\Gamma}\) where \(\Gamma\) is the context of bindings, defined inductively by:

\begin{align} \| \mathbf{var}\ x \|_\Gamma &= \Gamma(x) \\ \| \mathbf{lam}\ (x, s) \|_\Gamma &= \mathbf{LAM}\ (\lambda S.\ \| s \|_{\Gamma, x \mapsto S}) \\ \| \mathbf{app}\ (s, t) \|_\Gamma &= S\ (\|t\|_\Gamma) \text{ where } \|s\|_\Gamma = \mathbf{LAM}\ S \\ \| \mathbf{pair}\ (s, t) \|_\Gamma &= \mathbf{PAIR}\ (\|s\|_\Gamma, \|t\|_\Gamma) \\ \| \mathbf{fst}\ s \|_\Gamma &= S \text{ where } \|s\|_\Gamma = \mathbf{PAIR}\ (S, T) \\ \| \mathbf{snd}\ t \|_\Gamma &= T \text{ where } \|t\|_\Gamma = \mathbf{PAIR}\ (S, T) \end{align}

In the literature, usually the meaning is denoted using Oxford brackets \([\![t]\!]\) instead of the norm \(\|t\|\).

Then normalization by evaluation may be defined by reifying the meaning of any well-typed syntactic term.

We should prove soundness (if any two syntactic terms are \(\beta\eta\) equivalent, then they will have the same meaning) and completeness (if any two syntactic terms have equal meanings, then they are \(\beta\eta\) equivalent).

2.1. Reification/Evaluation and Alternatives

The "by evaluation" occurs in the reification function. Reification is just evaluation. We implemented it using a crude form of higher-order abstract syntax. There is another popular method, using closures. This seems to be first done in Andreas Abel's thesis. This could be viewed as the defunctionalization of the implementation we sketched above.

"A closure packages an expression that has not yet been evaluated with the runtime environment in which the expression was created."

2.2. Optimizations

The sketchy algorithm from the previous section is a faithful, but naive, implementation of the idea underlying normalization-by-evaluation.

There are various optimizations we could consider. For example, we could use higher-order-syntax more effectively.

  • Klaus Aehlig and Florian Haftmann and Tobias Nipkow,
    "A Compiled Implementation of Normalization by Evaluation".
    PDF
  • Mathieu Boespflug,
    "Efficient normalization by evaluation".
    2009 Workshop on Normalization by Evaluation, ed. Olivier Danvy, Aug 2009, Los Angeles, United States. Eprint: inria-00434283

3. References

  • David Thrane Christiansen, "Checking Dependent Types with Normalization by Evaluation: A Tutorial (Haskell Version)". PDF, 2019.
  • Danvy, Keller, and Puech, "Typeful Normalization by Evaluation". Eprint for OCaml implementation.
  • Lennart Augustsson, Simpler, Easier! Blog post dated 25 October 2007, giving an implementation of dependently typed lambda calculus in Haskell
  • Andres Löh, Conor McBride and Wouter Swierstra,
    "A Tutorial Implementation of a Dependently Typed Lambda Calculus".
    Eprint and code
  • Andreas Abel, "Normalization by Evaluation: Dependent Types and Impredicativity". PDF, PhD thesis (2013), 96 pages
  • Klaus Aehlig and Florian Haftmann and Tobias Nipkow,
    "A Compiled Implementation of Normalization by Evaluation".
    PDF
  • Mathieu Boespflug,
    "Efficient normalization by evaluation".
    2009 Workshop on Normalization by Evaluation, ed. Olivier Danvy, Aug 2009, Los Angeles, United States. Eprint: inria-00434283

Last Updated 2023-02-22 Wed 11:28.