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.
[], 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.
~ 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.
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?
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.
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?
(([#],[#]),([#],[#])). 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.
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.
``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.
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/>
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
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.