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.
