Smallest non-halting unlambda program

Is ```siisii the smallest Unlambda program that doesn't halt?

In other words, what is the smallest non-terminating combinator term in SKI augmented with $C$ (call/cc) and $D$ (delay)? Is it $SII(SII)$?

Intuitively speaking, a non-terminating program needs either:

• a combinator such as $Y$ which, when applied, reduces to a larger expression containing itself;

• or two combinators such as $S$ which, when applied, replicate at least one of their arguments: one to do the initial replication and one to be replicated.

Unlambda lacks a combinator of the first type, but has two combinators of the second type: $S$ and $C$.

In the SKI-calculus, following the intuition above, a non-terminating term needs to somehow apply $S$ with the first argument being $S$. So it would have to be of the form $Swx(Syz)$, i.e. ```swxsyz in Unlambda). This suggests that $SII(SII)$ is minimal. (Note that I've only given an intuition, I haven't proved it!)

However Unlambda also includes c (call/cc), and this is a very powerful operator in terms of replicating its argument. A term of the form $Cfx$ applies its own continuation $\phi$ to the function $f$; if $f \phi$ itself arranges not to destroy its context, then the term won't terminate. For example, $CI(CI)$ is non-terminating (exercise: work it out). ``cici is known as the Yin-Yang puzzle. To see it in action, make it print a trace of its execution: `.@ci.*ci.

Because $S$ requires 3 arguments and $C$ requires 2, intuitively, there can't be a non-terminating 3-combinator term, so the 4-combinator term we found above is minimal.

Here's a quick-and-dirty bash script that enumerates all possible Unlambda terms of up to 4 combinators (i.e. 3 application nodes) and prints out the ones that take more than 1 second to terminate. I omitted the I/O primitives which reduce like i, as well as e (exit) which obviously wouldn't help to make a program non-terminating. This is an experimental way to list the non-terminating terms — the terms not printed here are guaranteed to be terminating (assuming a correct implementation), and the terms printed here are likely to be non-terminating.

for a in s k i c d v; do
  for b in s k i c d v; do
    for c in s k i c d v; do
      for d in s k i c d v; do
        for p in @$a$b @@$a$b$c @$a@$b$c @@@$a$b$c$d @@$a@$b$c$d @@$a$b@$c$d @$a@@$b$c$d @$a@$b@$c$d; do
          p=${p//\@/\`}
              timeout 1 unlambda <<<$p || echo $p
        done
      done
    done
  done
done

The result of the experiment is that only the following terms are potentially non-terminating:

scc?
c?c?
``

where each ? can be independently i, c or d`. In other words, the non-terminating combinator terms are $SCCx$ and $Cx(Cy)$ (or so the experiment suggests, but it happens to be correct).

Exercises:

• Work out the reductions for these terms and check that they are indeed non-terminating. Do they loop or do they grow forever?

• Prove that all smaller terms terminate. (I don't think there's anything more interesting than a long case enumeration.)

• How does $SCCI$ relate with my intuition above concerning the minimum content of a non-terminating term — the $S$ replicates only $I$?

• Prove or disprove that there is no smaller non-terminating SKI term than $SII(SII)$. Are there others of the same size?

StackExchange Computer Science Q#29100, answer score: 7