[Note added 9-june-2005: This analysis is not as sharp as it could be,
because it isn't possible to represent arbitrary binary data as a
program string without expanding it.  It seems to be necessary to add
primitives to the combinatory system for reading arbitrary binary data
off the end of a program string.  Then there wouldn't seem to be any
effective procedure for telling where a program string ends, although
the prefix property would be preserved.]

Define a language of terms by the following:

1. X, K, and S are terms.
2. If t1 and t2 are terms, then (t1 t2) is a term.
3. All terms are generated by finitely many applications of (1) and

Define the small-step evaluation relation on terms by the following:

1. (X t) steps to (((t K) S) K).
2. ((K t1) t2) steps to t1.
3. (((S t1) t2) t3) steps to ((t1 t3) (t2 t3)).
4. If t1 steps to t2, then (t1 t3) steps to (t2 t3).
5. All small steps are generated by finitely many applications of (1),
(2), (3), and (4).

It is clear that if a term t steps to any term, it steps to a unique
one. It is computable whether a term t steps to any term as well as,
if so, the unique term to which it steps.

We say a term t halts if there is an integer n such that every (= any)
sequence of small steps starting from t consists of fewer than n

Define the valid program strings (each of which is a bitstring) and
their interpretations by the following:

1. "0" is a program string interpreted by X.
2. If s1 and s2 are program strings interpreted by t1 and t2,
respectively, then the concatenation of "1", s1, and s2 is interpreted
by (t1 t2).
3. All program strings are generated by finitely many applications of
(1) and (2).

It is clear that each valid program string has a unique
interpretation, and that no valid program string is a prefix of any
other valid program string. We can also associate a unique (infinite)
binary tree with the valid program strings, such that each leaf of the
tree corresponds to a valid program string by its path from the root
of the tree.

Consider the formal sum of

        2^-|s_i|        if the interpretation of s_i halts, or
        0               else

over the sequence {s_i} of valid program strings, arranged in some
standard order, |s| being the length in bits of a string s. By the
prefix property, this formal sum converges absolutely to a real number
omega, and thus the sum is independent of the arrangement of the valid
program strings.

A sequence of approximations {alpha_i} is defined by taking alpha_n as
the sum of

        2^-|s|          if every sequence of steps from the
                        interpretation of s consists of fewer than n
                        steps, or
        0               else

over all valid program strings s of length less than n. Then each
alpha_n is a (dyadic) rational number, computable given n. The
{alpha_i} are monotone increasing, and omega is the least upper bound
of the {alpha_i}.

The challenge is to construct the best possible bounds on omega. Since
X halts immediately, omega is at least 1/2. Since


(associating to the left) does not halt, and its program string is 83
bits long, omega is at most 1-2^-83.

The constant omega can also be interpreted as the probability that a
randomly selected valid program string is interpreted by a halting
term. Here the probability of choosing any given valid program string
s is 2^-|s|. Another way to phrase the experiment is to say that,
starting from the root of the infinite binary tree described above, a
path down the tree is constructed by repeated fair Bernoulli trials
choosing which child of a node in the path will be the next node in
the path, until a leaf is reached. It is easy to show that a leaf will
eventually be reached with probability 1, by considering the random
walk of the parameter "excess of 1s over 0s" in the partial program
strings generated as the experiment proceeds. By the syntax of valid
program strings, the experiment terminates at the first moment this
parameter becomes negative.