3
$\begingroup$

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?

$\endgroup$

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.