KRL — Knot Resolution Language

Contents

• What it is
• Architecture position
• The four KRL operations
• Grammar (sketch)
• TangleIR — the canonical interchange
• Usage
• Status
• Related

→ KRL architecture map (HTML)

What it is

KRL (Knot Resolution Language) is QuandleDB’s canonical resolution DSL: a database-facing language whose domain is knot/tangle identity, equivalence, transformation, and disambiguation. It is the user- and author-facing language for constructing, transforming, resolving, and retrieving knot/tangle presentations, invariants, fingerprints, equivalence classes, witnesses, and disambiguation results.

The name reflects the central operation: resolution. In knot theory, resolution is how crossings are resolved in the skein relation — the algebraic heart of invariant computation. KRL extends this to cover every interaction with the system: resolving structure, resolving equivalence, resolving queries.

KRL is database-facing but not merely a query language. "Query" would name only one of four operations; "resolution" names the mathematical act that runs through all of them. Two framings to avoid: "a database language" alone wrongly suggests SQL-for-knots, and "a surface DSL over Tangle" alone makes QuandleDB incidental and KRL too compiler-ish. KRL is precisely QuandleDB’s resolution DSL — it lowers through TangleIR into Tangle-level computation, with QuandleDB and Skein.jl as its persistence and computation backends.

Architecture position

KRL is the surface language of a federated resolution stack. Each layer answers a distinct question:

Layer	Role — and the question it answers
KRL (this repository)	User-/author-facing resolution DSL. "What question or claim are we making about knot-structured identity?" Spec, ABI, FFI scaffolds; implementations in KRLAdapter.jl (canonical) and quandledb/server/krl/.
TangleIR	Lowered intermediate representation. "What normalized computational object represents that resolution task?" Defined in KRLAdapter.jl, consumed by hyperpolymath/tangle.
Tangle	Full computational / programming substrate. "What executable knot-theoretic program or transformation system carries this out?" Proven type-safe small-step semantics (hyperpolymath/tangle/proofs/Tangle.lean).
QuandleDB	Persistence + invariant/equivalence database. "Where presentations, invariants, fingerprints, equivalence classes, witnesses, and results live." (hyperpolymath/quandledb)
Skein.jl	Computational / backend library. "One engine that computes, transforms, normalizes, or evaluates the objects." (hyperpolymath/Skein.jl)

This repo is responsible for:

• The KRL grammar specification (spec/grammar.ebnf).

• Idris2 ABI types (src/interface/Abi/).

• Zig FFI scaffolds (src/interface/ffi/).

• Example programs (examples/).

• The proof narrative (PROOF-NARRATIVE.md) and obligations registry.

The actual KRL parser, lowering, and adapter implementations live in the companion repos KRLAdapter.jl (canonical) and quandledb/server/krl/ (server-side query parser — different role). See PROOF-NARRATIVE.md for the two-implementation rationale and the equivalence obligation KR-6.

KRL is not responsible for:

• Invariant computation (→ JuliaKnot.jl)

• Persistence (→ Skein.jl)

• Equivalence reasoning (→ QuandleDB)

• Surface-language implementation (→ KRLAdapter.jl)

The four KRL operations

KRL has exactly four operations. The four-verb shape is deliberate: it stops "querying" from becoming the whole identity of the language.

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 or computed results

Operation	Knot concept	Primary site	Example syntax
Construct	Tangles, ports, composition, tensor	TanglePL	compose sigma1 sigma1 tensor a b close t
Transform	PD code, Reidemeister moves	JuliaKnot.jl	simplify t normalise t mirror t
Resolve	Isotopy, quandle, equivalence class	QuandleDB	equivalent? a b classify t near t
Retrieve	Invariants, witnesses, stored resolutions	Skein.jl + QuandleDB	find where jones = p where crossing < 8

Note

Retrieve is not arbitrary database querying. It recovers resolution-relevant artefacts: presentations, invariants, witnesses, equivalence classes, prior resolutions, explanations, and provenance. Generic data access — arbitrary filters, dashboards, reporting, analytics, exploratory search, index tuning — is an engine-layer affordance (Skein.jl predicates over SQLite; QuandleDB’s filtered endpoints), deliberately not elevated to a KRL operation or a rival query language. A separate query language is deferred, not absent; see docs/decisions/0002-query-language-deferred.adoc for the rationale and trigger conditions.

Grammar (sketch)

expr     ::= atom
           | expr ';' expr          (* sequential composition *)
           | expr '|' expr          (* tensor product *)
           | 'close' expr           (* closure / trace *)
           | 'mirror' expr
           | 'simplify' expr
           | 'let' IDENT '=' expr

atom     ::= IDENT                  (* named tangle *)
           | generator

generator ::= 'sigma' INT           (* positive crossing *)
           | 'sigma_inv' INT        (* negative crossing *)
           | 'cup' INT              (* cup on strands i,i+1 *)
           | 'cap' INT              (* cap on strands i,i+1 *)

query    ::= 'find' 'where' filter ('and' filter)*
filter   ::= IDENT '=' value
           | IDENT '<' INT
           | IDENT '>' INT

TangleIR — the canonical interchange

All KRL expressions compile to TangleIR. This is the object that flows between all layers of the stack:

struct Port
    id::Symbol
    side::Symbol        # :top | :bottom | :left | :right
    index::Int
    orientation::Symbol # :in | :out | :unknown
end

struct CrossingIR
    id::Symbol
    sign::Int           # +1 (positive) | -1 (negative)
    arcs::NTuple{4,Int} # PD-style: (a, b, c, d) arc indices
end

struct TangleMetadata
    name::Union{String,Nothing}
    source_text::Union{String,Nothing}
    tags::Vector{String}
    provenance::Symbol  # :user | :derived | :rewritten | :imported
    extra::Dict{Symbol,Any}
end

struct TangleIR
    id::UUID
    ports_in::Vector{Port}
    ports_out::Vector{Port}
    crossings::Vector{CrossingIR}
    components::Vector{Vector{Int}}  # arc index groups per component
    metadata::TangleMetadata
end

TangleIR is the single hardest-designed artifact in the stack. Every other interface is a view over it, a service to it, or a transformation of it.

Usage

using TanglePL, Skein

# parse and compile
ir = compile_tangle("sigma1 ; sigma1 ; sigma1")

# store
db = SkeinDB("knots.db")
id = store!(db, ir; name="trefoil")

# query
candidates = find_equivalence_candidates(db, ir)

# retrieve source
src = reconstruct_source(ir)   # generates valid KRL; not necessarily original

Status

• Grammar: defined (sketch above, formal PEG in progress)

• AST: defined

• Typechecker: boundary arity checking implemented

• Compiler (AST → TangleIR): in development

• Decompiler (IR → source): stub, in progress

• Skein integration: planned

Related

• Skein.jl — persistence and query

• QuandleDB — semantic fingerprinting

• JuliaKnot.jl — invariant engine

• Next-generation languages