#+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;
- applications as propositions everywhere: no relation application
  in term position, statements about results written flat as
  membership.

** Core Design Principles and Pipeline Specification

See: [[file:docs/core-design-and-pipeline.org][docs/core-design-and-pipeline.org]]

It describes the deeper design principles behind Sol and the
compiler/interpreter pipeline that preserves totality, as
implemented in =lib/=.

Topics covered 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

See: [[file:docs/virtual-machine-specification.org][docs/virtual-machine-specification.org]]

It describes the runtime architecture that executes Sol programs, as
implemented in =lib/= and =theories/=, and what the runtime owes the
future.

Topics covered 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=. Worked examples live in =examples/= (see
=examples/README.org=); machine checked proofs in =theories/=
(structural and lexicographic decrease, extracted into admission;
the interval characterizations behind propagation).

Machine checked proofs live in =theories/=: the admission checker's
core claim, that strict containment decreases a well founded
measure, is proven in Rocq and compiled as part of the default
build.

The design documents promised at the project's start now all exist:
the language specification, the integration decisions, the core
design and pipeline document, and the virtual machine
specification.