#+TITLE: The VM
* About
This document describes the first working version of the Sol
pipeline: parser, loader, admission checks and solver. A program goes
from text to answers entirely inside the library; the binary in
=bin/= is a thin host that links the standalone world, exactly as
decision 4 prescribes. RNT embeds the same engine by satisfying the
=WORLD= module type with its own catalog.
* Surface
The parser produces one uniform node category. Atoms and variables
share a spelling, so classification happens at loading, by context: a
name in term position is a variable, a block is a proposition, and a
top level bare block asserts a fact. Directives are message sends:
#+BEGIN_SRC sol
Relation named: Person schema: #( [name domain: String] [age domain: Integer] )
[Person name: "Marcos" age: 30]
Rule name: "adult" head: [Adult name: N] body:
[Person name: N age: A] :and [GreaterEqual left: A right: 18]
Query expression: [Adult name: N]
#+END_SRC
Delimiters follow the law of the specification: =[]= for
propositions, ={}= for records, =#()= for sequences, =()= for
grouping. =:or= binds looser than =:and=.
* Loading is admission
A program only becomes a world if everything in it is admitted:
- facts must be ground, match their schema exactly, and satisfy each
attribute domain. This is integrity control at load time, the same
membership check it always is. A Natural is an Integer and an
Integer is a Rational, literally.
- recursion must exhibit a lexicographic structural decrease.
Admission groups rule defined relations into strongly connected
components of the call graph and searches for an ordered list of
labels such that every call inside the component strictly shrinks
at some position, all earlier positions staying equal. Self
recursion is the one label case, like =T= inside =#(H | T)=;
mutual recursion like Even and Odd passing a shrinking list back
and forth is admitted the same way. The measure is stamped on the
recursive rules as their witness. No measure, no world.
- every referenced relation must exist, either builtin or declared.
This is rung one of the evidence ladder in decision 10. Bounded
quantification exists through =Between=; symbolic discharge and Rocq
certificates are future rungs.
* Solving
The solver works by dynamic goal selection. At each step it runs any
goal decidable under the current bindings; goals that are not yet
decidable wait. So conjunction stays commutative in fact, not just in
doctrine: the page order of =:and= operands never matters, and the
tests assert it.
When goals remain that cannot run, the engine first propagates over
the waiting membership constraints as one interval store. Bounds
with an empty intersection fail the branch outright: =X > 5= with
=X < 3= answers no, not a conditioned maybe, and so does asking one
value to be both an integer and a string. An integer variable
squeezed into a finite range converts to bounded generation:
=[Natural value: X] :and [LessThan left: X right: 4]= enumerates 0
through 3, the same admissible enumeration =Between= performs
explicitly, because the combination of constraints is a finite
relation. This is Sakura's cardinality analysis working inside the
engine.
If propagation finds neither a contradiction nor a finite range, two
things can happen. If every waiting goal is pure membership,
decidable the moment its variables ground, the answer comes back
with those goals as residual constraints: =[Integer value: X]= alone
answers =X= conditioned on =[Integer value: X]=, which is exactly
what the expression means. Constraining is not searching. If any
remaining goal is a stalled search, an unbounded recursion or an
infinite universal, the plan is rejected as non total. Membership is
never generation either way.
Recursive rules unfold only when their witness argument is ground, so
the admission proof becomes a runtime termination measure: the
witness shrinks structurally at every unfolding and the search
bottoms out.
* Negation and quantifiers
=:not= is decidable denial. =u :not d= establishes the universe =u=
and then refutes =d=; the denial only runs when its variables are
ground, deferring like any other goal, so negation as failure over
open goals cannot happen.
=Exists= lowers to a conjunction at loading, since query variables
are existential already; its =variable:= is renamed apart so the
scope cannot be forged. =ForAll= runs when its quantifier is
decidable: every solution of the quantifier must satisfy the body. A
universal over an infinite domain is a non total plan, rejected, as
decision 10 requires. Variables that live only under a universal are
not answer variables.
* Membership criteria as domains
A schema attribute is constrained by a primitive domain or by a
criterion: any relational expression with exactly one free variable,
the subject, bound to the attribute value at admission.
#+BEGIN_SRC sol
Relation named: Employee schema: #(
[name domain: String]
[dept domain: ([Department id: D])]
[score domain: ([Natural value: S] :and [LessThanEqual left: S right: 100])]
)
#+END_SRC
A foreign key is the criterion =([Department id: D])=, nothing more
special than that. Criteria run against the complete extension, so
the order facts appear in the source does not matter, the same way a
committed state is judged whole. A fact whose attribute fails its
criterion is an integrity violation and the program gets no world.
* Builtins
Domains check membership once ground: Integer, Natural, Rational,
String. Equality unifies. Plus and Times evaluate forward and solve
backward through the rationals, and results collapse to minimal
shape, so =[Plus left: 1/2 right: 1/2 result: R]= binds =R= to the
integer =1=. Comparisons decide once both sides are ground. Between
is the one relation allowed to enumerate, because its range is finite
by construction.
* Embedding
The solver is a functor over the =WORLD= module type: a host answers
=find= for its own relations and links the engine in-process. The
embedding test builds a toy kernel catalog in plain OCaml, compiles
query text through =World.expr_of_node=, and runs the same solver
with the same totality guard. That is the RNT shape: Sakura compiles
Sol (and Karuta lowered to Sol) to expressions, the kernel's catalog
answers =find=, and no process boundary exists.
* Running
=sol file.sol= loads the program and prints each query's answers.
=sol= alone is a REPL where declarations accumulate and queries run
immediately. Answers print as variable bindings in Sol notation, or
=yes.= and =no.= for closed queries.
