zlacker

>>jekude+(OP)
> The appendix is a great segue to Church's Lambda Calculus, which will probably be my next project.

Note that a straightforward universal machine for the lambda calculus can be orders of magnitude smaller than for Turing machines [1].

[1] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d8...

>>tromp+uD8
Is the unary encoding of the indices in some way optimal or could one compress the representations further using some [variable length] binary encoding, maybe at the loss of some other desirable properties?

>>danbru+8z9
A unary encoding is certainly optimal in simplicity.

For encoding size, it would be optimal if index i occurs roughly with frequency 2^-i. In many lambda terms of practical interest, one does see higher indices occurring much less frequently, so it's not terribly far from optimal. Some compression is certainly possible; within n binding lambdas, index n could be encoded as 1^n instead of 1^n 0, but again that severely complicates the interpreter itself.