I actually mentioned your hint file in details.md. Quite a roundabout way to decode its secrets!
I too suspect that writing in lambda's native functional style could save a lot of space. Compiling lisp.c from the ELVM repository generates a code much longer than LambdaLisp [1], which empirically shows that well I believe.
As for the pages of PDF, in mathematical terms, since any variable encodes to weight 1, I believe it would be something close to an encoding that degenerates all De Bruijn indices to 1, or in other words, one that only tries to weigh (or gives larger weight to) the complexity of abstraction depths and applications. Since that erases information about the variable I would guess it's not a universal method for weighing lambda sizes.
In this particular case for LambdaVM programs however, since the memory initialization clause nor the instruction clause never increases the maximum De Bruijn index value, I believe both the BLC size and "lambda page size" approximately grows linearly with the number of instructions, so I thought it would serve as an approximately-off-by-a-factor metric for weighing its size.
As for the ELVM lambda calculus back-end, I'll be sending the pull request very soon!
Thank you for taking a look, and many thanks for your constructive comments. I found the BLC language and interpreter to be elegant and that was what brought me here.
I was unaware of the nil-test-free method for Scott-encoded lists. It's true that it would remove a lot of bits from LambdaLisp's implementation. I'll also be using this for future projects. I was also unaware of Melvin Zhang's interpreter. I suspect that result sharing would improve the execution speed. I'll try to add that in one of the supported interpreters in the repository. Thank you very much for thoroughly reading my post and pointing these facts out. It has deepened my understanding and interest for binary lambda calculus.
I also want to say that Lazy K is one of my all-time favorite languages, as I mentioned in the post. It was about 10 years ago when I first found out about Lazy K - at that time I wrote a blog post about a language I made that directly transpiles to Lazy K (written in Japanese). Although at that time I couldn't fully grasp the language, I'm happy that now I could write large programs for Lazy K. I was thrilled to find that the Lazy K language proposal was now published on your website.
The basic tools required for implementing a LC interpreter in LC is demonstrated in LambdaLisp. Although LambdaLisp implements Lisp, the same tools can be used to implement a LC interpreter in LC.
The largest concern in question here may be how I/O is done. I/O can be done by viewing a lambda term as a function that takes a string as an input and outputs a string. Here, a "string" can be expressed as a "list" of "characters", where lists can be encoded using the Scott encoding, and characters can be encoded as a list of bits, and "bits" can be encoded as 0=\x.\y.x, 1=\x.\y.y. This I/O strategy is used in LambdaLisp as well, and is explained in my post in [1].
How Lisp terms are encoded as lambda terms in LambaLisp is explained in [2].
To implement a LC interpreter instead of a Lisp interpreter in LC, it then remains to somehow encode and quote a lambda calculus term into a lambda calculus term. The function described by tromp's reply in this thread, called the Universal Machine, does this - it does so by using an encoding called the binary lambda calculus (BLC) notation for encoding lambda terms into lambda terms. In this notation, an arbitrary lambda term in the usual plaintext notation such as \x.\y.\z.(x y z) can be encoded into a bitstream. The converse is also always possible. The Universal Machine uses the BLC notation for expressing lambda terms, with the same 0/1 bit encoding and list encoding mentioned earlier, and outputs a bitstream (encoded as lambda terms) representing the evaluation result. The BLC notation is described in my post in [3].
Thanks for your feedback, I forgot to mention the execution speed in the post. The number guessing game example (44 lines long) in the Usage section actually runs with an instantaneous response time on the terminal. I added some remarks on the execution speed.
Thank you for your compliment! It is very encouraging and I appreciate it. I was excited too when I actually got the neural network running on the emulator.
Author here. Thank you! I had a lot of fun as well working on this project. I appreciate you and everyone's compliments since it encourages me a lot for working hard on my projects and sharing them.
Thanks! That would be since the skippable timestep width is bounded by the size of the size of the patterns that you've memorized. Say we have a square pattern of size W. The outcome of this pattern within this region in 1 timestep is completely determined by its surrounding square region of size W+2c, with c as the speed of light (pixels per timestep), since patterns beyond that can never interfere with it unless its interference travels beyond the speed of light. For two timesteps the surrounding region would be of size W+4c, since more pixels can interfere with it within that amount of time. Therefore, If you memorize a pattern of size W+4c, you can predict the outcome of the inner square of size N after 2 timesteps, or the inner square of size W+2c after 1 timestep, etc. This sets an upper bound to the number of timesteps you can skip, depending on the sizes of the patterns that you have memorized. So if you've memorized a pattern of size W+200c, you can predict the outcome of the inner square of size c after 100 timesteps, but predicting the 101st timestep would require information of a region beyond the memorized pattern.
Hi, I'm the author of this project. HashLife actually does just that, by memoizing and reusing past occurrences and outcomes of the same pattern. Since one cell can only interact with its 8 neighbors in one timestep, there is a limit to the distance that a fixed-size pattern can interfere with in a fixed amount of time, analogous to the speed of light in physics. (It is in fact called the speed of light for cellular automatons as well, as described in https://en.wikipedia.org/wiki/Speed_of_light_(cellular_autom... .) Therefore, by remembering the outcomes of a certain pattern in a certain timeframe, you can jump to that amount of time in one step by using the memoized pattern. More details are explained in this article: https://www.drdobbs.com/jvm/an-algorithm-for-compressing-spa...
By the way, with all the passion for Lisp, simple but Turing-complete systems, and programming that I put into this project, I'm very happy that other people have enjoyed it too. Thanks to everyone for checking it out!
I too suspect that writing in lambda's native functional style could save a lot of space. Compiling lisp.c from the ELVM repository generates a code much longer than LambdaLisp [1], which empirically shows that well I believe.
As for the pages of PDF, in mathematical terms, since any variable encodes to weight 1, I believe it would be something close to an encoding that degenerates all De Bruijn indices to 1, or in other words, one that only tries to weigh (or gives larger weight to) the complexity of abstraction depths and applications. Since that erases information about the variable I would guess it's not a universal method for weighing lambda sizes.
In this particular case for LambdaVM programs however, since the memory initialization clause nor the instruction clause never increases the maximum De Bruijn index value, I believe both the BLC size and "lambda page size" approximately grows linearly with the number of instructions, so I thought it would serve as an approximately-off-by-a-factor metric for weighing its size.
As for the ELVM lambda calculus back-end, I'll be sending the pull request very soon!
[1] A Lisp interpreter implemented in lambda calculus: https://github.com/woodrush/lambdalisp