Skip to content

README.adoc

Latest commit

 

History

History
216 lines (138 loc) · 5.98 KB

README.adoc

File metadata and controls

216 lines (138 loc) · 5.98 KB

Tangle / KRL — Topological Programming Language

OpenSSF Best Practices License: MPL-2.0 Green Web

A research language exploring computation as topology, where programs are structured objects and equivalence is defined by transformation.

Overview

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

Core Idea

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 — Knot Resolution Language

KRL is the surface language used to interact with the system — a resolution DSL, not merely a query language.

It is organised around four fundamental operations:

Operation Role

Construct

Create or declare presentations, structures, claims, datasets

Transform

Rewrite, normalize, compose, concatenate, permute, mutate

Resolve

Decide / disambiguate / evaluate equivalence or identity questions

Retrieve

Inspect, fetch, project, explain, or return stored/computed results

KRL is not a general-purpose language; it is a domain language for structured objects and their equivalence. Retrieve recovers resolution-relevant artefacts (presentations, invariants, witnesses, equivalence classes, prior resolutions, explanations, provenance) — it is not arbitrary database querying. See krl docs/decisions/0002-query-language-deferred.adoc.

Architecture

Tangle is part of a layered system:

KRL (surface language — resolution DSL, not merely a query language) ↓ TangleIR (canonical interchange representation) ↓ Tangle core (this repo — proven type-safe small-step semantics) ↓ QuandleDB + Skein.jl (persistence + invariant/equivalence; computational engine)

* *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
  * decidability of type checking (`infer` ≡ `HasType`)

* *echo types* — structured loss as a type-system feature: `close` (braid
  closure) is the canonical lossy map, and `echoClose`/`lower`/`residue` make
  that loss recoverable at the type level (a simply-typed shadow of
  hyperpolymath/echo-types). All four safety theorems cover them.

See:

* `proofs/Tangle.lean` (and `proofs/README.md` to build/verify)
* `docs/spec/FORMAL-SEMANTICS.md`
* `PROOF-NARRATIVE.md` / `PROOF-NEEDS.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.


== License

This project is licensed under the Mozilla Public License, v. 2.0. See the `LICENSE` file for details.

SPDX-License-Identifier: MPL-2.0