β-Reduction (beta.ml)

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.

Next