0

Consider two terms of the SKI-combinator calculus $\alpha$ and $\beta$ such that the following derivations are valid.

  1. $\alpha \rightarrow \alpha_1$
  2. $\beta \rightarrow \beta_1$

Then we have two valid derivations for the term $(\alpha \beta)$. We can proceed on the left, or the right.

  1. $(\alpha \beta) \rightarrow (\alpha_1 \beta)$
  2. $(\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.

Mark
  • 5,696

1 Answers1

1

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.

MJD
  • 65,394
  • 39
  • 298
  • 580
Mark
  • 5,696
  • 1
    It also may be useful to know that if there is a normal form, it can always be reached via “normal-order evaluation”, which simply means the process of always reducing the leftmost reducible term. Other reduction orders may reach a normal form more quickly, but may also diverge. Normal-order evaluation may be slow, but if there is a normal form, normal-order evaluation will find it. Your $\gamma KI$ term is an example of this. – MJD Jun 01 '21 at 22:44