1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
#+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:
- 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.
|
