Leftmost β‑Reduction & Why It Matters
A clear, student‑friendly explanation with examples and an interactive quiz.
Standard (Leftmost) Reduction
(λx.(λy. x y) z)(λz. z)
→β (λy. (λz. z) y) z
→β (λz. z) z
→β z
Why this is standard:
- The first reduced redex is the outermost one:
(λx.(λy.xy)z)(λz.z).
- This λ is the leftmost λ in the entire term.
- Every later redex appears to the right of the previous one.
- No inner redex is reduced before its surrounding redex.
Non‑Standard (Inner‑First) Reduction
(λx.(λy. x y) z) (λz. z)
→β (λx. x z) (λz. z)
→β (λz. z) z
→β z
Why this is non‑standard:
- The first reduced redex is the inner one:
(λy.xy) z.
- This redex is to the right of the outer redex
(λx.(λy.xy)z)(λz.z).
- Reducing it first skips the leftmost redex, breaking the left‑to‑right rule.
Interactive Quiz
Score: 0 / 0