3 ms·
Is the 18506 pages long lambda term the normal form? I wonder how much that can be minimized by not beta reducing everything.
by atennapel 4y ago
Is the 18506 pages long lambda term the normal form? I wonder how much that can be minimized by not beta reducing everything.
- tromp 4y agoNo; the term has no normal form. It contains a lot of applications of the fix-point combinator Y. As a simpler example, here's a lambda term for reversing input: λ 1 ((λ 1 1) (λ λ λ λ 2 (4 4) (λ 1 4 2))) (λ λ 1) which similarly has no normal form.
- atennapel 4y agoAh yes, that makes sense. But is that PDF really the most minimal form? I can imagine if we write a program using lets: let nil = \n c. n; let cons = \hd tl n c. c hd tl; let map = ...; body And compile it as: (\nil cons map. body) (\n c. n) (\hd tl n c. c hd tl) (...) That we would get a more minimal form. But I cannot verify in what form the lambda expression in the PDF is. It just seems unbelievably large to me.
- tromp 4y agoYes, let bindings would get translated like that, but there would be some straightforward optimizations done, such as size-reducing beta-reductions, which strip out unused let bindings, and inline the single-use ones, as well as the multi-use ones whose definition is smaller than the unary encoded de-Bruijn index.
- atennapel 4y agoYes, I wonder if these optimizations are done in the PDF. I found the BLC encoding of the lambda expressions which is 407171813 bits, about 5 mb.
- tromp 4y agoI expect so, as the author is familiar with my tools [1] for doing these optimizations. [1] https://github.com/tromp/AIT https://github.com/tromp/AIT
- tromp 4y agoIndeed he uses it here [1], which also gets used in lambda-8cc. [1] https://github.com/woodrush/lambda-calculus-devkit https://github.com/woodrush/lambda-calculus-devkit