5 ms·
One invention that drew me to this topic was Binary Lambda Calculus, invented by John Tromp (“Tromp” as in Tromp-Taylor Rules). It’s just a direct binary encodi
by renonce 2y ago
One invention that drew me to this topic was Binary Lambda Calculus, invented by John Tromp (“Tromp” as in Tromp-Taylor Rules). It’s just a direct binary encoding of a lambda calculus term, but it gives you a concrete and concise representation which is useful for evaluating the complexity of an expression. I encountered it when viewing https://codegolf.stackexchange.com/questions/6430/shortest-terminating-program-whose-output-size-exceeds-grahams-number https://codegolf.stackexchange.com/questions/6430/shortest-t... and found that this language was the one that could write the most precise representation of a very large number with the fewest bits possible. I later learned that Graham’s number could be encoded in 120 bits (maybe 3~4 less), much more concise than equivalent mathematical language, and I’ve since been drawn into the field of googology. It was fascinating.
- tromp 2y agoThat Stack Exchange thread shows you can exceed Graham's number with the 49 bit lambda term (λ 1 1) (λ 1 (1 (λ λ 1 2 (λ λ 2 (2 1))))), or graphically ┬─┬ ┬─┬────────── └─┤ │ │ ──┬────── │ │ │ ┬─┼────── │ │ │ └─┤ ┬─┬── │ │ │ │ ┼─┼─┬ │ │ │ │ │ ├─┘ │ │ │ │ ├─┘ │ │ │ ├─┘ │ │ ├───┘ │ ├─┘ └─┘ Related: https://oeis.org/A333479 https://oeis.org/A333479
- renonce 2y agoYeah but it’s not representing a known number - I would rather say it is a proof that the busy beaver function for BLC at 49 bits is higher than Graham’s number. The fact that it represents known numbers concisely is more interesting to me.
- tromp 2y agoThen you'll be more interested in the 114 bit representation (λ (λ 2 1 (λ 1 (λ λ 1 2 (λ 1)) (λ λ 5 (2 1)) 3) 1) (λ λ 2 (3 2 1))) (λ λ 2 (2 (2 1))) of Graham's number [1]. [1] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/graham.lam https://github.com/tromp/AIT/blob/master/fast_growing_and_co...