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/architecture.plantuml | 72 +++++ docs/code.org | 272 ------------------ docs/command-interface.puml | 58 ---- docs/constraint-classification.puml | 82 ------ docs/constraint-enforcement-strategies.puml | 42 --- docs/constraints.org | 97 ------- docs/data-model.puml | 101 ------- docs/distribution-architecture.puml | 63 ---- docs/features.org | 429 ---------------------------- docs/infinite-relations.puml | 177 ------------ docs/infinite_relations_design.org | 348 ---------------------- docs/iterator-pipeline.puml | 45 --- docs/karuta-interface-layers.puml | 65 ----- docs/merkle-tree-hierarchy.puml | 50 ---- docs/module-dependencies.puml | 39 --- docs/provenance-lineage.puml | 69 ----- docs/query-execution-flow.puml | 54 ---- docs/reactive-queries.puml | 51 ---- docs/reliability_roadmap.org | 223 --------------- docs/roadmap.puml | 72 ----- docs/system-overview.puml | 81 ------ docs/temporal-queries.puml | 61 ---- docs/transaction-algo.org | 12 + docs/type-checking-flow.puml | 108 ------- docs/type-hierarchy.puml | 289 ------------------- 25 files changed, 84 insertions(+), 2876 deletions(-) create mode 100644 docs/architecture.plantuml delete mode 100644 docs/code.org delete mode 100644 docs/command-interface.puml delete mode 100644 docs/constraint-classification.puml delete mode 100644 docs/constraint-enforcement-strategies.puml delete mode 100644 docs/constraints.org delete mode 100644 docs/data-model.puml delete mode 100644 docs/distribution-architecture.puml delete mode 100644 docs/features.org delete mode 100644 docs/infinite-relations.puml delete mode 100644 docs/infinite_relations_design.org delete mode 100644 docs/iterator-pipeline.puml delete mode 100644 docs/karuta-interface-layers.puml delete mode 100644 docs/merkle-tree-hierarchy.puml delete mode 100644 docs/module-dependencies.puml delete mode 100644 docs/provenance-lineage.puml delete mode 100644 docs/query-execution-flow.puml delete mode 100644 docs/reactive-queries.puml delete mode 100644 docs/reliability_roadmap.org delete mode 100644 docs/roadmap.puml delete mode 100644 docs/system-overview.puml delete mode 100644 docs/temporal-queries.puml create mode 100644 docs/transaction-algo.org delete mode 100644 docs/type-checking-flow.puml delete mode 100644 docs/type-hierarchy.puml (limited to 'docs') diff --git a/docs/architecture.plantuml b/docs/architecture.plantuml new file mode 100644 index 0000000..90985ba --- /dev/null +++ b/docs/architecture.plantuml @@ -0,0 +1,72 @@ +@startuml +allowmixing + +package Client { + object "Query Interface" as query_interface +} + +package Algebra { + object "Unifier" as unifier + object "Bytecode Builder" as bytecode_builder + object "Parser" as parser + object "Lexer" as lexer +} + +query_interface --> lexer +lexer --> parser +parser --> unifier +unifier --> bytecode_builder + +package Query { + object "Schema Builder" as schema_builder + object "Facts Builder" as facts_builder + object "Optimizer" as optimizer + object "Commands Generator" as commands_generator + object "B+ Tree" as b_plus_tree +} + +bytecode_builder --> optimizer +optimizer --> commands_generator +facts_builder --> commands_generator +schema_builder --> commands_generator +commands_generator --> b_plus_tree +b_plus_tree --> query_interface + +package Coordinator { + object "File Historical Hashes" as file_historical_hashes + object "Location Hashes" as location_hashes + object "Command Parser" as command_parser + object "Curator" as curator +} + +commands_generator <-- command_parser + +package Disk { + object "Merkle Tree Root Generator" as merkle_tree + object "WAL Reader" as wal_reader + object "WAL Writer" as wal_writer + object "ARIES" as aries + object "SHA256 Hasher" as sha + object "Executor" as executor + map storage { + write => +λ + read => +λ + } + object "Courier" as courier + database Wal +} + +executor *--> merkle_tree +executor *--> sha +curator --> command_parser +command_parser --> executor +location_hashes *--> curator +file_historical_hashes *--> curator +executor --> aries +aries --> wal_reader +aries --> wal_writer +wal_writer --> Wal +wal_reader --> Wal +courier <-- wal_reader +courier --> storage +@enduml \ No newline at end of file diff --git a/docs/code.org b/docs/code.org deleted file mode 100644 index 30ff9c9..0000000 --- a/docs/code.org +++ /dev/null @@ -1,272 +0,0 @@ -#+TITLE: Code Documentation - -* Overview - -Domino is a content-addressed, immutable relational database engine written in Erlang. The system uses cryptographic hashing (SHA-256) and Merkle trees to provide version control, deduplication, and efficient synchronization capabilities. - -* Architecture - -** Design Patterns - -- *Content-Addressed Storage* :: All data (attributes, tuples, relations, databases) are identified by their cryptographic hash -- *Immutable Data Structures* :: All operations create new versions rather than modifying existing data -- *Merkle Trees* :: Relations and databases use merkle trees for efficient diffing and synchronization -- *Volcano Iterator Model* :: Query execution uses lazy evaluation with process-based iterators -- *Actor Model* :: Iterators are implemented as independent Erlang processes -- *Transactional Storage* :: Mnesia provides ACID guarantees for all mutations - -* Module Structure - -** operations.erl - -The core database operations module and main API. - -*** Public API - -**** Database & Relation Management -- =setup/0= :: Initialize Mnesia schema and create all tables -- =create_database/1= :: Create a new database state -- =create_relation/3= :: Add a relation to a database with schema -- =get_relations/1= :: List all relation names in a database -- =get_relation_hash/2= :: Get relation hash by name - -**** Tuple Operations -- =create_tuple/3= :: Insert a tuple into a relation (transactional) -- =retract_tuple/3= :: Remove a tuple from a relation (default: transactional) -- =retract_tuple/4= :: Remove a tuple with optional transaction control - -**** Relation Operations -- =clear_relation/2= :: Remove all tuples from a relation (default: transactional) -- =clear_relation/3= :: Clear relation with optional transaction control -- =retract_relation/2= :: Remove a relation from database (default: transactional) -- =retract_relation/3= :: Remove relation with optional transaction control - -**** Iterator Pattern (Volcano Model) -- =get_tuples_iterator/2= :: Create lazy iterator process for relation tuples -- =next_tuple/1= :: Pull next tuple from iterator (returns ={ok, Tuple} | done=) -- =close_iterator/1= :: Terminate iterator process -- =collect_all/1= :: Helper to consume entire iterator into list - -**** Utility Functions -- =hash/1= :: SHA-256 hash of term -- =hashes_from_tuple/1= :: Extract all tuple hashes from a relation - -** relation.erl - -Simple helper module for building tuples and relations conceptually. - -*** Public API -- =new_attribute/2= :: Create attribute map: =#{name => Name, value => Value}= -- =new_tuple/1= :: Convert list of attributes to map -- =new_relation/1= :: Convert list of tuples to sets:set - -** poc.erl - -Proof-of-concept demonstrating the Volcano Iterator Model for query execution. - -*** Key Concepts -- Content-addressed storage simulation using in-memory maps -- Lazy iterator chain: Scan → Select → Project -- Message-passing protocol for tuple streaming -- Automatic deduplication via hashing - -** main.erl - -OTP application entry point. Starts Mnesia on application startup. - -* Data Structures - -All core records are defined in =include/operations.hrl=. - -** attribute -#+BEGIN_SRC erlang --record(attribute, { - hash, % SHA-256 hash of value - value % Actual value (any Erlang term) -}). -#+END_SRC - -** tuple -#+BEGIN_SRC erlang --record(tuple, { - hash, % SHA-256 hash of entire tuple - relation, % Relation name (atom) - attribute_map % #{attr_name => value_hash} -}). -#+END_SRC - -** relation -#+BEGIN_SRC erlang --record(relation, { - hash, % hash({name, schema, tree_root}) - name, % Relation name (atom) - tree, % Merkle tree of tuple hashes - schema % Schema definition map -}). -#+END_SRC - -** database_state -#+BEGIN_SRC erlang --record(database_state, { - hash, % Merkle tree root hash - name, % Database name (atom) - tree, % Merkle tree of relations - relations, % #{relation_name => relation_hash} - timestamp % Creation/modification timestamp -}). -#+END_SRC - -* Data Flow - -** Creating a Tuple - -1. Store each attribute value separately (enables deduplication) -2. Build attribute_map with hashes: =#{name => AttrHash1, age => AttrHash2}= -3. Create tuple record with hash -4. Insert tuple hash into relation's merkle tree -5. Compute new relation hash from tree root -6. Update database merkle tree -7. Return updated database and relation - -All operations occur within a Mnesia transaction. - -** Querying Tuples - -1. Lookup relation hash from database -2. Read relation from Mnesia -3. Extract tuple hashes from merkle tree -4. Spawn iterator process with hash list -5. Client pulls tuples via message passing -6. Iterator resolves: hash → tuple → attribute hashes → actual values -7. Return materialized tuple map - -* Usage Examples - -** Basic Workflow - -#+BEGIN_SRC erlang -%% Setup -operations:setup(). - -%% Create database -DB = operations:create_database(my_app). - -%% Create relation with schema -{DB1, _Rel} = operations:create_relation(DB, users, #{ - name => string, - age => integer -}). - -%% Insert tuples -{DB2, _} = operations:create_tuple(DB1, users, #{name => "Alice", age => 30}). -{DB3, _} = operations:create_tuple(DB2, users, #{name => "Bob", age => 25}). - -%% Query tuples -Iterator = operations:get_tuples_iterator(DB3, users). -Tuples = operations:collect_all(Iterator). -%% Returns: [#{name => "Alice", age => 30}, #{name => "Bob", age => 25}] - -%% Remove tuple -{ok, RelHash} = operations:get_relation_hash(DB3, users). -[TupleHash|_] = operations:hashes_from_tuple(RelHash). -{atomic, {DB4, _}} = operations:retract_tuple(DB3, RelHash, TupleHash). - -%% Clear relation (remove all tuples, keep schema) -{atomic, {DB5, _}} = operations:clear_relation(DB4, RelHash). - -%% Remove relation entirely -{atomic, DB6} = operations:retract_relation(DB5, users). -#+END_SRC - -** Iterator Protocol - -#+BEGIN_SRC erlang -Iterator = operations:get_tuples_iterator(DB, users). - -%% Pull tuples one by one -case operations:next_tuple(Iterator) of - {ok, Tuple} -> process_tuple(Tuple); - done -> io:format("No more tuples~n") -end. - -%% Or collect all at once -AllTuples = operations:collect_all(Iterator). - -%% Clean up -operations:close_iterator(Iterator). -#+END_SRC - -* Key Implementation Details - -** Immutability & Versioning - -Every modification creates a new hash. Old versions remain accessible via their hash. Database evolution is tracked via timestamp and hash chain. - -** Deduplication - -Identical attribute values are stored once (content-addressed). Example: 1000 users with age=30 store the value "30" only once. - -** Transaction Semantics - -All mutations are wrapped in =mnesia:transaction/1=. Dirty reads are used for immutable data lookups. - -** Merkle Tree Strategy - -- Relations store tuple hashes as keys: ={TupleHash, <<>>}= -- Databases store relation names → hashes: ={RelationName, RelationHash}= -- Enables efficient diff computation between versions -- Foundation for distributed synchronization - -** Iterator Pattern - -- Decouples query execution from data access -- Enables pipelined query operators (future: select, project, join) -- Memory bounded (doesn't materialize entire relation) -- Process-based concurrency via Erlang actors - -** Schema Flexibility - -Schema stored as map (e.g., =#{name => string, age => integer}=). Currently not enforced, but provides foundation for future domain validation. - -* Dependencies - -- =merklet= (2.0.0) :: Merkle tree implementation for set reconciliation -- =mnesia= :: Distributed database for persistent storage -- =crypto= :: SHA-256 hashing - -* Testing - -The test suite (=test/operations_test.erl=) validates: - -- Functional correctness (CRUD operations) -- Hash determinism and consistency -- Transactional integrity -- Iterator protocol compliance -- State evolution tracking -- Cross-database consistency - -Run tests with: - -#+BEGIN_SRC sh -rebar3 eunit -#+END_SRC - -* Current State - -** Implemented -- Core data model (attribute, tuple, relation, database) -- Content-addressed storage with SHA-256 -- Immutable versioning -- Merkle tree integration -- Iterator-based lazy evaluation -- Transactional CRUD operations -- Comprehensive test suite - -** Not Yet Implemented -- Relational algebra operators (σ, π, ⋈, ∪, ∩, −) -- Schema validation and type checking -- Infinite relations (aleph₀) -- Join indexing -- Query optimization -- Distributed synchronization -- REPL/query console diff --git a/docs/command-interface.puml b/docs/command-interface.puml deleted file mode 100644 index 4c0319a..0000000 --- a/docs/command-interface.puml +++ /dev/null @@ -1,58 +0,0 @@ -@startuml command-interface -!theme plain -title Command-Based Interface Flow - -participant "Karuta" as K -participant "domino:execute/2" as API -participant "Command Validator" as V -participant "operations.erl" as Ops -database "Mnesia" as DB - -K -> API: execute(DB0, {create, relation, employee, Schema}) -activate API -API -> V: validate({create, relation, ...}) -activate V -V -> V: check schema format -V -> V: verify types -V --> API: ok -deactivate V - -API -> Ops: create_relation(DB0, employee, Schema) -activate Ops -Ops -> DB: transaction(fn -> ... end) -activate DB -DB -> DB: insert relation record -DB -> DB: update database tree -DB --> Ops: {atomic, {NewDB, Hash}} -deactivate DB -Ops --> API: {NewDB, Hash} -deactivate Ops - -API --> K: {ok, DB1, {relation_created, employee, Hash}} -deactivate API - -K -> API: execute(DB1, {insert, tuple, employee, Data}) -activate API -API -> V: validate({insert, tuple, ...}) -activate V -V -> V: check schema compliance -V -> V: verify constraints -V --> API: ok -deactivate V - -API -> Ops: create_tuple(DB1, employee, Data) -activate Ops -Ops -> DB: transaction(fn -> ... end) -activate DB -DB -> DB: store attribute values -DB -> DB: create tuple record -DB -> DB: update merkle tree -DB --> Ops: {atomic, {NewDB2, TupleHash}} -deactivate DB -Ops --> API: {NewDB2, TupleHash} -deactivate Ops - -API --> K: {ok, DB2, {tuple_inserted, TupleHash}} -deactivate API - -@enduml diff --git a/docs/constraint-classification.puml b/docs/constraint-classification.puml deleted file mode 100644 index 09094f1..0000000 --- a/docs/constraint-classification.puml +++ /dev/null @@ -1,82 +0,0 @@ -@startuml constraint-classification -!theme plain -title Constraint Classification (McGoveran Framework) - -package "Database Constraints" { - class RelationConstraints { - Which relations must/can exist - Example: referential integrity - } - - class CardinalityConstraints { - Relation size limits - Examples: - - exactly N tuples - - at most M tuples - } -} - -package "Relation Constraints" { - package "Tuple Constraints" { - class AttributeConstraints { - Domain constraints per attribute - Examples: - - age >= 18 - - salary > 0 - - name ≠ "" - } - - class TupleLevelConstraints { - Cross-attribute rules - Example: - if salary > 200k then age >= 30 - } - } - - package "Relation-Level Constraints" { - class KeyConstraints { - Uniqueness + not null - - Primary keys - - Candidate keys - - Composite keys - } - - class FunctionalDependencies { - A → B - Example: ZIP → {city, state} - } - - class ForeignKeys { - Inclusion dependencies - Example: employee.dept_id ⊆ department.id - } - } -} - -package "Transition Constraints" { - class StateTransitionRules { - Before → After constraints - Examples: - - salary (monotonic increasing) - - created_at (immutable) - } - - class TemporalConstraints { - Time-based rules - Example: end_date >= start_date - } -} - -package "Multi-Relation Constraints" { - class AggregateConstraints { - Cross-relation aggregates - Example: sum(dept_salaries) <= dept_budget - } - - class MutualExclusion { - Disjoint sets - Example: managers ∩ ICs = ∅ - } -} - -@enduml diff --git a/docs/constraint-enforcement-strategies.puml b/docs/constraint-enforcement-strategies.puml deleted file mode 100644 index 6e0305d..0000000 --- a/docs/constraint-enforcement-strategies.puml +++ /dev/null @@ -1,42 +0,0 @@ -@startuml constraint-enforcement-strategies -!theme plain -title Constraint Enforcement Strategies - -state "Operation Request" as Request -state "Immediate Validation" as Immediate -state "Deferred Validation" as Deferred -state "Execute Operation" as Execute -state "Transaction Commit" as Commit -state "Rollback" as Rollback -state "Success" as Success - -Request --> Immediate: Strategy 1:\nEager -Request --> Execute: Strategy 2:\nDeferred - -Immediate --> Execute: Valid -Immediate --> Rollback: Invalid - -Execute --> Deferred: At commit -Deferred --> Commit: Valid -Deferred --> Rollback: Invalid - -Commit --> Success -Rollback --> Request: Retry - -note right of Immediate - Immediate Checking: - - Validate before execute - - Simple reasoning - - May reject valid intermediate states - - Lower performance -end note - -note right of Deferred - Deferred Checking: - - Validate at transaction end - - Allows intermediate invalid states - - Better performance - - Complex error handling -end note - -@enduml diff --git a/docs/constraints.org b/docs/constraints.org deleted file mode 100644 index b3978e6..0000000 --- a/docs/constraints.org +++ /dev/null @@ -1,97 +0,0 @@ -#+TITLE: Constraints - -* Preamble -Under an ontological commitment to objects, with an objects-properties -modeling in a conceptual model, there are primitive and compound objects: - -** Primitive objects -These are things we directly observe their existence independent of their individual properties - -** Compound objects -These are collective properties observed through their relationships in groups or multigroups - -* Entity Properties -These are the properties derived by observation or measurement -procedures. They can be further divided in: -- Quantitative :: which include ordinal and cardinal properties; for - example, customer rating and price of a product. -- Qualitative :: observed only, for example an enum - -* 1st Order Properties -They are inferred properties not directly observable in entities. They -are abstractions generalized from multiple observed or measured -properties that share: -- The same kind of values; -- The same allowable manipulations, and; -- Meaningful comparability. - -They arise when several concrete properties, for example salary, -commission and department budget, meet the above criteria. They are -understood as deriving from a more general underlying property, in the -example aforementioned, compensation, budget or whatever. That -underlying abstraction is the 1OP. - -** 1st Order Properties in Context -These are directly observed or measured properties of entities that -appear in a specific group in context. In other words, they are -concrete properties associated with entities of a particular type -whithin a context of a specific group or multigroup. The context is -essential because the underlying 1OP may manifest as different 1OPiCs -depending on the entity type (employee VS department) or group -membership (sales employees VS marketing employees). - -They are related to 1OPs insofar as they are contextual instantiations -of a 1OP, therefore, all 1OPiCs of the same kind share comparable -value sets and allow operations because they derive from the same -root. To illustrate with one example: salary and commission are 1OPiC -of the 1OP Compensation in the context of employees. - -* Constraint Algebra -The costrait module attempts to implement constraints as relations, in -other words, it follows the principle that Entity/1OPs/1OPiCs should -be a relation or domain. - -** Core Distinction: Domains vs Relations -- Domain (#domain{}): A VALUE SET with membership criteria (e.g., integers, rationals) -- Relation (#relation{}): A SET OF TUPLES -`less_than` is NOT a domain. It is a binary relation (subset of D × D). - -** 1st Order Properties (1OPs) -A 1OP is a direct property (attribute) of individual entities. 1OPs can be: -- Observed/measured: directly observed from entities (e.g., `salary`, `commission`) -- Derived/inferred: computed from other 1OPs (e.g., `compensation` = salary + commission) - -** Types -Domain constraints: ARE the domains themselves (membership criteria) -- `integer` domain: membership test is_integer/1 -- `rational` domain: numerator, denominator (integers), denominator ≠ 0 -Attribute constraints (1OP constraints): Restrict attribute values -- Specify which domain the attribute draws from -- Add constraints beyond domain membership -- Example: `salary` draws from `rational` + [gt(0), lt(1000000)] - -** 1st Order Properties in Context (1OPiCs) -A 1OPiC is a 1OP that is DERIVED from other observed/measured 1OPs within -the context of a specific relation. -Examples in `employees` relation: -- `salary`: observed/measured 1OP (draws from `money` domain) -- `commission`: observed/measured 1OP (draws from `money` domain) -- `compensation`: 1OPiC derived as salary + commission in context of employees -The schema entry `#{compensation => money}` declares which domain the -derived 1OPiC draws its values from. - -** Binary Relations -Comparisons are proper relations (not domains!): -``` -Less_Than_Integer = {(a, b) | a, b in Z, a < b} -``` -To express "x < 5", we check: `(x, 5) in Less_Than_Integer` - -** First-Order Logic Interface -Constraints become membership tests in relations: -- `x < 5` becomes `(x, 5) in less_than` -- `x > 3 AND x < 10` becomes `(3, x) in less_than AND (x, 10) in less_than` - -** Negation -Negation requires an explicit universe: `not(R, Universe)` computes -the complement of R within Universe. diff --git a/docs/data-model.puml b/docs/data-model.puml deleted file mode 100644 index 59e2cff..0000000 --- a/docs/data-model.puml +++ /dev/null @@ -1,101 +0,0 @@ -@startuml data-model -!theme plain -title Data Model Core Abstractions - -class attribute { - + hash: SHA256 - + value: term() -} - -class tuple { - + hash: SHA256 - + relation: atom() - + attribute_map: #{name => hash} -} - -class relation { - + hash: SHA256 - + name: atom() - + tree: merkle_tree() - + schema: #{attr => type_relation} - + constraints: constraints() - + cardinality: {finite, N} | aleph_zero | continuum - + generator: function() | undefined - + provenance: provenance() -} - -class type_relation { - + name: atom() - + erlang_type: type() - + membership_predicate: function() - + unfold_generator: function() - + cardinality: aleph_zero | continuum -} - -class database_state { - + hash: SHA256 - + name: atom() - + tree: merkle_tree() - + relations: #{name => hash} - + type_relations: #{name => type_relation} - + timestamp: integer() -} - -database_state "1" *-- "many" relation : contains -database_state "1" *-- "many" type_relation : defines types -relation "1" *-- "many" tuple : contains -tuple "1" *-- "many" attribute : references -relation --> type_relation : schema references - -note right of attribute - Content-Addressed Storage: - - SHA-256 hash of value - - Automatic deduplication - - Immutable once stored - - Value Validation: - Value must be member of - type relation specified in schema -end note - -note right of relation - Storage Strategy: - - Finite: Merkle tree (materialized) - - Infinite: Generator (lazy) - - Type Relations: - - Primitives: natural, integer, real, string - - Composite: views over other relations -end note - -note left of type_relation - **Schema Philosophy:** - Attributes are typed by type relations (not primitives). - Types are relations (stored as infinite relations). - Schema validation = membership checking. - - **Type Relations are Relations:** - They define domains via: - 1. Erlang type constraint - 2. Additional predicates - 3. Unfold generator for enumeration - - Examples: - - natural[X] :- integer[X], X >= 0 - - complex[X] :- X is (A,B), real[A], real[B] -end note - -note bottom of database_state - **Schema Example:** - employee relation schema: - #{ - name => non_empty_string, % type relation - age => natural, % type relation - salary => positive_integer % type relation - } - - Each schema value is a reference to a type relation, - NOT a primitive type string like "integer" -end note - -@enduml diff --git a/docs/distribution-architecture.puml b/docs/distribution-architecture.puml deleted file mode 100644 index fd2fd8c..0000000 --- a/docs/distribution-architecture.puml +++ /dev/null @@ -1,63 +0,0 @@ -@startuml distribution-architecture -!theme plain -title Future Distribution Architecture (Proposed) - -node "Node 1" { - component "Domino Instance 1" as D1 - database "Mnesia Replica 1" as M1 - component "Merkle Tree 1" as MT1 -} - -node "Node 2" { - component "Domino Instance 2" as D2 - database "Mnesia Replica 2" as M2 - component "Merkle Tree 2" as MT2 -} - -node "Node 3" { - component "Domino Instance 3" as D3 - database "Mnesia Replica 3" as M3 - component "Merkle Tree 3" as MT3 -} - -cloud "Sync Protocol" { - [Hash Comparison] as HC - [Delta Transfer] as DT - [Conflict Resolution] as CR -} - -D1 --> MT1 -D2 --> MT2 -D3 --> MT3 - -MT1 --> M1 -MT2 --> M2 -MT3 --> M3 - -MT1 <--> HC: compare hashes -MT2 <--> HC -MT3 <--> HC - -HC --> DT: if different -DT --> CR: if conflict -CR --> M1: apply changes -CR --> M2 -CR --> M3 - -note right of HC - Merkle tree enables efficient sync: - 1. Compare root hashes - 2. If different, compare subtrees - 3. Transfer only changed branches - 4. O(log n) comparison complexity -end note - -note bottom of CR - Conflict Resolution Strategies: - - Last-write-wins (timestamp) - - CRDTs (commutative operations) - - Consensus (Raft/Paxos) - - Application-defined merge -end note - -@enduml diff --git a/docs/features.org b/docs/features.org deleted file mode 100644 index 98350c5..0000000 --- a/docs/features.org +++ /dev/null @@ -1,429 +0,0 @@ -#+TITLE: Domino Features & Roadmap - -* Extended Relational Model (RM/T) - :PROPERTIES: - :CATEGORY: semantic-modeling - :END: - An extended relational database engine based on E. F. Codd's RM/T (1979). - Captures more meaning through entity types, surrogates, and molecular semantics. - -** Implemented Features - -*** DONE Content-Addressed Storage - CLOSED: [2025-01-21] - - [X] SHA-256 surrogates for all entities - - [X] System-controlled entity identifiers (E-domain) - - [X] Automatic deduplication via content addressing - - [X] Immutable data structures - -*** DONE Entity Types (E-Relations) - CLOSED: [2025-01-21] - - [X] Kernel entity types (database, relation) - - [X] E-relations for entity existence assertion - - [X] Surrogate-based entity identification - - [X] Entity integrity enforcement - -*** DONE Property Relations (P-Relations) - CLOSED: [2025-01-21] - - [X] Immediate property storage - - [X] Single-valued property support - - [X] Property integrity (Rule 4) - - [X] Foreign key references via surrogates - -*** DONE Merkle Tree Integration - CLOSED: [2025-01-21] - - [X] Relations as Merkle trees - - [X] Database state versioning - - [X] Efficient state diffing - - [X] Content-addressed relation hashing - -*** DONE Volcano Iterator Model - CLOSED: [2025-01-21] - - [X] Lazy tuple evaluation - - [X] Process-based iterators - - [X] Message-passing protocol - - [X] Memory-bounded queries - -*** DONE Transactional Operations - CLOSED: [2025-01-21] - - [X] ACID guarantees via Mnesia - - [X] Atomic tuple insertion - - [X] Tuple retraction with transactions - - [X] Relation clear and retract operations - -*** DONE Comprehensive Test Suite - CLOSED: [2025-01-21] - - [X] Database creation tests - - [X] Relation and tuple operations - - [X] Hash consistency validation - - [X] Iterator protocol tests - - [X] Retraction and truncate tests - - [X] Join operation tests - - [X] Provenance tracking tests - -*** DONE Attribute-Level Provenance Tracking - CLOSED: [2025-01-22] - - [X] Nested metadata structure (meta.provenance) - - [X] Track immediate source of each attribute - - [X] Always enabled - every tuple includes metadata - - [X] Automatic provenance merging in joins - - [X] Conflict resolution for duplicate attributes - - [X] Clean separation of data attributes and metadata - - [X] Foundation for tuple-level lineage tracking (implemented) - -** Planned RM/T Extensions - -*** TODO Characteristic Entities - Multi-valued properties as subordinate entities. - - [ ] Characteristic entity types (C-relations) - - [ ] Characteristic graph (CG-relation) - - [ ] Characteristic tree hierarchy - - [ ] Characteristic integrity (Rule 5) - - [ ] Example: Job history as characteristic of Employee - -*** TODO Associative Entities - Relationships as first-class entities with properties. - - [ ] Associative entity types (A-relations) - - [ ] Association graph (AG-relation) - - [ ] Association integrity (Rule 6) - - [ ] Higher-order associations - - [ ] Example: Assignment(employee, project, start_date) - -*** TODO Generalization Hierarchies - Entity subtyping and inheritance. - - [ ] Unconditional gen inclusion (UGI-relation) - - [ ] Alternative gen inclusion (AGI-relation) - - [ ] Subtype integrity (Rule 7) - - [ ] Property inheritance - - [ ] Multiple inheritance support - - [ ] Example: Engineer/Secretary/Trucker subtypes of Employee - -*** TODO Cover Aggregation - Collections and groupings. - - [ ] Cover membership relation (KG-relation) - - [ ] Cover entity types - - [ ] Dynamic membership - - [ ] Heterogeneous covers - - [ ] Example: Convoys, Teams, Departments - -*** TODO Event Precedence - Temporal ordering and scripts. - - [ ] Event entity types (T-relations) - - [ ] Unconditional successor (US-relation) - - [ ] Alternative successor (AS-relation) - - [ ] Unconditional predecessor (UP-relation) - - [ ] Alternative predecessor (AP-relation) - - [ ] Example: Order → Shipment → Invoice - -*** TODO Extended Operators - Operators for molecular semantics. - - [ ] OUTER NATURAL JOIN - - [ ] OUTER UNION - - [ ] OUTER THETA-JOIN - - [ ] MAYBE operators (null handling) - - [ ] Graph operators (OPEN, CLOSE, STEP) - -*** TODO RM/T Catalog - Extensible schema catalog. - - [ ] CATR (relations catalog) - - [ ] CATRA (relation-attribute) - - [ ] CATA (attributes catalog) - - [ ] CATAD (attribute-domain) - - [ ] CATD (domains catalog) - - [ ] CATC (categories catalog) - - [ ] CATRC (relation-category) - -*** TODO Property Graph (PG-relation) - Link P-relations to E-relations. - - [ ] Property molecule types - - [ ] Dynamic property schema - - [ ] Property graph traversal - -** Classical Relational Algebra - -*** TODO Selection (σ) - Filter tuples by predicate. - - [ ] THETA-SELECT with comparison operators - - [ ] Support for <, ≤, =, ≥, >, ≠ - - [ ] TRUE and MAYBE versions (null handling) - -*** TODO Projection (π) - Project relation onto subset of attributes. - - [ ] Remove specified columns - - [ ] Eliminate duplicate rows - - [ ] Preserve set semantics - -*** TODO Cartesian Product (×) - Cross product of two relations. - - [ ] Unrestricted concatenation - - [ ] Basis for joins - -*** DONE Natural Join (⋈) - CLOSED: [2025-01-22] - Join on common attributes. - - [X] Equi-join with duplicate removal (equijoin_iterator) - - [X] Nested loop join strategy - - [X] Attribute conflict resolution (right_ prefix) - - [X] Attribute-level provenance tracking - - [X] Comprehensive test coverage - -*** DONE Theta Join (⋈θ) - CLOSED: [2025-01-22] - Join with arbitrary comparison. - - [X] Support all theta operators via predicate functions - - [X] Generalizes natural join - - [X] Nested loop join with custom predicates - - [X] Provenance merging from both sides - -*** TODO Union (∪) - Set union of compatible relations. - - [ ] Union-compatible constraint - - [ ] Duplicate removal - -*** TODO Intersection (∩) - Set intersection. - - [ ] Union-compatible constraint - -*** TODO Difference (−) - Set difference. - - [ ] Union-compatible constraint - -*** TODO Divide (÷) - Relational division. - - [ ] Algebraic universal quantifier - -*** TODO Rename (ρ) - Attribute renaming. - - [ ] Enable self-joins - -** Advanced Features - -*** DONE Tuple-Level Lineage Tracking - CLOSED: [2025-01-23] - Track complete operational history of each tuple through query pipelines. - -**** Status: IMPLEMENTED - -**** API Usage - - Metadata tracking is ALWAYS enabled. All tuples include the 'meta' field: - #+BEGIN_SRC erlang - %% Simple query (metadata automatically included) - Iter = operations:get_tuples_iterator(DB, employees, #{}). - - %% With constraints (metadata still included) - Iter = operations:get_tuples_iterator(DB, employees, - #{constraints => #{age => {gt, 30}}}). - - %% Results always have: - %% #{id => 1, name => "Alice", - %% meta => #{ - %% provenance => #{id => {employees, id}, name => {employees, name}}, - %% lineage => {base, employees} - %% }} - #+END_SRC - -**** Provenance vs. Lineage - - - *Provenance* (IMPLEMENTED): Tracks immediate source of each attribute - #+BEGIN_SRC erlang - meta => #{ - provenance => #{ - name => {employees, name}, - dept_name => {departments, dept_name} - } - } - #+END_SRC - - - *Lineage* (IMPLEMENTED): Tracks complete operation tree that created the tuple - #+BEGIN_SRC erlang - meta => #{ - provenance => #{...}, % Attribute sources - lineage => {project, [name, dept_name], - {join, dept_id, - {select, fun(T) -> maps:get(age, T) > 30 end, - {base, employees}}, - {base, departments}}} - } - #+END_SRC - -**** Type Definition - - #+BEGIN_SRC erlang - -type lineage_op() :: - {base, atom()} % Base relation - | {select, fun(), lineage_op()} % Filter operation - | {project, [atom()], lineage_op()} % Projection - | {join, atom(), lineage_op(), lineage_op()} % Join on attribute - | {theta_join, fun(), lineage_op(), lineage_op()} % Join with predicate - | {sort, fun(), lineage_op()} % Sort operation - | {take, pos_integer(), lineage_op()} % Limit operation - | {aggregate, atom(), atom(), lineage_op()}. % Aggregation (future) - #+END_SRC - -**** Use Cases - - - [ ] *Updatable Views*: Propagate updates back to base relations - - Example: =UPDATE view SET name = "Bob"= → trace lineage → =UPDATE employees SET name = "Bob"= - - - [ ] *Incremental View Maintenance*: Identify affected tuples when base data changes - - Example: If employees tuple changes, lineage identifies which view tuples need recomputation - - - [ ] *Audit Trails*: Track how sensitive data was transformed - - Example: "This salary came from: employees → join(departments) → aggregate(avg)" - - - [ ] *Query Explanation*: Debug complex pipelines - - Example: "Why is this tuple here?" → inspect lineage to see operations applied - - - [ ] *Provenance Queries*: Query the lineage itself - - Example: "Show all tuples derived from employees.id=5" - -**** Implementation Plan - - 1. [X] Extend =tuple_metadata()= type with lineage field - 2. [X] Add lineage construction to each iterator operator - - [X] select_iterator: ={select, Predicate, ChildLineage}= - - [X] project_iterator: ={project, Attributes, ChildLineage}= - - [X] equijoin_iterator: ={join, Attr, LeftLineage, RightLineage}= - - [X] theta_join_iterator: ={theta_join, Pred, LeftLineage, RightLineage}= - - [X] sort_iterator: ={sort, CompareFun, ChildLineage}= - - [X] take_iterator: ={take, N, ChildLineage}= - 3. [X] Implement lineage merging in joins (combine operation trees) - 4. [ ] Add lineage querying API for provenance analysis (future) - 5. [ ] Use lineage for updatable view update propagation (future) - 6. [X] Add comprehensive lineage tests - -**** Relation to Existing Code - - Relation-level provenance already exists in =#relation.provenance=: - #+BEGIN_SRC erlang - -type provenance() :: - {base, atom()} - | {join, provenance(), provenance()} - | {select, provenance(), constraints()} - | {project, provenance(), [atom()]} - | {take, provenance(), pos_integer()}. - #+END_SRC - - This tracks where *relations* come from. Lineage is the *tuple-level* - equivalent, tracking operational history of individual tuples through - query pipelines. - -**** Example: Complete Lineage Chain - - #+BEGIN_SRC erlang - % Query: employees → select(age>30) → join(departments) → project([name, dept_name]) - - % Resulting tuple with full lineage: - #{name => "Alice", - dept_name => "Engineering", - meta => #{ - provenance => #{ - name => {employees, name}, - dept_name => {departments, dept_name} - }, - lineage => { - project, [name, dept_name], - {join, dept_id, - {select, fun(T) -> maps:get(age, T) > 30 end, - {base, employees}}, - {base, departments}}} - }} - - % From this lineage, we can: - % 1. Trace "Alice" back to employees.name - % 2. Know she passed the age>30 filter - % 3. See she was joined with departments on dept_id - % 4. Understand the projection removed other attributes - #+END_SRC - -*** TODO Null Value Handling - Three-valued logic for incomplete information. - - [ ] "Value unknown" null type - - [ ] "Property inapplicable" null type - - [ ] E-null for "entity unknown" - - [ ] Null substitution principle - - [ ] MAYBE operators - -*** TODO Infinite Relations (Aleph₀) - Countably infinite relation generators. - - [ ] Integer generator - - [ ] Arithmetic relations (plus, minus, multiply) - - [ ] Lazy evaluation with constraints - - [ ] Partially materialized storage - - [ ] User-defined generators - -*** TODO View Integration - Merging multiple perspectives. - - [ ] View definition language - - [ ] Automatic view maintenance - - [ ] View update translation - -*** TODO Temporal Support - Time-varying databases. - - [ ] Transaction time - - [ ] Valid time - - [ ] Bitemporal support - - [ ] Non-forgetting mode - -*** TODO Distributed Synchronization - Merkle tree-based replication. - - [ ] Efficient diff protocol - - [ ] Conflict resolution - - [ ] Eventual consistency - -** Developer Experience - -*** TODO Query Language - High-level relational query language. - - [ ] Algebraic syntax - - [ ] Tuple calculus variant - - [ ] Domain calculus variant - -*** TODO REPL Console - Interactive query environment. - - [ ] Live query evaluation - - [ ] Schema introspection - - [ ] Query history - -*** TODO Visualization Tools - Graphical representation. - - [ ] Relation browser - - [ ] Join graph visualization - - [ ] Generalization hierarchy diagrams - - [ ] Query execution plans - -*** TODO Org Babel Integration - Literate programming support. - - [ ] Execute relational queries in org-mode - - [ ] Export results to tables - - [ ] Reproducible analysis - -** Documentation & Validation - -*** DONE Code Documentation - CLOSED: [2025-01-21] - - [X] Module architecture overview - - [X] Data structure specifications - - [X] Usage examples - - [X] Implementation details - -*** TODO Theoretical Validation - Ensure correctness. - - [ ] Formal proofs of operator properties - - [ ] Closure verification - - [ ] Idempotence tests - - [ ] Property-based testing with PropEr - - [ ] Comparison with Date & Darwen semantics - -*** TODO Research Papers - Link to foundational theory. - - [ ] Codd 1970: "A Relational Model" - - [ ] Codd 1979: "Extending the Database Relational Model" (RM/T) - - [ ] Codd 1985: "Does AlOL Need the Relational Algebra?" - - [ ] Date & Darwen: "Foundation for Future Database Systems" - -** References - - E. F. Codd (1979). "Extending the Database Relational Model to Capture More Meaning" - - E. F. Codd (1970). "A Relational Model of Data for Large Shared Data Banks" - - C. J. Date & Hugh Darwen. "Foundation for Future Database Systems: The Third Manifesto" diff --git a/docs/infinite-relations.puml b/docs/infinite-relations.puml deleted file mode 100644 index cd6aa0f..0000000 --- a/docs/infinite-relations.puml +++ /dev/null @@ -1,177 +0,0 @@ -@startuml infinite-relations -!theme plain -title Infinite Type Relations: Unfold Pattern & Membership - -abstract class InfiniteTypeRelation { - + name: atom() - + cardinality: aleph_zero | continuum - + erlang_type: type() - + membership_predicate: function() - + unfold_generator: function() - + constraints: constraints() -} - -class Naturals { - Erlang Type: integer() - Membership: natural[X] :- - erlang:is_integer(X), - X >= 0. - - Unfold Generator: - unfold(0, fun(N) -> N + 1 end) - → 0, 1, 2, 3, ... - - Cardinality: aleph_zero -} - -class Integers { - Erlang Type: integer() - Membership: integer[X] :- - erlang:is_integer(X). - - Unfold Generator: - unfold({0, 1}, fun({N, S}) -> - case S of - 1 -> {N, -1}; - -1 -> {N+1, 1} - end - end) - → 0, 1, -1, 2, -2, ... - - Cardinality: aleph_zero -} - -class Rationals { - Erlang Type: {integer(), integer()} - Membership: rational[X] :- - X is (P, Q), - integer[P], integer[Q], - Q ≠ 0. - - Unfold Generator: - Stern-Brocot tree unfold - → (0,1), (1,1), (1,2), ... - - Cardinality: aleph_zero -} - -class Reals { - Erlang Type: float() - Membership: real[X] :- - erlang:is_float(X). - - Unfold Generator: - IEEE 754 float enumeration - (impractical, continuum) - - Cardinality: continuum -} - -class Strings { - Erlang Type: string() - Membership: string[X] :- - erlang:is_list(X), - all_chars(X). - - Unfold Generator: - Length-ordered, lexicographic - → "", "a", "b", ..., "aa", ... - - Cardinality: aleph_zero -} - -class Plus { - Erlang Type: {integer(), integer(), integer()} - Membership: plus[A, B, Sum] :- - integer[A], integer[B], - Sum is A + B. - - Unfold Generator: - Diagonalization of ℤ × ℤ - → (0,0,0), (0,1,1), (1,0,1), ... - - Cardinality: continuum (ℤ × ℤ) -} - -package "Constraint Application" { - class ConstrainedGenerator { - Pattern: Apply constraints during unfold - base_generator: unfold() - constraints: [constraint()] - .. - filter_unfold(Gen, Constraints) -> - filter(Gen, satisfies_all(Constraints)) - } - - note bottom of ConstrainedGenerator - **Example 1: Bounded Naturals** - natural[X], X >= 0, X =< 100 - → Generates: 0, 1, 2, ..., 100 (finite!) - - **Example 2: Constrained Plus** - plus[5, B, 12] - → Solves: B = 7 - → Generates: single tuple (5, 7, 12) - - **Example 3: Range Query** - integer[X], X >= -10, X =< 10 - → Generates: 0, 1, -1, 2, -2, ..., 10, -10 - end note -} - -package "Composite Type Relations (Views)" { - class Complex { - Type Definition (Karuta): - complex[X] :- - X is (A, B), - real[A], real[B]. - - Implementation: - Unfold real × real with - product enumeration - - Not primitive: Defined as view - over primitive real relation - } -} - -InfiniteTypeRelation <|-- Naturals -InfiniteTypeRelation <|-- Integers -InfiniteTypeRelation <|-- Rationals -InfiniteTypeRelation <|-- Reals -InfiniteTypeRelation <|-- Strings -InfiniteTypeRelation <|-- Plus - -Naturals --> ConstrainedGenerator: apply\nconstraints -Integers --> ConstrainedGenerator -Rationals --> ConstrainedGenerator -Plus --> ConstrainedGenerator - -Reals --> Complex: used in\nproduct -Complex : (view relation) - -note right of Naturals - **Core Pattern:** Infinite relations use unfold - to generate members. Primitive types are - infinite relations. - - **Membership:** Erlang type + constraints - - **Unfold Pattern:** - unfold(Seed, Step) generates infinite sequence: - Seed, Step(Seed), Step(Step(Seed)), ... - - This enables lazy evaluation and - constraint-based pruning. -end note - -note left of Plus - **Function Relations:** - Mathematical functions like plus, multiply, etc. - are relations with continuum cardinality. - - Membership = evaluation - Generation = enumeration -end note - -@enduml 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 diff --git a/docs/iterator-pipeline.puml b/docs/iterator-pipeline.puml deleted file mode 100644 index 810ef63..0000000 --- a/docs/iterator-pipeline.puml +++ /dev/null @@ -1,45 +0,0 @@ -@startuml iterator-pipeline -!theme plain -title Volcano Iterator Model - Process Pipeline - -component "Scan Iterator\n(Process)" as P1 { - [Read from Relation] as S1 -} - -component "Select Iterator\n(Process)" as P2 { - [Apply Predicate] as S2 -} - -component "Project Iterator\n(Process)" as P3 { - [Filter Attributes] as S3 -} - -component "Sort Iterator\n(Process)" as P4 { - [Sort All Tuples] as S4 -} - -component "Take Iterator\n(Process)" as P5 { - [Limit N Tuples] as S5 -} - -P1 -right-> P2: {next, Pid}\n{tuple, T} | done -P2 -right-> P3: {next, Pid}\n{tuple, T} | done -P3 -right-> P4: {next, Pid}\n{tuple, T} | done -P4 -right-> P5: {next, Pid}\n{tuple, T} | done - -note bottom of P1 - Each iterator is an - independent Erlang process - - Message passing protocol: - - Request: {next, CallerPid} - - Response: {tuple, Data} | done - - Benefits: - - Lazy evaluation - - Memory-bounded - - Composable - - Concurrent -end note - -@enduml diff --git a/docs/karuta-interface-layers.puml b/docs/karuta-interface-layers.puml deleted file mode 100644 index cd5443e..0000000 --- a/docs/karuta-interface-layers.puml +++ /dev/null @@ -1,65 +0,0 @@ -@startuml karuta-interface-layers -!theme plain -title Karuta Interface Architecture Layers - -actor "Karuta Program" as Karuta - -package "Language Bindings" { - [Karuta FFI] as FFI - [Erlang Ports] as Ports - [NIF (Native)] as NIF -} - -package "Stable Contract Layer" { - component "domino.erl" as DominoAPI { - [create_database/1] - [execute/2] - [query/2] - [transaction/2] - } -} - -package "Command Processor" { - [Command Parser] as CmdParser - [Validator] as Validator - [Executor] as Executor -} - -package "Implementation Layer" { - component "operations.erl" as Ops { - [create_relation/3] - [create_tuple/3] - [get_tuples_iterator/2] - [etc...] - } -} - -database "Mnesia Storage" as Storage - -Karuta --> FFI -Karuta --> Ports -Karuta --> NIF - -FFI --> DominoAPI -Ports --> DominoAPI -NIF --> DominoAPI - -DominoAPI --> CmdParser -CmdParser --> Validator -Validator --> Executor - -Executor --> Ops -Ops --> Storage - -note right of DominoAPI - Stable, versioned interface - Command format: - {Verb, Entity, Name, Parameters} - - Examples: - {create, relation, employee, Schema} - {insert, tuple, employee, Data} - {query, relation, employee, Constraints} -end note - -@enduml diff --git a/docs/merkle-tree-hierarchy.puml b/docs/merkle-tree-hierarchy.puml deleted file mode 100644 index 4e86e26..0000000 --- a/docs/merkle-tree-hierarchy.puml +++ /dev/null @@ -1,50 +0,0 @@ -@startuml merkle-tree-hierarchy -!theme plain -title Merkle Tree Hierarchy - -package "Database Level" { - [Database Hash] as DBHash - database "Merkle Tree of Relations" as DBTree -} - -package "Relation Level" { - [Relation Hash 1] as R1Hash - [Relation Hash 2] as R2Hash - [Relation Hash N] as RNHash - - database "Merkle Tree of Tuples (R1)" as R1Tree - database "Merkle Tree of Tuples (R2)" as R2Tree -} - -package "Tuple Level" { - [Tuple Hash 1.1] as T11 - [Tuple Hash 1.2] as T12 - [Tuple Hash 2.1] as T21 - [Tuple Hash 2.2] as T22 -} - -DBHash --> DBTree -DBTree --> R1Hash -DBTree --> R2Hash -DBTree --> RNHash - -R1Hash --> R1Tree -R2Hash --> R2Tree - -R1Tree --> T11 -R1Tree --> T12 -R2Tree --> T21 -R2Tree --> T22 - -note bottom of DBHash - Single hash represents - entire database state - - Benefits: - - Version control - - Efficient diffing - - Distributed sync - - Integrity verification -end note - -@enduml diff --git a/docs/module-dependencies.puml b/docs/module-dependencies.puml deleted file mode 100644 index dcc955b..0000000 --- a/docs/module-dependencies.puml +++ /dev/null @@ -1,39 +0,0 @@ -@startuml module-dependencies -!theme plain -title Module Dependencies - -package "Entry Points" { - [main.erl] as Main - [repl.erl] as REPL -} - -package "Server Layer" { - [xml_server_app.erl] as XMLApp - [xml_server.erl] as XMLServer -} - -package "Query Layer" { - [query_planner.erl] as Planner -} - -package "Core Layer" { - [operations.erl] as Ops -} - -package "Support Modules" { - [relation.erl] as Relation - [generators.erl] as Generators - [visualizer.erl] as Visualizer -} - -Main --> XMLApp -XMLApp --> XMLServer -XMLServer --> Planner -REPL --> Ops - -Planner --> Ops -Ops --> Relation -Ops --> Generators -Ops --> Visualizer - -@enduml diff --git a/docs/provenance-lineage.puml b/docs/provenance-lineage.puml deleted file mode 100644 index 4e8f68a..0000000 --- a/docs/provenance-lineage.puml +++ /dev/null @@ -1,69 +0,0 @@ -@startuml provenance-lineage -!theme plain -title Provenance and Lineage Tracking - -component "Base Tuple\n(employee)" as T1 - -note right of T1 - **Data:** - id = 1 - name = "Alice" - age = 30 - salary = 100000 - - **Meta:** - provenance: - id: (employee, id) - name: (employee, name) - age: (employee, age) - salary: (employee, salary) - lineage: (base, employee) -end note - -component "After Select\n(age > 25)" as T2 - -note right of T2 - **Data:** - id = 1 - name = "Alice" - age = 30 - salary = 100000 - - **Meta:** - provenance: (same as above) - lineage: - select - fun(T) -> age > 25 end - (base, employee) -end note - -component "After Project\n[name, age]" as T3 - -note right of T3 - **Data:** - name = "Alice" - age = 30 - - **Meta:** - provenance: - name: (employee, name) - age: (employee, age) - lineage: - project - [name, age] - (select, _, (base, employee)) -end note - -T1 -down-> T2: select operation\nadds to lineage -T2 -down-> T3: project operation\nfilters provenance - -note bottom of T3 - **Benefits:** - - Data source tracking - - Query result explanation - - Reproducibility - - Debugging support - - Foundation for updatable views -end note - -@enduml diff --git a/docs/query-execution-flow.puml b/docs/query-execution-flow.puml deleted file mode 100644 index 998b0e2..0000000 --- a/docs/query-execution-flow.puml +++ /dev/null @@ -1,54 +0,0 @@ -@startuml query-execution-flow -!theme plain -title Query Execution Flow - -actor Client -participant "Query Planner" as Planner -participant "Scan Iterator" as Scan -participant "Select Iterator" as Select -participant "Project Iterator" as Project -participant "Operations API" as Ops -database "Mnesia" as DB - -Client -> Planner: query({project,\n {select, {scan, employee}, Pred},\n [name, age]}) -activate Planner -Planner -> Planner: parse & validate -Planner -> Scan: spawn_iterator(employee) -activate Scan -Planner -> Select: spawn_iterator(Scan, Pred) -activate Select -Planner -> Project: spawn_iterator(Select, [name, age]) -activate Project -Planner --> Client: {ok, Iterator} -deactivate Planner - -Client -> Project: next_tuple() -Project -> Select: next_tuple() -Select -> Scan: next_tuple() -Scan -> Ops: get_tuples_iterator(employee) -Ops -> DB: transaction(read tuple) -DB --> Ops: {ok, Tuple} -Ops --> Scan: {ok, Tuple} -Scan --> Select: {ok, Tuple} -Select -> Select: apply Predicate -Select --> Project: {ok, Tuple} -Project -> Project: filter attributes -Project --> Client: {ok, #{name => "Alice", age => 30}} - -Client -> Project: next_tuple() -Project -> Select: next_tuple() -Select -> Scan: next_tuple() -Scan -> Ops: get_tuples_iterator(employee) -Ops -> DB: transaction(read tuple) -DB --> Ops: done -Ops --> Scan: done -Scan --> Select: done -Select --> Project: done -Project --> Client: done - -Client -> Project: close_iterator() -deactivate Project -deactivate Select -deactivate Scan - -@enduml diff --git a/docs/reactive-queries.puml b/docs/reactive-queries.puml deleted file mode 100644 index bcba5d5..0000000 --- a/docs/reactive-queries.puml +++ /dev/null @@ -1,51 +0,0 @@ -@startuml reactive-queries -!theme plain -title Reactive Queries (Live Subscriptions) - -participant "Client" as C -participant "Subscription Manager" as SM -participant "Domino" as D -database "employee relation" as E - -C -> SM: subscribe(query: "age > 30") -activate SM -SM -> D: register_subscription(employee, predicate) -activate D -D -> E: initial query -E --> D: [{name: "Alice", age: 35}] -D --> SM: initial results -SM --> C: [{name: "Alice", age: 35}] -deactivate D -deactivate SM - -... time passes ... - -C -> D: insert(employee, {name: "Bob", age: 32}) -activate D -D -> D: check affected subscriptions -D -> D: evaluate predicate on new tuple\n(32 > 30? yes) -D -> SM: notify(subscription_id, {inserted: "Bob"}) -activate SM -SM -> C: delta: {inserted: {name: "Bob", age: 32}} -deactivate SM -deactivate D - -C -> D: insert(employee, {name: "Charlie", age: 25}) -activate D -D -> D: evaluate predicate\n(25 > 30? no) -D -> D: no notification needed -deactivate D - -note right of SM - Subscription tracks: - - Relation(s) to watch - - Filter predicate - - Client callback - - On mutation: - 1. Check which subscriptions affected - 2. Evaluate predicate on changed tuples - 3. Send delta (not full re-query) -end note - -@enduml diff --git a/docs/reliability_roadmap.org b/docs/reliability_roadmap.org deleted file mode 100644 index d47a00e..0000000 --- a/docs/reliability_roadmap.org +++ /dev/null @@ -1,223 +0,0 @@ -#+TITLE: Sakura Reliability Roadmap (Precise) - -* Scope - -Build Sakura into a correct and efficient first-order predicate logic (FOPL) -relational algebra engine where relations are first-class values with: - -- *Extension* :: denotation as a tuple set (finite stored set or generated stream) -- *Intension* :: logical meaning (schema + normalized constraints + derivation) - -* Formal Position on Issue =#48= - -Issue =#48= is *not* semantic redundancy. - -- =constraint:create_1op/3= is an attribute-constraint *definition* constructor. -- =constraint:add_attribute_constraint/3= is a relation-level *binding* operation. - -They are distinct layers. The defect is API ambiguity and weak invariants. - -- [ ] Require key/record coherence: key =:= =#attribute_constraint.attribute=. -- [ ] Provide one canonical "declare and bind" path to prevent invalid states. - -* Relation Contract (Non-Negotiable) - -** C1 Representation Contract - -- [ ] Exactly one extension mode per relation: - - finite stored: =tree =/= undefined= and =generator= is factory for tree iterator - - generated: =tree == undefined= and =generator= is mandatory -- [ ] Intension is always =#relation_constraints{}=, never raw =#{}=. -- [ ] =membership_criteria= is either removed (Issue =#47=) or treated as a derived cache from constraints, never a second source of truth. - -** C2 Identity Contract - -- [ ] Relation hash function is canonical and identical across all mutation paths. -- [ ] Hash input includes the same semantic fields in the same order, with explicit versioned format. -- [ ] Any relation update that changes intension or extension must change hash deterministically. - -** C3 Algebraic Closure Contract - -- [ ] Every algebra operator returns a relation with valid extension + intension. -- [ ] Constraint propagation rules are explicit and tested per operator. -- [ ] Result schema and constraints are compatible and normalized. - -* Current Critical Correctness Gaps - -- [ ] Non-canonical relation hash updates in =src/operations.erl=. -- [ ] Split semantics between =constraints= and =membership_criteria=. -- [ ] Mixed constraints shapes (=#relation_constraints{}= and raw maps). -- [ ] Placeholder substitution search in =constraint:find_satisfying_substitution/4=. -- [ ] Derived infinite/finite relations not consistently honoring constraints (=#13=, =#14=). -- [ ] Dual planner paths with mismatched behavior in =src/query_planner.erl=. -- [ ] Iterator close protocol mismatch (=stop= vs =close= forms). -- [ ] XML schema endpoint assumes map constraints and crashes. - -* Workstreams - -** W0 Safety and Determinism (P0) - -- [ ] Fix =xml_server= SCHEMA serialization for record constraints (=src/xml_server.erl=). -- [ ] Replace ad-hoc prints with =logger= (=#39=), remove debug output in constraint lookup. -- [ ] Make =repl:start/0= non-destructive; add explicit destructive reset command. -- [ ] Standardize iterator termination protocol across all iterator loops. -- [ ] Normalize constraints type in all constructors (planner/operators/operations). - -*Acceptance criteria* - -- [ ] No SCHEMA crash under any built-in relation set. -- [ ] No unsolicited stdout noise during normal queries. -- [ ] No relation loss on default REPL startup. -- [ ] No orphan iterator processes after collect/close paths. - -** W1 FOPL Semantics Core (P1) - -- [ ] Implement full variable binding search and substitution for partial constraints. -- [ ] Define and enforce formula AST for =and/or/not/exists/forall=. -- [ ] Separate logical membership from physical storage existence checks. -- [ ] Decide and document two-valued logic policy (no NULL) or explicit three-valued policy. -- [ ] Complete 1OPiC modeling (=#42=) and baseline 1OP constraints (=#28=). - -*Acceptance criteria* - -- [ ] Quantified constraints produce correct truth values on finite fixtures. -- [ ] Membership equivalence tests pass for stored vs generated extension of same intension. -- [ ] Constraint violation diagnostics identify failing attribute/formula branch. - -** W2 Constraint Model Consistency (P1) - -- [ ] Resolve =#48= with scope-safe API (define vs bind) and strict invariant checks. -- [ ] Implement relation creation with constraints in one call (=#15=). -- [ ] Decide fate of =membership_criteria= (=#47=): remove or strict derivation cache. -- [ ] Add migration helper to convert legacy constraint maps to =#relation_constraints{}=. -- [ ] Establish extension/intension introspection API for debugging and tooling. - -*Acceptance criteria* - -- [ ] No public path can construct mismatched attribute constraint key/record pairs. -- [ ] New relation creation API supports schema + constraints atomically. -- [ ] Intension is serialized/deserialized in one normalized shape everywhere. - -** W3 Planner Unification (P1) - -- [ ] Remove dual compile paths; keep one logical -> rewrite -> physical pipeline. -- [ ] Add semantic validation (schema compatibility, attribute existence, constraint shape). -- [ ] Add rewrite rules: projection pruning, predicate pushdown, limited join reordering. -- [ ] Add typed planner errors for REPL/XML consumers. - -*Acceptance criteria* - -- [ ] Same query plan always yields same output schema and row semantics across interfaces. -- [ ] Planner rejects invalid plans with stable machine-readable reasons. - -** W4 Algebra Completeness and Performance (P2) - -- [ ] Implement union/intersection/difference with strict compatibility checks. -- [ ] Implement semijoin/antijoin/division. -- [ ] Add hash join and merge join; keep nested loop fallback. -- [ ] Enforce bounded execution preconditions for blocking operators over infinite relations. -- [ ] Improve tuple hash retrieval path performance (=#7=). - -*Acceptance criteria* - -- [ ] Algebra law regression tests pass for finite relations (where laws apply). -- [ ] Join strategy selection is observable and benchmarked. -- [ ] Infinite + blocking plans fail fast with actionable diagnostics unless bounded. - -** W5 Versioning and Updatable Views (P2) - -- [ ] Implement branch metadata and lineage (=#43=). -- [ ] Implement fast-forward merge semantics and conflict checks (=#44=). -- [ ] Implement provenance-safe updatable ephemeral views (=#26=). - -*Acceptance criteria* - -- [ ] Branch/merge operations are deterministic and test-covered. -- [ ] Updatable views reject ambiguous write-back paths. - -** W6 Interfaces and Hardening (P2) - -- [ ] Replace XML =erl_eval= execution with safe parsed DSL/AST. -- [ ] Version protocol responses and provide structured errors. -- [ ] Add explain-analyze metrics (rows, time, strategy, spills/materialization). -- [ ] Add visualizer mode for relation semantics (schema, constraints, lineage, extension mode). -- [ ] Integrate or deprecate =relation.erl= helper model. - -*Acceptance criteria* - -- [ ] No arbitrary code execution path through external query interface. -- [ ] Interface responses are stable under malformed input and concurrency. - -* GitHub Issue Mapping - -** Core reliability and semantics - -- [ ] =#39= logging -- [ ] =#15= define constraints at finite relation creation -- [ ] =#14= derived finite from infinite honors/inherits constraints -- [ ] =#13= derived infinite honors constraints -- [ ] =#7= tuple hash retrieval performance - -** Constraint/data model - -- [ ] =#48= clarify define/bind API and enforce invariants -- [ ] =#47= remove/replace membership_criteria split -- [ ] =#42= proper 1OPiC model -- [ ] =#28 #29 #30 #31= 1st/2nd/3rd/4th order property constraints - -** Versioning and updates - -- [ ] =#43= branching -- [ ] =#44= fast-forward merge -- [ ] =#26= updatable views - -** Optional research tracks - -- [ ] =#45= nullary relations vs booleans -- [ ] =#40= state monad -- [ ] =#41= C node for hot loops -- [ ] =#19= chessboard integration - -* Verification Matrix (Must Exist in CI) - -- [ ] Unit tests: constraints AST eval, membership semantics, hash determinism -- [ ] Property tests: algebra laws, hash stability, propagation invariants -- [ ] Integration tests: REPL flows, XML QUERY/NEXT/CLOSE/SCHEMA, malformed inputs -- [ ] Performance tests: join algorithms, bounded infinite queries, Merkle hash retrieval -- [ ] Concurrency tests: iterator lifecycle and server session cleanup - -* Milestones and Exit Criteria - -** M1 (Safety Baseline) - -- Deliver W0 -- Close target issues: =#39 #15 #14 #13 #7= -- Exit: no destructive default startup, no XML schema crash, no protocol-level iterator leaks - -** M2 (Semantic Correctness) - -- Deliver W1 + W2 -- Close target issues: =#48 #47 #42 #28= (with foundations for =#29 #30 #31=) -- Exit: extension/intension invariants hold across create/query/derive flows - -** M3 (Planner and Performance) - -- Deliver W3 + W4 -- Exit: unified planner, bounded infinite behavior, measurable join improvements - -** M4 (Versioned Workflows) - -- Deliver W5 + W6 -- Close target issues: =#43 #44 #26= -- Exit: deterministic branch/merge and safe updatable views with stable interfaces - -* Execution Order - -1. W0 Safety and Determinism -2. W1 FOPL Semantics Core -3. W2 Constraint Model Consistency -4. W3 Planner Unification -5. W4 Algebra Completeness and Performance -6. W5 Versioning and Updatable Views -7. W6 Interfaces and Hardening -8. Optional research tracks (=#45 #40 #41 #19=) diff --git a/docs/roadmap.puml b/docs/roadmap.puml deleted file mode 100644 index 42ad8c2..0000000 --- a/docs/roadmap.puml +++ /dev/null @@ -1,72 +0,0 @@ -@startuml roadmap -!theme plain -title Suggested Implementation Roadmap - -package "Phase 1: Stable Interface (MVP)" { - [domino.erl wrapper] as P1_1 - [Command interface] as P1_2 - [Basic constraint validation] as P1_3 - [Karuta FFI bindings] as P1_4 -} - -package "Phase 2: Type System" { - [Fake-relations primitives] as P2_1 - [Constraint-based refinement] as P2_2 - [Subtype checking] as P2_3 - [Type inference] as P2_4 -} - -package "Phase 3: Advanced Constraints" { - [Foreign keys] as P3_1 - [Functional dependencies] as P3_2 - [Tuple/relation-level constraints] as P3_3 - [Transition constraints] as P3_4 -} - -package "Phase 4: Query Features" { - [Updatable views] as P4_1 - [Materialized views] as P4_2 - [Query optimization] as P4_3 - [Explain plans] as P4_4 -} - -package "Phase 5: Distribution" { - [Merkle sync] as P5_1 - [Multi-node replication] as P5_2 - [Partition strategies] as P5_3 - [Consistency protocols] as P5_4 -} - -package "Phase 6: Advanced Features" { - [Temporal queries] as P6_1 - [Reactive queries] as P6_2 - [Constraint solving] as P6_3 - [Datalog engine] as P6_4 -} - -P1_1 -down-> P2_1 -P1_2 -down-> P2_2 -P1_3 -down-> P3_1 -P1_4 -down-> P2_1 - -P2_1 -down-> P3_1 -P2_2 -down-> P3_2 -P2_3 -down-> P3_3 -P2_4 -down-> P4_1 - -P3_1 -down-> P4_1 -P3_2 -down-> P4_2 -P3_3 -down-> P4_3 -P3_4 -down-> P4_4 - -P4_1 -down-> P5_1 -P4_2 -down-> P5_2 -P4_3 -down-> P5_3 -P4_4 -down-> P6_1 - -P5_1 -down-> P6_1 -P5_2 -down-> P6_2 -P5_3 -down-> P6_3 -P5_4 -down-> P6_4 - -@enduml diff --git a/docs/system-overview.puml b/docs/system-overview.puml deleted file mode 100644 index 8d76fc5..0000000 --- a/docs/system-overview.puml +++ /dev/null @@ -1,81 +0,0 @@ -@startuml system-overview -!theme plain -title Domino System Overview - -package "Client Interfaces" { - [XML Server\n(TCP/IP Port 8080)] as XML - [REPL\n(Interactive Shell)] as REPL - [Direct API\n(Erlang Apps)] as API -} - -package "Query Processing Layer" { - package "Query Planner" { - [DSL Parser] as Parser - [Plan Validation\n& Compilation] as Validator - } - - package "Volcano Iterator Model" { - [Scan Iterator] as Scan - [Select Iterator] as Select - [Project Iterator] as Project - [Sort Iterator] as Sort - [Take Iterator] as Take - [Join Iterators] as Join - } -} - -package "Operations Layer (API)" { - [Database Management] as DBMgmt - [Relation Operations] as RelOps - [Tuple Operations] as TupleOps - [Iterator Management] as IterMgmt -} - -package "Data Model Layer" { - [Core Abstractions\nattribute, tuple,\nrelation, database_state] as CoreAbs - [Finite Relations\n(Merkle Trees)] as Finite - [Infinite Relations\n(Generators)] as Infinite -} - -package "Content-Addressed Storage" { - database "Mnesia" { - [attribute table] as AttrTable - [tuple table] as TupleTable - [relation table] as RelTable - [database_state table] as DBTable - } -} - -XML --> Parser -REPL --> Parser -API --> Parser - -Parser --> Validator -Validator --> Scan - -Scan --> Select -Select --> Project -Project --> Sort -Sort --> Take -Join --> Take - -Scan --> TupleOps -Select --> IterMgmt -Project --> IterMgmt - -DBMgmt --> CoreAbs -RelOps --> CoreAbs -TupleOps --> CoreAbs -IterMgmt --> CoreAbs - -CoreAbs --> Finite -CoreAbs --> Infinite - -Finite --> AttrTable -Finite --> TupleTable -Finite --> RelTable -Finite --> DBTable - -Infinite --> AttrTable - -@enduml diff --git a/docs/temporal-queries.puml b/docs/temporal-queries.puml deleted file mode 100644 index 7d72ed5..0000000 --- a/docs/temporal-queries.puml +++ /dev/null @@ -1,61 +0,0 @@ -@startuml temporal-queries -!theme plain -title Temporal Queries with Immutable Database States - -database "DB @ t0" as DB0 -note bottom of DB0 - hash = abc123... - timestamp = 2024-01-01 10:00 - - relations: - employee => hash_e0 -end note - -database "DB @ t1" as DB1 -note bottom of DB1 - hash = def456... - timestamp = 2024-01-01 11:00 - - relations: - employee => hash_e1 -end note - -database "DB @ t2" as DB2 -note bottom of DB2 - hash = ghi789... - timestamp = 2024-01-01 12:00 - - relations: - employee => hash_e2 -end note - -database "Current DB" as DB3 -note bottom of DB3 - hash = jkl012... - timestamp = 2024-01-01 13:00 - - relations: - employee => hash_e3 -end note - -DB0 -right-> DB1: insert tuple -DB1 -right-> DB2: update salary -DB2 -right-> DB3: delete tuple - -note top of DB0 - **Time Travel Queries:** - - query_at_time(2024-01-01 10:00) - → returns DB0 - - query_at_time(2024-01-01 12:00) - → returns DB2 - - diff(DB0, DB3) - → (inserted: [...], deleted: [...], modified: [...]) - - history(employee, id: 1) - → [(t0, state0), (t1, state1), (t2, state2)] -end note - -@enduml diff --git a/docs/transaction-algo.org b/docs/transaction-algo.org new file mode 100644 index 0000000..22903ec --- /dev/null +++ b/docs/transaction-algo.org @@ -0,0 +1,12 @@ +* Check if temporary file with the command hash with exists +To hash the command, we must hash its bytes without the timestamp, +since it will always vary given it's a transactional time, and add +instead the commit HEAD of the state of the database. + +If such file exists, load the transaction and storage offsets +alongside the command and attempt to write it as a recovery. +* Get the transaction offset of the transaction graph file AND storage file +* Write the offsets to a tmp file +* Write the command with a flag **flushed** set to false to a tmp file +* Attempt to execute the command +* Delete the temporary file diff --git a/docs/type-checking-flow.puml b/docs/type-checking-flow.puml deleted file mode 100644 index d1e6654..0000000 --- a/docs/type-checking-flow.puml +++ /dev/null @@ -1,108 +0,0 @@ -@startuml type-checking-flow -!theme plain -title Type Checking as Relation Membership Checking - -participant "Karuta Program" as K -participant "Type Checker" as TC -participant "Domino" as D -database "Type Relations\n(Infinite Relations)" as TR - -note over K,TR - **Type Checking:** Check if value is member of type relation - **Type Relations:** Primitives stored as infinite relations - **Membership:** Erlang type check + constraint satisfaction -end note - -K -> TC: insert(employee, {age: 25, name: "Alice"}) -activate TC - -TC -> D: check: natural[25]? -activate D -D -> TR: membership query: natural[25] -activate TR -TR -> TR: 1. Erlang type check:\n is_integer(25) → true -TR -> TR: 2. Constraint check:\n 25 >= 0 → true -TR --> D: true (25 ∈ natural) -deactivate TR -D --> TC: member ✓ -deactivate D - -TC -> D: check: non_empty_string["Alice"]? -activate D -D -> TR: membership query: non_empty_string["Alice"] -activate TR -TR -> TR: 1. Check string["Alice"]:\n is_list("Alice") ∧ all_chars → true -TR -> TR: 2. Constraint check:\n length("Alice") > 0 → true -TR --> D: true ("Alice" ∈ non_empty_string) -deactivate TR -D --> TC: member ✓ -deactivate D - -TC --> K: type_check passed ✓\n{age: 25, name: "Alice"} ∈ employee -deactivate TC - -== Type Check Failure Example == - -K -> TC: insert(employee, {age: -5, name: ""}) -activate TC - -TC -> D: check: natural[-5]? -activate D -D -> TR: membership query: natural[-5] -activate TR -TR -> TR: 1. Erlang type check:\n is_integer(-5) → true -TR -> TR: 2. Constraint check:\n -5 >= 0 → false ✗ -TR --> D: false (-5 ∉ natural) -deactivate TR -D --> TC: not_member ✗ -deactivate D - -TC --> K: type_error: -5 ∉ natural\nExpected: natural[Age]\nGot: Age = -5 -deactivate TC - -== Composite Type Example == - -K -> TC: check: complex[(3.14, 2.71)]? -activate TC - -TC -> D: check: complex[(3.14, 2.71)]? -activate D -note over D - complex[X] :- - X is (A, B), - real[A], real[B]. -end note - -D -> TR: membership query: real[3.14] -activate TR -TR -> TR: is_float(3.14) → true -TR --> D: true (3.14 ∈ real) -deactivate TR - -D -> TR: membership query: real[2.71] -activate TR -TR -> TR: is_float(2.71) → true -TR --> D: true (2.71 ∈ real) -deactivate TR - -D --> TC: member ✓\n(3.14, 2.71) ∈ complex -deactivate D - -TC --> K: type_check passed ✓ -deactivate TC - -note right of TR - **Type Relation Storage:** - - Primitives: infinite relations - - Membership: predicate evaluation - - No materialization needed - - Lazy constraint checking - - **Example:** - natural[X] is stored as: - - erlang_type: integer() - - constraint: X >= 0 - - generator: unfold(0, +1) -end note - -@enduml diff --git a/docs/type-hierarchy.puml b/docs/type-hierarchy.puml deleted file mode 100644 index c53a965..0000000 --- a/docs/type-hierarchy.puml +++ /dev/null @@ -1,289 +0,0 @@ -@startuml type-hierarchy -!theme plain -title Type System: Stratified Universes & Types as Relations - -package "Universe Stratification" { - class "Universe₀" as U0 { - Base values - Examples: 3, -5, 3.14, true, "hello" - The set of all runtime values - } - - class "Universe₁" as U1 { - Type relations (classify values) - Examples: natural, integer, real, boolean - Each type is a relation over Universe₀ - Type relations are infinite relations - } - - class "Universe₂" as U2 { - Type of type relations - The classifier of type relations - Prevents self-reference paradoxes - } - - class "Universe₃" as U3 { - Meta-type level - Type : Universe₂ : Universe₃ - } - - U0 : Universe₁ - U1 : Universe₂ - U2 : Universe₃ - U3 : Universe₄ - - note right of U1 - **Stratification prevents Russell's Paradox** - Type relations live in Universe₁ - and classify values in Universe₀. - A type cannot contain itself. - - natural : Universe₁ - 3 ∈ natural (3 ∈ Universe₀) - But: natural ∉ natural ✗ (universe mismatch) - end note -} - -package "Supertypes (Universe₁)" { - class Number { - Membership: number[X] where X : Universe₀ - Definition: Union of all numeric types - number[X] :- natural[X]; integer[X]; - rational[X]; real[X]. - Allows polymorphism over numeric types - Universe level: Universe₁ - } - - class Scalar { - Membership: scalar[X] where X : Universe₀ - Definition: Atomic (non-composite) values - scalar[X] :- number[X]; boolean[X]; string[X]. - Universe level: Universe₁ - } -} - -package "Numeric Type Relations (Universe₁)" { - class Naturals { - Membership: natural[X] where X : Universe₀ - Criteria: - - X is erlang:integer() - - X >= 0 - Cardinality: aleph_zero - Generator: 0, 1, 2, 3, ... - Universe level: Universe₁ - } - - class Integers { - Membership: integer[X] where X : Universe₀ - Criteria: - - X is erlang:integer() - Cardinality: aleph_zero - Generator: 0, 1, -1, 2, -2, ... - Universe level: Universe₁ - } - - class Rationals { - Membership: rational[X] where X : Universe₀ - Criteria: - - X is (P, Q) - - integer[P], integer[Q] - - Q ≠ 0 - Cardinality: aleph_zero - Generator: Stern-Brocot tree - Universe level: Universe₁ - } - - class Reals { - Membership: real[X] where X : Universe₀ - Criteria: - - X is erlang:float() - Cardinality: continuum - Generator: IEEE 754 floats - Universe level: Universe₁ - } -} - -package "Other Primitive Types (Universe₁)" { - class Strings { - Membership: string[X] where X : Universe₀ - Criteria: - - X is erlang:string() - Cardinality: aleph_zero - Ordering: by length, then lexicographic - Universe level: Universe₁ - } - - class Booleans { - Membership: boolean[X] where X : Universe₀ - Criteria: - - X is erlang:boolean() - - X ∈ {true, false} - Cardinality: 2 - Universe level: Universe₁ - } -} - -package "Constrained Type Relations (Universe₁)" { - class PositiveIntegers { - Definition: positive_int[X] where X : Universe₀ - Criteria: - - integer[X] - - X > 0 - Relation: positive_int ⊆ integer - Universe level: Universe₁ - } - - class BoundedInt { - Definition: bounded_int[X, Min, Max] - where X : Universe₀ - Criteria: - - integer[X] - - Min ≤ X ≤ Max - Relation: bounded_int ⊆ integer - Universe level: Universe₁ - } - - class NonEmptyStrings { - Definition: non_empty_string[X] - where X : Universe₀ - Criteria: - - string[X] - - length(X) > 0 - Relation: non_empty_string ⊆ string - Universe level: Universe₁ - } -} - -package "Composite Type Relations (Universe₁)" { - class Complex { - Definition (Karuta-style): - complex[X] where X : Universe₀ - complex[X] :- - X is (A, B), - real[A], real[B]. - - Interpretation: - - (A, B) where A is real part - - B is imaginary part - Relation: complex ⊆ real × real - Universe level: Universe₁ - } - - class Employee { - Definition: - employee[X] where X : Universe₀ - employee[X] :- - X is (Name, Age, Salary), - non_empty_string[Name], - positive_int[Age], - positive_int[Salary]. - - Relation: employee ⊆ string × ℕ⁺ × ℕ⁺ - Universe level: Universe₁ - } -} - -' Universe stratification relationships -U1 --> U0 : classifies values in -U2 --> U1 : types type relations -U3 --> U2 : meta-level - -' All type relations live in Universe₁ -U1 ..> Number : contains -U1 ..> Naturals : contains -U1 ..> Integers : contains -U1 ..> Rationals : contains -U1 ..> Reals : contains -U1 ..> Booleans : contains -U1 ..> Strings : contains -U1 ..> Scalar : contains - -' Type relation hierarchy (within Universe₁) -Number <|-- Naturals : ⊇ -Number <|-- Integers : ⊇ -Number <|-- Rationals : ⊇ -Number <|-- Reals : ⊇ - -Number <|-- Scalar : ⊇ -Booleans <|-- Scalar : ⊇ -Strings <|-- Scalar : ⊇ - -' Subset relations among numeric types -Naturals .up.|> Integers : ⊆ -Integers .up.|> Rationals : ⊆ -Rationals .up.|> Reals : ⊆ - -' Constrained types -Integers .down.|> PositiveIntegers : ⊇ -Integers .down.|> BoundedInt : ⊇ -Strings .down.|> NonEmptyStrings : ⊇ - -' Composite types (also in Universe₁) -Number .down.|> Complex : number × number -Complex : (view: pair of numbers) - -Scalar .down.|> Employee : scalar × scalar × scalar -Employee : (view: string × nat × nat) - -note right of Complex - **Views as Type Relations:** - Types can be defined as relational views - over other type relations. - - Example using supertype: - complex[C] :- C is (R, I), - number[R], number[I]. - - Or more specifically: - complex[C] :- C is (R, I), - real[R], real[I]. - - Views can use supertypes for flexibility! - All views live in Universe₁. -end note - -note left of Number - **Core Principle:** Every type is a relation - Type checking = membership checking in relations - T1 <: T2 iff T1 ⊆ T2 (subset relation) - - **Supertypes enable polymorphism:** - A function can accept number[X] and work - with naturals, integers, rationals, or reals. - - **Universe Levels:** - All type relations: Universe₁ - All values: Universe₀ - Type of types: Universe₂ - - **Erlang Type Mapping:** - natural → integer() + (≥ 0) - integer → integer() - rational → {integer(), integer()} - real → float() - string → string() - boolean → boolean() -end note - -note bottom of U0 - **Avoiding Russell's Paradox:** - - Like F*, Domino uses predicative universe - stratification. The key invariant: - - Type u#i : Type u#(i+1) - - In Domino: - - Values (3, "hello", true) : Universe₀ - - Type relations (natural, string) : Universe₁ - - Type : Universe₂ - - This prevents: - natural ∈ natural (universe mismatch!) - - A type relation cannot be a member of itself. - All type relations classify values in Universe₀ - but exist at Universe₁. -end note - -@enduml -- cgit v1.2.3