KRL (pronounced "curl") is the resolution language for QuandleDB. This repository holds its normative specification; the implementation lives in QuandleDB.
QuandleDB is a knot database — a database whose stored objects are knots and tangles, and whose intended identity relation is equivalence under ambient isotopy rather than byte equality. KRL is the language you use to work with it.
The point of a dedicated language is that the interesting questions about a knot database are hard ones — is this the same knot, what class does it fall in, what witnesses the answer — and you should be able to ask them directly rather than assembling them out of general-purpose data access. Record retrieval is one operation within KRL, because without it you could not get at anything; it is not what KRL is for.
The name reflects the central operation. In knot theory, resolution is how crossings are resolved in the skein relation — the algebraic heart of invariant computation. KRL generalises the word to every interaction with the system: resolving structure, resolving equivalence, retrieving relevant evidence.
Related projects, developed for different purposes:
| Project | What it is |
|---|---|
The knot database. Stores presentations, invariants, fingerprints, equivalence classes and witnesses. |
|
KRL (this repository) |
QuandleDB’s resolution language. Specified here, implemented in |
Independent Julia library for knot storage, indexing and invariant computation; used by QuandleDB. |
|
Independent Julia mathematical toolkit for diagrams, braids, invariants and transformations. |
|
A separate, general language for knot mathematics — topological, algebraic, geometric and logical. Turing-complete; not a backend for KRL. |
KRL and QuandleDB were designed together and are deliberately close. Tangle is a different project with a different remit that happens to share the subject matter. The two are related by domain, not by architecture: KRL does not compile to, lower into, or depend on Tangle.
|
Important
|
Earlier revisions of this README described a |
KRL has four operation families. The four-verb shape is deliberate: it stops "querying" from becoming the whole identity of the language.
| Operation | Knot concept | What it does |
|---|---|---|
construct |
Tangles, ports, composition, tensor |
create or declare presentations, structures, claims, datasets |
transform |
PD code, Reidemeister moves |
rewrite, normalise, compose, concatenate, permute, mutate |
resolve |
Isotopy, quandle, equivalence class |
decide, disambiguate, or evaluate equivalence and identity questions |
retrieve |
Invariants, witnesses, stored resolutions |
inspect, fetch, project, explain, or return stored or computed results |
|
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, index tuning — is an engine-layer affordance, deliberately not elevated to a KRL operation. No additional public language is precommitted; see the retrieval boundary decision. |
-
The grammar specification (
spec/grammar.ebnf). -
Idris2 ABI declarations (
src/interface/Abi/). -
A Zig FFI shim over the C ABI (
src/interface/ffi/). -
Example programs (
examples/*.krl). -
The proof narrative (
PROOF-NARRATIVE.adoc) and obligations registry.
It does not hold a parser or evaluator. Those are in
quandledb/server/krl/: a Julia lexer, parser, AST and evaluator, with a
separate compatibility frontend. These implement a fragment; they do not yet
execute all four operation families.
For a high-level proof progress summary, see PROOF-PROGRESS.adoc.
Assessed against what is in this tree, not against absent work.
| Component | State |
|---|---|
Grammar specification |
Drafted ( |
Examples |
Four |
Idris2 ABI |
Declared — 4 |
Zig FFI |
Compiles; 3/3 unit tests pass; |
Parser / evaluator |
Not in this repository (see above) |
Conformance suite |
Executable retrieval-fragment acceptance/rejection corpus in |
There is no parser here, so nothing in this repository can execute a KRL
program. tests/smoke/grammar_smoke.sh performs lexical-level checking only and
says so.
spec/SURFACES.adoc distinguishes the construction/resolution
draft from QuandleDB’s executable retrieval/candidate fragment. In the
former, | is tensor composition; in the latter it separates stages. These are
separately scoped contracts, not interchangeable grammars.
Run the fragment’s acceptance/rejection corpus against a concrete implementation:
julia --startup-file=no tests/conformance/retrieval_fragment.jl /path/to/quandledb
The evaluator’s resolution-boundary tests additionally reject demands for exact, sufficient or necessary assurance from an index bucket. Heuristic candidates remain available with an explicit warning. Full resolution syntax and witness checking are still implementation obligations.