Hamming’s exercise in SASL

Hamming's exercise in SASL.

In a slightly simplified version, the problem is to generate in increasing order "all positive integers that have no other prime factors than 2 and 3 . The solution 'a la SAsL that was designed by J.L.A. van de Sneepscheut was essentially the following:

def times n (a:b) = n*a : times n b ;

\begin{array}{l} i f a 0 < a 1 \rightarrow a 0: m e r g e b 0 (a 1: b 1) \ [ ] a 0 = a 1 \rightarrow a 1: m e r g e b 0 b 1 \ \lim _ {a \to a _ {1}} a > a _ {1} \rightarrow a _ {1}: \mathrm {m e r g e} (a _ {0}: b _ {0}) b _ {1} \ f _ {i}: x = 1: \mathrm {m e r g e} (\mathrm {t i m e s} 2 x) (\mathrm {t i m e s} \ \end{array}

(0)

This note records how -at the present state of my art- I prove the correctness of this program.

I need a notation for the $n$ -th element of a continued concatenation:

\begin{array}{r l}{\mathrm {s u b n (a ; b)} =}&{\underset {f} {\mathrm {i f}} n = 0 \rightarrow a}\&{\underset {f} {\mathrm {i f}} n > 0 \rightarrow \mathrm {s u b (n - 1)} b}\&{\underset {f} {\mathrm {i f}}}\end{array}

I need it in order to be able to express a simple

EWD792 - 1

theorem about the function dist which - remember the low binding power of the concatenation as indicated by the colon- is given by

[\text{dist}f\left( {a;b}\right) = {pa} : \text{dist}f\left( b\right) .]

Theorem 0:

(\underline {{A}} n: n ≥ 0: \mathrm {s u b} n (\mathrm {d i s t} f x) = f (\mathrm {s u b} n x))

Proof of Theorem 0. By mathematical induction (by what else?)

Case $n = 0$ :

\begin{array}{l} \mathrm {s u b} 0 (\mathrm {d i s t} f (a; b)) = \ \mathrm {s u b o} (f a: \mathrm {d i s t} f b) = \ f a = \ f (s u b 0 (a; b)) \ \end{array}

Case $n > 0$ :

\mathrm {s u b n} (\mathrm {d i s t} f (a; b)) =

s u b n (f a: d i s t f b) =

\begin{array}{l} \operatorname {s u b} (n - 1) (\operatorname {d i s t} f ^ {\prime} b) = \ f (s u b (n - 1) b) = \ \end{array}

f (s u b n (a; b))

(End of Proof of Theorem 0).

I think Theorem 0 so trivial that most people are willing to apply it without bothering to think about its proof. It should be formulated and proved once.

EWD7g2-2

Let min s be the smallest element from a set s of natural numbers. For an infinite set s we define the continued concatenation sort s by

\operatorname {s o r t} s = \min s: \operatorname {s o r t} (s - {\min s })

In terms of the set formater U we have to prove that in (0)

x = \operatorname {s o r t} \left(\bigcup n 2, n 3: n 2 ≥ 0, n 3 ≥ 0; 2 ^ {n 2} \cdot 3 ^ {n 3}\right) \tag {1}

To do so, we first prove about merge

Theorem 1. For two infinite sets so and s1 of natural numbers - the union of which we denote by s0+s1 - we have

m e r g e (\operatorname {s o r t} s 0) (\operatorname {s o r t} s 1) = \operatorname {s o r t} (s 0 + s 1)

Proof of Theorem 1 The theorem to be proved is of the

where $p$ and $q$ are functions of $p$ of natural numbers; their values be

$\left( {\underline{A}n : n ≥ 0 : \left( {\underline{A}so{s1}\because \text{sub}n\left( {pso{s1}}\right) = \text{sub}n\left( {qso{s1}}\right) }\right) }\right)$ and this is proved using mathematical induction over $n$ . The proof is straightforward and left to the reader. (End of Proof of Theorem 1.)

EWD792-3

It is now not difficult to show that $x$ ,as given by (1) satisfies (0).Thanks to Theorem 0 and $p < q ⇒ 2 \cdot p < 2 \cdot q $ we find

\begin{array}{l} t i m e s 2 x = \operatorname {s o r t} (\bigcup n 2, n 3: n 2 ≥ 1, n 3 ≥ 0: 2 ^ {n 2} \cdot 3 ^ {n 3}) \ a n d, s i m i l a r l y, \ \mathrm {f i m e s} 3 x = \mathrm {s c r t} (\bigcup n 2, n 3: n 2 ≥ 0, n 3 ≥ 1: 2 ^ {n 2} \cdot 3 ^ {n 3}) \ a n d t h e n, t h a n k s t o T h e o r e m 1 \ m e r g e (t i m e s 2 x) (d i m e s 3 x) = \ \operatorname {s o r t} (\bigcup n 2, n 3: n 2 ≥ 0 ∧ n 3 ≥ 0 ∧ n 2 + n 3 ≥ 1: 2 ^ {n 2} \cdot 3 ^ {n 3}) \ \mathrm {p r o m w h i c h i m m e d i a t e l y p o l l o w s} \ 1: m e r g e (t i m e s 2 x) (t i m e s 3 x) = x \ \end{array}

In order that program (0) is an effective program I think that we have to prove more. It seems that we have to prove the uniqueness of solution (1).

w i t h ^ {\prime} u n i q d e f i n e d b y

\operatorname {u n i g} n x = (\underline {{A}} i: 0 ≤ i < n: \operatorname {s u b} i x ≠ \omega)

I think we should prove in succession

\begin{array}{l} \mathrm {u n i q} n x ⇒ \mathrm {u n i q} n (\mathrm {t i m e s} m x) \ (\mathrm {u n i q} n y) ∧ (\mathrm {u n i q} n z) ⇒ \mathrm {u n i q} n (\mathrm {m e r g e} y z) \ a n d, f i n a l l y, f r o m t h e l a s t d e f i n i t i o n o f (0) \ u n i q n ^ {j} x ^ {j} ⇒ u n i q (n + 1) ^ {j} x. \ \end{array}

These proofs are very easy, but my current feeling is that we are not allowed to omit them.

(Continued after walking with the dogs.) My choice of identifier "unig" detrays my misunderstanding. Suppose the last definition had been

This - as is easily verified - has one solution, viz.

x = z e r o e s

(with def zeroes = 0 : zeroes). The solution is unique, but I expect no implementation to find it. We fool ourselves when we regard a SASL program just as a set of recursive equations. They are recursive definitions , quite definitely with a direction ! Perhaps it would have been more honest to write the defini-tion

z e r o e s := 0: z e r o e s

Plataonsstraat 5

5671 AL NUENEN

The Netherlands

15 June 1981

prof.dr. Edsger W.Dgksta

Burroughs Research Fellow