1. Beta-Redexes¶

Now that we have rigorously defined substitution in the previous section, we can define a rule for evaluating a function application, which is the main operation for any \(\lambda\) calculus interpreter. This rule is called \(\beta\)-reduction. An expression to which the rule can be applied is called a \(\beta\)-redex (short for \(\beta\)-reduction expression). So, a \(\beta\)-redex is formally defined as a \(\lambda\) expression of a specific form, namely, an application in which the first term is a function abstraction.

For example, \((\lambda x.(x \; v) \;\; (z \; (v \; u)))\) is a \(\beta\)-redex because \(\lambda x.(x \; v)\) is a function abstraction. On the other hand, \(((\lambda x.(x \; v) \;\; y) \;\; (z \; (v \; u)))\) is not because its first term is a function application and not a function abstraction. However, the application that comprises the first term of this expression is a \(\beta\)-redex. This illustrates that it is possible for expressions that may not themselves be \(\beta\)-redexes to contain sub-expressions that are.

A critical part of analyzing how any language evaluates function calls is to examine its semantics from the perspective of \(\beta\)-reduction.

2. Identifying Beta-Redexes¶

The following randomized problem will help you identify \(\beta\)-redexes. To earn credit for it, you will have to solve it correctly three times in a row.

3. Beta-Reduction is a Substitution¶

If we have a \(\beta\)-redex of the form \((\lambda x.E \;\; E')\), then to \(\beta\)-reduce this expression means to substitute \(E'\) for \(x\) in \(E\) using the substitution algorithm developed in the preceding section.

In other words, to evaluate a \(\beta\)-redex of the form

simply means to perform the following substitution:

Again, this is just the algorithm that you learned in Substitution Algorithm. Note that the result of a \(\beta\)-reduction is what you get by first stripping off the binding occurrence of the \(\lambda\)-abstraction, leaving just its body, and then substituting \(E'\) for x in that body.

For example, to \(\beta\)-reduce \((\lambda x.(x \; v) \;\; (z \; (v \; u)))\), you would first strip off \(\lambda x.\) to get \((x \; v)\) (that is, the body of the \(\lambda\)-abstraction), and then substitute \((z \; (v \; u))\) for \(x\) in that body, yielding the expression \(((z \;\; (v \;\; u)) \;\; v)\).

4. Some Beta-Reductions Require Alpha-Conversion¶

The following randomized problem will help you identify \(\beta\)-redexes and prepare to reduce them by determining whether an \(\alpha\)-conversion is needed. To earn credit for it, you will have to solve it correctly three times in a row.

5. Performing Beta-Reductions¶

The following randomized problem will provide practice performing \(\beta\)-reductions. To earn credit for it, you will have to solve it correctly three times in a row. Be Careful: remember that, because \(\beta\)-reducing uses the substitution algorithm, it may be necessary to perform an \(\alpha\)-conversion. For example, \(\beta\)-reducing \((\lambda x. \lambda u.(u \;\; x) \;\; (v \;\; u))\) yields \(\lambda a.(a \;\; (v \;\; u))\), where we must do an \(\alpha\)-conversion to avoid capturing the free variable \(u\).