This repository contains experimental database systems built on mathematical foundations that go beyond traditional relational or document models.
The shared goal is:
to treat semantic identity as primary, rather than raw data equality.
These systems store and operate on structured objects where identity is determined by equivalence under transformation.
Traditional databases treat identity as:
equality of rows
equality of documents
equality of keys
In contrast, these systems treat identity as:
equivalence classes of structured objects.
This enables:
deduplication based on structure, not representation
queries over equivalence classes
indexing by invariants rather than raw values
explicit tracking of transformation history
An algebraic database using quandle structures as a semantic identity layer.
Objects are indexed by algebraic invariants derived from their structure
Designed for equivalence detection under transformation (e.g. knot isotopy)
Status: early-stage; core extraction and fingerprinting in progress.
A persistence and indexing layer for topological objects.
Stores canonical representations (e.g. TangleIR)
Maintains invariant caches
Tracks rewrite history and provenance
Status: active, undergoing refactoring.
A self-normalising multimodal database with formal verification goals.
Rust core with Elixir/OTP orchestration
Focus on correctness and reliability guarantees
Status: design phase.
Across these systems:
Structured objects are primary, not rows or documents
Equivalence is a first-class concept
Invariants are used for indexing and identity
Provenance and transformation history are explicitly stored
Query systems operate over equivalence classes
Minimal typed calculi can provide small, inspectable test cases for identity, provenance, derivation history, and equivalence-aware indexing
These databases are designed to pair with languages in nextgen-languages:
KRL → QuandleDB / Skein (topological objects)
Other languages → domain-specific storage and verification systems
The broader goal is a unified ecosystem where:
languages define construction and transformation
databases define identity and retrieval
TypeFix Zero is a calibration calculus — TF0 exists to make the minimal typed/Turing-complete boundary explicit. It is intentionally smaller than TypeLL and should not inherit TypeLL’s open-ended production obligations. Its one non-total primitive, fix, is the designated source of Turing completeness.
This repository represents ongoing research work.
Components vary in maturity:
some systems are partially implemented
others are specified but not yet built
formal obligations are documented but not fully discharged
See proof and specification documents for current guarantees and gaps.