diff options
Diffstat (limited to '')
| -rw-r--r-- | docs/sakura-RNT-integration.org | 722 |
1 files changed, 722 insertions, 0 deletions
diff --git a/docs/sakura-RNT-integration.org b/docs/sakura-RNT-integration.org new file mode 100644 index 0000000..78ad5e2 --- /dev/null +++ b/docs/sakura-RNT-integration.org @@ -0,0 +1,722 @@ +#+TITLE: Sol / Sakura / RNT Integration +#+AUTHOR: Marcos Magueta + +* Purpose + +This document records the architectural decisions binding Sol to the +Sakura relational engine (=../sakura=) and the RNT database kernel +(=../RNT=). These decisions were reached by adversarial design review +(2026-07-11) and are normative: later documents (the pipeline +specification and the VM specification) must not contradict them +without revisiting the arguments recorded here. + +* The Stack, As It Exists + +Facts established from the codebases, not decisions: + +- *RNT* is a database kernel currently being rewritten in OCaml (the + original execution core was C++; its design carries over). Its + execution core, *FOL* (=lib/backend/execution/FOL.ml=), mechanically + evaluates first-order relational plans under the Volcano pull + model. Every plan terminates: evaluation is model + checking against one fixed, finite model, which is decidable. RNT + makes no independent termination judgements; it trusts plan + annotations. +- *Sakura* (OCaml) is the authoritative source of semantics. It owns + cardinality analysis (=Finite= / =ConstrainedFinite= / =AlephZero= / + =Continuum=), termination enforcement (=TAKE= insertion), join + ordering, and physical storage. +- Sakura's sublanguages are cleanly separated modules: DRL (pure + retrieval, total), ICL (integrity constraints as membership checks), + DCL (branch management and 3-way merge over content-addressed + tips), DML (delta semantics), DDL, with TCL planned. +- =sublanguage.ml= classifies operations categorically: a *Query* is a + natural transformation between instance functors (state unchanged); + a *Transition* is a morphism in the category of database states. +- RNT tuples are content-addressed: each tuple is stored under the + SHA256 digest of its serialized bytes. DCL branches point to tips + identified by hash. Database states are therefore already + first-class Merkle-style values in this architecture. +- *Karuta* is a Prolog-like language targeting the BEAM, positioned at + the application layer. + +* Decision 1: Totality Is a Stack-Wide Invariant + +** The decision + +Sol is total, and so is the entire database language stack. The +previously entertained idea of a Turing-complete PPL (predicate +procedure language) — recorded in =sakura/lib/sublanguage.ml= ("PPL -> +new effect class: potentially non-terminating computation") and in +=karuta-integration.org= ("a predicate procedure language might [be +Turing complete]") — is *retracted*. + +Problems that genuinely require Turing-complete computation belong in +the application layer (Karuta on the BEAM), not in the database. + +** The argument + +- P1. A very large class of useful programs is expressible in a total + language: arithmetic, data-structure algorithms, parsers, theorem + provers, sorting, type checkers, relational evaluators — anything + whose recursion is structural and provably terminating. +- P2. Admitting unbounded recursion anywhere in the stack re-imports + the halting problem into every layer above it, destroying the + termination guarantee that RNT's execution core is *named after* + (see =RNT/new-docs/fol.org=: "do not make the query language + Turing-complete"). +- P3. Stored procedures are the layer where users write the most + logic; that is the worst possible place to lose the guarantee. +- C. Therefore the database language is total, with no partial + escape hatch inside the database. Partiality lives outside, in the + application layer. + +* Decision 2: Sol Is the Database Language; Karuta Compiles to It + +** The decision + +- Sol is *the* language of the Sakura/RNT RDBMS, and its VM is the + database runtime. It plays the role SQL plays in PostgreSQL: the + language exposed at the REPL and over the wire. +- Karuta remains the application-layer language. It compiles to the + s-expression interchange form and internally targets Sol; this + compilation happens *inside Sakura* — Sakura hosts the Karuta + front-end and lowers it onto Sol, the same way it receives Sol + directly from the REPL or the wire. Karuta does not front the + sublanguages directly anymore; Sol does. +- The sublanguages (DRL, ICL, DCL, DML, DDL, TCL) are not separate + surface languages. They are fragments of Sol, distinguished + semantically (query vs. transition), not syntactically balkanized + as in SQL. + +** The argument + +- P1 (uniformity requirement). A stored relation and a computed + relation must be handled identically: the same application syntax, + the same membership semantics. "The same way we handle a relation + stored in the database, we invoke a function facing a relational + interface." +- P2. Two surface languages over one semantic core is the negation of + uniformity — it reproduces the SQL disease: a *collection* of + sublanguages with no harmonic whole. +- C. One language, Sol. Everything else (Karuta included) is a + compiler front-end or client of it. + +* Decision 3: Transitions Are Relations Over Database States + +** The decision + +Sol expresses state change (DML, DDL, DCL) as *relations between +database states*. A database state =S= is a first-class value — which +the architecture already supports, since tuples are content-addressed +and branch tips are hashes. + +An insert is a relation: + +#+BEGIN_SRC sol +[Insert relation: Person tuple: T before: S after: S'] +#+END_SRC + +This proposition holds exactly when state =S'= is state =S= with =T= +admitted into =Person= (which entails =T= passing every ICL +constraint attached to =Person= — membership checking and integrity +control are the same operation, per the language specification). + +Exactly *one* primitive effect exists, outside the logic, at the +edge: *commit* — advancing a branch tip (HEAD) from =S= to =S'=. As +in git: everything is pure value manipulation until the single +mutable reference moves. + +** The alternatives rejected + +- *Two-layer language* (pure core + imperative command shell, à la + Haskell IO): honest, but bifurcates the grammar into expressions + and commands — DML becomes a foreign sublanguage again, violating + Decision 2's uniformity premise. +- *Smalltalk message-sends with hidden effects* (=Person insert: T= + mutating in place): the surface says "message", the internals + perform a state morphism. Dishonest syntax — the construct's + surface form would not mean what the internals do. Rejected on the + syntax-honesty principle. + +** The argument + +- P1 (uniformity). Transitions expressed as relations use the same + application syntax, the same conjunction, the same proof-search + semantics as everything else in Sol. +- P2 (fact). Database states are already first-class Merkle values in + RNT/Sakura (content-addressed tuples, hash-identified branch + tips). State-as-value is not an invention; it is a recognition. +- P3 (honesty). =sublanguage.ml= already classifies DML/DDL/ICL/DCL + as morphisms in the category of database states. Making the states + and the morphism explicit in the surface syntax makes the language + say exactly what the semantics do. +- C. An insert *is* a relation over states. + +** What this buys + +Because =Insert(R, T, S, S')= is an ordinary proposition, it can be +*queried* as well as *performed*: + +- provenance and audit are ordinary conjunctions over the state + chain; +- time-travel queries are membership checks against old states; +- dry-run is evaluating the transition relation without committing; +- a transaction is a composition of transition relations + =S → S' → S''=, committed atomically by moving HEAD once, to the + final state; +- DCL merge is already a ternary relation over states (two tips and + an ancestor) — Decision 3 makes the rest of the language match it. + +** Acknowledged costs + +- State identity and equality must be defined precisely (hash + equality of content-addressed states is the candidate, but + canonical serialization must be specified). +- Sequencing becomes conjunction over chained state variables; the + planner must order these chains. This is real planning work, though + of the same kind DCL merge already performs. + +* Decision 4: Sol Is a Library; RNT Links Its Compiler and VM In-Process + +** The decision + +Sol — the whole pipeline: normalizer, planner, totality checker, and +VM — is built as a host-neutral OCaml library, parameterized over a +=WORLD= interface: the store that answers which relations exist, +their capabilities, how membership is checked against stored tuples, +and what commit means. + +Two hosts consume it: + +- *Standalone Sol*: a thin binary links the library with an + in-memory or file-backed world. This world exposes only the pure + fragment: no branches exist, so transition relations and commit are + simply absent capabilities (see Decision 5). This satisfies the + requirement that Sol be usable as a separate language for ordinary + (total) programs. +- *RNT*: the kernel links the library in-process as its execution + layer. RNT's planned split between "terminating first-order logic + and higher-order logic execution" is filled directly: the FOL core + executes the finite-plan fragment (=Plan.t=, Volcano), and the HOL + slot *is* Sol's engine — not a reimplementation, the same compiler + internals. The world is the object manager plus the + content-addressed store; commit advances a branch tip atomically + inside the kernel. + +** The argument + +The earlier framing — "Sol VM inside the kernel" versus "Sol VM as a +client of the kernel" — was a false dichotomy. + +- P1 (requirement). Sol must run standalone, with no database + present. +- P2 (Decisions 2–3). Sol's VM is the database runtime, and commit — + the single effect — must be atomic against RNT's branch tips. +- P3. A client-process VM satisfies P1 but makes the only effect + distributed, breaking P2. A kernel-welded VM satisfies P2 but + cannot exist without the database, breaking P1. +- C. The VM must be neither: a library over an abstract world. RNT + linking it in-process preserves atomicity; the standalone host + preserves independence. One implementation, two hosts — an + embeddable runtime in the manner of SQLite or Lua, where one of + the embeddings is the database kernel itself. + +The language specification already gestures at this seam: membership +criteria "constructed at the host language," capabilities as declared +operational permissions, =World= as a relation. The =WORLD= interface +is that seam made explicit. + +** Acknowledged costs + +- The world interface is a hard public contract. Capability + negotiation — which worlds support enumeration, solving, bounded + generation — must be specified precisely. +- Standalone-world semantics must be a strict subset of + database-world semantics, so that a program proven total against + the standalone world remains total in-kernel. + +* Decision 5: A State Is a Branch's Whole Tree + +** The decision + +The state values =S=, =S'= in transition relations denote *branch +states*: the catalog, schemas, ICL constraints, and the extension of +every relation *as one branch sees them*, as one content-addressed +tree — exactly a git commit object. Concretely, =S= is the Merkle +root hash of the branch's tree: a snapshot handle into the +content-addressed store, cheap to hold, structurally shared with +neighboring states. + +There is no global "database state" spanning branches. Transition +relations are meaningful only within a branch: a stored procedure +receives the branch's current root hash, evolves it purely — each +transition producing the successor hash — and yields the final hash, +which commit installs as the new tip. + +It works like git: all value manipulation is pure; history is a chain +of whole-database states; the single effect (Decision 3) is advancing +a branch tip to a new state. + +Consequently, transition relations exist only in the RNT/Sakura +world. The standalone world has no branches, hence no transitions and +no commit — standalone Sol is the pure total fragment. This is +capability negotiation (Decision 4) doing its job, not a special +case. + +** The alternative rejected + +Per-relation states — the database as a bag of independently +versioned relations — fail on two counts: + +- P1. DDL and ICL changes are also transitions (Decision 2); a + per-relation state has no place to record "the schema changed" or + "a constraint was added." +- P2. Integrity constraints span relations (foreign keys as + membership checks against *other* relations). A transition's + validity must be judged against a consistent snapshot of all + relations, or ICL checking is unsound. +- P3 (fact). DCL already works on whole tips: a branch is one hash, + and 3-way merge operates on two tips and an ancestor. + +Nothing is lost: in a content-addressed tree, per-relation hashes +still exist as internal nodes, and unchanged subtrees share +structure. + +** Acknowledged costs + +- Hashing must be incremental — a transition recomputes hashes along + the changed path only (O(path), not O(database)) — or commit + throughput dies. Merkle trees provide exactly this. +- Canonical serialization of states must be specified early; state + equality is hash equality only if serialization is deterministic. + +* Decision 6: Sequencing Comes from Linear State Threading, Not Syntax Order + +** The decision + +Transition sequencing derives *solely* from state-variable sharing, +never from syntactic position: + +#+BEGIN_SRC sol +[Insert relation: Person tuple: T1 before: S0 after: S1] :and +[Insert relation: Person tuple: T2 before: S1 after: S2] +#+END_SRC + +=:and= remains honestly commutative: swapping the conjuncts changes +nothing, because the chain =S0 → S1 → S2= is carried by unification. +The planner topologically sorts the state chain, the same discipline +Sakura already applies when ordering joins by variable binding. + +State variables obey a *linear discipline*, in the manner of +Mercury's =di=/=uo= (destructive-input / unique-output) modes on +=io.state=: within a transaction, each state value is consumed +exactly once (as =before:=) and produced exactly once (as =after:=). +The felt experience is procedural — a timely order, step after step — +but the order is implied by the dataflow, not decreed by the page. + +A transaction is a relational expression whose state variables form +one linear chain from the branch tip (=S0= = HEAD) to a final state, +followed by one commit of that final state (Decision 3). + +** The argument + +- P1. =:and= means logical conjunction, and conjunction is + commutative. +- P2 (syntax honesty). The surface form must mean what the internals + do. If evaluation order were read off the page, =:and= would be a + lie — sequencing dressed as conjunction. This is the same sin the + language specification already rejects in "newline adjacency + secretly means conjunction." +- P3. Unification is Sol's only binding mechanism; threading state + through shared variables introduces no new primitive. +- C. Order-from-dataflow is the only admissible sequencing. The + linear mode discipline makes chain-hood a static property: a fork + (two transitions consuming the same =S=) or a reuse is a mode + error caught at admission, not a planner heuristic. + +** Sugar policy + +A convenience form (e.g. a =Transaction do:= that auto-threads the +state variables) is permitted *only* as sugar with a published +elaboration into the explicit chain. It must never become a +primitive with its own semantics. + +** Acknowledged costs + +- Verbosity until sugar lands: users name =S0=, =S1=, =S2= + explicitly. +- The mode/linearity checker must be specified as part of admission + checking, alongside schema and totality checks. + +* Decision 7: Reads Are State-Scoped + +** The decision + +In the RNT/Sakura world, *every* read of a stored relation happens +from an explicit state. In the core language, a stored-relation +application carries the state it reads at: + +#+BEGIN_SRC sol +[Person id: P age: A at: S1] +#+END_SRC + +A scoping form is provided as sugar, with a published elaboration +that distributes the state over the stored-relation applications in +its body (Decision 6's sugar policy): + +#+BEGIN_SRC sol +[At state: S1 body: [Person id: P age: A] :and [Adult person: P]] +#+END_SRC + +At the REPL, a bare query elaborates to =at:= the current branch +tip's state — one uniform rule, not a second semantics. + +Standalone Sol is untouched: it has no stored relations, hence no +=at:=. + +** The argument + +- P1 (Decision 6). Order on the page carries no meaning; so "read + whatever the previous statement produced" is not available — it is + positional order, the outlawed lie. +- P2. Reads must therefore name their state, or a hidden convention + decides — dishonest syntax. +- P3. The alternative — all reads pinned to the transaction's initial + =S0= — makes read-your-own-writes inexpressible: a procedure that + inserts and then validates against the result cannot be written, + even though ICL checking inside the chain already reads + intermediate states. The language would forbid users what its own + machinery does. +- C. Reads are state-scoped in the core; terseness is recovered by + sugar, never by convention. + +** Acknowledged costs + +- =at:= becomes a reserved label on stored-relation applications; it + cannot be a schema attribute name. +- The elaboration of =At state: body:= must be specified precisely, + including its interaction with nested =At= forms (innermost wins) + and with transition relations (which are already explicit and are + not rescoped). + +* Decision 8: The Kernel Arbitrates Only the Tip; Conflict Policy Is DCL + +** The decision + +The only point of contention in RNT is the tip of a branch. The +kernel therefore provides exactly one concurrency primitive: *atomic +compare-and-swap on a branch tip* — install =Sn= as the tip iff the +tip still equals the =S0= the transaction started from. + +Everything above that primitive is the version-control language's +domain, and DCL is a fragment of Sol (Decision 2) operating on +states as values (Decision 5): + +- *fast-forward*: the tip is an ancestor of =Sn= — install directly; +- *rebase*: re-execute the procedure from the new tip — sound and + safe because a transaction is a pure, total function of its + initial state (Decisions 3, 6); nothing partial ever escaped; +- *3-way merge*: already a ternary relation over two tips and their + ancestor, with declared strategies (=PreferLeft=, =PreferRight=, + =RevertToAncestor=). + +Conflict policy is thus *expressed in the language*, not hardcoded +in the kernel. + +** The argument + +- P1. A pure total transaction has no partial effects to undo; + re-execution from a moved tip is always safe and always + terminates. The classical difficulty of transaction retry does not + exist here. +- P2. Given P1, any policy the kernel could hardcode (retry, merge, + reject) is expressible as relations over states — and DCL already + contains the vocabulary. +- P3 (minimality). A kernel primitive should exist only where the + kernel is the sole possible arbiter. Tip installation is the one + such place; policy is not. +- C. Kernel = CAS on the tip. Policy = DCL, in Sol. + +** Acknowledged costs + +- Any retry/arbitration loop is unbounded under contention. It lives + outside the total language — in the commit arbiter or client, + alongside the REPL loop. Sol proves each execution terminates; the + arbiter decides how many executions happen. Partiality is confined + to that boundary and must be documented as such, with a + fairness/backoff policy. + +* Decision 9: No DRL Syntax — the Plan Is Chosen by Analysis + +** The decision + +There is no distinguished DRL surface form. The user writes uniform +Sol; the planner decides how each subexpression executes. Since +*both* engines are total, engine choice is not a semantic +distinction and must not be a syntactic one: it changes performance, +never meaning (Codd's theorem licenses the lowering — the finite +first-order fragment and the plan algebra are the same queries). + +What actually distinguishes subexpressions is what their relations +*are*: + +- *stored relations* — scanned at an explicit state =S= + (Decision 7); +- *ephemeral relations* — algebraic artifacts of relational + operations, carrying provenance and lineage (Sakura's existing + notion); +- *rule- and procedure-defined relations* — unfolded, or evaluated + by fixpoint on Sol's engine. + +The planner — reusing Sakura's cardinality propagation (=Finite= / +=ConstrainedFinite= / =AlephZero= / =Continuum=), constraint +propagation, boundness/mode analysis, and join ordering — identifies +maximal finite, first-order, non-recursive subexpressions and lowers +them to the plan algebra (=Plan.t=) for RNT's FOL core. Everything +else runs on Sol's engine, which pulls from lowered plans as cursors +(Volcano composes across the seam). + +** The argument + +- P1 (Decision 2). Sublanguages are semantic fragments, not + syntactic ones; a DRL marker would re-balkanize the language. +- P2 (totality, Decision 1). Both engines halt, so there is no + observable semantic difference for a marker to honestly denote. +- P3 (fact). Sakura already computes the needed evidence — + cardinality tags, TAKE insertion, boundness-driven join ordering. + The lowering criterion reuses existing analysis. +- C. Fragment-by-analysis. The FOL core is an invisible optimization + target; the observable contract is only the tuple stream. + +** Acknowledged costs + +- Each lowering must be meaning-preserving and should be checkable + (the =Plan.t= translation is a verifiable step, not a trusted + one). +- A user who needs the guarantee "this runs as a flat finite plan" + gets it as a declarable *assertion* (reject if not lowerable), + never as a separate language. + +* Decision 10: Totality Is Established at Admission, Verified in Rocq + +** The decision + +Totality evidence is checked at *admission time*: defining a rule or +procedure is itself a DDL transition (=[DefineRule ... before: S +after: S']=), and the definition fails — the successor state does not +come to exist — unless the evidence is present. A state containing a +non-total rule is unrepresentable; queries therefore run against +states where everything is already proven total and pay nothing at +query time. + +The evidence is a closed ladder; each rung is recorded in the rule's +metadata: + +1. *Structural decrease* — the checker finds a strictly decreasing + argument (e.g. =Tail= < =[Head | Tail]= in =Length=). Automatic; + covers most honest recursion. +2. *Bounded quantification* — the searched space is =Finite= or + =ConstrainedFinite= by Sakura's cardinality analysis. +3. *Symbolic discharge* — algebraic properties prove the universal + or the recursion (e.g. =Plus(X, 0) = X= over all integers). +4. *Certificate* — a Rocq proof, checked before admission. Because + the certificate is verified, this rung is not a trusted escape + hatch. A merely *trusted* declaration remains possible only as a + last resort: named, auditable, and loud. + +Anything fitting no rung is *rejected* — never admitted as a pending +obligation. + +Two levels, not conflated: + +- *Object level*: the ladder above, run by the in-engine admission + checker on each definition. +- *Metatheory*: Rocq/Coq proves the guarantees of RNT/Sakura + themselves — soundness of the admission checker ("any accepted + rule is total"), meaning-preservation of the =Plan.t= lowering + (Decision 9), soundness of ICL checking, and merge respecting its + specification. Since RNT and Sakura are OCaml, the critical + checkers should be *extracted* from Rocq to OCaml, so the thing + proven is the thing running. + +** The argument + +- P1 (Decision 5). States are values. A state containing an unproven + rule is a state whose queries might not halt; admitting it + falsifies the totality invariant *inside* every descendant state. +- P2. "Obligation pending" is Coq's =admit=: tolerable in an + interactive proof, poisonous in a database that other parties + query concurrently. +- P3. A checker that is itself unverified moves the trust boundary + rather than discharging it; the Rocq metatheory closes that gap. +- C. Total-or-absent at admission; verified checker; certificates as + proofs, not promises. + +** Acknowledged costs + +- The structural-decrease checker and the symbolic-discharge engine + must be specified precisely (the pipeline document owns this). +- Rocq extraction constrains implementation style in the affected + modules (pure, extraction-friendly OCaml). +- Proof maintenance is a real, ongoing cost paid for the guarantee + that is the project's entire premise. + +* Decision 11: The Catalog Is Relations + +** The decision + +Everything in a state is a relation, and everything is queryable — +including the catalog itself. Relation definitions, schemas, rules, +constraints, and capabilities are tuples in catalog relations, stored +in the same content-addressed tree, read at a state like anything +else: + +#+BEGIN_SRC sol +[Relation name: N schema: Sch at: S] +[Constraint name: C relation: R body: B at: S] +#+END_SRC + +(A concrete catalog plan already exists on the Sakura/RNT side; this +decision binds Sol to it.) + +** What follows + +- DDL is DML on catalog relations: =DefineRelation= is an insert + into the catalog — one mechanism, not two (Decision 3 already made + DDL a transition; this removes its last special machinery). +- Admission checking (Decision 10) becomes ICL on the catalog: "a + rule tuple enters =Catalog.Rule= only with totality evidence" is + an ordinary integrity constraint on an ordinary relation. +- Introspection is an ordinary query at =S= — which merge, + migrations, and tooling need anyway. + +** The argument + +- P1 (Decision 2). A catalog reachable only through special forms is + a second interface — the SQL disease; =information_schema= is + SQL's own admission that it bolted this on too late. +- P2. Catalog-as-relations lets Decisions 3 and 10 collapse into + existing machinery instead of demanding parallel mechanisms. +- C. The catalog is stored relations, guarded by ICL, versioned in + the tree, queryable in Sol. + +** Acknowledged costs + +- Metacircular bootstrap: the catalog's schema must describe itself + (the fixed point every self-describing catalog has — Postgres's + =pg_class= describes =pg_class=), and some base constraints must + be primitive rather than ICL-expressed. + +* Decision 12: Subtyping Is Proven Inclusion; Identity Is Intensional; Quotients Are Canonical + +** The decision + +Sol's type system represents subtyping, and it is *semantic* +subtyping — subtyping is relation inclusion: + +#+BEGIN_EXAMPLE +S <: T ≜ ∀x. S(x) → T(x) +#+END_EXAMPLE + +Subsumption is not a rule added to the logic; it is the transitivity +of membership: =x ∈ S ∧ S ⊆ T ⊢ x ∈ T=. A refinement is a subtype by +construction (it is an intersection). =Natural <: Integer= because +ℕ ⊆ ℤ. + +Three clauses make this precise: + +*** (1) Inclusion judgments go through the evidence ladder + +=S <: T= is a universal over a possibly infinite domain — +undecidable in general. A subtyping judgment is therefore admitted +by exactly the regime of Decision 10: + +- declared-and-checked facts for the base lattice (=Natural <: + Integer= lives in the catalog, queryable, per Decision 11); +- symbolic discharge for refinements (constraint implication: + =x ≥ 18 → x ≥ 0=); +- finite scan for finite relations; +- Rocq certificate otherwise. + +Inclusion between arbitrary relations is never silently inferred. + +*** (2) Relation identity is intensional, never structural + +Two relations with identical label sets are not the same relation. +Identity comprises the schema *and* the membership criterion (the +intension) — one relation conjoined with a =GreaterThan= constraint +is semantically different from its unconstrained twin — and, for +ephemeral relations, provenance and lineage (Sakura's existing +notions). Consequently: + +- shape implies nothing: no structural typing, no implicit width + subtyping; +- a tuple with more labels does not silently inhabit a + narrower-schema relation — *projection* is the explicit morphism + for forgetting attributes, and it stays explicit. + +*** (3) Quotient domains use canonical minimal-shape representatives + +Rationals expose the classical quotient problem: ℚ is +ℤ × (ℤ∖{0}) quotiented by =(a,b) ~ (c,d) ⟺ ad = bc=, so +={numerator: 2 denominator: 2}=, ={numerator: 1 denominator: 1}=, +and =1= all denote one value. Sol resolves quotients by *canonical +representatives*, enforced by the domain's own membership criterion, +and canonicalization picks the *minimal shape*: an integer-valued +rational normalizes to the ground integer itself +(={numerator: 2 denominator: 2}= normalizes to =1=, not to +={numerator: 1 denominator: 1}=). + +Therefore ℤ ⊂ ℚ holds *literally, as membership inclusion* — +representation does not limit inclusion, and no injection or +coercion machinery exists. Non-canonical pairs are pre-values that +normalize in, via a normalization relation declared as part of the +domain's catalog definition: + +#+BEGIN_SRC sol +[RationalNormalize raw: {numerator: 2 denominator: 2} canonical: 1] +#+END_SRC + +The alternative — setoids, where all representatives are members and +every relation carries congruence obligations with a per-domain +=Equal= — is rejected: congruence proofs metastasize over every rule +ever defined. + +** The argument + +- P1 (Decision 5). States are content-addressed; state equality is + hash equality. If two representatives of one value could both be + stored, equal databases would hash differently — hash equality + would be a lie. Canonical forms are *mandated* by the Merkle + store, not merely preferred. +- P2. Given canonical forms, choosing the minimal shape as canonical + is the unique choice under which numeric-tower inclusion + (ℤ ⊂ ℚ) is true on the nose rather than simulated by coercion. +- P3. Normalization is already one third of Sol's execution model + ("proof search, constraint propagation, and normalization") — no + new primitive is introduced. +- C. Subtyping as proven inclusion, intensional identity, canonical + quotients. + +** Acknowledged costs + +- Operations over quotient domains accept mixed shapes and + normalize at the boundary (e.g. =Plus= over =Rational= handles + ground integers and canonical pairs). +- A quotient domain without a declared normalization relation is + rejected at admission: no equivalence without a normalizer. +- The subtype lattice for base domains must be seeded in the catalog + bootstrap (Decision 11's metacircular fixed point grows slightly). + +* Consequences for the Pending Documents + +- =docs/core-design-and-pipeline.org= must treat transition relations + as first-class in normalization, planning, and totality checking. +- =docs/virtual-machine-specification.org= must specify: the state + value representation (content-addressed), the evaluation of + transition relations, and the single commit primitive as the only + effectful operation in the VM. +- Sol's DRL fragment must normalize to plans executable by RNT's FOL + core (the =Plan.t= algebra: Scan, Project, Join, Union, Rename, + Take, Materialize), with Sakura-style cardinality annotation. |