Repository navigation
contract: normalize_kleene returns WhereSet (WHERE-terminal only); GKAT Where/Check negation duality pinned - #1687
Conversation
…AT negation duality pinned Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA
|
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 |
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. |
This PR covers item C of the post-merge review of #1677 and #1679 (
GPT:gpt-ada-01/20261021-pr1674-1682-consolidated-review-01). I took it on the operator's instruction (EXO-50/038). The original owners are session 01G22y (normalize_kleene) and session 01Vnc (GKAT); the operator aligns afterwards.C1. WHERE-preserving is not three-valued equivalent
The problem. #1677 measured that
normalize_kleenekeeps the TRUE rows but moves FALSE rows on 337 of 2000 expressions. Before this PR, the function returned a plainSetExpr, so callers could reuse the result underNOT.The change.
normalize_kleenenow returnsset_algebra::WhereSet, a newtype whose field is private.where_true()orinto_where_true(). Either name states the WHERE-only restriction at the call site.normalize_withis private, so the Kleene result cannot leave the module as a plainSetExpr.set_rules'SetNormalize, whose measure is terminal;k3_pg_parity.rs;k3_where_pg_parity.rs.Semantics::truthgate is unchanged.The new test
the_kleene_form_preserves_true_rows_but_not_false_rowsusesp AND NOT pwithpUNKNOWN:Empty;NOTover the result is TRUE, whereasNOT (p AND NOT p)is UNKNOWN.C2. GKAT projection and negation
Cond::Notnegates a guard that has already been projected. The newtests/k3_negation_duality.rschecks all four atoms (TRUE, FALSE, and NULL under both payloads), comparing each side against the SQL meaning rather than against the other side:Where(NOT p) = NOT Check(p);Check(NOT p) = NOT Where(p);NOT Where(p)differs from SQLWHERE NOT pexactly on the two NULL atoms;Disable runs: two, both red. One drops the validity test from
Where, the other fromCheck.The GKAT algorithm is unchanged; the module docs in
flow.rsnow name this boundary.Evidence
cargo check --workspace --all-targetspasses.-D warningsis clean for contract, quack and gkat-probe, and fmt is clean.k3_pg_parity: 2000/2000.k3_where_pg_parity: TRUE and FALSE rows equal on 2000/2000, FALSE rows moved on 337, two-valuednormalizewrong on 499.entries/2026-10-21-d-rft-0-kleene-normalization.md. The entries index and the supersession index regenerate unchanged.API change:
normalize_kleene's return type changes, andnormalize_withbecomes private. I found no callers outside the three files above (checked across the AdaWorldAPI sibling repos in this container).I will not merge this PR; it waits for your review.
Generated by Claude Code