From cc7749419cee4b4301c79c004c78e9fc76098c43 Mon Sep 17 00:00:00 2001 From: "Terence M. Rokop" Date: Tue, 4 Aug 2026 08:31:30 -0700 Subject: [PATCH 1/9] doc: add the Bellantoni-Cook design spec --- .../2026-08-04-bellantoni-cook-design.md | 1023 +++++++++++++++++ 1 file changed, 1023 insertions(+) create mode 100644 docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md diff --git a/docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md b/docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md new file mode 100644 index 0000000..d05991e --- /dev/null +++ b/docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md @@ -0,0 +1,1023 @@ +# Bellantoni-Cook syntax and semantics — design + + + + +- [Purpose](#purpose) +- [Sources](#sources) + - [Per-definition classification](#per-definition-classification) + - [Deviation 1: the class is the reformulation, not the original](#deviation-1-the-class-is-the-reformulation-not-the-original) + - [Deviation 2: `cond` argument order](#deviation-2-cond-argument-order) + - [Deviation 3: the syntax is a slice W-type](#deviation-3-the-syntax-is-a-slice-w-type) + - [Deviation 4: shapes carry the composition arities](#deviation-4-shapes-carry-the-composition-arities) + - [Deviation 5: environments as functions](#deviation-5-environments-as-functions) + - [Deviation 6: names](#deviation-6-names) + - [The paper's `mult` is ill-formed as printed](#the-papers-mult-is-ill-formed-as-printed) + - [Licence](#licence) +- [Design](#design) + - [Alternatives considered](#alternatives-considered) + - [Placement and file manifest](#placement-and-file-manifest) + - [The index and the signature](#the-index-and-the-signature) + - [The syntax](#the-syntax) + - [Finiteness and decidable admissibility](#finiteness-and-decidable-admissibility) + - [The semantics](#the-semantics) + - [Exposure](#exposure) + - [Reuse](#reuse) +- [Verification evidence](#verification-evidence) +- [Tests](#tests) +- [Documentation](#documentation) +- [Non-goals](#non-goals) +- [Deferred](#deferred) +- [Constraints](#constraints) + + + +## Purpose + +Define in Lean the syntax of the function class `B` of +[HeraudNowak2011] § 3.2 and its interpretation. + +The consumer is the translation to Cobham's class (Theorems 1 +and 2), which is what makes `B` a characterization of the +polynomial-time functions. It is § Deferred item 3, and this branch +adds it to `TODO.md` together with the two items it depends on and +the four triggers of § Deferred. That consumer is the whole +justification under CONTRIBUTING.md § Code is cost; the syntax and +the semantics are the definitions its statement quantifies over, +and nothing already in the tree consumes them. + +## Sources + +The paper is Sylvain Héraud and David Nowak, *A Formalization of +Polytime Functions*, arXiv:1102.5495 (v2, 31 May 2011). A short +version appeared as ITP 2011, LNCS 6898, pp. 119-134, +`doi:10.1007/978-3-642-22863-6_11`. Every section and page number +here is the arXiv version's, which is the source of record; the +short version is not established to carry the same numbering. + +The reference implementation is the Coq development +`github.com/davidnowak/bellantonicook` (opam +`coq-bellantonicook`), at commit +`1f03b9296104646ddc2b2b4b12e35a6619c17a99` (2018-09-13). Every +line number below is that revision's. +`src/BellantoniCook/BC.v` carries the syntax (12-19), the arity +apparatus (`Inductive Arities` 85-89, `aeq` 91-95, +`Fixpoint arities` 115-143, `arities2` 145-149), and the semantics +(`sem_rec` 380-386, `sem` 388-422). + +### Per-definition classification + +CONTRIBUTING.md § Cite the literature when transcribing requires +each definition to be marked transcription or novel. + +| Definition | Classification | +| --- | --- | +| the seven constructor forms of `B` | transcription, § 3.2 | +| the arity relation `A` | transcription, § 3.2 | +| every semantic clause | transcription, § 3.2 (with Deviation 2) | +| `plus`, `mult` and their subterms `plusStep`, `multBase`, `multStep` (test module) | transcription, § 3.2, corrected per § The paper's `mult` is ill-formed as printed | +| `Shape`, `Direction`, `rc`, `q`, `sig` | novel | +| `BC`, `BC.arity`, `BCOf` | novel | +| `Sem`, `transport`, `evalRec`, `evalValue`, `evalStep`, `BC.eval` | novel realisations of the transcribed clauses | +| `finEnumFin`, `finEnumCompDirection`, `sigFinitary` | novel | +| `compChildren`, `branchRec`, `badRaw`, `plusOf`, `multOf`, the `Raw` bindings and the four leaf terms `predTerm`, `condTerm`, `projNTerm`, `projSTerm` (test module) | novel | + +### Deviation 1: the class is the reformulation, not the original + +The class defined here is not Bellantoni and Cook's. Paper p. 6: + +> Reader may have noticed that our definition of Bellantoni-Cook's +> class is slightly different from the one in [6]. First, here the +> conditional `cond` distinguishes between three cases (empty, even +> or odd bitstrings), whereas in [6] the empty bitstring is treated +> as an even one. Second, here the base case for recursion is the +> empty bitstring, whereas in [6] it is any bitstring whose +> interpretation as a positive integer is 0 … + +Both differences are realised here: `cond` takes four safe +arguments and branches three ways, where the original branches two +ways on parity; and `evalRec`'s base clause is `[] ↦ g`, where the +original's is every zero-valued bitstring. The module docstring +states this and cites [HeraudNowak2011] and [BellantoniCook1992]. + +### Deviation 2: `cond` argument order + +The paper and its reference implementation disagree. Paper § 3.2 +gives `cond(; ε, x, y, z) = x`, `cond(; w0, x, y, z) = y`, +`cond(; w1, x, y, z) = z` — even selects the third safe argument, +odd the fourth. `BC.v:399-404` matches on the first of four safe +arguments and gives `| nil ↦ b`, `| true :: _ ↦ c`, +`| false :: _ ↦ d` — odd selects the third, even the fourth. + +This design follows the reference implementation. Rationale: the +implementation is the artifact against which the paper's theorems +were machine-checked, so its clause is the one the published +results certify; the paper's prose carries no corresponding check. +The implementation corroborates its own reading at `BC.v:455-457`, +where `cond_simpl_true` takes the hypothesis +`hd false (sem fc l1 l2) = true` and concludes with the third safe +argument. The module docstring records the discrepancy. + +The bit tested is the least significant: `Bitstring.v:50-55` gives +`bs2nat (false :: v') = 2 * bs2nat v'` and +`bs2nat (true :: v') = S (2 * bs2nat v')`, so the list head is the +low bit and the paper's `w0` is `false :: w`. + +### Deviation 3: the syntax is a slice W-type + +The Coq syntax is an untyped `Inductive BC` whose well-formedness +is carried by a separate `arities` function, with a semantics total +on ill-formed terms: an out-of-range projection yields the empty +bitstring, and `cond` carries three further clauses for safe +environments shorter than four (`BC.v:405-416`). + +Here the arity pair is an index. `docs/rules/lean-coding.md` +§ Recursion and induction through recursors forbids a +self-referential `inductive` and a self-calling `def`, so the +indexed syntax is the slice W-type of a signature functor over +`ℕ × ℕ` and the semantics is one application of its eliminator. +Consequences: + +- Only terms satisfying the arity relation inhabit `BCOf n s`, so + the reference implementation's default values are unreachable. +- The four hand-written induction principles of the reference + implementation (`BC_ind2'` 21-57, `BC_ind2` 59-77, + `BC_ind_inf'` 207-335, `BC_ind_inf` 337-367 — 216 lines) are + replaced by `SlicePFunctor.W.elim` and + `SlicePFunctor.W.induction`. Two reasons are given for them in + the source: `BC.v:8-9`, that Coq's generated recursor ignores the + `list BC` fields of `comp`, covers the first two; `BC.v:377`, + that `BC_ind_inf` "makes easier dealing with arities in inductive + proofs", covers the other two. +- The arity function is not ported as a term-level checker, so the + paper's "polytime checker" reading is not delivered. + `SlicePFunctor.decidableWValid` makes admissibility of a raw tree + decidable, so a checker is recoverable from what is already here. + Deferred. + +The paper's `B_inf` (§ 3.2, final two paragraphs, running onto +p. 8; `BCI.v:4-12`) replaces the single projection with `projIn` +and `projIs` and drops the arity annotations from `proj` and +`comp`. It is not ported. + +### Deviation 4: shapes carry the composition arities + +`Shape.comp` carries `n s m k` where the paper's `comp^{n,s}` +carries two superscripts. In the paper `m` and `k` are determined +by `|gN|`, `|gS|` and `A(h)`; here they must appear in the shape, +because `Direction` is a function of the shape alone and the number +of subterms depends on them. The correspondence is bijective on +well-formed terms: a term of `sig.W` with root shape +`comp n s m k` has exactly `m` normal and `k` safe argument +subterms, and its head subterm has arity `(m, k)`. + +### Deviation 5: environments as functions + +The Coq semantics takes two `list bs` and indexes them with `nth`, +defaulting to the empty bitstring. Here an environment is a +function `Fin n → List Bool`, total by construction, and the +semantics uses `Fin.append`, `Fin.cons` and `Fin.tail`. + +### Deviation 6: names + +`rec` cannot name a `Shape` constructor: `Shape.rec` is the +generated recursor (`inductive Foo | a | rec` fails +with `(kernel) constant has already been declared 'Foo.rec'`). The +shape is `safeRec`, after the standard term for the scheme; the +paper writes `rec`, Bellantoni and Cook "predicative recursion on +notation". `comp` keeps the paper's name. + +The semantics is `eval`, after mathlib's `Nat.Partrec.Code.eval`, +so that `e.eval` is available for `e : BC`. + +### The paper's `mult` is ill-formed as printed + +Page 7 prints +`mult := rec (comp^{1,0} O ⟨⟩ ⟨⟩) (comp^{1,2} plus ⟨π₁^{2,0}⟩ ⟨π₂^{2,1}⟩) (…)` +with `A(mult) = (2, 0)`. The recursion rule of p. 6 forces +`A(h_i) = (2, 1)`, so the superscripts must be `comp^{2,1}`; the +arguments confirm it independently, since `π₁^{2,0}` forces `n = 2` +and `π₂^{2,1}` forces `s = 1`. The reference implementation has +`comp^{2,1}`: `BCUnary.v:233` reads +`comp 2 1 plus_e ((proj 2 0 1) :: nil) ((proj 2 1 2) :: nil)`. +The printed step superscript coincides with `plus`'s, where +`comp^{1,2}` is correct. The printed base superscript +`comp^{1,0}` has no counterpart in `plus` and is correct as +printed. + +Under this design a literal transcription of the printed term +fails `decide`: `Shape.comp 1 2 1 1` requires its normal-argument +subterm at index `(1, 0)`, while `proj 2 0 1` carries `(2, 0)`. +§ Tests transcribes the reference implementation's arities. + +### Licence + +The reference development ships the CeCILL Free Software Licence +Agreement v2.1, though its README and opam metadata both name +CeCILL-A. Either way it is copyleft, and this repository is +Apache-2.0. No code is taken from it: the definitions are +transcribed from the paper, and Deviation 2 quotes three match arms +of `BC.v` as evidence for a factual claim about the two sources. +The development is catalogued in `docs/references.md`, which is +where the repository records external library pointers; no +attribution notice is added to the module. + +## Design + +### Alternatives considered + +**A `Geb/Cslib/` module over mathlib's `WType`,** targeting CSLib +instead. `Geb/Cslib/` may not import `Geb.Mathlib.*` +(`docs/rules/upstream-eligible.md:127`), so this route cannot use +the slice W-type: `WType` is unindexed, and the +index-and-admissibility fold (`Slice/W.lean:188-190`, itself a +`WType.elim`) and its decidability (`Slice/Decidable.lean:128`) +would be restated for this signature — perhaps 40 to 60 lines, +since only one signature is involved, not the 413-line general +`Slice/W.lean`. The arity relation would become a predicate to +reason about rather than the maps `q` and `rc`, and the checker of +§ Deviation 3 would be built rather than instantiated. Both routes are +upstream-eligible, so the choice is not between upstreaming and +not. + +The slice-W route is chosen on those two grounds — it restates +nothing, and it makes the arity relation data, the maps `q` and +`rc`, rather than a predicate, which is what § Deviation 3's +`BCOf` and the deferred checker rest on. Its own overhead is the +`@[expose]` discipline, the `@[reducible]` calibration recorded +below, and two `FinEnum` instances existing only to feed +`decidableWValid`, which is the smaller of the two. The subtree, +and with it the upstream target, follows from that choice rather +than preceding it: the slice W-type is `Geb.Mathlib.*`, which only +`Geb/Mathlib/` may import. + +**A uniform `Fin` `Direction`,** taking `Fin (1 + (m + k))` for +`comp` and splitting it with `Fin.cases` and `Fin.addCases`. That +leaves one `FinEnum` obligation instead of two, and lets every test +term's children be written with `![…]`. Against it: `rc` and +`evalValue`'s `comp` clause become index arithmetic rather than +case distinctions on a sum. The sum is kept, and § Tests pays the +cost with one `compChildren` helper. + +### Placement and file manifest + +| Path | Change | +| --- | --- | +| `docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md` | this spec; added, then removed | +| `docs/superpowers/plans/…` | the plan; added, then removed | +| `Geb/Mathlib.lean` | one `public import` added, in the form of `:8-10` | +| `Geb/Mathlib/Computability.lean` | new; the directory index, titled `# Computability — index` after `Geb/Mathlib/Data.lean` (a title naming `Geb.Mathlib.` would fail `scripts/lint-imports.sh`'s self-prefix check) | +| `Geb/Mathlib/Computability/BellantoniCook.lean` | new; the content | +| `GebTests/Mathlib.lean` | one import added, matching that file's existing form | +| `GebTests/Mathlib/Computability.lean` | new; the test directory index, titled `# Computability tests — index` after `GebTests/Mathlib/Data.lean` | +| `GebTests/Mathlib/Computability/BellantoniCook.lean` | new; the tests | +| `docs/references.bib` | two entries added | +| `docs/references.md` | one pointer added | +| `docs/index.md` | one bullet added | +| `TODO.md` | one subsection added, plus four trigger entries; its doctoc TOC re-run in the same commit | + +Commit order: the spec, then the plan, then the library module, +then the test module, then the documentation, then a final commit +removing the spec and the plan (CONTRIBUTING.md § Concern shape). + +The subtree is `Geb/Mathlib/`, whose allowed imports are +`Mathlib.*`, `Batteries.*` and `Geb.Mathlib.*` +(`docs/rules/upstream-eligible.md` § Subtree import rules; +`scripts/lint-imports.sh:179-180`). The design's only non-mathlib +import, `Geb.Mathlib.Data.PFunctor.Slice.*`, is a `Geb.Mathlib.*` +module, so the placement is legal with no rule change and the +module stays upstream-eligible. `Geb/Cslib/` is excluded: it may +not import `Geb.Mathlib.*` at all +(`docs/rules/upstream-eligible.md:127`), CSLib PRs having no access +to unupstreamed mathlib-targeted content. + +The upstream target is mathlib4. `Mathlib/Computability/` already +carries this artifact's construction: `Nat.Partrec.Code` +(`Mathlib/Computability/PartrecCode.lean:76`, `eval` at `:464`) is +a deep-embedded syntax with an `eval`, as `BC` and `BC.eval` are, +and `Nat.Primrec` and `Nat.Partrec` are the recursion-theoretic +material `B` sits beside. CSLib has a claim too — +`Cslib/Computability/README.md` names "complexity classes" in its +scope, where mathlib's complexity content is confined to +machine-model resource bounds (`TM2ComputableInPolyTime` and +relatives, in `TuringMachine/Computable.lean`). It is not taken, +because § Alternatives considered chooses the slice-W encoding on +technical grounds and only `Geb/Mathlib/` can host it. Were the +encoding ever revisited, the target would be open again. + +`scripts/extract-pr.sh:52-62` maps `Geb/Mathlib/*` to `Mathlib/` +and so extracts this module correctly. Its own comment records +that the mapping is an over-approximation for modules targeting +Lean core or Batteries; that reservation does not reach this one. + +Under § Floodgate test the branch stays ready to ship +dependency-ordered PRs: `B` ships after +`Geb/Mathlib/Data/PFunctor/Slice/`. That is ordinary here — 45 +non-index modules under `Geb/Mathlib/` already import +`Geb.Mathlib.*` siblings, 24 of them from another directory, as +`CategoryTheory/FinSetSkel/Quotient.lean:8-11` does. + +`Geb/Mathlib/Computability.lean` and its test counterpart are +directory index files, one per directory as the subtree's existing +`Data.lean`, `CategoryTheory.lean` and `Logic.lean` are. The +content is one module: this workstream states no lemmas, so nothing +separates a `Defs`/`Basic` split. + +All library declarations sit in `namespace BellantoniCook` — a +top-level namespace in mathlib's manner (`Turing`, `Language`), and +carrying no `Geb.Mathlib.` self-prefix, which +`docs/rules/upstream-eligible.md` forbids in namespace +declarations. `arity` and `eval` are written inside that namespace +as `def BC.arity` and `def BC.eval`, so that `e.arity` and `e.eval` +resolve for `e : BC`. + +Bitstrings are `List Bool` written directly. mathlib offers no +other carrier: `BitVec n` is fixed-width, `Nat.bits` cannot +distinguish +`0` from `00` (the paper's stated reason for leaving positive +integers), `FreeMonoid Bool` is `List Bool` plus unwanted +structure, and `Mathlib/Computability/Encoding.lean:94` itself uses +`List Bool`. + +### The index and the signature + +The index is `I := ℕ × ℕ`, the pair of normal and safe arities. All +four universe parameters are `0` and no universe annotation is +needed. + + inductive Shape + | zero + | proj (n s : ℕ) (i : Fin (n + s)) + | succ (b : Bool) + | pred + | cond + | safeRec (n s : ℕ) + | comp (n s m k : ℕ) + + @[expose, reducible] def Direction : Shape → Type + | .zero => Fin 0 + | .proj _ _ _ => Fin 0 + | .succ _ => Fin 0 + | .pred => Fin 0 + | .cond => Fin 0 + | .safeRec _ _ => Fin 3 + | .comp _ _ m k => Unit ⊕ Fin m ⊕ Fin k + + @[expose, reducible] def rc : (a : Shape) → Direction a → ℕ × ℕ + | .zero, i => i.elim0 + | .proj _ _ _, i => i.elim0 + | .succ _, i => i.elim0 + | .pred, i => i.elim0 + | .cond, i => i.elim0 + | .safeRec n s, ⟨0, _⟩ => (n, s) + | .safeRec n s, _ => (n + 1, s + 1) + | .comp _ _ m k, .inl () => (m, k) + | .comp n _ _ _, .inr (.inl _) => (n, 0) + | .comp n s _ _, .inr (.inr _) => (n, s) + + @[expose, reducible] def q : Shape → ℕ × ℕ + | .zero => (0, 0) + | .proj n s _ => (n, s) + | .succ _ => (0, 1) + | .pred => (0, 1) + | .cond => (0, 4) + | .safeRec n s => (n + 1, s) + | .comp n s _ _ => (n, s) + + @[expose] def sig : SlicePFunctor (ℕ × ℕ) (ℕ × ℕ) where + A := Shape + B := Direction + r := fun x ↦ rc x.1 x.2 + q := q + +`Shape` is non-recursive — no field mentions `Shape` — so +§ Recursion and induction through recursors does not reach it: the +rule's subject is self-reference, which `sig.W` carries, and a +non-recursive `inductive` is exactly the shape set `A` of a +`PFunctor`. `GebTests/Mathlib/Data/PFunctor/Presheaf/Fixtures.lean:129-134` +declares `inductive Shp` in the same role, with a hand-written +choice-free `FinEnum Shp` at 137. + +`Shape` carries no `deriving` clause. § Structure and typeclass +patterns' standard derivations would all apply — its fields are +`ℕ`, `Bool` and `Fin` — but nothing here consumes them, and +`DecidableEq`/`Repr` for `BC` are § Deferred item 6, which is where +a derivation on `Shape` would be introduced alongside its lift. + +`q` is the paper's arity relation read as a function of the shape +and `rc` is its hypotheses. `rc`'s `safeRec` clauses match +`Fin.mk 0` first, so direction `0` is `g` and directions `1` and +`2` are `h₀` and `h₁`. `comp`'s `inr (inl i) ↦ (n, 0)` is the +paper's "the functions in `gN` only have access to normal +variables"; `safeRec`'s directions `1` and `2` at `(n+1, s+1)` are +its `n_h = n_g + 1`, `s_h = s_g + 1`. + +`Direction`, `rc` and `q` carry `@[reducible]`, not +`@[implicit_reducible]`. Measured: with `implicit_reducible` every +numeral in § The semantics fails, thirteen errors of the form +`failed to synthesize instance of type class OfNat (Fin (q +(Shape.succ b)).2) 0`; `implicit_reducible` governs unification at +implicit transparency inside dependent types, which is what +`Slice/Basic.lean:83-87` documents it for, whereas `OfNat` +synthesis needs `reducible`. With `@[expose, reducible]` every +clause elaborates with no binder ascriptions. + +### The syntax + + @[expose] def BC : Type := sig.W + @[expose] def BC.arity : BC → ℕ × ℕ := sig.wIndex + @[expose] def BCOf (n s : ℕ) : Type := { e : BC // e.arity = (n, s) } + +`sig.W` is the admissibility subtype of `sig.toPFunctor.W` +(`Geb/Mathlib/Data/PFunctor/Slice/W.lean:221`), so a term of `BC` +is a raw tree together with a proof that every node's children +carry the indices `rc` prescribes. `BCOf n s` is the type of +expressions `e` with `A(e) = (n, s)`: it is what makes the arity +relation of § 3.2 a type rather than a side condition, and it is +what § Deferred item 3 quantifies over — Theorem 1 reads "for all +`f` in `B` with well defined arities `A(f)`, there exists `f'` in +`C` such that …", which is a statement about arity-indexed terms. +It is also what the deferred checker returns. + +### Finiteness and decidable admissibility + +`SlicePFunctor.decidableWValid` +(`Geb/Mathlib/Data/PFunctor/Slice/Decidable.lean:128`) requires +`DecidableEq I`, free for `ℕ × ℕ`, and `sig.toPFunctor.Finitary`, +which is `∀ a, FinEnum (sig.toPFunctor.B a)` +(`Geb/Mathlib/Data/PFunctor/Univariate/Finitary.lean:38`). + +The mathlib `FinEnum` instances this signature would resolve +through depend on `Classical.choice` — measured for `Fin n`, for +`PEmpty` and for sums, and `TODO.md:363-366` records the same for +`FinEnum.fin` and `ULift.instFinEnum`. Resolving `sigFinitary` +through them taints the module and fails `lake lint`, whose +permitted set is `standardAxioms = {propext, Quot.sound}` +(`GebMeta.lean:46-49`, checked by `detectNonstandardAxiom` at +`:113`; run by `scripts/pre-push.sh:30,39`). Two named choice-free +instances are supplied, following `Fixtures.lean:137`: + + scoped instance finEnumFin (n : ℕ) : + FinEnum (Fin n) where + card := n + equiv := Equiv.refl _ + decEq := inferInstance + + scoped instance finEnumCompDirection (m k : ℕ) : + FinEnum (Unit ⊕ Fin m ⊕ Fin k) where + card := 1 + (m + k) + equiv := (Equiv.sumCongr finOneEquiv.symm finSumFinEquiv).trans finSumFinEquiv + decEq := inferInstance + + instance sigFinitary : sig.toPFunctor.Finitary + | .zero => inferInstanceAs (FinEnum (Fin 0)) + | .proj _ _ _ => inferInstanceAs (FinEnum (Fin 0)) + | .succ _ => inferInstanceAs (FinEnum (Fin 0)) + | .pred => inferInstanceAs (FinEnum (Fin 0)) + | .cond => inferInstanceAs (FinEnum (Fin 0)) + | .safeRec _ _ => inferInstanceAs (FinEnum (Fin 3)) + | .comp _ _ m k => inferInstanceAs (FinEnum (Unit ⊕ Fin m ⊕ Fin k)) + +Four points, each measured: + +- `finEnumFin` and `finEnumCompDirection` are `scoped`. A bare + `instance` in the module's `public section` is global, and + `Geb.lean` re-exports `Geb.Mathlib`, so `finEnumFin` would + compete with `FinEnum.fin` at the same head symbol across the + repository: measured, `#synth FinEnum (Fin 3)` in a module + importing `Geb` returns `BellantoniCook.finEnumFin 3` when the + instance is bare and `FinEnum.fin` when it is `scoped`. + `Geb/Mathlib/CategoryTheory/FinCat/Decidable.lean:70` uses + `scoped instance` against the same pressure. Scoping costs the + test module nothing: `sigFinitary`'s branches resolve them by + `inferInstanceAs` from inside their own namespace, where they are + in scope and win on declaration order. +- `sigFinitary` is an `instance`, not a `def`: as a `def` it does + not fire for `decidableWValid`, and it draws `Definition … of + class type is semireducible`, fatal under `weak.warningAsError`. + As an `instance` it needs no attribute; + `GebTests/Mathlib/Data/PFunctor/Slice/Decidable.lean:49` declares + the analogous `finitaryTestSlice` bare. +- The branches are `inferInstanceAs`, not `inferInstance`: instance + search stops at reducible transparency on the projection + `sig.B a`, so a bare `inferInstance` reports + `failed to synthesize instance of type class FinEnum (sig.B + Shape.zero)`. + `GebTests/Mathlib/Data/PFunctor/Slice/Decidable.lean:46-48` + records the same for `decEq`, and does so where the signature is + an `abbrev`, so the cause is the projection, not `sig` being a + `def`. +- `finEnumFin` is built as a cardinality with `Equiv.refl`, the + construction `TODO.md` § PRA functors over finite-specification + base categories anticipates; `Geb/Mathlib/Data/FinEnum.lean:18-22` + documents the explicit-supply mitigation, available because the + instances are named. A trigger records that they move to + `Geb/Mathlib/Data/FinEnum.lean` when a second consumer appears; + moving them now would put a second concern on this branch. + +`finOneEquiv` is `Mathlib/Logic/Equiv/Defs.lean:907` and +`finSumFinEquiv` is `Mathlib/Logic/Equiv/Fin/Basic.lean:228`. + +### The semantics + + @[expose] def Sem : ℕ × ℕ → Type := + fun i ↦ (Fin i.1 → List Bool) → (Fin i.2 → List Bool) → List Bool + + @[expose] def transport {i j : ℕ × ℕ} (h : i = j) (v : Sem i) : Sem j := h ▸ v + +`transport` is named rather than written inline: `evalValue` uses +it six times, and a named function fixes the motive of `▸` once +instead of leaving it to be inferred at each site. + +The recursion on the bitstring `safeRec` consumes is `List.rec`, an +auto-generated recursor and so permitted: + + @[expose] def evalRec {n s : ℕ} (g : Sem (n, s)) + (h₀ h₁ : Sem (n + 1, s + 1)) : List Bool → Sem (n, s) := + List.rec g (fun b v ih x y ↦ + (if b then h₁ else h₀) (Fin.cons v x) (Fin.cons (ih x y) y)) + +`[] ↦ g` is Deviation 1's base case; `h₁` on `true` and `h₀` on +`false` is `BC.v:383-385`; the tail `v` becomes the new first +normal argument and the recursive value enters `h_b` in safe +position as `Fin.cons (ih x y) y`. + +The algebra is an auxiliary taking the compatibility hypothesis +pointwise, because the `Shape` match must generalize it: + + @[expose] def evalValue : (a : Shape) → (c : Direction a → Σ i, Sem i) → + (∀ b, (c b).1 = rc a b) → Sem (q a) + | .zero, _, _ => fun _ _ ↦ [] + | .proj _ _ i, _, _ => fun x y ↦ Fin.append x y i + | .succ b, _, _ => fun _ y ↦ b :: y 0 + | .pred, _, _ => fun _ y ↦ (y 0).tail + | .cond, _, _ => fun _ y ↦ + match y 0 with + | [] => y 1 + | true :: _ => y 2 + | false :: _ => y 3 + | .safeRec _ _, c, h => fun x y ↦ + evalRec (transport (h 0) (c 0).2) (transport (h 1) (c 1).2) + (transport (h 2) (c 2).2) (x 0) (Fin.tail x) y + | .comp _ _ _ _, c, h => fun x y ↦ + transport (h (.inl ())) (c (.inl ())).2 + (fun i ↦ transport (h (.inr (.inl i))) (c (.inr (.inl i))).2 x Fin.elim0) + (fun j ↦ transport (h (.inr (.inr j))) (c (.inr (.inr j))).2 x y) + + @[expose] def evalStep : + sig.toSliceDomPFunctor.Obj (Sigma.fst (β := Sem)) → Σ i, Sem i := + fun z ↦ ⟨sig.q z.1.1, + evalValue z.1.1 z.1.2 + ((sig.toSliceDomPFunctor.compatible_iff _ z.1.1 z.1.2).mp z.2)⟩ + + @[expose] def BC.eval : BC → Σ i, Sem i := + SlicePFunctor.W.elim sig (Σ i, Sem i) (Sigma.fst (β := Sem)) evalStep rfl + +`cond`'s indexing is `y 0` the tested bitstring, `y 1` the empty +case, `y 2` the odd case and `y 3` the even case — Deviation 2's +ordering. `comp`'s head child has arity `(m, k)` and is applied to +the normal arguments' values, each evaluated in the empty safe +environment `Fin.elim0`, and to the safe arguments' values. + +Returning `sig.q z.1.1` as `evalStep`'s first component makes the +eliminator's coherence obligation +`Sigma.fst ∘ evalStep = sig.obj Sigma.fst` hold by `rfl`. Note +`SlicePFunctor.W.elim sig …`, not `sig.W.elim …`: `sig.W` is a +type, not a term, so field notation does not chain through it. + +For `e : BCOf n s`, `e.property` rewrites the index of +`BC.eval e.val` to `(n, s)`; `SlicePFunctor.W.comp_elim` +(`W.lean:352`) is the lemma that the value's index is the tree's. + +### Exposure + +The library module opens a `public section`, and the thirteen +declarations shown above with `@[expose]` carry it — every one +except `Shape` and the three instances, which do not need it — +following +`Geb/Mathlib/Data/PFunctor/Slice/W.lean:132` and the rationale at +`:118`. The test module reduces `BC.eval` applications by `rfl` +across the module boundary, which needs the bodies of `BC.eval`, +`evalStep`, `evalValue`, `evalRec` and `transport`, and discharges +`sig.WValid` by `decide`, which needs `rc`. `sigFinitary` is +resolved by instance search rather than unfolded, so it needs no +`@[expose]`; measured, the tests succeed with all three instances +unexposed. + +The test module uses plain `import` and +`set_option linter.privateModule false`, following +`GebTests/Mathlib/Data/PFunctor/Slice/W.lean:25`. It opens +`BellantoniCook` for unqualified access to `sig`, `BC`, `BCOf` and +`BC.eval`. The `scoped` instances come into scope with it, but +nothing needs them to: `sigFinitary` names them from inside their +own namespace. Measured: the tests' `decide` and `rfl` both succeed with the +three instances unexposed and with no `open` at all. + +### Reuse + +| Coq | here | +| --- | --- | +| `if leb (S j) n then nth j vnl nil else nth (j-n) vsl nil` | `Fin.append x y i` | +| `v' :: vnl` / `tail vnl` / `nil` | `Fin.cons v x` / `Fin.tail x` / `Fin.elim0` | +| the four hand-written induction principles (216 lines) | `SlicePFunctor.W.elim`, `.induction` | +| `Arities`, `aeq`, `arities`, `arities2` | `q`, `rc`, `sig.wIndex` | +| `Fixpoint sem_rec` | `List.rec` | + +## Verification evidence + +Every declaration in § Design, and every test declaration named in +§ Tests, was built and elaborated against the repository toolchain +(v4.33.0-rc2) as two modules at library paths — the library with +`public section` and `@[expose]`, the tests with plain `import` and +`linter.privateModule false` — under the repository's option set +(`autoImplicit false`, `relaxedAutoImplicit false`, +`maxSynthPendingDepth 3`, `weak.linter.mathlibStandardSet true`, +`weak.linter.style.header true`, `weak.warningAsError true`, +`weak.linter.flexible true`, `pp.unicode.fun true`), with copyright +headers and module docstrings. Zero diagnostics on both. Measured: + +- `sig` elaborates as `SlicePFunctor.{0, 0, 0, 0} (ℕ × ℕ) (ℕ × ℕ)` + with no universe annotation. +- The coherence argument to `elim` is `rfl`. +- The transport is `h ▸ v`; no `Eq.mpr`, `cast`, `Subtype.ext` or + `simp` is required, and no clause needs a binder ascription once + `Direction`, `rc` and `q` are `@[reducible]`. +- `by decide` discharges admissibility across the module boundary + in 13.0 ms for `plus` and 22.1 ms for `mult` (25 nodes, + containing `plus` twice) at default `maxHeartbeats`. +- Every assertion of § Tests reduces by `rfl` across the module + boundary. The negative control `decide (sig.WValid badRaw)` + reduces to `false`. +- `#print axioms`: `sig` and `finEnumFin` depend on no axioms; + `sigFinitary`, `finEnumCompDirection`, `BC.eval`, `plus`, `mult` + and every assertion depend on `[propext, Quot.sound]`. Deleting + the two named instances, so that `sigFinitary` resolves through + mathlib's, yields `Classical.choice` on `sigFinitary`, `plus`, + `mult` and every assertion — not on `BC.eval`, which does not + depend on `sigFinitary`. Admissibility is where the taint would + enter, not evaluation. +- The `⟨WType.mk …, by decide⟩` form does not elaborate: instance + search fails to unify `decidableWValid`'s conclusion against a + goal containing an inline `WType.mk` application, reporting + `failed to synthesize Decidable (sig.WValid (WType.mk …))`. A + type ascription does not repair it; binding the raw tree as its + own `def` does, which is the form § Tests specifies. + +Recorded property: `Fin` numerals wrap, so a mistranscribed index +elaborates rather than failing — `(1 : Fin 1) = 0` and +`(5 : Fin 3) = 2` both close by `rfl`. This affects `proj`'s +`Fin (n + s)`, `cond`'s `y 0 … y 3` at `Fin 4`, and `safeRec`'s +`c 0 … c 2` at `Fin 3` alike. Only an expected-output check +distinguishes them, which is why every assertion states an output +and why § Tests carries `branchRec`. + +## Tests + +`GebTests/Mathlib/Computability/BellantoniCook.lean`. + +Each term is built in two steps, because the inline form does not +elaborate (§ Verification evidence): a raw tree bound as its own +`def` at type `sig.toPFunctor.W`, then the admissible term. + + def compChildren {m k : ℕ} (h : sig.toPFunctor.W) + (gN : Fin m → sig.toPFunctor.W) (gS : Fin k → sig.toPFunctor.W) : + Unit ⊕ Fin m ⊕ Fin k → sig.toPFunctor.W := + Sum.elim (fun _ ↦ h) (Sum.elim gN gS) + + def plusStepRaw : sig.toPFunctor.W := + WType.mk (.comp 1 2 0 1) + (compChildren (WType.mk (.succ true) Fin.elim0) Fin.elim0 + ![WType.mk (.proj 1 2 1) Fin.elim0]) + def plusStep : BC := ⟨plusStepRaw, by decide⟩ + +and likewise for the rest. `m` and `k` are implicit and solved by +unification against the expected `Direction (.comp …)`, which is +`@[reducible]` and reduces to the codomain's own +`Unit ⊕ Fin m ⊕ Fin k`. The codomain is written as that sum rather +than as `Direction (.comp n s m k)`, which would leave `n` and `s` +free and fail under `autoImplicit false`. + +Every term is bound this way, leaves included: the two-step form is +required wherever a `by decide` goal mentions the tree, so each of +`plusStepRaw`, `plusRaw`, `multBaseRaw`, `multStepRaw`, `multRaw`, +`branchRecRaw`, `predTermRaw`, `condTermRaw`, `projNTermRaw`, +`projSTermRaw` and `badRaw` is its own `def` at +`sig.toPFunctor.W`. Inline `WType.mk` applications are +admissible only as *children* of such a tree, never as the subject +of the `decide`. + +`safeRec`'s three children are `![…]` directly, +`Direction (.safeRec n s)` being `Fin 3`. A subterm that is already +a `BC` enters a parent's raw tree as `.val`. + +`plus` and `mult` are § 3.2's examples at arities `(1,1)` and +`(2,0)`, transcribed with the arities of the reference +implementation rather than the printed superscripts (§ The paper's +`mult` is ill-formed as printed): + +- `plusStep`: `comp 1 2 0 1`, head `succ true`, no normal + arguments, safe argument `proj 1 2 1`. +- `plus`: `safeRec 0 1`, children `![proj 0 1 0, plusStep, plusStep]`. +- `multBase`: `comp 1 0 0 0`, head `zero`, no arguments. +- `multStep`: `comp 2 1 1 1`, head `plus`, normal argument + `proj 2 0 1`, safe argument `proj 2 1 2`. +- `mult`: `safeRec 1 0`, children `![multBase, multStep, multStep]`. + +They compute unary arithmetic: +`plus x y = List.replicate x.length true ++ y` and +`mult x y = List.replicate (x.length * y.length) true`. The +justification is the definitions, not the reference development's +length lemmas (`plus_correct` at `BCUnary.v:172-173` and +`mult_correct` at `:236-237` state only `|plus m n| = |m| + |n|` +and `|mult m n| = |m| · |n|`, and a length equation does not +determine a value): `succ_e` is `succ true` (`BCUnary.v:116`), so +each step of `plus` (`:167-170`) prepends `true` to its safe +argument; `mult` (`:231-234`) iterates `plus` from the base +`zero_e 1 0`, which is `comp 1 0 zero nil nil` (`BC.v:1034-1035`) +and whose head `zero` evaluates to the empty bitstring +(`BC.v:390`, through the `comp` clause at `:419-421`). + +`plus` takes one normal and one safe argument; `mult` takes two +normal arguments and none safe (`sem mult_e [m; n] nil`). Each +assertion names its two environments accordingly. + +`plus` and `mult` both pass the same subterm as `safeRec`'s +directions 1 and 2, so neither discriminates `h₀` from `h₁`: with +those alone, transposing `c 1` and `c 2` in `evalValue` would leave +every assertion passing. `branchRec` closes this. It is +`safeRec 0 0` with children `![zero, proj 1 1 0, proj 1 1 1]`, of +arity `(1, 0)`, so that + + f [] = [], f (b :: v) = if b then f v else v + +Single-bit arguments do not discriminate: `f [false]` and +`f [true]` are both `[]` under the intended reading and under the +transposed one. The assertions are therefore at length two: +`branchRec` on `![[false, true]]` is `[true]` and on `![[true, true]]` +is `[]`. Measured: rebuilding `evalValue` with `c 1` and `c 2` +transposed fails exactly these two assertions and no others. + +`badRaw` is a `sig.toPFunctor.W`, not a `BC`: `plusStepRaw` with +its safe child replaced by `WType.mk (.proj 2 0 1) Fin.elim0`, +which carries index `(2, 0)` where `rc` demands `(1, 2)`. + +Four leaf terms cover what the compound terms do not: `predTerm` +and `condTerm`, `pred` and `cond` appearing in no other term; and +`projNTerm` (`proj 1 1 0`) and `projSTerm` (`proj 1 1 1`), which +separate the two halves of `Fin.append` at a single node, the +`Fin`-wraparound property above being what motivates checking them +apart. `zero` and `succ true` need no leaf term: they are the +heads of `multBase` and `plusStep`, whose outputs `eval_mult` and +`eval_plus_cons` already pin. Each leaf is a single node with +`Fin.elim0` children, admissible vacuously but still bound in two +steps. + +The twelve evaluation assertions have the form +`(BC.eval e).2 env₁ env₂ = out`; the negative control, whose +environments the coverage table marks `—`, is the thirteenth and +last row. Each evaluation assertion is named `eval_`, with a +suffix where one term carries several +— `eval_plus_nil`, `eval_plus_cons`, `eval_mult`, +`eval_branchRec_false`, `eval_branchRec_true`, +`eval_predTerm_nil`, `eval_predTerm_cons`, +`eval_condTerm_empty`, `eval_condTerm_odd`, `eval_condTerm_even`, +`eval_projNTerm`, `eval_projSTerm`. The negative control is +`wValid_badRaw_eq_false`, stated in the coverage table's +`decide (sig.WValid badRaw) = false` form rather than as +`¬ sig.WValid badRaw`, so that it too closes by `rfl`. Each +carries a `/-- … -/` +docstring, `docs/rules/lean-coding.md` § Comment and docstring +rules requiring one of every theorem of public interest, which the +module's `## Main statements` section makes these. + +Assertions are named `theorem`s. They cannot be `def`s — +`linter.defProp` rejects a `def` whose type is a `Prop`, and +`GebTests` inherits `mathlibStandardSet` and `weak.warningAsError` +from the package-level `[leanOptions]` (`lakefile.toml:12,15`; the +library-level block at `:59-60` overrides only +`linter.hashCommand`). The raw-tree and term `def`s anchor the +module's imports for `lake shake`, as `wLeaf`/`wNode` do in +`GebTests/Mathlib/Data/PFunctor/Slice/W.lean`; where an import is +still reported removable it carries a `-- shake: keep` comment, as +`GebTests/Mathlib/CategoryTheory/FinCat/FinCategory.lean:8-10` +does. + +Coverage. Each of the following is a `theorem` stating an expected +output and closing by `rfl`: + +| assertion | environments | output | +| --- | --- | --- | +| `plus` | `![[]]`, `![[false]]` | `[false]` | +| `plus` | `![[true, true]]`, `![[false]]` | `[true, true, false]` | +| `mult` | `![[true, true], [true, true, true]]`, `![]` | `List.replicate 6 true` | +| `branchRec` | `![[false, true]]`, `![]` | `[true]` | +| `branchRec` | `![[true, true]]`, `![]` | `[]` | +| `predTerm` | `![]`, `![[]]` | `[]` | +| `predTerm` | `![]`, `![[true, false]]` | `[false]` | +| `condTerm` | `![]`, `![[], [false], [true], [true, true]]` | `[false]` | +| `condTerm` | `![]`, `![[true], [false], [true], [true, true]]` | `[true]` | +| `condTerm` | `![]`, `![[false], [false], [true], [true, true]]` | `[true, true]` | +| `projNTerm` | `![[true]]`, `![[false]]` | `[true]` | +| `projSTerm` | `![[true]]`, `![[false]]` | `[false]` | +| `decide (sig.WValid badRaw)` | — | `false` | + +`BCOf` is exercised by two `def`s rather than `theorem`s, `BCOf n s` +being a type and not a `Prop`: +`def plusOf : BCOf 1 1 := ⟨plus, rfl⟩` and +`def multOf : BCOf 2 0 := ⟨mult, rfl⟩`. These subsume the arities: +each elaborates exactly when `BC.arity` of its term reduces to the +stated pair, so no separate `arity_plus`/`arity_mult` theorem is +carried. + +## Documentation + +- Module docstring: `# Title`, summary, `## Main definitions` (the + fourteen library declarations other than the three instances, + which mathlib's guide does not list there), `## Implementation notes` (the + W-type encoding and the rule requiring it; the transport and why + `evalValue` is separate; the choice-free `scoped` `FinEnum` + instances; the `@[reducible]` requirement), `## References` + (`[HeraudNowak2011]`, `[BellantoniCook1992]`), `## Tags` + (`Bellantoni-Cook, polytime, implicit computational complexity, + safe recursion, W-type, polynomial functor`). `## Main + statements` and `## Notation` are omitted as vacuous. Every + declaration carries a `/-- … -/` docstring; `Shape`'s seven + constructors are documented within the type's own docstring, as + `Fixtures.lean:127-128` documents `Shp`'s. All four new `.lean` + files carry the standard copyright header, and the two index + files carry a module docstring in the form of + `Geb/Mathlib/Data.lean`'s. +- The test module carries `# Title`, a summary and `## Tags`, as + `GebTests/Mathlib/Data/PFunctor/Slice/W.lean:11-23` does; plus + `## References` citing `[HeraudNowak2011]`, since `plus` and + `mult` are transcribed, and `## Main statements` for its named + theorems. `docs/rules/lean-coding.md` § Documentation requires + each section that has content. Its twenty-four `def`s — the + eleven raw trees, the ten terms, `compChildren`, `plusOf` and + `multOf` — each carry a `/-- … -/` docstring, § Comment and + docstring rules mandating one for every `def`. A raw tree's + states its shape and children; a term's states its arity and, + for `plus`, `mult` and `branchRec`, the function it computes; + `compChildren`'s states the head-then-normal-then-safe order it + imposes; `plusOf`'s and `multOf`'s state that they exhibit their + terms at the arities `§ Tests` claims. +- `docs/references.bib`: `HeraudNowak2011` as `@inproceedings` at + ITP 2011 (`author = {H{\'e}raud, Sylvain and Nowak, David}`, + `title`, `booktitle`, `series`, `volume = {6898}`, + `pages = {119--134}`, `publisher`, `year`, `doi`) carrying + `eprint = {1102.5495}`, `archivePrefix = {arXiv}`, + `primaryClass = {cs.CC}`, and a `note` recording that this + repository cites the arXiv version's section and page numbering. + The file's entries for works existing as both preprint and + publication are the published type with the preprint in `eprint` + (`AllaisAtkeyChapmanMcBrideMcKinna2021`, + `GhaniNordvallForsbergMalatesta2015`, `JohnsonYau2021`, + `AvanziniDalLago2018`, `AltenkirchChapmanUustalu2015`), `note` + being used only for what those fields cannot carry — as in + `HancockMcBrideGhaniMalatestaAltenkirch2013`, which is this + situation exactly: proceedings entry, `note` naming which + version's numbering the repository cites. `Vistoli2008` is + `@misc` because it has no publication, not because the preprint + is cited. The accented surname is + LaTeX-escaped, as `Par{\'e}` is. + `BellantoniCook1992` as `@article`: Bellantoni and Cook, *A new + recursion-theoretic characterization of the polytime functions*, + Computational Complexity 2(2), 97-110, 1992, + `doi:10.1007/BF01201998` — the field set and order of `Pare1974`. +- `docs/references.md` § Computability: a pointer to + `github.com/davidnowak/bellantonicook` at the commit named in + § Sources. +- `docs/index.md` § Implemented content: one bullet in the file's + flat one-bullet-per-module form, among the other `Geb/Mathlib/` + bullets and after those for + `Geb/Mathlib/Data/PFunctor/Slice/`, which it depends on, reading + to the effect of + "`Geb/Mathlib/Computability/BellantoniCook.lean` + — the function class `B` of [HeraudNowak2011] § 3.2: its arity + relation as a `SlicePFunctor` over `ℕ × ℕ`, its syntax as that + functor's slice W-type, and its semantics by the W-type's + eliminator. Depends on `Geb.Mathlib.Data.PFunctor.Slice.W` and + `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`. Every declaration of + the module has axioms within `propext` and `Quot.sound`; `sig` and + `finEnumFin` have none." + — covering the path, the concepts and the dependencies per + docs/process.md § Documentation + under `docs/`, and stating the axiom dependence in prose, as the + file's existing bullets do. +- `TODO.md`: a `### Bellantoni-Cook` subsection under `## Next up` + containing § Deferred items 1-3 with their scope, dependencies + and return, in the neighbouring subsections' form; and items 4 + to 7 under `## Triggers (do when condition fires)`, in that + section's `- **Bold title**: …` bullet form. + +## Non-goals + +Not part of the syntax and its interpretation, and not planned: +`sem_cost` (the time-complexity semantics) and `BCI`/`B_inf` with +its two translations. Neither forecloses the deferred work: +`BCLib.v`, `BC_to_Cobham.v` and `Cobham_to_BC.v` contain no +occurrence of `BCI` or of `sem_cost`, and `sem_cost` is first +defined at `BC.v:1365`, after Proposition 2 at `:1128`. + +## Deferred + +Items 1-3 are a dependency chain and go to `## Next up`. Items 4 +to 7 are triggers, none having a consumer yet, and go to +`## Triggers (do when condition fires)` in that section's +`- **Bold title**: …` bullet form. + +1. `MultiPoly`, the multivariate polynomial library. Required by + `BC_to_Cobham.v:2`, by `Cobham_to_BC.v:2`, and by Proposition 2, + whose statement `polymax_bounding` (`BC.v:1128`) is over + `poly_BC` (`:1075`), built from `pcst`, `pproj`, `pplus`, + `pmult`, `pcomp`, `pshift` and `pplusl`. Returns the polynomial + apparatus both later items are stated over. +2. Proposition 2, the polymax bounding of `B`. Depends on 1. + Returns the length bound that the translation of 3 requires. +3. Cobham's class and the translations of Theorems 1 and 2. + Depends on 1 and 2. Returns the characterization of polynomial + time, and is the consumer named in § Purpose. +4. Trigger: a workstream needs programmable building blocks for + terms of `B`. Port the derived function library of `BCLib.v`, + which depends only on the syntax and semantics delivered here. +5. Trigger: a second consumer of `finEnumFin` or + `finEnumCompDirection` appears. Move them to + `Geb/Mathlib/Data/FinEnum.lean`, the repository's home for + choice-free `FinEnum` support. +6. Trigger: a consumer needs `DecidableEq` or `Repr` for `BC`. + Derive them on `Shape` and lift along `sig.W`'s subtype. +7. Trigger: a workstream needs the paper's "polytime checker" as a + term-level artifact. Add an untyped `Ast` plus + `check : Ast → Option ((n s : ℕ) × BCOf n s)` over + `SlicePFunctor.decidableWValid`. + +## Constraints + +1. No `noncomputable`. `#print axioms` on every declaration lies + within `{propext, Quot.sound}`, measured monomorphically in the + consuming closure and re-measured at each toolchain bump + (`docs/rules/lean-coding.md` § Constructive-only Lean code). + `Quot.sound` is permitted, not excluded. The `FinEnum` instances + are the reason this is not automatic. +2. No self-referential `inductive` and no self-calling `def`; + `Shape` is non-recursive, the syntax's recursion is `sig.W`, and + the semantics' recursions are `SlicePFunctor.W.elim` and + `List.rec`. +3. All four new `.lean` files declare `module`. The library module uses + `public import` and a `public section`; the test module uses + plain `import` with `set_option linter.privateModule false` + (§ Exposure). +4. `scripts/pre-push.sh` clean, `lake shake`, `lake lint` and + `scripts/lint-imports.sh` included. `lake shake` has been observed to print a + `PANIC at Option.get!` trace from `Lake.Shake.visitModule` when + the first module under a new `GebTests/Mathlib//` appears. + It does not reproduce reliably, exits 0 when it occurs, and + occurs equally with an unrelated control module at the same + path, so it is a shake artifact rather than a property of this + design. The subtree's rules bind: + no import outside `Mathlib.*`, `Batteries.*`, `Geb.Mathlib.*` + (and `GebTests.Mathlib.*` for the test module); no bare umbrella + import; and no `Geb.Mathlib.` or `GebTests.Mathlib.` prefix + outside an `^import` line, in particular not in the namespace + declarations. +5. No `#guard`; every assertion is a `theorem` closing by `rfl`. + `plusOf` and `multOf` are `def`s, `BCOf n s` being a type rather + than a `Prop`. Should an assertion not reduce, the term is + shrunk until it does; `native_decide` is forbidden by + Constraint 1 and `#guard` by this constraint. +6. Lambda notation follows `docs/rules/lean-coding.md` § Coding + style: `↦`, not `=>`, in `fun`. +7. Library imports: `Geb.Mathlib.Data.PFunctor.Slice.W`, + `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`, + `Mathlib.Logic.Equiv.Fin.Basic`. The test module adds + `Geb.Mathlib.Data.PFunctor.Slice.Decidable`, besides + `Geb.Mathlib.Computability.BellantoniCook` itself. + + `Slice.Decidable` belongs to the tests, not the library: the + library uses `SlicePFunctor`, `.W`, `.wIndex` and `W.elim` from + `Slice/W.lean` and `PFunctor.Finitary` from + `Univariate/Finitary.lean`, and nothing from + `Slice/Decidable.lean`; `decidableWValid` is reached only by the + tests' `by decide`. Measured: + `lake shake --add-public --keep-implied --keep-prefix Geb + GebTests`, the form `scripts/pre-push.sh:42` runs, exits 0 with + no suggestion for either new file, and no `-- shake: keep` + comment is needed. Placing `Slice.Decidable` in the library + instead makes it exit 1, asking for `Slice.W` and + `Univariate.Finitary` to be added and `Slice.Decidable` + removed. + + `Mathlib.Data.Fin.Tuple.Basic` and `Mathlib.Data.Fin.VecNotation` + are not named, though the modules apply `Fin.append`, + `Fin.cons`, `Fin.tail` and `![…]` directly: + `Mathlib.Logic.Equiv.Fin.Basic` imports `VecNotation`, which + imports `Fin.Tuple.Basic`, so naming them makes plain + `lake shake` — the form mathlib CI runs — report both modules as + carrying a redundant import. Measured: with them named, plain + `lake shake --add-public --keep-prefix Geb GebTests` reports 16 + `Geb/Mathlib/` and 8 `GebTests` files against a baseline of 15 + and 7; without them, the baseline is unchanged and both modules + still build. Omitting them keeps the branch off the count in + `TODO.md`'s `lake shake --keep-implied` trigger and keeps the + upstream-eligible module minimal, as CONTRIBUTING.md § Floodgate + test requires of a PR shipped with no source-code change. From 480a3d656f53d29e5800080d3abe892bcdbbe0d6 Mon Sep 17 00:00:00 2001 From: "Terence M. Rokop" Date: Tue, 4 Aug 2026 13:48:53 -0700 Subject: [PATCH 2/9] doc: add the Bellantoni-Cook implementation plan --- .../plans/2026-08-04-bellantoni-cook.md | 1240 +++++++++++++++++ 1 file changed, 1240 insertions(+) create mode 100644 docs/superpowers/plans/2026-08-04-bellantoni-cook.md diff --git a/docs/superpowers/plans/2026-08-04-bellantoni-cook.md b/docs/superpowers/plans/2026-08-04-bellantoni-cook.md new file mode 100644 index 0000000..fc3ef1f --- /dev/null +++ b/docs/superpowers/plans/2026-08-04-bellantoni-cook.md @@ -0,0 +1,1240 @@ +# Bellantoni-Cook syntax and semantics — implementation plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use +> superpowers:subagent-driven-development (recommended) or +> superpowers:executing-plans to implement this plan task-by-task. +> Steps use checkbox (`- [ ]`) syntax for tracking. + +**Goal:** Define the function class `B` of [HeraudNowak2011] § 3.2 in Lean — +its syntax as the slice W-type of a signature functor over `ℕ × ℕ`, and its +interpretation by that type's eliminator. + +**Architecture:** A non-recursive `Shape` type carries the seven constructor +forms with their arity parameters; `q : Shape → ℕ × ℕ` and +`rc : (a : Shape) → Direction a → ℕ × ℕ` encode the paper's arity relation as +data (conclusions and hypotheses respectively); `sig` bundles them as a +`SlicePFunctor (ℕ × ℕ) (ℕ × ℕ)`; `BC := sig.W` admits exactly the +well-formed terms; and `BC.eval` is one application of +`SlicePFunctor.W.elim` into the dependent target `Σ i, Sem i`. + +**Tech Stack:** Lean 4 (toolchain v4.33.0-rc2), mathlib, +`Geb.Mathlib.Data.PFunctor.Slice.*`, `jj` for version control. + + + + +- [Global Constraints](#global-constraints) +- [Commit sequence](#commit-sequence) +- [File structure](#file-structure) +- [Task 1: Branch, spec commit, plan commit](#task-1-branch-spec-commit-plan-commit) +- [Task 2: The signature functor](#task-2-the-signature-functor) +- [Task 3: Finiteness and decidable admissibility](#task-3-finiteness-and-decidable-admissibility) +- [Task 4: The syntax and the semantics](#task-4-the-syntax-and-the-semantics) +- [Task 5: The test module](#task-5-the-test-module) +- [Task 6: Documentation](#task-6-documentation) +- [Task 7: The pre-push gate](#task-7-the-pre-push-gate) +- [Task 8: Remove the spec and the plan](#task-8-remove-the-spec-and-the-plan) + + + +## Global Constraints + +Every task's requirements implicitly include these. They are the spec's +§ Constraints, verbatim in substance. + +1. No `noncomputable`. `#print axioms` on every declaration lies within + `{propext, Quot.sound}`. `Quot.sound` is permitted, not excluded. +2. No self-referential `inductive` and no self-calling `def`. `Shape` is + non-recursive; the syntax's recursion is `sig.W`; the semantics' + recursions are `SlicePFunctor.W.elim` and `List.rec`. +3. All four new `.lean` files declare `module`. The library module uses + `public import` and a `public section`; the test module uses plain + `import` with `set_option linter.privateModule false`. +4. `scripts/pre-push.sh` clean, `lake shake`, `lake lint` and + `scripts/lint-imports.sh` included. +5. No `#guard`; every assertion is a `theorem` closing by `rfl`. `plusOf` and + `multOf` are `def`s, `BCOf n s` being a type rather than a `Prop`. +6. Lambda notation uses `↦`, not `=>`, in `fun`. +7. Library imports: `Geb.Mathlib.Data.PFunctor.Slice.W`, + `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`, + `Mathlib.Logic.Equiv.Fin.Basic`. The test module adds + `Geb.Mathlib.Data.PFunctor.Slice.Decidable` and the library module. + Neither module names `Mathlib.Data.Fin.Tuple.Basic` or + `Mathlib.Data.Fin.VecNotation`, though both apply `Fin.append`, + `Fin.cons`, `Fin.tail` and `![…]`: `Mathlib.Logic.Equiv.Fin.Basic` + supplies both transitively, and naming either makes plain `lake shake` + report the module carrying it. +8. Copyright headers take the form used throughout the tree: + + ```lean + /- + Copyright (c) 2026 Terence Rokop. All rights reserved. + Released under Apache 2.0 license as described in the file LICENSE. + Authors: Terence Rokop + -/ + ``` + +9. Commit messages follow the repository's Conventional-Commits-shaped + convention (`feat` / `fix` / `doc` / `style` / `refactor` / `test` / + `chore` / `perf` / `ci`), imperative present tense, no capital, no period. +10. **Version control is `jj`, not `git`.** A PreToolUse hook blocks + mutating `git` subcommands. Commit with `jj commit -m "…"`, which + commits the whole working copy and starts a fresh change. + +## Commit sequence + +The spec's § Placement fixes the phase order: spec, plan, library module, +test module, documentation, then a final commit removing the spec and the +plan. This plan spans the library phase over three commits (Tasks 2-4), +which refines that order without reordering it. + +## File structure + +| Path | Responsibility | +| --- | --- | +| `Geb/Mathlib/Computability.lean` | directory index; imports the content module | +| `Geb/Mathlib/Computability/BellantoniCook.lean` | the whole library: signature, finiteness, syntax, semantics | +| `GebTests/Mathlib/Computability.lean` | test directory index | +| `GebTests/Mathlib/Computability/BellantoniCook.lean` | the worked terms and the thirteen assertions | +| `Geb/Mathlib.lean` | gains one `public import` | +| `GebTests/Mathlib.lean` | gains one `import` | +| `docs/references.bib` | two entries | +| `docs/references.md` | one pointer | +| `docs/index.md` | one bullet | +| `TODO.md` | one `### Bellantoni-Cook` subsection, four trigger entries | + +One content module, not a `Defs`/`Basic` split: this workstream states no +lemmas, so there is nothing to separate. + +--- + +## Task 1: Branch, spec commit, plan commit + +**Files:** + +- Modify: none (version-control only) + +**Interfaces:** + +- Consumes: nothing +- Produces: a topic branch `feat/bellantoni-cook` whose first two commits + carry the spec and this plan + +- [ ] **Step 1: Create the topic branch on the current change** + +```bash +jj bookmark create feat/bellantoni-cook -r @ +``` + +- [ ] **Step 2: Confirm the working copy holds the spec and the plan** + +Run: `jj status` +Expected: two `A` lines, the spec and this plan, in one change. + +- [ ] **Step 3: Commit the spec alone** + +`jj commit` with paths keeps the named paths in the current commit and moves +everything else to a new working-copy commit on top, which is how the spec +and the plan become two commits in the order § Placement fixes. + +```bash +jj commit docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md \ + -m "doc: add the Bellantoni-Cook design spec" +``` + +- [ ] **Step 4: Confirm the plan is now the only working-copy change** + +Run: `jj status` +Expected: exactly one line, `A docs/superpowers/plans/2026-08-04-bellantoni-cook.md` + +- [ ] **Step 5: Commit the plan** + +```bash +jj commit -m "doc: add the Bellantoni-Cook implementation plan" +``` + +- [ ] **Step 6: Advance the bookmark to the new head** + +```bash +jj bookmark set feat/bellantoni-cook -r @- +``` + +Run: `jj log -r 'feat/bellantoni-cook'` +Expected: the bookmark points at the plan commit. + +--- + +## Task 2: The signature functor + +**Files:** + +- Create: `Geb/Mathlib/Computability.lean` +- Create: `Geb/Mathlib/Computability/BellantoniCook.lean` +- Modify: `Geb/Mathlib.lean` + +**Interfaces:** + +- Consumes: `SlicePFunctor` from `Geb.Mathlib.Data.PFunctor.Slice.W` +- Produces: + - `BellantoniCook.Shape : Type` — seven constructors, listed below + - `BellantoniCook.Direction : Shape → Type` + - `BellantoniCook.rc : (a : Shape) → Direction a → ℕ × ℕ` + - `BellantoniCook.q : Shape → ℕ × ℕ` + - `BellantoniCook.sig : SlicePFunctor (ℕ × ℕ) (ℕ × ℕ)` + +- [ ] **Step 1: Create the directory index** + +Create `Geb/Mathlib/Computability.lean`: + +```lean +/- +Copyright (c) 2026 Terence Rokop. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Terence Rokop +-/ +module + +public import Geb.Mathlib.Computability.BellantoniCook + +/-! +# Computability — index +-/ +``` + +The title must not name `Geb.Mathlib.`: `scripts/lint-imports.sh` rejects the +self-prefix outside an `^import` line, and a docstring title carrying it fails. + +- [ ] **Step 2: Create the content module with its header, imports and signature** + +Create `Geb/Mathlib/Computability/BellantoniCook.lean`: + +```lean +/- +Copyright (c) 2026 Terence Rokop. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Terence Rokop +-/ +module + +public import Geb.Mathlib.Data.PFunctor.Slice.W +public import Geb.Mathlib.Data.PFunctor.Univariate.Finitary +public import Mathlib.Logic.Equiv.Fin.Basic + +/-! +# The function class `B` of Bellantoni and Cook + +The syntax of the function class `B` and its interpretation, following +[HeraudNowak2011] § 3.2. Terms of `B` are built from a constant zero, +projections, two successors, a predecessor and a conditional, and are closed +under a composition and a recursion that distinguish normal from safe +argument positions; the distinction is what bounds the growth rate of the +definable functions. + +The class defined here is the reformulation of § 3.2, not the class of +[BellantoniCook1992]. Two differences: the conditional takes four safe +arguments and branches three ways, on the empty, odd and even bitstrings, +where the original branches two ways on parity and treats the empty +bitstring as even; and the base case of the recursion is the empty +bitstring, where the original's is every bitstring denoting zero. + +The two sources transpose the conditional's last two safe arguments. The +order here follows the authors' Coq development, that being the artifact +against which the paper's theorems were machine-checked. + +## Main definitions + +* `BellantoniCook.Shape` — the seven constructor forms, with their arities + as parameters. +* `BellantoniCook.Direction` — the subterm positions of a shape. +* `BellantoniCook.rc` — the arity each subterm position must carry. +* `BellantoniCook.q` — the arity a shape produces. +* `BellantoniCook.sig` — the signature, as a slice polynomial functor over + `ℕ × ℕ`. +* `BellantoniCook.BC` — an expression of `B`: a `sig`-tree whose every node + respects `rc`. +* `BellantoniCook.BC.arity` — its pair of normal and safe arities. +* `BellantoniCook.BCOf` — the expressions of a given arity pair. +* `BellantoniCook.Sem` — the meaning of an arity pair: a function of a + normal and a safe environment. +* `BellantoniCook.transport` — transport of a meaning along an equality of + arity pairs. +* `BellantoniCook.evalRec` — the recursion on the consumed bitstring. +* `BellantoniCook.evalValue` — the meaning of one node from its children's. +* `BellantoniCook.evalStep` — `evalValue` as a slice algebra. +* `BellantoniCook.BC.eval` — the interpretation, by the slice W-type's + eliminator. + +## Implementation notes + +This repository expresses all recursion through recursors, admitting +neither a self-referential `inductive` nor a self-calling `def`, so the +arity-indexed syntax is the slice W-type of `sig` and the interpretation is +one application of `SlicePFunctor.W.elim`. `Shape` is itself non-recursive +and so is the shape set of a `PFunctor`, not a datatype the rule reaches. + +`evalValue` is separate from `evalStep` because the match on `Shape` must +generalize the compatibility hypothesis, which arrives bundled in +`SliceDomPFunctor.Obj`. A child's meaning carries the index it was built at +rather than the index `rc` prescribes, equal but not definitionally so; +`transport` carries it across, with the motive of `▸` fixed once instead of +at each of the six sites. + +`Direction`, `rc` and `q` are `@[reducible]`. Instance search does not +delta-reduce a semireducible definition, and every numeral in `evalValue` +elaborates against `Fin (q a).1` or `Direction a`. + +`finEnumFin` and `finEnumCompDirection` are `scoped`, and hand-built: +mathlib's `FinEnum` instances depend on `Classical.choice`, which +`lake lint` rejects, and an unscoped instance at the head symbol `FinEnum +(Fin _)` would compete with `FinEnum.fin` wherever `Geb` is imported. + +## References + +* [HeraudNowak2011] +* [BellantoniCook1992] + +## Tags + +Bellantoni-Cook, polytime, implicit computational complexity, safe +recursion, W-type, polynomial functor +-/ + +namespace BellantoniCook + +public section + +/-- The seven constructor forms of `B`, each carrying its arities as +parameters: `zero` the constant empty bitstring; `proj n s i` the `i`th of +`n` normal and `s` safe variables; `succ b` the successor appending the bit +`b`; `pred` the predecessor; `cond` the four-argument conditional; +`safeRec n s` the recursion producing arity `(n + 1, s)`; and `comp n s m k` +the composition of an expression of arity `(m, k)` with `m` normal and `k` +safe argument expressions of arity `(n, 0)` and `(n, s)`. -/ +inductive Shape + | zero + | proj (n s : ℕ) (i : Fin (n + s)) + | succ (b : Bool) + | pred + | cond + | safeRec (n s : ℕ) + | comp (n s m k : ℕ) + +/-- The subterm positions of a shape. The five base forms have none; +`safeRec` has three, its base and its two step expressions; `comp` has its +head, its `m` normal arguments and its `k` safe arguments. -/ +@[expose, reducible] def Direction : Shape → Type + | .zero => Fin 0 + | .proj _ _ _ => Fin 0 + | .succ _ => Fin 0 + | .pred => Fin 0 + | .cond => Fin 0 + | .safeRec _ _ => Fin 3 + | .comp _ _ m k => Unit ⊕ Fin m ⊕ Fin k + +/-- The arity each subterm position must carry: the hypotheses of the +arity relation of [HeraudNowak2011] § 3.2. -/ +@[expose, reducible] def rc : (a : Shape) → Direction a → ℕ × ℕ + | .zero, i => i.elim0 + | .proj _ _ _, i => i.elim0 + | .succ _, i => i.elim0 + | .pred, i => i.elim0 + | .cond, i => i.elim0 + | .safeRec n s, ⟨0, _⟩ => (n, s) + | .safeRec n s, _ => (n + 1, s + 1) + | .comp _ _ m k, .inl () => (m, k) + | .comp n _ _ _, .inr (.inl _) => (n, 0) + | .comp n s _ _, .inr (.inr _) => (n, s) + +/-- The arity a shape produces: the conclusions of the arity relation of +[HeraudNowak2011] § 3.2. -/ +@[expose, reducible] def q : Shape → ℕ × ℕ + | .zero => (0, 0) + | .proj n s _ => (n, s) + | .succ _ => (0, 1) + | .pred => (0, 1) + | .cond => (0, 4) + | .safeRec n s => (n + 1, s) + | .comp n s _ _ => (n, s) + +/-- The signature of `B` as a slice polynomial functor over `ℕ × ℕ`, the +index being the pair of normal and safe arities. -/ +@[expose] def sig : SlicePFunctor (ℕ × ℕ) (ℕ × ℕ) where + A := Shape + B := Direction + r := fun x ↦ rc x.1 x.2 + q := q + +end + +end BellantoniCook +``` + +- [ ] **Step 3: Add the import to the subtree index** + +Modify `Geb/Mathlib.lean`: add `public import Geb.Mathlib.Computability` to +the import block, keeping the block alphabetically ordered as the file has it. + +- [ ] **Step 4: Build and verify zero diagnostics** + +Run: `lake build Geb.Mathlib.Computability Geb.Mathlib` +Expected: builds with no output beyond the progress lines. Any warning is a +failure — the package sets `weak.warningAsError = true`. Naming the index +modules rather than the content module alone is what exercises Step 1's and +Step 3's edits; a typo in either would otherwise surface only at Task 7. + +- [ ] **Step 5: Verify the arity relation transcribes correctly** + +Run this scratch check (do not commit it); it asserts every row of the +spec's signature table: + +```bash +cat > /tmp/bc-sig-check.lean <<'EOF' +import Geb.Mathlib.Computability.BellantoniCook +open BellantoniCook +example : q .zero = (0, 0) := rfl +example : q (.proj 2 3 0) = (2, 3) := rfl +example : q (.succ true) = (0, 1) := rfl +example : q .pred = (0, 1) := rfl +example : q .cond = (0, 4) := rfl +example : q (.safeRec 1 2) = (2, 2) := rfl +example : q (.comp 1 2 3 4) = (1, 2) := rfl +example : rc (.safeRec 1 2) 0 = (1, 2) := rfl +example : rc (.safeRec 1 2) 1 = (2, 3) := rfl +example : rc (.safeRec 1 2) 2 = (2, 3) := rfl +example : rc (.comp 1 2 3 4) (.inl ()) = (3, 4) := rfl +example : rc (.comp 1 2 3 4) (.inr (.inl 0)) = (1, 0) := rfl +example : rc (.comp 1 2 3 4) (.inr (.inr 0)) = (1, 2) := rfl +EOF +lake env lean /tmp/bc-sig-check.lean; rm -f /tmp/bc-sig-check.lean +``` + +Expected: no output, exit 0. A non-empty output means a row of `q` or `rc` +disagrees with the spec's table; fix the definition, not the check. + +- [ ] **Step 6: Commit** + +```bash +jj commit -m "feat(computability): add the Bellantoni-Cook signature functor" +``` + +--- + +## Task 3: Finiteness and decidable admissibility + +**Files:** + +- Modify: `Geb/Mathlib/Computability/BellantoniCook.lean` + +**Interfaces:** + +- Consumes: `sig`, `Direction`, `Shape` from Task 2; + `PFunctor.Finitary` from `Geb.Mathlib.Data.PFunctor.Univariate.Finitary` +- Produces: + - `BellantoniCook.finEnumFin (n : ℕ) : FinEnum (Fin n)` — `scoped` + - `BellantoniCook.finEnumCompDirection (m k : ℕ) : + FinEnum (Unit ⊕ Fin m ⊕ Fin k)` — `scoped` + - `BellantoniCook.sigFinitary : sig.toPFunctor.Finitary` + +- [ ] **Step 1: Add the three instances** + +Insert into `Geb/Mathlib/Computability/BellantoniCook.lean`, after `sig` and +inside the `public section`: + +```lean +/-- A choice-free `FinEnum (Fin n)`: the cardinality is `n` and the +enumeration is the identity. `scoped`, so that it does not compete with +mathlib's `FinEnum.fin` at the same head symbol outside this namespace. -/ +scoped instance finEnumFin (n : ℕ) : + FinEnum (Fin n) where + card := n + equiv := Equiv.refl _ + decEq := inferInstance + +/-- A choice-free `FinEnum` for `comp`'s directions. `scoped`, for the same +reason as `finEnumFin`. -/ +scoped instance finEnumCompDirection (m k : ℕ) : + FinEnum (Unit ⊕ Fin m ⊕ Fin k) where + card := 1 + (m + k) + equiv := (Equiv.sumCongr finOneEquiv.symm finSumFinEquiv).trans finSumFinEquiv + decEq := inferInstance + +/-- Every shape has finitely many directions, which is what makes +admissibility of a `sig`-tree decidable. The branches ascribe their +instances explicitly: instance search stops at reducible transparency on the +projection `sig.B a`, so a bare `inferInstance` does not find them. -/ +instance sigFinitary : sig.toPFunctor.Finitary + | .zero => inferInstanceAs (FinEnum (Fin 0)) + | .proj _ _ _ => inferInstanceAs (FinEnum (Fin 0)) + | .succ _ => inferInstanceAs (FinEnum (Fin 0)) + | .pred => inferInstanceAs (FinEnum (Fin 0)) + | .cond => inferInstanceAs (FinEnum (Fin 0)) + | .safeRec _ _ => inferInstanceAs (FinEnum (Fin 3)) + | .comp _ _ m k => inferInstanceAs (FinEnum (Unit ⊕ Fin m ⊕ Fin k)) +``` + +`sigFinitary` is an `instance`, not a `def`: as a `def` it does not fire for +`decidableWValid`, and it draws `Definition … of class type is +semireducible`, fatal under `weak.warningAsError`. It needs no attribute. + +- [ ] **Step 2: Build** + +Run: `lake build Geb.Mathlib.Computability.BellantoniCook` +Expected: builds, no output beyond progress lines. + +- [ ] **Step 3: Verify the instances are choice-free** + +Run: + +```bash +cat > /tmp/bc-axiom-check.lean <<'EOF' +import Geb.Mathlib.Computability.BellantoniCook +#print axioms BellantoniCook.finEnumFin +#print axioms BellantoniCook.finEnumCompDirection +#print axioms BellantoniCook.sigFinitary +EOF +lake env lean /tmp/bc-axiom-check.lean; rm -f /tmp/bc-axiom-check.lean +``` + +Expected: `'BellantoniCook.finEnumFin' does not depend on any axioms`, and +`[propext, Quot.sound]` for the other two. **`Classical.choice` anywhere is a +failure** — it means a branch resolved through a mathlib instance instead of +the two above. + +- [ ] **Step 4: Commit** + +```bash +jj commit -m "feat(computability): add choice-free finiteness for the signature" +``` + +--- + +## Task 4: The syntax and the semantics + +**Files:** + +- Modify: `Geb/Mathlib/Computability/BellantoniCook.lean` + +**Interfaces:** + +- Consumes: `sig`, `Shape`, `Direction`, `rc`, `q` from Task 2; + `sigFinitary` from Task 3; `SlicePFunctor.W`, `.wIndex`, `W.elim` from + `Geb.Mathlib.Data.PFunctor.Slice.W` +- Produces: + - `BellantoniCook.BC : Type` + - `BellantoniCook.BC.arity : BC → ℕ × ℕ` + - `BellantoniCook.BCOf (n s : ℕ) : Type` + - `BellantoniCook.Sem : ℕ × ℕ → Type` + - `BellantoniCook.transport {i j : ℕ × ℕ} (h : i = j) (v : Sem i) : Sem j` + - `BellantoniCook.evalRec {n s : ℕ} (g : Sem (n, s)) + (h₀ h₁ : Sem (n + 1, s + 1)) : List Bool → Sem (n, s)` + - `BellantoniCook.evalValue : (a : Shape) → + (c : Direction a → Σ i, Sem i) → (∀ b, (c b).1 = rc a b) → Sem (q a)` + - `BellantoniCook.evalStep : + sig.toSliceDomPFunctor.Obj (Sigma.fst (β := Sem)) → Σ i, Sem i` + - `BellantoniCook.BC.eval : BC → Σ i, Sem i` + +- [ ] **Step 1: Add the syntax** + +Insert after `sigFinitary`, inside the `public section`: + +```lean +/-- An expression of `B`: a `sig`-tree every node of which carries children +at the indices `rc` prescribes. -/ +@[expose] def BC : Type := sig.W + +/-- The arity pair of an expression: its normal and safe arities. -/ +@[expose] def BC.arity : BC → ℕ × ℕ := sig.wIndex + +/-- The expressions of arity `(n, s)`, which is the arity relation of +[HeraudNowak2011] § 3.2 as a type rather than a side condition. -/ +@[expose] def BCOf (n s : ℕ) : Type := { e : BC // e.arity = (n, s) } +``` + +- [ ] **Step 2: Add the semantic family and the transport** + +```lean +/-- The meaning of an arity pair: a function of a normal and a safe +environment, each a tuple of bitstrings, returning a bitstring. -/ +@[expose] def Sem : ℕ × ℕ → Type := + fun i ↦ (Fin i.1 → List Bool) → (Fin i.2 → List Bool) → List Bool + +/-- Transport of a meaning along an equality of arity pairs. Named so that +the motive of `▸` is fixed once rather than inferred at each use in +`evalValue`. -/ +@[expose] def transport {i j : ℕ × ℕ} (h : i = j) (v : Sem i) : Sem j := h ▸ v +``` + +- [ ] **Step 3: Add the recursion on the consumed bitstring** + +```lean +/-- The recursion `safeRec` performs on its first normal argument, by +`List.rec`. The base case is the empty bitstring; a step consumes the low +bit `b`, passes the remaining bitstring `v` as the new first normal +argument, and passes the recursive value in safe position. -/ +@[expose] def evalRec {n s : ℕ} (g : Sem (n, s)) + (h₀ h₁ : Sem (n + 1, s + 1)) : List Bool → Sem (n, s) := + List.rec g (fun b v ih x y ↦ + (if b then h₁ else h₀) (Fin.cons v x) (Fin.cons (ih x y) y)) +``` + +- [ ] **Step 4: Add the algebra** + +```lean +/-- The meaning of one node, from its children's meanings and the proof that +each child's index is the one `rc` prescribes. A separate definition from +`evalStep` because the match on `Shape` must generalize that proof. + +`cond` reads its first safe argument and returns the second, third or fourth +according as it is empty, odd or even — the ordering of the authors' Coq +development. `comp` applies its head's meaning to the normal arguments' +meanings, each in the empty safe environment, and to the safe arguments'. -/ +@[expose] def evalValue : (a : Shape) → (c : Direction a → Σ i, Sem i) → + (∀ b, (c b).1 = rc a b) → Sem (q a) + | .zero, _, _ => fun _ _ ↦ [] + | .proj _ _ i, _, _ => fun x y ↦ Fin.append x y i + | .succ b, _, _ => fun _ y ↦ b :: y 0 + | .pred, _, _ => fun _ y ↦ (y 0).tail + | .cond, _, _ => fun _ y ↦ + match y 0 with + | [] => y 1 + | true :: _ => y 2 + | false :: _ => y 3 + | .safeRec _ _, c, h => fun x y ↦ + evalRec (transport (h 0) (c 0).2) (transport (h 1) (c 1).2) + (transport (h 2) (c 2).2) (x 0) (Fin.tail x) y + | .comp _ _ _ _, c, h => fun x y ↦ + transport (h (.inl ())) (c (.inl ())).2 + (fun i ↦ transport (h (.inr (.inl i))) (c (.inr (.inl i))).2 x Fin.elim0) + (fun j ↦ transport (h (.inr (.inr j))) (c (.inr (.inr j))).2 x y) + +/-- `evalValue` as an algebra for `sig` in the slice over `ℕ × ℕ`. Returning +the shape's own output index as the first component makes the eliminator's +coherence obligation hold by `rfl`. -/ +@[expose] def evalStep : + sig.toSliceDomPFunctor.Obj (Sigma.fst (β := Sem)) → Σ i, Sem i := + fun z ↦ ⟨sig.q z.1.1, + evalValue z.1.1 z.1.2 + ((sig.toSliceDomPFunctor.compatible_iff _ z.1.1 z.1.2).mp z.2)⟩ + +/-- The interpretation of an expression: its arity pair together with its +meaning at that pair, by the slice W-type's eliminator. -/ +@[expose] def BC.eval : BC → Σ i, Sem i := + SlicePFunctor.W.elim sig (Σ i, Sem i) (Sigma.fst (β := Sem)) evalStep rfl +``` + +Note `SlicePFunctor.W.elim sig …`, not `sig.W.elim …`: `sig.W` is a type, +not a term, so field notation does not chain through it. + +- [ ] **Step 5: Build** + +Run: `lake build Geb.Mathlib.Computability.BellantoniCook` +Expected: builds, no output beyond progress lines. In particular no +`failed to synthesize instance of type class OfNat …`, which would mean +`Direction`, `rc` or `q` lost its `@[reducible]`. + +- [ ] **Step 6: Verify the axioms and run the linters** + +Run: + +```bash +cat > /tmp/bc-eval-axioms.lean <<'EOF' +import Geb.Mathlib.Computability.BellantoniCook +#print axioms BellantoniCook.BC.eval +#print axioms BellantoniCook.evalValue +#print axioms BellantoniCook.evalRec +EOF +lake env lean /tmp/bc-eval-axioms.lean; rm -f /tmp/bc-eval-axioms.lean +lake lint +scripts/lint-imports.sh +``` + +Expected: each line within `{propext, Quot.sound}` — some declarations +depend on fewer, which is not a failure. **`Classical.choice` anywhere is a +failure.** `lake lint` prints +`Running linter on specified modules: [Geb]` and +`-- Linting passed for Geb.`; `lint-imports.sh` prints +`lint-imports.sh: clean (N file(s) checked)`. + +- [ ] **Step 7: Commit** + +```bash +jj commit -m "feat(computability): add the Bellantoni-Cook syntax and semantics" +``` + +--- + +## Task 5: The test module + +**Files:** + +- Create: `GebTests/Mathlib/Computability.lean` +- Create: `GebTests/Mathlib/Computability/BellantoniCook.lean` +- Modify: `GebTests/Mathlib.lean` + +**Interfaces:** + +- Consumes: everything Task 4 produces, plus + `SlicePFunctor.decidableWValid` from + `Geb.Mathlib.Data.PFunctor.Slice.Decidable` +- Produces: nothing later tasks depend on + +- [ ] **Step 1: Create the test directory index** + +Create `GebTests/Mathlib/Computability.lean`: + +```lean +/- +Copyright (c) 2026 Terence Rokop. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Terence Rokop +-/ +module + +import GebTests.Mathlib.Computability.BellantoniCook + +/-! +# Computability tests — index +-/ +``` + +- [ ] **Step 2: Write the test module — header, terms, and the first two assertions** + +Create `GebTests/Mathlib/Computability/BellantoniCook.lean`: + +```lean +/- +Copyright (c) 2026 Terence Rokop. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Terence Rokop +-/ +module + +import Geb.Mathlib.Computability.BellantoniCook +import Geb.Mathlib.Data.PFunctor.Slice.Decidable + +/-! +# Worked expressions of the Bellantoni-Cook class + +The `plus` and `mult` of [HeraudNowak2011] § 3.2, a recursion whose two step +expressions differ, four single-node expressions, and one inadmissible raw +tree. Each expression is built in two steps — a raw tree bound as its own +definition, then the admissible expression — because an inline `WType.mk` +application blocks the instance search that `decide` needs. + +`plus` and `mult` are transcribed with the arities of the authors' Coq +development. The composition superscripts printed in § 3.2's `mult` are +`plus`'s and do not satisfy the paper's own arity relation. + +## Main statements + +The thirteen assertions below: twelve expected outputs of `BC.eval`, and one +inadmissible tree. + +## References + +* [HeraudNowak2011] + +## Tags + +Bellantoni-Cook, polytime, safe recursion +-/ + +set_option linter.privateModule false + +open BellantoniCook + +/-- The children of a `comp` node, in the order `Direction` gives them: the +head, then the normal arguments, then the safe arguments. -/ +def compChildren {m k : ℕ} (h : sig.toPFunctor.W) + (gN : Fin m → sig.toPFunctor.W) (gS : Fin k → sig.toPFunctor.W) : + Unit ⊕ Fin m ⊕ Fin k → sig.toPFunctor.W := + Sum.elim (fun _ ↦ h) (Sum.elim gN gS) + +/-- The step expression of `plus`: the successor appending `true`, applied +to the recursive value. -/ +def plusStepRaw : sig.toPFunctor.W := + WType.mk (.comp 1 2 0 1) + (compChildren (WType.mk (.succ true) Fin.elim0) Fin.elim0 + ![WType.mk (.proj 1 2 1) Fin.elim0]) + +/-- The step expression of `plus`, admissible. -/ +def plusStep : BC := ⟨plusStepRaw, by decide⟩ + +/-- `plus`, of arity `(1, 1)`: it prepends one `true` per bit of its normal +argument to its safe argument. -/ +def plusRaw : sig.toPFunctor.W := + WType.mk (.safeRec 0 1) + ![WType.mk (.proj 0 1 0) Fin.elim0, plusStep.val, plusStep.val] + +/-- `plus`, admissible. -/ +def plus : BC := ⟨plusRaw, by decide⟩ + +/-- The base expression of `mult`: the constant empty bitstring at +arity `(1, 0)`. -/ +def multBaseRaw : sig.toPFunctor.W := + WType.mk (.comp 1 0 0 0) + (compChildren (WType.mk .zero Fin.elim0) Fin.elim0 Fin.elim0) + +/-- The base expression of `mult`, admissible. -/ +def multBase : BC := ⟨multBaseRaw, by decide⟩ + +/-- The step expression of `mult`: `plus` of the second normal argument and +the recursive value. -/ +def multStepRaw : sig.toPFunctor.W := + WType.mk (.comp 2 1 1 1) + (compChildren plus.val ![WType.mk (.proj 2 0 1) Fin.elim0] + ![WType.mk (.proj 2 1 2) Fin.elim0]) + +/-- The step expression of `mult`, admissible. -/ +def multStep : BC := ⟨multStepRaw, by decide⟩ + +/-- `mult`, of arity `(2, 0)`: it produces one `true` per pair of bits of +its two normal arguments. -/ +def multRaw : sig.toPFunctor.W := + WType.mk (.safeRec 1 0) ![multBase.val, multStep.val, multStep.val] + +/-- `mult`, admissible. -/ +def mult : BC := ⟨multRaw, by decide⟩ + +/-- `plus` at its declared arity. Elaborating this is exactly the assertion +that `BC.arity plus` is `(1, 1)`. -/ +def plusOf : BCOf 1 1 := ⟨plus, rfl⟩ + +/-- `mult` at its declared arity. -/ +def multOf : BCOf 2 0 := ⟨mult, rfl⟩ + +/-- `plus` on an empty normal argument returns its safe argument. -/ +theorem eval_plus_nil : (BC.eval plus).2 ![[]] ![[false]] = [false] := rfl + +/-- `plus` prepends one `true` per bit of its normal argument. -/ +theorem eval_plus_cons : + (BC.eval plus).2 ![[true, true]] ![[false]] = [true, true, false] := rfl +``` + +- [ ] **Step 3: Build and check the first two assertions before writing the rest** + +Run: `lake build GebTests.Mathlib.Computability.BellantoniCook` +Expected: builds. A `Not a definitional equality` here means a term or a +semantic clause is wrong; fix it before continuing, since every later +assertion rests on the same clauses. + +- [ ] **Step 4: Add the remaining terms and assertions** + +Append to `GebTests/Mathlib/Computability/BellantoniCook.lean`: + +```lean +/-- `mult` produces one `true` per pair of bits of its two normal +arguments. -/ +theorem eval_mult : + (BC.eval mult).2 ![[true, true], [true, true, true]] ![] = + List.replicate 6 true := rfl + +/-- A recursion whose two step expressions differ: the `false` branch +returns the remaining bitstring, the `true` branch recurses. Without it no +assertion here would distinguish the two step expressions, `plus` and `mult` +passing the same expression as both. -/ +def branchRecRaw : sig.toPFunctor.W := + WType.mk (.safeRec 0 0) + ![WType.mk .zero Fin.elim0, WType.mk (.proj 1 1 0) Fin.elim0, + WType.mk (.proj 1 1 1) Fin.elim0] + +/-- The discriminating recursion, admissible. -/ +def branchRec : BC := ⟨branchRecRaw, by decide⟩ + +/-- On a `false`-headed argument the `false` branch returns the remaining +bitstring. Arguments of length one do not discriminate the branches: both +readings return the empty bitstring. -/ +theorem eval_branchRec_false : + (BC.eval branchRec).2 ![[false, true]] ![] = [true] := rfl + +/-- On a `true`-headed argument the `true` branch recurses. -/ +theorem eval_branchRec_true : + (BC.eval branchRec).2 ![[true, true]] ![] = [] := rfl + +/-- The predecessor as a single node. -/ +def predTermRaw : sig.toPFunctor.W := WType.mk .pred Fin.elim0 + +/-- The predecessor, admissible. -/ +def predTerm : BC := ⟨predTermRaw, by decide⟩ + +/-- The predecessor of the empty bitstring is the empty bitstring. -/ +theorem eval_predTerm_nil : (BC.eval predTerm).2 ![] ![[]] = [] := rfl + +/-- The predecessor drops the low bit. -/ +theorem eval_predTerm_cons : + (BC.eval predTerm).2 ![] ![[true, false]] = [false] := rfl + +/-- The conditional as a single node. -/ +def condTermRaw : sig.toPFunctor.W := WType.mk .cond Fin.elim0 + +/-- The conditional, admissible. -/ +def condTerm : BC := ⟨condTermRaw, by decide⟩ + +/-- On the empty bitstring the conditional returns its second safe +argument. -/ +theorem eval_condTerm_empty : + (BC.eval condTerm).2 ![] ![[], [false], [true], [true, true]] = [false] := + rfl + +/-- On an odd bitstring it returns its third. The authors' Coq development +assigns the third to the odd case and the fourth to the even case; § 3.2 +prints them the other way round. -/ +theorem eval_condTerm_odd : + (BC.eval condTerm).2 ![] ![[true], [false], [true], [true, true]] = + [true] := rfl + +/-- On an even bitstring it returns its fourth. -/ +theorem eval_condTerm_even : + (BC.eval condTerm).2 ![] ![[false], [false], [true], [true, true]] = + [true, true] := rfl + +/-- A projection onto a normal variable, as a single node. -/ +def projNTermRaw : sig.toPFunctor.W := WType.mk (.proj 1 1 0) Fin.elim0 + +/-- The normal projection, admissible. -/ +def projNTerm : BC := ⟨projNTermRaw, by decide⟩ + +/-- The normal projection returns the normal argument. -/ +theorem eval_projNTerm : + (BC.eval projNTerm).2 ![[true]] ![[false]] = [true] := rfl + +/-- A projection onto a safe variable, as a single node. Together with +`projNTerm` this separates the two halves of `Fin.append`, which a +mistranscribed index would silently permute. -/ +def projSTermRaw : sig.toPFunctor.W := WType.mk (.proj 1 1 1) Fin.elim0 + +/-- The safe projection, admissible. -/ +def projSTerm : BC := ⟨projSTermRaw, by decide⟩ + +/-- The safe projection returns the safe argument. -/ +theorem eval_projSTerm : + (BC.eval projSTerm).2 ![[true]] ![[false]] = [false] := rfl + +/-- `plusStepRaw` with its safe argument replaced by an expression of arity +`(2, 0)` where the signature demands `(1, 2)`. -/ +def badRaw : sig.toPFunctor.W := + WType.mk (.comp 1 2 0 1) + (compChildren (WType.mk (.succ true) Fin.elim0) Fin.elim0 + ![WType.mk (.proj 2 0 1) Fin.elim0]) + +/-- The inadmissible tree is rejected, so admissibility is not vacuous. -/ +theorem wValid_badRaw_eq_false : decide (sig.WValid badRaw) = false := rfl +``` + +- [ ] **Step 5: Add the import to the test subtree index** + +Modify `GebTests/Mathlib.lean`: add `import GebTests.Mathlib.Computability`, +in that file's existing plain-`import` form, keeping the block ordered. + +- [ ] **Step 6: Build the tests** + +Run: `lake build GebTests GebTests.Mathlib.Computability` +Expected: builds with no output beyond progress lines. The second target +exercises Steps 1 and 5, which the first does not reach: `GebTests` imports +the content module directly, not through the index. + +- [ ] **Step 7: Verify the assertions discriminate** + +The assertions must fail when the semantics is wrong. Check the three +clauses least covered elsewhere, restoring the file after each: + +```bash +# 1. Transpose the two step expressions in evalValue's safeRec clause: +# swap `(transport (h 1) (c 1).2)` and `(transport (h 2) (c 2).2)`. +lake build GebTests +# Expected: exactly eval_branchRec_false and eval_branchRec_true fail. +jj restore Geb/Mathlib/Computability/BellantoniCook.lean + +# 2. Replace evalValue's `.zero` clause body with `fun _ _ ↦ [true]`. +lake build GebTests +# Expected: eval_mult and eval_branchRec_true fail — `zero` is the base +# child of branchRec as well as the head of multBase. +jj restore Geb/Mathlib/Computability/BellantoniCook.lean + +# 3. Replace evalValue's `.succ` clause entirely with +# | .succ _b, _, _ => fun _ y ↦ y 0 +# Renaming the binder to `_b` is required: dropping the bit while +# leaving `b` bound fails the library build with +# `Variable name 'b' is not explicitly referenced`, so the tests +# would never be reached. +lake build GebTests +# Expected: eval_plus_cons and eval_mult fail. +jj restore Geb/Mathlib/Computability/BellantoniCook.lean +``` + +If any perturbation leaves the build green, the corresponding clause is +untested — stop and report it rather than proceeding. + +- [ ] **Step 8: Run the test-side linters** + +Run: `lake lint -- GebTests` then `scripts/lint-imports.sh` +Expected: `lake lint -- GebTests` prints three lines — +`Running linter on specified modules: [Geb, GebTests]`, then +`-- Linting passed for Geb.` and `-- Linting passed for GebTests.`; the +extra argument appends to `lintDriverArgs`, it does not replace it. +`scripts/lint-imports.sh` prints `lint-imports.sh: clean (N file(s) +checked)`. + +- [ ] **Step 9: Commit** + +```bash +jj commit -m "test(computability): add worked Bellantoni-Cook expressions" +``` + +--- + +## Task 6: Documentation + +**Files:** + +- Modify: `docs/references.bib` +- Modify: `docs/references.md` +- Modify: `docs/index.md` +- Modify: `TODO.md` + +**Interfaces:** + +- Consumes: the declaration names from Tasks 2-4 +- Produces: nothing later tasks depend on + +- [ ] **Step 1: Add the two bibliography entries** + +Insert into `docs/references.bib` beside the implicit-complexity entries +already there (`Leivant1999`, `DalLagoMartiniZorzi2010`, +`AvanziniDalLago2018`), which is where the file groups this subject. Align +the `=` as the neighbouring entries do: + +```bibtex +@inproceedings{HeraudNowak2011, + author = {H{\'e}raud, Sylvain and Nowak, David}, + title = {A Formalization of Polytime Functions}, + booktitle = {Interactive Theorem Proving (ITP 2011)}, + series = {Lecture Notes in Computer Science}, + volume = {6898}, + pages = {119--134}, + publisher = {Springer}, + year = {2011}, + doi = {10.1007/978-3-642-22863-6_11}, + eprint = {1102.5495}, + archivePrefix = {arXiv}, + primaryClass = {cs.CC}, + note = {This repository cites the arXiv version's section and + page numbering.}, +} + +@article{BellantoniCook1992, + author = {Bellantoni, Stephen and Cook, Stephen}, + title = {A new recursion-theoretic characterization of the + polytime functions}, + journal = {Computational Complexity}, + volume = {2}, + number = {2}, + pages = {97--110}, + year = {1992}, + doi = {10.1007/BF01201998}, +} +``` + +- [ ] **Step 2: Add the reference-implementation pointer** + +Add to `docs/references.md` § Computability: + +```markdown +- [davidnowak/bellantonicook](https://github.com/davidnowak/bellantonicook) + — the Coq development accompanying [HeraudNowak2011], at commit + `1f03b9296104646ddc2b2b4b12e35a6619c17a99`. Licensed CeCILL; no code is + taken from it. +``` + +- [ ] **Step 3: Add the docs/index.md bullet** + +Add to `docs/index.md` § Implemented content, immediately after the bullet +for `Geb/Mathlib/Data/PFunctor/Slice/Decidable.lean` — the last of the +`Slice/` bullets, and the module this one is nearest in subject: + +```markdown +- `Geb/Mathlib/Computability/BellantoniCook.lean` — the function class `B` + of [HeraudNowak2011] § 3.2: its arity relation as a `SlicePFunctor` over + `ℕ × ℕ`, its syntax as that functor's slice W-type, and its semantics by + the W-type's eliminator. Depends on + `Geb.Mathlib.Data.PFunctor.Slice.W` and + `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`. Every declaration of the + module has axioms within `propext` and `Quot.sound`; `sig` and + `finEnumFin` have none. +``` + +- [ ] **Step 4: Add the TODO.md subsection** + +Add as the last `###` subsection of `## Next up`, in the form the +neighbouring subsections use: + +```markdown +### Bellantoni-Cook + +Three items, in dependency order, over +`Geb/Mathlib/Computability/BellantoniCook.lean`. + +1. `MultiPoly`, the multivariate polynomial library of the reference + development. Required by its `BC_to_Cobham.v:2`, by its + `Cobham_to_BC.v:2`, and by Proposition 2, whose statement + `polymax_bounding` (`BC.v:1128`) is over `poly_BC` (`:1075`), built from + `pcst`, `pproj`, `pplus`, `pmult`, `pcomp`, `pshift` and `pplusl`. + Returns the polynomial apparatus items 2 and 3 are stated over. +2. Proposition 2, the polymax bounding of `B`. Depends on 1. Returns the + length bound the translation of item 3 requires. +3. Cobham's class and the translations of Theorems 1 and 2. Depends on 1 + and 2. Returns the characterization of the polynomial-time functions, + and is the consumer that justifies the definitions already committed. +``` + +- [ ] **Step 5: Add the four trigger entries** + +Add as the last four bullets of `## Triggers (do when condition fires)`, in +that section's `- **Bold title**: …` form: + +```markdown +- **A workstream needs programmable building blocks for terms of `B`**: + port the derived function library of the reference development's + `BCLib.v`, which depends only on the syntax and semantics already + committed. +- **A second consumer of `BellantoniCook.finEnumFin` or + `finEnumCompDirection` appears**: move them to + `Geb/Mathlib/Data/FinEnum.lean`, the repository's home for choice-free + `FinEnum` support. They are `scoped` in + `Geb/Mathlib/Computability/BellantoniCook.lean`. +- **A consumer needs `DecidableEq` or `Repr` for `BellantoniCook.BC`**: + derive them on `Shape` and lift along `sig.W`'s subtype. +- **A workstream needs the polytime checker of [HeraudNowak2011] as a + term-level artifact**: add an untyped `Ast` and + `check : Ast → Option ((n s : ℕ) × BellantoniCook.BCOf n s)` over + `SlicePFunctor.decidableWValid`. +``` + +- [ ] **Step 6: Regenerate the tables of contents and lint** + +Run: + +```bash +doctoc --update-only . +markdownlint-cli2 '**/*.md' +``` + +Expected: `Everything is OK.` and `Summary: 0 issues in 0 files`. `TODO.md` +carries a doctoc TOC and gains a heading, so it will change; commit that +change with the rest. + +- [ ] **Step 7: Commit** + +```bash +jj commit -m "doc: record the Bellantoni-Cook module and its follow-on work" +``` + +--- + +## Task 7: The pre-push gate + +**Files:** + +- Modify: none expected + +**Interfaces:** + +- Consumes: everything above +- Produces: evidence that the branch is shippable + +- [ ] **Step 1: Run the full checklist** + +Run: `scripts/pre-push.sh` +Expected: every step passes and the script exits 0. + +`lake shake` may print a `PANIC at Option.get!` trace from +`Lake.Shake.visitModule` when the first module under a new +`GebTests/Mathlib//` appears. It exits 0 when it occurs and reproduces +with an unrelated control module at the same path, so it is a shake artifact +rather than a property of this branch. A non-zero exit is a real failure. + +- [ ] **Step 2: Confirm the imports are minimal** + +Run: `lake shake --add-public --keep-prefix Geb GebTests` +Expected: the two new modules are **absent** from the reported file list. +The presence of either means it names `Mathlib.Data.Fin.Tuple.Basic` or +`Mathlib.Data.Fin.VecNotation`; remove the import, since +`Mathlib.Logic.Equiv.Fin.Basic` supplies both. + +The test module's declarations are module-private — it uses plain `import` +with no `public section` — so they cannot be inspected by `#print axioms` +from another file. `lake lint -- GebTests`, which Step 1 already ran, is what +enforces the axiom budget over them: it runs `GebMeta.detectNonstandardAxiom` +across the whole `GebTests` environment, private declarations included. + +- [ ] **Step 3: Commit only if the gate changed something** + +If the checklist regenerated a TOC or reformatted anything: + +```bash +jj commit -m "chore: satisfy the pre-push checklist for the Bellantoni-Cook branch" +``` + +Otherwise skip — a clean gate leaves no change to commit. + +--- + +## Task 8: Remove the spec and the plan + +**Files:** + +- Delete: `docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md` +- Delete: `docs/superpowers/plans/2026-08-04-bellantoni-cook.md` + +**Interfaces:** + +- Consumes: nothing +- Produces: a branch whose working tree carries only persistent content + +CONTRIBUTING.md § Concern shape: specs and plans record how the current +state was reached, not what it is, so they belong in history and not on an +active branch. They remain reachable in the commits of Task 1. + +- [ ] **Step 1: Delete both files** + +```bash +rm docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md +rm docs/superpowers/plans/2026-08-04-bellantoni-cook.md +``` + +- [ ] **Step 2: Confirm nothing else changed** + +Run: `jj status` +Expected: exactly two lines, both `D`. + +- [ ] **Step 3: Re-check the Markdown** + +The removal touches no `.lean` file, so the full checklist of Task 7 need +not run again; only its Markdown steps can be affected. + +```bash +doctoc --dryrun --update-only . +markdownlint-cli2 '**/*.md' +``` + +Expected: `Everything is OK.` and `Summary: 0 issues in 0 files`. + +- [ ] **Step 4: Commit** + +```bash +jj commit -m "doc: remove the Bellantoni-Cook spec and plan" +``` + +- [ ] **Step 5: Advance the bookmark** + +```bash +jj bookmark set feat/bellantoni-cook -r @- +``` + +Run: `jj log -r 'main..feat/bellantoni-cook'` +Expected: eight or nine commits — spec, plan, three library, tests, docs, +the removal, and the gate's only if it had something to commit. + +**Do not push.** AGENTS.md § No `jj git push` without user line-by-line +review: every push, including a first creation, waits on the user reading +the diff. From 5e3fef8eeea52ad4c1ac3a91582c051470ebd874 Mon Sep 17 00:00:00 2001 From: "Terence M. Rokop" Date: Tue, 4 Aug 2026 13:51:58 -0700 Subject: [PATCH 3/9] feat(computability): add the Bellantoni-Cook signature functor --- Geb/Mathlib.lean | 1 + Geb/Mathlib/Computability.lean | 12 ++ Geb/Mathlib/Computability/BellantoniCook.lean | 158 ++++++++++++++++++ 3 files changed, 171 insertions(+) create mode 100644 Geb/Mathlib/Computability.lean create mode 100644 Geb/Mathlib/Computability/BellantoniCook.lean diff --git a/Geb/Mathlib.lean b/Geb/Mathlib.lean index c6d1bc3..6438b33 100644 --- a/Geb/Mathlib.lean +++ b/Geb/Mathlib.lean @@ -6,6 +6,7 @@ Authors: Terence Rokop module public import Geb.Mathlib.CategoryTheory +public import Geb.Mathlib.Computability public import Geb.Mathlib.Data public import Geb.Mathlib.Logic diff --git a/Geb/Mathlib/Computability.lean b/Geb/Mathlib/Computability.lean new file mode 100644 index 0000000..fd3eaeb --- /dev/null +++ b/Geb/Mathlib/Computability.lean @@ -0,0 +1,12 @@ +/- +Copyright (c) 2026 Terence Rokop. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Terence Rokop +-/ +module + +public import Geb.Mathlib.Computability.BellantoniCook + +/-! +# Computability — index +-/ diff --git a/Geb/Mathlib/Computability/BellantoniCook.lean b/Geb/Mathlib/Computability/BellantoniCook.lean new file mode 100644 index 0000000..83dc2b9 --- /dev/null +++ b/Geb/Mathlib/Computability/BellantoniCook.lean @@ -0,0 +1,158 @@ +/- +Copyright (c) 2026 Terence Rokop. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Terence Rokop +-/ +module + +public import Geb.Mathlib.Data.PFunctor.Slice.W +public import Geb.Mathlib.Data.PFunctor.Univariate.Finitary +public import Mathlib.Logic.Equiv.Fin.Basic + +/-! +# The function class `B` of Bellantoni and Cook + +The syntax of the function class `B` and its interpretation, following +[HeraudNowak2011] § 3.2. Terms of `B` are built from a constant zero, +projections, two successors, a predecessor and a conditional, and are closed +under a composition and a recursion that distinguish normal from safe +argument positions; the distinction is what bounds the growth rate of the +definable functions. + +The class defined here is the reformulation of § 3.2, not the class of +[BellantoniCook1992]. Two differences: the conditional takes four safe +arguments and branches three ways, on the empty, odd and even bitstrings, +where the original branches two ways on parity and treats the empty +bitstring as even; and the base case of the recursion is the empty +bitstring, where the original's is every bitstring denoting zero. + +The two sources transpose the conditional's last two safe arguments. The +order here follows the authors' Coq development, that being the artifact +against which the paper's theorems were machine-checked. + +## Main definitions + +* `BellantoniCook.Shape` — the seven constructor forms, with their arities + as parameters. +* `BellantoniCook.Direction` — the subterm positions of a shape. +* `BellantoniCook.rc` — the arity each subterm position must carry. +* `BellantoniCook.q` — the arity a shape produces. +* `BellantoniCook.sig` — the signature, as a slice polynomial functor over + `ℕ × ℕ`. +* `BellantoniCook.BC` — an expression of `B`: a `sig`-tree whose every node + respects `rc`. +* `BellantoniCook.BC.arity` — its pair of normal and safe arities. +* `BellantoniCook.BCOf` — the expressions of a given arity pair. +* `BellantoniCook.Sem` — the meaning of an arity pair: a function of a + normal and a safe environment. +* `BellantoniCook.transport` — transport of a meaning along an equality of + arity pairs. +* `BellantoniCook.evalRec` — the recursion on the consumed bitstring. +* `BellantoniCook.evalValue` — the meaning of one node from its children's. +* `BellantoniCook.evalStep` — `evalValue` as a slice algebra. +* `BellantoniCook.BC.eval` — the interpretation, by the slice W-type's + eliminator. + +## Implementation notes + +This repository expresses all recursion through recursors, admitting +neither a self-referential `inductive` nor a self-calling `def`, so the +arity-indexed syntax is the slice W-type of `sig` and the interpretation is +one application of `SlicePFunctor.W.elim`. `Shape` is itself non-recursive +and so is the shape set of a `PFunctor`, not a datatype the rule reaches. + +`evalValue` is separate from `evalStep` because the match on `Shape` must +generalize the compatibility hypothesis, which arrives bundled in +`SliceDomPFunctor.Obj`. A child's meaning carries the index it was built at +rather than the index `rc` prescribes, equal but not definitionally so; +`transport` carries it across, with the motive of `▸` fixed once instead of +at each of the six sites. + +`Direction`, `rc` and `q` are `@[reducible]`. Instance search does not +delta-reduce a semireducible definition, and every numeral in `evalValue` +elaborates against `Fin (q a).1` or `Direction a`. + +`finEnumFin` and `finEnumCompDirection` are `scoped`, and hand-built: +mathlib's `FinEnum` instances depend on `Classical.choice`, which +`lake lint` rejects, and an unscoped instance at the head symbol `FinEnum +(Fin _)` would compete with `FinEnum.fin` wherever `Geb` is imported. + +## References + +* [HeraudNowak2011] +* [BellantoniCook1992] + +## Tags + +Bellantoni-Cook, polytime, implicit computational complexity, safe +recursion, W-type, polynomial functor +-/ + +namespace BellantoniCook + +public section + +/-- The seven constructor forms of `B`, each carrying its arities as +parameters: `zero` the constant empty bitstring; `proj n s i` the `i`th of +`n` normal and `s` safe variables; `succ b` the successor appending the bit +`b`; `pred` the predecessor; `cond` the four-argument conditional; +`safeRec n s` the recursion producing arity `(n + 1, s)`; and `comp n s m k` +the composition of an expression of arity `(m, k)` with `m` normal and `k` +safe argument expressions of arity `(n, 0)` and `(n, s)`. -/ +inductive Shape + | zero + | proj (n s : ℕ) (i : Fin (n + s)) + | succ (b : Bool) + | pred + | cond + | safeRec (n s : ℕ) + | comp (n s m k : ℕ) + +/-- The subterm positions of a shape. The five base forms have none; +`safeRec` has three, its base and its two step expressions; `comp` has its +head, its `m` normal arguments and its `k` safe arguments. -/ +@[expose, reducible] def Direction : Shape → Type + | .zero => Fin 0 + | .proj _ _ _ => Fin 0 + | .succ _ => Fin 0 + | .pred => Fin 0 + | .cond => Fin 0 + | .safeRec _ _ => Fin 3 + | .comp _ _ m k => Unit ⊕ Fin m ⊕ Fin k + +/-- The arity each subterm position must carry: the hypotheses of the +arity relation of [HeraudNowak2011] § 3.2. -/ +@[expose, reducible] def rc : (a : Shape) → Direction a → ℕ × ℕ + | .zero, i => i.elim0 + | .proj _ _ _, i => i.elim0 + | .succ _, i => i.elim0 + | .pred, i => i.elim0 + | .cond, i => i.elim0 + | .safeRec n s, ⟨0, _⟩ => (n, s) + | .safeRec n s, _ => (n + 1, s + 1) + | .comp _ _ m k, .inl () => (m, k) + | .comp n _ _ _, .inr (.inl _) => (n, 0) + | .comp n s _ _, .inr (.inr _) => (n, s) + +/-- The arity a shape produces: the conclusions of the arity relation of +[HeraudNowak2011] § 3.2. -/ +@[expose, reducible] def q : Shape → ℕ × ℕ + | .zero => (0, 0) + | .proj n s _ => (n, s) + | .succ _ => (0, 1) + | .pred => (0, 1) + | .cond => (0, 4) + | .safeRec n s => (n + 1, s) + | .comp n s _ _ => (n, s) + +/-- The signature of `B` as a slice polynomial functor over `ℕ × ℕ`, the +index being the pair of normal and safe arities. -/ +@[expose] def sig : SlicePFunctor (ℕ × ℕ) (ℕ × ℕ) where + A := Shape + B := Direction + r := fun x ↦ rc x.1 x.2 + q := q + +end + +end BellantoniCook From 6715812452286dfb9472add1281401ce0a1cf5ef Mon Sep 17 00:00:00 2001 From: "Terence M. Rokop" Date: Tue, 4 Aug 2026 13:58:48 -0700 Subject: [PATCH 4/9] feat(computability): add choice-free finiteness for the signature --- Geb/Mathlib/Computability/BellantoniCook.lean | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/Geb/Mathlib/Computability/BellantoniCook.lean b/Geb/Mathlib/Computability/BellantoniCook.lean index 83dc2b9..a9fd6f6 100644 --- a/Geb/Mathlib/Computability/BellantoniCook.lean +++ b/Geb/Mathlib/Computability/BellantoniCook.lean @@ -153,6 +153,36 @@ index being the pair of normal and safe arities. -/ r := fun x ↦ rc x.1 x.2 q := q +/-- A choice-free `FinEnum (Fin n)`: the cardinality is `n` and the +enumeration is the identity. `scoped`, so that it does not compete with +mathlib's `FinEnum.fin` at the same head symbol outside this namespace. -/ +scoped instance finEnumFin (n : ℕ) : + FinEnum (Fin n) where + card := n + equiv := Equiv.refl _ + decEq := inferInstance + +/-- A choice-free `FinEnum` for `comp`'s directions. `scoped`, for the same +reason as `finEnumFin`. -/ +scoped instance finEnumCompDirection (m k : ℕ) : + FinEnum (Unit ⊕ Fin m ⊕ Fin k) where + card := 1 + (m + k) + equiv := (Equiv.sumCongr finOneEquiv.symm finSumFinEquiv).trans finSumFinEquiv + decEq := inferInstance + +/-- Every shape has finitely many directions, which is what makes +admissibility of a `sig`-tree decidable. The branches ascribe their +instances explicitly: instance search stops at reducible transparency on the +projection `sig.B a`, so a bare `inferInstance` does not find them. -/ +instance sigFinitary : sig.toPFunctor.Finitary + | .zero => inferInstanceAs (FinEnum (Fin 0)) + | .proj _ _ _ => inferInstanceAs (FinEnum (Fin 0)) + | .succ _ => inferInstanceAs (FinEnum (Fin 0)) + | .pred => inferInstanceAs (FinEnum (Fin 0)) + | .cond => inferInstanceAs (FinEnum (Fin 0)) + | .safeRec _ _ => inferInstanceAs (FinEnum (Fin 3)) + | .comp _ _ m k => inferInstanceAs (FinEnum (Unit ⊕ Fin m ⊕ Fin k)) + end end BellantoniCook From 2c5fcbbbe97a4120187447ab911691699ac765f6 Mon Sep 17 00:00:00 2001 From: "Terence M. Rokop" Date: Tue, 4 Aug 2026 14:03:01 -0700 Subject: [PATCH 5/9] feat(computability): add the Bellantoni-Cook syntax and semantics --- Geb/Mathlib/Computability/BellantoniCook.lean | 71 +++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/Geb/Mathlib/Computability/BellantoniCook.lean b/Geb/Mathlib/Computability/BellantoniCook.lean index a9fd6f6..e6cfcba 100644 --- a/Geb/Mathlib/Computability/BellantoniCook.lean +++ b/Geb/Mathlib/Computability/BellantoniCook.lean @@ -183,6 +183,77 @@ instance sigFinitary : sig.toPFunctor.Finitary | .safeRec _ _ => inferInstanceAs (FinEnum (Fin 3)) | .comp _ _ m k => inferInstanceAs (FinEnum (Unit ⊕ Fin m ⊕ Fin k)) +/-- An expression of `B`: a `sig`-tree every node of which carries children +at the indices `rc` prescribes. -/ +@[expose] def BC : Type := sig.W + +/-- The arity pair of an expression: its normal and safe arities. -/ +@[expose] def BC.arity : BC → ℕ × ℕ := sig.wIndex + +/-- The expressions of arity `(n, s)`, which is the arity relation of +[HeraudNowak2011] § 3.2 as a type rather than a side condition. -/ +@[expose] def BCOf (n s : ℕ) : Type := { e : BC // e.arity = (n, s) } + +/-- The meaning of an arity pair: a function of a normal and a safe +environment, each a tuple of bitstrings, returning a bitstring. -/ +@[expose] def Sem : ℕ × ℕ → Type := + fun i ↦ (Fin i.1 → List Bool) → (Fin i.2 → List Bool) → List Bool + +/-- Transport of a meaning along an equality of arity pairs. Named so that +the motive of `▸` is fixed once rather than inferred at each use in +`evalValue`. -/ +@[expose] def transport {i j : ℕ × ℕ} (h : i = j) (v : Sem i) : Sem j := h ▸ v + +/-- The recursion `safeRec` performs on its first normal argument, by +`List.rec`. The base case is the empty bitstring; a step consumes the low +bit `b`, passes the remaining bitstring `v` as the new first normal +argument, and passes the recursive value in safe position. -/ +@[expose] def evalRec {n s : ℕ} (g : Sem (n, s)) + (h₀ h₁ : Sem (n + 1, s + 1)) : List Bool → Sem (n, s) := + List.rec g (fun b v ih x y ↦ + (if b then h₁ else h₀) (Fin.cons v x) (Fin.cons (ih x y) y)) + +/-- The meaning of one node, from its children's meanings and the proof that +each child's index is the one `rc` prescribes. A separate definition from +`evalStep` because the match on `Shape` must generalize that proof. + +`cond` reads its first safe argument and returns the second, third or fourth +according as it is empty, odd or even — the ordering of the authors' Coq +development. `comp` applies its head's meaning to the normal arguments' +meanings, each in the empty safe environment, and to the safe arguments'. -/ +@[expose] def evalValue : (a : Shape) → (c : Direction a → Σ i, Sem i) → + (∀ b, (c b).1 = rc a b) → Sem (q a) + | .zero, _, _ => fun _ _ ↦ [] + | .proj _ _ i, _, _ => fun x y ↦ Fin.append x y i + | .succ b, _, _ => fun _ y ↦ b :: y 0 + | .pred, _, _ => fun _ y ↦ (y 0).tail + | .cond, _, _ => fun _ y ↦ + match y 0 with + | [] => y 1 + | true :: _ => y 2 + | false :: _ => y 3 + | .safeRec _ _, c, h => fun x y ↦ + evalRec (transport (h 0) (c 0).2) (transport (h 1) (c 1).2) + (transport (h 2) (c 2).2) (x 0) (Fin.tail x) y + | .comp _ _ _ _, c, h => fun x y ↦ + transport (h (.inl ())) (c (.inl ())).2 + (fun i ↦ transport (h (.inr (.inl i))) (c (.inr (.inl i))).2 x Fin.elim0) + (fun j ↦ transport (h (.inr (.inr j))) (c (.inr (.inr j))).2 x y) + +/-- `evalValue` as an algebra for `sig` in the slice over `ℕ × ℕ`. Returning +the shape's own output index as the first component makes the eliminator's +coherence obligation hold by `rfl`. -/ +@[expose] def evalStep : + sig.toSliceDomPFunctor.Obj (Sigma.fst (β := Sem)) → Σ i, Sem i := + fun z ↦ ⟨sig.q z.1.1, + evalValue z.1.1 z.1.2 + ((sig.toSliceDomPFunctor.compatible_iff _ z.1.1 z.1.2).mp z.2)⟩ + +/-- The interpretation of an expression: its arity pair together with its +meaning at that pair, by the slice W-type's eliminator. -/ +@[expose] def BC.eval : BC → Σ i, Sem i := + SlicePFunctor.W.elim sig (Σ i, Sem i) (Sigma.fst (β := Sem)) evalStep rfl + end end BellantoniCook From f20abbb2671cb3b32ddb8659efc375145d2e8d7c Mon Sep 17 00:00:00 2001 From: "Terence M. Rokop" Date: Tue, 4 Aug 2026 14:08:34 -0700 Subject: [PATCH 6/9] test(computability): add worked Bellantoni-Cook expressions --- GebTests/Mathlib.lean | 1 + GebTests/Mathlib/Computability.lean | 12 ++ .../Mathlib/Computability/BellantoniCook.lean | 204 ++++++++++++++++++ 3 files changed, 217 insertions(+) create mode 100644 GebTests/Mathlib/Computability.lean create mode 100644 GebTests/Mathlib/Computability/BellantoniCook.lean diff --git a/GebTests/Mathlib.lean b/GebTests/Mathlib.lean index 7c84581..bda8fc6 100644 --- a/GebTests/Mathlib.lean +++ b/GebTests/Mathlib.lean @@ -6,6 +6,7 @@ Authors: Terence Rokop module import GebTests.Mathlib.CategoryTheory +import GebTests.Mathlib.Computability import GebTests.Mathlib.Data import GebTests.Mathlib.Logic diff --git a/GebTests/Mathlib/Computability.lean b/GebTests/Mathlib/Computability.lean new file mode 100644 index 0000000..e966dab --- /dev/null +++ b/GebTests/Mathlib/Computability.lean @@ -0,0 +1,12 @@ +/- +Copyright (c) 2026 Terence Rokop. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Terence Rokop +-/ +module + +import GebTests.Mathlib.Computability.BellantoniCook + +/-! +# Computability tests — index +-/ diff --git a/GebTests/Mathlib/Computability/BellantoniCook.lean b/GebTests/Mathlib/Computability/BellantoniCook.lean new file mode 100644 index 0000000..a417e7a --- /dev/null +++ b/GebTests/Mathlib/Computability/BellantoniCook.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2026 Terence Rokop. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Terence Rokop +-/ +module + +import Geb.Mathlib.Computability.BellantoniCook +import Geb.Mathlib.Data.PFunctor.Slice.Decidable + +/-! +# Worked expressions of the Bellantoni-Cook class + +The `plus` and `mult` of [HeraudNowak2011] § 3.2, a recursion whose two step +expressions differ, four single-node expressions, and one inadmissible raw +tree. Each expression is built in two steps — a raw tree bound as its own +definition, then the admissible expression — because an inline `WType.mk` +application blocks the instance search that `decide` needs. + +`plus` and `mult` are transcribed with the arities of the authors' Coq +development. The composition superscripts printed in § 3.2's `mult` are +`plus`'s and do not satisfy the paper's own arity relation. + +## Main statements + +The thirteen assertions below: twelve expected outputs of `BC.eval`, and one +inadmissible tree. + +## References + +* [HeraudNowak2011] + +## Tags + +Bellantoni-Cook, polytime, safe recursion +-/ + +set_option linter.privateModule false + +open BellantoniCook + +/-- The children of a `comp` node, in the order `Direction` gives them: the +head, then the normal arguments, then the safe arguments. -/ +def compChildren {m k : ℕ} (h : sig.toPFunctor.W) + (gN : Fin m → sig.toPFunctor.W) (gS : Fin k → sig.toPFunctor.W) : + Unit ⊕ Fin m ⊕ Fin k → sig.toPFunctor.W := + Sum.elim (fun _ ↦ h) (Sum.elim gN gS) + +/-- The step expression of `plus`: the successor appending `true`, applied +to the recursive value. -/ +def plusStepRaw : sig.toPFunctor.W := + WType.mk (.comp 1 2 0 1) + (compChildren (WType.mk (.succ true) Fin.elim0) Fin.elim0 + ![WType.mk (.proj 1 2 1) Fin.elim0]) + +/-- The step expression of `plus`, admissible. -/ +def plusStep : BC := ⟨plusStepRaw, by decide⟩ + +/-- `plus`, of arity `(1, 1)`: it prepends one `true` per bit of its normal +argument to its safe argument. -/ +def plusRaw : sig.toPFunctor.W := + WType.mk (.safeRec 0 1) + ![WType.mk (.proj 0 1 0) Fin.elim0, plusStep.val, plusStep.val] + +/-- `plus`, admissible. -/ +def plus : BC := ⟨plusRaw, by decide⟩ + +/-- The base expression of `mult`: the constant empty bitstring at +arity `(1, 0)`. -/ +def multBaseRaw : sig.toPFunctor.W := + WType.mk (.comp 1 0 0 0) + (compChildren (WType.mk .zero Fin.elim0) Fin.elim0 Fin.elim0) + +/-- The base expression of `mult`, admissible. -/ +def multBase : BC := ⟨multBaseRaw, by decide⟩ + +/-- The step expression of `mult`: `plus` of the second normal argument and +the recursive value. -/ +def multStepRaw : sig.toPFunctor.W := + WType.mk (.comp 2 1 1 1) + (compChildren plus.val ![WType.mk (.proj 2 0 1) Fin.elim0] + ![WType.mk (.proj 2 1 2) Fin.elim0]) + +/-- The step expression of `mult`, admissible. -/ +def multStep : BC := ⟨multStepRaw, by decide⟩ + +/-- `mult`, of arity `(2, 0)`: it produces one `true` per pair of bits of +its two normal arguments. -/ +def multRaw : sig.toPFunctor.W := + WType.mk (.safeRec 1 0) ![multBase.val, multStep.val, multStep.val] + +/-- `mult`, admissible. -/ +def mult : BC := ⟨multRaw, by decide⟩ + +/-- `plus` at its declared arity. Elaborating this is exactly the assertion +that `BC.arity plus` is `(1, 1)`. -/ +def plusOf : BCOf 1 1 := ⟨plus, rfl⟩ + +/-- `mult` at its declared arity. -/ +def multOf : BCOf 2 0 := ⟨mult, rfl⟩ + +/-- `plus` on an empty normal argument returns its safe argument. -/ +theorem eval_plus_nil : (BC.eval plus).2 ![[]] ![[false]] = [false] := rfl + +/-- `plus` prepends one `true` per bit of its normal argument. -/ +theorem eval_plus_cons : + (BC.eval plus).2 ![[true, true]] ![[false]] = [true, true, false] := rfl + +/-- `mult` produces one `true` per pair of bits of its two normal +arguments. -/ +theorem eval_mult : + (BC.eval mult).2 ![[true, true], [true, true, true]] ![] = + List.replicate 6 true := rfl + +/-- A recursion whose two step expressions differ: the `false` branch +returns the remaining bitstring, the `true` branch recurses. Without it no +assertion here would distinguish the two step expressions, `plus` and `mult` +passing the same expression as both. -/ +def branchRecRaw : sig.toPFunctor.W := + WType.mk (.safeRec 0 0) + ![WType.mk .zero Fin.elim0, WType.mk (.proj 1 1 0) Fin.elim0, + WType.mk (.proj 1 1 1) Fin.elim0] + +/-- The discriminating recursion, admissible. -/ +def branchRec : BC := ⟨branchRecRaw, by decide⟩ + +/-- On a `false`-headed argument the `false` branch returns the remaining +bitstring. Arguments of length one do not discriminate the branches: both +readings return the empty bitstring. -/ +theorem eval_branchRec_false : + (BC.eval branchRec).2 ![[false, true]] ![] = [true] := rfl + +/-- On a `true`-headed argument the `true` branch recurses. -/ +theorem eval_branchRec_true : + (BC.eval branchRec).2 ![[true, true]] ![] = [] := rfl + +/-- The predecessor as a single node. -/ +def predTermRaw : sig.toPFunctor.W := WType.mk .pred Fin.elim0 + +/-- The predecessor, admissible. -/ +def predTerm : BC := ⟨predTermRaw, by decide⟩ + +/-- The predecessor of the empty bitstring is the empty bitstring. -/ +theorem eval_predTerm_nil : (BC.eval predTerm).2 ![] ![[]] = [] := rfl + +/-- The predecessor drops the low bit. -/ +theorem eval_predTerm_cons : + (BC.eval predTerm).2 ![] ![[true, false]] = [false] := rfl + +/-- The conditional as a single node. -/ +def condTermRaw : sig.toPFunctor.W := WType.mk .cond Fin.elim0 + +/-- The conditional, admissible. -/ +def condTerm : BC := ⟨condTermRaw, by decide⟩ + +/-- On the empty bitstring the conditional returns its second safe +argument. -/ +theorem eval_condTerm_empty : + (BC.eval condTerm).2 ![] ![[], [false], [true], [true, true]] = [false] := + rfl + +/-- On an odd bitstring it returns its third. The authors' Coq development +assigns the third to the odd case and the fourth to the even case; § 3.2 +prints them the other way round. -/ +theorem eval_condTerm_odd : + (BC.eval condTerm).2 ![] ![[true], [false], [true], [true, true]] = + [true] := rfl + +/-- On an even bitstring it returns its fourth. -/ +theorem eval_condTerm_even : + (BC.eval condTerm).2 ![] ![[false], [false], [true], [true, true]] = + [true, true] := rfl + +/-- A projection onto a normal variable, as a single node. -/ +def projNTermRaw : sig.toPFunctor.W := WType.mk (.proj 1 1 0) Fin.elim0 + +/-- The normal projection, admissible. -/ +def projNTerm : BC := ⟨projNTermRaw, by decide⟩ + +/-- The normal projection returns the normal argument. -/ +theorem eval_projNTerm : + (BC.eval projNTerm).2 ![[true]] ![[false]] = [true] := rfl + +/-- A projection onto a safe variable, as a single node. Together with +`projNTerm` this separates the two halves of `Fin.append`, which a +mistranscribed index would silently permute. -/ +def projSTermRaw : sig.toPFunctor.W := WType.mk (.proj 1 1 1) Fin.elim0 + +/-- The safe projection, admissible. -/ +def projSTerm : BC := ⟨projSTermRaw, by decide⟩ + +/-- The safe projection returns the safe argument. -/ +theorem eval_projSTerm : + (BC.eval projSTerm).2 ![[true]] ![[false]] = [false] := rfl + +/-- `plusStepRaw` with its safe argument replaced by an expression of arity +`(2, 0)` where the signature demands `(1, 2)`. -/ +def badRaw : sig.toPFunctor.W := + WType.mk (.comp 1 2 0 1) + (compChildren (WType.mk (.succ true) Fin.elim0) Fin.elim0 + ![WType.mk (.proj 2 0 1) Fin.elim0]) + +/-- The inadmissible tree is rejected, so admissibility is not vacuous. -/ +theorem wValid_badRaw_eq_false : decide (sig.WValid badRaw) = false := rfl From 058a4946afdfc690ceaf179d0afbc6846128bd4f Mon Sep 17 00:00:00 2001 From: "Terence M. Rokop" Date: Tue, 4 Aug 2026 14:16:24 -0700 Subject: [PATCH 7/9] doc: record the Bellantoni-Cook module and its follow-on work --- TODO.md | 33 +++++++++++++++++++++++++++++++++ docs/index.md | 8 ++++++++ docs/references.bib | 29 +++++++++++++++++++++++++++++ docs/references.md | 4 ++++ 4 files changed, 74 insertions(+) diff --git a/TODO.md b/TODO.md index b536382..ecc2564 100644 --- a/TODO.md +++ b/TODO.md @@ -22,6 +22,7 @@ - [Exhaustive verification of presheaf PRA laws for finite instances](#exhaustive-verification-of-presheaf-pra-laws-for-finite-instances) - [PRA functors over finite-specification base categories](#pra-functors-over-finite-specification-base-categories) - [Finite categories as a full subcategory of `Cat`](#finite-categories-as-a-full-subcategory-of-cat) + - [Bellantoni-Cook](#bellantoni-cook) - [Triggers (do when condition fires)](#triggers-do-when-condition-fires) @@ -407,6 +408,23 @@ exercised by the PRA item above. Depends on the `FinCat` workstream. +### Bellantoni-Cook + +Three items, in dependency order, over +`Geb/Mathlib/Computability/BellantoniCook.lean`. + +1. `MultiPoly`, the multivariate polynomial library of the reference + development. Required by its `BC_to_Cobham.v:2`, by its + `Cobham_to_BC.v:2`, and by Proposition 2, whose statement + `polymax_bounding` (`BC.v:1128`) is over `poly_BC` (`:1075`), built from + `pcst`, `pproj`, `pplus`, `pmult`, `pcomp`, `pshift` and `pplusl`. + Returns the polynomial apparatus items 2 and 3 are stated over. +2. Proposition 2, the polymax bounding of `B`. Depends on 1. Returns the + length bound the translation of item 3 requires. +3. Cobham's class and the translations of Theorems 1 and 2. Depends on 1 + and 2. Returns the characterization of the polynomial-time functions, + and is the consumer that justifies the definitions already committed. + ## Triggers (do when condition fires) - **Choice-free bound for `Fin.divNat` in Batteries**: @@ -616,3 +634,18 @@ Depends on the `FinCat` workstream. the section, and its siblings do not although each declares named theorems. `docs/rules/lean-coding.md` § Documentation requires a section when it has content. Trigger: the next occasion to revise those modules. +- **A workstream needs programmable building blocks for terms of `B`**: + port the derived function library of the reference development's + `BCLib.v`, which depends only on the syntax and semantics already + committed. +- **A second consumer of `BellantoniCook.finEnumFin` or + `finEnumCompDirection` appears**: move them to + `Geb/Mathlib/Data/FinEnum.lean`, the repository's home for choice-free + `FinEnum` support. They are `scoped` in + `Geb/Mathlib/Computability/BellantoniCook.lean`. +- **A consumer needs `DecidableEq` or `Repr` for `BellantoniCook.BC`**: + derive them on `Shape` and lift along `sig.W`'s subtype. +- **A workstream needs the polytime checker of [HeraudNowak2011] as a + term-level artifact**: add an untyped `Ast` and + `check : Ast → Option ((n s : ℕ) × BellantoniCook.BCOf n s)` over + `SlicePFunctor.decidableWValid`. diff --git a/docs/index.md b/docs/index.md index 28218f1..e0bcda0 100644 --- a/docs/index.md +++ b/docs/index.md @@ -180,6 +180,14 @@ import-direction rules above are enforced by `WType.elim` fold `wValidData`/`wValidStep` alongside the tree's root index in a single pass, with correctness lemma `wValidBool_eq_true_iff`. `Classical.choice`-free. +- `Geb/Mathlib/Computability/BellantoniCook.lean` — the function class `B` + of [HeraudNowak2011] § 3.2: its arity relation as a `SlicePFunctor` over + `ℕ × ℕ`, its syntax as that functor's slice W-type, and its semantics by + the W-type's eliminator. Depends on + `Geb.Mathlib.Data.PFunctor.Slice.W` and + `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`. Every declaration of the + module has axioms within `propext` and `Quot.sound`; `sig` and + `finEnumFin` have none. - `Geb/Mathlib/Data/PFunctor/Presheaf/Decidable.lean` — decidability of the presheaf functor's naturality predicates. `PresheafDomPFunctorData.decidableIsNatural` decides `IsNatural` diff --git a/docs/references.bib b/docs/references.bib index 3ebdd32..f948965 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -253,6 +253,35 @@ @article{AvanziniDalLago2018 doi = {10.1016/j.ic.2018.05.003}, } +@inproceedings{HeraudNowak2011, + author = {H{\'e}raud, Sylvain and Nowak, David}, + title = {A Formalization of Polytime Functions}, + booktitle = {Interactive Theorem Proving (ITP 2011)}, + series = {Lecture Notes in Computer Science}, + volume = {6898}, + pages = {119--134}, + publisher = {Springer}, + year = {2011}, + doi = {10.1007/978-3-642-22863-6_11}, + eprint = {1102.5495}, + archivePrefix = {arXiv}, + primaryClass = {cs.CC}, + note = {This repository cites the arXiv version's section and + page numbering.}, +} + +@article{BellantoniCook1992, + author = {Bellantoni, Stephen and Cook, Stephen}, + title = {A new recursion-theoretic characterization of the + polytime functions}, + journal = {Computational Complexity}, + volume = {2}, + number = {2}, + pages = {97--110}, + year = {1992}, + doi = {10.1007/BF01201998}, +} + @misc{nLabSkeletalCategory, author = {{nLab authors}}, title = {Skeletal category}, diff --git a/docs/references.md b/docs/references.md index 95fd932..bfa5dfa 100644 --- a/docs/references.md +++ b/docs/references.md @@ -185,6 +185,10 @@ Conditions for considering these targets are in - [Mathlib.Computability.Primrec](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/Primrec.html) - [Mathlib.Computability.TMComputable](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/TMComputable.html) - [Mathlib.Computability.TuringMachine](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/TuringMachine.html) +- [davidnowak/bellantonicook](https://github.com/davidnowak/bellantonicook) + — the Coq development accompanying [HeraudNowak2011], at commit + `1f03b9296104646ddc2b2b4b12e35a6619c17a99`. Licensed CeCILL; no code is + taken from it. ## Monad algebra From f153e797ee48bd69bdb06941c488b778fb3689cd Mon Sep 17 00:00:00 2001 From: "Terence M. Rokop" Date: Tue, 4 Aug 2026 14:45:56 -0700 Subject: [PATCH 8/9] fix: cover the successor's bit and correct three documentation notes --- Geb/Mathlib/Computability/BellantoniCook.lean | 7 +++++++ .../Mathlib/Computability/BellantoniCook.lean | 16 ++++++++++++++-- TODO.md | 6 ++++-- docs/index.md | 6 +++--- 4 files changed, 28 insertions(+), 7 deletions(-) diff --git a/Geb/Mathlib/Computability/BellantoniCook.lean b/Geb/Mathlib/Computability/BellantoniCook.lean index e6cfcba..1487e63 100644 --- a/Geb/Mathlib/Computability/BellantoniCook.lean +++ b/Geb/Mathlib/Computability/BellantoniCook.lean @@ -72,6 +72,13 @@ at each of the six sites. delta-reduce a semireducible definition, and every numeral in `evalValue` elaborates against `Fin (q a).1` or `Direction a`. +`Mathlib.Logic.Equiv.Fin.Basic` is imported for `finSumFinEquiv`. It +transitively supplies `Mathlib.Data.Fin.Tuple.Basic`, the source of +`Fin.cons`, `Fin.tail` and `Fin.append` used here, and +`Mathlib.Data.Fin.VecNotation`, reached the same way by the test module's +`![…]` notation. Neither is imported by name, so that `lake shake` does not +report either as a redundant import. + `finEnumFin` and `finEnumCompDirection` are `scoped`, and hand-built: mathlib's `FinEnum` instances depend on `Classical.choice`, which `lake lint` rejects, and an unscoped instance at the head symbol `FinEnum diff --git a/GebTests/Mathlib/Computability/BellantoniCook.lean b/GebTests/Mathlib/Computability/BellantoniCook.lean index a417e7a..18f254a 100644 --- a/GebTests/Mathlib/Computability/BellantoniCook.lean +++ b/GebTests/Mathlib/Computability/BellantoniCook.lean @@ -23,8 +23,8 @@ development. The composition superscripts printed in § 3.2's `mult` are ## Main statements -The thirteen assertions below: twelve expected outputs of `BC.eval`, and one -inadmissible tree. +The fourteen assertions below: thirteen expected outputs of `BC.eval`, and +one inadmissible tree. ## References @@ -193,6 +193,18 @@ def projSTerm : BC := ⟨projSTermRaw, by decide⟩ theorem eval_projSTerm : (BC.eval projSTerm).2 ![[true]] ![[false]] = [false] := rfl +/-- The successor appending `false`, as a single node. Every other `succ` +node in this file carries `true`, so this one separates the constructor's +bit argument, which a transcription dropping it would not catch. -/ +def succFalseTermRaw : sig.toPFunctor.W := WType.mk (.succ false) Fin.elim0 + +/-- The `false`-successor, admissible. -/ +def succFalseTerm : BC := ⟨succFalseTermRaw, by decide⟩ + +/-- The `false`-successor prepends `false` to its safe argument. -/ +theorem eval_succFalseTerm : + (BC.eval succFalseTerm).2 ![] ![[true]] = [false, true] := rfl + /-- `plusStepRaw` with its safe argument replaced by an expression of arity `(2, 0)` where the signature demands `(1, 2)`. -/ def badRaw : sig.toPFunctor.W := diff --git a/TODO.md b/TODO.md index ecc2564..20d7a40 100644 --- a/TODO.md +++ b/TODO.md @@ -636,8 +636,10 @@ Three items, in dependency order, over when it has content. Trigger: the next occasion to revise those modules. - **A workstream needs programmable building blocks for terms of `B`**: port the derived function library of the reference development's - `BCLib.v`, which depends only on the syntax and semantics already - committed. + `BCLib.v`. Its `Require Import` line also names `BellantoniCook.Bitstring`, + whose bitstring type is the notation `bs := list bool`; that type is + `List Bool` directly here, so the port is unaffected by the additional + dependency. - **A second consumer of `BellantoniCook.finEnumFin` or `finEnumCompDirection` appears**: move them to `Geb/Mathlib/Data/FinEnum.lean`, the repository's home for choice-free diff --git a/docs/index.md b/docs/index.md index e0bcda0..bae3246 100644 --- a/docs/index.md +++ b/docs/index.md @@ -185,9 +185,9 @@ import-direction rules above are enforced by `ℕ × ℕ`, its syntax as that functor's slice W-type, and its semantics by the W-type's eliminator. Depends on `Geb.Mathlib.Data.PFunctor.Slice.W` and - `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`. Every declaration of the - module has axioms within `propext` and `Quot.sound`; `sig` and - `finEnumFin` have none. + `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`. `evalRec` depends on + `propext`; `finEnumCompDirection`, `sigFinitary`, `evalValue`, + `evalStep` and `BC.eval` on `propext` and `Quot.sound`. - `Geb/Mathlib/Data/PFunctor/Presheaf/Decidable.lean` — decidability of the presheaf functor's naturality predicates. `PresheafDomPFunctorData.decidableIsNatural` decides `IsNatural` From 4e6b3bda231a9d9030ea840ad47f9b1b04740de4 Mon Sep 17 00:00:00 2001 From: "Terence M. Rokop" Date: Tue, 4 Aug 2026 14:25:25 -0700 Subject: [PATCH 9/9] doc: remove the Bellantoni-Cook spec and plan --- .../plans/2026-08-04-bellantoni-cook.md | 1240 ----------------- .../2026-08-04-bellantoni-cook-design.md | 1023 -------------- 2 files changed, 2263 deletions(-) delete mode 100644 docs/superpowers/plans/2026-08-04-bellantoni-cook.md delete mode 100644 docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md diff --git a/docs/superpowers/plans/2026-08-04-bellantoni-cook.md b/docs/superpowers/plans/2026-08-04-bellantoni-cook.md deleted file mode 100644 index fc3ef1f..0000000 --- a/docs/superpowers/plans/2026-08-04-bellantoni-cook.md +++ /dev/null @@ -1,1240 +0,0 @@ -# Bellantoni-Cook syntax and semantics — implementation plan - -> **For agentic workers:** REQUIRED SUB-SKILL: Use -> superpowers:subagent-driven-development (recommended) or -> superpowers:executing-plans to implement this plan task-by-task. -> Steps use checkbox (`- [ ]`) syntax for tracking. - -**Goal:** Define the function class `B` of [HeraudNowak2011] § 3.2 in Lean — -its syntax as the slice W-type of a signature functor over `ℕ × ℕ`, and its -interpretation by that type's eliminator. - -**Architecture:** A non-recursive `Shape` type carries the seven constructor -forms with their arity parameters; `q : Shape → ℕ × ℕ` and -`rc : (a : Shape) → Direction a → ℕ × ℕ` encode the paper's arity relation as -data (conclusions and hypotheses respectively); `sig` bundles them as a -`SlicePFunctor (ℕ × ℕ) (ℕ × ℕ)`; `BC := sig.W` admits exactly the -well-formed terms; and `BC.eval` is one application of -`SlicePFunctor.W.elim` into the dependent target `Σ i, Sem i`. - -**Tech Stack:** Lean 4 (toolchain v4.33.0-rc2), mathlib, -`Geb.Mathlib.Data.PFunctor.Slice.*`, `jj` for version control. - - - - -- [Global Constraints](#global-constraints) -- [Commit sequence](#commit-sequence) -- [File structure](#file-structure) -- [Task 1: Branch, spec commit, plan commit](#task-1-branch-spec-commit-plan-commit) -- [Task 2: The signature functor](#task-2-the-signature-functor) -- [Task 3: Finiteness and decidable admissibility](#task-3-finiteness-and-decidable-admissibility) -- [Task 4: The syntax and the semantics](#task-4-the-syntax-and-the-semantics) -- [Task 5: The test module](#task-5-the-test-module) -- [Task 6: Documentation](#task-6-documentation) -- [Task 7: The pre-push gate](#task-7-the-pre-push-gate) -- [Task 8: Remove the spec and the plan](#task-8-remove-the-spec-and-the-plan) - - - -## Global Constraints - -Every task's requirements implicitly include these. They are the spec's -§ Constraints, verbatim in substance. - -1. No `noncomputable`. `#print axioms` on every declaration lies within - `{propext, Quot.sound}`. `Quot.sound` is permitted, not excluded. -2. No self-referential `inductive` and no self-calling `def`. `Shape` is - non-recursive; the syntax's recursion is `sig.W`; the semantics' - recursions are `SlicePFunctor.W.elim` and `List.rec`. -3. All four new `.lean` files declare `module`. The library module uses - `public import` and a `public section`; the test module uses plain - `import` with `set_option linter.privateModule false`. -4. `scripts/pre-push.sh` clean, `lake shake`, `lake lint` and - `scripts/lint-imports.sh` included. -5. No `#guard`; every assertion is a `theorem` closing by `rfl`. `plusOf` and - `multOf` are `def`s, `BCOf n s` being a type rather than a `Prop`. -6. Lambda notation uses `↦`, not `=>`, in `fun`. -7. Library imports: `Geb.Mathlib.Data.PFunctor.Slice.W`, - `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`, - `Mathlib.Logic.Equiv.Fin.Basic`. The test module adds - `Geb.Mathlib.Data.PFunctor.Slice.Decidable` and the library module. - Neither module names `Mathlib.Data.Fin.Tuple.Basic` or - `Mathlib.Data.Fin.VecNotation`, though both apply `Fin.append`, - `Fin.cons`, `Fin.tail` and `![…]`: `Mathlib.Logic.Equiv.Fin.Basic` - supplies both transitively, and naming either makes plain `lake shake` - report the module carrying it. -8. Copyright headers take the form used throughout the tree: - - ```lean - /- - Copyright (c) 2026 Terence Rokop. All rights reserved. - Released under Apache 2.0 license as described in the file LICENSE. - Authors: Terence Rokop - -/ - ``` - -9. Commit messages follow the repository's Conventional-Commits-shaped - convention (`feat` / `fix` / `doc` / `style` / `refactor` / `test` / - `chore` / `perf` / `ci`), imperative present tense, no capital, no period. -10. **Version control is `jj`, not `git`.** A PreToolUse hook blocks - mutating `git` subcommands. Commit with `jj commit -m "…"`, which - commits the whole working copy and starts a fresh change. - -## Commit sequence - -The spec's § Placement fixes the phase order: spec, plan, library module, -test module, documentation, then a final commit removing the spec and the -plan. This plan spans the library phase over three commits (Tasks 2-4), -which refines that order without reordering it. - -## File structure - -| Path | Responsibility | -| --- | --- | -| `Geb/Mathlib/Computability.lean` | directory index; imports the content module | -| `Geb/Mathlib/Computability/BellantoniCook.lean` | the whole library: signature, finiteness, syntax, semantics | -| `GebTests/Mathlib/Computability.lean` | test directory index | -| `GebTests/Mathlib/Computability/BellantoniCook.lean` | the worked terms and the thirteen assertions | -| `Geb/Mathlib.lean` | gains one `public import` | -| `GebTests/Mathlib.lean` | gains one `import` | -| `docs/references.bib` | two entries | -| `docs/references.md` | one pointer | -| `docs/index.md` | one bullet | -| `TODO.md` | one `### Bellantoni-Cook` subsection, four trigger entries | - -One content module, not a `Defs`/`Basic` split: this workstream states no -lemmas, so there is nothing to separate. - ---- - -## Task 1: Branch, spec commit, plan commit - -**Files:** - -- Modify: none (version-control only) - -**Interfaces:** - -- Consumes: nothing -- Produces: a topic branch `feat/bellantoni-cook` whose first two commits - carry the spec and this plan - -- [ ] **Step 1: Create the topic branch on the current change** - -```bash -jj bookmark create feat/bellantoni-cook -r @ -``` - -- [ ] **Step 2: Confirm the working copy holds the spec and the plan** - -Run: `jj status` -Expected: two `A` lines, the spec and this plan, in one change. - -- [ ] **Step 3: Commit the spec alone** - -`jj commit` with paths keeps the named paths in the current commit and moves -everything else to a new working-copy commit on top, which is how the spec -and the plan become two commits in the order § Placement fixes. - -```bash -jj commit docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md \ - -m "doc: add the Bellantoni-Cook design spec" -``` - -- [ ] **Step 4: Confirm the plan is now the only working-copy change** - -Run: `jj status` -Expected: exactly one line, `A docs/superpowers/plans/2026-08-04-bellantoni-cook.md` - -- [ ] **Step 5: Commit the plan** - -```bash -jj commit -m "doc: add the Bellantoni-Cook implementation plan" -``` - -- [ ] **Step 6: Advance the bookmark to the new head** - -```bash -jj bookmark set feat/bellantoni-cook -r @- -``` - -Run: `jj log -r 'feat/bellantoni-cook'` -Expected: the bookmark points at the plan commit. - ---- - -## Task 2: The signature functor - -**Files:** - -- Create: `Geb/Mathlib/Computability.lean` -- Create: `Geb/Mathlib/Computability/BellantoniCook.lean` -- Modify: `Geb/Mathlib.lean` - -**Interfaces:** - -- Consumes: `SlicePFunctor` from `Geb.Mathlib.Data.PFunctor.Slice.W` -- Produces: - - `BellantoniCook.Shape : Type` — seven constructors, listed below - - `BellantoniCook.Direction : Shape → Type` - - `BellantoniCook.rc : (a : Shape) → Direction a → ℕ × ℕ` - - `BellantoniCook.q : Shape → ℕ × ℕ` - - `BellantoniCook.sig : SlicePFunctor (ℕ × ℕ) (ℕ × ℕ)` - -- [ ] **Step 1: Create the directory index** - -Create `Geb/Mathlib/Computability.lean`: - -```lean -/- -Copyright (c) 2026 Terence Rokop. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Terence Rokop --/ -module - -public import Geb.Mathlib.Computability.BellantoniCook - -/-! -# Computability — index --/ -``` - -The title must not name `Geb.Mathlib.`: `scripts/lint-imports.sh` rejects the -self-prefix outside an `^import` line, and a docstring title carrying it fails. - -- [ ] **Step 2: Create the content module with its header, imports and signature** - -Create `Geb/Mathlib/Computability/BellantoniCook.lean`: - -```lean -/- -Copyright (c) 2026 Terence Rokop. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Terence Rokop --/ -module - -public import Geb.Mathlib.Data.PFunctor.Slice.W -public import Geb.Mathlib.Data.PFunctor.Univariate.Finitary -public import Mathlib.Logic.Equiv.Fin.Basic - -/-! -# The function class `B` of Bellantoni and Cook - -The syntax of the function class `B` and its interpretation, following -[HeraudNowak2011] § 3.2. Terms of `B` are built from a constant zero, -projections, two successors, a predecessor and a conditional, and are closed -under a composition and a recursion that distinguish normal from safe -argument positions; the distinction is what bounds the growth rate of the -definable functions. - -The class defined here is the reformulation of § 3.2, not the class of -[BellantoniCook1992]. Two differences: the conditional takes four safe -arguments and branches three ways, on the empty, odd and even bitstrings, -where the original branches two ways on parity and treats the empty -bitstring as even; and the base case of the recursion is the empty -bitstring, where the original's is every bitstring denoting zero. - -The two sources transpose the conditional's last two safe arguments. The -order here follows the authors' Coq development, that being the artifact -against which the paper's theorems were machine-checked. - -## Main definitions - -* `BellantoniCook.Shape` — the seven constructor forms, with their arities - as parameters. -* `BellantoniCook.Direction` — the subterm positions of a shape. -* `BellantoniCook.rc` — the arity each subterm position must carry. -* `BellantoniCook.q` — the arity a shape produces. -* `BellantoniCook.sig` — the signature, as a slice polynomial functor over - `ℕ × ℕ`. -* `BellantoniCook.BC` — an expression of `B`: a `sig`-tree whose every node - respects `rc`. -* `BellantoniCook.BC.arity` — its pair of normal and safe arities. -* `BellantoniCook.BCOf` — the expressions of a given arity pair. -* `BellantoniCook.Sem` — the meaning of an arity pair: a function of a - normal and a safe environment. -* `BellantoniCook.transport` — transport of a meaning along an equality of - arity pairs. -* `BellantoniCook.evalRec` — the recursion on the consumed bitstring. -* `BellantoniCook.evalValue` — the meaning of one node from its children's. -* `BellantoniCook.evalStep` — `evalValue` as a slice algebra. -* `BellantoniCook.BC.eval` — the interpretation, by the slice W-type's - eliminator. - -## Implementation notes - -This repository expresses all recursion through recursors, admitting -neither a self-referential `inductive` nor a self-calling `def`, so the -arity-indexed syntax is the slice W-type of `sig` and the interpretation is -one application of `SlicePFunctor.W.elim`. `Shape` is itself non-recursive -and so is the shape set of a `PFunctor`, not a datatype the rule reaches. - -`evalValue` is separate from `evalStep` because the match on `Shape` must -generalize the compatibility hypothesis, which arrives bundled in -`SliceDomPFunctor.Obj`. A child's meaning carries the index it was built at -rather than the index `rc` prescribes, equal but not definitionally so; -`transport` carries it across, with the motive of `▸` fixed once instead of -at each of the six sites. - -`Direction`, `rc` and `q` are `@[reducible]`. Instance search does not -delta-reduce a semireducible definition, and every numeral in `evalValue` -elaborates against `Fin (q a).1` or `Direction a`. - -`finEnumFin` and `finEnumCompDirection` are `scoped`, and hand-built: -mathlib's `FinEnum` instances depend on `Classical.choice`, which -`lake lint` rejects, and an unscoped instance at the head symbol `FinEnum -(Fin _)` would compete with `FinEnum.fin` wherever `Geb` is imported. - -## References - -* [HeraudNowak2011] -* [BellantoniCook1992] - -## Tags - -Bellantoni-Cook, polytime, implicit computational complexity, safe -recursion, W-type, polynomial functor --/ - -namespace BellantoniCook - -public section - -/-- The seven constructor forms of `B`, each carrying its arities as -parameters: `zero` the constant empty bitstring; `proj n s i` the `i`th of -`n` normal and `s` safe variables; `succ b` the successor appending the bit -`b`; `pred` the predecessor; `cond` the four-argument conditional; -`safeRec n s` the recursion producing arity `(n + 1, s)`; and `comp n s m k` -the composition of an expression of arity `(m, k)` with `m` normal and `k` -safe argument expressions of arity `(n, 0)` and `(n, s)`. -/ -inductive Shape - | zero - | proj (n s : ℕ) (i : Fin (n + s)) - | succ (b : Bool) - | pred - | cond - | safeRec (n s : ℕ) - | comp (n s m k : ℕ) - -/-- The subterm positions of a shape. The five base forms have none; -`safeRec` has three, its base and its two step expressions; `comp` has its -head, its `m` normal arguments and its `k` safe arguments. -/ -@[expose, reducible] def Direction : Shape → Type - | .zero => Fin 0 - | .proj _ _ _ => Fin 0 - | .succ _ => Fin 0 - | .pred => Fin 0 - | .cond => Fin 0 - | .safeRec _ _ => Fin 3 - | .comp _ _ m k => Unit ⊕ Fin m ⊕ Fin k - -/-- The arity each subterm position must carry: the hypotheses of the -arity relation of [HeraudNowak2011] § 3.2. -/ -@[expose, reducible] def rc : (a : Shape) → Direction a → ℕ × ℕ - | .zero, i => i.elim0 - | .proj _ _ _, i => i.elim0 - | .succ _, i => i.elim0 - | .pred, i => i.elim0 - | .cond, i => i.elim0 - | .safeRec n s, ⟨0, _⟩ => (n, s) - | .safeRec n s, _ => (n + 1, s + 1) - | .comp _ _ m k, .inl () => (m, k) - | .comp n _ _ _, .inr (.inl _) => (n, 0) - | .comp n s _ _, .inr (.inr _) => (n, s) - -/-- The arity a shape produces: the conclusions of the arity relation of -[HeraudNowak2011] § 3.2. -/ -@[expose, reducible] def q : Shape → ℕ × ℕ - | .zero => (0, 0) - | .proj n s _ => (n, s) - | .succ _ => (0, 1) - | .pred => (0, 1) - | .cond => (0, 4) - | .safeRec n s => (n + 1, s) - | .comp n s _ _ => (n, s) - -/-- The signature of `B` as a slice polynomial functor over `ℕ × ℕ`, the -index being the pair of normal and safe arities. -/ -@[expose] def sig : SlicePFunctor (ℕ × ℕ) (ℕ × ℕ) where - A := Shape - B := Direction - r := fun x ↦ rc x.1 x.2 - q := q - -end - -end BellantoniCook -``` - -- [ ] **Step 3: Add the import to the subtree index** - -Modify `Geb/Mathlib.lean`: add `public import Geb.Mathlib.Computability` to -the import block, keeping the block alphabetically ordered as the file has it. - -- [ ] **Step 4: Build and verify zero diagnostics** - -Run: `lake build Geb.Mathlib.Computability Geb.Mathlib` -Expected: builds with no output beyond the progress lines. Any warning is a -failure — the package sets `weak.warningAsError = true`. Naming the index -modules rather than the content module alone is what exercises Step 1's and -Step 3's edits; a typo in either would otherwise surface only at Task 7. - -- [ ] **Step 5: Verify the arity relation transcribes correctly** - -Run this scratch check (do not commit it); it asserts every row of the -spec's signature table: - -```bash -cat > /tmp/bc-sig-check.lean <<'EOF' -import Geb.Mathlib.Computability.BellantoniCook -open BellantoniCook -example : q .zero = (0, 0) := rfl -example : q (.proj 2 3 0) = (2, 3) := rfl -example : q (.succ true) = (0, 1) := rfl -example : q .pred = (0, 1) := rfl -example : q .cond = (0, 4) := rfl -example : q (.safeRec 1 2) = (2, 2) := rfl -example : q (.comp 1 2 3 4) = (1, 2) := rfl -example : rc (.safeRec 1 2) 0 = (1, 2) := rfl -example : rc (.safeRec 1 2) 1 = (2, 3) := rfl -example : rc (.safeRec 1 2) 2 = (2, 3) := rfl -example : rc (.comp 1 2 3 4) (.inl ()) = (3, 4) := rfl -example : rc (.comp 1 2 3 4) (.inr (.inl 0)) = (1, 0) := rfl -example : rc (.comp 1 2 3 4) (.inr (.inr 0)) = (1, 2) := rfl -EOF -lake env lean /tmp/bc-sig-check.lean; rm -f /tmp/bc-sig-check.lean -``` - -Expected: no output, exit 0. A non-empty output means a row of `q` or `rc` -disagrees with the spec's table; fix the definition, not the check. - -- [ ] **Step 6: Commit** - -```bash -jj commit -m "feat(computability): add the Bellantoni-Cook signature functor" -``` - ---- - -## Task 3: Finiteness and decidable admissibility - -**Files:** - -- Modify: `Geb/Mathlib/Computability/BellantoniCook.lean` - -**Interfaces:** - -- Consumes: `sig`, `Direction`, `Shape` from Task 2; - `PFunctor.Finitary` from `Geb.Mathlib.Data.PFunctor.Univariate.Finitary` -- Produces: - - `BellantoniCook.finEnumFin (n : ℕ) : FinEnum (Fin n)` — `scoped` - - `BellantoniCook.finEnumCompDirection (m k : ℕ) : - FinEnum (Unit ⊕ Fin m ⊕ Fin k)` — `scoped` - - `BellantoniCook.sigFinitary : sig.toPFunctor.Finitary` - -- [ ] **Step 1: Add the three instances** - -Insert into `Geb/Mathlib/Computability/BellantoniCook.lean`, after `sig` and -inside the `public section`: - -```lean -/-- A choice-free `FinEnum (Fin n)`: the cardinality is `n` and the -enumeration is the identity. `scoped`, so that it does not compete with -mathlib's `FinEnum.fin` at the same head symbol outside this namespace. -/ -scoped instance finEnumFin (n : ℕ) : - FinEnum (Fin n) where - card := n - equiv := Equiv.refl _ - decEq := inferInstance - -/-- A choice-free `FinEnum` for `comp`'s directions. `scoped`, for the same -reason as `finEnumFin`. -/ -scoped instance finEnumCompDirection (m k : ℕ) : - FinEnum (Unit ⊕ Fin m ⊕ Fin k) where - card := 1 + (m + k) - equiv := (Equiv.sumCongr finOneEquiv.symm finSumFinEquiv).trans finSumFinEquiv - decEq := inferInstance - -/-- Every shape has finitely many directions, which is what makes -admissibility of a `sig`-tree decidable. The branches ascribe their -instances explicitly: instance search stops at reducible transparency on the -projection `sig.B a`, so a bare `inferInstance` does not find them. -/ -instance sigFinitary : sig.toPFunctor.Finitary - | .zero => inferInstanceAs (FinEnum (Fin 0)) - | .proj _ _ _ => inferInstanceAs (FinEnum (Fin 0)) - | .succ _ => inferInstanceAs (FinEnum (Fin 0)) - | .pred => inferInstanceAs (FinEnum (Fin 0)) - | .cond => inferInstanceAs (FinEnum (Fin 0)) - | .safeRec _ _ => inferInstanceAs (FinEnum (Fin 3)) - | .comp _ _ m k => inferInstanceAs (FinEnum (Unit ⊕ Fin m ⊕ Fin k)) -``` - -`sigFinitary` is an `instance`, not a `def`: as a `def` it does not fire for -`decidableWValid`, and it draws `Definition … of class type is -semireducible`, fatal under `weak.warningAsError`. It needs no attribute. - -- [ ] **Step 2: Build** - -Run: `lake build Geb.Mathlib.Computability.BellantoniCook` -Expected: builds, no output beyond progress lines. - -- [ ] **Step 3: Verify the instances are choice-free** - -Run: - -```bash -cat > /tmp/bc-axiom-check.lean <<'EOF' -import Geb.Mathlib.Computability.BellantoniCook -#print axioms BellantoniCook.finEnumFin -#print axioms BellantoniCook.finEnumCompDirection -#print axioms BellantoniCook.sigFinitary -EOF -lake env lean /tmp/bc-axiom-check.lean; rm -f /tmp/bc-axiom-check.lean -``` - -Expected: `'BellantoniCook.finEnumFin' does not depend on any axioms`, and -`[propext, Quot.sound]` for the other two. **`Classical.choice` anywhere is a -failure** — it means a branch resolved through a mathlib instance instead of -the two above. - -- [ ] **Step 4: Commit** - -```bash -jj commit -m "feat(computability): add choice-free finiteness for the signature" -``` - ---- - -## Task 4: The syntax and the semantics - -**Files:** - -- Modify: `Geb/Mathlib/Computability/BellantoniCook.lean` - -**Interfaces:** - -- Consumes: `sig`, `Shape`, `Direction`, `rc`, `q` from Task 2; - `sigFinitary` from Task 3; `SlicePFunctor.W`, `.wIndex`, `W.elim` from - `Geb.Mathlib.Data.PFunctor.Slice.W` -- Produces: - - `BellantoniCook.BC : Type` - - `BellantoniCook.BC.arity : BC → ℕ × ℕ` - - `BellantoniCook.BCOf (n s : ℕ) : Type` - - `BellantoniCook.Sem : ℕ × ℕ → Type` - - `BellantoniCook.transport {i j : ℕ × ℕ} (h : i = j) (v : Sem i) : Sem j` - - `BellantoniCook.evalRec {n s : ℕ} (g : Sem (n, s)) - (h₀ h₁ : Sem (n + 1, s + 1)) : List Bool → Sem (n, s)` - - `BellantoniCook.evalValue : (a : Shape) → - (c : Direction a → Σ i, Sem i) → (∀ b, (c b).1 = rc a b) → Sem (q a)` - - `BellantoniCook.evalStep : - sig.toSliceDomPFunctor.Obj (Sigma.fst (β := Sem)) → Σ i, Sem i` - - `BellantoniCook.BC.eval : BC → Σ i, Sem i` - -- [ ] **Step 1: Add the syntax** - -Insert after `sigFinitary`, inside the `public section`: - -```lean -/-- An expression of `B`: a `sig`-tree every node of which carries children -at the indices `rc` prescribes. -/ -@[expose] def BC : Type := sig.W - -/-- The arity pair of an expression: its normal and safe arities. -/ -@[expose] def BC.arity : BC → ℕ × ℕ := sig.wIndex - -/-- The expressions of arity `(n, s)`, which is the arity relation of -[HeraudNowak2011] § 3.2 as a type rather than a side condition. -/ -@[expose] def BCOf (n s : ℕ) : Type := { e : BC // e.arity = (n, s) } -``` - -- [ ] **Step 2: Add the semantic family and the transport** - -```lean -/-- The meaning of an arity pair: a function of a normal and a safe -environment, each a tuple of bitstrings, returning a bitstring. -/ -@[expose] def Sem : ℕ × ℕ → Type := - fun i ↦ (Fin i.1 → List Bool) → (Fin i.2 → List Bool) → List Bool - -/-- Transport of a meaning along an equality of arity pairs. Named so that -the motive of `▸` is fixed once rather than inferred at each use in -`evalValue`. -/ -@[expose] def transport {i j : ℕ × ℕ} (h : i = j) (v : Sem i) : Sem j := h ▸ v -``` - -- [ ] **Step 3: Add the recursion on the consumed bitstring** - -```lean -/-- The recursion `safeRec` performs on its first normal argument, by -`List.rec`. The base case is the empty bitstring; a step consumes the low -bit `b`, passes the remaining bitstring `v` as the new first normal -argument, and passes the recursive value in safe position. -/ -@[expose] def evalRec {n s : ℕ} (g : Sem (n, s)) - (h₀ h₁ : Sem (n + 1, s + 1)) : List Bool → Sem (n, s) := - List.rec g (fun b v ih x y ↦ - (if b then h₁ else h₀) (Fin.cons v x) (Fin.cons (ih x y) y)) -``` - -- [ ] **Step 4: Add the algebra** - -```lean -/-- The meaning of one node, from its children's meanings and the proof that -each child's index is the one `rc` prescribes. A separate definition from -`evalStep` because the match on `Shape` must generalize that proof. - -`cond` reads its first safe argument and returns the second, third or fourth -according as it is empty, odd or even — the ordering of the authors' Coq -development. `comp` applies its head's meaning to the normal arguments' -meanings, each in the empty safe environment, and to the safe arguments'. -/ -@[expose] def evalValue : (a : Shape) → (c : Direction a → Σ i, Sem i) → - (∀ b, (c b).1 = rc a b) → Sem (q a) - | .zero, _, _ => fun _ _ ↦ [] - | .proj _ _ i, _, _ => fun x y ↦ Fin.append x y i - | .succ b, _, _ => fun _ y ↦ b :: y 0 - | .pred, _, _ => fun _ y ↦ (y 0).tail - | .cond, _, _ => fun _ y ↦ - match y 0 with - | [] => y 1 - | true :: _ => y 2 - | false :: _ => y 3 - | .safeRec _ _, c, h => fun x y ↦ - evalRec (transport (h 0) (c 0).2) (transport (h 1) (c 1).2) - (transport (h 2) (c 2).2) (x 0) (Fin.tail x) y - | .comp _ _ _ _, c, h => fun x y ↦ - transport (h (.inl ())) (c (.inl ())).2 - (fun i ↦ transport (h (.inr (.inl i))) (c (.inr (.inl i))).2 x Fin.elim0) - (fun j ↦ transport (h (.inr (.inr j))) (c (.inr (.inr j))).2 x y) - -/-- `evalValue` as an algebra for `sig` in the slice over `ℕ × ℕ`. Returning -the shape's own output index as the first component makes the eliminator's -coherence obligation hold by `rfl`. -/ -@[expose] def evalStep : - sig.toSliceDomPFunctor.Obj (Sigma.fst (β := Sem)) → Σ i, Sem i := - fun z ↦ ⟨sig.q z.1.1, - evalValue z.1.1 z.1.2 - ((sig.toSliceDomPFunctor.compatible_iff _ z.1.1 z.1.2).mp z.2)⟩ - -/-- The interpretation of an expression: its arity pair together with its -meaning at that pair, by the slice W-type's eliminator. -/ -@[expose] def BC.eval : BC → Σ i, Sem i := - SlicePFunctor.W.elim sig (Σ i, Sem i) (Sigma.fst (β := Sem)) evalStep rfl -``` - -Note `SlicePFunctor.W.elim sig …`, not `sig.W.elim …`: `sig.W` is a type, -not a term, so field notation does not chain through it. - -- [ ] **Step 5: Build** - -Run: `lake build Geb.Mathlib.Computability.BellantoniCook` -Expected: builds, no output beyond progress lines. In particular no -`failed to synthesize instance of type class OfNat …`, which would mean -`Direction`, `rc` or `q` lost its `@[reducible]`. - -- [ ] **Step 6: Verify the axioms and run the linters** - -Run: - -```bash -cat > /tmp/bc-eval-axioms.lean <<'EOF' -import Geb.Mathlib.Computability.BellantoniCook -#print axioms BellantoniCook.BC.eval -#print axioms BellantoniCook.evalValue -#print axioms BellantoniCook.evalRec -EOF -lake env lean /tmp/bc-eval-axioms.lean; rm -f /tmp/bc-eval-axioms.lean -lake lint -scripts/lint-imports.sh -``` - -Expected: each line within `{propext, Quot.sound}` — some declarations -depend on fewer, which is not a failure. **`Classical.choice` anywhere is a -failure.** `lake lint` prints -`Running linter on specified modules: [Geb]` and -`-- Linting passed for Geb.`; `lint-imports.sh` prints -`lint-imports.sh: clean (N file(s) checked)`. - -- [ ] **Step 7: Commit** - -```bash -jj commit -m "feat(computability): add the Bellantoni-Cook syntax and semantics" -``` - ---- - -## Task 5: The test module - -**Files:** - -- Create: `GebTests/Mathlib/Computability.lean` -- Create: `GebTests/Mathlib/Computability/BellantoniCook.lean` -- Modify: `GebTests/Mathlib.lean` - -**Interfaces:** - -- Consumes: everything Task 4 produces, plus - `SlicePFunctor.decidableWValid` from - `Geb.Mathlib.Data.PFunctor.Slice.Decidable` -- Produces: nothing later tasks depend on - -- [ ] **Step 1: Create the test directory index** - -Create `GebTests/Mathlib/Computability.lean`: - -```lean -/- -Copyright (c) 2026 Terence Rokop. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Terence Rokop --/ -module - -import GebTests.Mathlib.Computability.BellantoniCook - -/-! -# Computability tests — index --/ -``` - -- [ ] **Step 2: Write the test module — header, terms, and the first two assertions** - -Create `GebTests/Mathlib/Computability/BellantoniCook.lean`: - -```lean -/- -Copyright (c) 2026 Terence Rokop. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Terence Rokop --/ -module - -import Geb.Mathlib.Computability.BellantoniCook -import Geb.Mathlib.Data.PFunctor.Slice.Decidable - -/-! -# Worked expressions of the Bellantoni-Cook class - -The `plus` and `mult` of [HeraudNowak2011] § 3.2, a recursion whose two step -expressions differ, four single-node expressions, and one inadmissible raw -tree. Each expression is built in two steps — a raw tree bound as its own -definition, then the admissible expression — because an inline `WType.mk` -application blocks the instance search that `decide` needs. - -`plus` and `mult` are transcribed with the arities of the authors' Coq -development. The composition superscripts printed in § 3.2's `mult` are -`plus`'s and do not satisfy the paper's own arity relation. - -## Main statements - -The thirteen assertions below: twelve expected outputs of `BC.eval`, and one -inadmissible tree. - -## References - -* [HeraudNowak2011] - -## Tags - -Bellantoni-Cook, polytime, safe recursion --/ - -set_option linter.privateModule false - -open BellantoniCook - -/-- The children of a `comp` node, in the order `Direction` gives them: the -head, then the normal arguments, then the safe arguments. -/ -def compChildren {m k : ℕ} (h : sig.toPFunctor.W) - (gN : Fin m → sig.toPFunctor.W) (gS : Fin k → sig.toPFunctor.W) : - Unit ⊕ Fin m ⊕ Fin k → sig.toPFunctor.W := - Sum.elim (fun _ ↦ h) (Sum.elim gN gS) - -/-- The step expression of `plus`: the successor appending `true`, applied -to the recursive value. -/ -def plusStepRaw : sig.toPFunctor.W := - WType.mk (.comp 1 2 0 1) - (compChildren (WType.mk (.succ true) Fin.elim0) Fin.elim0 - ![WType.mk (.proj 1 2 1) Fin.elim0]) - -/-- The step expression of `plus`, admissible. -/ -def plusStep : BC := ⟨plusStepRaw, by decide⟩ - -/-- `plus`, of arity `(1, 1)`: it prepends one `true` per bit of its normal -argument to its safe argument. -/ -def plusRaw : sig.toPFunctor.W := - WType.mk (.safeRec 0 1) - ![WType.mk (.proj 0 1 0) Fin.elim0, plusStep.val, plusStep.val] - -/-- `plus`, admissible. -/ -def plus : BC := ⟨plusRaw, by decide⟩ - -/-- The base expression of `mult`: the constant empty bitstring at -arity `(1, 0)`. -/ -def multBaseRaw : sig.toPFunctor.W := - WType.mk (.comp 1 0 0 0) - (compChildren (WType.mk .zero Fin.elim0) Fin.elim0 Fin.elim0) - -/-- The base expression of `mult`, admissible. -/ -def multBase : BC := ⟨multBaseRaw, by decide⟩ - -/-- The step expression of `mult`: `plus` of the second normal argument and -the recursive value. -/ -def multStepRaw : sig.toPFunctor.W := - WType.mk (.comp 2 1 1 1) - (compChildren plus.val ![WType.mk (.proj 2 0 1) Fin.elim0] - ![WType.mk (.proj 2 1 2) Fin.elim0]) - -/-- The step expression of `mult`, admissible. -/ -def multStep : BC := ⟨multStepRaw, by decide⟩ - -/-- `mult`, of arity `(2, 0)`: it produces one `true` per pair of bits of -its two normal arguments. -/ -def multRaw : sig.toPFunctor.W := - WType.mk (.safeRec 1 0) ![multBase.val, multStep.val, multStep.val] - -/-- `mult`, admissible. -/ -def mult : BC := ⟨multRaw, by decide⟩ - -/-- `plus` at its declared arity. Elaborating this is exactly the assertion -that `BC.arity plus` is `(1, 1)`. -/ -def plusOf : BCOf 1 1 := ⟨plus, rfl⟩ - -/-- `mult` at its declared arity. -/ -def multOf : BCOf 2 0 := ⟨mult, rfl⟩ - -/-- `plus` on an empty normal argument returns its safe argument. -/ -theorem eval_plus_nil : (BC.eval plus).2 ![[]] ![[false]] = [false] := rfl - -/-- `plus` prepends one `true` per bit of its normal argument. -/ -theorem eval_plus_cons : - (BC.eval plus).2 ![[true, true]] ![[false]] = [true, true, false] := rfl -``` - -- [ ] **Step 3: Build and check the first two assertions before writing the rest** - -Run: `lake build GebTests.Mathlib.Computability.BellantoniCook` -Expected: builds. A `Not a definitional equality` here means a term or a -semantic clause is wrong; fix it before continuing, since every later -assertion rests on the same clauses. - -- [ ] **Step 4: Add the remaining terms and assertions** - -Append to `GebTests/Mathlib/Computability/BellantoniCook.lean`: - -```lean -/-- `mult` produces one `true` per pair of bits of its two normal -arguments. -/ -theorem eval_mult : - (BC.eval mult).2 ![[true, true], [true, true, true]] ![] = - List.replicate 6 true := rfl - -/-- A recursion whose two step expressions differ: the `false` branch -returns the remaining bitstring, the `true` branch recurses. Without it no -assertion here would distinguish the two step expressions, `plus` and `mult` -passing the same expression as both. -/ -def branchRecRaw : sig.toPFunctor.W := - WType.mk (.safeRec 0 0) - ![WType.mk .zero Fin.elim0, WType.mk (.proj 1 1 0) Fin.elim0, - WType.mk (.proj 1 1 1) Fin.elim0] - -/-- The discriminating recursion, admissible. -/ -def branchRec : BC := ⟨branchRecRaw, by decide⟩ - -/-- On a `false`-headed argument the `false` branch returns the remaining -bitstring. Arguments of length one do not discriminate the branches: both -readings return the empty bitstring. -/ -theorem eval_branchRec_false : - (BC.eval branchRec).2 ![[false, true]] ![] = [true] := rfl - -/-- On a `true`-headed argument the `true` branch recurses. -/ -theorem eval_branchRec_true : - (BC.eval branchRec).2 ![[true, true]] ![] = [] := rfl - -/-- The predecessor as a single node. -/ -def predTermRaw : sig.toPFunctor.W := WType.mk .pred Fin.elim0 - -/-- The predecessor, admissible. -/ -def predTerm : BC := ⟨predTermRaw, by decide⟩ - -/-- The predecessor of the empty bitstring is the empty bitstring. -/ -theorem eval_predTerm_nil : (BC.eval predTerm).2 ![] ![[]] = [] := rfl - -/-- The predecessor drops the low bit. -/ -theorem eval_predTerm_cons : - (BC.eval predTerm).2 ![] ![[true, false]] = [false] := rfl - -/-- The conditional as a single node. -/ -def condTermRaw : sig.toPFunctor.W := WType.mk .cond Fin.elim0 - -/-- The conditional, admissible. -/ -def condTerm : BC := ⟨condTermRaw, by decide⟩ - -/-- On the empty bitstring the conditional returns its second safe -argument. -/ -theorem eval_condTerm_empty : - (BC.eval condTerm).2 ![] ![[], [false], [true], [true, true]] = [false] := - rfl - -/-- On an odd bitstring it returns its third. The authors' Coq development -assigns the third to the odd case and the fourth to the even case; § 3.2 -prints them the other way round. -/ -theorem eval_condTerm_odd : - (BC.eval condTerm).2 ![] ![[true], [false], [true], [true, true]] = - [true] := rfl - -/-- On an even bitstring it returns its fourth. -/ -theorem eval_condTerm_even : - (BC.eval condTerm).2 ![] ![[false], [false], [true], [true, true]] = - [true, true] := rfl - -/-- A projection onto a normal variable, as a single node. -/ -def projNTermRaw : sig.toPFunctor.W := WType.mk (.proj 1 1 0) Fin.elim0 - -/-- The normal projection, admissible. -/ -def projNTerm : BC := ⟨projNTermRaw, by decide⟩ - -/-- The normal projection returns the normal argument. -/ -theorem eval_projNTerm : - (BC.eval projNTerm).2 ![[true]] ![[false]] = [true] := rfl - -/-- A projection onto a safe variable, as a single node. Together with -`projNTerm` this separates the two halves of `Fin.append`, which a -mistranscribed index would silently permute. -/ -def projSTermRaw : sig.toPFunctor.W := WType.mk (.proj 1 1 1) Fin.elim0 - -/-- The safe projection, admissible. -/ -def projSTerm : BC := ⟨projSTermRaw, by decide⟩ - -/-- The safe projection returns the safe argument. -/ -theorem eval_projSTerm : - (BC.eval projSTerm).2 ![[true]] ![[false]] = [false] := rfl - -/-- `plusStepRaw` with its safe argument replaced by an expression of arity -`(2, 0)` where the signature demands `(1, 2)`. -/ -def badRaw : sig.toPFunctor.W := - WType.mk (.comp 1 2 0 1) - (compChildren (WType.mk (.succ true) Fin.elim0) Fin.elim0 - ![WType.mk (.proj 2 0 1) Fin.elim0]) - -/-- The inadmissible tree is rejected, so admissibility is not vacuous. -/ -theorem wValid_badRaw_eq_false : decide (sig.WValid badRaw) = false := rfl -``` - -- [ ] **Step 5: Add the import to the test subtree index** - -Modify `GebTests/Mathlib.lean`: add `import GebTests.Mathlib.Computability`, -in that file's existing plain-`import` form, keeping the block ordered. - -- [ ] **Step 6: Build the tests** - -Run: `lake build GebTests GebTests.Mathlib.Computability` -Expected: builds with no output beyond progress lines. The second target -exercises Steps 1 and 5, which the first does not reach: `GebTests` imports -the content module directly, not through the index. - -- [ ] **Step 7: Verify the assertions discriminate** - -The assertions must fail when the semantics is wrong. Check the three -clauses least covered elsewhere, restoring the file after each: - -```bash -# 1. Transpose the two step expressions in evalValue's safeRec clause: -# swap `(transport (h 1) (c 1).2)` and `(transport (h 2) (c 2).2)`. -lake build GebTests -# Expected: exactly eval_branchRec_false and eval_branchRec_true fail. -jj restore Geb/Mathlib/Computability/BellantoniCook.lean - -# 2. Replace evalValue's `.zero` clause body with `fun _ _ ↦ [true]`. -lake build GebTests -# Expected: eval_mult and eval_branchRec_true fail — `zero` is the base -# child of branchRec as well as the head of multBase. -jj restore Geb/Mathlib/Computability/BellantoniCook.lean - -# 3. Replace evalValue's `.succ` clause entirely with -# | .succ _b, _, _ => fun _ y ↦ y 0 -# Renaming the binder to `_b` is required: dropping the bit while -# leaving `b` bound fails the library build with -# `Variable name 'b' is not explicitly referenced`, so the tests -# would never be reached. -lake build GebTests -# Expected: eval_plus_cons and eval_mult fail. -jj restore Geb/Mathlib/Computability/BellantoniCook.lean -``` - -If any perturbation leaves the build green, the corresponding clause is -untested — stop and report it rather than proceeding. - -- [ ] **Step 8: Run the test-side linters** - -Run: `lake lint -- GebTests` then `scripts/lint-imports.sh` -Expected: `lake lint -- GebTests` prints three lines — -`Running linter on specified modules: [Geb, GebTests]`, then -`-- Linting passed for Geb.` and `-- Linting passed for GebTests.`; the -extra argument appends to `lintDriverArgs`, it does not replace it. -`scripts/lint-imports.sh` prints `lint-imports.sh: clean (N file(s) -checked)`. - -- [ ] **Step 9: Commit** - -```bash -jj commit -m "test(computability): add worked Bellantoni-Cook expressions" -``` - ---- - -## Task 6: Documentation - -**Files:** - -- Modify: `docs/references.bib` -- Modify: `docs/references.md` -- Modify: `docs/index.md` -- Modify: `TODO.md` - -**Interfaces:** - -- Consumes: the declaration names from Tasks 2-4 -- Produces: nothing later tasks depend on - -- [ ] **Step 1: Add the two bibliography entries** - -Insert into `docs/references.bib` beside the implicit-complexity entries -already there (`Leivant1999`, `DalLagoMartiniZorzi2010`, -`AvanziniDalLago2018`), which is where the file groups this subject. Align -the `=` as the neighbouring entries do: - -```bibtex -@inproceedings{HeraudNowak2011, - author = {H{\'e}raud, Sylvain and Nowak, David}, - title = {A Formalization of Polytime Functions}, - booktitle = {Interactive Theorem Proving (ITP 2011)}, - series = {Lecture Notes in Computer Science}, - volume = {6898}, - pages = {119--134}, - publisher = {Springer}, - year = {2011}, - doi = {10.1007/978-3-642-22863-6_11}, - eprint = {1102.5495}, - archivePrefix = {arXiv}, - primaryClass = {cs.CC}, - note = {This repository cites the arXiv version's section and - page numbering.}, -} - -@article{BellantoniCook1992, - author = {Bellantoni, Stephen and Cook, Stephen}, - title = {A new recursion-theoretic characterization of the - polytime functions}, - journal = {Computational Complexity}, - volume = {2}, - number = {2}, - pages = {97--110}, - year = {1992}, - doi = {10.1007/BF01201998}, -} -``` - -- [ ] **Step 2: Add the reference-implementation pointer** - -Add to `docs/references.md` § Computability: - -```markdown -- [davidnowak/bellantonicook](https://github.com/davidnowak/bellantonicook) - — the Coq development accompanying [HeraudNowak2011], at commit - `1f03b9296104646ddc2b2b4b12e35a6619c17a99`. Licensed CeCILL; no code is - taken from it. -``` - -- [ ] **Step 3: Add the docs/index.md bullet** - -Add to `docs/index.md` § Implemented content, immediately after the bullet -for `Geb/Mathlib/Data/PFunctor/Slice/Decidable.lean` — the last of the -`Slice/` bullets, and the module this one is nearest in subject: - -```markdown -- `Geb/Mathlib/Computability/BellantoniCook.lean` — the function class `B` - of [HeraudNowak2011] § 3.2: its arity relation as a `SlicePFunctor` over - `ℕ × ℕ`, its syntax as that functor's slice W-type, and its semantics by - the W-type's eliminator. Depends on - `Geb.Mathlib.Data.PFunctor.Slice.W` and - `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`. Every declaration of the - module has axioms within `propext` and `Quot.sound`; `sig` and - `finEnumFin` have none. -``` - -- [ ] **Step 4: Add the TODO.md subsection** - -Add as the last `###` subsection of `## Next up`, in the form the -neighbouring subsections use: - -```markdown -### Bellantoni-Cook - -Three items, in dependency order, over -`Geb/Mathlib/Computability/BellantoniCook.lean`. - -1. `MultiPoly`, the multivariate polynomial library of the reference - development. Required by its `BC_to_Cobham.v:2`, by its - `Cobham_to_BC.v:2`, and by Proposition 2, whose statement - `polymax_bounding` (`BC.v:1128`) is over `poly_BC` (`:1075`), built from - `pcst`, `pproj`, `pplus`, `pmult`, `pcomp`, `pshift` and `pplusl`. - Returns the polynomial apparatus items 2 and 3 are stated over. -2. Proposition 2, the polymax bounding of `B`. Depends on 1. Returns the - length bound the translation of item 3 requires. -3. Cobham's class and the translations of Theorems 1 and 2. Depends on 1 - and 2. Returns the characterization of the polynomial-time functions, - and is the consumer that justifies the definitions already committed. -``` - -- [ ] **Step 5: Add the four trigger entries** - -Add as the last four bullets of `## Triggers (do when condition fires)`, in -that section's `- **Bold title**: …` form: - -```markdown -- **A workstream needs programmable building blocks for terms of `B`**: - port the derived function library of the reference development's - `BCLib.v`, which depends only on the syntax and semantics already - committed. -- **A second consumer of `BellantoniCook.finEnumFin` or - `finEnumCompDirection` appears**: move them to - `Geb/Mathlib/Data/FinEnum.lean`, the repository's home for choice-free - `FinEnum` support. They are `scoped` in - `Geb/Mathlib/Computability/BellantoniCook.lean`. -- **A consumer needs `DecidableEq` or `Repr` for `BellantoniCook.BC`**: - derive them on `Shape` and lift along `sig.W`'s subtype. -- **A workstream needs the polytime checker of [HeraudNowak2011] as a - term-level artifact**: add an untyped `Ast` and - `check : Ast → Option ((n s : ℕ) × BellantoniCook.BCOf n s)` over - `SlicePFunctor.decidableWValid`. -``` - -- [ ] **Step 6: Regenerate the tables of contents and lint** - -Run: - -```bash -doctoc --update-only . -markdownlint-cli2 '**/*.md' -``` - -Expected: `Everything is OK.` and `Summary: 0 issues in 0 files`. `TODO.md` -carries a doctoc TOC and gains a heading, so it will change; commit that -change with the rest. - -- [ ] **Step 7: Commit** - -```bash -jj commit -m "doc: record the Bellantoni-Cook module and its follow-on work" -``` - ---- - -## Task 7: The pre-push gate - -**Files:** - -- Modify: none expected - -**Interfaces:** - -- Consumes: everything above -- Produces: evidence that the branch is shippable - -- [ ] **Step 1: Run the full checklist** - -Run: `scripts/pre-push.sh` -Expected: every step passes and the script exits 0. - -`lake shake` may print a `PANIC at Option.get!` trace from -`Lake.Shake.visitModule` when the first module under a new -`GebTests/Mathlib//` appears. It exits 0 when it occurs and reproduces -with an unrelated control module at the same path, so it is a shake artifact -rather than a property of this branch. A non-zero exit is a real failure. - -- [ ] **Step 2: Confirm the imports are minimal** - -Run: `lake shake --add-public --keep-prefix Geb GebTests` -Expected: the two new modules are **absent** from the reported file list. -The presence of either means it names `Mathlib.Data.Fin.Tuple.Basic` or -`Mathlib.Data.Fin.VecNotation`; remove the import, since -`Mathlib.Logic.Equiv.Fin.Basic` supplies both. - -The test module's declarations are module-private — it uses plain `import` -with no `public section` — so they cannot be inspected by `#print axioms` -from another file. `lake lint -- GebTests`, which Step 1 already ran, is what -enforces the axiom budget over them: it runs `GebMeta.detectNonstandardAxiom` -across the whole `GebTests` environment, private declarations included. - -- [ ] **Step 3: Commit only if the gate changed something** - -If the checklist regenerated a TOC or reformatted anything: - -```bash -jj commit -m "chore: satisfy the pre-push checklist for the Bellantoni-Cook branch" -``` - -Otherwise skip — a clean gate leaves no change to commit. - ---- - -## Task 8: Remove the spec and the plan - -**Files:** - -- Delete: `docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md` -- Delete: `docs/superpowers/plans/2026-08-04-bellantoni-cook.md` - -**Interfaces:** - -- Consumes: nothing -- Produces: a branch whose working tree carries only persistent content - -CONTRIBUTING.md § Concern shape: specs and plans record how the current -state was reached, not what it is, so they belong in history and not on an -active branch. They remain reachable in the commits of Task 1. - -- [ ] **Step 1: Delete both files** - -```bash -rm docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md -rm docs/superpowers/plans/2026-08-04-bellantoni-cook.md -``` - -- [ ] **Step 2: Confirm nothing else changed** - -Run: `jj status` -Expected: exactly two lines, both `D`. - -- [ ] **Step 3: Re-check the Markdown** - -The removal touches no `.lean` file, so the full checklist of Task 7 need -not run again; only its Markdown steps can be affected. - -```bash -doctoc --dryrun --update-only . -markdownlint-cli2 '**/*.md' -``` - -Expected: `Everything is OK.` and `Summary: 0 issues in 0 files`. - -- [ ] **Step 4: Commit** - -```bash -jj commit -m "doc: remove the Bellantoni-Cook spec and plan" -``` - -- [ ] **Step 5: Advance the bookmark** - -```bash -jj bookmark set feat/bellantoni-cook -r @- -``` - -Run: `jj log -r 'main..feat/bellantoni-cook'` -Expected: eight or nine commits — spec, plan, three library, tests, docs, -the removal, and the gate's only if it had something to commit. - -**Do not push.** AGENTS.md § No `jj git push` without user line-by-line -review: every push, including a first creation, waits on the user reading -the diff. diff --git a/docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md b/docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md deleted file mode 100644 index d05991e..0000000 --- a/docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md +++ /dev/null @@ -1,1023 +0,0 @@ -# Bellantoni-Cook syntax and semantics — design - - - - -- [Purpose](#purpose) -- [Sources](#sources) - - [Per-definition classification](#per-definition-classification) - - [Deviation 1: the class is the reformulation, not the original](#deviation-1-the-class-is-the-reformulation-not-the-original) - - [Deviation 2: `cond` argument order](#deviation-2-cond-argument-order) - - [Deviation 3: the syntax is a slice W-type](#deviation-3-the-syntax-is-a-slice-w-type) - - [Deviation 4: shapes carry the composition arities](#deviation-4-shapes-carry-the-composition-arities) - - [Deviation 5: environments as functions](#deviation-5-environments-as-functions) - - [Deviation 6: names](#deviation-6-names) - - [The paper's `mult` is ill-formed as printed](#the-papers-mult-is-ill-formed-as-printed) - - [Licence](#licence) -- [Design](#design) - - [Alternatives considered](#alternatives-considered) - - [Placement and file manifest](#placement-and-file-manifest) - - [The index and the signature](#the-index-and-the-signature) - - [The syntax](#the-syntax) - - [Finiteness and decidable admissibility](#finiteness-and-decidable-admissibility) - - [The semantics](#the-semantics) - - [Exposure](#exposure) - - [Reuse](#reuse) -- [Verification evidence](#verification-evidence) -- [Tests](#tests) -- [Documentation](#documentation) -- [Non-goals](#non-goals) -- [Deferred](#deferred) -- [Constraints](#constraints) - - - -## Purpose - -Define in Lean the syntax of the function class `B` of -[HeraudNowak2011] § 3.2 and its interpretation. - -The consumer is the translation to Cobham's class (Theorems 1 -and 2), which is what makes `B` a characterization of the -polynomial-time functions. It is § Deferred item 3, and this branch -adds it to `TODO.md` together with the two items it depends on and -the four triggers of § Deferred. That consumer is the whole -justification under CONTRIBUTING.md § Code is cost; the syntax and -the semantics are the definitions its statement quantifies over, -and nothing already in the tree consumes them. - -## Sources - -The paper is Sylvain Héraud and David Nowak, *A Formalization of -Polytime Functions*, arXiv:1102.5495 (v2, 31 May 2011). A short -version appeared as ITP 2011, LNCS 6898, pp. 119-134, -`doi:10.1007/978-3-642-22863-6_11`. Every section and page number -here is the arXiv version's, which is the source of record; the -short version is not established to carry the same numbering. - -The reference implementation is the Coq development -`github.com/davidnowak/bellantonicook` (opam -`coq-bellantonicook`), at commit -`1f03b9296104646ddc2b2b4b12e35a6619c17a99` (2018-09-13). Every -line number below is that revision's. -`src/BellantoniCook/BC.v` carries the syntax (12-19), the arity -apparatus (`Inductive Arities` 85-89, `aeq` 91-95, -`Fixpoint arities` 115-143, `arities2` 145-149), and the semantics -(`sem_rec` 380-386, `sem` 388-422). - -### Per-definition classification - -CONTRIBUTING.md § Cite the literature when transcribing requires -each definition to be marked transcription or novel. - -| Definition | Classification | -| --- | --- | -| the seven constructor forms of `B` | transcription, § 3.2 | -| the arity relation `A` | transcription, § 3.2 | -| every semantic clause | transcription, § 3.2 (with Deviation 2) | -| `plus`, `mult` and their subterms `plusStep`, `multBase`, `multStep` (test module) | transcription, § 3.2, corrected per § The paper's `mult` is ill-formed as printed | -| `Shape`, `Direction`, `rc`, `q`, `sig` | novel | -| `BC`, `BC.arity`, `BCOf` | novel | -| `Sem`, `transport`, `evalRec`, `evalValue`, `evalStep`, `BC.eval` | novel realisations of the transcribed clauses | -| `finEnumFin`, `finEnumCompDirection`, `sigFinitary` | novel | -| `compChildren`, `branchRec`, `badRaw`, `plusOf`, `multOf`, the `Raw` bindings and the four leaf terms `predTerm`, `condTerm`, `projNTerm`, `projSTerm` (test module) | novel | - -### Deviation 1: the class is the reformulation, not the original - -The class defined here is not Bellantoni and Cook's. Paper p. 6: - -> Reader may have noticed that our definition of Bellantoni-Cook's -> class is slightly different from the one in [6]. First, here the -> conditional `cond` distinguishes between three cases (empty, even -> or odd bitstrings), whereas in [6] the empty bitstring is treated -> as an even one. Second, here the base case for recursion is the -> empty bitstring, whereas in [6] it is any bitstring whose -> interpretation as a positive integer is 0 … - -Both differences are realised here: `cond` takes four safe -arguments and branches three ways, where the original branches two -ways on parity; and `evalRec`'s base clause is `[] ↦ g`, where the -original's is every zero-valued bitstring. The module docstring -states this and cites [HeraudNowak2011] and [BellantoniCook1992]. - -### Deviation 2: `cond` argument order - -The paper and its reference implementation disagree. Paper § 3.2 -gives `cond(; ε, x, y, z) = x`, `cond(; w0, x, y, z) = y`, -`cond(; w1, x, y, z) = z` — even selects the third safe argument, -odd the fourth. `BC.v:399-404` matches on the first of four safe -arguments and gives `| nil ↦ b`, `| true :: _ ↦ c`, -`| false :: _ ↦ d` — odd selects the third, even the fourth. - -This design follows the reference implementation. Rationale: the -implementation is the artifact against which the paper's theorems -were machine-checked, so its clause is the one the published -results certify; the paper's prose carries no corresponding check. -The implementation corroborates its own reading at `BC.v:455-457`, -where `cond_simpl_true` takes the hypothesis -`hd false (sem fc l1 l2) = true` and concludes with the third safe -argument. The module docstring records the discrepancy. - -The bit tested is the least significant: `Bitstring.v:50-55` gives -`bs2nat (false :: v') = 2 * bs2nat v'` and -`bs2nat (true :: v') = S (2 * bs2nat v')`, so the list head is the -low bit and the paper's `w0` is `false :: w`. - -### Deviation 3: the syntax is a slice W-type - -The Coq syntax is an untyped `Inductive BC` whose well-formedness -is carried by a separate `arities` function, with a semantics total -on ill-formed terms: an out-of-range projection yields the empty -bitstring, and `cond` carries three further clauses for safe -environments shorter than four (`BC.v:405-416`). - -Here the arity pair is an index. `docs/rules/lean-coding.md` -§ Recursion and induction through recursors forbids a -self-referential `inductive` and a self-calling `def`, so the -indexed syntax is the slice W-type of a signature functor over -`ℕ × ℕ` and the semantics is one application of its eliminator. -Consequences: - -- Only terms satisfying the arity relation inhabit `BCOf n s`, so - the reference implementation's default values are unreachable. -- The four hand-written induction principles of the reference - implementation (`BC_ind2'` 21-57, `BC_ind2` 59-77, - `BC_ind_inf'` 207-335, `BC_ind_inf` 337-367 — 216 lines) are - replaced by `SlicePFunctor.W.elim` and - `SlicePFunctor.W.induction`. Two reasons are given for them in - the source: `BC.v:8-9`, that Coq's generated recursor ignores the - `list BC` fields of `comp`, covers the first two; `BC.v:377`, - that `BC_ind_inf` "makes easier dealing with arities in inductive - proofs", covers the other two. -- The arity function is not ported as a term-level checker, so the - paper's "polytime checker" reading is not delivered. - `SlicePFunctor.decidableWValid` makes admissibility of a raw tree - decidable, so a checker is recoverable from what is already here. - Deferred. - -The paper's `B_inf` (§ 3.2, final two paragraphs, running onto -p. 8; `BCI.v:4-12`) replaces the single projection with `projIn` -and `projIs` and drops the arity annotations from `proj` and -`comp`. It is not ported. - -### Deviation 4: shapes carry the composition arities - -`Shape.comp` carries `n s m k` where the paper's `comp^{n,s}` -carries two superscripts. In the paper `m` and `k` are determined -by `|gN|`, `|gS|` and `A(h)`; here they must appear in the shape, -because `Direction` is a function of the shape alone and the number -of subterms depends on them. The correspondence is bijective on -well-formed terms: a term of `sig.W` with root shape -`comp n s m k` has exactly `m` normal and `k` safe argument -subterms, and its head subterm has arity `(m, k)`. - -### Deviation 5: environments as functions - -The Coq semantics takes two `list bs` and indexes them with `nth`, -defaulting to the empty bitstring. Here an environment is a -function `Fin n → List Bool`, total by construction, and the -semantics uses `Fin.append`, `Fin.cons` and `Fin.tail`. - -### Deviation 6: names - -`rec` cannot name a `Shape` constructor: `Shape.rec` is the -generated recursor (`inductive Foo | a | rec` fails -with `(kernel) constant has already been declared 'Foo.rec'`). The -shape is `safeRec`, after the standard term for the scheme; the -paper writes `rec`, Bellantoni and Cook "predicative recursion on -notation". `comp` keeps the paper's name. - -The semantics is `eval`, after mathlib's `Nat.Partrec.Code.eval`, -so that `e.eval` is available for `e : BC`. - -### The paper's `mult` is ill-formed as printed - -Page 7 prints -`mult := rec (comp^{1,0} O ⟨⟩ ⟨⟩) (comp^{1,2} plus ⟨π₁^{2,0}⟩ ⟨π₂^{2,1}⟩) (…)` -with `A(mult) = (2, 0)`. The recursion rule of p. 6 forces -`A(h_i) = (2, 1)`, so the superscripts must be `comp^{2,1}`; the -arguments confirm it independently, since `π₁^{2,0}` forces `n = 2` -and `π₂^{2,1}` forces `s = 1`. The reference implementation has -`comp^{2,1}`: `BCUnary.v:233` reads -`comp 2 1 plus_e ((proj 2 0 1) :: nil) ((proj 2 1 2) :: nil)`. -The printed step superscript coincides with `plus`'s, where -`comp^{1,2}` is correct. The printed base superscript -`comp^{1,0}` has no counterpart in `plus` and is correct as -printed. - -Under this design a literal transcription of the printed term -fails `decide`: `Shape.comp 1 2 1 1` requires its normal-argument -subterm at index `(1, 0)`, while `proj 2 0 1` carries `(2, 0)`. -§ Tests transcribes the reference implementation's arities. - -### Licence - -The reference development ships the CeCILL Free Software Licence -Agreement v2.1, though its README and opam metadata both name -CeCILL-A. Either way it is copyleft, and this repository is -Apache-2.0. No code is taken from it: the definitions are -transcribed from the paper, and Deviation 2 quotes three match arms -of `BC.v` as evidence for a factual claim about the two sources. -The development is catalogued in `docs/references.md`, which is -where the repository records external library pointers; no -attribution notice is added to the module. - -## Design - -### Alternatives considered - -**A `Geb/Cslib/` module over mathlib's `WType`,** targeting CSLib -instead. `Geb/Cslib/` may not import `Geb.Mathlib.*` -(`docs/rules/upstream-eligible.md:127`), so this route cannot use -the slice W-type: `WType` is unindexed, and the -index-and-admissibility fold (`Slice/W.lean:188-190`, itself a -`WType.elim`) and its decidability (`Slice/Decidable.lean:128`) -would be restated for this signature — perhaps 40 to 60 lines, -since only one signature is involved, not the 413-line general -`Slice/W.lean`. The arity relation would become a predicate to -reason about rather than the maps `q` and `rc`, and the checker of -§ Deviation 3 would be built rather than instantiated. Both routes are -upstream-eligible, so the choice is not between upstreaming and -not. - -The slice-W route is chosen on those two grounds — it restates -nothing, and it makes the arity relation data, the maps `q` and -`rc`, rather than a predicate, which is what § Deviation 3's -`BCOf` and the deferred checker rest on. Its own overhead is the -`@[expose]` discipline, the `@[reducible]` calibration recorded -below, and two `FinEnum` instances existing only to feed -`decidableWValid`, which is the smaller of the two. The subtree, -and with it the upstream target, follows from that choice rather -than preceding it: the slice W-type is `Geb.Mathlib.*`, which only -`Geb/Mathlib/` may import. - -**A uniform `Fin` `Direction`,** taking `Fin (1 + (m + k))` for -`comp` and splitting it with `Fin.cases` and `Fin.addCases`. That -leaves one `FinEnum` obligation instead of two, and lets every test -term's children be written with `![…]`. Against it: `rc` and -`evalValue`'s `comp` clause become index arithmetic rather than -case distinctions on a sum. The sum is kept, and § Tests pays the -cost with one `compChildren` helper. - -### Placement and file manifest - -| Path | Change | -| --- | --- | -| `docs/superpowers/specs/2026-08-04-bellantoni-cook-design.md` | this spec; added, then removed | -| `docs/superpowers/plans/…` | the plan; added, then removed | -| `Geb/Mathlib.lean` | one `public import` added, in the form of `:8-10` | -| `Geb/Mathlib/Computability.lean` | new; the directory index, titled `# Computability — index` after `Geb/Mathlib/Data.lean` (a title naming `Geb.Mathlib.` would fail `scripts/lint-imports.sh`'s self-prefix check) | -| `Geb/Mathlib/Computability/BellantoniCook.lean` | new; the content | -| `GebTests/Mathlib.lean` | one import added, matching that file's existing form | -| `GebTests/Mathlib/Computability.lean` | new; the test directory index, titled `# Computability tests — index` after `GebTests/Mathlib/Data.lean` | -| `GebTests/Mathlib/Computability/BellantoniCook.lean` | new; the tests | -| `docs/references.bib` | two entries added | -| `docs/references.md` | one pointer added | -| `docs/index.md` | one bullet added | -| `TODO.md` | one subsection added, plus four trigger entries; its doctoc TOC re-run in the same commit | - -Commit order: the spec, then the plan, then the library module, -then the test module, then the documentation, then a final commit -removing the spec and the plan (CONTRIBUTING.md § Concern shape). - -The subtree is `Geb/Mathlib/`, whose allowed imports are -`Mathlib.*`, `Batteries.*` and `Geb.Mathlib.*` -(`docs/rules/upstream-eligible.md` § Subtree import rules; -`scripts/lint-imports.sh:179-180`). The design's only non-mathlib -import, `Geb.Mathlib.Data.PFunctor.Slice.*`, is a `Geb.Mathlib.*` -module, so the placement is legal with no rule change and the -module stays upstream-eligible. `Geb/Cslib/` is excluded: it may -not import `Geb.Mathlib.*` at all -(`docs/rules/upstream-eligible.md:127`), CSLib PRs having no access -to unupstreamed mathlib-targeted content. - -The upstream target is mathlib4. `Mathlib/Computability/` already -carries this artifact's construction: `Nat.Partrec.Code` -(`Mathlib/Computability/PartrecCode.lean:76`, `eval` at `:464`) is -a deep-embedded syntax with an `eval`, as `BC` and `BC.eval` are, -and `Nat.Primrec` and `Nat.Partrec` are the recursion-theoretic -material `B` sits beside. CSLib has a claim too — -`Cslib/Computability/README.md` names "complexity classes" in its -scope, where mathlib's complexity content is confined to -machine-model resource bounds (`TM2ComputableInPolyTime` and -relatives, in `TuringMachine/Computable.lean`). It is not taken, -because § Alternatives considered chooses the slice-W encoding on -technical grounds and only `Geb/Mathlib/` can host it. Were the -encoding ever revisited, the target would be open again. - -`scripts/extract-pr.sh:52-62` maps `Geb/Mathlib/*` to `Mathlib/` -and so extracts this module correctly. Its own comment records -that the mapping is an over-approximation for modules targeting -Lean core or Batteries; that reservation does not reach this one. - -Under § Floodgate test the branch stays ready to ship -dependency-ordered PRs: `B` ships after -`Geb/Mathlib/Data/PFunctor/Slice/`. That is ordinary here — 45 -non-index modules under `Geb/Mathlib/` already import -`Geb.Mathlib.*` siblings, 24 of them from another directory, as -`CategoryTheory/FinSetSkel/Quotient.lean:8-11` does. - -`Geb/Mathlib/Computability.lean` and its test counterpart are -directory index files, one per directory as the subtree's existing -`Data.lean`, `CategoryTheory.lean` and `Logic.lean` are. The -content is one module: this workstream states no lemmas, so nothing -separates a `Defs`/`Basic` split. - -All library declarations sit in `namespace BellantoniCook` — a -top-level namespace in mathlib's manner (`Turing`, `Language`), and -carrying no `Geb.Mathlib.` self-prefix, which -`docs/rules/upstream-eligible.md` forbids in namespace -declarations. `arity` and `eval` are written inside that namespace -as `def BC.arity` and `def BC.eval`, so that `e.arity` and `e.eval` -resolve for `e : BC`. - -Bitstrings are `List Bool` written directly. mathlib offers no -other carrier: `BitVec n` is fixed-width, `Nat.bits` cannot -distinguish -`0` from `00` (the paper's stated reason for leaving positive -integers), `FreeMonoid Bool` is `List Bool` plus unwanted -structure, and `Mathlib/Computability/Encoding.lean:94` itself uses -`List Bool`. - -### The index and the signature - -The index is `I := ℕ × ℕ`, the pair of normal and safe arities. All -four universe parameters are `0` and no universe annotation is -needed. - - inductive Shape - | zero - | proj (n s : ℕ) (i : Fin (n + s)) - | succ (b : Bool) - | pred - | cond - | safeRec (n s : ℕ) - | comp (n s m k : ℕ) - - @[expose, reducible] def Direction : Shape → Type - | .zero => Fin 0 - | .proj _ _ _ => Fin 0 - | .succ _ => Fin 0 - | .pred => Fin 0 - | .cond => Fin 0 - | .safeRec _ _ => Fin 3 - | .comp _ _ m k => Unit ⊕ Fin m ⊕ Fin k - - @[expose, reducible] def rc : (a : Shape) → Direction a → ℕ × ℕ - | .zero, i => i.elim0 - | .proj _ _ _, i => i.elim0 - | .succ _, i => i.elim0 - | .pred, i => i.elim0 - | .cond, i => i.elim0 - | .safeRec n s, ⟨0, _⟩ => (n, s) - | .safeRec n s, _ => (n + 1, s + 1) - | .comp _ _ m k, .inl () => (m, k) - | .comp n _ _ _, .inr (.inl _) => (n, 0) - | .comp n s _ _, .inr (.inr _) => (n, s) - - @[expose, reducible] def q : Shape → ℕ × ℕ - | .zero => (0, 0) - | .proj n s _ => (n, s) - | .succ _ => (0, 1) - | .pred => (0, 1) - | .cond => (0, 4) - | .safeRec n s => (n + 1, s) - | .comp n s _ _ => (n, s) - - @[expose] def sig : SlicePFunctor (ℕ × ℕ) (ℕ × ℕ) where - A := Shape - B := Direction - r := fun x ↦ rc x.1 x.2 - q := q - -`Shape` is non-recursive — no field mentions `Shape` — so -§ Recursion and induction through recursors does not reach it: the -rule's subject is self-reference, which `sig.W` carries, and a -non-recursive `inductive` is exactly the shape set `A` of a -`PFunctor`. `GebTests/Mathlib/Data/PFunctor/Presheaf/Fixtures.lean:129-134` -declares `inductive Shp` in the same role, with a hand-written -choice-free `FinEnum Shp` at 137. - -`Shape` carries no `deriving` clause. § Structure and typeclass -patterns' standard derivations would all apply — its fields are -`ℕ`, `Bool` and `Fin` — but nothing here consumes them, and -`DecidableEq`/`Repr` for `BC` are § Deferred item 6, which is where -a derivation on `Shape` would be introduced alongside its lift. - -`q` is the paper's arity relation read as a function of the shape -and `rc` is its hypotheses. `rc`'s `safeRec` clauses match -`Fin.mk 0` first, so direction `0` is `g` and directions `1` and -`2` are `h₀` and `h₁`. `comp`'s `inr (inl i) ↦ (n, 0)` is the -paper's "the functions in `gN` only have access to normal -variables"; `safeRec`'s directions `1` and `2` at `(n+1, s+1)` are -its `n_h = n_g + 1`, `s_h = s_g + 1`. - -`Direction`, `rc` and `q` carry `@[reducible]`, not -`@[implicit_reducible]`. Measured: with `implicit_reducible` every -numeral in § The semantics fails, thirteen errors of the form -`failed to synthesize instance of type class OfNat (Fin (q -(Shape.succ b)).2) 0`; `implicit_reducible` governs unification at -implicit transparency inside dependent types, which is what -`Slice/Basic.lean:83-87` documents it for, whereas `OfNat` -synthesis needs `reducible`. With `@[expose, reducible]` every -clause elaborates with no binder ascriptions. - -### The syntax - - @[expose] def BC : Type := sig.W - @[expose] def BC.arity : BC → ℕ × ℕ := sig.wIndex - @[expose] def BCOf (n s : ℕ) : Type := { e : BC // e.arity = (n, s) } - -`sig.W` is the admissibility subtype of `sig.toPFunctor.W` -(`Geb/Mathlib/Data/PFunctor/Slice/W.lean:221`), so a term of `BC` -is a raw tree together with a proof that every node's children -carry the indices `rc` prescribes. `BCOf n s` is the type of -expressions `e` with `A(e) = (n, s)`: it is what makes the arity -relation of § 3.2 a type rather than a side condition, and it is -what § Deferred item 3 quantifies over — Theorem 1 reads "for all -`f` in `B` with well defined arities `A(f)`, there exists `f'` in -`C` such that …", which is a statement about arity-indexed terms. -It is also what the deferred checker returns. - -### Finiteness and decidable admissibility - -`SlicePFunctor.decidableWValid` -(`Geb/Mathlib/Data/PFunctor/Slice/Decidable.lean:128`) requires -`DecidableEq I`, free for `ℕ × ℕ`, and `sig.toPFunctor.Finitary`, -which is `∀ a, FinEnum (sig.toPFunctor.B a)` -(`Geb/Mathlib/Data/PFunctor/Univariate/Finitary.lean:38`). - -The mathlib `FinEnum` instances this signature would resolve -through depend on `Classical.choice` — measured for `Fin n`, for -`PEmpty` and for sums, and `TODO.md:363-366` records the same for -`FinEnum.fin` and `ULift.instFinEnum`. Resolving `sigFinitary` -through them taints the module and fails `lake lint`, whose -permitted set is `standardAxioms = {propext, Quot.sound}` -(`GebMeta.lean:46-49`, checked by `detectNonstandardAxiom` at -`:113`; run by `scripts/pre-push.sh:30,39`). Two named choice-free -instances are supplied, following `Fixtures.lean:137`: - - scoped instance finEnumFin (n : ℕ) : - FinEnum (Fin n) where - card := n - equiv := Equiv.refl _ - decEq := inferInstance - - scoped instance finEnumCompDirection (m k : ℕ) : - FinEnum (Unit ⊕ Fin m ⊕ Fin k) where - card := 1 + (m + k) - equiv := (Equiv.sumCongr finOneEquiv.symm finSumFinEquiv).trans finSumFinEquiv - decEq := inferInstance - - instance sigFinitary : sig.toPFunctor.Finitary - | .zero => inferInstanceAs (FinEnum (Fin 0)) - | .proj _ _ _ => inferInstanceAs (FinEnum (Fin 0)) - | .succ _ => inferInstanceAs (FinEnum (Fin 0)) - | .pred => inferInstanceAs (FinEnum (Fin 0)) - | .cond => inferInstanceAs (FinEnum (Fin 0)) - | .safeRec _ _ => inferInstanceAs (FinEnum (Fin 3)) - | .comp _ _ m k => inferInstanceAs (FinEnum (Unit ⊕ Fin m ⊕ Fin k)) - -Four points, each measured: - -- `finEnumFin` and `finEnumCompDirection` are `scoped`. A bare - `instance` in the module's `public section` is global, and - `Geb.lean` re-exports `Geb.Mathlib`, so `finEnumFin` would - compete with `FinEnum.fin` at the same head symbol across the - repository: measured, `#synth FinEnum (Fin 3)` in a module - importing `Geb` returns `BellantoniCook.finEnumFin 3` when the - instance is bare and `FinEnum.fin` when it is `scoped`. - `Geb/Mathlib/CategoryTheory/FinCat/Decidable.lean:70` uses - `scoped instance` against the same pressure. Scoping costs the - test module nothing: `sigFinitary`'s branches resolve them by - `inferInstanceAs` from inside their own namespace, where they are - in scope and win on declaration order. -- `sigFinitary` is an `instance`, not a `def`: as a `def` it does - not fire for `decidableWValid`, and it draws `Definition … of - class type is semireducible`, fatal under `weak.warningAsError`. - As an `instance` it needs no attribute; - `GebTests/Mathlib/Data/PFunctor/Slice/Decidable.lean:49` declares - the analogous `finitaryTestSlice` bare. -- The branches are `inferInstanceAs`, not `inferInstance`: instance - search stops at reducible transparency on the projection - `sig.B a`, so a bare `inferInstance` reports - `failed to synthesize instance of type class FinEnum (sig.B - Shape.zero)`. - `GebTests/Mathlib/Data/PFunctor/Slice/Decidable.lean:46-48` - records the same for `decEq`, and does so where the signature is - an `abbrev`, so the cause is the projection, not `sig` being a - `def`. -- `finEnumFin` is built as a cardinality with `Equiv.refl`, the - construction `TODO.md` § PRA functors over finite-specification - base categories anticipates; `Geb/Mathlib/Data/FinEnum.lean:18-22` - documents the explicit-supply mitigation, available because the - instances are named. A trigger records that they move to - `Geb/Mathlib/Data/FinEnum.lean` when a second consumer appears; - moving them now would put a second concern on this branch. - -`finOneEquiv` is `Mathlib/Logic/Equiv/Defs.lean:907` and -`finSumFinEquiv` is `Mathlib/Logic/Equiv/Fin/Basic.lean:228`. - -### The semantics - - @[expose] def Sem : ℕ × ℕ → Type := - fun i ↦ (Fin i.1 → List Bool) → (Fin i.2 → List Bool) → List Bool - - @[expose] def transport {i j : ℕ × ℕ} (h : i = j) (v : Sem i) : Sem j := h ▸ v - -`transport` is named rather than written inline: `evalValue` uses -it six times, and a named function fixes the motive of `▸` once -instead of leaving it to be inferred at each site. - -The recursion on the bitstring `safeRec` consumes is `List.rec`, an -auto-generated recursor and so permitted: - - @[expose] def evalRec {n s : ℕ} (g : Sem (n, s)) - (h₀ h₁ : Sem (n + 1, s + 1)) : List Bool → Sem (n, s) := - List.rec g (fun b v ih x y ↦ - (if b then h₁ else h₀) (Fin.cons v x) (Fin.cons (ih x y) y)) - -`[] ↦ g` is Deviation 1's base case; `h₁` on `true` and `h₀` on -`false` is `BC.v:383-385`; the tail `v` becomes the new first -normal argument and the recursive value enters `h_b` in safe -position as `Fin.cons (ih x y) y`. - -The algebra is an auxiliary taking the compatibility hypothesis -pointwise, because the `Shape` match must generalize it: - - @[expose] def evalValue : (a : Shape) → (c : Direction a → Σ i, Sem i) → - (∀ b, (c b).1 = rc a b) → Sem (q a) - | .zero, _, _ => fun _ _ ↦ [] - | .proj _ _ i, _, _ => fun x y ↦ Fin.append x y i - | .succ b, _, _ => fun _ y ↦ b :: y 0 - | .pred, _, _ => fun _ y ↦ (y 0).tail - | .cond, _, _ => fun _ y ↦ - match y 0 with - | [] => y 1 - | true :: _ => y 2 - | false :: _ => y 3 - | .safeRec _ _, c, h => fun x y ↦ - evalRec (transport (h 0) (c 0).2) (transport (h 1) (c 1).2) - (transport (h 2) (c 2).2) (x 0) (Fin.tail x) y - | .comp _ _ _ _, c, h => fun x y ↦ - transport (h (.inl ())) (c (.inl ())).2 - (fun i ↦ transport (h (.inr (.inl i))) (c (.inr (.inl i))).2 x Fin.elim0) - (fun j ↦ transport (h (.inr (.inr j))) (c (.inr (.inr j))).2 x y) - - @[expose] def evalStep : - sig.toSliceDomPFunctor.Obj (Sigma.fst (β := Sem)) → Σ i, Sem i := - fun z ↦ ⟨sig.q z.1.1, - evalValue z.1.1 z.1.2 - ((sig.toSliceDomPFunctor.compatible_iff _ z.1.1 z.1.2).mp z.2)⟩ - - @[expose] def BC.eval : BC → Σ i, Sem i := - SlicePFunctor.W.elim sig (Σ i, Sem i) (Sigma.fst (β := Sem)) evalStep rfl - -`cond`'s indexing is `y 0` the tested bitstring, `y 1` the empty -case, `y 2` the odd case and `y 3` the even case — Deviation 2's -ordering. `comp`'s head child has arity `(m, k)` and is applied to -the normal arguments' values, each evaluated in the empty safe -environment `Fin.elim0`, and to the safe arguments' values. - -Returning `sig.q z.1.1` as `evalStep`'s first component makes the -eliminator's coherence obligation -`Sigma.fst ∘ evalStep = sig.obj Sigma.fst` hold by `rfl`. Note -`SlicePFunctor.W.elim sig …`, not `sig.W.elim …`: `sig.W` is a -type, not a term, so field notation does not chain through it. - -For `e : BCOf n s`, `e.property` rewrites the index of -`BC.eval e.val` to `(n, s)`; `SlicePFunctor.W.comp_elim` -(`W.lean:352`) is the lemma that the value's index is the tree's. - -### Exposure - -The library module opens a `public section`, and the thirteen -declarations shown above with `@[expose]` carry it — every one -except `Shape` and the three instances, which do not need it — -following -`Geb/Mathlib/Data/PFunctor/Slice/W.lean:132` and the rationale at -`:118`. The test module reduces `BC.eval` applications by `rfl` -across the module boundary, which needs the bodies of `BC.eval`, -`evalStep`, `evalValue`, `evalRec` and `transport`, and discharges -`sig.WValid` by `decide`, which needs `rc`. `sigFinitary` is -resolved by instance search rather than unfolded, so it needs no -`@[expose]`; measured, the tests succeed with all three instances -unexposed. - -The test module uses plain `import` and -`set_option linter.privateModule false`, following -`GebTests/Mathlib/Data/PFunctor/Slice/W.lean:25`. It opens -`BellantoniCook` for unqualified access to `sig`, `BC`, `BCOf` and -`BC.eval`. The `scoped` instances come into scope with it, but -nothing needs them to: `sigFinitary` names them from inside their -own namespace. Measured: the tests' `decide` and `rfl` both succeed with the -three instances unexposed and with no `open` at all. - -### Reuse - -| Coq | here | -| --- | --- | -| `if leb (S j) n then nth j vnl nil else nth (j-n) vsl nil` | `Fin.append x y i` | -| `v' :: vnl` / `tail vnl` / `nil` | `Fin.cons v x` / `Fin.tail x` / `Fin.elim0` | -| the four hand-written induction principles (216 lines) | `SlicePFunctor.W.elim`, `.induction` | -| `Arities`, `aeq`, `arities`, `arities2` | `q`, `rc`, `sig.wIndex` | -| `Fixpoint sem_rec` | `List.rec` | - -## Verification evidence - -Every declaration in § Design, and every test declaration named in -§ Tests, was built and elaborated against the repository toolchain -(v4.33.0-rc2) as two modules at library paths — the library with -`public section` and `@[expose]`, the tests with plain `import` and -`linter.privateModule false` — under the repository's option set -(`autoImplicit false`, `relaxedAutoImplicit false`, -`maxSynthPendingDepth 3`, `weak.linter.mathlibStandardSet true`, -`weak.linter.style.header true`, `weak.warningAsError true`, -`weak.linter.flexible true`, `pp.unicode.fun true`), with copyright -headers and module docstrings. Zero diagnostics on both. Measured: - -- `sig` elaborates as `SlicePFunctor.{0, 0, 0, 0} (ℕ × ℕ) (ℕ × ℕ)` - with no universe annotation. -- The coherence argument to `elim` is `rfl`. -- The transport is `h ▸ v`; no `Eq.mpr`, `cast`, `Subtype.ext` or - `simp` is required, and no clause needs a binder ascription once - `Direction`, `rc` and `q` are `@[reducible]`. -- `by decide` discharges admissibility across the module boundary - in 13.0 ms for `plus` and 22.1 ms for `mult` (25 nodes, - containing `plus` twice) at default `maxHeartbeats`. -- Every assertion of § Tests reduces by `rfl` across the module - boundary. The negative control `decide (sig.WValid badRaw)` - reduces to `false`. -- `#print axioms`: `sig` and `finEnumFin` depend on no axioms; - `sigFinitary`, `finEnumCompDirection`, `BC.eval`, `plus`, `mult` - and every assertion depend on `[propext, Quot.sound]`. Deleting - the two named instances, so that `sigFinitary` resolves through - mathlib's, yields `Classical.choice` on `sigFinitary`, `plus`, - `mult` and every assertion — not on `BC.eval`, which does not - depend on `sigFinitary`. Admissibility is where the taint would - enter, not evaluation. -- The `⟨WType.mk …, by decide⟩` form does not elaborate: instance - search fails to unify `decidableWValid`'s conclusion against a - goal containing an inline `WType.mk` application, reporting - `failed to synthesize Decidable (sig.WValid (WType.mk …))`. A - type ascription does not repair it; binding the raw tree as its - own `def` does, which is the form § Tests specifies. - -Recorded property: `Fin` numerals wrap, so a mistranscribed index -elaborates rather than failing — `(1 : Fin 1) = 0` and -`(5 : Fin 3) = 2` both close by `rfl`. This affects `proj`'s -`Fin (n + s)`, `cond`'s `y 0 … y 3` at `Fin 4`, and `safeRec`'s -`c 0 … c 2` at `Fin 3` alike. Only an expected-output check -distinguishes them, which is why every assertion states an output -and why § Tests carries `branchRec`. - -## Tests - -`GebTests/Mathlib/Computability/BellantoniCook.lean`. - -Each term is built in two steps, because the inline form does not -elaborate (§ Verification evidence): a raw tree bound as its own -`def` at type `sig.toPFunctor.W`, then the admissible term. - - def compChildren {m k : ℕ} (h : sig.toPFunctor.W) - (gN : Fin m → sig.toPFunctor.W) (gS : Fin k → sig.toPFunctor.W) : - Unit ⊕ Fin m ⊕ Fin k → sig.toPFunctor.W := - Sum.elim (fun _ ↦ h) (Sum.elim gN gS) - - def plusStepRaw : sig.toPFunctor.W := - WType.mk (.comp 1 2 0 1) - (compChildren (WType.mk (.succ true) Fin.elim0) Fin.elim0 - ![WType.mk (.proj 1 2 1) Fin.elim0]) - def plusStep : BC := ⟨plusStepRaw, by decide⟩ - -and likewise for the rest. `m` and `k` are implicit and solved by -unification against the expected `Direction (.comp …)`, which is -`@[reducible]` and reduces to the codomain's own -`Unit ⊕ Fin m ⊕ Fin k`. The codomain is written as that sum rather -than as `Direction (.comp n s m k)`, which would leave `n` and `s` -free and fail under `autoImplicit false`. - -Every term is bound this way, leaves included: the two-step form is -required wherever a `by decide` goal mentions the tree, so each of -`plusStepRaw`, `plusRaw`, `multBaseRaw`, `multStepRaw`, `multRaw`, -`branchRecRaw`, `predTermRaw`, `condTermRaw`, `projNTermRaw`, -`projSTermRaw` and `badRaw` is its own `def` at -`sig.toPFunctor.W`. Inline `WType.mk` applications are -admissible only as *children* of such a tree, never as the subject -of the `decide`. - -`safeRec`'s three children are `![…]` directly, -`Direction (.safeRec n s)` being `Fin 3`. A subterm that is already -a `BC` enters a parent's raw tree as `.val`. - -`plus` and `mult` are § 3.2's examples at arities `(1,1)` and -`(2,0)`, transcribed with the arities of the reference -implementation rather than the printed superscripts (§ The paper's -`mult` is ill-formed as printed): - -- `plusStep`: `comp 1 2 0 1`, head `succ true`, no normal - arguments, safe argument `proj 1 2 1`. -- `plus`: `safeRec 0 1`, children `![proj 0 1 0, plusStep, plusStep]`. -- `multBase`: `comp 1 0 0 0`, head `zero`, no arguments. -- `multStep`: `comp 2 1 1 1`, head `plus`, normal argument - `proj 2 0 1`, safe argument `proj 2 1 2`. -- `mult`: `safeRec 1 0`, children `![multBase, multStep, multStep]`. - -They compute unary arithmetic: -`plus x y = List.replicate x.length true ++ y` and -`mult x y = List.replicate (x.length * y.length) true`. The -justification is the definitions, not the reference development's -length lemmas (`plus_correct` at `BCUnary.v:172-173` and -`mult_correct` at `:236-237` state only `|plus m n| = |m| + |n|` -and `|mult m n| = |m| · |n|`, and a length equation does not -determine a value): `succ_e` is `succ true` (`BCUnary.v:116`), so -each step of `plus` (`:167-170`) prepends `true` to its safe -argument; `mult` (`:231-234`) iterates `plus` from the base -`zero_e 1 0`, which is `comp 1 0 zero nil nil` (`BC.v:1034-1035`) -and whose head `zero` evaluates to the empty bitstring -(`BC.v:390`, through the `comp` clause at `:419-421`). - -`plus` takes one normal and one safe argument; `mult` takes two -normal arguments and none safe (`sem mult_e [m; n] nil`). Each -assertion names its two environments accordingly. - -`plus` and `mult` both pass the same subterm as `safeRec`'s -directions 1 and 2, so neither discriminates `h₀` from `h₁`: with -those alone, transposing `c 1` and `c 2` in `evalValue` would leave -every assertion passing. `branchRec` closes this. It is -`safeRec 0 0` with children `![zero, proj 1 1 0, proj 1 1 1]`, of -arity `(1, 0)`, so that - - f [] = [], f (b :: v) = if b then f v else v - -Single-bit arguments do not discriminate: `f [false]` and -`f [true]` are both `[]` under the intended reading and under the -transposed one. The assertions are therefore at length two: -`branchRec` on `![[false, true]]` is `[true]` and on `![[true, true]]` -is `[]`. Measured: rebuilding `evalValue` with `c 1` and `c 2` -transposed fails exactly these two assertions and no others. - -`badRaw` is a `sig.toPFunctor.W`, not a `BC`: `plusStepRaw` with -its safe child replaced by `WType.mk (.proj 2 0 1) Fin.elim0`, -which carries index `(2, 0)` where `rc` demands `(1, 2)`. - -Four leaf terms cover what the compound terms do not: `predTerm` -and `condTerm`, `pred` and `cond` appearing in no other term; and -`projNTerm` (`proj 1 1 0`) and `projSTerm` (`proj 1 1 1`), which -separate the two halves of `Fin.append` at a single node, the -`Fin`-wraparound property above being what motivates checking them -apart. `zero` and `succ true` need no leaf term: they are the -heads of `multBase` and `plusStep`, whose outputs `eval_mult` and -`eval_plus_cons` already pin. Each leaf is a single node with -`Fin.elim0` children, admissible vacuously but still bound in two -steps. - -The twelve evaluation assertions have the form -`(BC.eval e).2 env₁ env₂ = out`; the negative control, whose -environments the coverage table marks `—`, is the thirteenth and -last row. Each evaluation assertion is named `eval_`, with a -suffix where one term carries several -— `eval_plus_nil`, `eval_plus_cons`, `eval_mult`, -`eval_branchRec_false`, `eval_branchRec_true`, -`eval_predTerm_nil`, `eval_predTerm_cons`, -`eval_condTerm_empty`, `eval_condTerm_odd`, `eval_condTerm_even`, -`eval_projNTerm`, `eval_projSTerm`. The negative control is -`wValid_badRaw_eq_false`, stated in the coverage table's -`decide (sig.WValid badRaw) = false` form rather than as -`¬ sig.WValid badRaw`, so that it too closes by `rfl`. Each -carries a `/-- … -/` -docstring, `docs/rules/lean-coding.md` § Comment and docstring -rules requiring one of every theorem of public interest, which the -module's `## Main statements` section makes these. - -Assertions are named `theorem`s. They cannot be `def`s — -`linter.defProp` rejects a `def` whose type is a `Prop`, and -`GebTests` inherits `mathlibStandardSet` and `weak.warningAsError` -from the package-level `[leanOptions]` (`lakefile.toml:12,15`; the -library-level block at `:59-60` overrides only -`linter.hashCommand`). The raw-tree and term `def`s anchor the -module's imports for `lake shake`, as `wLeaf`/`wNode` do in -`GebTests/Mathlib/Data/PFunctor/Slice/W.lean`; where an import is -still reported removable it carries a `-- shake: keep` comment, as -`GebTests/Mathlib/CategoryTheory/FinCat/FinCategory.lean:8-10` -does. - -Coverage. Each of the following is a `theorem` stating an expected -output and closing by `rfl`: - -| assertion | environments | output | -| --- | --- | --- | -| `plus` | `![[]]`, `![[false]]` | `[false]` | -| `plus` | `![[true, true]]`, `![[false]]` | `[true, true, false]` | -| `mult` | `![[true, true], [true, true, true]]`, `![]` | `List.replicate 6 true` | -| `branchRec` | `![[false, true]]`, `![]` | `[true]` | -| `branchRec` | `![[true, true]]`, `![]` | `[]` | -| `predTerm` | `![]`, `![[]]` | `[]` | -| `predTerm` | `![]`, `![[true, false]]` | `[false]` | -| `condTerm` | `![]`, `![[], [false], [true], [true, true]]` | `[false]` | -| `condTerm` | `![]`, `![[true], [false], [true], [true, true]]` | `[true]` | -| `condTerm` | `![]`, `![[false], [false], [true], [true, true]]` | `[true, true]` | -| `projNTerm` | `![[true]]`, `![[false]]` | `[true]` | -| `projSTerm` | `![[true]]`, `![[false]]` | `[false]` | -| `decide (sig.WValid badRaw)` | — | `false` | - -`BCOf` is exercised by two `def`s rather than `theorem`s, `BCOf n s` -being a type and not a `Prop`: -`def plusOf : BCOf 1 1 := ⟨plus, rfl⟩` and -`def multOf : BCOf 2 0 := ⟨mult, rfl⟩`. These subsume the arities: -each elaborates exactly when `BC.arity` of its term reduces to the -stated pair, so no separate `arity_plus`/`arity_mult` theorem is -carried. - -## Documentation - -- Module docstring: `# Title`, summary, `## Main definitions` (the - fourteen library declarations other than the three instances, - which mathlib's guide does not list there), `## Implementation notes` (the - W-type encoding and the rule requiring it; the transport and why - `evalValue` is separate; the choice-free `scoped` `FinEnum` - instances; the `@[reducible]` requirement), `## References` - (`[HeraudNowak2011]`, `[BellantoniCook1992]`), `## Tags` - (`Bellantoni-Cook, polytime, implicit computational complexity, - safe recursion, W-type, polynomial functor`). `## Main - statements` and `## Notation` are omitted as vacuous. Every - declaration carries a `/-- … -/` docstring; `Shape`'s seven - constructors are documented within the type's own docstring, as - `Fixtures.lean:127-128` documents `Shp`'s. All four new `.lean` - files carry the standard copyright header, and the two index - files carry a module docstring in the form of - `Geb/Mathlib/Data.lean`'s. -- The test module carries `# Title`, a summary and `## Tags`, as - `GebTests/Mathlib/Data/PFunctor/Slice/W.lean:11-23` does; plus - `## References` citing `[HeraudNowak2011]`, since `plus` and - `mult` are transcribed, and `## Main statements` for its named - theorems. `docs/rules/lean-coding.md` § Documentation requires - each section that has content. Its twenty-four `def`s — the - eleven raw trees, the ten terms, `compChildren`, `plusOf` and - `multOf` — each carry a `/-- … -/` docstring, § Comment and - docstring rules mandating one for every `def`. A raw tree's - states its shape and children; a term's states its arity and, - for `plus`, `mult` and `branchRec`, the function it computes; - `compChildren`'s states the head-then-normal-then-safe order it - imposes; `plusOf`'s and `multOf`'s state that they exhibit their - terms at the arities `§ Tests` claims. -- `docs/references.bib`: `HeraudNowak2011` as `@inproceedings` at - ITP 2011 (`author = {H{\'e}raud, Sylvain and Nowak, David}`, - `title`, `booktitle`, `series`, `volume = {6898}`, - `pages = {119--134}`, `publisher`, `year`, `doi`) carrying - `eprint = {1102.5495}`, `archivePrefix = {arXiv}`, - `primaryClass = {cs.CC}`, and a `note` recording that this - repository cites the arXiv version's section and page numbering. - The file's entries for works existing as both preprint and - publication are the published type with the preprint in `eprint` - (`AllaisAtkeyChapmanMcBrideMcKinna2021`, - `GhaniNordvallForsbergMalatesta2015`, `JohnsonYau2021`, - `AvanziniDalLago2018`, `AltenkirchChapmanUustalu2015`), `note` - being used only for what those fields cannot carry — as in - `HancockMcBrideGhaniMalatestaAltenkirch2013`, which is this - situation exactly: proceedings entry, `note` naming which - version's numbering the repository cites. `Vistoli2008` is - `@misc` because it has no publication, not because the preprint - is cited. The accented surname is - LaTeX-escaped, as `Par{\'e}` is. - `BellantoniCook1992` as `@article`: Bellantoni and Cook, *A new - recursion-theoretic characterization of the polytime functions*, - Computational Complexity 2(2), 97-110, 1992, - `doi:10.1007/BF01201998` — the field set and order of `Pare1974`. -- `docs/references.md` § Computability: a pointer to - `github.com/davidnowak/bellantonicook` at the commit named in - § Sources. -- `docs/index.md` § Implemented content: one bullet in the file's - flat one-bullet-per-module form, among the other `Geb/Mathlib/` - bullets and after those for - `Geb/Mathlib/Data/PFunctor/Slice/`, which it depends on, reading - to the effect of - "`Geb/Mathlib/Computability/BellantoniCook.lean` - — the function class `B` of [HeraudNowak2011] § 3.2: its arity - relation as a `SlicePFunctor` over `ℕ × ℕ`, its syntax as that - functor's slice W-type, and its semantics by the W-type's - eliminator. Depends on `Geb.Mathlib.Data.PFunctor.Slice.W` and - `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`. Every declaration of - the module has axioms within `propext` and `Quot.sound`; `sig` and - `finEnumFin` have none." - — covering the path, the concepts and the dependencies per - docs/process.md § Documentation - under `docs/`, and stating the axiom dependence in prose, as the - file's existing bullets do. -- `TODO.md`: a `### Bellantoni-Cook` subsection under `## Next up` - containing § Deferred items 1-3 with their scope, dependencies - and return, in the neighbouring subsections' form; and items 4 - to 7 under `## Triggers (do when condition fires)`, in that - section's `- **Bold title**: …` bullet form. - -## Non-goals - -Not part of the syntax and its interpretation, and not planned: -`sem_cost` (the time-complexity semantics) and `BCI`/`B_inf` with -its two translations. Neither forecloses the deferred work: -`BCLib.v`, `BC_to_Cobham.v` and `Cobham_to_BC.v` contain no -occurrence of `BCI` or of `sem_cost`, and `sem_cost` is first -defined at `BC.v:1365`, after Proposition 2 at `:1128`. - -## Deferred - -Items 1-3 are a dependency chain and go to `## Next up`. Items 4 -to 7 are triggers, none having a consumer yet, and go to -`## Triggers (do when condition fires)` in that section's -`- **Bold title**: …` bullet form. - -1. `MultiPoly`, the multivariate polynomial library. Required by - `BC_to_Cobham.v:2`, by `Cobham_to_BC.v:2`, and by Proposition 2, - whose statement `polymax_bounding` (`BC.v:1128`) is over - `poly_BC` (`:1075`), built from `pcst`, `pproj`, `pplus`, - `pmult`, `pcomp`, `pshift` and `pplusl`. Returns the polynomial - apparatus both later items are stated over. -2. Proposition 2, the polymax bounding of `B`. Depends on 1. - Returns the length bound that the translation of 3 requires. -3. Cobham's class and the translations of Theorems 1 and 2. - Depends on 1 and 2. Returns the characterization of polynomial - time, and is the consumer named in § Purpose. -4. Trigger: a workstream needs programmable building blocks for - terms of `B`. Port the derived function library of `BCLib.v`, - which depends only on the syntax and semantics delivered here. -5. Trigger: a second consumer of `finEnumFin` or - `finEnumCompDirection` appears. Move them to - `Geb/Mathlib/Data/FinEnum.lean`, the repository's home for - choice-free `FinEnum` support. -6. Trigger: a consumer needs `DecidableEq` or `Repr` for `BC`. - Derive them on `Shape` and lift along `sig.W`'s subtype. -7. Trigger: a workstream needs the paper's "polytime checker" as a - term-level artifact. Add an untyped `Ast` plus - `check : Ast → Option ((n s : ℕ) × BCOf n s)` over - `SlicePFunctor.decidableWValid`. - -## Constraints - -1. No `noncomputable`. `#print axioms` on every declaration lies - within `{propext, Quot.sound}`, measured monomorphically in the - consuming closure and re-measured at each toolchain bump - (`docs/rules/lean-coding.md` § Constructive-only Lean code). - `Quot.sound` is permitted, not excluded. The `FinEnum` instances - are the reason this is not automatic. -2. No self-referential `inductive` and no self-calling `def`; - `Shape` is non-recursive, the syntax's recursion is `sig.W`, and - the semantics' recursions are `SlicePFunctor.W.elim` and - `List.rec`. -3. All four new `.lean` files declare `module`. The library module uses - `public import` and a `public section`; the test module uses - plain `import` with `set_option linter.privateModule false` - (§ Exposure). -4. `scripts/pre-push.sh` clean, `lake shake`, `lake lint` and - `scripts/lint-imports.sh` included. `lake shake` has been observed to print a - `PANIC at Option.get!` trace from `Lake.Shake.visitModule` when - the first module under a new `GebTests/Mathlib//` appears. - It does not reproduce reliably, exits 0 when it occurs, and - occurs equally with an unrelated control module at the same - path, so it is a shake artifact rather than a property of this - design. The subtree's rules bind: - no import outside `Mathlib.*`, `Batteries.*`, `Geb.Mathlib.*` - (and `GebTests.Mathlib.*` for the test module); no bare umbrella - import; and no `Geb.Mathlib.` or `GebTests.Mathlib.` prefix - outside an `^import` line, in particular not in the namespace - declarations. -5. No `#guard`; every assertion is a `theorem` closing by `rfl`. - `plusOf` and `multOf` are `def`s, `BCOf n s` being a type rather - than a `Prop`. Should an assertion not reduce, the term is - shrunk until it does; `native_decide` is forbidden by - Constraint 1 and `#guard` by this constraint. -6. Lambda notation follows `docs/rules/lean-coding.md` § Coding - style: `↦`, not `=>`, in `fun`. -7. Library imports: `Geb.Mathlib.Data.PFunctor.Slice.W`, - `Geb.Mathlib.Data.PFunctor.Univariate.Finitary`, - `Mathlib.Logic.Equiv.Fin.Basic`. The test module adds - `Geb.Mathlib.Data.PFunctor.Slice.Decidable`, besides - `Geb.Mathlib.Computability.BellantoniCook` itself. - - `Slice.Decidable` belongs to the tests, not the library: the - library uses `SlicePFunctor`, `.W`, `.wIndex` and `W.elim` from - `Slice/W.lean` and `PFunctor.Finitary` from - `Univariate/Finitary.lean`, and nothing from - `Slice/Decidable.lean`; `decidableWValid` is reached only by the - tests' `by decide`. Measured: - `lake shake --add-public --keep-implied --keep-prefix Geb - GebTests`, the form `scripts/pre-push.sh:42` runs, exits 0 with - no suggestion for either new file, and no `-- shake: keep` - comment is needed. Placing `Slice.Decidable` in the library - instead makes it exit 1, asking for `Slice.W` and - `Univariate.Finitary` to be added and `Slice.Decidable` - removed. - - `Mathlib.Data.Fin.Tuple.Basic` and `Mathlib.Data.Fin.VecNotation` - are not named, though the modules apply `Fin.append`, - `Fin.cons`, `Fin.tail` and `![…]` directly: - `Mathlib.Logic.Equiv.Fin.Basic` imports `VecNotation`, which - imports `Fin.Tuple.Basic`, so naming them makes plain - `lake shake` — the form mathlib CI runs — report both modules as - carrying a redundant import. Measured: with them named, plain - `lake shake --add-public --keep-prefix Geb GebTests` reports 16 - `Geb/Mathlib/` and 8 `GebTests` files against a baseline of 15 - and 7; without them, the baseline is unchanged and both modules - still build. Omitting them keeps the branch off the count in - `TODO.md`'s `lake shake --keep-implied` trigger and keeps the - upstream-eligible module minimal, as CONTRIBUTING.md § Floodgate - test requires of a PR shipped with no source-code change.