7.3. Equivalence of modes

{One way of viewing recursive modes is to consider them as infinite trees. Such a "mode tree" is obtained by repeatedly substituting in some spelling, for each 'MU application', the 'MODE' of the corresponding 'MU definition of MODE'. Thus, the spelling 'mui definition of structured with integral field letter i reference to mui application field letter n mode' would give rise to the following mode tree:

Two spellings are equivalent if and only if they give rise to identical mode trees. The equivalence syntax tests the equivalence of two spellings by, as it were, simultaneously developing the two trees until a difference is found (resulting in a blind alley) or until it becomes apparent that no difference can be found. The growing production tree reflects to some extent the structure of the mode trees.}

7.3.1. Syntax

B) HEAD :: PLAIN ; PREF{71A } ; structured with ; FLEXETY ROWS of ; procedure with ; union of ; void.

C) TAILETY :: MOID ; FIELDS mode ; PARAMETERS yielding MOID ; MOODS mode ; EMPTY.

D) PARTS :: PART ; PARTS PART.

E) PART :: FIELD ; PARAMETER.

a) WHETHER MOID1 equivalent MOID2{64b ,71m,72c} : WHETHER safe MOID1 equivalent safe MOID2{b}.

b) WHETHER SAFE1 MOID1 equivalent SAFE2 MOID2{a,b,e,i,j,n} : where (SAFE1) contains (remember MOID1 MOID2) or (SAFE2) contains (remember MOID2 MOID1), WHETHER true ; unless (SAFE1) contains (remember MOID1 MOID2) or (SAFE2) contains (remember MOID2 MOID1), WHETHER (HEAD3) is (HEAD4) and remember MOID1 MOID2 SAFE3 TAILETY3 equivalent SAFE4 TAILETY4{b,d,e,k,q,-}, where SAFE3 HEAD3 TAILETY3 develops from SAFE1 MOID1{c} and SAFE4 HEAD4 TAILETY4 develops from SAFE2 MOID2{c}.

c) WHETHER SAFE2 HEAD TAILETY develops from SAFE1 MOID{b,c} : where (MOID) is (HEAD TAILETY), WHETHER (HEAD) shields SAFE1 to SAFE2{74a,b,c,d ,-}; where (MOID) is (MU definition of MODE), unless (SAFE1) contains (MU has), WHETHER SAFE2 HEAD TAILETY develops from MU has MODE SAFE1 MODE{c}; where (MOID) is (MU application) and (SAFE1) is (NOTION MU has MODE SAFE3) and (NOTION) contains (yin) and (NOTION) contains (yang), WHETHER SAFE2 HEAD TAILETY develops from SAFE1 MODE{c}.

d) WHETHER SAFE1 FIELDS1 mode equivalent SAFE2 FIELDS2 mode{b} : WHETHER SAFE1 FIELDS1 equivalent SAFE2 FIELDS2{f,g,h,i}.

e) WHETHER SAFE1 PARAMETERS1 yielding MOID1 equivalent SAFE2 PARAMETERS2 yielding MOID2{b} : WHETHER SAFE1 PARAMETERS1 equivalent SAFE2 PARAMETERS2{f,g,h,j} and SAFE1 MOID1 equivalent SAFE2 MOID2{b}.

f) WHETHER SAFE1 PARTS1 PART1 equivalent SAFE2 PARTS2 PART2{d,e,f} : WHETHER SAFE1 PARTS1 equivalent SAFE2 PARTS2{f,g,h,i,j} and SAFE1 PART1 equivalent SAFE2 PART2{i,j}.

g) WHETHER SAFE1 PARTS1 PART1 equivalent SAFE2 PART2{d,e,f} : WHETHER false.

h) WHETHER SAFE1 PART1 equivalent SAFE2 PARTS2 PART2{d,e,f} : WHETHER false.

i) WHETHER SAFE1 MODE1 field TAG1 equivalent SAFE2 MODE2 field TAG2{d,f} : WHETHER (TAG1) is (TAG2) and SAFE1 MODE1 equivalent SAFE2 MODE2{b}.

j) WHETHER SAFE1 MODE1 parameter equivalent SAFE2 MODE2 parameter{e,f} : WHETHER SAFE1 MODE1 equivalent SAFE2 MODE2{b}.

k) WHETHER SAFE1 MOODS1 mode equivalent SAFE2 MOODS2 mode{b} : WHETHER SAFE1 MOODS1 suhset of SAFE2 MOODS2{l,m,n} and SAFE2 MOODS2 subset of SAFE1 MOODS1{l,m,n} and MOODS1 number equals MOODS2 number{o,p}.

l) WHETHER SAFE1 MOODS1 MOOD1 subset of SAFE2 MOODS2{k,l,46s ,64b} : WHETHER SAFE1 MOODS1 subset of SAFE2 MOODS2{l,m,n} and SAFE1 MOOD1 subset of SAFE2 MOODS2{m,n}.

m) WHETHER SAFE1 MOOD1 subset of SAFE2 MOODS2 MOOD2{k,l,m,46s ,64b} : WHETHER SAFE1 MOOD1 subset of SAFE2 MOODS2{m,n} or SAFE1 MOOD1 subset of SAFE2 MOOD2{n}.

n) WHETHER SAFE1 MOOD1 subset of SAFE2 MOOD2{k,l,m,64b } : WHETHER SAFE1 MOOD1 equivalent SAFE2 MOOD2{b}.

o) WHETHER MOODS1 MOOD1 number equals MOODS2 MOOD2 number{k,o} : WHETHER MOODS1 number equals MOODS2 number{o,p,-}.

p) WHETHER MOOD1 number equals MOOD2 number{k,o} : WHETHER true.

q) WHETHER SAFE1 EMPTY equivalent SAFE2 EMPTY{b} : WHETHER true. {Rule a introduces the 'SAFE's which are used as associative memories during the determination of equivalence. There are two of them, one belonging to each mode. Rule b draws an immediate conclusion if the 'MOID's under consideration are already remembered (see below) in an appropriate 'SAFE' in the form 'remember MOID1 MOID2'. If this is not the case, then the two 'MOID's are first remembered in a 'SAFE' (the one on the left) and then each 'MOID' is developed (rule c) and split into its 'HEAD' and its 'TAILETY', e.g., 'reference to real' is split into 'reference to' and 'real'.

If the 'HEAD's differ, then the matter is settled (rule b); otherwise the 'TAILETY's are analyzed according to their structure (which must be the same if the 'HEAD's are identical). In each case, except where the 'HEAD's were 'union of', the equivalence is determined by examining the corresponding components, according to the following scheme:

FIXME

In the case of unions, the 'TAILETY's are of the form 'MOODS1 mode' and 'MOODS2 mode'. Since 'MOOD's within equivalent unions may commute, as in the modes specified by UNION (REAL, INT) and UNION (INT, REAL), the equivalence is determined by checking that 'MOODS1' is a subset of 'MOODS2' and that 'MOODS2' is a subset of 'MOODS1', where the subset test, of course, invokes the equivalence test recursively (rules k, l, m, n, o, p).

A 'MOID' is developed (rule c) into the form 'HEAD TAILETY' by determining that

1. it is already of that form: in which case markers ('yin' and 'yang') may be placed in its 'SAFE' for the later determination of well-formedness (see 7.4 );
2. it is some 'MU definition of MODE': in which case 'MU has MODE' is stored in its 'SAFE' (provided that this particular 'MU' is not there already) and the 'MODE' is developed;
3. it is some 'MU application': in which case there must be some 'MU has MODE' in its 'SAFE' already. That 'MODE' is then developed after a well-formedness check (see 7.4 ) consisting of the determination that there is at least one 'yin' and at least one 'yang' in the 'SAFE' which is more recent than the 'MU has MODE'.

{Before a pair of 'TAILETY's is tested for equivalence, it is remembered in the 'SAFE' that the original pair of 'MOID's is being tested. This is used to force a shortcut to 'WHETHER true' if these 'MOID's should ever be tested again for equivalence lower down the production tree. Since the number of pairs of component 'MOID's that can be derived from any two given 'MOID's is finite, it follows that the testing process terminates.

It remains to be shown that the process is correct. Consider the unrestricted (possibly infinite) production tree that would be obtained if there were no shortcut in the syntax (by omitting the first alternative together with the first member of the other alternative of rule b). If two 'MOID's are not equivalent, then there exists in their mode trees a shortest path from the top node to some node exhibiting a difference. Obviously, the reflection of this shortest path in the unrestricted production tree cannot contain a repeated test for the equivalence of any pair of 'MOID's, and therefore none of the shortcuts to 'WHETHER true' in the restricted production tree can occur on this shortest path. Consequently, the path to the difference must be present also in the (restricted) production tree produced by the syntax. If the testing process does not exhibit a difference in the restricted tree, then no difference can be found in any number of steps: i.e., the 'MOID's are equivalent.}
 
Next