Evaluators, Normalizers, Reducers: from denotational to operational semantics

Introduction

Taking the call-by-value untyped lambda-calculus with De-Bruijn--indexed variables, integers and integer operations as an example, we embed it in OCaml and demonstrate several interpreters. Notable among them are two normalizers, which turn a lambda-calculus term into the corresponding value term (weak normal form), if it exists. One normalizer is `denotational', based on normalization-by-evaluation. The other is a reducer.

The reducer normalizes terms by successive rewriting -- finding a redex and reducing it -- until it either gets stuck or produces a value. The reducer is instrumented to count the number of reduction steps. The reducer is written to be as close as possible to the familiar big-step or structural operational semantics of the calculus. Therefore, its count of reduction steps can be trusted to represent the complexity of term reduction.

The tagless-final style is designed around a compositional mapping of terms of the embedded DSL to the values in some `repr` domain -- i.e., denotational semantics. Operational semantics in the tagless-final style did not seem possible all. After all, to find a redex we have to pattern-match on a term. Performing an application, i.e., substituting into abstraction's body, calls for more pattern-matching. Tagless-final terms are not represented by a data type (AST); how do we pattern-match on them? This article demonstrates, explaining how to search for a redex and substitute in the tagless-final style. Operational semantics turns out not only possible but also relatively straightforward and even profitable (e.g., letting us short-circuit the substitution when the variable in question does not appear in the term).

Version
The current version is June 2019, based on fragments written in 2011
References
reducer.ml [23K]
The complete code for all the interpreters, plus many examples and tests

The calculus and its denotational semantics

Our calculus is the untyped call-by-value lambda-calculus with De-Bruijn--indexed variables, integers, and operations to increment an integer and to branch on zero. It can be presented as the following OCaml signature:
```    module type Lambda = sig
type repr

val vz  : repr               (* variable of the De Bruijn index 0 *)
val vs  : repr -> repr       (* next De Bruijn index (weakening) *)

val lam : repr -> repr       (* abstraction *)
val (/) : repr -> repr -> repr  (* application *)

(* Constants *)
val int : int  -> repr                (* integer literal *)
val inc : repr -> repr                (* successor *)
val ifz : repr * repr * repr -> repr  (* branch on zero *)
end
```
The calculus is an instance of a lambda calculus over an algebraic signature, which in our case contains zero-arity function symbol (constant) for each natural number; the arity one constant for the successor `inc`, and the arity three constant `ifz`. Incidentally, the full `Lambda` signature is also algebraic.

The signature `Lambda` can be read as the context-free grammar of the language: `repr` is the start symbol and `lam`, `inc`, etc. are the terminals. In the conventional CFG notation it would look as:

```    repr -> "vz"
repr -> "vs" repr
repr -> "lam" repr
...
```
This grammar derives, for example, `lam vz` -- the identity combinator.

OCaml programmers might look at `Lambda` as defining a set of OCaml functions to construct terms of the embedded calculus. All such terms are represented as OCaml values of the abstract type `repr`. Thus `vz` is the term for the 0-index free variable, and `lam` is the OCaml function that constructs the lambda-abstraction term given the term for the abstraction's body. Thus `lam vz` is the OCaml expression that evaluates to the value of the type `repr` that represents the identity combinator. Since we use OCaml expressions to construct lambda-calculus terms, we follow OCaml syntactic conventions regarding fixity, parentheses, application operation associativity and precedence, etc. For example, `lam (lam (vs vz))` represents the K combinator. We can write this expression without parentheses, using `@@` -- the right-associative OCaml application operator of low precedence -- as `lam @@ lam @@ vs vz`. The second Church numeral looks as `lam @@ lam @@ vs vz / (vs vz / vz)` (in OCaml, slash is the infix operator, of a higher precedence compared to `@@`).

To specify the meaning of the `vz`, `lam`, etc. operations, is to implement the `Lambda` signature. An implementation, such as `NativeEval` below, tells what `repr` is, concretely -- and how exactly `vz`, `lam` etc. operations construct the `repr` values that represent the free-variable, the abstraction, etc. terms. In other words, an implementation of `Lambda` tells how to compute the meaning, or, the `repr` value, of each term from the `repr` values of its immediate subterms. An implementation of `Lambda` thus specifies a denotational semantics of the calculus.

Specifically, `NativeEval` maps closed lambda-terms either to OCaml integers or OCaml functions. The calculus is untyped; the semantics domain is therefore the disjoint union `v` below. We also have to account for open terms, and hence introduce the environment: a list of `v` values that are assumed as meanings for free variables. The list is ordered by the De Bruijn index. Thus the term meaning `repr` is a partial function from the environment to `v` (if the environment does not tell the meaning of all free variables in a term, we cannot make any sense of the term):

```    module NativeEval = struct
[@@@warning "-8"]                  (* annotation: partial pattern-match is intentional, don't warn *)
type v =                           (* the value domain *)
| I of int
| A of (v->v)                       (* generally, a partial function *)
type repr = v list -> v               (* also a partial function *)

let vz    = fun (h::_) -> h
let vs e  = fun (_::t) -> e t
let lam e = fun env -> A (fun x -> e (x::env))
let (/) e1 e2 = fun env ->
match e1 env with A f -> f (e2 env)

let int x = fun _ -> I x
let inc e = fun env -> match e env with I x -> I (x+1) (* partial *)
let ifz (e1,e2,e3) = fun env -> match e1 env with      (* partial *)
| I 0            -> (e2 / (int 0)) env
| I n when n > 0 -> (e3 / (int (n-1))) env
end
```
It should now be clear what `ifz(n,v1,v2)` means exactly: `n` is supposed to be an integer; `v1` and `v2` are functions. If `n` means 0, `ifz(n,v1,v2)` amounts to the application of `v1` to 0; otherwise, `ifz(n,v1,v2)` means the same as the application of `v2` to the predecessor of `n`. In other words, `ifz` is the pattern-matcher (deconstructor) on integers.

`NativeEval` is but one implementation of `Lambda`. Another implementation, called `Show`, maps each term to a string, the pretty-printed representation of the term. The reader may want to write this implementation on their own (and then compare to the one in the accompanying code).

Initial Algebra semantics: the syntactic semantics

A lambda-term, say, `lam vz`, in the `NativeEval` interpretation means the identity function on `NativeEval.v`. According to the `Show` implementation, however, the same term means the string `"Lx1. x1"`. One may ask: what does the term `lam vz` mean by itself? A glib answer is that a term embedded in the tagless-final style means whatever its interpretation makes it to mean. Technically, an embedded term may be regarded as a function that takes an interpretation of its syntactic forms (i.e., an implementation of its signature) and returns the `repr` value produced by that implementation. To say it in OCaml:
```    type lambda = {e: 'a. (module Lambda with type repr = 'a) -> 'a}
```
Different implementations of `Lambda` generally choose different concrete types for `repr` -- therefore the type `lambda` stands for a polymorphic function: there is a implicit `forall` before `'a.`, quantifying that type variable. Moreover, `lambda` is the first-class polymorphic function: we do want to pass terms as arguments to other functions. In OCaml, first-class polymorphic values have to be embedded in a record (in our case, the record with the field `e`). Since we chose modules for tagless-final signatures and implementations, `lambda`'s argument is a value of the module type: OCaml has first-class modules. We could just as well have used OCaml records or objects -- and we will use something like that in the follow-up article. The modules are more convenient and we use them for now.

Although `lambda` is the glib technical answer to the question about the inherent meaning of embedded terms, it could be taken seriously. In fact, we may define a denotational semantics in which our lambda-calculus terms indeed mean `lambda`. It is the most banal -- one may say, `syntactic' -- implementation of `Lambda`. We show only the representative part; the reader may want to finish as an exercise.

```    module LambdaSelf : (Lambda with type repr = lambda) = struct
type repr = lambda
let vz = {e = fun (type a) (module L : Lambda with type repr = a) ->
L.vz}
let vs e = {e = fun (type a) ((module L : Lambda with type repr = a) as l)->
L.vs (e.e l)}
let lam e = {e = fun (type a) ((module L : Lambda with type repr = a) as l)->
L.lam (e.e l)}
...
end
```
One can now say what `lam vz` means `by itself': it tells how to interpret itself, using whatever interpreter the user may provide. That is, `lam vz` takes an interpreter as an argument and directs it to find the meanings of `vz` and use the interpretation of `lam` to build the complete denotation. The `intrinsic' meaning of an embedded term is, hence, the guiding of its interpretation according to its structure. This is what syntax means, doesn't it? (The reason the above implementation is called `LambdaSelf` will become clear in the follow-up article).

One may say above more `mathematically': we have already mentioned that `Lambda` is an algebraic signature. Its implementations -- `NativeEval`, `Show`, `LambdaSelf` and many more below -- are hence `Lambda`-algebras. Each algebra has its own set of `repr` values (the carrier set), which supports `vz`, `vs`, etc. operations. Of all `Lambda`-algebras, `LambdaSelf` is special: it is so-called `word' algebra, which is an initial algebra. For any `Lambda`-algebra `L`, there is a unique total function `Lambda.repr -> L.repr` that `respects' the operations: the unique homomorphism. In fact, any implementation of a `Lambda`-signature is exactly the definition of that homomorphism. For example, passing the `NativeEval` interpreter, as the first-class--module argument, to a `LambdaSelf` term obtains the `NativeEval`'s interpretation of the term, as we shall see momentarily.

Banal as it may be, `LambdaSelf` is insightful, and also practically useful. First of all, it lets us easily write terms and have them interpreted. Here a few sample terms:

```    open LambdaSelf
let ci = lam vz
let ck = lam @@ lam @@ vs vz                  (* the K combinator *)
let c2 = lam @@ lam @@ vs vz / (vs vz / vz)   (* second Church numeral *)

let et3 = lam @@ inc(inc(vz / int 1))        (* higher-order, numeric *)
let et3a = et3 / (lam @@ inc(inc(inc vz)))

let delta  : lambda = lam @@ vz / vz
let lomega : lambda = lam @@ delta / delta
```
They all have the type `lambda`, which is inferred in all cases (although we often prefer to write the type explicitly as an annotation, to make sure we define a proper embedded term). We use OCaml definitions to give names to embedded terms; moreover, we can use the names to incorporate already defined terms into new ones (see `et3a` and `lomega`).

A bit more complex is the the applicative fixpoint combinator,

```    let fixa : lambda =
lam (vz /
(lam @@ delta / (lam @@ vs (vs vz) / (lam (delta / vs vz / vz))) / vz))
```
using which we define the recursive function to add two numbers, by induction on the second summand:
```    let add : lambda =
lam @@ fixa / (lam @@ lam @@
let y = vz and self = vs vz and x = vs (vs vz) in
ifz(y, lam @@ vs x, lam @@ inc(vs self / vz)))
```
We take another advantage of OCaml let-bindings, to give meaningful names to De Bruijn indices.

The `lambda` terms are also straightforward to evaluate, as we have said earlier:

```    let eval : lambda -> NativeEval.v = fun {e} -> e (module NativeEval) []
```
The evaluator takes a (closed) `lambda` term, passes it the `NativeEval` implementation as the first-class module, and applies the resulting `repr` value to the empty environment. Thus we may try
```    eval Sample.et3a
(* NativeEval.I 6 : NativeEval.v *)

eval LambdaSelf.(add / int 1 / int 4)
(* NativeEval.I 5 : NativeEval.v *)
```
(The evaluation result is shown in the comments). Likewise, we define `show : lambda -> string`, so that `show c2` gives `"Lx1. Lx2. x1 (x1 x2)"`. When printing terms, we use concrete variable names for readability.
References
Algebras Lecture notes on Universal Algebra, with the detailed explanation of initial algebras

Tagless-final with objects
A simpler example of the tagless-final DSL embedding, using objects (which are extensible records)

Normalizer by evaluation

We now turn to normalizers, which transform a closed `Lambda` term into the corresponding weak normal form -- or diverge if it does not exist. The weak normal form -- also called value -- is a closed term of the particular shape: either `int x` for some integer `x` or `lam e` for some `e`. The normalizers differ from the earlier `eval : lambda -> NativeEval.v` and `show : lambda -> string` in that they map a lambda-term to another lambda-term. Thus the two normalizers to be described below both have the type `lambda -> lambda`. The identity function also has this type; the normalizers, however, always return a lambda-term that is a value.

Our first normalizer is `denotational' and hence easily coded in the tagless-final style. In fact, we have already written most of its code: `NativeEval`, which maps a `lambda` term to its `NativeEval.v` meaning. If only we could turn this meaning to a value lambda-term... Let's try:

```    let rec dyn : NativeEval.v -> lambda = function
| NativeEval.I x -> LambdaSelf.int x
| NativeEval.A f -> LambdaSelf.lam (dyn (f ???))
```
Since `f` above is a `v -> v` function, we have to apply it to something, in such a way that the result is easily convertible to `lambda` representing the body of the abstraction. The easy solution is to extend the `NativeEval.v` data type with another variant, for the term being reconstructed:
```    type v =
| I of int
| A of (v->v)
| T of lambda
```
Then
```    let rec dyn : v -> lambda = function
| I x -> LambdaSelf.int x
| T e -> e
| A f -> LambdaSelf.lam (dyn (f (T LambdaSelf.vz)))
```
hoping that the function `f`, upon receiving `T LambdaSelf.vz`, will produce `T e` where `e` is the term that corresponds to the abstraction's body. For example, `lam vz` naturally means the (tagged) OCaml identity function: `A (fun x -> x)`; applying `dyn` gives us `LambdaSelf.lam LambdaSelf.vz : lambda` as desired. We now have to adjust `NativeEval` to produce the hoped-for denotations.

There is a slight problem however: we naturally wish `int 1` to be interpreted as `I 1` -- but not when it appears under `lam`, as in `lam (int 1)`. In the latter case, it ought to be interpreted as `LambdaSelf.int 1`. Luckily, we already have the solution to this context-sensitivity problem. To account for open terms, the meaning `repr` in `NativeEval` is a function from the environment to `v`. The environment is a list of `v` values to use when substituting for free variables. Normally, these values are tagged either with `I` or `A`. However, the `dyn` function above will also pass `T LambdaSelf.vz` to request the result as a `T`-tagged `lambda` term (the `read-out'). We can, hence, easily tell if the current context is under lambda: the environment contains at least one `T`-tagged value at the top. (A little exercise: can we say that the environment is either a list of `I` and `A` values, or entirely `T`-tagged values?)

```    module NBE = struct
[@@@warning "-8"]                  (* partial pattern-match is intentional *)
type v =                           (* the value domain *)
| I of int
| A of (v->v)
| T of lambda
type repr = v list -> v

let rec dyn : v -> lambda = function
| I x -> LambdaSelf.int x
| T e -> e
| A f -> LambdaSelf.(lam (dyn (f (T vz))))

let vz   = fun (h::_) -> h            (* Substitution under lam is OK *)
let vs e = fun (_::t) ->
match e t with
| T e -> T LambdaSelf.(vs e)
| e   -> e
let lam e = function
| T _::_ as env ->                   (* readout in progress *)
T LambdaSelf.(lam (dyn (e (T vz::env))))
| env -> A (fun x -> e (x::env))
let (/) e1 e2 = function
| T _::_ as env -> T LambdaSelf.(dyn (e1 env) / dyn (e2 env))
| env           -> match e1 env with A f  -> f (e2 env)

let int x = function
| T _::_  -> T (LambdaSelf.int x)    (* readout in progress *)
| _       -> I x
let inc e = function
| T _::_  as env -> T LambdaSelf.(inc (dyn @@ e env))
| env -> match e env with
| I x -> I (x+1)
| T e -> T LambdaSelf.(inc e)
let ifz = (* exercise *)
end
```
Most denotations have two cases: one for read-out (for building terms) and the other as in `NativeEval`. Only `vz` has the single interpretation: the substitution is performed uniformly in any context.

The denotational normalizer is thus:

```    let neval   : lambda -> (NBE.v list -> NBE.v) = fun {e} -> e (module NBE)
let nbe     : lambda -> lambda = fun e -> NBE.dyn @@ neval e []
let nbeshow : lambda -> string = fun e -> show @@ nbe e
```
(incidentally, `neval` is that unique homomorphism from `LambdaSelf` to `NBE` -- do you see that?)

For example, `nbeshow lomega` produces the same string as `show lomega`: lambda-abstractions always evaluate to themselves, even if there are redices inside. Not surprisingly, `nbeshow (add / int 1 / int 4)` yields `"5"`, which is the pretty-printed representation of `int 5`. Now, however, we can also `nbeshow (add / int 1)`. For sure, we could `eval (add / int 1)` with `NativeEval`. The result, however, is a (`A`-tagged) OCaml function, which is opaque. The new `nbeshow` lets us see the resulting lambda-term:

```    "Lx1. ifz x1 (Lx2. 1) (Lx2. S ((Lx3. (Lx4. x4 x4) (Lx4. (Lx5. Lx6. ifz x6 (Lx7. 1) (Lx7. S (x5 x7))) (Lx5. (Lx6. x6 x6) x4 x5)) x3) x2))"
```
Still, the result of `nbe (add / int 1)` agrees with that of the `NativeEval`, the definitional interpreter. To quickly check:
```    let e = LambdaSelf.(add / int 1) in
let A f1 = eval e in
let A f2 = eval (nbe e) in
List.for_all (fun n -> f1 (NativeEval.I n) = f2 (NativeEval.I n))
[0;1;2;3;4;100]
```
produces `true`: `f1` and `f2` agree, at least on the given sample inputs.

One may easily observe from the `NBE` code that, when restricted to `v` values without `T`-tags, it behaves just like `NativeEval`. In particular, for any closed term `e`, `neval e []`, if terminates, is either `I x` for some integer `x` or `A f` for some `v->v` function. One may further observe, with a slightly bit more effort, that if `v` is the result of `neval e []` for some closed term `e`, then `neval (dyn v) []` is `v`, extensionally. (The extra effort is generalizing this statement to open terms). That is, `dyn` is the left-inverse for the `NBE` interpretation. The function like `dyn` is typically called `reify' in the normalization-by-evaluation literature. Putting these observations together we obtain that for any closed term `e`, `nbe e` is a value term and

```    eval e === eval (nbe e)
```
where `===` means that either two sides both diverge, or they are the same integer or the same, as a mapping, OCaml function (that is, `===` is the extensional equality). That means `nbe` is meaning-preserving and it does yield a value: it is the correct normalizer.

Incidentally, normalization-by-evaluation is a technique for normalizing terms, or partially evaluating them. A partial evaluator can perform reductions even under lambda. Although this often improves efficiency when the lambda-term is subsequently applied, in this article we keep close to the operational semantics and avoid any extra reductions. (It is also worth contemplating what may happen when partially evaluating a term like `lomega`.)

Operational semantics: structural and big-step

Finally we come to the reducer and the operational semantics. The familiar Plotkin's structural operational semantics (SOS) is defined by the following familiar reduction rules, adjusted to our notation:
```    -------  (where v is a value: either lam e or int x)
v --> v

------------------------  (beta)
(lam e) / v --> e{vz:=v}

-------------------------  (inc)
inc (int x) --> int (x+1)

--------------------------------  (if0) (v1,v2 are values)
ifz(int 0,v1,v2) --> v1 / int 0

-------------------------------------  (ifn) (n>0)
ifz(int n,v1,v2) --> v2 / (int (n-1))

e1 --> e1'
-------------------- (e1 is not a value)
e1 / e2 --> e1' / e2

e2 --> e2'
------------------ (e2 is not a value)
v / e2 --> v / e2'

e1 --> e1'
-------------------------  (e1 is not a value)
inc e1 --> inc e1'

e --> e'
------------------------------  (e is not a value)
ifz(e,e1,e2) --> ifz(e',e1,e2)

(the two more similar ifz compatibility rules are skipped)
```
where `e{vz:=v}` stands for the substitution of the value `v` for the free variable `vz` in `e`, adjusting the other De Bruijn indices. The rules are all disjoint; the last six (including the two skipped ones) are the compatibility rules, implicitly defining the evaluation contexts. The reducer `sos` below applies the rules until it either obtains a value, or no rule is applicable: it got stuck. That is, `sos` computes the transitive closure of `-->`.

The operational semantics treats `inc e` and `ifz(e,e1,e2)` terms essentially like applications: in either case, if the arguments are not values, compatibility rules are applied. If the arguments are values, the reduction looks at what sort of value it is, and does something meaningful (performs substitution or the increment). Our reducer below indeed treats the terms with `inc` and `ifz` as applications.

Incidentally, the operational semantics may also be specified in the big-step, `natural' style, as the `==>` relation of a term and the corresponding value:

```    -------
v ==> v

e1 ==> lam e1'   e2 ==> v2   e1'{vz:=v2} ==> v
-----------------------------------------------
e1 / e2 ==> v
```
(the rules for `inc` and `ifz` are left as an exercise).

Pattern-matching in tagless-final style

Whatever style of the operational semantics we choose, we have to analyze the shape of a term -- is it an application, is it a lambda-term, and if so, what is its body, etc. -- and substitute for a free variable in a term. It might be surprising to some that this classification task can be formulated as a denotational semantics. The semantic domain is a pair, of the term itself (so that we may return it, should it turns out a value) and its kind; see `repr` below. The kind tells if the term is an application (and if so, its applicands) or a value. In the latter case, is it an integer value or a functional value, that is, something that takes an argument and either substitutes it or does something fancier. Since `repr` denotations are built bottom-up, one has to account for another possibility: if a term is open. The classification of an open term depends on what its free variables mean. An open term is a term with free variables to substitute. We also keep track of the depth of an open term, the largest De Bruijn index of its free variables (which is the length of the needed environment).
```    module Classifier = struct
[@@@warning "-8"]                  (* partial pattern-match is intentional *)
type repr = {term: lambda;         (* term as it is *)
kind: kind}           (* and its kind *)
and kind =
| App of repr * repr             (* subject to reductions *)
(* Expressions of the kind Int and Applicable are values *)
| Int of int
| Applicable of (repr -> repr)      (* can be applied to an argument,
which must be a value
*)
(* The three kinds above are closed. The remaining kind is
for open expressions. The first argument is the depth:
the number of lambdas needed to close the expression
*)
| Open of int * (repr list -> repr)

let vz  = {term = LambdaSelf.vz;
kind = Open (1,fun (h::_) -> h)}

let rec vs e = match e.kind with
| Open (n,e') ->
{term = LambdaSelf.vs e.term;
kind = Open (n+1,fun (_::t) -> vs (e' t))}
(* vs may end up being applied to a closed value after the substitution.
In that case, it does nothing.
*)
| _   -> e

let rec lam e =
{term = LambdaSelf.lam e.term;
kind = match e.kind with
| Open (1,t) -> Applicable (fun x -> t [x])
| Open (n,t) when n > 1 ->
Open (n-1,fun env -> lam (t (vz::env)))
| _ -> Applicable (fun _ -> e)     (* constant function *)
}

let rec (/) e1 e2 = (* exercise *)

let int x = {term = LambdaSelf.int x;
kind = Int x}

(* introducing delta-redices *)
let delta_inc =
{term = LambdaSelf.(lam @@ inc vz);
kind = Applicable (function {kind = Int n} -> int (n+1))}
let rec inc e =
{term = LambdaSelf.(inc e.term);
kind = match e.kind with
| Open(n,t) -> Open(n,fun env -> inc (t env))
| _         -> App (delta_inc,e)
}

let ifz = (* exercise *)
end
```
One may notice that as we build `repr` bottom-up, we also build the function to substitute for the term's free variables. The substitution function is a bit smart: it avoids rebuilding or even looking into subterms that are known to be closed and hence have nothing to substitute for.

It is worth pointing out how `kind` differs from the familiar abstract syntax tree for the lambda-calculus. First, we do not distinguish `inc` and `ifz`: either is treated as applications. However, we do distinguish open terms.

Structural operational semantics reducer

Once the classification is done, reduction is just following the rules. Below is the reducer for the SOS semantics. It applies the SOS rules until it either obtains a value, or no rule is applicable (that is, it got stuck). As we explained earlier, `inc e` and `ifz(e,e1,e2)` terms are treated as applications.
```    let sos : lambda -> lambda = fun {e} ->
let open Classifier in
let rec step : repr -> repr =         (* the --> reduction of SOS *)
fun e -> match e.kind with
| Applicable _ | Int _ -> e               (* value *)
| Open _ -> assert false                  (* cannot happen *)
| App (e1,e2) -> match (e1.kind,e2.kind) with
| (Applicable f,Int _) | (Applicable f,Applicable _) ->
f e2                                (* redex *)
| (App _,_) -> step e1 / e2             (* compatibility rules *)
| (_,App _) -> e1 / step e2
| _         -> failwith "stuck"
in
let rec loop : repr -> repr =         (* transitive closure of step *)
fun e -> match e.kind with
| Applicable _ | Int _ -> e               (* value *)
| _ -> loop (step e)                      (* keep stepping *)
in (loop (e (module Classifier))).term

let sosshow : lambda -> string = fun e -> show @@ sos e
```
The `sos` reducer can be used just like the earlier `nbe` normalizer. They do produce identical results (see the accompanying code for that test, among many others).

The naively implemented SOS reducer is inefficient: too many pattern-matches on the shape of the term. (Do you see that?) A simple modification turns it into the efficient, natural, big-step reducer -- which we suggest as an exercise. The accompanying code also makes the big-step reducer count the number of reductions.

Conclusions

We thus demonstrated (among others) two normalizers for the call-by-value lambda-calculus with constants. One follows the denotational approach and the other operational, reducing a term to a value by successively re-writing it according to the reduction rules. We can do operational semantics in the tagless-final style, after all. Curiously, even the operational approaches rely on denotational semantics.

The normalizers are written in the host language, OCaml. Next we lower normalizers to (into) the embedded language itself, showing off our calculus serving as a metalanguage to embed itself and evaluate the self-embedded expressions.