v3.0.1

blam 3.0.1 changes no interface. It republishes the README with what has been established since 3.0.0, chiefly a 162-bit self-interpreter, and corrects how the busy-beaver values are credited.

A 162-bit self-interpreter

BLC's smallest known self-interpreter is now 162 bits, six below Sean Palmer's 168 (tromp/AIT's int.lam). On the way it went through a 165 (Codex's design), which computes the skip once, on the whole stream, before dispatch.

• What changed. The 162 keeps the 165's recursion and its second-bit stage and replaces the reader. The reader applies the input stream to the identity, so after a 0 the first cell selects its own tail as the zero branch. After a 1 it reopens the stream, hands the tail to the continuation, and skips the variable's code with the second-bit stage as an erased third operand. That stage is now the reader's last operand instead of a let.
• Proved. Lean proves it correct for every closed program (selfint_contract162 in lean/Blc/Selfint162.lean). It proves the 165 and Palmer's 168 the same way. An independent adversarial review re-derived the contract and the size.
• Checked. It passes the self-interpreter battery (667 programs pass, 1 skipped, none fail) and the extended battery through 21 bits (3,341 pass, 2 skipped, none fail). Its let structure is the unique minimum up to three cuts. Its βη component through slack 24 (12,024,847 terms) holds nothing smaller.
• Universal machines. The same reader gives 172 bits (non-strict) and 184 (strict), against Tromp's 178 and 190. Both of Tromp's wirings follow from a self-interpreter's contract, so Lean proves U (⌜M⌝ ++ N) →β* M N for every closed M for all six machines around the 162, the 165 and the 168, Tromp's own uni.lam included. Each is pinned to its wire (lean/Blc/Universal.lean). blam selfint wiring --strict (lab) now runs a seventh strictness probe, Codex's counterexample to base environments that apply the parser; battery.py --strict runs the same seven.
• Lower bounds. Every self-interpreter has at least 37 bits, by a handwritten proof that two independent reviews checked (global floor). At least 27 bits are kernel-checked in Lean.
• How it was found. Codex, refuting a step in Claude's proof that the 165's reader was optimal, built a 44-bit reader as a counterexample. Spliced into the 165, it gave a correct 166. blam golf letopt then moved the second-bit stage into the reader's operand slot, which was Grok's idea, and that gave 162.

The full record is docs/classical/self-interpreter/interpreter.md.

The rest of tromp/AIT

The golf branch, sent upstream as tromp/AIT#13, shrinks 40 programs by 1,159 bits in all:

• the IOCCC BLC8 universal machine goes from 43 bytes to 38 (strict) and 36 (non-strict);
• the bytewise BLC2 machine goes from 500 bits to 390;
• the constant in KP(x) ≤ KO(x) + c goes from 615 to 540;
• the symmetry-of-information constants drop by up to 132 bits;
• Loader's number fits in 1781 bits.

The 162's reader is in all six programs that share it: int.lam, uni.lam, int4, ko2kp, nf and pairup_Kp. docs/classical/golf.md records how each one was checked.

Correction

The 3.0.0 README said the census establishes BBλ(33) = 1,812, BBλ(34) = 327,686 and BBλ(35) = 38,127,987,424,941. These are Tromp's values (OEIS A333479). The census and blam's kernel-checked adjudications confirm them independently. The README also no longer quotes the census bound BBλ(41) ≥ 38,127,987,424,947. It is true, but A333479 already lists a(36) = 5·2²⁵⁶ + 6, which makes it uninformative.

Found and checked with Claude (Anthropic), Codex (OpenAI), Grok (xAI) and Gemini (Google).

v3.0.0

blam 3.0.0 brings John Tromp's own tools into blam. blam blc is his blc, and blam uni is his universal machine. Both run his programs on a new call-by-need machine, and both are checked byte for byte against his originals. Every command that takes a term now also accepts λ-notation and .lam, .blc and .blc8 files. It is a major release because the qalc pillar's public types changed (listed below).

Tromp's tools

blam blc ACTION PROGFILE [ARGS...] runs every one of the 31 actions of Tromp's blc, with no GHC required:

• the run family: run, run8, runf, runO;
• normal forms: nf, hnf, nf_size;
• printing: print, db, printlc;
• the encoders: blc, blc2, size, size2, size0;
• the combinatory-logic translations: comb, combOK, comb_nf, bcw, bcl, blcOK;
• the lambda diagrams: diagram, boxchar, pbm, and their alternative forms;
• tex, html, nfhtml.

blam blc blc reproduces every checked-in .blc in tromp/AIT. Standard input is read lazily, the way blc reads it, so primes.lam starts printing immediately in a terminal and an interactive program shows its output before it waits for input. Endless output streams, so blam blc run primes.lam | head works.

blam uni [-b] [PROGRAM...] is the universal machine. It has bit and byte modes, looks up $BLCPATH names, composes several programs left to right, and reads embedded input from a single program file, all as uni.c does. It decodes output the way uni does, by application: λx.λy.λz.x z is the bit 0. It does this through a decoder that rebuilds the output from marker constructors no program can forge, so output that breaks uni's protocol is reported as an error instead of being misread.

A call-by-need machine (classical::lazy) runs both tools. Tromp's brainfuck interpreter prints Hello World! at once on it, where the call-by-name KN machine prints nothing in 2³⁰ transitions. Its memory is the live data, held to a hard cap (--live), and its input can be a lazily read stream. On every closed term of 26 bits or fewer it produces the KN machine's normal forms. The KN machine stays the engine for the census, Solomonoff, Ω and busy-beaver measurements, whose β-counts are leftmost-outermost.

Term notation. normalize, adjudicate and golf take wire bits, a .lam, .blc or .blc8 file, or λ-notation on the command line: '(\x.x x) (\y.y)', de Bruijn '(\1 1) (\1)', or λ in place of \. blam normalize --db prints the normal form in de Bruijn notation. On the library side, blc::notation parses Tromp's .lam language, prints his two notations, and implements optimize 57 2 1 as compile. classical::io holds his I/O conventions: input lists, bshow, a streaming output reader, and the uni decoder.

blam golf is now in the default build.

The contract, including the few deliberate differences from Tromp's tools, is docs/classical/programs.md.

How it was checked

Every comparison ran against Tromp's tools built from the pinned corpus, using the harnesses in tools/ait/:

• Every non-run action on every .lam program in tromp/AIT: 2,791 pairs byte-identical and none different. 247 pairs finish on neither side; these are normal forms of the fast-growing programs.
• The run family on every closed program of 20 bits or fewer, plus 2,500 random larger ones, each on ten inputs: 38,382 successful and 5,408 erroring pairs byte-identical, including the output written before an input error. None differs.
• blam uni against uni.rs, in 20,804 runs: wherever uni.rs prints, blam prints the same bytes; wherever it fails, blam fails too, having printed no more than uni.rs did. On output that breaks uni's protocol, uni.py, uni.rs and uni.c disagree with one another.

Results since 2.1.0

• BBλ(33) = 1,812, BBλ(34) = 327,686, and BBλ(35) = 38,127,987,424,941. These are exact, via kernel-checked Lean adjudications of every program the census leaves open at those sizes. The 35-bit value is the Church numeral 3^27, proved symbolically. The census also gives BBλ(41) ≥ 38,127,987,424,947.
• Nine binary digits of the true halting probability Ω are pinned, Ω = 0.001000000…. The tenth is almost surely 0 by estimate, but not proven.
• The coding theorem on BLC's own machine has a certified constant c ≥ 3.689.
• AIT golf: the IOCCC BLC8 universal machine shrinks from 43 to 41 bytes (38 non-strict), the BLC2 machine from 500 to 399 bits, and 45 programs shrink under certified β-golf.
• The 168-bit self-interpreter: nothing smaller exists in any searched space, and a lower bound by modules sums to exactly 168.
• qALC: the finite-clock census has converged through 27 bits, and the speed prior has a certified stopping rule.
• Speed: a census of 4..40 takes about 21 s wall on an M5 Max.

docs/STATUS.md has the evidence for each.

Breaking changes

• qalc types. mark::Lp is now an opaque shared handle; the old struct is LpNode. LogEntry and TapeEntry payloads, several state fields and NfRun.zipper are now Shared<…>. NfRow.rule, ColRow and ProbeRow carry Rule = Cow<'static, str>. SemanticsError gained TickBeyondClock.
• No longer public: qalc::wf, the two *_without_digest admission entry points, and classical::escalation::{app, lam, emit_bits}, whose names shadowed the crate-root term constructors.
• Task splitting. blc::enumerate::split_tasks and split_tasks_at now split by exact term count. Task boundaries differ, though enumeration order is unchanged.
• Checkpoints are blamckpt v5; v4 files must be regenerated.
• Library additions: Sink gains a defaulted idle method, Pool::from_term is iterative, and blc::notation, classical::io and classical::lazy are new.

Credits

As with everything in this repository, the design, implementation and verification were done by AI agents working in a9's repository, directed and reviewed by a9. Claude (Anthropic) built the blc and uni reimplementations, the call-by-need machine and the differential harnesses. Codex (OpenAI) gave four rounds of adversarial review. Each round found real defects, with reproducers: holes in the memory cap, uni's decoding by application, embedded input, input errors under runf, blocking reads after cancellation, and the reference interpreters' disagreements. The lambda calculus, the encoding, the BBλ problem and the reference tools are John Tromp's.

---

Merged in #10 · Full changelog: v2.1.0...v3.0.0

v2.1.0

What's Changed

• Dev by @a9lim in #7

Full Changelog: v2.0.0...v2.1.0

v2.0.0

What's Changed

• ci: bump actions/checkout from 6 to 7 by @dependabot[bot] in #1
• ci: bump actions/cache from 4 to 6 by @dependabot[bot] in #2
• Dev by @a9lim in #4
• Dev by @a9lim in #5

New Contributors

• @dependabot[bot] made their first contribution in #1

Full Changelog: v1.0.1...v2.0.0

v1.0.1

What's Changed

• Dev by @a9lim in #3

New Contributors

• @a9lim made their first contribution in #3

Full Changelog: v1.0.0...v1.0.1

v1.0.0

First public release. Binary lambda calculus engine for algorithmic information theory: exhaustive term censuses 4..41 bits, the first BBλ(41) bound, exact Ω bracketing, 297 kernel-checked divergence certificates (Lean 4, zero sorries), and the qBLC quantum operator census. On crates.io as blam; AGPL-3.0-or-later.

Full Changelog: https://github.com/a9lim/blam/commits/v1.0.0