|
3 | 3 | **Status:** TEST-PINNED (in PR, branch `claude/eager-albattani-iufugq`). **Basis:** `ADR-2026-10-20-SIX` §2 (`entries/2026-10-20-six-decisions.md`). |
4 | 4 |
|
5 | 5 | - **Moved:** relalg's rewrite rules to `lance_graph_contract::set_algebra::normalize`, unchanged except absorption. relalg's `normalize` converts `Rel` ↔ `SetExpr` (`Plane(i)` ↔ `Sym(i)`, `Atom` ↔ `Res`) and delegates. `symbolic`, `run`, lowering and the public API are unchanged. The contract stays dependency-free. |
6 | | -- **Absorption** is matched against flattened sibling sets, removing one child at a time against the children still kept. That closes N17 (`ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN`). |
7 | | -- **`Runs`:** sorted, disjoint, half-open intervals with `∩ ∪ ∖`. `complement(universe)` refuses a set that reaches past the universe. |
| 6 | +- **Absorption** is matched against flattened sibling sets, removing one child at a time against the children still kept, in two forms: (1) a member of the dual child is a sibling, or a junction of siblings; (2) a sibling junction's members all occur in the dual child (`x ∨ (x ∧ y)` with `x` itself a conjunction). That closes N17 (`ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN`) for `x` a leaf, an `And` or an `Or`. Form 2 was found by crepe-plan-probe's N17 pin (CI `probe`), which this PR flips to assert the reduction. |
| 7 | +- **`Runs`:** sorted, disjoint, half-open intervals with `∩ ∪ ∖`, each one merge pass, O(n + m). `complement(universe)` refuses a set that reaches past the universe. |
8 | 8 | - **Regression:** the 16 pre-existing relalg tests pass unchanged. 3 tests are new: `conversion_round_trips` plus 2 in `tests/absorption_n17.rs`. |
9 | 9 | - **Disable runs** (commands: `cargo test --manifest-path crates/lance-graph-relalg/Cargo.toml --no-fail-fast` and `cargo test -p lance-graph-contract --lib set_algebra`): |
10 | 10 |
|
11 | 11 | | probe | what breaks | |
12 | 12 | |---|---| |
13 | 13 | | contract `normalize` returns its input | 10 of 14 `rewrites.rs` tests, and both N17 tests in relalg | |
14 | | - | generalized absorption off | only the N17 tests: one in relalg, two in the contract | |
| 14 | + | absorption form 1 off | only the N17 tests: one in relalg, two in the contract | |
| 15 | + | absorption form 2 off | only `absorption_of_a_superset_conjunction` | |
| 16 | + | `max` dropped in the `union` merge | `runs_obey_the_set_laws_against_bitsets` | |
15 | 17 | | absorption on a partial cover (`all` → `any`) | the silence twin, and the bitset differential (an unsound rule) | |
16 | 18 |
|
17 | 19 | - **Scope held:** no joins, gathers, positional addressing, recursion, D-MPS-8 or `graph_hop`. Measures (`Count`/`Sum` on `Runs`) are not in this PR. |
|
0 commit comments