John Tromp

The increasing recognition that "Language Modeling Is Compression" https://arxiv.org/pdf/2309.10668.pdf has not yet been accompanied by recognition that lossless compression is the most principled unsupervised loss function for world models in general, including foundation language models in particular.

Take, for instance, the unprincipled definition of "parameter count" not only in the LLM scaling law literature, but the Zoo of what statisticians called "Information Criteria for Model Selection". https://en.wikipedia.org/wiki/Model_selection#Criteria

The reductio ad absurdum of "parameter count" is arithmetic coding where an entire dataset can be encoded as a single "parameter" of arbitrary precision.

By contrast, the algorithmic bit of information (whether part of an executable instruction or program literal) is an unambiguous quantity up to the choice of instruction set. If you want to quibble about that instruction set choice, take it up with John Tromp https://tromp.github.io/cl/cl.html because what I'm about to propose obviates that along with a lot of other "arguments".

Since any executable archive of any kind of data can serve as a model of the world generating that data, it follows that any executable archive of any text corpus can serve as a language model with a rigorous "parameter count". Therefore, a procedure which runs LLM benchmarks against any such executable archive as a language model, contributes a uniquely rigorous data point to the literature on LLM…

Not sure about this specific paper, but I've been following John Tromp's work on this for a while. Its current homepage seems to be on GitHub https://tromp.github.io/cl/cl.html

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/Data-Aviary-Birds.html

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…

Oh, no, not this paper again.

Please see https://boardgames.stackexchange.com/questions/58127/ for reference. The first picture there shows a game supposedly "won by Black", due to a refusal to acknowledge that Black's stones are hopelessly dead everywhere except the top-right of the board. The "exploit" that the adversarial AI has found is, in effect, to convince KataGo to pass in this position, and then claim that White has no territory. It doesn't do this by claiming it could possibly make life with alternating play; it does so, in effect, by citing a ruleset that doesn't include the idea of removing dead stones (https://tromp.github.io/go.html) and expects everything to be played out (using area scoring) for as long as either player isn't satisfied.

Tromp comments: "As a practical shortcut, the following amendment allows dead stone removal" - but this isn't part of the formalization, and anyway the adversarial AI could just not agree, and it's up to KataGo to make pointless moves until it does. To my understanding, the formalization exists in large part because early Go programs often couldn't reliably tell when the position was fully settled (just like beginner players). It's also relevant on a theoretical level for some algorithms - which would like to know with certainty what the score is in any given position, but would theoretically have to already play Go perfectly in order to compute that.

(If you're interested in why so many rulesets exist, what kinds of…

Combinators are math, and a little like Lisp - building functions from primitives and operations with the ability to apply them, where even the notion of variables are functions - functions all the way down.

The y combinator is this: λf.(λx.x x)(λx.f(x x))

Lambda diagrams get you visualizations like this:

https://tromp.github.io/cl/diagrams.html

When considering logic and functions, when thinking in the space of combinators, you can ask questions like "What is Plus times Plus" and have a sensible result.
https://www.youtube.com/watch?v=RcVA8Nj6HEo

Combinators are awesome.

The site linked by OP is a specific collection of combinators with bird names, riffing on the "To Mock a Mockingbird" puzzle book and subsequent meme of giving combinators bird names.

There's a lot of chess configs, but there's a LOT of atoms in the observable universe. I suspect there's a few in the unobservable universe too.

Chess configs = 4.8 x 10^44, Atoms > 10^70

https://tromp.github.io/chess/chess.html https://physics.stackexchange.com/questions/47941/dumbed-down-explanation-how-scientists-know-the-number-of-atoms-in-the-universe

You might be able to pull off a low-resolution lookup table. Take some big but manageable number N (e.g 10^10) and calculate the maximally even distribution of those points over the total space of chessboard configurations. Then make a lookup table for those configs. In play, for configs not in the table, interpolate between nearest points in the table.

Yeah it terminates.

A tiny 63 bit program[0] in this language represents a number unfathomably larger than not only ack(9,9), but the far larger Graham’s Number as well. It originates in a Code Golf challenge asking for the “Shortest terminating program whose output size exceeds Graham’s number”, answered by user Patcail and further optimized by user 2014MELO03. With one final optimization applied.

Here's a really short program. Let's calculate 2 * 3

(λn m s. n (m s)) (λf n. f (f n)) (λf n. f (f (f n))) eventually it terminates with

λ s n.s (s (s (s (s (s n))))) which is just the church encoding of 6.

[0] https://tromp.github.io/blog/2023/11/24/largest-number