Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions docs/r3-design-schedule-2026-05-06.md
Original file line number Diff line number Diff line change
Expand Up @@ -49,10 +49,12 @@ Prior `AbelianGroup<Nat>` references in r3-structure.md, r3-program-plan.md, thi

1. **Axes in R3 scope**: `MachineWidth<bits>` only. `RegisterClass<R>` / `EndianMode<E>` / alignment / signedness-as-axis deferred post-R3 absent a closure-gate forcing them. **Discipline note (Brian directive)**: this is a separation-of-facts/concerns exercise — algebra is one axis of fact, machine constraint is another, target lowering (e.g., Rust emission) is a *projection / coercion* over both. Integer modeling is the canonical exercise for this discipline; getting comfortable with the separation is the broader R3 modeling work.
2. **Interaction substrate shape**: **REST-API-style typed-contract interactions between models** (Brian directive 2026-05-06: *"these models interact a la rest apis interacting — scalable / no dual representations (.dag generated)"*). Each model (algebra, machine-constraint) declares its interface in `.dag`; the interaction substrate (composition, projection, coercion) is **`.dag`-generated**, not hand-coded. **Hard constraint: no dual representations** — any Rust counterpart must be generated from `.dag`, never hand-maintained (per `feedback_isomorphism_or_generation_for_mirrors` + `feedback_no_generated_code_on_disk`). Closed-enumeration lookup-maps and parallel Rust mirrors are both rejected (bridges).
3. **Type-level spelling**: `Int<64>` parses/elaborates as `Compose<AbelianGroup, MachineWidth<64>>` parametrically. Surface intuition is the literal product `Int × MachineWidth<64>`; substrate spelling is parametric. Equivalent under both algebra-side options per PR #1815. **Distinction (per claude review observation)**: the *elaboration* of a particular `Compose<AbelianGroup, MachineWidth<64>>` term is parser/elaborator behavior; the **interaction substrate** (composition/projection/coercion machinery operating *on* such Compose terms) is what's `.dag`-generated per sub-decision 2 — not the `Compose<...>` *type itself*. S3 worker brief should preserve this distinction.
4. **Approximate-algebra layering**: algebra-side approximation (`ApproximateField<Rational>`) and machine-side approximation (`MachineWidth<64>`) stay as independent axes that compose. `Real<64>` = `Compose<ApproximateField<Rational>, MachineWidth<64>>` carries both layers explicitly per S8's named-axiom-relaxation discipline.
3. **Type-level spelling**: `Int<64>` parses/elaborates as **`Compose<Int, MachineWidth<64>>`** parametrically — first slot is the **algebraic concept** (the fully-applied carrier+witness composite, e.g., `Int = AbelianGroup<GroupCompletion<Nat>>` per #1466 already on main), second slot is the machine-constraint axis. **Critical correction (per codex BLOCKING 2026-05-06)**: prior phrasing `Compose<AbelianGroup, MachineWidth<64>>` was wrong — `AbelianGroup<T>` is a *witness shape* generic over carrier `T`, not a carrier constructor (per `dsl/std/algebra.dag:148-150`: *"T = GroupCompletion<M> is the carrier; AbelianGroup<T> carries op/identity/inverse over that carrier"*). Putting bare `AbelianGroup` in `Compose<...>` slot-1 composes the witness rather than the integer concept; correct form is `Compose<Int, MachineWidth<64>>` where `Int` IS the carrier+witness composite. Same pattern for: `UInt<64>` = `Compose<UInt, MachineWidth<64>>` (where `UInt = CommutativeMonoid<Nat>` per #1818), `Real<64>` = `Compose<Real, MachineWidth<64>>` (where `Real = ApproximateField<Rational>`), `Nat<8>` = `Compose<Nat, MachineWidth<8>>`. Surface intuition is the literal product `Int × MachineWidth<64>`; substrate spelling is the parametric `Compose<concept, MachineConstraint>`. **Distinction (per claude review observation)**: the *elaboration* of a particular `Compose<Int, MachineWidth<64>>` term is parser/elaborator behavior; the **interaction substrate** (composition/projection/coercion machinery operating *on* such Compose terms) is what's `.dag`-generated per sub-decision 2 — not the `Compose<...>` *type itself*. S3 worker brief should preserve this distinction.
4. **Approximate-algebra layering**: algebra-side approximation (`Real = ApproximateField<Rational>`) and machine-side approximation (`MachineWidth<64>`) stay as independent axes that compose. `Real<64>` = `Compose<Real, MachineWidth<64>>` carries both layers explicitly per S8's named-axiom-relaxation discipline (the algebra-side approximation is internal to `Real`'s definition; the machine-side approximation is the second slot).
5. **Demonstration breadth — NOT a target** (Brian directive 2026-05-06: *"3 is not a target, we shouldn't be 'targeting' modeling, we are just doing our best job to faithfully represent the concepts"*). The 3-pair demonstration (`Int<64>` / `Real<64>` / `Nat<8>`) is the **minimum existence proof** that the substrate carries the concept faithfully. **Faithful representation of the concept is the closure criterion**; pair-counting is not. Once the parser handles generic interaction syntax + the substrate carries the algebra+machine separation, all valid pairs work by construction. Closure-gate predicate phrasing should reflect "concept is faithfully modeled" not "≥3 pairs land".
6. **Target-specificity — universal substrate, faithful target lowering** (Brian directive 2026-05-06 elaborated): `MachineConstraint<C>` is **universal substrate** — every target carries machine-constraint facts as substrate. Targets lacking native machine-width semantics handle lowering by **faithfully representing the concept in a target-available primitive**, NOT by omission. For Python u8: lower to `numpy.uint8` / `ctypes.c_uint8` / explicit literal-bits via `int & 0xFF` discipline — pick whichever Python idiom faithfully carries the 8-bit-natural-number concept. The substrate stays universal; Grounding handles per-target faithful-lowering selection. *Brian framing: "if python lacks — we would have to actually represent the struct using something that python faithfully provides — i.e. either literal bits or otherwise."* Faithful representation > target-conditioned omission.
6. **Target-specificity — universal faithful representation, cost lens as the discriminator** (Brian directive 2026-05-06 elaborated 2x): `MachineConstraint<C>` is **universal substrate** — every target carries machine-constraint facts as substrate. **Universality of faithful representation** (Brian directive 2026-05-06: *"in all cases we should be able to represent the structure with literal bits/objects or whatever — the cost would be enormous — in those cases, we would look for alternatives like better modeling/libraries/int & 0xFF"*): every target language CAN faithfully represent every concept; literal-bits / direct-object construction is always available as the floor (universal but expensive). **The cost lens (T-CostLens-Composition) is the discriminator** that orders the faithful-representation alternatives by per-primitive realization cost: `cost_lens_reads_target_realization` reads the target language spec's per-primitive realization cost; `coercion_cost_equals_complexity_by_construction` makes "the choice between faithful representations IS the cost-lens application" structural-not-conventional. **Grounding selects the lowest-cost faithful representation** per target by reading the cost lens output. For Python u8: cost-tier 1 = `numpy.uint8` (low cost when numpy available; native operations align), cost-tier 2 = `ctypes.c_uint8` (always-available, medium cost), cost-tier 3 = `int & 0xFF` discipline (universal floor, high cost). All three are faithful (carry the 8-bit-natural-number structure); cost lens orders them; Grounding picks tier-1 when available, falls back through tiers as needed. **Faithful representation > target-conditioned omission** AND **cost lens > heuristic-or-bridge selection**.

**Implication for `docs/design-numeric-construction.md:194-198`**: that doc's existing Python row (`Nat<N>` for any N → Python `int` with "size hint informs runtime checks but doesn't change carrier") is **NOT a faithful representation** — it drops the width-structure to opaque metadata; the cost lens cannot read what isn't there. Reframing routes to **T-Numeric-Construction / Grounding lane paydown**: replace the size-hint-on-int row with a **cost-tiered table** of faithful representations (numpy.uint8 / ctypes.c_uint8 / int-and-mask-discipline) so the cost lens reads structural facts, not metadata. Not bundled here per scope; tracked-not-silent and routed to the cost-lens-bearing lane.

**S3 dispatch unblocked on machine-constraint side** (independent of T-Numeric-Construction algebra-side Option A vs B selection per PR #1815 — interaction semantics carries through under either). **Sub-decision 2's `.dag`-generated discipline** means S3 worker brief must specify the interaction substrate as `.dag`-declared with any Rust counterpart generated, not hand-authored.

Expand Down
Loading
Loading