Oh dear, I have failed. The whole point of that paper was supposed to be that all this theory stuff actually has practical applications. The same techniques that worked on that toy problem can be used on real problems and produce similar results.
I did some follow-up work after that paper to implement binary arithmetic in the lambda calculus, and using that, of course, you can compute "real" factorials. Here it is computing the factorial of 100 in under a second:
? (time (pbn (bn_fact (bn 100))))
(PBN (BN_FACT (BN 100)))
took 942,269 microseconds (0.942269 seconds) to run.
64,791 microseconds (0.064791 seconds, 6.88%) of which was spent in GC.
During that period, and with 4 available CPU cores,
878,343 microseconds (0.878343 seconds) were spent in user mode
111,475 microseconds (0.111475 seconds) were spent in system mode
759,285,088 bytes of memory allocated.
504 minor page faults, 0 major page faults, 0 swaps.
93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000
((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
(λ f
(λ n
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n)
(λ dummy ((λ (l r s) (s l r)) (λ (_t e) _t) (λ s (λ (_t e) _t))))
(λ dummy
(((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
(λ f
(λ (n1 n2 r)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n1) (λ dummy r)
(λ dummy
(f
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ s (λ (_t e) _t))) (λ dummy ((λ p (p (λ (l r) r))) l)))
(λ x x))))
n1)
((λ (l r s) (s l r)) (λ (_t e) e) n2)
(((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n1)
(((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
(λ f
(λ (n1 n2 c)
(λ nil
(((λ (c _t e) (c _t e))
((λ (p q) (p q (λ (_t e) e))) ((λ p (p (λ (l r) (λ (_t e) e)))) n1)
((λ p (p (λ (l r) (λ (_t e) e)))) n2))
(λ dummy
(c ((λ (l r s) (s l r)) (λ (_t e) _t) (λ s (λ (_t e) _t)))
(λ s (λ (_t e) _t))))
(λ dummy
((λ (l r s) (s l r))
((λ (b1 b2 c)
(b1 (b2 c ((λ c (c (λ (_t e) e) (λ (_t e) _t))) c))
(b2 ((λ c (c (λ (_t e) e) (λ (_t e) _t))) c) c)))
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n1)
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n2)
c)
(f
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ s (λ (_t e) _t)))
(λ dummy ((λ p (p (λ (l r) r))) l)))
(λ x x))))
n1)
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ s (λ (_t e) _t)))
(λ dummy ((λ p (p (λ (l r) r))) l)))
(λ x x))))
n2)
((λ (b1 b2 c) (b1 (b2 (λ (_t e) _t) c) (b2 c (λ (_t e) e))))
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e))
(λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n1)
((λ (l)
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
(λ dummy (λ (_t e) e))
(λ dummy ((λ p (p (λ (l r) l))) l)))
(λ x x))))
n2)
c)))))
(λ x x))))))
n2 r (λ (_t e) e))
r))))
(λ x x))))))
n
(f
(((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
(λ f
(λ n
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n) (λ dummy n)
(λ dummy
(λ nil
(((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) l))) n)
(λ dummy
(((λ p (p (λ (l r) (λ (_t e) e)))) ((λ p (p (λ (l r) r))) n))
(λ s (λ (_t e) _t))
((λ (l r s) (s l r)) (λ (_t e) e) ((λ p (p (λ (l r) r))) n))))
(λ dummy ((λ (l r s) (s l r)) (λ (_t e) _t) (f ((λ p (p (λ (l r) r))) n)))))
(λ x x)))))
(λ x x))))))
n))
(λ s (λ (_t e) _t)))))
(λ x x))))))"