A generalization of the functions head and tail (unfinished)

A generalization of the functions head and tail.

by Edsger W. Dgksra and C. S. Scholten

We consider sequences defined as structures on the natural coordinate $x$ . Let $S$ be such a sequence. The functions $h\left( = \text{head}\right)$ and $t\left( = \text{tail}\right)$ are defined

$$ h. S = S _ {0} ^ {x} \qquad a n d \quad f. S = S _ {1 + x} ^ {x} $$

Note that h.s is an "element" -viz. the "leading" one- and t.s is again a sequence -viz. "the rest". (With the : for concatenation -as,for instance in SASL- we have the identity $S = h.S : t.S$ .)

There are several ways of expressing $S^{\prime}$ sub $s$ i.e. that $S^{\prime}$ is a postfix of $s$ ..

$$ S ^ {\prime} \mathrm {s u b} S \equiv (E n: n \geqslant 0: S ^ {\prime} = t ^ {n}. S) \quad o r $$

$$ S ^ {\prime} \underline {{\text {s u b}}} S \equiv (E n: n > 0: S ^ {\prime} = S _ {n + X} ^ {X}) $$

We prefer the latter one. Representing the natural number n by a string of zeros, and hence addition by juxtaposition, we would get

$$ S ^ {\prime} \underline {{\mathrm {s u b}}} S \equiv (\operatorname {E n}: n \in {0 } ^ {*}: S ^ {\prime} = S _ {n x} ^ {x}) $$

The above is extended to tuples of sequences. Illustrating it for two we thus define

$$ (S ^ {\prime}, T ^ {\prime}) \underline {{\operatorname {s u b}}} (S, T) \equiv (\operatorname {E n}: n \in {0 } ^ {*}: (S ^ {\prime}, T ^ {\prime}) = (S, T) _ {n x} ^ {x}). $$

Substitution being defined to distribute over pair forming.

the quantified expression may be rewritten as

$$ (S ^ {\prime}, T ^ {\prime}) = (S _ {n x} ^ {x}, T _ {n x} ^ {x}) $$

with element-wise application of equality this yields

$$ S ^ {\prime} = S _ {n x} ^ {x} \wedge T ^ {\prime} = T _ {n x} ^ {x} $$

To complete the understanding of the above we define for sequences S and T equality by

$$ S = T \equiv h. S = h. T \wedge t. S = t. T $$

We mention without proof

$$ S = T \equiv (\underline {{A}} (S, T): (S, T) \underline {{\mathrm {s u b}}} (S, T): h. S ^ {\prime} = h. T ^ {\prime}) $$

(The proof is left as an exercise for the authors.)

A sequence is a special instance of a rooted tree with constant fan-out, viz. with fan-out $= 1$ , in exactly the same way as ${0}$ is a special case of a finite alphabet. In the following, C stands for an alphabet of $m$ characters, our tuples will be $m$ -tuples and our trees trees with constant fan-out $= m$ .

We now consider a tree as a structure defined on a coordinate $x$ ranging over $C^*$ . Let $S$ be such a tree. The function head has its obvious analogue: it is known under the name root, and we shall denote it by $r$ and define it by

$$ r. S = S _ {< } ^ {x} $$

in which $\Leftrightarrow$ denotes the empty string.

The corresponding notion sub, however, poses a problem. Do we define

$$ S ^ {\prime} \underline {{\operatorname {s u b}}} S \equiv (E n: n e C ^ {*}: S ^ {\prime} = S _ {n x} ^ {x}) $$

or $S^{\prime}$ sub $S\equiv (E_n:n\in C^x:S^{\prime} = S_{xn}^{x})$ ？

Note In either case we have the theorem - mentioned without proof- that for trees $S$ and $T$

$$ S = T \equiv (\underline {{A}} S ^ {\prime}, T ^ {\prime}: (S ^ {\prime}, T ^ {\prime}) \underline {{\mathrm {s u b}}} (S, T): r. S ^ {\prime} = r. T ^ {\prime}) $$

(End of Note.)

In this stage we have no grounds for preferring the one sub over the other. (For a single character alphabet, the two definitions coincide.)

For $m \geq 2$ ,we have two different ways of defining under control of a parameter $c\;c \in {C}^{ * }$ ,a new free in terms of a given one:

$$ c \underline {{e x}} S = S _ {c x} ^ {x} $$

$$ S _ {e x} = S _ {x c} ^ {x} $$

Here we have used the same operator $\underline{\mathbf{\alpha}}\mathbf{x}$ as asymmetric infix operator between a tree and an element of $C^*$ .

with $b \in {C}^{ * }$ and $c \in {C}^{ * }$ we then have

$$ c \underline {{e x}} (b \underline {{e x}} S) = (b c) \underline {{e x}} S $$

$$ (S \underline {{e x}} b) \underline {{e x}} c = S \underline {{e x}} (c b); $$

note that on account of the types of b.c. and S, the parentheses in the left-hand sides of the above could have been omitted.

Furthermore, we have

$$ b \underline {{e x}} (S \underline {{e x}} c) = (b \underline {{e x}} S) \underline {{e x}} c $$

both sides being equal to $S_{b\times c}^{*}$ . Consequently, also here the parentheses may be omitted. We conclude that the "continued" ex of which 1 operand is a free while the others are from C* needs no parentheses.

Finally, note that $\Leftrightarrow \underline{\underline{\mathrm{ex}}}\;$ and $\;$ ex<> are identity operators. Note also

$$ r. (c \underline {{e x}} S) = r. (S \underline {{e x}} c) $$

So much for the general ex

of special interest is the use of ex with the string operand of length 1 . Let e be a parameter ranging over the strings of length 1 in $C^*$ or - if we don't distinguish between one-element strings and elements- ranging over $C$ ; e has m distinct

possible values. For such e ,

$e$ ex $S$ is called "son tree $n$ r.e. of $S$ " and

Sex e is called "daughter free n.e of $S$ ".

These are the closest analogue of the function tail : firstly it has an additional parameter ranging over C , secondly there is the distinction between sons and daughters. The latter distinction gives us two alternative recursive definitions for the equality of two trees S and T :

$$ \begin{array}{l} S = T \equiv r. S = r. T \wedge (\underline {{A}} e: e \in C: e \underline {{e}} x S = e \underline {{e}} x T) \ S = T \equiv r. S = r. T \wedge (\underline {{A}} e. e \in C: S \underline {{e}} x e = T \underline {{e}} x e). \ \end{array} $$

After ex we turn our attention to a number of unary operators, to begin with some that form a new tree from a given one.

Consider the function rev on strings, with be $C_^$ $c \in C^*$ , and e∈C given by

$$ \begin{array}{l} \operatorname {r e v} < > = < \ \text {r e v .} e \quad = e \ r e v. (b c) = (r e v. c) (r e v. b) \ \end{array} $$

In terms of rev we now define the "transpose"

$$ S ^ {T} = S _ {r e v. x} ^ {x} $$

Since $\left. {\operatorname{rev}.}\left( {\operatorname{rev}.x}\right) = x}\right} ,{\left( {S}^{T}\right) }^{T} = S$ . The connection between the transpose and $\underline{\mathrm{ex}}$ is given by

$$ (b \underline {{e x}} S) ^ {T} = S ^ {T} \underline {{e x}} (\operatorname {r e v}. b), a n d i n p a r t i c u l a r $$

$$ (e \underline {{e x}} S) ^ {T} = S ^ {T} \underline {{e x}} e $$

For our purposes, the transpose is not a very important operator; it has been mentioned because it illustrates an underlying duality so nicely.

For the sake of completeness we also mention $\mathsf{ROT}$ defined by $\mathsf{ROT. S} = \mathsf{S}_{\mathsf{rot}.x}^{\mathsf{x}}$

where $\operatorname{rot}.\angle > = \angle >$

$$ r o t (e b) = b e $$

This is a function in which we are even less in- terested than in the transpose. This is because our interest in such infinite trees, i.e. functions on $C^$ stems from considerations about recursion, which relate elements of $C^$ with, say, a common prefix, a relation which is completely destroyed by rot. (So we hardly take the trouble to observe

$$ e \underline {{\underline {{e x}}}} (\mathrm {R o T . S}) = S \underline {{\underline {{e x}}}} e $$

Now we return to e ex S ; it is again a tree, comprising , so to speak, /m-th of the elements of S minus its root. Let now e range over C; the combined elements of the resulting m trees comprise all the elements of S exept the root: it can be viewed, therefore, as a function on $C^+$ , i.e. all non-empty finite strings of $C^*$ . We can denote

EWD929-6

the aggregate of the son trees of s by s.s and