According to Chris Hankin in his book (Lambda Calculus a Guide for Computer Scientists). A reduction sequence $\sigma: M_0 \to^{\Delta_0} M_1 \to^{\Delta_1}M_2 \to^{\Delta_2}\ldots $ is a standard reduction if for any pair $(\Delta_i, \Delta_{i+1})$, $\Delta_{i+1}$ is not a residual of a redex to left of $\Delta_{i}$ relative to the given reduction from $M_{i}$ to $M_{i}$. The Standardization Theorem says that if a term $A$ $\beta$-reduces to $B$, then there is a standard path from $A$ to $B$. On the other hand, in the leftmost strategy, outermost redex is always reduced first. The Leftmost Reduction Theorem says that if a term $A$ $\beta$-reduces to $B$, and $B$ is in $\beta$-normal form, then the leftmost strategy reaches $B$. My question is:

1- I'm not seeing the difference between the reductions Standardization and Leftmost, for me, it seems to say the same thing.

2- Why the Leftmost Reduction Theorem is a particular case of the standardization Theorem?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.