On iteration and recursion

It is customary - I know, in fact, of no other way- to define iteration recursively. But the technique, though as sound as sound can be, has a property that might be very nasty, at least from a methodological point of view. (And if it turns out not to be that nasty, it is at least annoying.)

I can already illustrate what I have in mind with the syntax for natural numbers, for which there are at least three forms:

$\left. { < \text{natural number} > \mathrel{\text{:=}} }\right| <$ natural number $> <$ digit $>$

$<$ natural number $> \because <$ digit $> \left| { < \text{digit} > }\right| <$ natural number $>$

<na>

$\left. { < \text{digit} > }\right| <$ natural number $> <$ natural number $>$

In a way the last syntax is perhaps the most honest. It leads, however, to an ambiguous parsing of all natural numbers of at least 3 digits: it defines parsing as a nondeterministic process. The first two syntaxes represent the two usual ways of resolving that nondeterminacy. The purpose of this note is to explore how much that choice can hurt.

It is quite possible that most of the exploration can, indeed, be carried out in terms of the above example. But, firstly, I am not an expert in automatic computer generation, and, secondly, my interest in the question arose in connection with other associative operations than concatenation.

We encounter the same phenomenon with iterated functional composition, with

f ^ {0} x = x, \mathrm {s u p p l e m e n t e d w i t h}

f ^ {n + 1} x = f (f ^ {n} x) o r w i t h

f ^ {n + 1} x = f ^ {n} (f x) \mathrm {o r w i t h}

f ^ {n + m} x = f ^ {n} (f ^ {m} x) \mathrm {a n d} f ^ {1} x = f x.

We also encounter it in programming languages like SAS, in which we can define - with my syntax-

\begin{array}{r l}{\mathrm {c h i p n (a : b)} =}&{\mathrm {i f n = 0 \rightarrow a : b}}\&{\mathrm {i f n > 0 \rightarrow c h i p (n - 1) b}}\&{\mathrm {f i},}\end{array}

\begin{array}{r l}{\mathrm {c h o p} n x}&{= \mathrm {i f} n = 0 \rightarrow x}\&{\mathrm {i f} n > 0 \rightarrow q \mathrm {w h e r e}}\&{\mathrm {p :} q = \mathrm {c h o p} (n - 1) x}\&{\mathrm {f i .}}\end{array}

(For the sake of comparison it would perhaps have been nicer to define chip by the trivially equivalent text

\begin{array}{l} \begin{array}{r l}{\mathrm {c h i p n x}}&{= \mathrm {i f n = 0 \rightarrow x}}\&{\mathrm {I I n > 0 \rightarrow c h i p (n - 1) b w h e r e}}\&{\mathrm {a : b = x}}\end{array} \ \begin{array}{l} \rho_ {i} \ f \end{array} \ \end{array}

Clearly chip and chop are the same functions, and it does not seem unreasonable to require from implementa-

tions that they evaluate chip and chop at the same ex- pense (in terms of time, space, and amount of garbage generated). In this note I intend to explore whether theorems about the one are more easily proved than about the other. (I hope there is no difference, but if there is, we had better know.)

In terms of $t$ - for "tail" they are defined by

c h i p 0 x = x

c h i p (n + 1) x = c h i p n (t | x)

\operatorname {c h o p} O x = x

c h o p ^ {\prime} (n + 1) x = t l (c h o p n x)

\mathrm {L e m m a O A}

c h i p n (t | x) = t | (c h i p n x)

L e m m a o B

\overline {{c h o p n (t l x)}} = t 1 (\overline {{c h o p n x}})

\mathrm {P r o o f} B y \mathrm {i n d u c t i o n}; n = 0 \mathrm {i s o b v i o u s .}

c h i p (n + 1) (+ x)

= {\mathrm {d e f i n i t i o n o p c h i p} }

c h i p n (t | (t | x))

= {\mathrm {i n d u c t i o n h y p o t h e s i s} }

t! (c h i p n (t! x))

= {\mathrm {d e f i n i t i o n o f c h i p} }

t l (c h i p (n + 1) x)

Q E D

\mathrm {P r o o f} B y \mathrm {i n d u c t i o n}; n = 0 \mathrm {i s o b v i o u s}.

c h o p (n + 1) (+ 1 x)

= {\mathrm {d e f i n i t i o n} o f c h o p }

t! (c h o p n (t | x))

= {\mathrm {i n d u c t i o n h y p o t h e s i s} }

t l (t l (c h o p n x))

= {\mathrm {d e f i n i t i o n} o p c h o p }

t! (c h o p (n + 1) x)

Q E D.

I have carried out those two silly proofs side by side for the sake of comparison: they are equally simple.

The awkward thing is that I could not find a proof for chip $n \times =$ chop $n \times$ that was symmetric in chip and chop ! I needed either Lemma O'H or Lemma OB. I was very much annoyed when I found myself forced to treat an obviously symmetric situation asymmetrically.

Let us now look at the proofs of

chip n (twice x) = twice (chip n x) and

with twice $\left( {a;b}\right) = 2 * a$ : twice $b$ ,from which we immediately derive ${t1}\left( {{twice}x}\right) = {twice}\left( {{t1}x}\right)$ . The theorems hold for $n = 0$ ; we only need to compare the induction steps.

chip (n+1) (twice x) chop (n+1) (twice x) = {definition of chip} {definition of chop} chip n (tl (twice x)) tl (chop n (twice x)) = {properly of twice} {induction hypothesis} chip n (twice (tl x)) tl (twice (chop n x)) = {induction hypothesis} {properly of twice} twice (chip n (tl x)) twice (tl (chop n x)) = {definition of chip} {definition of chop} twice (chip (n+1) x) twice (chop (n+1) x) QED.

Again, the two proofs are equally simple. From the above experience I am willing to extrapolate that proofs in terms of chip are as straightforward as those in terms of chop. But now it becomes profoundly annoying that they are different. The cleanest way out is undoubtedly to establish for iterated function application immediately

f (m + n) x = f m (f n x)

and to use that equality in all subsequent proofs. Thus all subsequent arguments about iteration - and we must encounter many of them - are insensitive to the irrelevant

choice whether iteration has been originally defined in the style of chip or in the style of chop . It would then be honest to define

\begin{array}{l} \mathrm {c h o i p} n (a: b) = \ \begin{array}{r l}{\mathrm {i f} n = 0}&{\rightarrow a: b}\{\mathrm {i f} n = 1}&{\rightarrow b}\end{array} \ \begin{array}{r l}{\mathrm {I I} p, q: p > 0 ∧ q > 0 ∧ p + q = n \rightarrow}&\{\mathrm {c h o i p} p (\mathrm {c h o i p} q (a: b))}&\end{array} \ p _ {i} \ \end{array}

where I have taken the liberty of using an "initializing

Plataansstaat 5

5671 AL NUENEN

The Netherlands

14 April 1982

prof. dr. Edsger W. Dgksha

Burroughs Research Fellow