In the CL-calculus, there is a 'brute force' way of telling whether two expressions F and G are equivalent. We substitute values (mark or void) for the letters. Of course, there are many ways of doing this. Suppose we call each way of assigning a value to every one of the n letters appearing in the expressions, a 'valuation' (so the number of such valuations is 2n). In the section Consequences of the Standard Form Lemma we established the following
If V is a valuation, let FV stand for the value attained by F when values are substituted for the letters of F according to the scheme laid down by V. If FV = GV for all possible valuations V, then F and G are CL-equivalent (meaning that one can get from one to the other using the allowed steps of the CL-calculus, namely wrap, delete, copy and their inverses).
As stated in 'Consequences' the theorem is a corollary of the following
If EV = _ for all possible valuations V of E, then E is void-equivalent (meaning that E can be reduced to the void using the allowed steps of the CL-calculus).
The Test Theorem follows from this because F and G are CL-equivalent if and only if their equivalence expression
(F(G))((F)G)
is void-equivalent. Another easy corollary (just apply theorem 2.2 to the circled expression (E)) is the following:
If EV = O for all possible valuations V of E then E is mark-equivalent.
We will give proofs of theorems 2.2 and 2.3 below.
Can we do the same sort of thing in the CLS-calculus? We must recognize at the outset that we will need to tread rather carefully. For if E is mark-equivalent (meaning now E≅O) we can no longer infer that (E) is void-equivalent. Also there is the question, what is the appropriate definition of a valuation of a CLS-expression? For the subscripts of the atoms (which are the equivalents, in CLS, of the letters in CL) are now liable to be changed by substitutions: how will a valuation keep pace with that?
We begin our approach to these daunting questions by introducing the notion of a 'valuation string', restricting ourselves, to start with, to the CL-calculus. We will then establish the first of our criteria for mark-equivalence in CLS.
A valuation string in CL is an expression each of whose factors is either a letter or a letter in a circle, and in which no letter is repeated. Note that the void counts as a valuation string (it's just that the number of letters is zero), but the mark does not. A valuation string is 'complete' (with respect to a given expression) if it contains every letter that occurs in the expression. Thus the valuation string
p (q) (r)
is not complete with respect to the expression
((p)(q(r)(t))),
but
p(q)(r)t
is.
Let V be a valuation string, complete with respect to an expression E, then the expression VE is equivalent either to V or to the mark O.
In the presence of V, each letter (for example, x) that appears in E can be uncopied, leaving behind either a blank (in case x is a factor of V) or a mark (in case it is (x) that is a factor of V). By doing this with all the letters, we reduce E to a C-expression (circle-expression), which is C-equivalent either to _ or to O. Thus either
VE = V_ = V
or
VE = VO = O ◊
Consider the set of all complete valuation strings involving n letters. It is clear that the set has N = 2n elements (since each letter may appear in a string either as itself, or circled); let those elements be denoted Vi, with i running from 1 to N. Now consider the expression Ωn formed as follows
Ωn ≡ ( (V1)(V2)...(VN) ).
Then
Ωn = _ ,
that is, Ωn is CL-equivalent to the void.
We make use of the lemma of the CL-calculus,
(A) = (Ax)(A(x))
where A is any expression and x is any letter. When the number of letters is zero, there is only one valuation string, _ , and
Ω0 ≡ ( ( ) ) = _
∴ (Ω0) = ( ).
Applying our lemma with the void substituted for A and the first letter, a say, substituted for x:
(Ω0) = ( ) = (a)((a)) ≡ (Ω1).
Applying the lemma to each of the two factors in turn, and using the second letter, b say, for x, we obtain:
(Ω1) = (a) ((a)) = (ab) (a(b)) ((a)b) ((a)(b)) ≡ (Ω2).
The step may be repeated as many times as necessary, until we obtain the expression (Ωn), which is necessarily equivalent to (Ω0) = O. Therefore
Ωn = Ω0 = _ ◊
a) Suppose that in the presence of any complete valuation string E is reduced to the void; in other words,
V E = V
for any V in the set of complete valuation strings (N in number). Then E = _ .
b) Suppose, on the contrary, that E is reduced by any valuation string to the mark. Then E = O.
Using Lemma 2.5,
E = E _ = E Ωn = E ( (V1)(V2)...(VN) )
= ( (E V1)(E V2)...(E VN) ) ;
the last step uses the CL-move we have called 'distribute' (see this page), extended from the usual 2 to N factors inside the outer circle. Now, in case (a) each occurrence of E is reduced to _ , so each E Vi is equivalent to just Vi, which converts the expression back into Ωn, implying E = _ . In case (b), each factor of the form (E Vi) is equivalent to (O), equivalent to the void; which means that the outer circle contains nothing, and is therefore a mark. Thus E = O ◊
Theorems 2.2 and 3.3 are comprehended in parts a) and b), respectively, of Theorem 2.6. Note that part b) does not really require to be proved separately, since if E is always reduced to O, then (E) is always reduced to _ .
We say that a CLS-expression, E, is 'mark-equivalent' if and only if
E ≅ O .
If A = B, and θ is any substitution, then
Aθ = Bθ.
A = B says that there is some sequence of CL-operations that converts A into B. This sequence may ultimately broken down into a sequence of (un)wraps, (un)deletes and (un)copies. But the very same sequence of operations cannot fail to convert Aθ into Bθ. This is because any substitution necessarily preserves the 'sameness' of atoms. That is, if two atoms are the same, and are therefore able to participate in a 'copy' or 'uncopy' operation, they will still be the same, and just as able to participate in 'copy', after the substitution θ has been applied◊
Under the same assumptions, A Aθ = B Bθ.
If an expression E is converted into K by some combination of theta-copies and CL-operations, the same effect can be achieved by performing all the theta-copies first, and keeping the CL-operations to the end.
For simplicity, let us assume that just three theta-copies are involved: it will be apparent that our reasoning can be extended to more complicated instances. Suppose then that E Eθ is CL-equivalent to F, that F Fφ is CL-equivalent to G, and that G Gψ is CL-equivalent to K. Let us introduce the abbreviation
E[1+θ]
for the expression
E Eθ.
What we want to show is that E[1+θ][1+φ][1+ψ] is CL-equivalent to K. It is given that E[1+θ] is CL-equivalent to F; then E[1+θ][1+φ] is CL-equivalent to F[1+φ] by Corollary 2.9. But it is given that F[1+φ] = G, therefore E[1+θ][1+φ] = G. By the same reasoning,
E[1+θ][1+φ][1+ψ] = F[1+φ][1+ψ] = G[1+ψ] = K ◊
A necessary and sufficient condition for E to be mark-equivalent, is that there should exist a set of substitutions θ1, θ2.. θn such that
Eθ1 Eθ2 ... Eθn = O,
where = denotes CL-equivalence (not mere CLS-equivalence).
(i) We prove first sufficiency of the condition. O = Eθ1Eθ2.. Eθn implies (by the dominance of the mark O)
O =
E Eθ1 Eθ2 Eθ1θ2
Eθ3 Eθ1θ3 Eθ2θ3
Eθ1θ2θ3 ...
= E [1+θ1][1+θ2] ... [1+θn] ,
where, as before, [1+θ] stands for the operation which converts an expression F into F Fθ. Thus E is transformed into an expression that is CL-equivalent to O by doing n of these operations in succession, therefore E is CLS-equivalent to O.
(ii) Necessity. Suppose it is given that E ≅ O. This means that some combination of theta-copies and CL-operations converts E into O. It is possible that some of the theta-copy steps might be reverse theta-copies (where F Fθ is converted to F). But such steps can be omitted. For the effect of such a step is simply to get rid of an unwanted sub-expression Fθ. If the step is omitted, the unwanted sub-expression remains as an appendage to the 'wanted' part of the expression. If many such steps are omitted, the wanted expression will end up accompanied by a whole lot of unwanted 'junk'. However, if the wanted expression is CL-equivalent to O, then so is the whole expression, including the junk (by repeated application of 'delete'). Therefore, without loss of generality, we may assume that all the theta-copy steps are positive (not reverse) theta-copies.
By the Delay Principle (Lemma 2.10), we may assume that the sequence of steps leading from E to the mark consists of a number of theta-copies, followed by a number of CL-steps. So the sequence of theta-copies turns E into an expression that is CL-equivalent to O. Thus
O =
E[1+φ1][1+φ2]...[1+φm]
= E Eφ1 Eφ2 Eφ1φ2
Eφ3 Eφ1φ3 Eφ2φ3
Eφ1φ2φ3 ...
But each term in this last expression is actually of the form Eθ for some θ — where we use the facts a) that 'do nothing' may be regarded as a trivial sort of substitution, and b) that the effect of performing two substitutions in a row may be regarded as the effect of performing just one (more comprehensive) substitution. Thus the expression is of the form
Eθ1 Eθ2.. Eθn = O,
as required to prove Lemma 2.11◊