nokolisp VS AIT

Code: https://github.com/timonoko/nokolisp

My "compiler" was totally context-free and made in assembler. Which means that it compiles every instruction in complete vacuum and assumes stuff comes in AX and BX registers (with rest-pointer in CX, I think). And result in AX.

But this proved not to be a bad start at all. Once you understand the limitations of the "compiler", you can modify the macros accordingly. One of the feature of the compiler was that it assigned absolute memory places for variables, so you could stop wasting stack and do early assignments to temporary variables.

Unfortunately the source is quite incomprehensible now because of insane use of nested macros: https://github.com/timonoko/nokolisp

But the example given above works, no doubt about it:

    > (setq test (ncompile '(cons 1 (cons 2 3))))

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...