Big (and non-computable) Numbers
scottaaronson.com
scottaaronson.com
It makes me wonder: what is the lambda-calculus equivalent of the busy beaver? Number of normal-order steps before normalization (for a given program size)? Are the LCBB numbers different for different evaluation orders? What metric do you use for program size: depth? Number of lambdas?