From 245fb6ead39e0000b6079deb5ecc8840d8c2924c Mon Sep 17 00:00:00 2001 From: "russell@unturf.com" Date: Sun, 10 May 2026 07:45:40 -0400 Subject: [PATCH] =?UTF-8?q?PLFA=20+=20SF-LF=20+=20PM=20Vol=201=20ingest:?= =?UTF-8?q?=2062=20->=2068/92=20(74%)=20=E2=80=94=20pillar=20IX=20nearly?= =?UTF-8?q?=20closed?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three new substrates targeting the lambda-calculus gap (pillar IX was 5/14 stuck) and the type-theoretic Russell's Paradox Resolution record (last pillar II straggler): PLFA - Programming Language Foundations in Agda (Wadler/Kokke/Siek, Edinburgh CS, CC-BY-4.0) plfa.github.io BFS depth=2 max=60 -> 58 docs / 413 chunks Untyped + simply-typed lambda calculus, Confluence/Church-Rosser, progress + preservation, de Bruijn, beta/alpha/eta reduction. Software Foundations Vol 1 - Logical Foundations (Pierce et al., Penn CIS, MIT-licensed) softwarefoundations.cis.upenn.edu/lf-current/ BFS depth=2 max=40 -> 33 docs / 367 chunks. Coq induction proofs, lambda calculus. Whitehead-Russell Principia Mathematica Vol 1 (1910 Cambridge, PD by age, PG #78050 single-page HTML) -> 1 doc / 231 chunks. Preface + intro + chs I-III only; formal type theory body (*24 onwards) not transcribed. Plus 4 new citation-alias rows per #000041 (decision_by="fox 2026-05-10"): Barendregt -> PLFA (+5 pillar IX) Barendregt -> Software Foundations LF (+1 pillar IX, supplementary) Jech -> PM Vol 1 (cascade miss; 0 lift) Landau -> Software Foundations LF (cascade miss; 0 lift) Per-pillar: IX: 5/14 -> 11/14 (+6 — beta/alpha/eta + Church-Rosser + extensionality + fixed-point) Others stable. Title-haystack hack reverted: initial backfill appended ", Barendregt substrate" to PLFA + SF docs, which would have let the resolver match Barendregt citations directly via the haystack (mis-labeling chains as DIRECT instead of via_alias). Now uses clean citation-alias substitution; audit trail preserves substitution. Cumulative day-of-2026-05-10: 18 -> 68 / 92 (+50 records, +54pp). 24 records still stuck. Top blockers: - Pillar I formal proof axioms (3) — Hilbert-Ackermann needed - Pillar III symbolic-axiom cascade misses (6) — Peano/Dedekind/SF have content; FTS5 token cascade doesn't surface - Pillar V Kolmogorov axioms (4) — Laplace narrative not enough, Kolmogorov 1933 URAA-blocked until 2058 - Pillar VII advanced identities (5) — Bogart skews intro - Pillar IX (3) — Turing/Bohm-Jacopini/Orbit-Stabilizer cascade misses - Pillar VI (2) — Newton 1729 vocab mismatch - Pillar II Russell's Paradox Resolution (1) — PM Vol 1 *24+ not transcribed --- Makefile | 9 ++ bench/fixtures/textbooks/manifest-v1.jsonl | 3 + .../lambda-and-pm-additions-2026-05-10.md | 133 ++++++++++++++++++ 3 files changed, 145 insertions(+) create mode 100644 bench/results/lambda-and-pm-additions-2026-05-10.md diff --git a/Makefile b/Makefile index 9a971d1..2071fee 100644 --- a/Makefile +++ b/Makefile @@ -892,6 +892,15 @@ textbook-dedekind: ## Dedekind Essays on the Theory of Numbers 1901 (PD, PG #210 $(ARBORIST) --db "$(CRAWL_SHARDS_DIR)/textbook_dedekind-essays-theory-numbers.db" \ ingest --source textbook_tex --url "$$url" +textbook-plfa: ## PLFA - Programming Language Foundations in Agda (CC-BY-4.0) + $(MAKE) textbook ID=plfa-wadler-kokke-siek + +textbook-sf-lf: ## Software Foundations Vol 1 Logical Foundations (MIT, Pierce et al.) + $(MAKE) textbook ID=sf-pierce-logical-foundations + +textbook-pm: ## Whitehead-Russell Principia Mathematica Vol 1 (PD, PG #78050 — preface+intro only) + $(MAKE) textbook ID=whitehead-russell-pm-vol1-1910 + test-crawler: bootstrap-crawler ## run only the lifted crawler tests $(VENV)/bin/pytest -q tests/crawler diff --git a/bench/fixtures/textbooks/manifest-v1.jsonl b/bench/fixtures/textbooks/manifest-v1.jsonl index 25fc2ec..cc67d00 100644 --- a/bench/fixtures/textbooks/manifest-v1.jsonl +++ b/bench/fixtures/textbooks/manifest-v1.jsonl @@ -18,3 +18,6 @@ {"id":"russell-pom-1903","title":"The Principles of Mathematics","author":"Bertrand Russell (Klement HTML typesetting 2024)","year":"1903 (orig.); 2024 (Klement HTML reformat)","license":"CC-BY-SA-4.0","license_url":"https://creativecommons.org/licenses/by-sa/4.0/","domain":"logic-foundations","pillar_targets":["I","II"],"urls":["https://people.umass.edu/klement/pom/pom.html"],"home_url":"https://people.umass.edu/klement/pom/","notes":"Kevin C. Klement's HTML typesetting of Russell's 1903 *Principles of Mathematics*. Russell's text is PD (1903 + URAA expired); Klement's typesetting is CC-BY-SA-4.0. Single-page HTML (~25K lines / ~1MB). Russell PoM is more class-theoretic and ZFC-foundational than IMP 1919 (PoM was the precursor to Principia Mathematica). Pillar I/II coverage extension: contains Russell's Paradox derivation, class theory, relations, magnitudes — what IMP and PM leave for the technical reader. Cited by claim-pack as Mendelson/Enderton substrate."} {"id":"laplace-philosophical-essay-probabilities","title":"A Philosophical Essay on Probabilities","author":"Pierre-Simon Laplace (Truscott + Emory transl. 1902)","year":"1814 (French orig.); 1902 (English Truscott-Emory)","license":"PD","license_url":"https://en.wikipedia.org/wiki/Public_domain","domain":"probability","pillar_targets":["V"],"urls":["https://www.gutenberg.org/cache/epub/58881/pg58881-images.html"],"home_url":"https://www.gutenberg.org/ebooks/58881","notes":"PG eBook #58881, single-page HTML. Laplace 1814 *Essai philosophique sur les probabilités* is the foundational popular treatise on probability — predates Kolmogorov 1933 by 119 years but covers expected value, conditional probability, additive law, large-numbers reasoning, applications to natural philosophy. PD by age (Truscott-Emory English 1902 = pre-1929 US PD). Pillar V substrate; Kolmogorov 1933 axiomatizes what Laplace introduces narratively."} {"id":"dedekind-essays-theory-numbers","title":"Essays on the Theory of Numbers (I. Continuity and irrational numbers, II. The nature and meaning of numbers)","author":"Richard Dedekind (Wooster Woodruff Beman, transl. 1901)","year":"1872 + 1888 (German orig.); 1901 (English Beman)","license":"PD","license_url":"https://en.wikipedia.org/wiki/Public_domain","domain":"arithmetic","pillar_targets":["III"],"urls":[],"home_url":"https://www.gutenberg.org/ebooks/21016","tex_url":"https://www.gutenberg.org/files/21016/21016-t/21016-t.tex","notes":"PG eBook #21016 — TeX-only (no HTML edition); ingest via textbook_tex pipeline (proven against Hilbert + Boole + Peano). Dedekind is the OTHER pillar III primary alongside Peano: 'Was sind und was sollen die Zahlen?' (1888) introduced the chains-and-induction definition of natural numbers; 'Stetigkeit und irrationale Zahlen' (1872) is the cuts construction of the reals. Beman 1901 English. PD by age. Closes the induction / completeness side of Landau citations that Peano alone misses."} +{"id":"plfa-wadler-kokke-siek","title":"Programming Language Foundations in Agda","author":"Philip Wadler, Wen Kokke, Jeremy G. Siek","year":"2018+ (continuously revised)","license":"CC-BY-4.0","license_url":"https://creativecommons.org/licenses/by/4.0/","domain":"lambda-calculus","pillar_targets":["IX"],"urls":[],"home_url":"https://plfa.github.io/","crawl_url":"https://plfa.github.io/","crawl_depth":2,"crawl_max":60,"notes":"Open-source Agda + lambda calculus textbook from University of Edinburgh; CC-BY-4.0 explicit. Covers introduction to lambda calculus, untyped lambda calculus with full normalisation, Confluence/Church-Rosser, simply-typed lambda calculus, properties (progress + preservation), de Bruijn representation. Pillar IX substrate for the 7-record Barendregt block (β/α/η-conversion, Church-Rosser theorem, fixed-point, Turing completeness)."} +{"id":"sf-pierce-logical-foundations","title":"Software Foundations Volume 1: Logical Foundations","author":"Benjamin C. Pierce et al. (Penn)","year":"2007+ (continuously revised)","license":"MIT","license_url":"https://opensource.org/licenses/MIT","domain":"logic-foundations","pillar_targets":["I","III","IX"],"urls":[],"home_url":"https://softwarefoundations.cis.upenn.edu/lf-current/","crawl_url":"https://softwarefoundations.cis.upenn.edu/lf-current/toc.html","crawl_depth":2,"crawl_max":40,"notes":"Coq-based open textbook on logical foundations of programming languages from UPenn; MIT-licensed (verified against included LICENSE file in lf-current/lf.tgz). Covers basic functional programming, induction, lists, polymorphism + higher-order functions, propositional logic, indexed propositions, total + partial relations, lambda calculus, simply-typed lambda calculus. Pillar III substrate (induction primary) + pillar IX substrate (lambda calculus). Caveat: heavy Coq syntax; the prose-to-code ratio is lower than PLFA."} +{"id":"whitehead-russell-pm-vol1-1910","title":"Principia Mathematica, Volume 1 (Preface + Introduction + Chapters I-III)","author":"Alfred North Whitehead + Bertrand Russell","year":"1910 (Cambridge)","license":"PD","license_url":"https://en.wikipedia.org/wiki/Public_domain","domain":"logic-foundations","pillar_targets":["I","II"],"urls":["https://www.gutenberg.org/cache/epub/78050/pg78050-images.html"],"home_url":"https://www.gutenberg.org/ebooks/78050","notes":"PG eBook #78050, single-page HTML — Volume 1 Preface + Introduction + Chapters I-III only (~20-25% of full Vol 1; the *1 through *97 numbered propositions / type theory formalization not in this excerpt). Includes discussion of paradox resolution + theory of types in narrative form. Pillar I/II — supplementary substrate; the formal type-theoretic Russell's Paradox Resolution lives in the missing body, but the conceptual treatment is here. PD by age (1910 + URAA = 95 years = 2005)."} diff --git a/bench/results/lambda-and-pm-additions-2026-05-10.md b/bench/results/lambda-and-pm-additions-2026-05-10.md new file mode 100644 index 0000000..addfe3a --- /dev/null +++ b/bench/results/lambda-and-pm-additions-2026-05-10.md @@ -0,0 +1,133 @@ +# PLFA + Software Foundations + PM Vol 1 ingest — 2026-05-10 + +**Date:** 2026-05-10 (UTC) +**Author:** blackops + fox +**Method:** added 3 more substrates targeting the lambda-calculus +gap (pillar IX) + the type-theoretic Russell's Paradox Resolution +record (pillar II), under fox's "yes, continue" directive. + +## Headline + +**62 → 68 / 92 records resolve (+6, 74% coverage).** Pillar IX +nearly closed; PLFA + Software Foundations between them caught all +the β/α/η-conversion + Church-Rosser + extensionality + fixed-point +records. + +| Pillar | Pre-turn | Post-turn | +|---|---|---| +| I (logic) | 10/13 | 10/13 | +| II (set theory) | 9/10 | 9/10 | +| III (arithmetic) | 7/13 | 7/13 | +| IV (geometry) | 18/18 | 18/18 | +| V (probability) | 1/5 | 1/5 | +| VI (classical phys) | 3/5 | 3/5 | +| VII (combinatorics) | 9/14 | 9/14 | +| IX (lambda + algebra) | 5/14 | **11/14** | +| **Total** | **62/92 (67%)** | **68/92 (74%)** | + +## Three new ingests + +### PLFA — Programming Language Foundations in Agda + +- Manifest `id: plfa-wadler-kokke-siek`, license `CC-BY-4.0` +- Author: Philip Wadler, Wen Kokke, Jeremy G. Siek (Edinburgh CS) +- Source: `https://plfa.github.io/` (BFS depth=2 max=60) +- Landed: **58 docs / 413 chunks** +- Coverage: untyped lambda calculus, Confluence/Church-Rosser, + simply-typed lambda calculus, properties (progress + preservation), + de Bruijn representation, β/α/η reduction. Pillar IX core. + +### Software Foundations Vol 1 — Logical Foundations + +- Manifest `id: sf-pierce-logical-foundations`, license `MIT` + (verified against `lf-current/lf.tgz` LICENSE file) +- Author: Benjamin C. Pierce et al. (Penn CIS) +- Source: `https://softwarefoundations.cis.upenn.edu/lf-current/toc.html` + (BFS depth=2 max=40) +- Landed: **33 docs / 367 chunks** +- Coverage: Coq induction proofs, lists, polymorphism, propositional + logic, lambda calculus, simply-typed lambda calculus. Pillar III + + IX dual substrate. + +### Whitehead-Russell *Principia Mathematica* Volume 1 + +- Manifest `id: whitehead-russell-pm-vol1-1910`, license `PD` +- Source: PG eBook #78050 single-page HTML +- Landed: **1 doc / 231 chunks** +- Coverage: Preface + Introduction + Chapters I-III only (~20-25% + of full Vol 1). The *1-*97 numbered propositions / formal type + theory not in this excerpt; narrative discussion of paradox + types + is. Pillar II — supplementary substrate for Russell's Paradox + Resolution citation. + +## Four new citation aliases (decision_by="fox 2026-05-10") + +| Original | Substitute | Records lifted | +|---|---|---| +| Barendregt — Lambda Calculus Syntax & Semantics | PLFA (Wadler/Kokke/Siek) | +5 | +| Barendregt — Lambda Calculus Syntax & Semantics | Software Foundations LF (Pierce) | +1 | +| Jech — Set Theory | Whitehead-Russell PM Vol 1 | 0 (cascade miss) | +| Landau — Foundations of Analysis | Software Foundations LF (Pierce) | 0 (cascade miss) | + +## Title-haystack hack reverted + +Initial title backfill on PLFA + SF-LF appended `, Barendregt +substrate` to document titles — a haystack hack that would let the +resolver match Barendregt citations DIRECTLY against PLFA without +the alias mechanism, masking the substitution as DIRECT in audit +logs. Reverted to clean alias-driven matching: aliases register the +substitution explicitly, audit trail preserves who/why, and the +shard's title carries only its actual author signature +(`Wadler Kokke Siek` / `Pierce et al.`). + +## Honest gaps remaining (24 records) + +| Pillar | Stuck | Blocker | +|---|---|---| +| I (3) | Existential Introduction, Vacuous Quantification, Double Negation Elimination | natural-deduction proof-theory; Hilbert-Ackermann 1928 would close (no PD HTML found) | +| II (1) | Russell's Paradox Resolution | PM Vol 1 PG #78050 has only intro material; *24 onward (formal types) not transcribed | +| III (6) | Axiom of Zero / Distinctness / Injectivity of Successor / Induction Schema / Commutativity / Distributivity | Peano + Dedekind + SF-LF cascades all miss; symbolic axioms vs prose-keyword cascade mismatch | +| V (4) | Kolmogorov 3 axioms + Inclusion-Exclusion | Laplace 1814 doesn't axiomatize σ-algebras; Kolmogorov 1933 itself URAA-blocked until 2058 | +| VI (2) | Newton's Third Law, Conservation of Momentum | 1729 vocab mismatch; term-aliases registered but cascade tokens miss | +| VII (5) | Empty-Set/Boundary, Hockey-Stick, Vandermonde, Catalan, Stars-and-Bars | Bogart skews intro; advanced enumerative identities not named | +| IX (3) | Turing Completeness of λ-Calculus, Böhm-Jacopini Theorem, Orbit-Stabilizer | Turing/Böhm not in PLFA core; Orbit-Stabilizer cascade miss in Judson | + +## Cumulative session — 2026-05-10 + +| Snapshot | Resolved | % | Drivers | +|---|---|---|---| +| Start | 18/92 | 20% | Hilbert pillar IV only | +| 3 high-conf aliases | 33/92 | 36% | Goldstein/Newton, Stanley/Bogart, Dummit-Foote/Judson | +| Newton recrawl | 35/92 | 38% | deeper Principia text | +| 7 medium-conf aliases | 39/92 | 42% | Mendelson/Enderton/Jech/Landau | +| Peano + title backfill | 54/92 | 59% | Peano + author-surname haystack fix | +| 3 new textbooks (Russell PoM + Laplace + Dedekind) | 62/92 | 67% | pillar I/II jumped | +| **PLFA + SF-LF + PM Vol 1** | **68/92** | **74%** | **this turn — pillar IX** | + +**Day's lift: +50 records absolute (+54 pp).** + +## Reproducibility + +```bash +make textbook-plfa # CC-BY-4.0 BFS crawl, ~58 docs +make textbook-sf-lf # MIT BFS crawl, ~33 docs +make textbook-pm # PG #78050 single-page HTML +arborist warrant-resolve --use-aliases --write +# → 68 / 92 (74%) +``` + +## References + +- `#000041` — citation-aliases mechanism (19 rows live total) +- `#000042` — term-aliases mechanism (6 rows live total) +- `#000031` — surface-ingest cited textbooks; Phase 1 follow-up + (source-side title-from-author backfill) deferred +- `#000038` — Phase 4 content acquisition; remaining acquisition + candidates without HTML editions: Hilbert-Ackermann 1928, + Whitehead-Russell PM Vol 1 *24-*97 (full), Kolmogorov 1933 + (URAA-blocked) +- Today's bench journals (chronological): + - `bench/results/citation-aliases-batch-2026-05-10.md` + - `bench/results/medium-confidence-aliases-and-peano-2026-05-10.md` + - `bench/results/three-more-textbooks-2026-05-10.md` + - this file: `bench/results/lambda-and-pm-additions-2026-05-10.md`