McCarthy’s 91–function: an unfortunate paradigm
EWD845 · 1981–1984 · PDF · Source language: English. · Local OCR-derived source needs manual review.
McCarthy's 91-function: an unfortunate paradigm
McCarthy's 91-function -see below- is an ingenious and at first sight baffling construction, which deserved all the attention it attracted when it became known. Unfortunately it also acquired the status of "difficult testcase" for any proposed theory or set of proof rules for recursively defined functions. This is unfortunate for two reasons. Firstly, this function can be dealt with -see below- by such thoroughly elementary means that it is doubtful whether it is a very good testcase; secondly, its contortions are of such a nature -see below- that any method of dealing with it shows more of those contortions than of the method that is supposed to be illustrated.
McCarthy's 91-function is $g$ ,given by the following recursive definition
$$ g (x) = \inf x > 1 0 0 \rightarrow x - 1 0 ] x \leq 1 0 0 \rightarrow g (g (x + 1 1)) $$
and one is asked to demonstrate that it equals
$$ f (x) = \inf x > 1 0 1 \rightarrow x - 1 0 \quad \mathrm {f o r} x \leq 1 0 1 \rightarrow 9 1 $$
Here we go!
$$ g (x) $$
$$ = {\mathrm {d e f i n i t i o n} g } $$
$$ i f x > 1 0 0 \rightarrow x - 1 0 ] x \leq 1 0 0 \rightarrow g (g (x + 1 1)) f _ {i} $$
$= {$ splitting the first alternative and unfolding once in the second alternative $}$
$$ \begin{array}{l} i f x > 1 0 1 \rightarrow x - 1 0 \ ] x = 1 0 1 \rightarrow 9 1 \ [ ] x \leq 1 0 0 \rightarrow g (i f x + 1 1 > 1 0 0 \rightarrow x + 1 1 - 1 0 \ [ [ x + 1 1 \leqslant 1 0 0 \rightarrow g (g (x + 1 1 + 1 1)) ] _ {i} ] \ \end{array} $$
$$ F C $$
$$ \begin{array}{l} = {\mathrm {s p l i t t i n g o f t h e l a s t a l t e r n a t i v e a n d s i m p l i f i c a t i o n} } \ i f x > 1 0 1 \rightarrow x - 1 0 \ ] x = 1 0 1 \rightarrow 9 1 \ [ 8 9 < x \leqslant 1 0 0 \rightarrow g (x + 1) \ [ x \leq 8 g \rightarrow g ^ {3} (x + 2 2) \ f _ {i} \ = {\mathrm {t e r m i n a t i n g} \mathrm {t a i l - r e c u r s i o n o f t h i r d a l f e r n a t i v e} } \ i f x > 1 0 1 \rightarrow x - 1 0 \ ] x = 1 0 1 \rightarrow 9 1 \ [ 8 g < x \leq 1 0 0 \rightarrow g (1 0 1) \ [ x \leq 8 g \rightarrow g ^ {3} (x + 2 2) \ f _ {i} \ = {\mathrm {c o m b i n a t i o n o f s e c o n d a n d t h i r d a l t e r n a t i v e} \ i f x > 1 0 1 \rightarrow x - 1 0 \ [ 8 9 < x \leq 1 0 1 \rightarrow 9 1 \ [ ] x \leq 8 g \rightarrow g ^ {2 n + 3} (y) \quad \mathrm {f o r s o m e} n \geq 0 \mathrm {a n d} 8 g < y \leq 1 1 1 \ \frac {1}{2} \ = {a p p l y i n g g o n c e i n t h e l a s t a l f e r n a t i v e } \ i f x > 1 0 1 \rightarrow x - 1 0 \ \mathbb {I} 8 9 < x \leq 1 0 1 \rightarrow 9 1 \ | x \leq 8 g \rightarrow g ^ {2 n + 2} (y) \mathrm {f o r s o m e} n \geq 0 \mathrm {a n d} 9 1 \leq y \leq 1 0 1 \ p _ {i} \ = {\mathrm {a p p l y i n g} g \mathrm {a n o t h e r t i m e i n t h e l a s t a l t e r n a t i v e} } \ \end{array} $$
$$ \begin{array}{l} i f x > 1 0 1 \rightarrow x - 1 0 \ [ 8 9 < x \leq 1 0 1 \rightarrow 9 1 \ \mathrm {I I} \times 5 8 9 \rightarrow g ^ {2 n + 1} (g 1) \mathrm {f o r s o m e} n \geq 0 \ p _ {i} \ = {\mathrm {s i n c e} g (g 1) = g 1, \mathrm {t h e l a s t t w o c a n b e c o m b i n e d} } \ i f x > 1 0 1 \rightarrow x - 1 0 \ [ [ x \leq 1 0 1 \rightarrow 9 ] \ f _ {i} \ = {\mathrm {d e f i n i t i o n o f} p } \ f (x) \ \end{array} $$
Q.E.D.
That is all, in a long sequence of minute transformations. It is a winding argument that, of course, can be delivered in 57 varieties, but when you have seen one of them, you have seen them all. The g1-function is, as said, an ingenious construction, but it is an unfortunate paradigm since it leads to demonstrations that are both lengthy and boring.
I hope this is the last technical note in which the 91-function is treated.
Plataanstraat 5
5671 AL NUENEN
The Netherlands
21 December 1983
prof.dr.Edsger W.Dykgsta
Burroughs Research Fellow