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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
|
#+TITLE: Sol
Sol is a total relational language inspired by Prolog, Coq, relational
algebra, constraint logic programming, and the message-oriented syntax
of Smalltalk.
The project explores a language where relations are the primary
semantic objects, types are expressed as membership criteria, and
execution is understood as proof search, constraint propagation, and
normalization.
Sol is intentionally not Turing complete. Its purpose is not to encode
arbitrary partial computation, but to provide a disciplined environment
for total relational computation, dependent relational typing, and
integrity-preserving constraint systems.
* Design
** Language Specification
The first document defines the surface language and its semantics.
See: [[file:docs/language-specification.org][docs/language-specification.org]]
This document covers:
- core syntax;
- atoms, labels, variables, literals, and blocks;
- relation applications;
- explicit conjunction and disjunction;
- joins through unification;
- domains as unary relations;
- infinite domains as membership constraints rather than enumerators;
- membership criteria;
- constraints as relations;
- existential and universal quantification;
- recursion and totality;
- higher-order relations;
- primary and secondary type systems.
This is the foundational document for Sol as a language.
** Sol / Sakura / RNT Integration
This document records the normative architectural decisions binding
Sol to the Sakura relational engine and the RNT database kernel.
See: [[file:docs/sakura-RNT-integration.org][docs/sakura-RNT-integration.org]]
It covers:
- totality as a stack-wide invariant (the Turing-complete PPL idea is
retracted; partiality lives in the application layer);
- Sol as the database language and runtime, with Karuta compiling to
it;
- the sublanguages (DRL, ICL, DCL, DML, DDL, TCL) as semantic
fragments of Sol rather than separate surface languages;
- transitions (DML, DDL, DCL) as relations over first-class,
content-addressed branch states;
- commit (advancing a branch tip) as the single primitive effect —
the kernel arbitrates only the tip; conflict policy is DCL;
- Sol as a host-neutral library over a =WORLD= interface, linked
in-process by RNT as its higher-order execution engine and by a
thin standalone host;
- sequencing by linear state threading (Mercury-style), never by
syntactic order;
- state-scoped reads (=at:=);
- plan selection by analysis (no DRL surface syntax);
- totality established at admission via a closed evidence ladder,
with checkers verified in Rocq;
- the catalog as ordinary queryable relations;
- subtyping as proven relation inclusion, intensional relation
identity, and canonical representatives for quotient domains.
** Core Design Principles and Pipeline Specification
This document has not been written yet.
It should describe the deeper design principles behind Sol and the
compiler/interpreter pipeline needed to preserve totality.
Expected topics include:
- why Sol is intentionally not Turing complete;
- how Sol relates to Prolog, Coq, Datalog, and relational algebra;
- relations as dependent types;
- membership checking as typing;
- constraints as ordinary relations;
- equality as a relation with special operational capabilities;
- the distinction between membership, constraint propagation, and
generation;
- termination and totality strategies;
- structural recursion;
- bounded enumeration;
- symbolic solving;
- stratified negation;
- finite-world reasoning;
- higher-order relation restrictions;
- proof obligations and certificates.
It should also describe the expected pipeline:
#+BEGIN_EXAMPLE
source text
parsing
AST construction
relation-expression normalization
schema checking
variable and scope analysis
unification planning
constraint planning
totality checking
solver selection
proof/search execution
residual constraints or normalized result
#+END_EXAMPLE
This document should explain how Sol remains expressive while avoiding
the unrestricted partiality of ordinary Turing-complete languages.
** Virtual Machine Specification
This document has not been written yet.
It should describe the runtime architecture required to execute Sol
programs.
Expected topics include:
- VM object model;
- relation objects;
- domain relations;
- query objects;
- rule objects;
- variables and logic cells;
- substitutions;
- unification store;
- constraint store;
- conjunction and disjunction execution;
- equality handling;
- membership checking;
- relation indexes;
- finite relation scans;
- symbolic solver hooks;
- quantifier execution;
- tabling and memoization;
- totality-preserving search;
- bounded generation;
- integrity-control hooks;
- interaction with stored relations;
- error and proof-obligation reporting.
The VM specification should explain how Sol expressions are evaluated
without becoming an unrestricted Prolog runtime.
In particular, it should make clear how the VM distinguishes:
- checking membership;
- accumulating constraints;
- solving symbolically;
- enumerating finite relations;
- bounded generation;
- and rejecting non-total execution plans.
* Current Status
The language has a specification, a set of normative integration
decisions, and a working first implementation in OCaml:
- a parser for the surface syntax under the delimiter law;
- a loader whose admission enforces totality: structural decrease
witnesses on recursive rules, schema and domain checks on facts,
membership criteria (refinements and foreign keys) solved against
the complete extension;
- a solver with dynamic goal selection, so conjunction is
commutative in fact and non total plans are rejected instead of
attempted;
- decidable negation, Exists and ForAll;
- backward-solving arithmetic over the integers and rationals with
minimal shape preserved;
- a =WORLD= functor for embedding, exercised by a host-defined
catalog in the tests, and a standalone binary with a REPL.
See =docs/vm.org= for behavior, =docs/terms.org= for the term
algebra.
Build with =nix develop -c dune build=; run the tests with =nix
develop -c dune runtest=; run a program with =dune exec sol --
file.sol=.
The next documents to produce are:
1. =docs/core-design-and-pipeline.org=
2. =docs/virtual-machine-specification.org=
These should build on the language specification, the integration
decisions, and the implementation as it stands.
|
