In 1958 Curry proved that if the leftmost reduction of a λ-term $X_1$ is infinite, then all reductions starting at X1 can be continued for ever, i.e. $X_1$ has no normal form.
How to show that the leftmost reduction is infinite?
Do I understand correctly that if at some point of reduction of term $T$ we meet a term $T_j$ that was already occurred previously ($T_j = T_i, i<j$) then term $T$ does not have a normal form? Meaning that reduction made a loop.
$T \to ... \to T_i \to ... \to T_j$, $T_i=T_j$ (intentionally, for example: $SII(SII)=SII(SII)$) implies $T$ does not have normal form?
So we can use quasi-leftmost reduction to show this looping and prove infinite reduction?
Quasi-leftmost reduction vs leftmost reduction description.
