A research language exploring computation as topology, where programs are structured objects and equivalence is defined by transformation.
Tangle (via KRL — Knot Resolution Language) is an experimental programming language in which:
programs are structured as tangles (braids), and program equivalence is defined by isotopy.
Rather than treating programs as sequences of instructions, Tangle treats them as composable topological objects.
This allows reasoning about programs in terms of:
-
structure
-
equivalence under transformation
-
invariants of representation
The central idea of Tangle is:
computation is construction of structured objects, and meaning is preserved under valid transformations.
In this setting:
-
programs are graphs/braids
-
execution corresponds to transformation
-
equivalence is not syntactic equality, but structural equivalence
This aligns with concepts from:
-
knot theory (Reidemeister moves)
-
category theory (morphisms and composition)
-
algebraic invariants (classification via structure)
KRL is the surface language used to interact with the system.
It is organised around four fundamental operations:
| Operation | Role |
|---|---|
Construct |
Build structured objects (tangles, compositions) |
Transform |
Rewrite structures (e.g. simplification, normalisation) |
Resolve |
Determine equivalence classes |
Retrieve |
Query objects by invariants or structure |
KRL is not a general-purpose language; it is a domain language for structured objects and their equivalence.
Tangle is part of a layered system:
KRL (surface language) ↓ TangleIR (canonical representation) ↓ VerisimCore (categorical abstraction) ↓ Skein / QuandleDB (storage and equivalence)
* *TangleIR* is the central representation shared across layers * other components provide views, transformations, or storage --- == Formal Core A core fragment of the language has been formalised and mechanised. This includes: * a typed core language (braid words, composition, tensor) * small-step operational semantics * mechanised proofs in Lean 4: * progress * preservation * determinism * type safety See: * `Tangle.lean` * `docs/spec/FORMAL-SEMANTICS.md` This formal core covers the *structural heart of the language*, though not all surface features. --- == Current Status Tangle/KRL is an *active research system*. At present: * grammar is defined (EBNF / PEG in progress) * AST and type system are partially implemented * compiler pipeline (AST → TangleIR) is in development * decompilation (IR → source) is incomplete * database integration (Skein / QuandleDB) is planned or partial It should be read as: > a formally grounded core with an evolving implementation and surrounding research system. --- == Scope === Implemented / Grounded * core grammar (defined) * AST and type structure * Lean formalisation of core fragment * partial compiler pipeline * example programs --- === In Progress * parser and full compiler * IR integration across components * equivalence resolution via QuandleDB * invariant-based querying --- === Research Directions * richer categorical abstractions * deeper integration with algebraic databases * optimisation via equivalence classes * alternative evaluation models based on rewriting These are not yet stable features. --- == Relationship to Other Projects Tangle is closely connected to: * *QuandleDB* — equivalence and classification via algebraic invariants * *Skein.jl* — persistence and indexing of structured objects * *Nextgen Languages* — broader research context --- == How to Read This Repository Recommended entry points: * `Tangle.lean` — mechanised type safety proof * `docs/spec/FORMAL-SEMANTICS.md` — formal model * grammar files (`src/tangle.ebnf` or equivalent) * examples demonstrating composition and transformation --- == Summary Tangle/KRL is best understood as: > a research language that treats programs as structured objects, with meaning defined by transformation and equivalence, supported by a partially mechanised formal core and an evolving implementation.