diff options
| -rw-r--r-- | README.org | 176 |
1 files changed, 176 insertions, 0 deletions
diff --git a/README.org b/README.org new file mode 100644 index 0000000..5de75cf --- /dev/null +++ b/README.org @@ -0,0 +1,176 @@ +#+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 + +At the moment, the project has a working conceptual direction and a +language specification draft. + +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 and clarify how Sol +can be implemented while preserving totality. |