|
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 |
3 | 2 |
|
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. |
10 | 4 |
|
11 | | -link:docs/krl_map.html[→ KRL architecture map (HTML)] |
| 5 | +License: PMPL-1.0-or-later |
12 | 6 |
|
13 | | -== What it is |
| 7 | +--- |
14 | 8 |
|
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 |
18 | 10 |
|
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: |
24 | 12 |
|
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.* |
27 | 14 |
|
28 | | -== Architecture position |
| 15 | +Rather than treating programs as sequences of instructions, Tangle treats them as *composable topological objects*. |
29 | 16 |
|
30 | | -KRL is the surface language of a four-layer stack: |
| 17 | +This allows reasoning about programs in terms of: |
31 | 18 |
|
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 |
38 | 22 |
|
39 | | -The TanglePL module (this repo) is responsible for: |
| 23 | +--- |
40 | 24 |
|
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 |
45 | 26 |
|
46 | | -It is *not* responsible for: |
| 27 | +The central idea of Tangle is: |
47 | 28 |
|
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.* |
51 | 30 |
|
52 | | -== The four KRL operations |
| 31 | +In this setting: |
53 | 32 |
|
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"] |
55 | 52 | |=== |
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 |
76 | 66 | |=== |
77 | 67 |
|
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