Repository navigation
D-RFT-0 / D-QSP-0: Kleene form of set normalization (SQL NULL), PostgreSQL differential - #1668
Merged
Merged
Conversation
`set_algebra::normalize` is two-valued. A union that covers a lane becomes `All`, and a conjunct that covers a lane disappears. On a NULL row both promote UNKNOWN to TRUE. PostgreSQL 16 keeps 1 of the rows `(1), (NULL)` for `WHERE x < 5 OR x >= 5`; `All` keeps both. That is why `set_rules::SetNormalize` refused every rewrite under `Truth::ThreeValued`. `normalize_kleene` (and `normalize_with(e, Logic)`) changes only those cases: - a covered I32 lane becomes `x >= i32::MIN`, which is TRUE exactly on the non-NULL rows; - a covered U32 lane keeps its atoms. Every other rewrite keeps the rows where the expression is TRUE under Kleene logic. Two-valued `normalize` is unchanged; relalg's 8 test suites still pass. `SetNormalize` under three-valued semantics now applies the Kleene form instead of refusing. The Complement and RelationalDifference guards are unchanged. Tests: - an independent Kleene evaluator over 3000 random expressions with NULL lanes, plus its twin showing the two-valued form wrong on some of the same inputs; - the six lane covers one at a time; - a catalogue differential over 600 three-valued measures, all rules. Re-pinned: the two experiment-E tests that asserted `SetNormalize` → `NotTwoValued` now assert the rewrite and the unchanged count. Example `k3_pg_parity` (PostgreSQL 16.14, 2000 expressions × 200 rows): - as written = Kleene oracle = normalize_kleene on 2000/2000 (1537 rewritten); - two-valued normalize is wrong on 474. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
…s (docs) - entries/2026-10-21-d-rft-0-kleene-normalization.md: the defect, the precise fix, the PostgreSQL differential and 5 disable runs. - entries/2026-10-21-d-rft-d-lfa-0-assessment.md: the smallest falsifiable D-RFT-1..5 sequence, the rs-graph-llm copy-versus-reuse census with the Rubicon mapping, and the physical-shape proof plan. PROPOSAL; nothing in it is measured. - STATUS_BOARD: new D-RFT / D-QSP section. LATEST_STATE: contract inventory delta. entries index regenerated. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configuration
Warning Billing warning: we have not been able to collect payment for this subscription for more than 72 hours. Please update the payment method or pay any pending invoices in Billing to avoid service interruption. Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
AdaWorldAPI
marked this pull request as ready for review
October 21, 2026 18:58
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 82e937499e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
psql answers while it reads, so writing the whole script before draining stdout blocks once the stdout pipe fills (Codex review on #1668). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
…p; egglog/datafrog/Ascent evaluation Exploration map (ADOPT-NOW/PROBE/PARK/SKIP, nothing adopted): reconciled D-RFT ID table, stratum/carrier/equality declaration per step, 12 named count-fold probes, the Semijoin ADMISSION B gap and the oracle-scope question. Two companion entries: the PostgreSQL construct map onto the ClassView polyfill surfaces, and the three-engine evaluation. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 21, 2026
#1668's co-research entry led with 'D-QSP / D-RFT / D-LFA', so the index derived the same id as #1667's plan entry, and the index on main was regenerated before the merge brought in a 420th entry. Retitle the entry and regenerate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 21, 2026
Operator-approved amendment after #1670: - D-LFA-1: a structured Rubicon reference flow and an optimized variant are GKAT-equivalent (same actions, declared guards and projections), plus a separate trace check that RequestCommit never occurs without a valid revision and MUL authorization. RequestCommit is an intent, not a Lance write. Three disable runs; GoTo/GoBack refused; WaitForInput is an observation at resume; the snapshot/codebook generation gate stays independent. - Guard projection: WHERE {T} vs CHECK {T,U} declared per guard, never interchanged; commit authorization never inherits CHECK semantics. - D-LFA-2: integration with graph-flow, thought-git verbs, Kanban transitions and authorized proposals against the from-scratch oracle; no second scheduler, evaluator, state store or commit owner. - D-GKAT-0: independent, unclaimed fixture probe (G1, G2, G5); no runtime, dependency or executor. D-RFT-2 unchanged; D-RFT-4 keeps thought binding/frontier. Co-research map: D-GKAT-0 and P-GKAT-RUBICON probe rows. STATUS_BOARD: D-RFT-0 shipped (#1668); D-LFA-1/2 and D-GKAT-0 rows. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
What
Implements D-RFT-0 / D-QSP-0 from the #1667 plans (claim: EXO-50
session_01G22yT6htkcdyXsihxxXdrg/031). #1667 is unchanged and stays the planning reference.The defect.
contract::set_algebra::normalizeis two-valued: a union that covers a lane becomesAll, and a whole-lane conjunct disappears. On a NULL row, both turn UNKNOWN into TRUE.PostgreSQL 16.14:
SELECT count(*) FROM (VALUES (1),(NULL)) v(x) WHERE x<5 OR x>=5returns 1;Allwould count 2. Because of this,set_rules::SetNormalizerefused every rewrite underTruth::ThreeValued.The fix. It is precise rather than a blanket refusal:
set_algebra::{Logic, normalize_kleene, normalize_with}. In Kleene mode:I32lane becomesx >= i32::MIN, which is TRUE exactly on the non-NULL rows (an existingRes, no new vocabulary);U32lane keeps its atoms;normalizeis unchanged. relalg's 8 suites pass.SetNormalizeunderThreeValuednow applies the Kleene form.ComplementandRelationalDifferencestill refuse.Filter::sql_whereis already correct and is not touched.Evidence
examples/k3_pg_parity.rs, PostgreSQL 16.14, 2000 exprs × 200 rowsnormalize_kleeneon 2000/2000 (1537 rewritten); two-valued wrong on 474-D warnings, Rust 1.99.0Disable runs, each red on its named test:
All;All;SetNormalizeuses the two-valued form;!=. This one was green at first; it is now pinned bynormalize_kleene_never_grows_leaf_count.Re-pinned: the experiment-E test that asserted
SetNormalize → NotTwoValuednow asserts the Kleene rewrite and the unchanged count. The example skips withSKIPwithout a PostgreSQL server, so CI does not depend on one.Also in this PR (docs only)
entries/2026-10-21-d-rft-d-lfa-0-assessment.md:lance-graph-flowcopy-versus-reuse census, with the Rubicon mapping and a falsifier;It is a PROPOSAL with no measurements, and it claims none of those D-ids.
Open
Symis assumed two-valued underThreeValued(contract statement).NOT IN (…, NULL),COALESCE, nullable arithmetic, empty/all-NULLSUM,COUNT(expr).Do not merge automatically.
Generated by Claude Code