#+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.
- a recursive rule must exhibit a structurally decreasing argument:
some label whose call argument sits strictly inside the head
argument, like =T= inside =#(H | T)=. The label is kept as the
rule's witness. No witness, no world.
- mutual recursion between relations is rejected for now. Self
recursion with a witness is the admitted form.
- 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.
If no remaining goal can ever run, the plan is rejected as non
total. =[Integer value: X]= alone is not an enumeration, it is an
error telling you to bind or bound =X=. Membership is not generation.
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.
* 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.
* 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.
