# Twice twice twice

Q: What does the function twice twice twice do?

## Contents

### 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 `f16 x`.

### Any number of twices

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 `f2↑↑n x`, where `2↑↑n` is Knuth's hyperpower notation, equal to 2 to the 2 to the ... to the 2, with 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)
(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))))
```