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 λ calculus interpreter. This rule is called β reduction. An expression to which the rule can be applied is called a β redex (short for β reduction expression). So, a β redex is formally defined as a λ 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 β reduction.
3.6.2. Identifying Beta-redexes (1)¶
This randomized problem will help you identify β-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 β-redexes and prepare to reduce them by determining whether an α-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 β-reductions. To earn credit for it, you will have to solve it correctly three times in a row.
