diff --git a/.claude/board/entries/2026-10-21-d-rft-0-kleene-normalization.md b/.claude/board/entries/2026-10-21-d-rft-0-kleene-normalization.md index 2533e7376..158c2e9b4 100644 --- a/.claude/board/entries/2026-10-21-d-rft-0-kleene-normalization.md +++ b/.claude/board/entries/2026-10-21-d-rft-0-kleene-normalization.md @@ -68,3 +68,12 @@ Without a server the example prints `SKIP` and exits 0. - empty / all-NULL `SUM` (the `SumFamily::Sym` path exists; no PostgreSQL differential yet); - `COUNT(expr)` vs `COUNT(*)`. - **Not done:** a PostgreSQL arm in CI. The example is a lab instrument only. + +## Correction: WHERE-terminal admission (post-merge review) + +Written by `session_013z2e1YXkm6o6HNrDn5BPWA` on the operator's instruction (EXO-50 `/038`), from `GPT:gpt-ada-01/20261021-pr1674-1682-consolidated-review-01` item 3. + +- `normalize_kleene` keeps the TRUE rows only; #1677 measured FALSE rows moving on 337/2000. It now returns `set_algebra::WhereSet` instead of a `SetExpr`. `where_true()` / `into_where_true()` name the WHERE-only restriction at every call site; `normalize_with` is private, so the Kleene result cannot leave the module as a plain `SetExpr`. `set_rules`' `SetNormalize` (a measure, terminal) and the two PostgreSQL examples take the set out explicitly. No new rule or framework; the existing `Semantics::truth` gate is unchanged. +- Test `the_kleene_form_preserves_true_rows_but_not_false_rows`: `p ∧ ¬p` with `p` UNKNOWN keeps its (empty) TRUE rows, becomes `Empty`, and `NOT` over it is TRUE where `NOT (p ∧ ¬p)` is UNKNOWN. +- GKAT (#1679): `Cond::Not` negates a projected guard. `tests/k3_negation_duality.rs` checks on all four atoms (TRUE, FALSE, NULL under both payloads) that `Where(NOT p) = NOT Check(p)`, `Check(NOT p) = NOT Where(p)`, that `NOT Where(p)` differs from SQL `WHERE NOT p` exactly on the two NULL atoms, and that no form reads a NULL payload. Two disables red (`Where` or `Check` without the validity test). The GKAT algorithm is unchanged; `flow.rs` docs name the boundary. +- Unchanged after the change: contract 1626 tests pass; `k3_pg_parity` 2000/2000; `k3_where_pg_parity` TRUE/FALSE equal 2000/2000, FALSE moved on 337, two-valued wrong on 499. diff --git a/crates/gkat-probe/src/flow.rs b/crates/gkat-probe/src/flow.rs index e35605162..46d740dc2 100644 --- a/crates/gkat-probe/src/flow.rs +++ b/crates/gkat-probe/src/flow.rs @@ -43,6 +43,13 @@ //! //! A Boolean observable is read with [`Cond::Is`]. Using a K3 projection on a //! Boolean observable, or `Is` on a K3 one, is refused. +//! +//! [`Cond::Not`] negates a guard AFTER projection; there is no SQL `NOT` +//! before projection in this language. The two meet through +//! `Where(NOT p) = NOT Check(p)` and `Check(NOT p) = NOT Where(p)`, so +//! `Cond::Not(Where(p))` is SQL `CHECK(NOT p)`, not `WHERE NOT p`; a +//! translator that lowers SQL `WHERE NOT p` must emit +//! `Cond::Check(p).negated()` (`tests/k3_negation_duality.rs`). use crate::expr::{Action, Atoms, BExp, Exp, Refusal}; diff --git a/crates/gkat-probe/tests/k3_negation_duality.rs b/crates/gkat-probe/tests/k3_negation_duality.rs new file mode 100644 index 000000000..c36a57686 --- /dev/null +++ b/crates/gkat-probe/tests/k3_negation_duality.rs @@ -0,0 +1,87 @@ +//! The SQL-negation / projection boundary of the K3 encoding (#1679). +//! +//! `Cond::Not` is Boolean negation of a guard that is already projected. SQL +//! `NOT` acts on the K3 value before projection. With `Where(p) = valid ∧ leaf` +//! and `Check(p) = ¬valid ∨ leaf` the two meet only through the duality +//! +//! * `Where(NOT p) = NOT Check(p)` +//! * `Check(NOT p) = NOT Where(p)` +//! +//! so `Cond::Not(Where(p))` is SQL `CHECK(NOT p)`, never SQL `WHERE NOT p`; +//! they differ exactly where `p` is UNKNOWN. Checked on all four atoms of one +//! observable: TRUE `(1,1)`, FALSE `(0,1)`, and NULL under both payloads. + +use gkat_probe::Atom; +use gkat_probe::flow::{Cond, Kind, Signature}; + +const P: &str = "p"; + +fn sig() -> Signature { + Signature { + observables: vec![(P, Kind::K3)], + actions: vec![], + } +} + +/// (leaf, valid) bits: test 0 is the leaf, test 1 its validity. +const T: Atom = Atom(0b11); +const F: Atom = Atom(0b10); +const NULL_0: Atom = Atom(0b00); +const NULL_1: Atom = Atom(0b01); +const ATOMS: [Atom; 4] = [T, F, NULL_0, NULL_1]; + +/// SQL semantics of the K3 value of `p` on an atom: `None` is UNKNOWN. +fn k3(a: Atom) -> Option { + a.holds(1).then(|| a.holds(0)) +} + +fn eval(c: Cond) -> [bool; 4] { + let g = sig().guard(&c).expect("guard"); + ATOMS.map(|a| g.eval(a)) +} + +/// FAILS IF: the translator's negation is taken for SQL negation, or a +/// projection reads a NULL payload. Each side is compared with the SQL +/// meaning computed from `k3`, not with the other side. +#[test] +fn negating_a_projection_is_the_dual_projection_of_the_sql_negation() { + // SQL meanings, per atom. + let where_not_p = ATOMS.map(|a| k3(a).map(|b| !b) == Some(true)); + let check_not_p = ATOMS.map(|a| k3(a).map(|b| !b) != Some(false)); + assert_eq!(where_not_p, [false, true, false, false]); + assert_eq!(check_not_p, [false, true, true, true]); + + // The only spellings of the SQL forms in the flow language. + assert_eq!( + eval(Cond::Check(P).negated()), + where_not_p, + "Where(NOT p) = NOT Check(p)" + ); + assert_eq!( + eval(Cond::Where(P).negated()), + check_not_p, + "Check(NOT p) = NOT Where(p)" + ); + + // Boolean NOT of WHERE is not SQL WHERE NOT: they differ on both NULL atoms + // and nowhere else. + let not_where = eval(Cond::Where(P).negated()); + let differs: Vec = ATOMS + .iter() + .zip(not_where.iter().zip(where_not_p.iter())) + .filter(|(_, (a, b))| a != b) + .map(|(atom, _)| *atom) + .collect(); + assert_eq!(differs, vec![NULL_0, NULL_1]); + + // Payload blindness under NULL, for every form above. + for c in [ + Cond::Where(P), + Cond::Check(P), + Cond::Where(P).negated(), + Cond::Check(P).negated(), + ] { + let v = eval(c.clone()); + assert_eq!(v[2], v[3], "{c:?} reads the payload of a NULL"); + } +} diff --git a/crates/lance-graph-contract/examples/k3_pg_parity.rs b/crates/lance-graph-contract/examples/k3_pg_parity.rs index 5ae63d409..7767dd3df 100644 --- a/crates/lance-graph-contract/examples/k3_pg_parity.rs +++ b/crates/lance-graph-contract/examples/k3_pg_parity.rs @@ -203,7 +203,7 @@ fn main() { "SELECT count(*) FILTER (WHERE {}), count(*) FILTER (WHERE {}), \ count(*) FILTER (WHERE {}) FROM t;\n", sql(e), - sql(&normalize_kleene(e)), + sql(normalize_kleene(e).where_true()), sql(&normalize(e)) )); } @@ -257,7 +257,7 @@ fn main() { assert_eq!(n[1], n[0], "normalize_kleene changed the count: {e:?}"); kleene_ok += 1; two_valued_wrong += usize::from(n[2] != n[0]); - rewritten += usize::from(normalize_kleene(e) != *e); + rewritten += usize::from(normalize_kleene(e).where_true() != e); } println!( "PostgreSQL {}: {EXPRS} expressions over {ROWS} rows; as written = Kleene oracle = \ diff --git a/crates/lance-graph-contract/src/set_algebra.rs b/crates/lance-graph-contract/src/set_algebra.rs index 513b49222..8971fae06 100644 --- a/crates/lance-graph-contract/src/set_algebra.rs +++ b/crates/lance-graph-contract/src/set_algebra.rs @@ -70,6 +70,16 @@ //! TRUE). A [`SetExpr::Sym`] is two-valued by definition, so its complement //! rule stays. //! +//! **WHERE-terminal only.** The Kleene form keeps the TRUE rows and nothing +//! else: it may move a row between FALSE and UNKNOWN. `p ∧ ¬p` becomes +//! `Empty`, which is FALSE on a row where `p` is UNKNOWN, so `NOT` over the +//! result selects that row while `NOT (p ∧ ¬p)` does not (PostgreSQL agrees; +//! `examples/k3_where_pg_parity.rs` measures it). The result is therefore a +//! [`WhereSet`], not a [`SetExpr`]: a consumer that negates or embeds it must +//! take the set out explicitly with [`WhereSet::into_where_true`], which names +//! the restriction at the call site. A measure (`Count`, `Sum`) and a SQL +//! `WHERE` are terminal and may. +//! //! An interval is always emitted as `<` / `>` bounds or one `==`. //! //! Zero dependencies. @@ -197,13 +207,37 @@ pub fn normalize(e: &SetExpr) -> SetExpr { } /// [`normalize`] for lanes that may hold NULL: the result is TRUE on exactly -/// the rows where `e` is TRUE under Kleene logic (module docs). -pub fn normalize_kleene(e: &SetExpr) -> SetExpr { - normalize_with(e, Logic::Kleene) +/// the rows where `e` is TRUE under Kleene logic (module docs). Its FALSE and +/// UNKNOWN rows are not those of `e`, so it is returned as a [`WhereSet`]. +pub fn normalize_kleene(e: &SetExpr) -> WhereSet { + WhereSet(normalize_with(e, Logic::Kleene)) +} + +/// The result of [`normalize_kleene`]: a set whose TRUE rows are the original +/// expression's TRUE rows under Kleene logic. Its FALSE / UNKNOWN split is +/// not the original's, so it is valid only where a terminal reads TRUE rows +/// (a measure, a SQL `WHERE`), never under `NOT`, inside a `CHECK`, or as an +/// operand of a larger three-valued expression (module docs). +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[must_use] +pub struct WhereSet(SetExpr); + +impl WhereSet { + /// The set, to be read only as "the rows where it is TRUE". + pub fn where_true(&self) -> &SetExpr { + &self.0 + } + + /// Take the set out for a terminal that reads TRUE rows. The caller + /// asserts that nothing negates or embeds it in a three-valued context. + pub fn into_where_true(self) -> SetExpr { + self.0 + } } -/// [`normalize`] under `logic`. -pub fn normalize_with(e: &SetExpr, logic: Logic) -> SetExpr { +/// [`normalize`] under `logic`. Private: the Kleene result must leave this +/// module as a [`WhereSet`]. +fn normalize_with(e: &SetExpr, logic: Logic) -> SetExpr { let mut cur = nnf(e, false); for _ in 0..64 { let next = simplify(&cur, logic); @@ -911,9 +945,13 @@ mod tests { let null = nulls(1 + k % 5); let e = g.expr(5); let want = true_rows(&w, &null, &e); - let n = normalize_kleene(&e); + let n = normalize_kleene(&e).into_where_true(); assert_eq!(true_rows(&w, &null, &n), want, "{e:?}\n => {n:?}"); - assert_eq!(normalize_kleene(&n), n, "not idempotent: {e:?}"); + assert_eq!( + normalize_kleene(&n).into_where_true(), + n, + "not idempotent: {e:?}" + ); changed += usize::from(n != e); two_valued_wrong += usize::from(true_rows(&w, &null, &normalize(&e)) != want); } @@ -972,7 +1010,11 @@ mod tests { for e in &covers { let want = true_rows(&w, &null, e); assert_eq!(want.iter().filter(|&&b| b).count(), N.div_ceil(2), "{e:?}"); - assert_eq!(true_rows(&w, &null, &normalize_kleene(e)), want, "{e:?}"); + assert_eq!( + true_rows(&w, &null, normalize_kleene(e).where_true()), + want, + "{e:?}" + ); assert_ne!(true_rows(&w, &null, &normalize(e)), want, "{e:?}"); } } @@ -1016,11 +1058,14 @@ mod tests { let mut g = Gen(0xB0B); for _ in 0..3000 { let e = g.expr(5); - assert!(normalize_kleene(&e).leaves() <= e.leaves(), "{e:?}"); + assert!( + normalize_kleene(&e).into_where_true().leaves() <= e.leaves(), + "{e:?}" + ); } // The `!=` case on its own: `x != 1` stays one atom. let ne = SetExpr::i32(0, Cmp::Ne, 1); - assert_eq!(normalize_kleene(&ne), ne); + assert_eq!(normalize_kleene(&ne).into_where_true(), ne); } fn x() -> SetExpr { @@ -1201,3 +1246,81 @@ mod tests { assert_eq!(Runs::empty().complement(5).unwrap(), Runs::full(5)); } } + +#[cfg(test)] +mod where_terminal { + use super::*; + + /// Kleene evaluation of the one-lane fixture: `x` is `[3, NULL]`. + fn k(e: &SetExpr, null: bool) -> Option { + match e { + SetExpr::All => Some(true), + SetExpr::Empty => Some(false), + SetExpr::Res(Res::I32 { op, t, .. }) => { + if null { + None + } else { + let x = 3; + Some(match op { + Cmp::Lt => x < *t, + Cmp::Le => x <= *t, + Cmp::Gt => x > *t, + Cmp::Ge => x >= *t, + Cmp::Eq => x == *t, + Cmp::Ne => x != *t, + }) + } + } + SetExpr::Not(c) => k(c, null).map(|b| !b), + SetExpr::And(cs) => { + let vs: Vec> = cs.iter().map(|c| k(c, null)).collect(); + if vs.contains(&Some(false)) { + Some(false) + } else if vs.contains(&None) { + None + } else { + Some(true) + } + } + SetExpr::Or(cs) => k( + &SetExpr::negated(SetExpr::And( + cs.iter().cloned().map(SetExpr::negated).collect(), + )), + null, + ), + _ => unreachable!("fixture uses I32 residuals only"), + } + } + + /// FAILS IF: the Kleene form is claimed to be fully three-valued + /// equivalent. `p ∧ ¬p` keeps its TRUE rows (none) but becomes `Empty`, + /// which is FALSE where `p` is UNKNOWN; so `NOT` over the normalized set + /// selects the NULL row and `NOT` over the original does not. This pins + /// why [`normalize_kleene`] returns a [`WhereSet`]. + #[test] + fn the_kleene_form_preserves_true_rows_but_not_false_rows() { + let p = SetExpr::i32(0, Cmp::Lt, 5); + let e = SetExpr::And(vec![p.clone(), SetExpr::negated(p)]); + let n = normalize_kleene(&e); + assert_eq!(n.where_true(), &SetExpr::Empty); + for null in [false, true] { + assert_eq!( + k(&e, null) == Some(true), + k(n.where_true(), null) == Some(true), + "TRUE rows must agree (null = {null})" + ); + } + // Present row: both FALSE. NULL row: original UNKNOWN, normalized FALSE. + assert_eq!(k(&e, false), Some(false)); + assert_eq!(k(&e, true), None); + assert_eq!(k(n.where_true(), true), Some(false)); + let not_orig = SetExpr::negated(e); + let not_norm = SetExpr::negated(n.into_where_true()); + assert_eq!(k(¬_orig, true), None, "NOT (p AND NOT p) is UNKNOWN"); + assert_eq!( + k(¬_norm, true), + Some(true), + "NOT over the WHERE form is TRUE" + ); + } +} diff --git a/crates/lance-graph-contract/src/set_rules.rs b/crates/lance-graph-contract/src/set_rules.rs index e5627a94a..9a6138ea8 100644 --- a/crates/lance-graph-contract/src/set_rules.rs +++ b/crates/lance-graph-contract/src/set_rules.rs @@ -443,7 +443,8 @@ fn apply(rule: Rule, m: &Measure, sem: &Semantics) -> Option normalize(set), - Truth::ThreeValued => normalize_kleene(set), + // Terminal: a measure reads only the TRUE rows. + Truth::ThreeValued => normalize_kleene(set).into_where_true(), }; if n == *set { return None; diff --git a/crates/lance-graph-quack/examples/k3_where_pg_parity.rs b/crates/lance-graph-quack/examples/k3_where_pg_parity.rs index 1d5af0b8d..4dc8229c8 100644 --- a/crates/lance-graph-quack/examples/k3_where_pg_parity.rs +++ b/crates/lance-graph-quack/examples/k3_where_pg_parity.rs @@ -382,7 +382,7 @@ fn main() { let (tbits, fbits) = line.split_once(',').expect("two columns"); let (pg_t, pg_f) = (plane(tbits), plane(fbits)); unknown_rows += ROWS - tbits.matches('1').count() - fbits.matches('1').count(); - let (f, nk) = (filter(e), filter(&normalize_kleene(e))); + let (f, nk) = (filter(e), filter(normalize_kleene(e).where_true())); for mode in [Mode::InPlace, Mode::Fused] { let neg = Filter::Not(Box::new(f.clone())); assert!( @@ -404,7 +404,7 @@ fn main() { &keep(&t, &Filter::Not(Box::new(nk.clone())), Mode::InPlace), &pg_f, )); - rewritten += usize::from(normalize_kleene(e) != *e); + rewritten += usize::from(normalize_kleene(e).where_true() != e); two_valued_wrong += usize::from(differ( &keep(&t, &filter(&normalize(e)), Mode::InPlace), &pg_t,