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