-
Notifications
You must be signed in to change notification settings - Fork 1
fix: resolve B-0357 ID collision #2263
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
151 changes: 151 additions & 0 deletions
151
docs/backlog/P1/B-0367-first-class-uncertainty-semiring-parameterized-weight.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,151 @@ | ||
| --- | ||
| id: B-0367 | ||
| priority: P1 | ||
| status: open | ||
| title: "First-class uncertainty — semiring-parameterized weight type for DBSP" | ||
| effort: L | ||
| created: 2026-05-09 | ||
| last_updated: 2026-05-09 | ||
| depends_on: [] | ||
| classification: research | ||
| decomposition: atomic | ||
| owners: [algebra-owner] | ||
| type: feature | ||
| tags: [algebra, uncertainty, semiring, bayesian, inference, openspec] | ||
| --- | ||
|
|
||
| # B-0357 — First-class uncertainty in DBSP | ||
|
|
||
|
|
||
| ## What | ||
|
|
||
| Parameterize the DBSP weight type so the same circuit | ||
| topology can run over different semirings — integer (current), | ||
| probabilistic, Gaussian, interval, provenance. Uncertainty | ||
| becomes a first-class property of every query result, not | ||
| an afterthought bolted on top. | ||
|
|
||
| ## Why | ||
|
|
||
| The OpenSpec compiler needs to produce specs that carry | ||
| uncertainty through the compilation chain. A spec that | ||
| says "this query returns rows" is weaker than one that | ||
| says "this query returns rows with confidence 0.87." | ||
| Without first-class uncertainty, the OpenSpec → formal spec | ||
| → F# pipeline can only express exact results — it can't | ||
| compile the "how sure are we?" question. | ||
|
|
||
| This is also the bridge to the Infer.NET BP/EP direction | ||
| from AGENDA.md: belief propagation IS incremental Bayesian | ||
|
|
||
| inference, which IS DBSP over a probabilistic semiring. | ||
| Same circuit, different weight type. | ||
|
|
||
| ## The algebra | ||
|
|
||
| DBSP operators (D, I, z⁻¹) are linear over the weight | ||
| semiring. Current: (Z, +, ×) — the integer ring. The | ||
| generalization: | ||
|
|
||
| ``` | ||
| ZSet<'K, 'W when 'W : ISemiring> | ||
| where ISemiring provides: | ||
| zero: 'W | ||
| add: 'W -> 'W -> 'W | ||
| mul: 'W -> 'W -> 'W | ||
| (optionally) negate: 'W -> 'W // ring, not just semiring | ||
| ``` | ||
|
|
||
| Candidate weight types: | ||
|
|
||
| | Semiring | Weight | Answers | Ring? | | ||
| |---|---|---|---| | ||
| | Integer (current) | int64 | multiplicity + retraction | yes | | ||
|
Comment on lines
+59
to
+61
|
||
| | Boolean | bool | exists? | no | | ||
| | Tropical | (float, min, +) | shortest path / confidence | no | | ||
| | Probabilistic | [0,1] | how likely? | no | | ||
| | Gaussian | (μ, σ²) | estimate + uncertainty | yes | | ||
| | Interval | [lo, hi] | bounded uncertainty | yes | | ||
| | Provenance | polynomial | which inputs contributed? | yes | | ||
|
|
||
| ## Key design decisions | ||
|
|
||
| 1. **Ring vs semiring**: retraction (negative weights) | ||
| requires a ring (additive inverse). Pure semirings | ||
| (boolean, tropical, probabilistic) don't support | ||
| retraction — they'd need the counting variant or | ||
| a different fixpoint strategy. | ||
|
|
||
| 2. **Distinct operator**: currently clamps to {0, 1}. | ||
| Under probabilistic weights, becomes a threshold | ||
| operator (clamp below cutoff to zero). Under | ||
| Gaussian, becomes a significance test. | ||
|
|
||
| 3. **Semi-naive optimization**: requires subtraction | ||
| (Δ = new - old). Non-ring semirings need the | ||
| RecursiveCounting variant or a different incremental | ||
| strategy. | ||
|
|
||
| 4. **Performance**: generic weight dispatch vs | ||
| specialized paths. The integer path must not regress. | ||
|
|
||
| ## Prior art | ||
|
|
||
| - Green, Karvounarakis, Tannen 2007 "Provenance | ||
| Semirings" (PODS) — the foundational framework | ||
| - Budiu et al. 2022 "DBSP" — Z-ring instantiation | ||
| - Infer.NET — Bayesian inference as message passing | ||
| (the EP/BP direction from AGENDA.md) | ||
|
|
||
| - Reaqtor — standing queries with checkpoint (the | ||
| durability layer for streaming inference) | ||
|
|
||
| ## What exists in Zeta today | ||
|
|
||
| - `src/Core/ZSet.fs` — hardcoded `Weight = int64` | ||
| - `src/Bayesian/BayesianAggregate.fs` — Bayesian | ||
| aggregation but external to the weight algebra | ||
| - `src/Core/NovelMath.fs` — tropical semiring work | ||
| (non-integer semiring already explored) | ||
| - `src/Core/Algebra.fs` — algebraic laws, currently | ||
| integer-specific | ||
|
|
||
| ## Acceptance criteria | ||
|
|
||
| - [ ] `Weight` type is generic with ISemiring constraint | ||
| - [ ] Integer path performance unchanged (zero regression) | ||
| - [ ] At least one non-integer semiring compiles and | ||
| passes a smoke test (Gaussian or Interval) | ||
| - [ ] OpenSpec can express uncertainty in spec output | ||
| - [ ] Z3 lemmas generalize to semiring axioms | ||
|
|
||
| ## Composes with | ||
|
|
||
| - OpenSpec compiler (the motivation — specs need uncertainty) | ||
| - Infer.NET BP/EP direction (belief propagation = DBSP | ||
| over probabilistic semiring) | ||
| - `src/Bayesian/` (absorbs into the weight algebra) | ||
| - Tropical semiring work in `NovelMath.fs` | ||
| - The Superfluid reactor equation (uncertainty in the | ||
| learning gain term) | ||
|
|
||
| ## Prior art — time-uncertainty in production databases | ||
|
|
||
| Aaron 2026-05-09: "lookup spanner and cockroach db real db | ||
| primitives of time and lamport include uncertainty measurement | ||
| on the datetime" + "there is tidb we should research this | ||
| actually and decide if we want to support multiple and make | ||
| it pluggable." | ||
|
|
||
| | System | Timestamp model | Uncertainty primitive | | ||
| |---|---|---| | ||
| | Spanner | TrueTime (GPS + atomic) | `[earliest, latest]` interval; commit-wait | | ||
| | CockroachDB | HLC (Lamport + wall-clock) | Read uncertainty restart window | | ||
| | TiDB | TSO (centralized oracle) | Single-point, no interval | | ||
|
Comment on lines
+137
to
+141
|
||
| | YugabyteDB | HLC variant | Similar to CockroachDB | | ||
|
|
||
| Lamport's logical clocks → Spanner's TrueTime intervals → | ||
| Zeta's weight semiring intervals. Three instantiations of | ||
| "carry uncertainty, don't pretend precision." | ||
|
|
||
| **Research question:** should Zeta parameterize the | ||
| time-uncertainty model (pluggable, like the weight | ||
| semiring) so it works over any of these backends? Or | ||
| hardcode one model? | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This change adds
B-0367as a new file but leavesdocs/backlog/P1/B-0357-first-class-uncertainty-semiring-parameterized-weight.mdin place, so the same backlog item now exists twice with identical content/title under different IDs. Because backlog automation enumerates everydocs/backlog/P*/B-*.mdfile, this creates duplicate planning entries and still leaves the originalB-0357collision unresolved againstB-0357-replace-tautology-z3-agenda-proofs-with-real-verification.md.Useful? React with 👍 / 👎.