# 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.