lambda-8cc VS AIT

ycombinator siding with the Amazonian cult of the carcinisation?! blasphemy! this submission is like a wanted poster for react-use-lambda to be summoned into existence from the great beyond https://github.com/woodrush/lambda-8cc

It is not what you want exactly, but there is a x86 C Compiler written in lambda-calculus, it has a pretty detailed "How it was done" in details.md - maybe you will find it interesting.

That said, I'm not sure where is the actual compiler implementation, files in src/ seem to be various tools: https://github.com/woodrush/lambda-8cc/tree/main/src

It is described in https://github.com/tromp/AIT/blob/master/fast_growing_and_co...

A = λxλyλz. x z (y (λ_.z)), which is encoded as bit 0 (left branch), while bit 1 (right branch) encodes prefix application.

[1] https://github.com/tromp/AIT/blob/master/ait/allA.lam

I expect so, as the author is familiar with my tools [1] for doing these optimizations.

[1] https://github.com/tromp/AIT

Haskell is not far from being a layer of syntactic sugar on top of the lambda calculus.

For an example of a non-trivial program, see this binary lambda calculus self-interpreter: https://github.com/tromp/AIT/blob/master/uni.lam

While Goodstein sequences do get really long quite fast, they're not that easy to code. This [1] binary lambda calculus program may be the shortest possible, but still takes 351 bits. Meanwhile, in a mere 215 bits, we can encode a Laver table [2] program that potentially grows so much faster than Goodstein, that it's not even provable in ZFC [3].

[1] https://github.com/tromp/AIT/blob/master/goodstein.lam

[2] https://github.com/tromp/AIT/blob/master/laver.lam

[3] https://codegolf.stackexchange.com/questions/79620/laver-tab...