|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | +-- SPDX-License-Identifier: MPL-2.0 |
| 3 | +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | + |
| 5 | +-- EchoSelectiveProjection: the relational-algebra selection/projection |
| 6 | +-- commutativity (the subset case) as an Echo-fibre statement. Closes |
| 7 | +-- echo-types#174's sibling echo-types#176 (consumer: affinescript |
| 8 | +-- db-theory #4, `stdlib/Select.affine`). |
| 9 | +-- |
| 10 | +-- The classical law (Codd): for selection σ_p (predicate-driven row |
| 11 | +-- filter) and projection π_S (column-subset), |
| 12 | +-- |
| 13 | +-- σ_p(π_S(R)) = π_S(σ_p(R)) when p references only columns in S, |
| 14 | +-- σ_p(π_S(R)) ≠ π_S(σ_p(R)) when p references a column NOT in S. |
| 15 | +-- |
| 16 | +-- *Honest level.* "=" between relations is SET equality: same rows. |
| 17 | +-- The Echo formalisation states it as a per-projected-value LOGICAL |
| 18 | +-- equivalence `_⇔_` of the two result fibres (co-membership), which is |
| 19 | +-- exactly set-equality of the result relations. A full `_↔_` (with |
| 20 | +-- round-trips) would additionally require the predicate family to be |
| 21 | +-- proof-irrelevant (`is-prop`); set-equality does not, and `_⇔_` is the |
| 22 | +-- faithful level. See the companion remark. |
| 23 | +-- |
| 24 | +-- *The column-safe condition.* "p references only columns in S" is |
| 25 | +-- formalised as: p factors through the projection — there is a |
| 26 | +-- predicate `q : S → Set` on the projected columns with `p b ⇔ q |
| 27 | +-- (projection b)` for every record `b`. This `factors` field IS the |
| 28 | +-- "uses only columns in S" hypothesis. |
| 29 | +-- |
| 30 | +-- *The Echo content.* With `pf = projection ∘ f` (the projected map), |
| 31 | +-- `Echo pf s` is π_S(R) at projected value `s` — the rows projecting to |
| 32 | +-- `s`. The two composites: |
| 33 | +-- |
| 34 | +-- ProjectSelect s = Σ (Echo pf s) (λ e → p (f (proj₁ e))) |
| 35 | +-- -- π_S(σ_p(R)) at s: rows projecting to s that satisfy p |
| 36 | +-- SelectProject s = Σ (Echo pf s) (λ _ → q s) |
| 37 | +-- -- σ_q(π_S(R)) at s: rows projecting to s, kept iff q holds at s |
| 38 | +-- |
| 39 | +-- `select-project-commute` is `∀ s → ProjectSelect s ⇔ SelectProject s`. |
| 40 | +-- The proof is K-free: pattern-matching the fibre witness `pf x ≡ s` as |
| 41 | +-- `refl` (s a free variable, so --without-K-safe) collapses the |
| 42 | +-- transport, and the predicate move is exactly the `factors` field. |
| 43 | +-- |
| 44 | +-- *The counterexample.* `no-column-safe-lift` shows a predicate that |
| 45 | +-- reads a projected-away column (`proj₂`, with projection `= proj₁`) |
| 46 | +-- admits NO column-restricted lift `q` at all: the records `(true,true)` |
| 47 | +-- and `(true,false)` share projection `true` but disagree on the |
| 48 | +-- predicate, so any `q true` would be both inhabited and empty. This is |
| 49 | +-- the "≠" direction: σ and π do not commute for such a predicate. |
| 50 | +-- |
| 51 | +-- Headlines (pinned in Smoke.agda): |
| 52 | +-- * SelectiveProjection -- the column-safe setup record |
| 53 | +-- * select-project-commute -- σ–π commute (column-safe), per s |
| 54 | +-- * column-safe-example -- worked column-safe instance |
| 55 | +-- * no-column-safe-lift -- counterexample (non-column-safe ⇒ ✗) |
| 56 | + |
| 57 | +module EchoSelectiveProjection where |
| 58 | + |
| 59 | +open import Echo using (Echo) |
| 60 | +open import Data.Product.Base using (Σ; _,_; proj₁; proj₂; _×_) |
| 61 | +open import Data.Bool.Base using (Bool; true; false) |
| 62 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 63 | +open import Relation.Nullary using (¬_) |
| 64 | + |
| 65 | +---------------------------------------------------------------------- |
| 66 | +-- Logical equivalence (set-equality level). Kept local and minimal — |
| 67 | +-- the σ–π law is co-membership of the two result relations, not a |
| 68 | +-- structure-carrying bijection. |
| 69 | +---------------------------------------------------------------------- |
| 70 | + |
| 71 | +record _⇔_ (P Q : Set) : Set where |
| 72 | + constructor equiv |
| 73 | + field |
| 74 | + to : P → Q |
| 75 | + from : Q → P |
| 76 | + |
| 77 | +---------------------------------------------------------------------- |
| 78 | +-- The column-safe selection/projection setup. |
| 79 | +---------------------------------------------------------------------- |
| 80 | + |
| 81 | +record SelectiveProjection {A B : Set} (f : A → B) (S : Set) : Set₁ where |
| 82 | + field |
| 83 | + projection : B → S -- π_S |
| 84 | + p : B → Set -- σ predicate on full records |
| 85 | + q : S → Set -- its restriction to the projected columns |
| 86 | + -- "p uses only columns in S": p factors through projection as q. |
| 87 | + factors : ∀ b → p b ⇔ q (projection b) |
| 88 | + |
| 89 | + -- The projected map; `Echo pf s` = π_S(R) at projected value s. |
| 90 | + pf : A → S |
| 91 | + pf a = projection (f a) |
| 92 | + |
| 93 | + -- π_S(σ_p(R)) at s : rows projecting to s that satisfy p. |
| 94 | + ProjectSelect : S → Set |
| 95 | + ProjectSelect s = Σ (Echo pf s) (λ e → p (f (proj₁ e))) |
| 96 | + |
| 97 | + -- σ_q(π_S(R)) at s : rows projecting to s, kept iff q holds at s. |
| 98 | + SelectProject : S → Set |
| 99 | + SelectProject s = Σ (Echo pf s) (λ _ → q s) |
| 100 | + |
| 101 | +---------------------------------------------------------------------- |
| 102 | +-- σ–π commute (column-safe): the two result relations co-inhabit at |
| 103 | +-- every projected value. Set-equality of σ_p(π_S(R)) and π_S(σ_p(R)). |
| 104 | +---------------------------------------------------------------------- |
| 105 | + |
| 106 | +select-project-commute : |
| 107 | + ∀ {A B : Set} {f : A → B} {S : Set} (sp : SelectiveProjection f S) (s : S) → |
| 108 | + SelectiveProjection.ProjectSelect sp s ⇔ SelectiveProjection.SelectProject sp s |
| 109 | +select-project-commute {f = f} sp s = equiv to from |
| 110 | + where |
| 111 | + open SelectiveProjection sp |
| 112 | + to : ProjectSelect s → SelectProject s |
| 113 | + to ((x , refl) , pe) = (x , refl) , _⇔_.to (factors (f x)) pe |
| 114 | + from : SelectProject s → ProjectSelect s |
| 115 | + from ((x , refl) , qs) = (x , refl) , _⇔_.from (factors (f x)) qs |
| 116 | + |
| 117 | +---------------------------------------------------------------------- |
| 118 | +-- Worked column-safe instance: 2-column Bool records, project to |
| 119 | +-- column 0, predicate "column 0 is true" — uses only the projected |
| 120 | +-- column, so it factors (the identity equivalence). |
| 121 | +---------------------------------------------------------------------- |
| 122 | + |
| 123 | +column-safe-example : SelectiveProjection {Bool × Bool} {Bool × Bool} (λ b → b) Bool |
| 124 | +column-safe-example = record |
| 125 | + { projection = proj₁ |
| 126 | + ; p = λ b → proj₁ b ≡ true |
| 127 | + ; q = λ s → s ≡ true |
| 128 | + ; factors = λ b → equiv (λ z → z) (λ z → z) |
| 129 | + } |
| 130 | + |
| 131 | +---------------------------------------------------------------------- |
| 132 | +-- Counterexample (the "≠" direction): a predicate reading a |
| 133 | +-- projected-away column has NO column-restricted lift. `(true,true)` |
| 134 | +-- and `(true,false)` share projection `true` but disagree on |
| 135 | +-- `proj₂ · ≡ true`, so any candidate `q true` is both inhabited and |
| 136 | +-- empty. Hence σ and π do not commute for such a predicate. |
| 137 | +---------------------------------------------------------------------- |
| 138 | + |
| 139 | +no-column-safe-lift : |
| 140 | + ¬ Σ (Bool → Set) (λ q → ∀ b → (proj₂ b ≡ true) ⇔ q (proj₁ b)) |
| 141 | +no-column-safe-lift (q , fac) |
| 142 | + with _⇔_.from (fac (true , false)) (_⇔_.to (fac (true , true)) refl) |
| 143 | +... | () |
| 144 | + |
| 145 | +---------------------------------------------------------------------- |
| 146 | +-- Companion remark. |
| 147 | +-- |
| 148 | +-- `_⇔_` (set-equality of the result relations) is the faithful level: |
| 149 | +-- relational-algebra equality is membership equality. Upgrading to a |
| 150 | +-- structure-preserving `_↔_` would need the predicate family to be |
| 151 | +-- proof-irrelevant (an `is-prop (p b)` field); under `--safe |
| 152 | +-- --without-K` that is an extra hypothesis, not free, and it adds no |
| 153 | +-- relational-algebra content. NOT claimed: σ–π commutativity for |
| 154 | +-- arbitrary (non-column-safe) predicates (refuted by |
| 155 | +-- `no-column-safe-lift`); any runtime query-planner behaviour (the |
| 156 | +-- decision of whether a predicate is column-safe lives in the |
| 157 | +-- consumer). The carrier encodes only the property. |
| 158 | +---------------------------------------------------------------------- |
| 159 | + |
| 160 | +NotProved-arbitrary-predicate-commute : Set |
| 161 | +NotProved-arbitrary-predicate-commute = Bool |
| 162 | + |
| 163 | +NotProved-runtime-query-planner : Set |
| 164 | +NotProved-runtime-query-planner = Bool |
0 commit comments