core design and pipeline document

1 files changed, 129 insertions, 0 deletions

diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org
new file mode 100644
index 0000000..9e085f8
--- /dev/null
+++ b/docs/core-design-and-pipeline.org
@@ -0,0 +1,129 @@
+#+TITLE: Core Design and Pipeline
+
+* About
+
+This document explains why Sol is built the way it is and what the
+pipeline does to a program, stage by stage. It builds on the language
+specification, on the decisions in the integration document, and on
+the implementation in =lib/=, which realizes the first version of
+every stage described here.
+
+* Why Sol is not Turing complete
+
+A database must answer. A query language with unbounded recursion or
+unbounded search imports the halting problem into every question you
+ask it, and the guarantee that RNT's execution core is named after
+disappears. Sol refuses that trade at the language level, not by
+convention.
+
+The bet behind the refusal: the programs a database language actually
+needs are total. Arithmetic, aggregation, structural recursion over
+finite data, integrity checking, parsing, normalization, all of it
+lives comfortably inside primitive recursion. What genuinely needs
+partiality does not belong in the database; it belongs in the
+application layer, and Karuta keeps it there.
+
+* Where Sol sits among its ancestors
+
+- From Prolog: relations as the unit of meaning, unification as the
+  join mechanism, rules as definition. Removed: unbounded search,
+  negation as failure over open goals, the cut, and every other
+  operational leak that makes Prolog programs mean what the
+  interpreter does instead of what the logic says.
+- From Datalog: the discipline that queries over finite data
+  terminate. Added: structured terms (records, sequences), real
+  arithmetic with backward solving, and recursion beyond
+  stratification, admitted per rule by a termination proof.
+- From Coq: totality as an admission requirement, not a hope. A rule
+  without a decrease witness has the same status as a non
+  structurally recursive Fixpoint: it does not enter the system.
+  Rocq later takes the metatheory itself (decision 10).
+- From relational algebra: the finite first order fragment is plan
+  shaped, and lowering to RNT's FOL core (Codd's theorem justifies
+  the move) is a performance decision, never a semantic one
+  (decision 9).
+
+* Types are membership, membership is proof
+
+Sol has no type layer beside the logic. =[Integer value: X]= is a
+proposition, a constraint, and a typing judgment at once; a schema
+criterion like =([Natural value: S] :and [LessThanEqual left: S
+right: 100])= is a dependent refinement checked by the solver against
+the same semantics every query uses. Foreign keys, range checks and
+type checks are one mechanism, membership, applied at different
+moments. Subtyping is proven inclusion (decision 12); values keep
+one canonical shape so inclusion is literal, never coerced.
+
+* The three modes of a relation
+
+The implementation keeps the specification's central distinction
+mechanical:
+
+- membership :: decidable check of a ground tuple. Domains check
+  against the host; stored relations scan; rule relations unfold.
+- constraint :: a goal not yet decidable waits. The planner defers
+  it, other goals bind its variables, and it runs when ground.
+- generation :: only bounded forms may enumerate. =Between= is the
+  first; every future generator must carry its bound in its
+  arguments.
+
+A goal that fits none of the three is a non total plan and the query
+is rejected with the stuck goals named. Nothing diverges, nothing
+silently enumerates an infinite domain.
+
+* The pipeline
+
+Source text moves through these stages, each one total:
+
+1. lexing and parsing (=lib/lexer=, =lib/parser=): one uniform node
+   category under the delimiter law. The grammar does not decide
+   what a name is.
+2. classification and resolution (=lib/world=): context decides.
+   Names in term position become variables; blocks become
+   applications; =Exists= lowers to conjunction; quantified
+   variables rename apart, unforgeably.
+3. admission (=lib/world=, =lib/program=): the gate where totality
+   is enforced. Schemas register; facts must be ground, match their
+   schema, satisfy primitive domains immediately and membership
+   criteria against the complete extension; recursive rules must
+   exhibit a structural decrease witness; mutual recursion is cut;
+   every reference must resolve. A program that passes admission
+   owns a world; one that does not, does not exist as a program.
+4. planning and solving (=lib/vm=): dynamic goal selection over the
+   admitted world. Selection is the plan; it reorders freely because
+   conjunction is commutative, and it re-derives executability as
+   bindings grow, which is what makes rule unfolding safe: the
+   witness argument is ground and strictly shrinking at every
+   unfolding.
+5. reading answers: solutions are the query's free variables
+   resolved to canonical terms.
+
+Sakura's fuller pipeline (cardinality tags, join ordering, TAKE,
+lowering to =Plan.t=) refines stages 3 and 4 without changing their
+meaning; the =WORLD= functor is the seam it plugs into.
+
+* Totality strategies, honestly ranked
+
+What the implementation enforces today is rung one and part of rung
+two of the ladder in decision 10:
+
+- structural decrease on self recursive rules, with the witness
+  demanded ground at unfolding;
+- bounded enumeration through =Between=;
+- decidable negation and universals only over decidable quantifiers.
+
+Not yet present: symbolic discharge (algebraic proof of universals
+over infinite domains), Rocq certificates as admission evidence,
+mutual recursion under a lexicographic measure, and a constraint
+store that residuates instead of rejecting. Each arrives as a
+strengthening of admission or planning; none changes the semantics
+of what is already admitted.
+
+* What embedding means
+
+The engine is a library over =WORLD= (decision 4). The standalone
+binary is one host with an in-memory catalog and no transitions. RNT
+is the other host: its catalog answers =find=, queries arrive as
+compiled expressions through =World.expr_of_node=, and commit stays
+the kernel's single effect outside the language. The embedding test
+in =test/test_embedding.ml= is the working sketch of that shape.