About the correctness of a few SASL programs

About the correctness of a few SASL programs

Shortly after my arrival in Austin, Texas, I mentioned the longest-upsequence problem. A few -warm!- days later, dr. fiamilton Richards offered me four solutions for my consideration. I shall render his solutions in the offi-cial SASL syntax -in spite of my objections to it - and in order to save dr. Richards from possible blame I would like to stress that the inefficiency of the first solution was quite deliberate.

Given a sequence $M$ of integers, find a longest ascending subsequence (i.e. upsequence) of $M$ .

First solution: Generates all subsequences, filters out the non-ascending ones, and chooses the longest.

longest (filter ascending (sub s M))

where

\begin{array}{l} \begin{array}{r l} \overline {{s u b s}} (\cdot) & = ((\cdot),) \end{array} \ s u b s (p: x) = {p: s u b x; s u b x \gets s u b s x } + + s u b s x \ \text {w h e r e} \text {s u b s x} = \text {s u b s x} \ \end{array}

\begin{array}{l} a s c e n d i n g () = \underline {{\mathrm {t r u e}}} \ a s c e n d i n g (a, \cdot) = t r u e \ a s c e n d i n g (a: b: x) = \overline {{a ≤ b}} ∧ a s c e n d i n g (b: x) \ \end{array}

\begin{array}{l} \begin{array}{r l} \text {p i f t e r c (C)} & = () \end{array} \ f i l t e r c (a: x) = c a \rightarrow a: f i l t e r c x; \ f i t h e r c x \ \end{array}

(NB. The semicolon plays the role of else.)

\begin{array}{l} \mathrm {l o n g e s t} (a, \cdot) = a \ l o n g e s t (a: x) = l o n g e r a 1 x \rightarrow a; 1 x \ \mathrm {w h e r e} | x = \mathrm {l o n g e s t} x \ l o n g e r x () = t r u e \ l o n g e r () y = f o l s e \ l o n g e r (a: x) (b: y) = l o n g e r x y \ \end{array}

Let me add some legenda to the above. With x a sequence of integers, the value of subs x is a list of all sub- sequences of $x$ . Between the braces subx is the bound

variable ; it is of type subsequence and the $\leftarrow$ indicates that it ranges over the elements of subsx . (The list formation denoted by the shorthand of the braces is order preserving. If subx1 occurs before subx2 in subsx , p:subx1 occurs before p:subx2 in the whole brace expression.) The ++ denotes concatenation. It is clear that subs (p:x) contains twice as many elements as subs x : all subsequences of M, including the empty one, are generated.

The argument of ascending is of type integer sequence. (I find myself reserving the term sequence for what is syntactically a list of integers. Thus I avoid having to talk about lists of lists.) The function ascending - which is of type boolean - is separately defined for the empty sequence, for the 1-element sequence, and for the sequence of 2 or more elements. The last one is recursive and recursion ends with a 1-element sequence as argument - viz when $x = ()$ . Our program, however, requires ascending () to be defined as well (one way or the other).

The function filter is a very common one. (I suspect it is in the library, for Richards had omitted its definition.) The first argument is a boolean function that accepts as argu

The value of longest applied to a non-empty list of sequences is a sequence; longer is a boolean function defined on two sequences, and defined provided at least one of its arguments is of finite length. We note that, M being finite, all our sequences are finite. Denoting the length of a sequence by $#$ ,longer $x,y = \left( {# x ≥ # y}\right)$ .

Note that the names subsx and lx have only been introduced for the sake of efficiency; automatic introduction of them requires the mechanized detection of common subexpressions.

This program is very unsophisticated, so much so, as a matter of fact, that I feel that a more elaborate correctness argument would to my taste be wasted. I felt obliged, how ever, to state explicitly the type of all expressions, and of all arguments, and to check that all functions are applied

to arguments of the appropriate type and that the functions are defined for all arguments to which they may be applied.

If quite likely error would be to forget to define "ascending ( )", the more so since its value is irrelevant for $M ≠ \left( \right)$ .

Another likely error is to define erroneously subs $() = \left( \right)$ The list of subsequences of an empty sequence is not the empty list, but a 1-element list containing the empty sequence as its only element. So much for the first solution.

Second solution: Generates only upsequences.

longest (ups M)

\frac {\mathrm {w h e r e}}{\mathrm {u p s}} () = ((.),)

\begin{array}{l} u p s (p: x) = {p: u p x; u p x \gets u p s x; u p x = () | h d u p x z p } + u p s x \ \begin{array}{c} \text {w h e r e} \text {u p s x} = \text {u p s} \text {x} \ \text {x} \end{array} \ \end{array}

Let me add some legenda first. Here list formation is filtered

There are now two ways open to us. One of them is to read the above definition carefully and to say to ourselves yes, ups M is the list of all upsequences of M. That would satisfy me, but for the sake of argument we shall pursue the second path and remember our first solution. Because longest is a function and our first solution is correct, so is our second one provided we can prove

(0) ups $M =$ filter ascending (subs $M$ )

Let us try. We first investigate the case $M = ()$

\begin{array}{l} f i l t e r a s c e n d i n g (s u b s ()) \ = {\mathrm {d e p . o f s u b s} } \ f i t h e r a s c e n d i n g ((\cdot),) \ = {\text {d e f . o f} f i l t e r } \ \mathrm {a s c e n d i n g () \rightarrow () : f i l t e r a s c e n d i n g () ;} \ f i l t e r a s c e n d i n g () \ \end{array}

\begin{array}{l} = {\mathrm {a s c e n d i n g} () = \mathrm {t r u e} } \ (,) \colon f i l t e r ^ {\prime} a s c e n d i n g () \ = {\mathrm {d e f i n i t i o n o f f i l l e r} } \ () \vdots () \ = {a: () = (a, }) } \ ((\cdot), \cdot) \ \end{array}

Note. I believe that SASL does

not require the outer parentheses.

Aside. I am not so certain I like SASL's special notation " $x,{}^{\prime \prime }$ for the one-element list containing only $x$ . (End of

Now the case $M = p$ : for the sake of brevity we shall eliminate the identifiers $\operatorname{sub}x$ and $\operatorname{up}x$ .

\begin{array}{l} f i l t e r a s c e n d i n g (s u b s (p: x)) \ = {\mathrm {d e f . o f s u b s} } \ \mathrm {f i t h e r a s c e n d i n g} ({p: \mathrm {s u b x}; \mathrm {s u b x} \gets \mathrm {s u b s} x } + + \mathrm {s u b s} x) \ = {\mathrm {l e m m a} 0 \mathrm {a b o u t f i l t e r} } \ f i l t e r a s c e n d i n g {p: s u b x; s u b x \gets s u b s x } \ + + \mathrm {p i l t e r} \mathrm {a s c e n d i n g (s u b s} x) \ = {\mathrm {l e m m a} 1 \mathrm {a b o u t f i l t e r a n d l i s t f o r m a t i o n} } \ {p: \mathrm {s u b} x; \mathrm {s u b} x \gets \mathrm {s u b s} x; \mathrm {a s c e n d i n g} (p: \mathrm {s u b} x) } \ + + \mathrm {f i l t e r a s c e n d i n g (s u b s} x) \ = {\mathrm {d e f i n i t i o n o f a s c e n d i n g} } \ {p: \mathrm {s u b x}: \mathrm {s u b x} \gets \mathrm {s u b s} x; \mathrm {s u b x} = () | (p ≤ h d \mathrm {s u b x} ∧ a s c e n d i n g \mathrm {s u b x}) } \ + + f i l t e r a c c e n d i n g (s u b s x) \ = {b e c a u s e a s c e n d i n g (\cdot) = t r u e } \ {p: \mathrm {s u b x}: \mathrm {s u b x} \gets \mathrm {s u b s} \times ; (\mathrm {s u b x} = () | p ≤ h d \mathrm {s u b x}) ∧ \mathrm {a s c e n d i n g s u b x} } \ + + \mathrm {f i l t e r a s c e n d i n g (s u b s} x) \ = {\mathrm {l e m m a} 2 \mathrm {a b o u t f i l t e r a n d l i s t f o r m a t i o n} } \ {p; \operatorname {s u b x}: \operatorname {s u b x} \gets f i l t e r a s c e n d i n g (\operatorname {s u b s} x); \operatorname {s u b x} = () | p s h d \operatorname {s u b x} } \ + + f i l t e r a s c e n d i n g (s u b s x) \ \end{array}

\begin{array}{l} \mathrm {L e m m a 0 :} \mathrm {F i l t e r c (A + + B)} = \mathrm {F i l t e r c A} + + \mathrm {F i l t e r c B} \ \mathrm {L e m m a 1 :} \mathrm {f i l t e r} c {f x; x \gets y ^ {\prime} } = {f x; x \gets y ^ {\prime}; c (f x) } \ \mathrm {L e m m a 2 :} {f x; x \gets y; b (f x) \wedge c x } = \ {f x; x \gets f i t h e r c y; b (f x) } \ \end{array}

Realizing that $\operatorname{subx}$ is a dummy we see that

Third solution: For each element of $M$ ,generates only the longest upsequence beginning with that component.

longest (up's M)

where

\begin{array}{l} \overline {{u p s ^ {\prime}}} () = ((:) _ {0}) \ u p s ^ {\prime} (p: x) = (p: \mathrm {l o n g e s t} {u p; u p \gets u p x; u p = () | h d u p ≥ p }): u p x \ \frac {\mathrm {w h e r e}}{x} \mathrm {u p x} = \frac {\mathrm {u p s ^ {\prime}}}{} x \ \end{array}

*

This time further legenda are not necessary. It is undoubt- edly possible to derive the third solution from the second one in very much the same way as we have derived the second solution from the first one. This time we would have to ex- ploit the properties of longest such as

\mathrm {l o n g e s t} (A + B) = \mathrm {l o n g e s t} ((\mathrm {l o n g e s t} A): B)

and

\mathrm {l o n g e s t} {p: u p; \dots } = p: \mathrm {l o n g e s t} {u p; \dots }

I shall not do it, nor prove above properties of longest since I don't expect the exercise to be instructive.

We note that inventing new identifiers has become a burden for the author: he reuses upx in a meaning very different from the one it had in the second solution.

The number of subsequences to be investigated has been reduced drastically: from $2^{N}$ in the first solution, via $N^{2}$ in the second solution to $N$ in the third one.

I find it hard to estimate the third solution's time complexity. My guess is that longest will in general be invoked order $N^2$ times , and that the algorithm is there. fore of order $N^3$ . The nature of longest is such that I see very little gain from lazy evaluation. (For lock of experience and knowledge above estimations are hardly "educated guesses".)

*

Fourth solution: Restricts exploration to those upsequences that are not included in longer upsequences.

longsf (up's M) where

\begin{array}{l} u p s ^ {\prime \prime} () = ((:) _ {2}) \ u p s ^ {\prime \prime} (p; x) = (p; \mathrm {l o n g s i f t} {u p; u p \gets u p x; u p = () | h d u p ≥ p 3): u p x \ l o n g s i f t = l o n g e s t \cdot s i f t \ s i f A = s i f F ^ {\prime} \mathrm {P o s I n f} \ \mathrm {s i f} _ {1} ^ {\prime} \min () = ((),) \ \begin{array}{r l}{\mathrm {s i f f} ^ {\prime} \min (a; x)}&{= a = () \rightarrow \mathrm {s i f f} ^ {\prime} \min x;}\&{p ≥ \min a, \rightarrow \mathrm {s i f f} ^ {\prime} \min x}\end{array} \ a: s i f t ^ {\prime} p x \ \mathrm {w h e r e} (p: r) = a \ \end{array}

￥

Legenda: the - in the definition of longsift denotes func- tional composition, which needs to be indicated explicitly because in SASL functional application is defined to be left-associative. The name longsift could have been avoided at the price of another parenthesis pair

(p: \mathrm {l o n g e s t} (\mathrm {s i f t} {u p; u p \gets u p x; u p = () | h d u p ≥ p })

and similarly in the first line.

The whole purpose of the introduction of shift is to reduce the number of (expensive) invocations of longest. One has to prove that

longest ${up;up\gets upx;\dots } =$ longest(sift ${up;up\gets upx;\dots }$ 1 but now we are reaching the stage of the coding trick since now we have to take into account the order in which the sequences occur in upx plus the fact that the list forma- tion with the braces is -contrary to what the braces from set notation suggest! - order-preserving. Process sift drops those sequences of which it can cheaply be established that they are not a longest upsequence from the set considered, viz. by comparing their first elements with the minimum element of $M$ "to their left and encountered so far". (I refer the interested reader to EWD824 , of which Richards was unaware.)

才

For the sake of completeness I mention that Mark Scheevel and Bill Kelley have written SASL programs for a longest upsequence and the maximum upsequence length, probably the first and certainly the latter being of order ${N}^{2}$ -and not of order $N \cdot \log N$ since the binary search of the imper- ative program had to be replaced by a linear one. They used foldl

[\text{fold} \mid \operatorname{op} \mid r\text{.}]

which is nothing but the SASL coding of a for- statement

maxup M

where

maxup = length $\cdot$ maxupsequence

maxupsequence = foldl add ()

add () $n = n$ ;( )

add (m:mm) n = n > m → n: m: mm;

trickle m mm

where

trickle mk (mk1 : mm) = n ≥ mk1 → n: mk1: mm

mk : trickle mk1 mm

trickle ${mk}\left( \right) = n : \left( \right)$

maxupsequence generates a list of the k "best" upsequence heads; the best ith upsequence is the upsequence of length i with the smallest head.

I was pleased to see their use of : () instead of the comma to construct a singleton list. Note, however, their reuse of the identifier mm .

From all the above, pg. EWD825-3 in particular left me with very mixed feelings. On the one hand I had recently learned to appreciate such proofs that consist of a chain of simple manipulations, on the other hand I knew I was disgusted. Why?

There is something profoundly wrong with the cost/performance ratio. You see, while I have recently used a similar style for very concise proofs of surprising theorems, this time the theorem was obvious to start with, a circumstance that makes the whole exercise insipid.

Besides that, Lemma 2 made me suspicious: it is just a Funny way of rewriting the well-known formula

[ Q \wedge (\underline {{E}} _ {i}: P _ {i}) = (\underline {{E}} _ {i}: Q \wedge P _ {i}) ]

From predicate calculus.

Furthermore there is a whole class of functions $f$

f: bag of elements $\rightarrow$ element

with the property $f\left( {{B}{0} \oplus {B}{1}}\right) = f\left( {{f}{B}{0}{0} \oplus {f}{B}{1}{1}}\right)$ ,and it hurts to have to write this down in the very special form

\mathrm {l o n g e s t} (A + B) = \mathrm {l o n g e s t} (\mathrm {l o n g e s t} A + \mathrm {l o n g e s t} B)

It has most definitely nothing to do with the concatenation

The set $A$ of all subsequences of $M$ is defined by

(A x :) x in A = x is subsequence of M)

With subs as defined on pg. EWD825-0, we can prove that $\mathit{sub}M$ represents a particular listing of the elements of $A$ ; it is probably a mistake to take $\mathit{sub}M$ as $A$ 's definition and to derive all relevant properties of $A$ from the way in which $\mathit{sub}$ has been defined. My manipulations on pg. EWD825-3 are very close to program development by transforations, a technique that seems to invite making that mistake.

Burroughs Corporation 12201 Technology Blvd AUSTIN, Texas 78759 U.S.A.

31 May 1982 prop. dr. Edsger W. Dyrkstra Burroughs Research Fellow