Normalization by Evaluation Four Ways: Reconstructing NbE Designs from First Principles

I’ve been trying to learn normalization by evaluation (NbE) the past week, and have been getting hung up on different presentations. Why do some implementations look so different from others: some have reify and reflect, while some have only read-back (which appears to be reify)? Why do some have explicit type-annotated injection from normal to neutrals?

In this tutorial, I’ll rederive various designs for NbE from first principles. We’ll start with an evaluator for the simply typed λ-calculus, and from it derive some normalizer. But, whenever practical, we’ll stop and question a design decision, and explore how this gives us a slightly different normalizer.

1 The Syntax

This describes the syntax, represented as quasiquote’d lists, λ-calculus terms. For example, the following is an Expression: `(lambda (s) (lambda (x) (s x))).

The definition is incomplete. We need the following definitions of Base and Variable

2 A Semantics

Next, we define the semantics for this syntax. That is, we define a definitional interpreter for these expressions. That is, we define a meta-circular evaluator for this language.

We interpret Base?s as itself, λ functions as semantics/meta functions.

This semantics is sound with respect to the syntax. Here’s a little example:

The semantics does give us values of terms we can reason about. In the above example, I perform addition on Church numeral in the syntax, and I get a semantic value that acts like meta-language natural numbers.

But, how do I know this semantics is right? For one, I’d like to know the semantics is sound with respect to our syntax: two β-equivalent things result in the same value:

If I had a better meta-language, I might be able to prove that rather than test it. Maybe I’ll redo this in Agda later.

But I’d also like to know that this semantics is complete: and two equal values are in fact β-equivalent.

I might also want to be able to get back the syntax of a value. If the semantics is sound, then that value ought to be equal to its β-normal form, so getting back to its syntax ought to give me a normal form, i.e., going from syntax, to value, to syntax should be normalization.

Turns out, these are essentially the same question. If I can go from syntax, to value, to syntax, and what I get is β-equivalent to what I started with, then my sound semantics is also complete.

3 Digression: Refining the Type of the Syntax

That’s better; now we know eval never has to deal with unbound variables. But it still might have to deal with ill-typed terms: what is I ask for the semantics of `(,(base 5) ,(base 5))? That’s nonsense.

Phew; now its a semantics.

But that’s a lot of details that mostly doesn’t contribute to understanding the normalizers, so I’m going to stick with the simplified definition.

4 The Normalizer

Before our digression, we want to know if we can go from values back to syntax. There is some reason to do this, both practically (to get a normalizer) and theoretically (to prove completeness).

Well. This code almost works, but it’s not well typed. Here’s what it does: if the value is a Base?, we just return that, since it’s an expression. If the value is a procedure? (a semantic function), we want to construct a syntactic λ whose body is the result of reifying the value you get after applying the semantic function to the fresh syntactic variable.

But that application is not well typed, since the semantic function takes a Value, but a Variable is not a Value.

But now we break an invariant in our evaluator: semantic application expected a procedure?, but it might get a Variable. This is easier to see in the indexed definition of Value:

We could also view this through the definition of Value: (1) do we allow a Variable to be a (Value `(-> ,A ,B)), or (2) only allow a Variable to be a (Value 'Base)]?

4.1 Choice {1} The Intensional Residualizing Semantics

Notice that since we might apply a Variable in the application case, we must extend Value further to allow stuck expressions other than Variables to be considered Values. In general, we extend Value to include any Neutral term. A Neutral is either a Variable or an elimination form (function application, in our case) whose target operand is a Neutral.

If we pick option one, do-app will be simpler and unconnected with our normalizer. If we pick option two, do-app must call into the reifier to transform the v2 into an Expression.

4.1.1 Choice {1,1} The Intensional Residualizing Readback Semantics

In this semantics, we inject all terms, including neutral terms, into the domain of Values, then separately read back any Value (including neutral values) into an Expression. I call this the readback semantics, since the process of getting Values back to Expressions has this one-way loop producing syntax, reminiscent of (but in the opposite direction of) the reader.

Now we can define reify, or as its called in this presentation, read-back-11, properly. However, since Values can be Neutrals, we also need a second definition, read-back-neutral-11, which takes Neutrals to Expressions.

In a sufficiently rich meta language, we could prove this semantics sound and complete.

4.1.2 Choice {1,2} The Intensional Residualizing Reify Semantics

Instead of embedding Values in Neutrals, we could eagerly transform a Value back into an Expression when building a Neutral. This makes the evaluator and the normalizer mutually recursive, but means all Neutrals are by construction Expressions, which makes reasoning a little easier.

The type definitions are as follows:

Then, in do-app, we call into reify.

The major difference is the result of a term with a λ function as an argument, which we can observe in semantic application of a neutral to function values:

4.1.3 Digression: Refining reify’s Type: Normal or Expression

We actually could have arrived at Choice {1,2} The Intensional Residualizing Reify Semantics through another route, had we introduced a third choice: whether or not to refine the type of reify when we started defining it.

Had we decided to refine the type of reify to guarantee it produces not arbitrary Expressions, but only Normal Expressions, we would probably have ended up with an equivalent NbE design to Choice {1,2} The Intensional Residualizing Reify Semantics.

Observe that all the "Expression"s produced by reify-12 are Normal. Had we started by designing that refined type, we may not have been tempted to define NeutralValue at all, since we already had a perfectly good Neutral.

4.2 Choice {2} The Extensional (Meta-circular) Semantics

Back-tracking all the way to the top of our choice tree, we could have decide to change reify-1 to transform a Variable into a Value before trying to apply the semantic function to the Variable.

To do this, we need to know something about the variable: it’s type. Is it a function, or a base? If it’s a base, then we can just return it, since a Base is also a Value. Otherwise, we need to construct a semantic function.

First we modify both reify and reflect to take a type. We use the same syntax of types, Type, introduced in Digression: Refining the Type of the Syntax. Then, we define reflect recursively on the type argument.

We had to generalize the type so instead of taking a Variable, it takes a Neutral Expresson.

Intuitvely, when we have a Variable at function type, we want to build a semantics function that will, given a Value of type A, produce a Value of type B. To build the right function, we need to "apply" n. Except we can’t apply it; it’s a variable. So we want to build a neutral application of that variable. But that means we must convert the value v to a Normal Expression, so we reify it. By generalizing reflect-2, we can continue reflecting that Neutral to a Value.

This requires the following modified definition of reify-2, which now must return a Normal. We must also update it to be recursive on the type, rather than the term.

That is, a Neutral is a Value only at type 'Base. That is the only situation where a Neutral term must be returned from reflect-2.

This design decision is a very nice one. It forces us into a good design, refining the type of reify to insist it produces a Normal. It completely reuses the existing semantics, rather than requiring the semantics to be modified. It leads to single syntactic definition of Neutral rather than raising questions about whether it should be include exotic subterms from the semantic domain.

5 A Secret Third Thing: The Extensional Residualizing Semantics

Implicit in our starting semantics was another choice: to use a meta-circular semantics, or not. The meta-circular semantics is quite natural for a denotational semantics of a simple syntax, or as quick and efficient interpreter for a simple language. However, we might have wanted to reason about semantic functions inductively. Or perhaps we wanted to enrich our semantic functions with more structure. Or perhaps we wanted to implement our interpreter with explicit closures.

From this definition, how do we build the normalizer?

Previously, reflect built a semantic function. In the body of that semantic function, the call to reify was delayed until a real semantic Value was produced. Now, however, we’re trying to build closure. We don’t have a semantic value, so what do we pass to reify? What environment do we use for the closure? How do we reflect a closure, which is not a neutral?

We can’t define reflect, so let’s see if we can change where we use reflect. This call in reify is at fault: (reify B (do-app-c v (reflect A x))). We cannot reflect that variable if its a function type. So here’s an idea: we modify do-app to work on Neutrals. We’re sort of forced into the design choice in Choice {1,1} The Intensional Residualizing Readback Semantics, although with one additional complication: since reify now requires a type, we’ll need to remember the type of Neutral values.

We make reflect into a syntactic construct, which embeds a Neutral with its type into the domain of semantic values.

We inline the base case of the definition of reflect, to unwrap the any remaining neutrals. (Try leaving out that case and running the following example to understand it better.)

6 Full Implementation