blam — binary lambda machine

A fast Rust engine for John Tromp's binary lambda calculus, plus qBLC, a quantum extension with exact Clifford+T semantics. Built for algorithmic information theory — exhaustive term censuses, busy-beaver frontiers, exact Solomonoff/Kolmogorov measurement, machine-checked divergence certificates — and shipped as a library with a set of measurement drivers on top.

Design principles throughout: every fast path is differential-tested against a naive executable spec; every engine is total (fuel exhaustion is a typed verdict, never a hang, and resource limits are charged on a shared work meter); every quantum amplitude is exact (ℤ[ω]/√2^k integers — no floating point anywhere).

Install

cargo add blam

For the full lab — canonical data tables, the Lean formalization, and Tromp's reference corpus for conformance tests:

git clone --recurse-submodules https://github.com/a9lim/blam

Library

The reference core is term / parse / eval: a textbook-faithful normal-order normalizer that serves as the executable spec. Terms use 1-indexed de Bruijn (Var(1) = innermost binder), matching the wire format (00 λ, 01 application, 1ⁿ0 variable n); closed-term code is prefix-free, which is what makes the Kraft sums of AIT exact.

use blam::{normalize, parse_all, Budget};

// (λx.x x)(λx.x) — bits in, bits out
let term = parse_all("01000110100010")?;
let nf = normalize(&term, &mut Budget::new(1_000))?;
assert_eq!(nf.to_bits(), "0010"); // λx.x

vm is the production engine: a defunctionalized Crégut-style strong-normalization machine (~166M β/s single-thread), arena-backed, with β and transition budgets and the normal form streamed to a Sink — measuring a gigabyte-scale normal form costs O(1) space.

use blam::vm::{Machine, StringSink, TermPool};

let mut pool = TermPool::new();
let root = pool.decode_str("01000110100010").unwrap();
let mut nf = StringSink(String::new());
let steps = Machine::new().normalize(&pool, root, 1_000, &mut nf)?;
assert_eq!((nf.0.as_str(), steps), ("0010", 2));

Around the core: oracle (Tromp's syntactic divergence prefilter), bb (the escalation engine: redex-history loop detection plus a semantic self-feedback divergence certificate), cert (trusted checkers for three machine-checkable divergence-certificate classes), and enumerate (parallel closed-term enumeration, u64-packed).

qBLC

The quantum pillar mirrors the layout with a q prefix: qeval is the reference evaluator, qvm the lockstep-verified fast path, dw the exact ring. Programs are ordinary untyped BLC — quantum enters through an application signature of five primitives (new / meas / cnot / t / h, order frozen by a predeclared pilot). Qubits are opaque runtime handles with dynamic linearity (cloning is a runtime Err, not a type error), measurement branches the machine with exact weights — nothing is ever sampled — and each branch leaf carries a typed fate: Halt(store), Diverge-by-budget (Unknown), Capacity, or Err.

use blam::qeval::{apply_signature, run, Prim, QBudget};
use blam::term::{app, lam, var};

// λ⁵. cnot (h (new t)) (new t) — a Bell pair, in 41 bits (the size
// where entanglement first enters the census)
let body = app(
    app(var(2), app(var(5), app(var(3), var(1)))),
    app(var(3), var(1)),
);
let p = (0..5).fold(body, |b, _| lam(b));

let order = [Prim::H, Prim::Meas, Prim::New, Prim::Cnot, Prim::T];
let leaves = run(apply_signature(&p, &order), &QBudget::default());
// one Halt leaf: 2 live qubits, amplitudes exactly (|00⟩ + |11⟩)/√2,
// mass exactly 1, in 9 contractions

Runnable versions of these snippets: examples/normalize.rs, examples/bell.rs, examples/parse_file.rs.

Drivers

The measurements live in src/bin/, all rayon-parallel:

bin	what it does
census	adjudicate every closed term in a size range (halt / diverge / unknown) through a ladder of engines
solomonoff	Solomonoff prior m(x), prefix complexity K(x), two-sided Ω bounds — exact 2⁻⁶⁴-unit arithmetic
certsearch	divergence-certificate discovery sweep over a frontier file
certlean	emit the certificate kills as Lean 4 modules for kernel checking
certdiag / tracescan	frontier classification and probe instruments
qcensus	the quantum operator census (--cond-k K for the dimension-conditioned mode)
qpilot / qselfint / qradical	signature-order pilot, self-interpretation measurement, dyadicity hunt
slotsearch	exhaustive self-interpreter slot searches

cargo build --release

# census of all closed terms of 4..40 bits, with self-verification
target/release/census 4 40 --verify

# one-term verbose adjudication
target/release/census --term 010001101000011010

# Ω / K sweep;  quantum census
target/release/solomonoff 4 41 --table data/solomonoff_table.txt
target/release/qcensus --max-n 41 --trans 67108864 --out data/qcensus_table.txt

# certificate sweep, then kernel-check the kills in Lean
target/release/certsearch --terms-file data/unknowns.txt
cargo run --release --bin certlean && cd lean && lake build Certs

Knobs: BLC_WORK_MULT (work-meter multiplier; 2 = memory-bounded adjudication), BLC_PROBE_FUEL (certificate probe β budget). The standing measurement protocols are encoded in scripts/ (spot-check, census regeneration, certificate re-certification).

Verification

• The fast VM is lockstep-verified against the naive spec — output bits and β-step counts — over every closed term ≤18 bits; the quantum fast path likewise, over full leaf sequences (fates, stores, exact masses) for the entire ≤24-bit population.
• Conformance tests parse Tromp's own corpus from the ref/AIT submodule (the a9lim/AIT fork, pinned at upstream plus one additive commit; CI enforces additivity). Every published A114852 count and BBλ value in range is reproduced exactly.
• Halt counts are invariant under every engine change in the repo's history — CI diffs a census spot-check against the canonical table on every push.
• Every one of the 297 certificate kills is an individually kernel-checked ¬HasNormalForm theorem in Lean 4 (zero sorries, no mathlib), pinned to its wire bits by a kernel-checked encoding.

Selected results

The measurements this engine exists for, in one breath: the complete census of all 526,039,969 closed terms of 4–41 bits (~16.5 min on an M5 Max) giving the first BBλ(41) bound (≥ 1,074,266,118 bits) and a fully mechanical BBλ(32); Ω restricted to ≤41 bits exactly bracketed in [0.124105086764, 0.124105092919]; the 170-bit self-interpreter certified locally optimal; and on the quantum side the first computed operator census of quantum-preparing programs (to our knowledge) — Ω_success exactly, single- and two-qubit state rankings, entanglement entering at exactly 41 bits, irrationality invading in measured layers (operator entries at 34, leaf masses at 45, per-size aggregates at 53), and qBLC self-interpreting in 176 bits.

The full story, with cross-checks and open questions: DESIGN-BLC and DESIGN-QBLC (architecture and measured results), LEDGER (the lab notebook), the canonical tables in data/, and the Lean formalization in lean/.

Layout

• src/ — the library (reference core + engines, quantum pillar q-prefixed); src/bin/ — the drivers.
• examples/ — the README snippets, runnable.
• tests/ — unit, differential, conformance, and certificate soundness batteries.
• docs/ — design specs, proof plans, the lab notebook.
• data/ — canonical measurement outputs (regenerated, never hand-edited; superseded generations live in git history).
• scripts/ — the standing protocols, runnable.
• lean/ — the Lean 4 formalization (own README).
• tools/ — analysis sub-labs: cert/ (certificate spec + kills), interp/ (self-interpreter lab), uni/ (upstream PR kit), blcc.py (the .lam→.blc encoder oracle).
• ref/AIT — submodule: the conformance corpus and execution oracles.

The crates.io package ships the engine alone (src/ + this README); everything else lives in the repo.

Attribution

The λ-calculus, the encoding, the BBλ problem, the reference implementations, and the published values are all John Tromp's (tromp/AIT); src/bb.rs and src/oracle.rs re-implement algorithms from BB.lhs/AIT.lhs. This repo is an independent engine, verified against his.

Built by a9lim with Claude (Anthropic) and Codex (OpenAI) as agent collaborators — docs/LEDGER.md and the commit history are the honest record of what that looked like.

AGPL-3.0-or-later — covering this repo's own code (© 2026 a9lim). The ref/AIT submodule is upstream Tromp material (which carries no license file; rights remain the author's), referenced by pin, never vendored.