Binary Lambda Calculus (2020)
tromp.github.io
tromp.github.io
This has a ton of really interesting implications.
Even though Kolmogorov complexity is technically incomputable due to the halting problem, you can estimate it. One method of doing that is to create a bunch of random Turing machines and see how often they produce some output string[1]. You have to cut them off after running for a while to prevent infinite loops but it turns out that the output probability of a string strongly correlates with its Kolmogorov complexity.
This works for neural networks as well. You can treat a neural network as a binary classifier, or more generally a boolean function that has some number of binarized inputs mapping to a single binary output.
I explored this a bit in a blog post I wrote a while ago[2]. By randomly initializing weights and counting the truth tables produced, you can estimate Boolean complexity for different expressions which is NP hard.
[1] https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4014489/
[2] https://cprimozic.net/blog/boolean-logic-with-neural-network...
I just don’t agree that this can be fairly summarized as “estimating Kolmogorov complexity”.
Kolmogorov complexity isn’t a statistical measure — it doesn’t matter how unlikely the machine that produces the output string is. And the time limit they have to impose to actually run those machines is crucial; some of the machines they have to abort would eventually produce an output and halt.
BLC provides a functional busy beaver function [3] that is more fine-grained than the TM-based one.
The byte oriented version BLC8 is one of the 128 languages in the quine relay [3].
[1] https://www.ioccc.org/2012/tromp/tromp.c
[2] https://www.ioccc.org/2012/tromp/hint.html
[4] https://esoteric.codes/blog/the-128-language-quine-relay
http://stephenbalaban.com/a-binary-lambda-calculus-parser-in...
Binary Lambda Calculus (2012) - https://news.ycombinator.com/item?id=26769650 - April 2021 (12 comments)
Most functional (tromp - implementing Binary Lambda Calculus) - https://news.ycombinator.com/item?id=4673056 - Oct 2012 (1 comment)
Others?
https://en.wikipedia.org/wiki/Iota_and_Jot
http://cleare.st/code/iota-jot-zot
> Every combination of 0's and 1's is a syntactically valid Jot program, including the null program.
[1] https://tromp.github.io/cl/Binary_lambda_calculus.html#Brain...
I’m kind of tempted by the idea of sugaring it using symbol properties such that one could use obfuscating names without breaking the elegant alpha compare and convert.