From 7d0fdcf2048bc736c82f84e92dcfc68b3d6ac45c Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 10 May 2026 22:59:48 -0300 Subject: add nested loop join strategy to VM and tests --- docs/tarski-sakura-separation.md | 98 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 98 insertions(+) create mode 100644 docs/tarski-sakura-separation.md (limited to 'docs/tarski-sakura-separation.md') diff --git a/docs/tarski-sakura-separation.md b/docs/tarski-sakura-separation.md new file mode 100644 index 0000000..a33e2e3 --- /dev/null +++ b/docs/tarski-sakura-separation.md @@ -0,0 +1,98 @@ +# Tarski / Sakura Separation of Concerns + +This document describes how query analysis responsibilities are divided between +the **Sakura** OCaml frontend and the **Tarski** FOL runtime inside the C++ VM. + +## The Two Runtimes + +The VM hosts two distinct execution cores: + +| Core | Language | Responsibility | +|---|---|---| +| **Tarski** | C++ (this repo) | Mechanical FOL plan execution via Volcano pull model | +| **Sakura** | OCaml | Query parsing, cardinality analysis, plan emission, physical storage | + +Sakura is the authoritative source of data and of query semantics. The SQLite +backend in this repository exists only for isolated testing; in production, +CursorManager streams data from Sakura over a well-defined interface. + +## What Sakura Is Responsible For + +### Cardinality analysis and constraint propagation + +Every relation in Sakura carries a cardinality tag: `Finite`, `ConstrainedFinite`, +`AlephZero`, or `Continuum`. When a query joins multiple relations, Sakura +propagates these tags through the plan to determine the cardinality of the result. + +This analysis is non-trivial. Consider: + +```karuta +natural[A], natural[B], natural[C], plus[A,B,C], eq[C, 10]. +``` + +Each of `natural`, `plus`, and `eq` is individually `AlephZero`. But Sakura can +determine that binding `C = 10` via `eq` constrains `plus[A,B,10]` to a finite +set of natural-number pairs, making the overall result finite. Replacing +`natural` with `integer` changes the result to infinite, because negative pairs +also satisfy `plus[A,B,10]`. + +Tarski does not repeat this analysis. It receives a plan that is already +annotated with cardinality metadata and executes it mechanically. + +### Termination guarantees + +If a query produces an infinite result set, Sakura adds a `TAKE` node to the +plan before emission. Tarski enforces the `TAKE` limit but makes no independent +judgement about whether a plan terminates. + +### Join ordering + +Sakura orders the children of each JOIN so that variables are bound from the +outer (left) side before the inner (right) side is probed. This ensures that +builtin relations — which may have `AlephZero` cardinality when arguments are +unbound — are always probed with fully or partially bound arguments, enabling +O(1) membership validation rather than unbounded enumeration. + +### Physical storage + +Sakura owns the physical storage layer. CursorManager pulls paginated tuple +streams from Sakura; the cursor abstraction hides whether the underlying data +comes from a stored relation or an ephemeral builtin generator. + +## What Tarski Is Responsible For + +### Mechanical plan execution + +Tarski receives a complete, annotated plan tree from Sakura and executes it via +the Volcano pull model: `VM::Next(PlanNode*)` propagates demand from the root +to the leaves, returning one tuple at a time. + +### Cardinality-aware execution strategy + +Each `PlanNode` carries the cardinality tag Sakura attached at plan time. Tarski +uses this tag only to choose an execution strategy — never to reason about +termination: + +- **Finite / ConstrainedFinite inner side** → safe to materialize for + nested-loop join. +- **AlephZero inner side, all args bound** → probe via `membership_criteria` + in O(1); the generator is never called. +- **AlephZero inner side, unbound args** → should not occur; Sakura must have + added a `TAKE` node or reordered the join. Tarski may assert in debug builds. + +### TAKE enforcement + +`TAKE` is a first-class node in the plan tree. When `VM::Next` passes through a +`TAKE` node it decrements a counter and returns `nullptr` once the limit is +reached, regardless of what the subtree would produce. + +## Why This Division Is Correct + +The cardinality analysis described above requires understanding the **semantics** +of each relation — what `plus` means over naturals versus integers, how `eq` +interacts with a functional relation, and so on. That knowledge lives in Sakura. +Duplicating it in Tarski would couple two layers that must remain independent and +would place type-level reasoning inside a mechanical executor. + +Tarski's contract is simple: given a safe plan, produce correct tuples. Sakura's +contract is: emit only safe plans. -- cgit v1.2.3