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:

lexing and parsing (lib/lexer, lib/parser): one uniform node category under the delimiter law. The grammar does not decide what a name is.
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.
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.
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.
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:

lexicographic structural decrease across call graph components, with every measure position demanded ground at unfolding; self recursion and mutual recursion are the same check;
bounded enumeration through Between;
decidable negation and universals over decidable quantifiers;
residuation: open membership returns as residual constraints instead of failing the plan;
interval propagation over residue: contradictions fail, finite integer ranges enumerate;
symbolic discharge, first fragment: universals over infinite domains decided by kind inclusion, interval entailment, and the unit identities of the numeric relations, with refutations backed by counterexamples.

Not yet present: symbolic discharge beyond that fragment (richer algebraic theories, arithmetic decrease measures) and Rocq certificates as admission evidence. 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.