# Twice twice twice

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

### Tracing the expansion

A: Consider the following Haskell program.

data Exp = Ap Exp Exp | Twice | F | X pretty :: Exp -> String pretty (Ap e1 e2) = pretty e1 ++ " " ++ pretty2 e2 pretty e = pretty2 e pretty2 :: Exp -> String pretty2 Twice = "twice" pretty2 F = "f" pretty2 X = "x" pretty2 e = "(" ++ pretty e ++ ")" reduce :: Exp -> Maybe Exp reduce (Ap (Ap Twice f) x) = return (Ap f (Ap f x)) reduce (Ap F x) = do x' <- reduce x; return (Ap F x') reduce (Ap g x) = do g' <- reduce g; return (Ap g' x) reduce e = Nothing trace :: (a -> Maybe a) -> a -> [a] trace f x = tr (Just x) where tr Nothing = [] tr (Just x) = x : tr (f x) foo :: Exp foo = Ap (Ap (Ap (Ap Twice Twice) Twice) F) X main = putStr (unlines (map pretty (trace reduce foo)))

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))))