[eobxszpt] Conway chained arrow notation

There are only a few interesting and practically computably numbers expressible in Conway chained arrow notation. Here are the results, in increasing size, of an exhaustive enumeration of chain lengths 3 and 4, with chain elements between 1 and 5:

2->3->2
3->2->2
4->2->2
5->2->2
2->3->3
2->4->2
3->2->3 = 3->3->2
4->3->2
5->3->2
2->5->2
There are no interesting chains of length 4 that are computable.

All other chains exhausted 100 seconds of CPU time or 1 GB of RAM, whichever was exhausted first. 3->3->3 is an example of a chain which exhausts CPU time before RAM.

The uninteresting cases are
1 -> X = 1
X -> 1 = X
p -> 1 -> X = p
p -> q -> 1 -> X = p^q
2 -> 2 -> X = 4
where X is a chain and p and q are numbers.

3->4->2 is within the realm of imagination to calculate someday.  The first few digits are 1258014290... and the last digits are ...6100739387, and in total 3,638,334,640,025 digits long.

Just for the fun audacity of saying it: Note that all numbers compactly expressible in chained arrow notation are actually quite small, as numbers go.  Infinity is a long ways off.

This Haskell implementation manipulates chains in reverse as lists, since the recursion happens at the end of the chain (front of the list). However, we do occasionally need to look at the front of the chain (end of the list), for example for the 2 -> 2 -> X optimization.

module Main where { import Control.Exception (assert); import System.Environment (getArgs) ; import Data.List (intersperse) ; data Element = N Integer | Internal Chain deriving (Show); {- The chain is stored in reverse. The head of the list is the last element of the chain. -} type Chain = [Element] ; {-| Do one simplification. -} simplify :: Chain -> Chain ; simplify c = case (optimize c) of { Just result -> result ; _ -> case c of { [] -> error "empty chain" ; [N _] -> c ; [(N x) , (N y)] -> [N (y ^ x)] ; (N 1) : rest -> rest ; (N _) : (N 1) : _rest -> error "should have been simplified by internal_1" {- rest -} ; (N q) : (N p) : x -> assert (p > 0 && q > 0) $ (N $ pred q) : (Internal [N q, N $ pred p, maybe_internal x]) : x ; _ -> do_first (not . isN) eval_internal c ; } } ; isN :: Element -> Bool ; isN (N _) = True ; isN (Internal _) = False ; {-| avoid unnecessary parentheses -} maybe_internal :: Chain -> Element ; maybe_internal [N i] = N i ; maybe_internal c = Internal c ; eval_internal :: Element -> Element ; eval_internal c = case c of { Internal [(N i)] -> N i ; Internal x -> maybe_internal $ simplify x ; N _ -> error "should not be N" } ; {- | apply f to the first element which satisfies p -} do_first :: (a -> Bool) -> (a -> a) -> [a] -> [a] ; do_first _ _ [] = [] ; do_first p f (h : t) = if (p h) then (f h) : t else h : (do_first p f t) ; showelem :: Element -> String ; showelem (N i) = show i ; showelem (Internal c) = "(" ++ show_chain c ++ ")" ; show_chain :: Chain -> String ; show_chain = concat . intersperse " -> " . map showelem . reverse ; print_chain :: Chain -> IO () ; print_chain = putStrLn . show_chain ; step_by_step :: Chain -> IO () ; step_by_step c = case c of {[N _] -> print_chain c ; _ -> print_chain c >> (step_by_step $ simplify c) } ; {- Optimizations for looking at the front or middle of the chain -} optimize :: Chain -> Maybe Chain ; optimize c = case (reverse c) of { (N 2) : (N 2) : _ -> Just [N 4] ; (N 1) : _ -> Just [N 1] ; _ -> internal_1 c } ; {- search for an internal 1 because X -> 1 -> Y = X. -} internal_1 :: Chain -> Maybe Chain ; internal_1 c = case c of { [] -> Nothing ; (N 1) : rest -> Just rest ; _ : rest -> internal_1 rest} ; read_chain :: [String] -> Chain ; read_chain = map N . reverse . map read; full_simplify :: Chain -> Integer ; full_simplify c = case c of { [N i] -> i ; _ -> full_simplify $ simplify c } ; main :: IO () ; main = do { args <- getArgs ; case args of { "show" : rest -> step_by_step $ read_chain rest ; _ -> print $ full_simplify $ read_chain args } } }