A tentative axiomatization of ascending sequences

A tentative axiomatization of ascending sequences

Yesterday I tried to base my lecture on EWD817 "An introduction to three algorithms for sorting in situ", which I had written with A.J.M.van Gasteren in early 1982. At the time, I remember, I liked that text very much, but yesterday I learned that now, more than 11 years later, the text did not work anymore. I found it too verbose and was several times tempted to resort to pictures: I gave a fairly abominable lecture. So let me try an alternative.

We use capital letters $X, Y, Z, \ldots$ as variables of type "finite sequence", lower case letters $p, q, r, \ldots$ as variables of type "singleton sequence", and $\varepsilon$ to denote the empty sequence. Consequently, $X := p$ and $Y := z$ are instances of legal instantiations, $p := X$ and $q := z$ are not. The associative operation of concatenation is - dangerously and stupidly, but let me sin for once! denoted by juxtaposition with a binding power higher than functional application, which is denoted by an infix dot.

At least for the time being, I won't. axiomatize concatenation; this will not prevent me from carrying out mathematical induction over the length or the grammar of sequences.

(This because mathematical induction over a potentially ambiguous grammar is felt to be a separate issue.) Hence I do not commit myself concerning the status - axiom or theorem - of propositions like

$$ X Y = X \equiv Y = \varepsilon $$

$$ Y X = X \equiv Y = \varepsilon $$

$$ X Y = \varepsilon \equiv X = \varepsilon \wedge Y = \varepsilon $$

$$ p X \neq X \quad X _ {p} \neq X $$

$$ p X = q Y \vee X p = Y q \Rightarrow p = q \wedge X = Y, e k. $$

I wish to capture "ascending sequences", defined in terms of the relation $\leq$ , which is a total order on the singletons:

$$ p \leq p \quad (\mathrm {r e f l e x i v e}) $$

$$ p \leq q \land q \leq p \Rightarrow p = q (\mathrm {a n t i s y m m e t r i c}) $$

$$ p \leq q \land q \leq r \Rightarrow p \leq r (\mathrm {t r a n s i t i v e}) $$

$$ p \leq q \vee q \leq p \quad (\mathrm {t o t a l}) $$

but propose to do that via a relation between sequences. Informally $X \times Y$ says that $p \leq q$ holds for any $p$ from $X$ and any $q$ from $Y$ . The relation $\chi$ - let us pronounce it as "under-" has been intro-

duced in the hope that it will reduce the number of universal quantificatons we have to indicate explicitly. The special character $\prec$ has been introduced because $\prec$ has properties very different from $\leq$ : $\prec$ is not reflexive,not antisymmetric, not transitive,and not total.

(0) X X $p \cdot q \equiv p \leq q$ (1) (2) $XY \prec Z \equiv X \prec Z \land Y \prec Z$ (3) $Z \prec {XY} \equiv Z \prec X \land Z \prec Y$

Relation $\prec$ is not transitive :

$$ X \prec Y \land Y \prec Z \Rightarrow X \prec Z $$

reduces for $Y \mathrel{\text{:=}} \varepsilon$ on account of (0) to $X \prec Z$ ,which need not hold. Replace

${X}{1} < {Y}{9} \land {Y}_{9} < 2 \Rightarrow X < 2$

We shall prove (4) to show the pattern. To prove (4) we observe $X \sim {Y}_{9}\;Y \sim Y\;Z$ $X \prec Y \land X \prec q \land Y \prec Z \land q \prec Z$

$$ \begin{array}{l} \Rightarrow \begin{array}{r l} & X \prec q \wedge q \prec 2 \ & {(5) } \end{array} \ x \prec z, \mathrm {w h e r e} \ \end{array} $$

(5) $x \prec q \land q \prec z \Rightarrow x \prec z$

represents our remaining proof obligation, which we meet by mathematical induction over (the length $\phi$ ) 2. For the base we observe $\left( {2 \mathrel{\text{:=}} \varepsilon }\right)$

$$ \begin{array}{l} X \prec \varepsilon \ = \left{ \begin{array}{l} {(0)} \ {\mathrm {t r u e}} \end{array} \right} \ \Leftrightarrow \quad \begin{array}{l} {{\mathrm {p r e d . c a l c .} }} \ {X \prec q \land q \prec 2} \end{array} \ \end{array} $$

For the step we observe $\left( {Z \vdots r - z}\right)$

$$ \begin{array}{l} x \prec r 2 \ = {3 } \ \end{array} $$

$$ X \prec r \wedge X \prec Z $$

$$ \begin{array}{l} \Leftrightarrow \left{ \begin{array}{l} e x h y p o t h e s i, i. e. (5) \ X \times r \wedge X \times q \wedge q \times Z \end{array} \right. \ \Leftrightarrow \quad {(6) } \ \end{array} $$

$$ \begin{array}{l} x \prec q \land q \prec r \land q \prec 2 \ = {^ {\prime} (3) } \ \end{array} $$

$$ x \prec q \land q \prec r Z \qquad w h e r e $$

(6) $X \prec q \land q \prec r \Rightarrow X \prec r$

represents our remaining proof obligation,

which can be met by induction over (the length of) $X$ . For the base $\left( {X = \varepsilon }\right)$ we observe

$$ \begin{array}{r l} & {\varepsilon \prec q \land q \prec r \Rightarrow \varepsilon \prec r} \ {=} & {{0, p r e d. c a l c }} \ & {\mathrm {t r u e}} \end{array} $$

for the step we observe $\left( {X = pX}\right)$

$$ \begin{array}{l} = \begin{array}{l} p X \prec r \ {(2) } \end{array} \ \Leftrightarrow \begin{array}{l} p \prec r \land X \prec r \ \Leftrightarrow {e x h y p o t h e s i, (6) } \end{array} \ = \begin{array}{l} p \prec r \land^ {\sim} X \prec q \land q \prec r \ {(1) } \end{array} \ \leqslant \begin{array}{l} p \leq r \land X \prec q \land q \prec r \ {s \leq i s t r a n s i t i v e } \end{array} \ p \leq q \land q \leq r \land X \prec q \land q \prec r \ = {(\mathrm {1}) a n d p r e d. c a l c. } \ = {2 } \ \end{array} $$

$$ p X \prec q \land q \prec r, $$

with which our proof obligations have been

needed.

I would like to define the function "asc" of type: sequence $\rightarrow$ bool

(7) $\operatorname{asc.}p$ (8) $\operatorname{asc.} XY \equiv \operatorname{asc.} X \wedge \operatorname{asc.} Y \wedge X \prec Y,$

but I am not quite sure about my proof obligations that this definition of $\mathrm{{asc}}$ makes sense, i.e. does not lead to contradiction. My gut feeling is that I have done my duty when I have shown that "asc" is a function, i.e. satisfies

$$ X = Y \Rightarrow (\operatorname {a s c}, X \equiv \operatorname {a s c}, Y) $$

for all possible ways in which $X = Y$ can hold, where the possible ways are listed by the axioms about equality of sequences.

So we would have to show that

(7) $\land \left( 8\right)$ is compatible with

$\operatorname{asc.}X \equiv \operatorname{asc.}{X\varepsilon }$ and

$\operatorname {a s c},X\equiv \operatorname {a s c},\varepsilon X$

the obligation rising from $x = {x\sum }$ and

defining (concluding?) asc. 3 , i.e. the empty sequence is ascending .

so we have to show that (7)∧(8)

is compatible with

(9) $\operatorname{asc.} X\left( {Y2}\right) \equiv \operatorname{asc.}\left( {XY}\right) 2\;,\;$

the obligation rising from the associativity of

concatenation; I expect to prove (9) in view of (8) thanks to the associativity of $\land$ .

$$ \begin{array}{l} \operatorname {a s c}. X (Y Z) \ = {(8) \mathrm {w i t h} Y _ {i} = Y Z } \ a s c. X \wedge a s c. Y Z \wedge X \prec Y Z \ = {(8) \mathrm {w i t h} X, Y := Y Z; (3) \mathrm {w i t h} X, Y, Z := Y, Z, X } \ \operatorname {a s c}. X \wedge \operatorname {a s c}. Y \wedge \operatorname {a s c}. Z \wedge Y \wedge Z \wedge X \wedge Y \wedge X \wedge Z \ = {(\mathbf {8}), (\mathbf {2}) } \ a s c. X Y \wedge a s c. Z \wedge X Y \prec Z \ {(\mathfrak {g}) \mathrm {w i t h} X, Y := X Y, Z } \ a s c. (X Y) Z \ \end{array} $$

The above proof is of an almost embarrassing triviality, but it is nice that we did not need mathematical induction.

A simple lemma is

(10) $\operatorname{asc.}XYZ \Rightarrow \operatorname{asc.}XZ$

which is proved in the same vein as the previous

one :

$$ \begin{array}{l} a s c. X Y Z \ = {\mathrm {s e e a b o v e} } \ \operatorname {a s c}. X \wedge \operatorname {a s c}. Y \wedge \operatorname {a s c}. Z \wedge Y \prec Z \wedge X \prec Y \wedge X \prec Z \ \Rightarrow \quad {\mathrm {p r e d . c a l c .} } \ \operatorname {a s c.} X \wedge \operatorname {a s c.} Z \wedge X \prec Z \ = {8 } \ \mathrm {a s c .} X Z \ \end{array} $$

Repeated application of (10) tells us that

(11) any subsequence of an ascending

Slightly more ambitious is

(12) $\operatorname{asc.}X_{p}Y \equiv \operatorname{asc.}X_{p} \land \operatorname{asc.}pY$

We observe for any $X, p, Y$ ,

$$ \begin{array}{l} \operatorname {a s c}. X _ {p} \wedge \operatorname {a s c}. p Y \ = {(8) + w i c e } \ \mathrm {a s c .} X \wedge \mathrm {a s c .} P \wedge \mathrm {a s c .} Y \wedge \ X \mapsto p \land p \mapsto Y \ = {^ {\prime} (4) } \ a s c. X \wedge a s c. p \wedge a s c. Y \wedge \ X \prec p \land p \prec Y \land X \prec Y \ = {(8) a n d (2) o r (3) } \ \operatorname {a s c.} X _ {p} Y \ \end{array} $$

Remark It was a surprise for me that nothing is gained by proving (12) with a ping-pong argument. (End of Remark.)

And now we are ready to prove the beautiful

(13) $\operatorname{asc.}XY \Rightarrow \operatorname{asc.}{Xp} \vee \operatorname{asc.}{p}^{Y}$

Regretably, I cannot avoid case analysis

(i) $Y = \mathcal{E}$ and (ii) $Y = {qZ}$

(i) Since $Y = \varepsilon \Rightarrow \operatorname{asc.}pY$ on account of (7)

lemma (13) has been proved in this case.

(ii) In this case we rewrite our demonstran-

dum (13) with $Y \mathrel{\text{:=}} {9Z}\;$ by shunting as

$$ \operatorname {a s c}. X _ {q} Z \wedge \neg \operatorname {a s c}. p q Z \Rightarrow \operatorname {a s c}. X _ {p} $$

and observe for arbitrary $p,q,x,z$

$$ a s c. X q Z \wedge \neg a s c. p q Z $$

$= \left{ {\left( {12}\right) ,{twice},\text{and}{de Morgan}}\right}$

$$ a s c. X q \wedge a s c. q Z \wedge (\neg a s c. p q \vee \neg a s c. q Z) $$

$\Rightarrow$ ${$ pred. calc. $}$

$\Rightarrow \;\left{ {\text{since} - \left( 1\right) ,{\left( 7\right) }^{\prime },\left( 8\right) - 7\operatorname{asc.}{pq} \Rightarrow \operatorname{asc.}{qp}}\right}$

$$ \begin{array}{l} a s c. X q \land \neg a s c. p q \ a s c. X _ {q} \wedge a s c. q p \ = {1 2 } \ \begin{array}{l} \mathrm {a s c . X q p} \ {\mathrm {(1 0)} } \end{array} \ \mathrm {a s c .} X _ {p} \ \end{array} $$

which completes the proof of (13)

The next theorem to be proved is (of course)

(14) $\operatorname{asc.}Z \Rightarrow \left\langle {\exists X,Y : XY = Z : \operatorname{asc.}{Xp} \land \operatorname{asc.}{pY}}\right\rangle$

or, in view of (12), equivalently

(14) $\operatorname{asc.}Z \Rightarrow \left\langle {\exists X,Y : XY = Z : \operatorname{asc.}{XpY}}\right\rangle$ ,

a lemma that can be viewed as underlying the feasibility of "insertion sort".

One way of proving this is by mathematical induction over the length of 2 . For the base we have to show

$$ \operatorname {a s c}. \varepsilon \Rightarrow \langle \exists U, V: U V = \varepsilon : \operatorname {a s c}. U p V \rangle ; $$

the witness $U = \varepsilon , V = \varepsilon$ demonstrates the truth of its consequent. For the step it suffices to show

$$ \operatorname {a s c}. Z q \Rightarrow \langle \exists U, V: U V = Z q: \operatorname {a s c}. U p V \rangle ; $$

if $q\le p$ we can take as witness $U = Zq,V = \varepsilon$ . asc. Up reduces to asc.Zqp or (12) to asc.Zq aasc.qp, which is implied; if $p\le q$ ,we take XY satisfying (14)

(15) ${XY} = 2,$ asc. $X$ p , asc. $pY$

and can take as witness $U = X$ , $V = Yq$ , and observe, (assuming $\operatorname{asc.} Zq \wedge p \leq q$ )

$$ \begin{array}{l} \operatorname {a s c}. U _ {p} V \ = {(1 2) } \ a s c. U _ {p} \wedge a s c. p V \ = {\mathrm {d e f .} o u t V } \ a s c. X p \wedge a s c. p Y q \ = {(\dot {1} 5): a s c. X p } \ a s c. p Y q \ = {^ {(8)} } \ a s c. p \wedge a s c. Y q \wedge p \prec Y q \ \Leftrightarrow {(\mathrm {7}), (\mathrm {8}), (\mathrm {3}) } \ a s c. X Y q \wedge p \prec Y \wedge p \prec q \ \end{array} $$

$\Leftrightarrow \quad {(15): XY = Z,(8),(1)}$

$$ \begin{array}{l} a s c. Z q \wedge a s c. p Y \wedge p \leq q \ = {C _ {1 5}: a s c. p Y } \ a s c. 2 q \land p \leq q \ \end{array} $$

which was our assumption.

For the sake of completeness we give a different phrasing of virtually the same proof of (14)

Let $Y$ be the shortest sequence that $X$ and $Y$ furthermore satisfy

(16) ${XY} = Z \land \operatorname{asc.}{Xp}$

[Such a shortest sequence exists. for (16) has at least 1 solution: $X = \varepsilon ,Y = Z]$ . Our proof obligation is now -see (14)-

(17) $\operatorname{asc.}pY.$

If $Y = \varepsilon$ ,(17) holds because of (7).

otherwise, we write $Y = {qU}$ ,and have to conclude

(17) $\operatorname{asc. p q } \cup$

From

(16') ${X}{9}U = 2\; \land \;\operatorname{asc.}{X}{p}$

(18) $\operatorname{asc.2}$ (19) $\rightarrow \operatorname{asc} \cdot X$ q

where (18) is a reminder of the antecedent of (14) and (19) expresses that Y was the shortest sequence meeting the require- ment. We observe, using (16'), (18)

true

$$ \begin{array}{l} \Rightarrow {1 6 ^ {\prime} \wedge (1 8) } \ a s c. X q U \wedge a s c. X p \ \Rightarrow \quad {(8) } \ \operatorname {a s c}. X _ {q} \wedge \operatorname {a s c}. X _ {p} \ = {(1 9) } \ a s c. X q \wedge a s c. X p \wedge \neg a s c. X q p \ = {(8), (7) } \ \operatorname {a s c}. X q \wedge \operatorname {a s c}. X p \wedge (\neg \operatorname {a s c}. X q \vee \neg X q \prec p) \ \Rightarrow \quad {\mathrm {p r e d . c a l c .} } \ a s c. X p \wedge \neg X q \prec p \ \Rightarrow {(8), (2), (1) } \ X \prec p \land (\neg X \prec p \lor \neg q \leq p) \ \Rightarrow \quad {\mathrm {p r e d . c a l c .} } \ p < q \ \Rightarrow {1), (7), (8); (1 6 ^ {\prime}), (1 8), (8) } \ a s c. p q \land a s c. q U \ = {(\dot {1} 2) } \ \operatorname {a s c .} p q U. \ \end{array} $$

I have no distinct preference for the latter phrasing. Austin, 27 Oct. - 10 Nov. 1993

prof. Dr. Edsger W. Dykstra, Dept. of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188, USA