Let us begin with an example: if there is an expression like `let x = y in x + y`, it is obvious that `x` equals `y`, so we can replace the whole `let` expression with `y + y`. Such translation is called *β-reduction* of K-normal forms. (The term β-reduction originates in another system called λ-calculus, of which ours is a special case.) It is not always necessary in ordinary programs, but is sometimes effective after other optimizations.

In MinCaml, function `Beta.g` is the core of β-reduction. It takes expression `e` with a mapping `env` from variables to equal variables, and returns the β-reduced expression. Again, the important case is `let x = e1 in e2`, where we first β-reduce `e1` and, if the result is a variable `y`, add to `env` the mapping from `x` to `y` before β-reducing `e2`. And if we encounter variable `x`, we look up env and replace `x` with variable `y`. Since variables appear everywhere in K-normal forms, function find is defined and used for this replacement.