Skip to content

Home

Jump to bottom
Peter Lodri edited this page Jun 10, 2026 · 1 revision

A reproducible open dataset + engine for the normalization geometry of the untyped λ-calculus, built around the open Barendregt–Geuvers–Klop (BGK) conjecture.

Code: MIT · Data & docs: CC BY 4.0 · Pure Python 3.9+ (standard library only, no dependencies).

What this is

This project asks a concrete combinatorial question in service of a famous open problem. The BGK conjecture (TLCA Problem #9, open since the 1990s) asks whether weak normalization (WN) implies strong normalization (SN) in pure type systems — i.e. whether having some terminating reduction forces every reduction to terminate. The known counterexample mechanism is erasure: a function that throws away its argument (like λa.λb.b) can have a normal form even when its argument loops forever. In the erasure-free λI-calculus, this gap closes — there WN ⟺ SN (Church 1941; Barendregt Thm 9.1.5) — and Klop's ι-translation transports erasing λK terms into the non-erasing λI[,] calculus, isolating erasure as the obstruction. Nothing here resolves BGK; the experiments corroborate the mechanism, not the theorem.

The headline contribution is an open-data census: we classify closed untyped λ-terms by natural size (de Bruijn indices, with |index k| = k+1, |λM| = 1+|M|, |MN| = 1+|M|+|N|) into SN, separator (= WN ∧ ¬SN, the "WN∖SN gap"), non-WN, and undecided (within the engine's bounded caps). Our closed-term counts match OEIS A275057 (Lescanne 2016) exactly, term-for-term, validating the model. On top of that base we tabulate the separator-density curve and the smallest witnesses — quantities that, as far as the literature shows, were previously unrecorded. This is machine-assisted research: every quantitative claim is computed, then cross-checked against primary sources; proven theorems (cited) are kept distinct from our empirical measurements, and the undecided remainder is stated explicitly.

Start here

  • The Research — the BGK conjecture, λI vs λK, erasure, conservation, and Klop's ι-translation, with citations.
  • Results and Findings — headline numbers, the separator-density curve, the decidability horizon, and how they sit against the published asymptotics.
  • Engine and API — the reduction-graph analyzer: term representation, analyze(t, node_cap, size_cap), and how SN/WN/non-WN are decided.
  • Dataset — the open data: per-size SN/SEP/NWN/UND counts, densities, Wilson CIs, and the smallest-separator witness; CSV/JSON schema.
  • Reproduce — run the census, rebuild the dataset, and run the BGK lab from scratch (stdlib-only).
  • Contributing and Experiments — how to extend the engine, add experiments, and contribute under the license.
  • FAQ — open vs proven, the two opposing size conventions, the decidability horizon, and other common questions.

Headline results

  • Smallest closed non-WN term is Ω at natural size 9 — (λx.x x)(λx.x x).
  • Smallest closed separator (WN ∧ ¬SN) has natural size 13: (λa.λb.b) Ω = λλ0 (λ(0 0) λ(0 0)) — an erasing function applied to Ω. Apparently undocumented; the WN∖SN gap is not tabulated in the combinatorics-of-λ literature.
  • Model validated against OEIS A275057 — closed-term counts 0, 1, 1, 3, 6, 17, 41, 116, 313, 895, 2550, 7450, 21881, … match exactly.
  • Method: exact enumeration for n ≤ 16, then uniform Monte-Carlo (K = 50 000 samples) for n in {17 … 55}. Decided-SN stays ≥ 99% through n = 55; the undecided fraction climbs (0 → ~10% at n = 55); separator density of decided terms rises ~0.014% at n = 13 → ~0.4% at n = 55. The Monte-Carlo run itself became intractable around n = 70 (the practical decidability horizon).
  • Consistent with theory, honestly framed: Bendkowski–Grygiel–Lescanne–Zaionc (2017, Cor. 4) prove SN-density → 0 in this natural-size model; our high decided-SN is consistent because the non-SN mass hides in a growing undecidable tail. This is the opposite of David–Grygiel–Kozik–Raffalli–Theyssier–Zaionc (2013), whose convention (variables cost 0) gives SN-density → 1. The size convention controls the answer. The asymptotic WN density / WN∖SN gap is computed in neither paper — it remains open.
  • BGK conservation lab (companion, 7 experiments in src/bgk_lab.py): λI exhaustive check finds 0 separators / 3.13 M terms; the perpetual-strategy law diverges ⟺ ¬SN holds with 0 violations / 762 k; Klop's ι-translation transfer SN(M) ⟺ SN(ι(M)) holds with 0 violations / 711 k. (The λK separator onset in the lab's own ad-hoc enumeration is size 12 — a different convention from the census's closed-de-Bruijn size 13.)

Key links

Standing on Church (1941); Barendregt, Bergstra, Klop, Volken; Sørensen; Geuvers; de Vrijer; David et al. (2013); Bendkowski–Grygiel–Lescanne–Zaionc (2017); Lescanne (OEIS A275057). Bonus tooling: crabcc (v6.3 indexed Linux 6.18 LTS — 3.87 M symbols, 68,875 files, ~177 s).

Clone this wiki locally