Lots of info about Lambda Calculus itself, the closely-related Combinatory Logic, and how Tromp arrived at his tiny little BLC. Pretty much a tour de force of mathematical logic.
I was about to post this masterpiece. The self interpreter is like some sort of Platonic mathematical treasure, like the Gosper Glider Gun or the Monster Group. (Please feel free to suggest other examples.)
[edit: some more off the top of my head; the Burning Ship, minimal ZFC-undecidable Turing machine[0], Milnor's 7-Sphere)
PDS: My new all-time favorite article on HN in the field of Turing Machines, Lambda Calculus, Tiny Languages, etc.
>"This program celebrates the close connection between obfuscation and conciseness, by implementing the most concise language known,
Binary Lambda Calculus (BLC)."
[...]
>"The BLC universal machine may be small at 650 bytes of C (952 bytes including layout),
but written as a self interpreter in BLC it is downright minuscule at 232 bits (29 bytes):"
[...]
>"A half byte `cat'
The shortest (closed) lambda calculus term is \x x (\ 1 in De Bruijn notation) which is the identity function. When its encoding 0010 is fed into the universal machine, it will simply copy the input to the output. (well, not that simply, since each byte is smashed to bits and rebuilt from scratch) Voila: a half byte cat:"
[...]
>"A BLC assembler
Writing BLC programs can be made slightly less painful with this parser that translates single-letter-variable lambda calculus into BLC:"
PDS: Opinion: Not just brilliant -- but insanely, utterly, astronomically brilliant!
My hat, as someone deeply interested in the fundamentals of computation, and as someone who could never accomplish what you did -- goes off to you!
John Tromp is an active HN user and he almost surely replies to any mention to BLC or similar. I personally find Jot [1] more elegant though, where every bit sequence is a valid program. (I'm not very qualified to say which one is more compact in general however.)
> I personally find Jot [1] more elegant though, where every bit sequence is a valid program
In BLC every bit sequence is a valid program prefix, meaning it's either a complete program on its own, or we can stick another arbitrary bit on the end to get another valid program prefix.
This isn't quite as elegant as having every bit sequence be a valid program. However, I find the idea of self-delimiting programs even more elegant; which AFAIK doesn't apply to either Jot or BLC. Self-delimiting programs are like program prefixes, with an extra constraint that no program is a prefix of another. This way we can feed a parser one bit at a time (e.g. generated by tossing a coin), and if it ever forms a valid program then we can stop reading/generating bits, since there's no other program possible from that prefix. This is useful in algorithmic information theory (e.g. Kolmogorov complexity).
It also features prominently on my homepage https://tromp.github.io/ as an image in a font custom designed to look good on shirts, such as the one I wear in my picture:-)
Lots of info about Lambda Calculus itself, the closely-related Combinatory Logic, and how Tromp arrived at his tiny little BLC. Pretty much a tour de force of mathematical logic.