undefined | Better HN

0 pointsatennapel3y ago0 comments

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

0 comments

3 comments · 1 top-level

tromp3y ago· 2 in thread

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

atennapelOP3y ago

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

tromp3y ago

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

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

1 more reply

j / k navigate · click thread line to collapse