One terminating reduction, or all of them?
The Barendregt–Geuvers–Klop conjecture asks when weak normalization (some reduction halts) forces strong normalization (every reduction halts). We make it measurable: enumerate terms, reduce them every possible way, and hunt for the gap.
Conservation at scale
Every closed \lambda I-term up to size 24, reduced to a fixed point under all strategies. If the conjecture were going to break over λI, it would break here.
Separators: where WN and SN part ways
Allow erasure and the gap opens. We enumerate the terms that normalize one way and diverge another, and find the smallest.
Reduction geometry of SN terms
For strongly-normalizing terms, the reduction graph is finite — but how big, how deep, how branchy? Two views of the same 83k-term sample.
The perpetual law
A non-terminating term can hide its infinite path from a careless strategy. Barendregt's perpetual strategy F_\infty never misses it.
The ι-translation
If erasure is the obstruction, remove it. The ι-translation rewrites every term into the erasure-free fragment by keeping what it would have thrown away.
Speedup: innermost vs outermost
When both strategies terminate, how much does redex order cost you? Almost always, eager (innermost) is the bargain.
The reduction-graph zoo
α-quotiented reduction graphs for hand-picked small terms. ¬SN graphs carry a cycle; SN graphs don't.
crabcc × the Linux kernel
The reductions above were tractable because the engine's symbol layer is fast. Here it is pointed at the hardest target we had lying around: the Linux kernel.
Research notes
Where this lab sits in the literature. The conjecture is decades old; the contribution here is exhaustive, reproducible evidence.