In this section we continue to work our way towards a viable notion of valuation for CLS-expressions.
A mutable may be converted, by substitution, into a different mutable; or into an immutable (possibly with subscriptum). But immutables can never be turned back into mutables. When a mutable is replaced by a subscripted immutable it may well be that some of the indices are mutable, in other words, susceptible of further change. Only when a subscriptum is completely free of mutables, at any depth, is it absolutely fixed and incapable of further change. We will refer to such mutable-free terms as 'ground terms'. We may think of mutables as being 'up in the air', immutables with mutable indices as being 'somewhat up in the air', and immutables with no mutability in them as having been brought right down to earth or grounded.
A ground atom is an atom whose subscriptum is composed only of ground terms. Ground atoms cannot be changed by any substitution. They are as it were impervious to substitution; the same applies to expressions, all of whose atoms are ground atoms.
We will find that ground atoms play a rôle in the CLS-calculus somewhat similar to that played by letters in the CL-calculus. In particular, in the context of the CLS-calculus, a valuation string is defined to be an expression each of whose factors is either a ground atom or a circled ground atom; and in which no ground atom appears more than once.
But when is a valuation string 'complete' (for a given expression)? Presumably, when it contains all the ground atoms, not just that the expression contains, but that it is capable of containing, when subjected to substitutions. As we shall see in a moment, this makes 'CLS' (Circle, Letter and Subscript) a lot more difficult to deal with than 'CL' (Circle and Letter); because in many cases, the set of 'possible ground atoms' is not merely rather large, but actually infinite.
This is the recipe: go through the expression, inspecting all the terms that appear as subscripts. Make an inventory of all the immutables that occur in the terms, with their 'arities'. (Recall that the 'arity' of an immutable, or of an upper-case head-letter of an atom, is the number of indices that it takes in its subscript.) If all the immutables have arity zero, then life is simple: the Herbrand Universe is simply the set of immutables occurring in the expression. Otherwise, we can only say that the zeroth level of the Herbrand Universe is the set of arity-zero immutables. If this set is empty, we take the line that the zeroth level contains a single element called e. It is, as it were, just an unfortunate accident that our expression doesn't actually contain any occurrence of e! (The reason for this move is that without it, we don't actually get any ground terms at all. Its justification is another matter - a question that we will leave to one side for the time being.)
So much for the zeroth level. The first level is the set of terms which are immutables of non-zero arity, supplied with indices belonging to the zeroth level; in general, the nth level consists of immutables, with at least one index belonging to the (n-1)th level of the Herbrand Universe, the rest belonging to any of the levels lower than the nth.
There only needs to be one immutable with arity 1 for the Herbrand Universe to be infinite, with an infinite number of levels. For example,
H = { ae, aae, aaae, ... }
Even in more complicated examples, however, thanks to the fact that any conceivable ground term may be assigned to a level, the set of ground terms is countably infinite i.e. capable of being brought into one-to-one correspondence with the natural numbers 1, 2, 3, 4, ... For the number of ground terms belonging to any one level is clearly finite, and can be counted off in some sort of 'alphabetical order'; which implies that the whole lot can be counted off by starting off with the zeroth order and working up the levels.
We can therefore think of the Herbrand Universe as consisting of a set
{g1, g2, g3, g4, g5, ...}
where each element gi is a ground term.
A ground atom consists of an upper-case 'head', P, say, with a set of indices, each one belonging to the Herbrand Uinverse. Again, the ground atoms may be sorted out into levels, the (-1)th level consisting of 'heads' of zero arity (no subscript); the 0th level consisting of heads with indices that are all ground terms of level 0; the nth level consisting of heads with with at least one index from level n of the Herbrand Universe, but no index from a level higher than n. Again, the set of ground atoms generated by the heads and the immutables occurring in the expression is countable, and we may write it
{ G1, G2, G3, G4, G5, ... }.
A substitution θ is a 'ground substitution' for an expression E iff Eθ contains no atoms that are not ground atoms. In other words, all mutables have been eliminated: θ replaces every mutable by a ground term. The expression Eθ is then a 'ground instance' of E. Among the ground atoms occuring in a ground instance there is one that has the highest number (when the Herbrand atom-set is counted out). The 'level' of the ground instance is this number (i.e. the ordinal number of its highest ground atom). Yet again, the set of ground instances of E is infinite but countable. (Remember that E itself is a finite expression.)
A partial valuation string of length n (for a CLS-expression) is a valuation string in which each member of the subset (of the set of ground atoms)
{ G1, G2, ... Gn }
occurs just once. Clearly, there are 2n partial valuation strings of length n (as each Gi may appear circled or not).
The partial valuation strings may be thought of as the nodes of a tree (in fact, a rooted binary tree).
A 'tree', in Graph Theory, is defined to be a set of nodes, together with a set of connectors, each one running between two nodes, such that between any two nodes there is exactly one path; where a path is defined as a sequence of nodes such that any two successive members af the sequence are connected (by a connector). In a 'rooted tree' each node except a special 'root node' a) has a unique parent node, connected to its child by a connector, and closer than its child to the root node; and b) has the root node as an ancestor (i.e. parent of a parent of a parent ... as many times as is necessary).
A partial valuation string is an expression
H1 H2 ... Hn
such that each Hi is either Gi or (Gi). Suppose we say that its parent is just
H1 H2 ... Hn-1
and that _ is the root node; then it is clear that the set of partial valuation strings has the structure of a rooted tree. The tree is binary because each node has just two children (i.e. nodes of which it is a parent). They are obtained by adding on either Gn+1 or (Gn+1) to the parent string.
In the CLS-calculus, a complete valuation string is an expression of the form
H1 H2 H3 ...
which does not come to an end. In tree terms, this is an infinite branch of the tree, extending to all levels. Every ground atom is represented in it, either circled or not; it is therefore capable of drawing out (by 'uncopy') all the ground atoms from any ground instance of the generative expression E, and thus reducing it to a C-expression, thus ultimately to _ or O.
Let us say that a partial valuation string V of length n is 'marked' by its generative expression E if there exists a ground instance Eθ, of level n or lower, such that
V Eθ = H1 H2 ... Hn Eθ = O .
(Because its level is no higher than n, Eθ can contain no ground atom that does not appear in V, therefore V has the power in any case to reduce Eθ to _ or O .)