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