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
|
#+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.
When goals remain that cannot run, two things can happen. If every
one of them 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.
|
