# Twice twice twice

**Q: What does the function twice twice twice do?**

### Tracing the expansion

A: Consider the following Haskell program.

dataExp=ApExpExp|Twice|F|Xpretty::Exp→Stringpretty(Ape_{1}e_{2}) =prettye_{1}++ " " ++pretty_{2}e_{2}prettye=pretty_{2}epretty_{2}::Exp→Stringpretty_{2}Twice= "twice"pretty_{2}F= "f"pretty_{2}X= "x"pretty_{2}e= "(" ++prettye++ ")"reduce::Exp→MaybeExpreduce(Ap(ApTwicef)x) =return(Apf(Apfx))reduce(ApFx) =dox'←reducex;return(ApFx')reduce(Apgx) =dog'←reduceg;return(Apg'x)reducee=Nothingtrace:: (a→Maybea) →a→ [a]tracefx=tr(Justx)wheretrNothing= []tr(Justx) =x:tr(fx)foo::Expfoo=Ap(Ap(Ap(ApTwiceTwice)Twice)F)Xmain=putStr(unlines(mappretty(tracereducefoo)))

Its output is as follows.

twice twice twice f x twice (twice twice) f x twice twice (twice twice f) x twice (twice (twice twice f)) x twice (twice twice f) (twice (twice twice f) x) twice twice f (twice twice f (twice (twice twice f) x)) twice (twice f) (twice twice f (twice (twice twice f) x)) twice f (twice f (twice twice f (twice (twice twice f) x))) f (f (twice f (twice twice f (twice (twice twice f) x)))) f (f (f (f (twice twice f (twice (twice twice f) x))))) f (f (f (f (twice (twice f) (twice (twice twice f) x))))) f (f (f (f (twice f (twice f (twice (twice twice f) x)))))) f (f (f (f (f (f (twice f (twice (twice twice f) x))))))) f (f (f (f (f (f (f (f (twice (twice twice f) x)))))))) f (f (f (f (f (f (f (f (twice twice f (twice twice f x))))))))) f (f (f (f (f (f (f (f (twice (twice f) (twice twice f x))))))))) f (f (f (f (f (f (f (f (twice f (twice f (twice twice f x)))))))))) f (f (f (f (f (f (f (f (f (f (twice f (twice twice f x))))))))))) f (f (f (f (f (f (f (f (f (f (f (f (twice twice f x)))))))))))) f (f (f (f (f (f (f (f (f (f (f (f (twice (twice f) x)))))))))))) f (f (f (f (f (f (f (f (f (f (f (f (twice f (twice f x))))))))))))) f (f (f (f (f (f (f (f (f (f (f (f (f (f (twice f x)))))))))))))) f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))

Plainly, therefore, *twice* *twice* *twice* *f* *x* computes

.
*f*^{16} *x*

### Any number of *twice*s

Generalizing, we might ask about the function *twice* *twice* ... *twice* with *n* occurrences of *twice*.
Here's a note that gives a proof that this function, when applied to *f* and *x*, computes

, where *f*^{2↑↑n} *x*`2↑↑`

is Knuth's hyperpower notation, equal to 2 to the 2 to the ... to the 2, with *n**n* occurrences of 2.

### A machine-checked proof

Actually, it's not too difficult to get the Boyer-Moore theorem prover to accept a proof of this result. Because the theorem prover uses a first-order language and *twice* is a higher order function, it's necessary to defunctionalize a bit, choose representations for various functions, and write an *apply* function. The prover also needs some guidance in finding the right inductive arguments. Here is the proof script:

; (apply f x) computes f x (defn apply (fun x) (if (equal fun 'inc) (add1 x) (if (equal fun 'id) x (if (equal fun 'twice) (cons 'twice x) (if (and (listp fun) (equal (car fun) 'twice)) ; (twice . f) represents the partial application twice f ; so (apply (twice . f) x) = f (f x) (apply (cdr fun) (apply (cdr fun) x)) nil))))) ; (funpow f n x) represents f^n x (defn funpow (fun n x) (if (zerop n) x (apply fun (funpow fun (sub1 n) x)))) ; (pow2 n) is 2^n (defn pow2 (n) (if (zerop n) 1 (times 2 (pow2 (sub1 n))))) ; f^1 x = f x (prove-lemma funpow-1 (rewrite) (equal (funpow fun 1 x) (apply fun x)) ((expand (funpow fun 1 x)))) ; f^(a+b) x = f^a (f^b x) (prove-lemma funpow-plus (rewrite) (equal (funpow fun (plus a b) x) (funpow fun a (funpow fun b x)))) (prove-lemma times-2 (rewrite) (equal (times 2 a) (plus a a))) ; This recursive function shows the inductive pattern that must be ; followed in proving the next theorem (defn induct-1 (n fun x) (if (zerop n) t (and (induct-1 (sub1 n) fun x) (induct-1 (sub1 n) fun (funpow fun (pow2 (sub1 n)) x))))) ; twice^n f x = f^(2^n) x (prove-lemma funpow-twice (rewrite) (equal (apply (funpow 'twice n fun) x) (funpow fun (pow2 n) x)) ((induct (induct-1 n fun x)))) ; (tee-n n) is the function T_n = twice twice ... twice (n occurrences) (defn tee-n (n) (if (zerop n) 'id (apply (tee-n (sub1 n)) 'twice))) ; (hyper2 n) is 2^^n a la Knuth (defn hyper2 (n) (if (zerop n) 1 (pow2 (hyper2 (sub1 n))))) ; Another function that guides an inductive proof (defn induct-2 (n fun x) (if (zerop n) t (induct-2 (sub1 n) 'twice fun))) ; T_n f x = f^(2^^n) x (prove-lemma tee-n-hyper (rewrite) (equal (apply (apply (tee-n n) fun) x) (funpow fun (hyper2 n) x)) ((induct (induct-2 n fun x))))