|
| 1 | +#+TITLE: Infinite Relations Design |
| 2 | +#+AUTHOR: Nekoma Team |
| 3 | +#+DATE: 2025-01-22 |
| 4 | + |
| 5 | +* Overview |
| 6 | + |
| 7 | +This document specifies the design for infinite relations in Domino, enabling |
| 8 | +countably infinite (ℵ₀) and uncountably infinite (continuum) relations alongside |
| 9 | +finite relations. |
| 10 | + |
| 11 | +** Core Principle |
| 12 | + |
| 13 | +*Everything is a relation.* Types are relations. Functions are relations. |
| 14 | +Numbers are relations. This unifies the type system with the data model. |
| 15 | + |
| 16 | +* Cardinality System |
| 17 | + |
| 18 | +** Cardinality Types |
| 19 | + |
| 20 | +#+BEGIN_SRC erlang |
| 21 | +-type cardinality() :: {finite, non_neg_integer()} % Finite set with N elements |
| 22 | + | aleph_zero % Countably infinite (ℵ₀) |
| 23 | + | continuum. % Uncountably infinite (2^ℵ₀) |
| 24 | +#+END_SRC |
| 25 | + |
| 26 | +** Properties |
| 27 | + |
| 28 | +- Finite relations have explicit tuple count: ={finite, 1000}= |
| 29 | +- Countably infinite relations: =aleph_zero= |
| 30 | +- Uncountably infinite relations: =continuum= |
| 31 | + |
| 32 | +* Extended Data Model |
| 33 | + |
| 34 | +** Modified Relation Record |
| 35 | + |
| 36 | +#+BEGIN_SRC erlang |
| 37 | +-record(relation, { |
| 38 | + hash, % Content hash (for finite) or generator hash (for infinite) |
| 39 | + name, % Relation name (atom) |
| 40 | + tree, % Merkle tree (finite only), undefined for infinite |
| 41 | + schema, % Schema definition |
| 42 | + cardinality, % {finite, N} | aleph_zero | continuum |
| 43 | + generator, % Generator function (infinite only), undefined for finite |
| 44 | + is_function % Boolean: true if relation represents a function |
| 45 | +}). |
| 46 | +#+END_SRC |
| 47 | + |
| 48 | +** Generator Specification |
| 49 | + |
| 50 | +Generators are functions that produce tuples on-demand based on constraints. |
| 51 | + |
| 52 | +#+BEGIN_SRC erlang |
| 53 | +-type generator_spec() :: |
| 54 | + {primitive, atom()} % Built-in: naturals, integers, rationals |
| 55 | + | {function_relation, atom(), arity()} % Built-in function: plus/3, times/3 |
| 56 | + | {custom, fun((constraints()) -> tuple())} % User-defined generator |
| 57 | + | {derived, relational_operation()}. % Derived from other relations |
| 58 | + |
| 59 | +-type constraints() :: #{ |
| 60 | + attribute_name() => constraint_spec() |
| 61 | +}. |
| 62 | + |
| 63 | +-type constraint_spec() :: |
| 64 | + {eq, value()} % Equality: age = 30 |
| 65 | + | {neq, value()} % Inequality: age ≠ 30 |
| 66 | + | {lt, value()} % Less than: age < 30 |
| 67 | + | {lte, value()} % Less than or equal |
| 68 | + | {gt, value()} % Greater than |
| 69 | + | {gte, value()} % Greater than or equal |
| 70 | + | {in, [value()]} % Membership: age in [20,30,40] |
| 71 | + | {range, value(), value()} % Range: age in [20..30] |
| 72 | + | {member_of, relation_name()}. % Type constraint: x ∈ Naturals |
| 73 | +#+END_SRC |
| 74 | + |
| 75 | +* Primitive Infinite Relations |
| 76 | + |
| 77 | +** Naturals (ℕ) |
| 78 | + |
| 79 | +#+BEGIN_SRC erlang |
| 80 | +Schema: #{value => natural} |
| 81 | +Cardinality: aleph_zero |
| 82 | +Generator: Enumerates 0, 1, 2, 3, ... |
| 83 | + |
| 84 | +Example tuples: |
| 85 | + #{value => 0} |
| 86 | + #{value => 1} |
| 87 | + #{value => 2} |
| 88 | + ... |
| 89 | +#+END_SRC |
| 90 | + |
| 91 | +** Integers (ℤ) |
| 92 | + |
| 93 | +#+BEGIN_SRC erlang |
| 94 | +Schema: #{value => integer} |
| 95 | +Cardinality: aleph_zero |
| 96 | +Generator: Enumerates 0, 1, -1, 2, -2, 3, -3, ... |
| 97 | + |
| 98 | +Enumeration strategy: Interleave positive and negative |
| 99 | + f(0) = 0 |
| 100 | + f(2n) = n (for n > 0) |
| 101 | + f(2n+1) = -n (for n > 0) |
| 102 | +#+END_SRC |
| 103 | + |
| 104 | +** Rationals (ℚ) |
| 105 | + |
| 106 | +#+BEGIN_SRC erlang |
| 107 | +Schema: #{numerator => integer, denominator => natural} |
| 108 | +Cardinality: aleph_zero |
| 109 | +Generator: Stern-Brocot tree or Calkin-Wilf sequence |
| 110 | + |
| 111 | +Constraints: |
| 112 | + - denominator > 0 |
| 113 | + - gcd(numerator, denominator) = 1 (reduced form) |
| 114 | + |
| 115 | +Example tuples: |
| 116 | + #{numerator => 0, denominator => 1} % 0/1 |
| 117 | + #{numerator => 1, denominator => 1} % 1/1 |
| 118 | + #{numerator => 1, denominator => 2} % 1/2 |
| 119 | + #{numerator => 2, denominator => 1} % 2/1 |
| 120 | + #{numerator => 1, denominator => 3} % 1/3 |
| 121 | + ... |
| 122 | +#+END_SRC |
| 123 | + |
| 124 | +** Reals (ℝ) - Theoretical |
| 125 | + |
| 126 | +#+BEGIN_SRC erlang |
| 127 | +Schema: #{value => real} |
| 128 | +Cardinality: continuum |
| 129 | +Generator: Not fully enumerable (conceptual only) |
| 130 | + |
| 131 | +Note: In practice, we can only represent computable reals or |
| 132 | + algebraic reals (still countable but more expressive). |
| 133 | +#+END_SRC |
| 134 | + |
| 135 | +* Function Relations |
| 136 | + |
| 137 | +A relation R is a *function* if: ∀a ∃!b : (a,b) ∈ R |
| 138 | + |
| 139 | +That is, for every input, there exists exactly one output. |
| 140 | + |
| 141 | +** Plus (addition) |
| 142 | + |
| 143 | +#+BEGIN_SRC erlang |
| 144 | +Name: plus |
| 145 | +Schema: #{a => number, b => number, sum => number} |
| 146 | +Cardinality: aleph_zero (when a,b ∈ ℤ or ℚ) |
| 147 | +Is_function: false (it's a 3-way relation, not (a,b) → sum) |
| 148 | +Function view: plus(a, b) = sum where (a, b, sum) ∈ Plus |
| 149 | + |
| 150 | +Generator: For each (a, b) pair, yield #{a => A, b => B, sum => A + B} |
| 151 | + |
| 152 | +Constraints required for iteration: |
| 153 | + - At least two of {a, b, sum} must be bounded |
| 154 | + |
| 155 | +Valid queries: |
| 156 | + - plus where a ∈ [0..10], b ∈ [0..10] ✓ (finite result: 121 tuples) |
| 157 | + - plus where a = 5, b ∈ Naturals ✓ (countable: {5,0,5}, {5,1,6}, ...) |
| 158 | + - plus where sum = 10 ✓ (countable: infinitely many a+b=10) |
| 159 | + - plus with no constraints ✗ (cannot enumerate) |
| 160 | +#+END_SRC |
| 161 | + |
| 162 | +** Times (multiplication) |
| 163 | + |
| 164 | +#+BEGIN_SRC erlang |
| 165 | +Name: times |
| 166 | +Schema: #{a => number, b => number, product => number} |
| 167 | +Cardinality: aleph_zero |
| 168 | +Generator: For each (a, b) pair, yield #{a => A, b => B, product => A * B} |
| 169 | +#+END_SRC |
| 170 | + |
| 171 | +** Successor |
| 172 | + |
| 173 | +#+BEGIN_SRC erlang |
| 174 | +Name: successor |
| 175 | +Schema: #{n => integer, succ => integer} |
| 176 | +Cardinality: aleph_zero |
| 177 | +Is_function: true (n → succ is a function) |
| 178 | +Generator: For each n, yield #{n => N, succ => N + 1} |
| 179 | +#+END_SRC |
| 180 | + |
| 181 | +* Cardinality Algebra |
| 182 | + |
| 183 | +Rules for computing cardinality of relational operations: |
| 184 | + |
| 185 | +** Union (∪) |
| 186 | + |
| 187 | +| Left | Right | Result | Notes | |
| 188 | +|------------+------------+------------+--------------------------| |
| 189 | +| {finite,m} | {finite,n} | {finite,≤m+n} | May have duplicates | |
| 190 | +| {finite,n} | aleph_zero | aleph_zero | Finite + infinite = infinite | |
| 191 | +| aleph_zero | aleph_zero | aleph_zero | ℵ₀ + ℵ₀ = ℵ₀ | |
| 192 | +| aleph_zero | continuum | continuum | Continuum dominates | |
| 193 | +| continuum | continuum | continuum | 2^ℵ₀ + 2^ℵ₀ = 2^ℵ₀ | |
| 194 | + |
| 195 | +** Cartesian Product (×) |
| 196 | + |
| 197 | +| Left | Right | Result | Notes | |
| 198 | +|------------+------------+---------------+-----------------------| |
| 199 | +| {finite,m} | {finite,n} | {finite,m·n} | Product of sizes | |
| 200 | +| {finite,n} | aleph_zero | aleph_zero | n · ℵ₀ = ℵ₀ | |
| 201 | +| aleph_zero | aleph_zero | aleph_zero | ℵ₀ · ℵ₀ = ℵ₀ | |
| 202 | +| aleph_zero | continuum | continuum | ℵ₀ · 2^ℵ₀ = 2^ℵ₀ | |
| 203 | +| continuum | continuum | continuum | 2^ℵ₀ · 2^ℵ₀ = 2^ℵ₀ | |
| 204 | + |
| 205 | +** Natural Join (⋈) |
| 206 | + |
| 207 | +Cardinality depends on join selectivity: |
| 208 | + |
| 209 | +| Left | Right | Result | Notes | |
| 210 | +|------------+------------+------------+------------------------------------| |
| 211 | +| {finite,m} | {finite,n} | {finite,k} | k ≤ min(m,n) typically | |
| 212 | +| {finite,n} | aleph_zero | varies | Could be finite or aleph_zero | |
| 213 | +| aleph_zero | aleph_zero | varies | Depends on join condition | |
| 214 | + |
| 215 | +*Examples:* |
| 216 | + |
| 217 | +#+BEGIN_SRC erlang |
| 218 | +%% Finite ⋈ Infinite (finite result) |
| 219 | +Employees = {finite, 100} % 100 employees |
| 220 | +Naturals = aleph_zero % Infinite numbers |
| 221 | +Employees ⋈ Naturals on employee_id = value |
| 222 | + ⇒ {finite, 100} % At most 100 matches |
| 223 | + |
| 224 | +%% Infinite ⋈ Infinite (infinite result) |
| 225 | +Naturals ⋈ Plus on Naturals.value = Plus.a |
| 226 | + ⇒ aleph_zero % For each natural n, infinite (n,b,n+b) tuples |
| 227 | + |
| 228 | +%% Infinite ⋈ Infinite (finite result with constraints) |
| 229 | +(Naturals where value < 10) ⋈ (Naturals where value < 10) |
| 230 | + ⇒ {finite, 100} % 10 × 10 = 100 |
| 231 | +#+END_SRC |
| 232 | + |
| 233 | +** Selection (σ) |
| 234 | + |
| 235 | +| Input | Result | Notes | |
| 236 | +|------------+------------+------------------------------------| |
| 237 | +| {finite,n} | {finite,k} | k ≤ n (filtering reduces size) | |
| 238 | +| aleph_zero | varies | Could be finite or aleph_zero | |
| 239 | +| continuum | varies | Could be any cardinality | |
| 240 | + |
| 241 | +*Examples:* |
| 242 | + |
| 243 | +#+BEGIN_SRC erlang |
| 244 | +σ(Naturals, value < 10) ⇒ {finite, 10} % Bounded selection |
| 245 | +σ(Naturals, value > 5) ⇒ aleph_zero % Infinite result |
| 246 | +σ(Naturals, value % 2 = 0) ⇒ aleph_zero % Even numbers (infinite) |
| 247 | +#+END_SRC |
| 248 | + |
| 249 | +** Projection (π) |
| 250 | + |
| 251 | +| Input | Result | Notes | |
| 252 | +|------------+------------+---------------------------------| |
| 253 | +| {finite,n} | {finite,k} | k ≤ n (duplicates removed) | |
| 254 | +| aleph_zero | aleph_zero | Typically preserves infinity | |
| 255 | +| continuum | continuum | Typically preserves cardinality | |
| 256 | + |
| 257 | +* Constraint System |
| 258 | + |
| 259 | +** Mandatory Constraints |
| 260 | + |
| 261 | +Queries on infinite relations *must* provide constraints that bound the iteration. |
| 262 | + |
| 263 | +#+BEGIN_SRC erlang |
| 264 | +%% INVALID: Cannot iterate infinite relation without constraints |
| 265 | +Iterator = get_tuples_iterator(DB, naturals). ❌ |
| 266 | + |
| 267 | +%% VALID: Bounded by constraint |
| 268 | +Iterator = get_tuples_iterator(DB, naturals, #{value => {range, 0, 100}}). ✓ |
| 269 | +#+END_SRC |
| 270 | + |
| 271 | +** Constraint Validation |
| 272 | + |
| 273 | +Before executing a query on an infinite relation, validate: |
| 274 | + |
| 275 | +1. *Finite result check*: Do constraints guarantee finite result? |
| 276 | +2. *Bounded iteration check*: Can we enumerate results in finite time? |
| 277 | + |
| 278 | +#+BEGIN_SRC erlang |
| 279 | +validate_constraints(Relation, Constraints) -> |
| 280 | + case Relation#relation.cardinality of |
| 281 | + {finite, _} -> |
| 282 | + ok; % Finite relations don't need constraints |
| 283 | + aleph_zero -> |
| 284 | + case infers_finite_result(Relation, Constraints) of |
| 285 | + true -> ok; |
| 286 | + false -> {error, unbounded_iteration} |
| 287 | + end; |
| 288 | + continuum -> |
| 289 | + {error, uncountable_relation} % Cannot iterate continuum |
| 290 | + end. |
| 291 | +#+END_SRC |
| 292 | + |
| 293 | +** Constraint Inference |
| 294 | + |
| 295 | +Smart inference of finiteness: |
| 296 | + |
| 297 | +#+BEGIN_SRC erlang |
| 298 | +%% These constraints imply finite results: |
| 299 | +#{value => {range, 0, 100}} % Range is finite |
| 300 | +#{value => {in, [1,2,3,4,5]}} % Membership in finite set |
| 301 | +#{value => {lt, 10}} % Bounded above (if naturals) |
| 302 | + |
| 303 | +%% These do NOT imply finite results: |
| 304 | +#{value => {gt, 10}} % Unbounded above |
| 305 | +#{value => {neq, 5}} % Excludes one element |
| 306 | +#+END_SRC |
| 307 | + |
| 308 | +* Implementation Strategy |
| 309 | + |
| 310 | +** Phase 1: Core Infrastructure |
| 311 | +1. Extend =relation= record with =cardinality= and =generator= fields |
| 312 | +2. Implement cardinality algebra functions |
| 313 | +3. Add constraint validation framework |
| 314 | + |
| 315 | +** Phase 2: Primitive Relations |
| 316 | +1. Implement =naturals= generator |
| 317 | +2. Implement =integers= generator (interleaving strategy) |
| 318 | +3. Implement =rationals= generator (Stern-Brocot or Calkin-Wilf) |
| 319 | + |
| 320 | +** Phase 3: Function Relations |
| 321 | +1. Implement =plus= relation |
| 322 | +2. Implement =times= relation |
| 323 | +3. Implement =successor=, =predecessor= relations |
| 324 | + |
| 325 | +** Phase 4: Query Engine |
| 326 | +1. Extend iterator model to support generators |
| 327 | +2. Implement constraint-based enumeration |
| 328 | +3. Add cardinality inference for query results |
| 329 | + |
| 330 | +** Phase 5: Relational Operators |
| 331 | +1. Extend join to handle infinite relations |
| 332 | +2. Extend union with cardinality tracking |
| 333 | +3. Extend selection with constraint propagation |
| 334 | + |
| 335 | +* Open Questions |
| 336 | + |
| 337 | +1. *Partial materialization*: Should we cache generated tuples? |
| 338 | +2. *Generator composition*: How to compose generators for derived relations? |
| 339 | +3. *Constraint solving*: Do we need a full constraint solver (CLP)? |
| 340 | +4. *Termination guarantees*: How to prove queries terminate? |
| 341 | +5. *Physical storage*: How to persist infinite relation definitions? |
| 342 | + |
| 343 | +* References |
| 344 | + |
| 345 | +- Codd, E. F. (1979). "Extending the Database Relational Model" |
| 346 | +- Cantor, G. "On the Cardinality of Sets" |
| 347 | +- Stern-Brocot Tree: Enumeration of rationals |
| 348 | +- Calkin-Wilf Tree: Alternative rational enumeration |
0 commit comments