Skip to content

Commit 3198ab6

Browse files
Update README.adoc (#1)
1 parent 8da84d6 commit 3198ab6

1 file changed

Lines changed: 173 additions & 160 deletions

File tree

README.adoc

Lines changed: 173 additions & 160 deletions
Original file line numberDiff line numberDiff line change
@@ -1,178 +1,191 @@
1-
// SPDX-License-Identifier: PMPL-1.0-or-later
2-
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
1+
= Tangle / KRL — Topological Programming Language
32

4-
= KRL — Knot Resolution Language
5-
Jonathan Jewell (hyperpolymath)
6-
:toc: left
7-
:toc-title: Contents
8-
:doctype: article
9-
:icons: font
3+
A research language exploring *computation as topology*, where programs are structured objects and equivalence is defined by transformation.
104

11-
link:docs/krl_map.html[→ KRL architecture map (HTML)]
5+
License: PMPL-1.0-or-later
126

13-
== What it is
7+
---
148

15-
KRL (Knot Resolution Language) is a compositional language for constructing,
16-
transforming, resolving, and retrieving topological objects: tangles, knots,
17-
and links.
9+
== Overview
1810

19-
The name reflects the central operation: _resolution_.
20-
In knot theory, resolution is how crossings are resolved in the skein relation —
21-
the algebraic heart of invariant computation. KRL extends this to cover
22-
every interaction with the system: resolving structure, resolving equivalence,
23-
resolving queries.
11+
Tangle (via KRL — Knot Resolution Language) is an experimental programming language in which:
2412

25-
"Query" would name only one of four operations. "Resolution" names the mathematical
26-
act that runs through all of them.
13+
> *programs are structured as tangles (braids), and program equivalence is defined by isotopy.*
2714

28-
== Architecture position
15+
Rather than treating programs as sequences of instructions, Tangle treats them as *composable topological objects*.
2916

30-
KRL is the surface language of a four-layer stack:
17+
This allows reasoning about programs in terms of:
3118

32-
----
33-
KRL surface syntax ← this repository (TanglePL compiler module)
34-
TangleIR ← canonical interchange object
35-
VerisimMorphism ← abstract categorical view (VerisimCore)
36-
Skein.jl + QuandleDB ← persistence and semantic indexing
37-
----
19+
* structure
20+
* equivalence under transformation
21+
* invariants of representation
3822

39-
The TanglePL module (this repo) is responsible for:
23+
---
4024

41-
* Parsing KRL source text
42-
* Building and typechecking the AST
43-
* Compiling AST to `TangleIR`
44-
* Reconstructing source from IR (lossy but readable)
25+
== Core Idea
4526

46-
It is *not* responsible for:
27+
The central idea of Tangle is:
4728

48-
* Invariant computation (→ JuliaKnot.jl)
49-
* Persistence (→ Skein.jl)
50-
* Equivalence reasoning (→ QuandleDB)
29+
> *computation is construction of structured objects, and meaning is preserved under valid transformations.*
5130

52-
== The four KRL operations
31+
In this setting:
5332

54-
[cols="1,2,1,2"]
33+
* programs are graphs/braids
34+
* execution corresponds to transformation
35+
* equivalence is not syntactic equality, but *structural equivalence*
36+
37+
This aligns with concepts from:
38+
39+
* knot theory (Reidemeister moves)
40+
* category theory (morphisms and composition)
41+
* algebraic invariants (classification via structure)
42+
43+
---
44+
45+
== KRL — Knot Resolution Language
46+
47+
KRL is the surface language used to interact with the system.
48+
49+
It is organised around four fundamental operations:
50+
51+
[cols="1,3"]
5552
|===
56-
|Operation |Knot concept |Repo |Example syntax
57-
58-
|*Construct* |Tangles, ports, composition, tensor |TanglePL
59-
|`compose sigma1 sigma1` +
60-
`tensor a b` +
61-
`close t`
62-
63-
|*Transform* |PD code, Reidemeister moves |JuliaKnot.jl
64-
|`simplify t` +
65-
`normalise t` +
66-
`mirror t`
67-
68-
|*Resolve* |Isotopy, quandle, equivalence class |QuandleDB
69-
|`equivalent? a b` +
70-
`classify t` +
71-
`near t`
72-
73-
|*Retrieve* |Jones/Alexander invariants, indexed store |Skein.jl
74-
|`find where jones = p` +
75-
`where crossing < 8`
53+
|Operation |Role
54+
55+
|Construct
56+
|Build structured objects (tangles, compositions)
57+
58+
|Transform
59+
|Rewrite structures (e.g. simplification, normalisation)
60+
61+
|Resolve
62+
|Determine equivalence classes
63+
64+
|Retrieve
65+
|Query objects by invariants or structure
7666
|===
7767

78-
== Grammar (sketch)
79-
80-
----
81-
expr ::= atom
82-
| expr ';' expr (* sequential composition *)
83-
| expr '|' expr (* tensor product *)
84-
| 'close' expr (* closure / trace *)
85-
| 'mirror' expr
86-
| 'simplify' expr
87-
| 'let' IDENT '=' expr
88-
89-
atom ::= IDENT (* named tangle *)
90-
| generator
91-
92-
generator ::= 'sigma' INT (* positive crossing *)
93-
| 'sigma_inv' INT (* negative crossing *)
94-
| 'cup' INT (* cup on strands i,i+1 *)
95-
| 'cap' INT (* cap on strands i,i+1 *)
96-
97-
query ::= 'find' 'where' filter ('and' filter)*
98-
filter ::= IDENT '=' value
99-
| IDENT '<' INT
100-
| IDENT '>' INT
101-
----
102-
103-
== TangleIR — the canonical interchange
104-
105-
All KRL expressions compile to `TangleIR`. This is the object that flows
106-
between all layers of the stack:
107-
108-
[source,julia]
109-
----
110-
struct Port
111-
id::Symbol
112-
side::Symbol # :top | :bottom | :left | :right
113-
index::Int
114-
orientation::Symbol # :in | :out | :unknown
115-
end
116-
117-
struct CrossingIR
118-
id::Symbol
119-
sign::Int # +1 (positive) | -1 (negative)
120-
arcs::NTuple{4,Int} # PD-style: (a, b, c, d) arc indices
121-
end
122-
123-
struct TangleMetadata
124-
name::Union{String,Nothing}
125-
source_text::Union{String,Nothing}
126-
tags::Vector{String}
127-
provenance::Symbol # :user | :derived | :rewritten | :imported
128-
extra::Dict{Symbol,Any}
129-
end
130-
131-
struct TangleIR
132-
id::UUID
133-
ports_in::Vector{Port}
134-
ports_out::Vector{Port}
135-
crossings::Vector{CrossingIR}
136-
components::Vector{Vector{Int}} # arc index groups per component
137-
metadata::TangleMetadata
138-
end
139-
----
140-
141-
`TangleIR` is the single hardest-designed artifact in the stack.
142-
Every other interface is a view over it, a service to it, or a transformation of it.
143-
144-
== Usage
145-
146-
[source,julia]
147-
----
148-
using TanglePL, Skein
149-
150-
# parse and compile
151-
ir = compile_tangle("sigma1 ; sigma1 ; sigma1")
152-
153-
# store
154-
db = SkeinDB("knots.db")
155-
id = store!(db, ir; name="trefoil")
156-
157-
# query
158-
candidates = find_equivalence_candidates(db, ir)
159-
160-
# retrieve source
161-
src = reconstruct_source(ir) # generates valid KRL; not necessarily original
162-
----
163-
164-
== Status
165-
166-
* Grammar: defined (sketch above, formal PEG in progress)
167-
* AST: defined
168-
* Typechecker: boundary arity checking implemented
169-
* Compiler (AST → TangleIR): in development
170-
* Decompiler (IR → source): stub, in progress
171-
* Skein integration: planned
172-
173-
== Related
174-
175-
* link:../skein-jl/README.adoc[Skein.jl] — persistence and query
176-
* link:../quandle-db/README.adoc[QuandleDB] — semantic fingerprinting
177-
* link:../julia-knot/README.adoc[JuliaKnot.jl] — invariant engine
178-
* link:../nextgen-languages/README.adoc[Next-generation languages]
68+
KRL is not a general-purpose language; it is a *domain language for structured objects and their equivalence*.
69+
70+
---
71+
72+
== Architecture
73+
74+
Tangle is part of a layered system:
75+
76+
---
77+
78+
KRL (surface language)
79+
80+
TangleIR (canonical representation)
81+
82+
VerisimCore (categorical abstraction)
83+
84+
Skein / QuandleDB (storage and equivalence)
85+
-------------------------------------------
86+
87+
* *TangleIR* is the central representation shared across layers
88+
* other components provide views, transformations, or storage
89+
90+
---
91+
92+
== Formal Core
93+
94+
A core fragment of the language has been formalised and mechanised.
95+
96+
This includes:
97+
98+
* a typed core language (braid words, composition, tensor)
99+
* small-step operational semantics
100+
* mechanised proofs in Lean 4:
101+
102+
* progress
103+
* preservation
104+
* determinism
105+
* type safety
106+
107+
See:
108+
109+
* `Tangle.lean`
110+
* `docs/spec/FORMAL-SEMANTICS.md`
111+
112+
This formal core covers the *structural heart of the language*, though not all surface features.
113+
114+
---
115+
116+
== Current Status
117+
118+
Tangle/KRL is an *active research system*.
119+
120+
At present:
121+
122+
* grammar is defined (EBNF / PEG in progress)
123+
* AST and type system are partially implemented
124+
* compiler pipeline (AST → TangleIR) is in development
125+
* decompilation (IR → source) is incomplete
126+
* database integration (Skein / QuandleDB) is planned or partial
127+
128+
It should be read as:
129+
130+
> a formally grounded core with an evolving implementation and surrounding research system.
131+
132+
---
133+
134+
== Scope
135+
136+
=== Implemented / Grounded
137+
138+
* core grammar (defined)
139+
* AST and type structure
140+
* Lean formalisation of core fragment
141+
* partial compiler pipeline
142+
* example programs
143+
144+
---
145+
146+
=== In Progress
147+
148+
* parser and full compiler
149+
* IR integration across components
150+
* equivalence resolution via QuandleDB
151+
* invariant-based querying
152+
153+
---
154+
155+
=== Research Directions
156+
157+
* richer categorical abstractions
158+
* deeper integration with algebraic databases
159+
* optimisation via equivalence classes
160+
* alternative evaluation models based on rewriting
161+
162+
These are not yet stable features.
163+
164+
---
165+
166+
== Relationship to Other Projects
167+
168+
Tangle is closely connected to:
169+
170+
* *QuandleDB* — equivalence and classification via algebraic invariants
171+
* *Skein.jl* — persistence and indexing of structured objects
172+
* *Nextgen Languages* — broader research context
173+
174+
---
175+
176+
== How to Read This Repository
177+
178+
Recommended entry points:
179+
180+
* `Tangle.lean` — mechanised type safety proof
181+
* `docs/spec/FORMAL-SEMANTICS.md` — formal model
182+
* grammar files (`src/tangle.ebnf` or equivalent)
183+
* examples demonstrating composition and transformation
184+
185+
---
186+
187+
== Summary
188+
189+
Tangle/KRL is best understood as:
190+
191+
> 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.

0 commit comments

Comments
 (0)