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¶

This 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 that we substitute \(E'\) for \(x\) in \(E\) using the substitution algorithm developed in the preceding section. For example, \(\beta\)-reducing \((\lambda x.(x \; v) \;\; (z \; (v \; u)))\) would yield the expression \(((z \;\; (v \;\; u)) \;\; v)\).

4. Some Beta-Reductions Require Alpha-Conversion¶

This 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¶

This 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. BeCareful: 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\).