A somewhat open letter to D.A.Turner

EWD759 · 1979–1981 · PDF · source transcription · Source language: English.

A somewhat open letter to D.A. Turner.

Dear David,

I read with considerable interest your "Program Proving and Applicative Languages", but when I tried to apply your techniques to the first slightly more ambitious example my assistant W.H.J. Feijen came up with, it turned out to be a very humbling experience: I clearly lacked the knack of dealing with SASL programs.

Consider the following short SASL definitions (my syntax! I trust you will forgive me that)

def k x y (p : q) =
if p ≤ y → k (x + 1) y q ⌷ p > y → x : k x (y + 1) (p : q)
fi ;

def g = k 0 0 f

Here f is supposed to be ascending, i.e. to satisfy (P₀ f ) with

P₀ (a : b : c) = a ≤ b ∧ P₀ (b : c)

and unbounded, i.e. to satisfy (Ay : y ≥ 0: P₁ y f ) with

P₁ y (p : q) = p > y ∨ (P₁ y q).

When f is ascending and unbounded, it is clearly an infinite list. (I try to use the more positive term "continued concatenation" for that, but that is another story.)

You would do me a great service by showing me a proof that when f is ascending and unbounded, g is ascending and unbounded.

The precise formal relation between g and f is that for all y ≥ 0

sub y g = (N x : x ≥ 0 : y ≥ (sub x f ))

(0)

where sub is defined by

def sub n (p : q) =
if n = 0 → p ⌷ n > 0 → sub (n−1) q fi

and the (N ... ) should be read as: the number of distinct values x in the range x ≥ 0 such that y ≥ (sub x f). You would do me a great service by showing me as well, how you would prove (0). I am looking forward to your reply.

With my greetings and best wishes,

Yours ever

Edsger

5 November 1980