Register

# 3.6. Beta-Reduction¶

## 3.6.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. A critical part of analyzing how any language evaluates function calls is to examine its semantics from the perspective of $\beta$ reduction.

## 3.6.2. Identifying Beta-redexes (1)¶

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.6.3. Identifying Beta-redexes (2)¶

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.

## 3.6.4. Performing Beta Reductions¶

This randomized problem will make you practice performing $\beta$-reductions. To earn credit for it, you will have to solve it correctly three times in a row.