Functional Bits: Lambda-calculus based algorithmic information theory [pdf]
tromp.github.io
tromp.github.io
http://tromp.github.io/cl/cl.html
which links to an explanation of the graphical notation, to my corresponding IOCCC entry from 2012, and to a Wikipedia page on Binary Lambda Calculus that has since been deleted.
See this paper on how to cluster using compression: https://arxiv.org/pdf/cs/0312044.pdf
Is Lambda calculus a good match for algorithmic information theory. The versions of AIT I've read involved either Turing machines, hand-waving of computation or recursive function. Lambda calculus seems more complex and thus harder to integrate with an AIT that mostly needs to know that strings are programs, that not all programs terminate, that some programs can give a substring of their string as outputs and so-forth.
For AIT, the binary encodings used in this paper have the nice property that they're complete and prefix-free, meaning that every binary string either decodes to a term (perhaps using only an initial portion of the string), or can be extended (arbitrarily) until it gives rise to a term.
At first glance, it feels like it would be hard for lambda terms to "give a substring of their string as outputs", since that would require re-encoding a subterm. However, I don't think that's as bad as it sounds. For example, consider that a Turing machine can only move its head along the tape one cell at a time (we could use any finite step size, but we usually stick to one), which makes it difficult/impossible to "preserve" a section of tape. Hence Turing machines which "give a substring of their string as outputs" might sound simple, but would probably be somewhat complicated to ensure that any "corruption" caused when traversing the tape gets "undone" afterwards.
(Unless they're multitape machines, like monotone turing machines!)
> In the context of his Metabiology programme, Gregory Chaitin, a founder of the theory of algorithmic information, introduced a theoretical computational model that evolves ‘organisms’ relative to their environment considerably faster than classical random mutation. While theoretically sound, the ideas had not been tested and further advancements were needed for their actual implementation. Here we follow an experimental approach heavily based on the theory that Chaitin himself helped found. We apply his ideas on evolution operating in software space on synthetic and biological examples and even if further investigation is needed this work represents the first step towards testing and advancing a sound algorithmic framework for biological evolution.
I also like that the citations include Emperor's New Mind; Godel, Escher, Bach; the Brainfuck homepage, and Haskell. The effects of these ideas on a couple generations of young minds is bearing fruit.
It feels like we're on the brink of gamifying a lot of important math.
This is a great paper. But I burn so much mental energy trying to focus when I read something vs. when I listen to a video lecture. So I end up retaining more watching stuff and every more taking some notes.
The paper assumes knowledge of combinatory logic and lambda calculus, which you could probably find videos about. This paper uses pretty standard notation, so almost any video/course/book/blog/etc. should be OK. The main thing this paper does is to define a way to encode such programs as a string of bits.
Note that combinatory logic is one of the simplest Turing-complete programming languages, but it's so simple that it's basically unusable for anything more elaborate than toy examples (the paper actually has a quote from Chaitin saying this!). Once you're comfortable playing with little examples containing a handful of symbols, that's basically all you really need.
There's a nice book of mathematical puzzles https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird which is actually based on combinatory logic. This is why combinatory logic terms are sometimes referred to as "birds", e.g. in this Haskell library: https://hackage.haskell.org/package/data-aviary-0.4.0/docs/D...
If you're familiar with other programming languages, it's usually pretty easy to implement combinatory logic and play with it. For example, here are 'S' and 'K' in Javascript:
function k(x, y) { return y; }
function s(x, y, z) { return x(z)(y(z)); }
This isn't quite right, due to most languages using strict evaluation, but the following Haskell is essentially correct: k x y = y
s x y z = x z (y z)
There's also the esoteric language "unlambda" which implements these directly, including the "monadic IO" that the paper mentions https://en.wikipedia.org/wiki/UnlambdaLambda calculus is more tricky than combinatory logic, since it contains variables. It's also more widely used (e.g. as the basis for many functional programming languages, like Haskell and Scheme), so there should be more material available. In essence, when you see something like:
λa b c.x y z
You can think of it as acting like this Javascript: function(a, b, c) {
return x(y)(z);
}
When it comes to Kolmogorov complexity, maybe the Wikipedia page and its citations will help ( https://en.wikipedia.org/wiki/Kolmogorov_complexity )? Notice that all of the definitions, etc. on that page assume that we're talking about some particular programming language or machine, but the examples use pseudocode rather than a "real" programming language. This paper is basically saying that we should use lambda calculus as that language, and we can measure the size/length of a program by encoding it as binary according to the method given.