From 8c640a262969ef44cd8bc0e0abe95e2a54f4c3f5 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Thu, 5 Mar 2026 23:42:15 -0300 Subject: ocaml re-migration --- docs/infinite_relations_design.org | 348 ------------------------------------- 1 file changed, 348 deletions(-) delete mode 100644 docs/infinite_relations_design.org (limited to 'docs/infinite_relations_design.org') diff --git a/docs/infinite_relations_design.org b/docs/infinite_relations_design.org deleted file mode 100644 index c13e783..0000000 --- a/docs/infinite_relations_design.org +++ /dev/null @@ -1,348 +0,0 @@ -#+TITLE: Infinite Relations Design -#+AUTHOR: Nekoma Team -#+DATE: 2025-01-22 - -* Overview - -This document specifies the design for infinite relations in Domino, enabling -countably infinite (ℵ₀) and uncountably infinite (continuum) relations alongside -finite relations. - -** Core Principle - -*Everything is a relation.* Types are relations. Functions are relations. -Numbers are relations. This unifies the type system with the data model. - -* Cardinality System - -** Cardinality Types - -#+BEGIN_SRC erlang --type cardinality() :: {finite, non_neg_integer()} % Finite set with N elements - | aleph_zero % Countably infinite (ℵ₀) - | continuum. % Uncountably infinite (2^ℵ₀) -#+END_SRC - -** Properties - -- Finite relations have explicit tuple count: ={finite, 1000}= -- Countably infinite relations: =aleph_zero= -- Uncountably infinite relations: =continuum= - -* Extended Data Model - -** Modified Relation Record - -#+BEGIN_SRC erlang --record(relation, { - hash, % Content hash (for finite) or generator hash (for infinite) - name, % Relation name (atom) - tree, % Merkle tree (finite only), undefined for infinite - schema, % Schema definition - cardinality, % {finite, N} | aleph_zero | continuum - generator, % Generator function (infinite only), undefined for finite - is_function % Boolean: true if relation represents a function -}). -#+END_SRC - -** Generator Specification - -Generators are functions that produce tuples on-demand based on constraints. - -#+BEGIN_SRC erlang --type generator_spec() :: - {primitive, atom()} % Built-in: naturals, integers, rationals - | {function_relation, atom(), arity()} % Built-in function: plus/3, times/3 - | {custom, fun((constraints()) -> tuple())} % User-defined generator - | {derived, relational_operation()}. % Derived from other relations - --type constraints() :: #{ - attribute_name() => constraint_spec() -}. - --type constraint_spec() :: - {eq, value()} % Equality: age = 30 - | {neq, value()} % Inequality: age ≠ 30 - | {lt, value()} % Less than: age < 30 - | {lte, value()} % Less than or equal - | {gt, value()} % Greater than - | {gte, value()} % Greater than or equal - | {in, [value()]} % Membership: age in [20,30,40] - | {range, value(), value()} % Range: age in [20..30] - | {member_of, relation_name()}. % Type constraint: x ∈ Naturals -#+END_SRC - -* Primitive Infinite Relations - -** Naturals (ℕ) - -#+BEGIN_SRC erlang -Schema: #{value => natural} -Cardinality: aleph_zero -Generator: Enumerates 0, 1, 2, 3, ... - -Example tuples: - #{value => 0} - #{value => 1} - #{value => 2} - ... -#+END_SRC - -** Integers (ℤ) - -#+BEGIN_SRC erlang -Schema: #{value => integer} -Cardinality: aleph_zero -Generator: Enumerates 0, 1, -1, 2, -2, 3, -3, ... - -Enumeration strategy: Interleave positive and negative - f(0) = 0 - f(2n) = n (for n > 0) - f(2n+1) = -n (for n > 0) -#+END_SRC - -** Rationals (ℚ) - -#+BEGIN_SRC erlang -Schema: #{numerator => integer, denominator => natural} -Cardinality: aleph_zero -Generator: Stern-Brocot tree or Calkin-Wilf sequence - -Constraints: - - denominator > 0 - - gcd(numerator, denominator) = 1 (reduced form) - -Example tuples: - #{numerator => 0, denominator => 1} % 0/1 - #{numerator => 1, denominator => 1} % 1/1 - #{numerator => 1, denominator => 2} % 1/2 - #{numerator => 2, denominator => 1} % 2/1 - #{numerator => 1, denominator => 3} % 1/3 - ... -#+END_SRC - -** Reals (ℝ) - Theoretical - -#+BEGIN_SRC erlang -Schema: #{value => real} -Cardinality: continuum -Generator: Not fully enumerable (conceptual only) - -Note: In practice, we can only represent computable reals or - algebraic reals (still countable but more expressive). -#+END_SRC - -* Function Relations - -A relation R is a *function* if: ∀a ∃!b : (a,b) ∈ R - -That is, for every input, there exists exactly one output. - -** Plus (addition) - -#+BEGIN_SRC erlang -Name: plus -Schema: #{a => number, b => number, sum => number} -Cardinality: aleph_zero (when a,b ∈ ℤ or ℚ) -Is_function: false (it's a 3-way relation, not (a,b) → sum) -Function view: plus(a, b) = sum where (a, b, sum) ∈ Plus - -Generator: For each (a, b) pair, yield #{a => A, b => B, sum => A + B} - -Constraints required for iteration: - - At least two of {a, b, sum} must be bounded - -Valid queries: - - plus where a ∈ [0..10], b ∈ [0..10] ✓ (finite result: 121 tuples) - - plus where a = 5, b ∈ Naturals ✓ (countable: {5,0,5}, {5,1,6}, ...) - - plus where sum = 10 ✓ (countable: infinitely many a+b=10) - - plus with no constraints ✗ (cannot enumerate) -#+END_SRC - -** Times (multiplication) - -#+BEGIN_SRC erlang -Name: times -Schema: #{a => number, b => number, product => number} -Cardinality: aleph_zero -Generator: For each (a, b) pair, yield #{a => A, b => B, product => A * B} -#+END_SRC - -** Successor - -#+BEGIN_SRC erlang -Name: successor -Schema: #{n => integer, succ => integer} -Cardinality: aleph_zero -Is_function: true (n → succ is a function) -Generator: For each n, yield #{n => N, succ => N + 1} -#+END_SRC - -* Cardinality Algebra - -Rules for computing cardinality of relational operations: - -** Union (∪) - -| Left | Right | Result | Notes | -|------------+------------+------------+--------------------------| -| {finite,m} | {finite,n} | {finite,≤m+n} | May have duplicates | -| {finite,n} | aleph_zero | aleph_zero | Finite + infinite = infinite | -| aleph_zero | aleph_zero | aleph_zero | ℵ₀ + ℵ₀ = ℵ₀ | -| aleph_zero | continuum | continuum | Continuum dominates | -| continuum | continuum | continuum | 2^ℵ₀ + 2^ℵ₀ = 2^ℵ₀ | - -** Cartesian Product (×) - -| Left | Right | Result | Notes | -|------------+------------+---------------+-----------------------| -| {finite,m} | {finite,n} | {finite,m·n} | Product of sizes | -| {finite,n} | aleph_zero | aleph_zero | n · ℵ₀ = ℵ₀ | -| aleph_zero | aleph_zero | aleph_zero | ℵ₀ · ℵ₀ = ℵ₀ | -| aleph_zero | continuum | continuum | ℵ₀ · 2^ℵ₀ = 2^ℵ₀ | -| continuum | continuum | continuum | 2^ℵ₀ · 2^ℵ₀ = 2^ℵ₀ | - -** Natural Join (⋈) - -Cardinality depends on join selectivity: - -| Left | Right | Result | Notes | -|------------+------------+------------+------------------------------------| -| {finite,m} | {finite,n} | {finite,k} | k ≤ min(m,n) typically | -| {finite,n} | aleph_zero | varies | Could be finite or aleph_zero | -| aleph_zero | aleph_zero | varies | Depends on join condition | - -*Examples:* - -#+BEGIN_SRC erlang -%% Finite ⋈ Infinite (finite result) -Employees = {finite, 100} % 100 employees -Naturals = aleph_zero % Infinite numbers -Employees ⋈ Naturals on employee_id = value - ⇒ {finite, 100} % At most 100 matches - -%% Infinite ⋈ Infinite (infinite result) -Naturals ⋈ Plus on Naturals.value = Plus.a - ⇒ aleph_zero % For each natural n, infinite (n,b,n+b) tuples - -%% Infinite ⋈ Infinite (finite result with constraints) -(Naturals where value < 10) ⋈ (Naturals where value < 10) - ⇒ {finite, 100} % 10 × 10 = 100 -#+END_SRC - -** Selection (σ) - -| Input | Result | Notes | -|------------+------------+------------------------------------| -| {finite,n} | {finite,k} | k ≤ n (filtering reduces size) | -| aleph_zero | varies | Could be finite or aleph_zero | -| continuum | varies | Could be any cardinality | - -*Examples:* - -#+BEGIN_SRC erlang -σ(Naturals, value < 10) ⇒ {finite, 10} % Bounded selection -σ(Naturals, value > 5) ⇒ aleph_zero % Infinite result -σ(Naturals, value % 2 = 0) ⇒ aleph_zero % Even numbers (infinite) -#+END_SRC - -** Projection (π) - -| Input | Result | Notes | -|------------+------------+---------------------------------| -| {finite,n} | {finite,k} | k ≤ n (duplicates removed) | -| aleph_zero | aleph_zero | Typically preserves infinity | -| continuum | continuum | Typically preserves cardinality | - -* Constraint System - -** Mandatory Constraints - -Queries on infinite relations *must* provide constraints that bound the iteration. - -#+BEGIN_SRC erlang -%% INVALID: Cannot iterate infinite relation without constraints -Iterator = get_tuples_iterator(DB, naturals). ❌ - -%% VALID: Bounded by constraint -Iterator = get_tuples_iterator(DB, naturals, #{value => {range, 0, 100}}). ✓ -#+END_SRC - -** Constraint Validation - -Before executing a query on an infinite relation, validate: - -1. *Finite result check*: Do constraints guarantee finite result? -2. *Bounded iteration check*: Can we enumerate results in finite time? - -#+BEGIN_SRC erlang -validate_constraints(Relation, Constraints) -> - case Relation#relation.cardinality of - {finite, _} -> - ok; % Finite relations don't need constraints - aleph_zero -> - case infers_finite_result(Relation, Constraints) of - true -> ok; - false -> {error, unbounded_iteration} - end; - continuum -> - {error, uncountable_relation} % Cannot iterate continuum - end. -#+END_SRC - -** Constraint Inference - -Smart inference of finiteness: - -#+BEGIN_SRC erlang -%% These constraints imply finite results: -#{value => {range, 0, 100}} % Range is finite -#{value => {in, [1,2,3,4,5]}} % Membership in finite set -#{value => {lt, 10}} % Bounded above (if naturals) - -%% These do NOT imply finite results: -#{value => {gt, 10}} % Unbounded above -#{value => {neq, 5}} % Excludes one element -#+END_SRC - -* Implementation Strategy - -** Phase 1: Core Infrastructure -1. Extend =relation= record with =cardinality= and =generator= fields -2. Implement cardinality algebra functions -3. Add constraint validation framework - -** Phase 2: Primitive Relations -1. Implement =naturals= generator -2. Implement =integers= generator (interleaving strategy) -3. Implement =rationals= generator (Stern-Brocot or Calkin-Wilf) - -** Phase 3: Function Relations -1. Implement =plus= relation -2. Implement =times= relation -3. Implement =successor=, =predecessor= relations - -** Phase 4: Query Engine -1. Extend iterator model to support generators -2. Implement constraint-based enumeration -3. Add cardinality inference for query results - -** Phase 5: Relational Operators -1. Extend join to handle infinite relations -2. Extend union with cardinality tracking -3. Extend selection with constraint propagation - -* Open Questions - -1. *Partial materialization*: Should we cache generated tuples? -2. *Generator composition*: How to compose generators for derived relations? -3. *Constraint solving*: Do we need a full constraint solver (CLP)? -4. *Termination guarantees*: How to prove queries terminate? -5. *Physical storage*: How to persist infinite relation definitions? - -* References - -- Codd, E. F. (1979). "Extending the Database Relational Model" -- Cantor, G. "On the Cardinality of Sets" -- Stern-Brocot Tree: Enumeration of rationals -- Calkin-Wilf Tree: Alternative rational enumeration -- cgit v1.2.3