# Elementary Tutorial on Normalization-by-Evaluation

This tutorial was originally meant as a five-minute introduction to normalization-by-evaluation (NBE) for undergraduates. It is elementary because it assumes only the elementary school Math as background. No programming experience is necessary either. This tutorial can even be played as a game with shells on a seashore. The rules are elementary, but the game is not always simple. Playing on a seashore may well be a good occasion to see that computation, reduction, normalization, proofs of progress and preservation -- are just games of shuffling symbols.

There may be some who peer beyond symbols, who view them as shadows of real things, who look for intuitions behind the seemingly arbitrary rules and seek to grasp the meaning of the game. Such people are no doubt to discover NBE -- as it has been done many times before. This tutorial is to prompt the rediscovery.

## Set up

Let us start with a game/puzzle, which is a simple version of many an exercises in elementary school. It is played with bags and bundles. A bag may be empty, which we write as `[]`, or containing one or more shells, written as `#`. Shells are game tokens without distinctions: two bags with three shells each are two copies of the same bag, and written identically as `[###]`. A bundle is either a bag, or a tie-up of two bundles, shown by writing the two bundles side-by-side separated by a comma, with the parentheses around. Here are a few sample bundles: `[##]`, `([##],[])`, `([##],([###],[#]))`; the first one is also a bag. Let us be pedantic and say that nothing else is a bundle (resp. bag); for example, `[[]]` or `(#,[&])` are not bundles because they are not made of zero or more `#` enclosed in brackets, possibly paired up.

The game is thus: given a bundle find another one that is `equivalent', or `equal', but `simpler' -- ultimately, the simplest. Great many games, er, exercises in school, are of this form. For example, we would be given a `bundle' like `5x - 3 = 3x + 7` and asked to find the equivalent but simplest (`x = 5`, in our case).

To start playing we have to say exactly what it means for two bundles to be equal, and to be simpler.

References
Our game is actually a variation on Chap. 3 of B. Pierce's `Types and Programming Languages'. That whole textbook is a collection of progressively more complicated symbol-shuffling games -- although they are not called as such.

## Equality

It is entirely up to us to make the rules of our game, in particular, to define the `sameness', or the equality, of bundles. We can do it by pointing at two bundles and declaring them equal -- or, by writing the two bundles around the `~` sign: `([#],([##],[###])) ~ ([##],([#],[###]))`. To state many such equality declarations we need a more concise way of writing them, like the following.

We declare that `([],[S])` is equal to `[S]` where `S` stands for an arbitrary number of shells including zero. We further declare that `([#S],([T],[U])) ~ ([S],([#T],[U]))`, where where `S` and `T` and `U` stand for an arbitrary number of shells, and `#S` stands for one more shell than `S` (the same for `#T`). Finally, we say that in a tie-up of two bags, the order is irrelevant. With fewer words, the declarations may be written as

```    (Ax0)  ([],[S]) ~ [S]
(Ax1)  ([#S],([T],[U])) ~ ([S],([#T],[U]))
(AxS)  ([S],[T]) ~ ([T],[S])
```
where (Ax0), (Ax1) and (AxS) are the names of the declarations, to refer to them later (we refer to all three as (Ax01S)). These are so-called schematic declarations, with the variables `S`, `T` and `U` standing for some arbitrary number of shells. Using variables to concisely express an (infinite) set of declarations is akin to using indefinites and pronouns in natural languages to make a statement about (infinitely) many particular cases. For example, (Ax0) can be voiced as: ``The tie-up of the empty bag with a bag is equal to that bag''.

It is also `natural' to declare any bundle to be equal to itself; the order of the bundles in the equality declaration should not matter either. All in all, we extend the set of equality declarations with the following rules (to be collectively referred to as (Deduc)):

```    (Refl)  A ~ A
(Symm)  If A ~ B then B ~ A
(Trans) If A ~ B and B ~ C then A ~ C
(Cong)  If A ~ B then (A,C) ~ (B,C) and (C,A) ~ (C,B)
```
where `A`, `B` and `C` stand for arbitrary bundles. For example, the rule (Trans) says that if `A`, `B`, `C` are three bundles and we have already found out (from the declarations (Ax01S) and applications of (Deduc)) that `A` is equal to `B` and `B` is equal to `C`, we hereby declare that `A` is equal to `C`. Incidentally, instead of enumerating (Deduc) to complete the definition of the equality, one could have said that our equality is the reflexive, symmetric, transitive and compatible closure of (Ax01S). Or, shorter, the equality is the the smallest congruence that contains (Ax01S). Or, even shorter: a (finitary) equational theory of (Ax01S) -- which is the name we will be using.

One may have noticed a sleight of hand: why was it `natural' to adopt (Refl)? A glib answer is that from experience, a game without (Deduc) is not very interesting. One may have sensed though that perhaps the game is not as mindless and arbitrary as we (or the proponents of the syntactic approach) pretend it to be. Hold this thought.

We set up the rules of the game, in particular, the basic equality declarations such as (Ax01S) as we wish. Is the equality really that arbitrary? May equality declarations be `wrong' or `worse' than others? The shuffling of symbols has no inherent `truth' or `goodness'. Setting up the equality is indeed arbitrary. There is however one case to keep in mind.

Suppose we add one more declaration to the equational theory (Ax01S):

```    (AxU) ([#],[]) ~ ([],[])
```
One one hand, by (Ax0), `([],[]) ~ []`. On the other hand, by (AxS), `([#],[])` is equal to `([],[#])`, which, by (Ax0), is equal to `[#]`. By (Trans), we obtain that `[#] ~ []`, which leads us to conclude that all bags are equal, and, eventually, all bundles are equal.

Exercise: Demonstrate that in the equational theory of (Ax01S,AxU) all bags are indeed equal to `[]`, and hence, all equal. Start by demonstrating that `[##] ~ []`.

Exercise: Demonstrate that in the equational theory of (Ax01S), if we assume that all bags are equal, then all bundles are equal.

The fact that in (Ax01S,AxU) everything is equal does not per se condemn the theory: after all, at the level of games, there is no notion of good and bad. It is our game, we can do what we want. One cannot shrug a feeling however that a degenerate equational theory is not very useful, or interesting. Again we defer dealing with feelings until later. For now, let's state one criterion of quality of an equational theory -- non-triviality: there are two things in its domain which are not equal.

Exercise: Make a case that (Ax01S) is non-trivial.

Exercise: Consider an equational theory (Empty) that has no equality declarations other than (Deduc). It is in some sense opposite of the trivial equational theory like (Ax01S, AxU). In which sense?

Exercise: Demonstrate that in the equational theory (Ax01S) we have `(A,B) ~ (B,A)` for arbitrary bundles `A` and `B`, not just bags. We will come to this exercise again, but one should really try it now.

References
In our game, bags contain shells, not variables. There are no variables in bundles either. Variables come only in equality schemas, as a rhetorical device to concisely state an infinite number of declarations -- similar to indefinites in natural languages. In universal algebra, however, it is customary to add variables to the syntax of terms -- in which case we have to add to (Deduc) the rule that a variable may be replaced (that is, instantiated) with an arbitrary term. That rule is often combined with (Cong) to give what is called the substitution rule: replacing instances of the same variable with equal terms preserves the equality.

## The winning strategy

Having defined the equality, we are yet to say what is `simpler'. That is simple: of two equal bundles one is simpler if it has fewer tie-ups. We are ready to play: who finds the simplest bundle equal to the given?

Here is the first strategy: given a bundle, find out all its equal bundles and choose the simplest. To be more concrete: find a big empty box and put the initial bundle in there. Then repeat the following: pick a random bundle from the box, make a copy and return the original to the box. Check to see if the left-hand side or the right-hand-side of any instance of any (Ax01S) declaration is identical to the bundle in hand or a sub-bundle of it. Replace the matching sub-bundle with the other hand-side of the matching declaration, and put the new bundle into the box unless it was already there. For example, suppose we hold `([##],[#])` in hand. Its sub-bundle `[#]` matches the right-hand-side of an instance of (Ax0): `([],[#]) ~ [#]`. Replacing the sub-bundle with the left-hand-side gives `([##],([],[#]))`, which is the new bundle to put into the box.

This trivial procedure has a non-trivial property: it produces all and only bundles that are equal to the given, according to the rules (Ax01S) as well as (Deduc). Indeed, the initial bundle is still in the box, as (Refl) says it should be. Applying (Ax01S) to sub-bundles follows (Cong). Thus (Deduc) does `naturally' come out, doesn't it? Do try to convince yourself that only equal bundles are produced and any bundle equal to the original shall eventually be in the box, after some finite number of repetitions of the procedure. Is this trivial to see?

What is easy to see are the drawbacks: the procedure goes on forever. The right-to-left application of (Ax0), demonstrated above, always applies, replacing a bag with a bundle. Not only we never stop, we also keep generating more and more complex bundles, getting further away from the goal.

Upon reflection, we are not really interested in all bundles equal to the given; only in those that lead us to the goal, e.g., being simpler. Producing equal bundles should be more focused. Previously we applied an instance of an equality declaration (Ax01S) either left-to-right or right-to-left to produce an equal bundle. The right-to-left application adds a new tie-up but the left-to-right application removes, simplifying the bundle. Let us then apply (Ax0) only left-to-right. It is not clear however how to orient (Ax1) and (AxS), which, especially the latter, do not obviously simplify anything. There is the second problem: `(([#],[#]),([#],[#]))`. The oriented (Ax0) does not apply, (Ax1) does not apply in any direction, and swapping the bags per (AxS) does not give anything new. One may hence conclude that this is as simple as it gets -- loosing the game, as we shall see.

Exercise: Can you find a simpler bundle equal to `(([#],[#]),([#],[#]))`? Which equality declarations did you use to demonstrate the equality?

Here is a more elaborate proposal: we orient (Ax0) as described earlier; orient (Ax1) left-to-right; apply (Symm) and (Trans) to (Ax0) and (AxS) deriving `([S],[]) ~ [S]` and use it both ways. All in all, we get the following rules to produce new bundles:

```    (R0)  ([],[S]) -> [S]
(R1)  ([#S],([T],[U])) -> ([S],([#T],[U]))
(R0S) [S]      -> ([S],[])
(RS0) ([S],[]) -> [S]
```
Here (R0), (R1), (R0S) and (RS0) are the labels for easy reference; all four rules are to be called (R01S). We write the rules with the arrow instead of the `~` sign, showing the direction of their application. Thus given a bundle, find a sub-bundle that matches the left-hand-side of one of the above rules (where the variables are replaced with the appropriate number of shells). Replace the sub-bundle with the right-hand-side of the rule, obtaining the new equal bundle. There may be many choices. For example, given `([#],([],[]))`, we may apply (R1) to the entire bundle (with `S`, `T` and `U` standing for zero number of shells), obtaining `([],([#],[]))`. Or we may apply (R0) or (RS0) to the sub-bundle `([],[])` obtaining `([#],[])`. Or we may apply (R0S) to any of the contained bags, obtaining `(([#],[]),([],[]))` and `([#],(([],[]), []))` and `([#],([],([],[])))`.

As an example, let's see if we can simplify the problematic bundle from the earlier exercise. Shown below is the sequence of produced bundles, and the rules applied:

```    (([#],[#]),([#],[#]))
-> (([#],[#]),([#],([#],[])))           By (R0S)
-> (([#],[#]),([],([##],[])))           By (R1)
-> (([#],[#]),([##],[]))                By (R0)
-> (([#],[#]),[##])                     By (RS0)
```

Exercise: Complete the example and produce simpler bundles. What is the simplest you could get?

Since the rules (R01S) are the particular cases of the equality declarations, applying them assuredly produces the bundles equal to the original. As to producing simpler bundles -- (R0S) is the odd one out, leading to a more complex bundle. Furthermore, it can apply again and again. Thus our system of rules is not generally terminating.

Yet there exists a way of making choices in applying the rules: the winning strategy. It leads to the simplest possible equal bundle for any given bundle -- in a finite number of steps. Can you formulate this strategy? Can you convince yourself that it always works?

Exercise: Recall the earlier exercise: Demonstrate that in the equational theory (Ax01S) we have `(A,B) ~ (B,A)` for arbitrary bundles `A` and `B`, not just bags. Has it become easier?

Exercise: Can you come up with another winning strategy of using the rules (R01S)? Or perhaps you can find another system of bundle-producing rules that invariably leads to the simplest equal bundle no matter how we apply the rules?

Exercise: From the beginning we were talking about the simplest equal bundle. Nothing in general guarantees it exists: there might be different bundles all equal to the original and maximally simple in the defined sense (in our game, having no tie-ups). Could you offer an argument why in our game the simplest bundle does exist, that is, simplest bundles are unique?

References
The oriented equalities, or rules, are technically called reductions, and the game of producing new bundles (or, terms) by re-writing their subterms according to the rules is called term re-writing. Ideally, no matter how we chose rules and sub-terms to apply, we invariably get to one term to which rules no longer apply -- the so-called normal form. That is, all strategies are winning (if a normal form is the goal).
Our system (R01S) is not ideal: there are strategies (choices of the rule application) that go on forever. Furthermore, the simplest bundle is not, strictly speaking, a normal form, because (R0S) can apply to it too. In many games played in Programming Language theory, the goal is not synonymous with a normal form either: there often is a pre-conceived objective, against which we judge the result of reductions. We shall talk about the meaning next. Incidentally, we will see that NBE applies even to less than ideal re-writing systems, like ours.

We obtained the reductions (R01S) by orienting the equalities (Ax01S) or their combinations. Transforming a set of equalities to an ideal term rewriting system is the objective of Knuth–Bendix completion algorithm. Besides equalities, the algorithm takes as input the reduction ordering on terms (that is, the `simplicity ordering'). It does not always succeed. Although we did not follow the algorithm, we have illustrated its key steps: orienting, combining, and discarding of equalities.

Instead of starting with equalities and then trying to complete them, one may start by postulating reductions. The equational theory is then definable as the least congruence containing the reductions. Such an approach is often used in Programming Language theory.

Generating all bundles equal to the original and looking for the one with some desired properties is called bottom-up evaluation in Prolog/Datalog. It pays to be focused and generate only those things bringing us closer to the goal -- which is called `magic set re-writing' in logic programming.

## What does this all mean?

We did our best to present the game as the mindless shuffling of bags and shells -- yet did occasionally wonder if its rules are `natural', `good', `interesting'. One cannot help making analogies, on which to base intuitions and value judgements. One can dismiss them as `pure metaphysics' -- or one can take them seriously, formalize, and use rigorously as any other mathematical theory.

In talking about bags of shells, it is hard not to think of the number of shells in a bag -- and use the number to mentally label the bag, to signify the bag, to take to be the meaning of the bag. One may likewise take the total number of shells in a bundle to be the meaning of the bundle. Is this a good, useful intuition? Let's check if it is compatible with the rules of the game: the equations.

To make the talk about meaning more precise and less verbose, we need notation. If `A` is a bag or a bundle, we write `{A}` for its meaning -- in our case, the total number of shells in it. It can be computed as

```    { [] }    = 0
{ [#S] }  = 1 + { [S] }
{ (A,B) } = {A} + {B}
```
Observe that the meaning of a tie-up `(A,B)` is determined only from the meaning of the tied-up bundles `A` and `B` -- and not from their shape, structure, etc. The meaning, hence, does not depend on the context: a bundle, say, `([##],([###],[#]))` means the number 6 -- whether it is taken by itself or as a part of a more complicated bundle. Our meaning assignment is thus modular -- or, technically speaking, `compositional'.

Let us now look at the meaning of the equality declarations. Recall (Ax0): `([],[S]) ~ [S]`. Its left-hand-side means `{ ([],[S]) }`, which is `{[]} + {[S]}`, which, with a bit of arithmetic, is `{[S]}` -- the meaning of the right-hand-side. As an equality declaration, (Ax0) is just that: a juxtaposition of two bundles with the `~` sign in-between. It is neither true nor false. If we interpret bags and bundles as numbers, (Ax0) comes to mean an elementary-school algebraic equality `0+x=x` -- which is the true equality. We may now speak of the truth.

All in all, for (Ax01S) we have the following interpretation:

```    (Ax0)  0 + x = x
(Ax1)  (1 + x) + (y + z) = x + ((1 + y) + z)
(AxS)  x + y = y + x
```
where `x`, `y` and `z` are some numbers (the meanings of some bags `[S]`, `[T]` and `[U]`). These are all true elementary-school algebraic equalities.

For (Deduc), we have

```    (Refl)  x = x
(Symm)  If x = y then y = x
(Trans) If x = y and y = z then x = z
(Cong)  If x = y then x + z = y + z and z + x = z + y
```
which are the true statements about equality on numbers -- in fact, about equality in general. That is why we called (Deduc) natural: it reflects the fundamental intuition of equality.

Thus, the way we assigned meaning, a natural number, to a bag or bundle is consistent with equality declarations: turning each declaration into a true elementary-school algebraic equality. Technically, one says that natural numbers as meanings plus the way of assigning them to bags and bundles is a model of the equational theory (Ax01S). We will refer to this model as (Nat01S). Since any equality declaration in the theory (Ax01S) turns into the true equality in (Nat01S), whenever two bundles are equal in (Ax01S), they have the same natural number as their meaning in (Nat01S). One could say that the things that are equal in theory are actually equal in `practice' (i.e., in the model).

What about the converse: are the bundles that mean the same natural number in (Nat01S) are equal in (Ax01S)? That is, if `{A} = {B}` then `A ~ B` is an instance of (Ax01S) or a combination of them according to (Deduc)? This seems like a useful, and rather strong, proposition. Is it true? How does one even go about demonstrating it?

That equality in `practice' (model) implies equality in theory is indeed hard to demonstrate in general. Luckily, in our case, the hard work has already been done: establishing the winning strategy that reduces any bundle to its equal bag. (The exact formulation of that strategy was an exercise to the reader.) Consider two bundles `A` and `B` with the same meaning. Let's apply the winning strategy to `A` and obtain the bag `A'`. Recall, the winning strategy (or actually any strategy of applying reductions (R01S)) produces only equal bags. Therefore, `A ~ A'`. Applying the winning strategy to `B` gives the bag `B'` such that `B ~ B'`. Anything that is equal in theory is equal in model, therefore, `{A} = {A'}` and `{B} = {B'}`. Since `A` and `B` have the same meaning by assumption, then `{A'} = {B'}`, which means by the meaning assignment of (Nat01S) that the bags `A'` and `B'` have the same number of shells: they are identical. Thus we obtain that `A ~ A'` and `B ~ A'`; by (Symm) and (Trans) we have to conclude that `A ~ B`.

The just demonstrated property is called completeness. It means that the notions of equality in (Nat01S) and (Ax01S) coincide. It is very useful, and hence goes by many names: the equational theory (Ax01S) is the complete theory of (Nat01S); (Ax01S) is complete for (Nat01S); (Ax01S) is an axiomatization of (Nat01S).

Recall again our running exercise: Demonstrate that in the equational theory (Ax01S) we have `(A,B) ~ (B,A)` for arbitrary bundles `A` and `B`, not just bags. It has become trivial, has it not? Since `(A,B)` and `(B,A)` have the same number of shells, they are equal in the model (Nat01S), and hence, by completeness, equal in the theory (Ax01S). We can thus prove many more interesting facts about (Ax01S).

Exercise: Demonstrate that in the equational theory (Ax01S) we have `(A,(B,C)) ~ ((A,B),C)` for arbitrary bundles `A`, `B` and `C`.

Exercise: A game may have many models, depending on what aspects of the game one is interested to model. Here is another model for our game: the meanings are the booleans, `true` and `false`, and the meaning assignment is

```    { [] }    = false
{ [#S] }  = not { [S] }
{ (A,B) } = xor {A} {B}
```
where `not` is the boolean negation and `xor` is the exclusive or. Convince yourself that it is a model of (Ax01S). Is (Ax01S) complete for this model? If no, what could be added to (Ax01S) to make the theory complete?

Exercise: What is a model of the trivial equational theory (Ax01S,AxU)? What is a model of (Empty)?

Exercise: Here is yet another model: the meanings are integers, and the meaning assignment is

```    { [] }    = 0
{ [#] }   = 1
{ [##S] } = 2
{ (A,B) } = ({A} + {B}) mod 3
```
How a complete equational theory of that model may look like? What would be the simplest bags?

## Normalization by Evaluation

One of the applications of completeness, of (Ax01S) for (Nat01S), is the normalization-by-evaluation (NBE). Consider a bag such as `(([#],[#]),([#],[#]))`. To find the simplest bag equal to it, we may apply the winning strategy -- which takes a rather few steps. On the other hand, we may find the meaning of the bundle: `{(([#],[#]),([#],[#]))} = (1+1)+(1+1) = 4`, which is the elementary calculation. Then the bag `[####]` with 4 shells is the simplest bag equal to the original. If `N` is a natural number, let `!N` be a bag with `N` shells. Then the algorithm of finding the simplest form of any bundle `A` is hence: `!{A}`.

NBE is thus a way to win the mindless game by round-tripping through semantics. That is the point of assigning meaning: to relate the obscure to the familiar. We may then rely on what we already know about the meaning objects such as numbers, use our intuitions and judgements, speak of truth and goodness.

References
In the most general formulation, to perform NBE for a set `X` of objects, we introduce another set `M` of meanings with two functions between them: `eval: X -> M` and `reify: M -> X`. The set `M` should have (easily) computable equality. Above we wrote `eval x` as `{x}` and reify as the exclamation mark. The two functions should satisfy the natural conditions that the domain of `reify` be equal to the range of `eval` (so that the composition `reify . eval` is defined) and `eval (reify m) = m` for all `m` in the domain of `reify`. Then according to NBE, a `normal form' of `x in X` is defined to be `reify (eval x)`.

Although thus obtained `normal form' fits the intuitions (it means the same in `M` as the original term and performing NBE twice is the same as doing it once), it is weak to be useful. One wants to relate the normal form `reify (eval x)` to the original `x` in the world of objects `X` (not just in the world of meanings `M`). One wants to say that `reify (eval x)` is equal to `x`. To be able to say that, however, we have to first define equality on `X` -- either by equality declarations or reductions. Alternatively, we may define equality on `X` model-theoretically, by introducing another, `canonical' set of meanings `W` with the corresponding mapping from `X` to `W`, and defining two elements of `X` as equal just in case they have the same meaning in `W`.

## Connections

Although the formalistic method -- the mindless game -- is commonly associated with Hilbert school, one of its earliest advocate was the philosopher C.I.Lewis, who formulated it, as a `heterodox view of the logistic method', in perhaps the most concise way:
``A mathematical system is any set of strings of recognizable marks in which some of the strings are taken initially and the remainder derived from these by operations performed according to rules which are independent of any meaning assigned to the marks.''
[C.I. Lewis, A Survey of Symbolic Logic, 1918, p. 355] cited from Alasdair Urquhart: Emil Post

Emil Post took this `heterodox view' to the heart. He introduced the consistency and completeness criteria without any appeal to meaning. They now bear his name. We have mentioned the consistency criterion in Equality: not everything should be equal. Post also introduced the most general symbol-shuffling game framework: Post system, with by now familiar inference rules. The inference rules have now become the standard way to specify grammars, write logical and type-system derivations, reductions in programming systems -- and, in general, to present algorithms in Programming Language theory. Our game of bags and bundles is a Post system. Thus Lewis' `heterodox view' has now become orthodox.

The view that Lewis objected to -- looking for meaning behind the `marks', as a guidance and intuition -- has a long history, going back to Plato and his doctrine of Forms. One can see in his writing the concepts of meaning assignments (evaluation) and reification.

Lewis heterodox view and Hilbert formalism were rooted in positivism. To positivist philosophers (Vienna Circle) and many mathematicians of 1920s and 1930s, talking about meaning and truth was `metaphysics', better avoided. It was Alfred Tarski who demonstrated that truth can be defined rigorously, in a mathematically acceptable way. Model theory, started by Tarski, Robinson and Maltsev, showed that `meaning' can not only be mathematically respectable, but also fruitful. NBE is just another evidence of that.

References
Alasdair Urquhart: Emil Post
Handbook of the History of Logic. Volume 5. Logic from Russell to Church. Dov M. Gabbay and John Woods (Editors), 2008 Elsevier BV.

Silverman, Allan: Plato's Middle Period Metaphysics and Epistemology
The Stanford Encyclopedia of Philosophy (Fall 2014 Edition), Edward N. Zalta (ed.)
<https://plato.stanford.edu/archives/fall2014/entries/plato-metaphysics/>
Plato's doctrine of Forms and the metaphor of the Cave

Alfred Tarski: Truth and Proof
Scientific American, 1969, pp. 63-77.

Hodges, Wilfrid: "Model Theory"
The Stanford Encyclopedia of Philosophy (Fall 2018 Edition), Edward N. Zalta (ed.)
<https://plato.stanford.edu/archives/fall2018/entries/model-theory/>

Linnebo, O/ystein: Platonism in the Philosophy of Mathematics
The Stanford Encyclopedia of Philosophy (Spring 2018 Edition), Edward N. Zalta (ed.)
<https://plato.stanford.edu/archives/spr2018/entries/platonism-mathematics/>

References
Peter Dybjer and Andrzej Filinski: Normalization and Partial Evaluation
APPSEM 2000: International Summer School on Applied Semantics, Advanced Lectures. Springer LNCS 2395, 2002, 137--192
<http://www.diku.dk/~andrzej/papers/NaPE.pdf>
This is a proper, extensive tutorial on NBE, assuming quite a bit more background

Andreas Abel: Normalization by Evaluation -- Dependent Types and Impredicativity. 2013. Habilitationsschrift. Institut fuer Informatik Ludwig-Maximilians-Universitaet Muenchen
A quite more advanced exposition and survey with extensive bibliography

Evaluators, Normalizers, Reducers: from denotational to operational semantics
Even the reduction semantics can be presented as a form of NBE

Sound and Efficient Language-Integrated Query -- Maintaining the ORDER
NBE for optimizing database queries

Embedded probabilistic programming
NBE for optimizing probabilistic programs: variable elimination in exact inference

Type-directed partial evaluation
Danvy's TDPE was an one of many independent (re-)discoveries of NBE

## Conclusions

Normalization-by-Evaluation thus can be approached just by playing simple games and thinking about winning moves and strategies. The game is mindless and its rules are arbitrary. Yet it turns out that by looking for the meaning behind the rules, relating game tokens and moves to familiar objects gives us intuitions about the play -- and also the method to win it. In short, NBE is a way to win purely syntactic games by round-tripping through semantics.

NBE is almost inevitable once we start thinking about meaning behind symbols or objects. One can discern the key concepts of NBE already in Plato's writing, in particular, in his metaphor of the Cave. In recent times, NBE has been discovered independently in several communities: partial evaluation and type theory, to name the two. As far as we can see, the first documented discovery was not by a computer scientist, but by a philosopher: Per Martin-Loef.