D.A. Turner's reply.
In reply to EWD759, D.A. Turner sent me the following proof by returning mail.
“Thank you for your “somewhat open letter”, which arrived yesterday. You pose several task —the order in which I have decided to tackle them is to establish first the precise formal relationship between f and g.
First some notation. I shall call the elements of a list f , f_{0} f_{1} f_{2} etc. and I shall use the notation
[h(i)]^{B}_{i=A} |
Now I define a function “upto”
upto i f = least j ≥ 0 such that f_{j} > i | (upto.0) |
g = [upto i f ] ^{∞} _{i=0} | (Theorem 1) |
a > i ⊢ upto i (a:f ) = 0 | (upto.1) | |
a ≤ i ⊢ upto i (a:f ) = 1 + upto i f | (upto.2) |
We have also your definition of the function “k”
p ≤ y ⊢ k x y (p:q) = k (x+1) y q | (k.1) | |
p > y ⊢ k x y (p:q) = x : k x (y+1)(p:q) | (k.2) |
From these four propositions we shall deduce the following generalization of Theorem 1.
Theorem 0. k x y f = [x + upto i f ] ^{∞} _{i=y}
Proof by structural induction on f, which is an infinite list of integers.
case Ω_{L} (Note — we need to distinguish between Ω_{L}, the undefined element in the space to which f belongs, and Ω_{I}, the undefined integer. The relationship between them is Ω_{L} = [Ω_{I}] ^{∞} _{i=0} )
k x y Ω_{L} = Ω_{L} from k.1, k.2 by case exhaustion |
[x + upto i Ω_{L}] ^{∞} _{i=y} | |||||
= [x + Ω_{I}] ^{∞} _{i=y} | from upto.1, upto.2 | ||||
= [Ω_{I}] ^{∞} _{i=y} | properties of Ω | ||||
= Ω_{L} | as required |
case p:f
k x y ( p:f ) | |||
= [x]^{p−y} ++ k x p ( p:f ) | by repeated appl. of k.2 | ||
= [x]^{p−y} ++ k (x+1) p f ) | by k.1 | ||
= [x]^{p−y} ++ [(x+1) + upto i f ] ^{∞} _{i=p} | ex hyp. | ||
= [x]^{p−y} ++ [x + (1 + upto i f )] ^{∞} _{i=p} | properties of + | ||
= [x]^{p−y} ++ [x + upto i (p:f ))] ^{∞} _{i=p} | by upto.2 | ||
= [x + upto i (p:f ))] ^{∞} _{i=y} | by upto.1 and rearranging |
QED Theorem 0.
Whence, since g = k 0 0 f, we have immediatly
Theorem 1 g = [upto i f ] ^{∞} _{i=0}
Also you asked me to establish that g is A) ascending and B) unbounded, given appropriate assumptions about f. This now follows easily from the above. (Relaxing the level of formality somewhat) we have:
A) from upto.0 it follows (by transitivity of “>” that “upto i f " is an ascending function of i. Therefore, whatever the nature of f, g is ascending.
B) Let us define “f is unbounded” to mean, “for any N≥0, there is a j ≥0 such that f_{j} > N. Assume f is unbounded (f ascending not relevant. Then, from upto.0,
upto i f is defined for all i ≥0 |
* *
*
I am slightly uneasy in “case Ω_{L}” —particularly after the parenthetical remark explaining the difference between Ω_{L} and Ω_{I}— about the justification “from k.1, k.2 by case exhaustion”. My uneasyness is certainly caused by lack of familiarity how to deal with Ω. Take
funny (p:q) = | if p≥10 → 1: funny q | ||
⫿ p<10 → 1: funny q | |||
fi |
Is funny Ω_{L} = Ω_{L}? Or is funny Ω_{L} = ones (with ones = 1: ones)? I expect the first answer though I would prefer the second one, if I am giving full weight to the remark in [1], page 37).
The first point to be made is that in reasoning about SASL programs, Ω can be treated just like any other value as regards being substitutable in equationsPerhaps I have failed to fathom the complete depth of the constrained “as regards being substitutable in equations”.
The correspondence was triggered by remarks in [1] such as the recommendation of applicative programming (pg 14):
The proofs (like the programs themselves) are very much shorter than the proofs of the corresponding imperative programs.I had my doubts, which have not been dispelled by the comparison of Turner’s proof with the one given in EWD758.
[1] Turner, D.A. “Program Proving and Applicative Languages”, August 1980
Plantaanstraat 5 | 27 December 1980 |
5671 AL NUENEN | prof. dr. Edsger W. Dijkstra |
The Netherlands | Burroughs Research Fellow |
Transcribed by Martin P.M. van der Burgt
Last revision