3 ms·
Similar to how lambda calculus "just is" (and it's very elegant and useful for math proofs), but nobody writes non-trivial programs in it...
by bbkane 7mo ago
Similar to how lambda calculus "just is" (and it's very elegant and useful for math proofs), but nobody writes non-trivial programs in it...
- tromp 7mo agoMake that almost nobody. I wrote a non-trivial lambda program [1] which enumerates proofs in the Calculus of Constructions to demonstrate [2] that BBλ(1850) > Loader's Number. [1] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/loader.lam https://github.com/tromp/AIT/blob/master/fast_growing_and_co... [2] https://codegolf.stackexchange.com/questions/176966/golf-a-number-bigger-than-loaders-number/274634#274634 https://codegolf.stackexchange.com/questions/176966/golf-a-n...