Consider two terms of the SKI-combinator calculus $\alpha$ and $\beta$ such that the following derivations are valid.
- $\alpha \rightarrow \alpha_1$
- $\beta \rightarrow \beta_1$
Then we have two valid derivations for the term $(\alpha \beta)$. We can proceed on the left, or the right.
- $(\alpha \beta) \rightarrow (\alpha_1 \beta)$
- $(\alpha \beta) \rightarrow (\alpha \beta_1)$
How do we get around this "non-determinism" when modeling computation using SKI-combinators? If we don't choose carefully, we can even end up in an infinite sequence of derivations, even if there is a sequence of derivations that terminates. This is the case for recursive combinators. For example, consider $\gamma$ such that $\gamma x y\rightarrow (x y)(\gamma x y)$. You can see that $\gamma K I \rightarrow K I (\gamma I K) \rightarrow I$, but we could also just keep expanding the $\gamma$ term for as long as we like.
A normal form is a term in which no further derivations can occur. It is known that in SKI combinator calculus, if a term reduces to a normal form, that form is unique. This is known as the Church-Rosser theorem. This resolves any possible ambiguity in specifying computations.