From e6661bfa6a3d7dc477d0b7717c80bd536eca2d68 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 14 Mar 2026 11:39:04 -0300 Subject: =?UTF-8?q?Branching=20and=20na=C3=AFve=20merge=20strategies?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * AGPL license * branching and merging * Delete LICENSE in favor of separate PR Signed-off-by: Marcos Magueta * add unmonitored tests and docs --------- Signed-off-by: Marcos Magueta --- docs/dcl-quantification.org | 480 -------------------------------------------- docs/dcl.org | 105 ++++++++++ docs/icl-quantification.org | 480 ++++++++++++++++++++++++++++++++++++++++++++ docs/icl.org | 108 ++++++++++ docs/karuta-integration.org | 26 ++- docs/n-way-binding.org | 8 +- 6 files changed, 718 insertions(+), 489 deletions(-) delete mode 100644 docs/dcl-quantification.org create mode 100644 docs/dcl.org create mode 100644 docs/icl-quantification.org create mode 100644 docs/icl.org (limited to 'docs') diff --git a/docs/dcl-quantification.org b/docs/dcl-quantification.org deleted file mode 100644 index 81e9cad..0000000 --- a/docs/dcl-quantification.org +++ /dev/null @@ -1,480 +0,0 @@ -#+TITLE: DCL Quantification: Runtime Model and Evaluation - -* Overview - -This document describes precisely how DCL constraints are represented, compiled, -and evaluated at runtime. It covers the full stack from the s-expression syntax -through AST compilation, context construction, and recursive evaluation — with -particular attention to the cost model of quantifiers, which is the primary target -for future performance work. - -* Constraint Type (~lib/constraint.ml~) - -The runtime constraint type is an algebraic tree: - -#+begin_src ocaml -type t = - | MemberOf of { target : relation_name; binding : binding } - | Not of { body : t; universe : relation_name } - | And of t list - | Or of t list - | Exists of { variable : attr_name; quantifier : relation_name; body : t } - | Forall of { variable : attr_name; quantifier : relation_name; body : t } -#+end_src - -A ~binding~ is a ~BindingMap~ (a ~Map.Make(String)~) from target attribute names -to ~binding_expr~: - -#+begin_src ocaml -type binding_expr = - | Var of attr_name (* resolved from current tuple at eval time *) - | Const of Conventions.AbstractValue.t (* literal, resolved at compile time *) -#+end_src - -The ~variable~ field in ~Exists~ and ~Forall~ names the bound tuple for use in -~Var~ expressions inside the body. Attributes from the quantifier row are merged -into the evaluation tuple under the prefix ~variable ^ "."~, so ~(Var "d.dept_id")~ -unambiguously refers to the ~dept_id~ attribute of the tuple bound to variable ~"d"~. -See [[*Tuple Extension: ~extend_tuple~][Tuple Extension: extend_tuple]] for the implementation and [[*The Variable Namespacing Problem][The Variable Namespacing Problem]] -for the history of the bug this fixes. - -* Evaluation Context (~eval_context~) - -Evaluation does not access storage or the database directly. It works through an -~eval_context~ record built once per insert operation and closed over a specific -~(storage, db)~ snapshot: - -#+begin_src ocaml -type eval_context = { - check_membership : - relation_name -> - (attr_name * Conventions.AbstractValue.t) list -> - bool; - iterate_finite : - relation_name -> - (attr_name * Conventions.AbstractValue.t) list list option; -} -#+end_src - -Both fields are closures. This indirection decouples ~Constraint.evaluate~ from -the storage backend and allows the same constraint tree to be evaluated against -different snapshots. - -** ~check_membership~ - -Built in ~Manipulation.Make.build_eval_context~. Given a relation name and a list -of ~(attr_name, value)~ pairs, it returns ~true~ iff a tuple exists in the named -relation whose attributes match every pair in the list. - -The implementation: -1. Looks up the relation in the ~db~ snapshot. -2. Constructs a synthetic ~Tuple.Materialized~ from the bound pairs and runs - ~rel.membership_criteria~ against it. If it fails, returns ~false~ immediately. -3. If the relation has no Merkle tree (ephemeral/generator relation), - ~membership_criteria~ alone is trusted and the function returns ~true~. -4. If the relation has a tree, it calls ~Merkle.keys tree~ to obtain *all* tuple - hashes, then linearly scans them. For each hash it: - a. Loads the raw bytes from storage (~Storage.load_raw~). - b. Deserialises the ~Storable.Tuple.t~ to get the attribute hash list. - c. For each bound pair ~(bk, bv)~, finds the matching attribute by name, loads - its value bytes from storage (~Storage.load_raw~ again), unmarshals it, and - compares with ~Stdlib.(=)~. - d. Short-circuits to ~true~ on the first tuple that satisfies all pairs. - e. Returns ~false~ if no tuple matches. - -The cost of a single ~check_membership~ call on a relation of cardinality /n/ with -/a/ bound attributes and average /k/ attributes per stored tuple is: - - O(n · (1 + a · k)) storage round-trips in the worst case. - -No indexes exist. Every check is a full table scan at the storage level. - -** ~iterate_finite~ - -Given a relation name, returns ~Some rows~ where ~rows~ is a fully materialised -list of rows, each a ~(attr_name * AbstractValue.t) list~. Returns ~None~ if the -relation has infinite or unconstrained cardinality -(~AlephZero~ or ~Continuum~ in ~Conventions.Cardinality~). - -Only relations with cardinality ~Finite _~ or ~ConstrainedFinite~ are iterable. -Generator-based relations with no tree return ~Some []~. - -The materialisation path: -1. ~Merkle.keys tree~ — loads all tuple hashes. -2. For each hash: ~Storage.load_raw~ → ~Storable.Tuple.of_bytes~ → attribute hash list. -3. For each attribute hash: ~Storage.load_raw~ → ~Marshal.from_bytes~. - -This eagerly materialises the *entire* quantifier relation into memory before -evaluation begins. For a relation of cardinality /n/ with /k/ attributes each, -the cost is O(n · k) storage loads and the full result occupies O(n · k) memory. - -* Variable Resolution: ~bind~ - -Before a ~MemberOf~ check is executed, the binding map is resolved against the -current tuple via ~bind~: - -#+begin_src ocaml -let bind (b : binding) (tuple : Tuple.materialized) - : (attr_name * Conventions.AbstractValue.t) list = - BindingMap.fold - (fun target_attr expr acc -> - let value = match expr with - | Const v -> Some v - | Var src_attr -> - match Tuple.AttributeMap.find_opt src_attr tuple.attributes with - | Some attr -> Some attr.Attribute.value - | None -> None - in - match value with - | Some v -> (target_attr, v) :: acc - | None -> acc) - b [] -#+end_src - -Key behaviour: -- ~Const v~ is lifted directly; no attribute lookup. -- ~Var src_attr~ looks up ~src_attr~ in ~tuple.attributes~. If the attribute is - absent, the pair is *silently dropped* from the bound list. A ~MemberOf~ with - incomplete bindings may match unintended tuples or always pass if the target - relation contains tuples with fewer attributes. -- The result is a plain assoc list, not a map; duplicate keys are possible if - the binding contains both a ~Const~ and a ~Var~ targeting the same name. - -* Tuple Extension: ~extend_tuple~ - -When a quantifier (~Exists~ or ~Forall~) iterates over a row, it extends the -current evaluation tuple by merging that row's attributes in: - -#+begin_src ocaml -and extend_tuple (tuple : Tuple.materialized) - (variable : attr_name) - (row : (attr_name * Conventions.AbstractValue.t) list) - : Tuple.materialized = - let extra_attrs = - List.fold_left - (fun acc (k, v) -> - Tuple.AttributeMap.add (variable ^ "." ^ k) { Attribute.value = v } acc) - tuple.attributes row - in - { tuple with attributes = extra_attrs } -#+end_src - -Two important facts: - -1. *Quantifier attributes are namespaced by the variable name.* Each attribute ~k~ - from the quantifier row is inserted as ~variable ^ "." ^ k~. The incoming tuple's - own attributes are never overwritten. ~(Var "dept_id")~ resolves to the base - tuple's value; ~(Var "d.dept_id")~ resolves to the value contributed by the - quantifier bound to ~"d"~. See [[*The Variable Namespacing Problem][The Variable Namespacing Problem]] for the - earlier behaviour where ~variable~ was ignored and overwrites were silent. - -2. *A new ~AttributeMap~ is allocated on every extend call.* With /a/ existing - attributes and /r/ new attributes from the row, ~fold_left~ performs /r/ - ~AttributeMap.add~ operations each building on the previous map. For /q/ - nested quantifiers of cardinalities /n₁, n₂, ..., nq/, ~extend_tuple~ is - called /n₁ · n₂ · ... · nq/ times total — once per combination. - -* Recursive Evaluation: ~evaluate~ - -#+begin_src ocaml -let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t) - : (bool, diagnostic) result = -#+end_src - -The function is structurally recursive over the constraint tree. Each case: - -** ~MemberOf~ - -#+begin_src ocaml -| MemberOf { target; binding } -> - let bound_values = bind binding tuple in - if ctx.check_membership target bound_values then Ok true - else Error (MembershipFailed { target; bound_values }) -#+end_src - -Resolves bindings from the current tuple (O(|binding|) attribute lookups), then -delegates to ~check_membership~. Returns ~Ok true~ or ~Error~ (never ~Ok false~) -— the ~Ok false~ branch of ~Exists~/~Forall~ is distinguished from ~Error~. - -** ~Not~ - -#+begin_src ocaml -| Not { body; universe = _ } -> - match evaluate ctx tuple body with - | Ok true -> Ok false - | Ok false -> Ok true - | Error (MembershipFailed _) -> Ok true - | Error d -> Error d -#+end_src - -~MembershipFailed~ from the body is treated as ~Ok true~ (negation of a failed -membership = the tuple is not a member = negation succeeds). The ~universe~ field -is a declarative annotation for closed-world reasoning and is not used at runtime. - -** ~And~ / ~Or~ - -Both use short-circuit evaluation: -- ~And~: stops at the first ~Ok false~ or ~Error~. -- ~Or~: stops at the first ~Ok true~; swallows ~Error~ branches and continues. - -Neither produces diagnostics for the other branches once a decision is reached. -Note that ~evaluate_named~ (which evaluates all named constraints on a tuple) does -*not* short-circuit — it collects all failures before returning. - -** ~Exists~ - -#+begin_src ocaml -| Exists { variable; quantifier; body } -> - match ctx.iterate_finite quantifier with - | None -> Error (UnboundedQuantifier { variable; quantifier }) - | Some rows -> - let rec check = function - | [] -> Ok false - | row :: rest -> - let extended_tuple = extend_tuple tuple variable row in - match evaluate ctx extended_tuple body with - | Ok true -> Ok true - | Ok false -> check rest - | Error _ -> check rest - in - check rows -#+end_src - -The execution model: -1. ~iterate_finite~ is called, fully materialising the quantifier relation. -2. Rows are iterated sequentially. For each row, ~extend_tuple~ merges it into - the current tuple, and ~evaluate~ recurses into the body. -3. The first ~Ok true~ short-circuits: remaining rows are not evaluated. -4. Both ~Ok false~ and ~Error~ from the body are treated identically — the row is - skipped and iteration continues. *Errors inside the body of an ~Exists~ are - silently discarded.* -5. If all rows are exhausted without ~Ok true~, returns ~Ok false~. - -An ~Exists~ over a relation of cardinality /n/ with a body whose evaluation cost -is /C/ has worst-case cost O(n · C). Nesting two ~Exists~ quantifiers over -relations of cardinalities /n/ and /m/ has worst-case cost O(n · m · C). -In general, /q/ nested quantifiers produce O(∏ nᵢ · C) body evaluations — a -Cartesian product. - -** ~Forall~ - -#+begin_src ocaml -| Forall { variable; quantifier; body } -> - match ctx.iterate_finite quantifier with - | None -> Error (UnboundedQuantifier { variable; quantifier }) - | Some rows -> - let rec check = function - | [] -> Ok true - | row :: rest -> - let extended_tuple = extend_tuple tuple variable row in - match evaluate ctx extended_tuple body with - | Ok true -> check rest - | Ok false -> Ok false - | Error (MembershipFailed _) -> Ok false - | Error d -> Error d - in - check rows -#+end_src - -Symmetric to ~Exists~ but short-circuits on ~Ok false~ or ~MembershipFailed~. -Unlike ~Exists~, other ~Error~ variants (e.g., ~UnboundedQuantifier~) are -propagated rather than silently consumed. The cost model is identical: O(∏ nᵢ · C). - -* The Variable Namespacing Problem - -This section documents the original bug and explains why the current implementation -is correct. In the initial implementation, ~extend_tuple~ took ~variable~ as -~_variable~ — a named-but-discarded argument — and merged quantifier row attributes -flat into the tuple under their original names. This had two consequences. - -** Attribute Shadowing (fixed) - -If the incoming tuple and the quantifier row shared an attribute name, the -quantifier's value won silently. Concretely: an Employee with ~dept_id=99~ being -checked by an ~Exists~ over Department rows would have its ~dept_id~ overwritten -by each Department row's ~dept_id~ in turn. ~(Var "dept_id")~ in the body then -resolved to the Department's own id, not the Employee's. An FK constraint written -as ~(MemberOf (target "Department") (binding ((dept_id (Var "dept_id")))))~ inside -an ~Exists~ over Department would always pass — it was validating the Department -against itself rather than checking whether the Employee's ~dept_id~ existed. - -** Multi-Quantifier Ambiguity (fixed) - -With two nested quantifiers over relations sharing attribute names, the inner -quantifier's pass through ~extend_tuple~ overwrote what the outer one had written. -There was no way to write a body that simultaneously referred to attributes from -two distinct quantifier rows of the same name. - -** Resolution - -Both problems are resolved by namespacing: each attribute ~k~ from the quantifier -row is stored as ~variable ^ "." ^ k~. The base tuple is never modified. The -~variable~ argument, previously discarded as ~_variable~, is now the namespace -prefix. The fix is in ~lib/constraint.ml~ with an inline TODO describing the -deeper issue of tuple-level provenance as a structural solution. - -* N-Ary Quantification - -The current AST represents each quantifier as a single ~(variable, quantifier)~ -pair. N-ary constraints across three or more relations require nesting: - -#+begin_src lisp -(Exists (variable "b") (quantifier "Building") - (Exists (variable "r") (quantifier "Room") - (Exists (variable "s") (quantifier "Suite") - ...))) -#+end_src - -This is semantically correct once namespacing is in place, but verbose and implies -a strict left-to-right evaluation order with no opportunity for reordering. - -The proposed n-ary form makes the binding list first-class: - -#+begin_src lisp -(Exists - (bindings ((b "Building") (r "Room") (s "Suite"))) - (body ...)) -#+end_src - -The executor folds over the binding list left-to-right, extending the tuple at -each step — equivalent to nested ~Exists~ but expressed as a single node: - -#+begin_src ocaml -| Exists { bindings; body } -> - let rec go bindings tuple = - match bindings with - | [] -> evaluate ctx tuple body - | (variable, quantifier) :: rest -> - match ctx.iterate_finite quantifier with - | None -> Error (UnboundedQuantifier { variable; quantifier }) - | Some rows -> - let rec check = function - | [] -> Ok false - | row :: rest' -> - let extended = extend_tuple tuple variable row in - match go rest extended with - | Ok true -> Ok true - | Ok false | Error _ -> check rest' - in - check rows - in - go bindings tuple -#+end_src - -The cost remains O(∏ nᵢ · C) — the n-ary form does not change the complexity, -but it makes the binding structure explicit and opens the door to reordering -optimisations (e.g., evaluate the smallest relation first). - -* Performance Inventory - -The following is a precise account of known costs and inefficiencies, intended -as a reference for future optimisation work. - -** Eager Full Materialisation of Quantifier Relations - -~iterate_finite~ loads every tuple in the quantifier relation from storage before -the first body evaluation begins. For a ~Forall~ whose first body call returns -~Ok false~, all subsequent tuples were loaded needlessly. A streaming/lazy -iterator would allow early termination before full materialisation. - -** Linear Scan in ~check_membership~ - -Every ~MemberOf~ check performs a full linear scan over all tuple hashes in the -target relation's Merkle tree. There are no secondary indexes. For a relation of -cardinality /n/: - -- /n/ calls to ~Storage.load_raw~ to fetch stored tuples. -- For each tuple, up to /a/ additional ~Storage.load_raw~ calls to fetch - attribute values. -- Comparison via structural equality (~Stdlib.(=)~) on unmarshalled ~Obj.t~ values. - -An index mapping ~(relation_name, attr_name, value_hash)~ to tuple hashes would -reduce this to O(log n) or O(1) per ~MemberOf~ check. - -** AttributeMap Allocation per ~extend_tuple~ Call - -~extend_tuple~ allocates a new ~AttributeMap~ on every invocation by folding over -the row into the existing map. For nested quantifiers of cardinalities -/n₁ × n₂ × ... × nq/, this allocates ∏ nᵢ maps during a single constraint check. -A persistent/functional map amortises this somewhat (structural sharing), but -each call still produces a new root node. - -A flat association list or array, indexed by a fixed schema, would be cheaper -for extend and lookup at the cost of schema rigidity. - -** Redundant Storage Loads Across Constraints - -The ~eval_context~ is built once per ~create_tuple~ call, but it is not a cache — -every ~check_membership~ and ~iterate_finite~ call re-reads from storage. If a -relation is referenced in multiple constraints or multiple ~MemberOf~ nodes within -one constraint tree, its tuples are loaded multiple times. - -A constraint-session cache (a ~Hashtbl~ from relation_name to materialised rows, -populated lazily on first access) would eliminate redundant loads within a single -tuple insertion. - -** No Short-Circuit Across Named Constraints - -~evaluate_named~ evaluates every constraint in the named list, collecting all -failures before returning: - -#+begin_src ocaml -let failures = - List.filter_map - (fun (name, c) -> - match evaluate ctx tuple c with - | Ok true -> None - | Ok false -> Some (name, ...) - | Error d -> Some (name, d)) - named -in -#+end_src - -For a tuple that violates the first constraint, all remaining constraints are -still evaluated at full cost. Short-circuiting on first failure is correct when -complete diagnostics are not required (e.g., interactive insertion). A lazy stream -of failures, computed on demand, would support both use cases. - -** Cartesian Product Complexity of Nested Quantifiers - -For /q/ nested ~Exists~/~Forall~ quantifiers over relations of cardinalities -/n₁, n₂, ..., nq/ with body cost /C/: - - Worst-case body evaluations = n₁ × n₂ × ... × nq - - Worst-case storage loads = (∑ nᵢ · kᵢ) + n₁ · n₂ · ... · nq · C_membership - -Where /kᵢ/ is the attribute count of relation /i/ and /C_membership/ is the cost -of ~check_membership~ on the body's target relation. - -Mitigations: -- *Evaluate smallest relation first* (selectivity-based reordering): reduces the - Cartesian product by pruning earlier. -- *Push ~MemberOf~ filters into the iteration*: instead of iterating all rows of - the quantifier relation and then checking membership, filter the quantifier rows - during iteration using the same index that would accelerate ~check_membership~. -- *Semi-join reduction*: for FK-style constraints, a single hash lookup suffices - and no Cartesian product is needed. - -* Summary of Call Chain for a Single Tuple Insertion - -#+begin_example -create_tuple - └── build_eval_context (storage, db) [once per insertion] - └── evaluate_named ctx tuple named_constraints [once per insertion] - └── evaluate ctx tuple c [once per named constraint] - ├── Exists / Forall - │ └── iterate_finite quantifier [materialises full relation] - │ ├── Merkle.keys tree - │ └── Storage.load_raw × (n × k) - │ └── for each row: - │ ├── extend_tuple [allocates new AttributeMap] - │ └── evaluate ctx extended_tuple body - │ └── MemberOf - │ ├── bind [resolves Vars from extended tuple] - │ └── check_membership target bound_values - │ ├── Merkle.keys tree - │ └── Storage.load_raw × (n' × (1 + a)) - └── And / Or / Not - └── evaluate (recursive) -#+end_example diff --git a/docs/dcl.org b/docs/dcl.org new file mode 100644 index 0000000..92fc19d --- /dev/null +++ b/docs/dcl.org @@ -0,0 +1,105 @@ +#+TITLE: DCL — Database Control Language + +DCL manages branches: named pointers to database states. It provides +Git-like operations built on Sakura's append-only, content-addressed +storage. Every mutation automatically advances the current branch tip, +so you never need to track hashes manually. + +* Syntax reference + +| Command | Effect | +|--------------------------------------------+--------------------------------------| +| ~(CreateBranch (name N))~ | Create branch N at current state | +| ~(CreateBranch (name N) (hash H))~ | Create branch N at a specific hash | +| ~(Checkout N)~ | Switch to branch N, restore its db | +| ~(GetHead)~ | Print the current HEAD branch name | +| ~(GetBranchTip N)~ | Print the stored hash of branch N | +| ~(UpdateBranchTip (name N) (hash H))~ | Manually advance branch N to hash H | +| ~(Merge (left L) (right R) (strategy S))~ | 3-way merge branch R into L | + +Branch state is always queryable as relations: + +#+begin_src sexp +(Base sakura:branch) ; name × hash for every branch +(Base sakura:head) ; single-tuple: current branch name +#+end_src + +Merge strategies: + +| Strategy | Behaviour on conflict | +|--------------------+----------------------------------------------| +| ~PreferLeft~ | Keep the left branch's version | +| ~PreferRight~ | Keep the right branch's version | +| ~RevertToAncestor~ | Revert conflicting relation to the LCA state | + +* Example: travelling through history + +#+begin_src sexp +(CreateRelation (name "scores") (schema ((player "string") (pts "integer")))) + +(CreateBranch (name "v0")) + +(InsertTuple (relation "scores") (attributes ((player (Str "Alice")) (pts (Int 10))))) + +(CreateBranch (name "v1")) + +(InsertTuple (relation "scores") (attributes ((player (Str "Bob")) (pts (Int 25))))) + +(CreateBranch (name "v2")) +#+end_src + +Now jump around and watch the relation change: + +#+begin_src sexp +(Checkout "v0") +(Base scores) +; (0 rows) + +(Checkout "v1") +(Base scores) +; ┌────────┬─────┐ +; │ player │ pts │ +; ├────────┼─────┤ +; │ Alice │ 10 │ +; └────────┴─────┘ + +(Checkout "v2") +(Base scores) +; ┌────────┬─────┐ +; │ player │ pts │ +; ├────────┼─────┤ +; │ Alice │ 10 │ +; │ Bob │ 25 │ +; └────────┴─────┘ +#+end_src + +* Example: diverge and merge + +#+begin_src sexp +(Checkout "master") +(CreateBranch (name "feature")) + +(Checkout "master") +(InsertTuple (relation "users") (attributes ((id (Int 1)) (name (Str "Alice"))))) + +(Checkout "feature") +(InsertTuple (relation "users") (attributes ((id (Int 2)) (name (Str "Bob"))))) + +(Merge (left "master") (right "feature") (strategy PreferLeft)) + +(Checkout "master") +(Base users) +; ┌────┬───────┐ +; │ id │ name │ +; ├────┼───────┤ +; │ 1 │ Alice │ +; │ 2 │ Bob │ +; └────┴───────┘ +#+end_src + +* See also + +- ~lib/dcl/~ — AST, parser, executor +- ~lib/management/branch.ml~ — branch registry and ephemeral relations +- ~lib/management/merge.ml~ — 3-way merge engine +- ~lib/management/diff.ml~ — relation diff used internally by merge diff --git a/docs/icl-quantification.org b/docs/icl-quantification.org new file mode 100644 index 0000000..7a81551 --- /dev/null +++ b/docs/icl-quantification.org @@ -0,0 +1,480 @@ +#+TITLE: ICL Quantification: Runtime Model and Evaluation + +* Overview + +This document describes precisely how ICL constraints are represented, compiled, +and evaluated at runtime. It covers the full stack from the s-expression syntax +through AST compilation, context construction, and recursive evaluation — with +particular attention to the cost model of quantifiers, which is the primary target +for future performance work. + +* Constraint Type (~lib/constraint.ml~) + +The runtime constraint type is an algebraic tree: + +#+begin_src ocaml +type t = + | MemberOf of { target : relation_name; binding : binding } + | Not of { body : t; universe : relation_name } + | And of t list + | Or of t list + | Exists of { variable : attr_name; quantifier : relation_name; body : t } + | Forall of { variable : attr_name; quantifier : relation_name; body : t } +#+end_src + +A ~binding~ is a ~BindingMap~ (a ~Map.Make(String)~) from target attribute names +to ~binding_expr~: + +#+begin_src ocaml +type binding_expr = + | Var of attr_name (* resolved from current tuple at eval time *) + | Const of Conventions.AbstractValue.t (* literal, resolved at compile time *) +#+end_src + +The ~variable~ field in ~Exists~ and ~Forall~ names the bound tuple for use in +~Var~ expressions inside the body. Attributes from the quantifier row are merged +into the evaluation tuple under the prefix ~variable ^ "."~, so ~(Var "d.dept_id")~ +unambiguously refers to the ~dept_id~ attribute of the tuple bound to variable ~"d"~. +See [[*Tuple Extension: ~extend_tuple~][Tuple Extension: extend_tuple]] for the implementation and [[*The Variable Namespacing Problem][The Variable Namespacing Problem]] +for the history of the bug this fixes. + +* Evaluation Context (~eval_context~) + +Evaluation does not access storage or the database directly. It works through an +~eval_context~ record built once per insert operation and closed over a specific +~(storage, db)~ snapshot: + +#+begin_src ocaml +type eval_context = { + check_membership : + relation_name -> + (attr_name * Conventions.AbstractValue.t) list -> + bool; + iterate_finite : + relation_name -> + (attr_name * Conventions.AbstractValue.t) list list option; +} +#+end_src + +Both fields are closures. This indirection decouples ~Constraint.evaluate~ from +the storage backend and allows the same constraint tree to be evaluated against +different snapshots. + +** ~check_membership~ + +Built in ~Manipulation.Make.build_eval_context~. Given a relation name and a list +of ~(attr_name, value)~ pairs, it returns ~true~ iff a tuple exists in the named +relation whose attributes match every pair in the list. + +The implementation: +1. Looks up the relation in the ~db~ snapshot. +2. Constructs a synthetic ~Tuple.Materialized~ from the bound pairs and runs + ~rel.membership_criteria~ against it. If it fails, returns ~false~ immediately. +3. If the relation has no Merkle tree (ephemeral/generator relation), + ~membership_criteria~ alone is trusted and the function returns ~true~. +4. If the relation has a tree, it calls ~Merkle.keys tree~ to obtain *all* tuple + hashes, then linearly scans them. For each hash it: + a. Loads the raw bytes from storage (~Storage.load_raw~). + b. Deserialises the ~Storable.Tuple.t~ to get the attribute hash list. + c. For each bound pair ~(bk, bv)~, finds the matching attribute by name, loads + its value bytes from storage (~Storage.load_raw~ again), unmarshals it, and + compares with ~Stdlib.(=)~. + d. Short-circuits to ~true~ on the first tuple that satisfies all pairs. + e. Returns ~false~ if no tuple matches. + +The cost of a single ~check_membership~ call on a relation of cardinality /n/ with +/a/ bound attributes and average /k/ attributes per stored tuple is: + + O(n · (1 + a · k)) storage round-trips in the worst case. + +No indexes exist. Every check is a full table scan at the storage level. + +** ~iterate_finite~ + +Given a relation name, returns ~Some rows~ where ~rows~ is a fully materialised +list of rows, each a ~(attr_name * AbstractValue.t) list~. Returns ~None~ if the +relation has infinite or unconstrained cardinality +(~AlephZero~ or ~Continuum~ in ~Conventions.Cardinality~). + +Only relations with cardinality ~Finite _~ or ~ConstrainedFinite~ are iterable. +Generator-based relations with no tree return ~Some []~. + +The materialisation path: +1. ~Merkle.keys tree~ — loads all tuple hashes. +2. For each hash: ~Storage.load_raw~ → ~Storable.Tuple.of_bytes~ → attribute hash list. +3. For each attribute hash: ~Storage.load_raw~ → ~Marshal.from_bytes~. + +This eagerly materialises the *entire* quantifier relation into memory before +evaluation begins. For a relation of cardinality /n/ with /k/ attributes each, +the cost is O(n · k) storage loads and the full result occupies O(n · k) memory. + +* Variable Resolution: ~bind~ + +Before a ~MemberOf~ check is executed, the binding map is resolved against the +current tuple via ~bind~: + +#+begin_src ocaml +let bind (b : binding) (tuple : Tuple.materialized) + : (attr_name * Conventions.AbstractValue.t) list = + BindingMap.fold + (fun target_attr expr acc -> + let value = match expr with + | Const v -> Some v + | Var src_attr -> + match Tuple.AttributeMap.find_opt src_attr tuple.attributes with + | Some attr -> Some attr.Attribute.value + | None -> None + in + match value with + | Some v -> (target_attr, v) :: acc + | None -> acc) + b [] +#+end_src + +Key behaviour: +- ~Const v~ is lifted directly; no attribute lookup. +- ~Var src_attr~ looks up ~src_attr~ in ~tuple.attributes~. If the attribute is + absent, the pair is *silently dropped* from the bound list. A ~MemberOf~ with + incomplete bindings may match unintended tuples or always pass if the target + relation contains tuples with fewer attributes. +- The result is a plain assoc list, not a map; duplicate keys are possible if + the binding contains both a ~Const~ and a ~Var~ targeting the same name. + +* Tuple Extension: ~extend_tuple~ + +When a quantifier (~Exists~ or ~Forall~) iterates over a row, it extends the +current evaluation tuple by merging that row's attributes in: + +#+begin_src ocaml +and extend_tuple (tuple : Tuple.materialized) + (variable : attr_name) + (row : (attr_name * Conventions.AbstractValue.t) list) + : Tuple.materialized = + let extra_attrs = + List.fold_left + (fun acc (k, v) -> + Tuple.AttributeMap.add (variable ^ "." ^ k) { Attribute.value = v } acc) + tuple.attributes row + in + { tuple with attributes = extra_attrs } +#+end_src + +Two important facts: + +1. *Quantifier attributes are namespaced by the variable name.* Each attribute ~k~ + from the quantifier row is inserted as ~variable ^ "." ^ k~. The incoming tuple's + own attributes are never overwritten. ~(Var "dept_id")~ resolves to the base + tuple's value; ~(Var "d.dept_id")~ resolves to the value contributed by the + quantifier bound to ~"d"~. See [[*The Variable Namespacing Problem][The Variable Namespacing Problem]] for the + earlier behaviour where ~variable~ was ignored and overwrites were silent. + +2. *A new ~AttributeMap~ is allocated on every extend call.* With /a/ existing + attributes and /r/ new attributes from the row, ~fold_left~ performs /r/ + ~AttributeMap.add~ operations each building on the previous map. For /q/ + nested quantifiers of cardinalities /n₁, n₂, ..., nq/, ~extend_tuple~ is + called /n₁ · n₂ · ... · nq/ times total — once per combination. + +* Recursive Evaluation: ~evaluate~ + +#+begin_src ocaml +let rec evaluate (ctx : eval_context) (tuple : Tuple.materialized) (c : t) + : (bool, diagnostic) result = +#+end_src + +The function is structurally recursive over the constraint tree. Each case: + +** ~MemberOf~ + +#+begin_src ocaml +| MemberOf { target; binding } -> + let bound_values = bind binding tuple in + if ctx.check_membership target bound_values then Ok true + else Error (MembershipFailed { target; bound_values }) +#+end_src + +Resolves bindings from the current tuple (O(|binding|) attribute lookups), then +delegates to ~check_membership~. Returns ~Ok true~ or ~Error~ (never ~Ok false~) +— the ~Ok false~ branch of ~Exists~/~Forall~ is distinguished from ~Error~. + +** ~Not~ + +#+begin_src ocaml +| Not { body; universe = _ } -> + match evaluate ctx tuple body with + | Ok true -> Ok false + | Ok false -> Ok true + | Error (MembershipFailed _) -> Ok true + | Error d -> Error d +#+end_src + +~MembershipFailed~ from the body is treated as ~Ok true~ (negation of a failed +membership = the tuple is not a member = negation succeeds). The ~universe~ field +is a declarative annotation for closed-world reasoning and is not used at runtime. + +** ~And~ / ~Or~ + +Both use short-circuit evaluation: +- ~And~: stops at the first ~Ok false~ or ~Error~. +- ~Or~: stops at the first ~Ok true~; swallows ~Error~ branches and continues. + +Neither produces diagnostics for the other branches once a decision is reached. +Note that ~evaluate_named~ (which evaluates all named constraints on a tuple) does +*not* short-circuit — it collects all failures before returning. + +** ~Exists~ + +#+begin_src ocaml +| Exists { variable; quantifier; body } -> + match ctx.iterate_finite quantifier with + | None -> Error (UnboundedQuantifier { variable; quantifier }) + | Some rows -> + let rec check = function + | [] -> Ok false + | row :: rest -> + let extended_tuple = extend_tuple tuple variable row in + match evaluate ctx extended_tuple body with + | Ok true -> Ok true + | Ok false -> check rest + | Error _ -> check rest + in + check rows +#+end_src + +The execution model: +1. ~iterate_finite~ is called, fully materialising the quantifier relation. +2. Rows are iterated sequentially. For each row, ~extend_tuple~ merges it into + the current tuple, and ~evaluate~ recurses into the body. +3. The first ~Ok true~ short-circuits: remaining rows are not evaluated. +4. Both ~Ok false~ and ~Error~ from the body are treated identically — the row is + skipped and iteration continues. *Errors inside the body of an ~Exists~ are + silently discarded.* +5. If all rows are exhausted without ~Ok true~, returns ~Ok false~. + +An ~Exists~ over a relation of cardinality /n/ with a body whose evaluation cost +is /C/ has worst-case cost O(n · C). Nesting two ~Exists~ quantifiers over +relations of cardinalities /n/ and /m/ has worst-case cost O(n · m · C). +In general, /q/ nested quantifiers produce O(∏ nᵢ · C) body evaluations — a +Cartesian product. + +** ~Forall~ + +#+begin_src ocaml +| Forall { variable; quantifier; body } -> + match ctx.iterate_finite quantifier with + | None -> Error (UnboundedQuantifier { variable; quantifier }) + | Some rows -> + let rec check = function + | [] -> Ok true + | row :: rest -> + let extended_tuple = extend_tuple tuple variable row in + match evaluate ctx extended_tuple body with + | Ok true -> check rest + | Ok false -> Ok false + | Error (MembershipFailed _) -> Ok false + | Error d -> Error d + in + check rows +#+end_src + +Symmetric to ~Exists~ but short-circuits on ~Ok false~ or ~MembershipFailed~. +Unlike ~Exists~, other ~Error~ variants (e.g., ~UnboundedQuantifier~) are +propagated rather than silently consumed. The cost model is identical: O(∏ nᵢ · C). + +* The Variable Namespacing Problem + +This section documents the original bug and explains why the current implementation +is correct. In the initial implementation, ~extend_tuple~ took ~variable~ as +~_variable~ — a named-but-discarded argument — and merged quantifier row attributes +flat into the tuple under their original names. This had two consequences. + +** Attribute Shadowing (fixed) + +If the incoming tuple and the quantifier row shared an attribute name, the +quantifier's value won silently. Concretely: an Employee with ~dept_id=99~ being +checked by an ~Exists~ over Department rows would have its ~dept_id~ overwritten +by each Department row's ~dept_id~ in turn. ~(Var "dept_id")~ in the body then +resolved to the Department's own id, not the Employee's. An FK constraint written +as ~(MemberOf (target "Department") (binding ((dept_id (Var "dept_id")))))~ inside +an ~Exists~ over Department would always pass — it was validating the Department +against itself rather than checking whether the Employee's ~dept_id~ existed. + +** Multi-Quantifier Ambiguity (fixed) + +With two nested quantifiers over relations sharing attribute names, the inner +quantifier's pass through ~extend_tuple~ overwrote what the outer one had written. +There was no way to write a body that simultaneously referred to attributes from +two distinct quantifier rows of the same name. + +** Resolution + +Both problems are resolved by namespacing: each attribute ~k~ from the quantifier +row is stored as ~variable ^ "." ^ k~. The base tuple is never modified. The +~variable~ argument, previously discarded as ~_variable~, is now the namespace +prefix. The fix is in ~lib/constraint.ml~ with an inline TODO describing the +deeper issue of tuple-level provenance as a structural solution. + +* N-Ary Quantification + +The current AST represents each quantifier as a single ~(variable, quantifier)~ +pair. N-ary constraints across three or more relations require nesting: + +#+begin_src lisp +(Exists (variable "b") (quantifier "Building") + (Exists (variable "r") (quantifier "Room") + (Exists (variable "s") (quantifier "Suite") + ...))) +#+end_src + +This is semantically correct once namespacing is in place, but verbose and implies +a strict left-to-right evaluation order with no opportunity for reordering. + +The proposed n-ary form makes the binding list first-class: + +#+begin_src lisp +(Exists + (bindings ((b "Building") (r "Room") (s "Suite"))) + (body ...)) +#+end_src + +The executor folds over the binding list left-to-right, extending the tuple at +each step — equivalent to nested ~Exists~ but expressed as a single node: + +#+begin_src ocaml +| Exists { bindings; body } -> + let rec go bindings tuple = + match bindings with + | [] -> evaluate ctx tuple body + | (variable, quantifier) :: rest -> + match ctx.iterate_finite quantifier with + | None -> Error (UnboundedQuantifier { variable; quantifier }) + | Some rows -> + let rec check = function + | [] -> Ok false + | row :: rest' -> + let extended = extend_tuple tuple variable row in + match go rest extended with + | Ok true -> Ok true + | Ok false | Error _ -> check rest' + in + check rows + in + go bindings tuple +#+end_src + +The cost remains O(∏ nᵢ · C) — the n-ary form does not change the complexity, +but it makes the binding structure explicit and opens the door to reordering +optimisations (e.g., evaluate the smallest relation first). + +* Performance Inventory + +The following is a precise account of known costs and inefficiencies, intended +as a reference for future optimisation work. + +** Eager Full Materialisation of Quantifier Relations + +~iterate_finite~ loads every tuple in the quantifier relation from storage before +the first body evaluation begins. For a ~Forall~ whose first body call returns +~Ok false~, all subsequent tuples were loaded needlessly. A streaming/lazy +iterator would allow early termination before full materialisation. + +** Linear Scan in ~check_membership~ + +Every ~MemberOf~ check performs a full linear scan over all tuple hashes in the +target relation's Merkle tree. There are no secondary indexes. For a relation of +cardinality /n/: + +- /n/ calls to ~Storage.load_raw~ to fetch stored tuples. +- For each tuple, up to /a/ additional ~Storage.load_raw~ calls to fetch + attribute values. +- Comparison via structural equality (~Stdlib.(=)~) on unmarshalled ~Obj.t~ values. + +An index mapping ~(relation_name, attr_name, value_hash)~ to tuple hashes would +reduce this to O(log n) or O(1) per ~MemberOf~ check. + +** AttributeMap Allocation per ~extend_tuple~ Call + +~extend_tuple~ allocates a new ~AttributeMap~ on every invocation by folding over +the row into the existing map. For nested quantifiers of cardinalities +/n₁ × n₂ × ... × nq/, this allocates ∏ nᵢ maps during a single constraint check. +A persistent/functional map amortises this somewhat (structural sharing), but +each call still produces a new root node. + +A flat association list or array, indexed by a fixed schema, would be cheaper +for extend and lookup at the cost of schema rigidity. + +** Redundant Storage Loads Across Constraints + +The ~eval_context~ is built once per ~create_tuple~ call, but it is not a cache — +every ~check_membership~ and ~iterate_finite~ call re-reads from storage. If a +relation is referenced in multiple constraints or multiple ~MemberOf~ nodes within +one constraint tree, its tuples are loaded multiple times. + +A constraint-session cache (a ~Hashtbl~ from relation_name to materialised rows, +populated lazily on first access) would eliminate redundant loads within a single +tuple insertion. + +** No Short-Circuit Across Named Constraints + +~evaluate_named~ evaluates every constraint in the named list, collecting all +failures before returning: + +#+begin_src ocaml +let failures = + List.filter_map + (fun (name, c) -> + match evaluate ctx tuple c with + | Ok true -> None + | Ok false -> Some (name, ...) + | Error d -> Some (name, d)) + named +in +#+end_src + +For a tuple that violates the first constraint, all remaining constraints are +still evaluated at full cost. Short-circuiting on first failure is correct when +complete diagnostics are not required (e.g., interactive insertion). A lazy stream +of failures, computed on demand, would support both use cases. + +** Cartesian Product Complexity of Nested Quantifiers + +For /q/ nested ~Exists~/~Forall~ quantifiers over relations of cardinalities +/n₁, n₂, ..., nq/ with body cost /C/: + + Worst-case body evaluations = n₁ × n₂ × ... × nq + + Worst-case storage loads = (∑ nᵢ · kᵢ) + n₁ · n₂ · ... · nq · C_membership + +Where /kᵢ/ is the attribute count of relation /i/ and /C_membership/ is the cost +of ~check_membership~ on the body's target relation. + +Mitigations: +- *Evaluate smallest relation first* (selectivity-based reordering): reduces the + Cartesian product by pruning earlier. +- *Push ~MemberOf~ filters into the iteration*: instead of iterating all rows of + the quantifier relation and then checking membership, filter the quantifier rows + during iteration using the same index that would accelerate ~check_membership~. +- *Semi-join reduction*: for FK-style constraints, a single hash lookup suffices + and no Cartesian product is needed. + +* Summary of Call Chain for a Single Tuple Insertion + +#+begin_example +create_tuple + └── build_eval_context (storage, db) [once per insertion] + └── evaluate_named ctx tuple named_constraints [once per insertion] + └── evaluate ctx tuple c [once per named constraint] + ├── Exists / Forall + │ └── iterate_finite quantifier [materialises full relation] + │ ├── Merkle.keys tree + │ └── Storage.load_raw × (n × k) + │ └── for each row: + │ ├── extend_tuple [allocates new AttributeMap] + │ └── evaluate ctx extended_tuple body + │ └── MemberOf + │ ├── bind [resolves Vars from extended tuple] + │ └── check_membership target bound_values + │ ├── Merkle.keys tree + │ └── Storage.load_raw × (n' × (1 + a)) + └── And / Or / Not + └── evaluate (recursive) +#+end_example diff --git a/docs/icl.org b/docs/icl.org new file mode 100644 index 0000000..c2258bf --- /dev/null +++ b/docs/icl.org @@ -0,0 +1,108 @@ +#+TITLE: ICL — Integrity Control Language + +ICL registers integrity constraints on relations. A constraint is a +membership check: before any tuple is inserted, Sakura verifies that +the tuple belongs to every constraint-relation attached to the target +relation. + +Constraints are expressed as S-expressions and sent over the wire like +any other command. + +* Syntax + +#+begin_src +(RegisterConstraint + (constraint_name "") + (relation_name "") + (body )) +#+end_src + +A ~~ is one of: + +| Form | Meaning | +|-------------------------------------------------+--------------------------------| +| ~(MemberOf (target R) (binding (...)))~ | Tuple must be in relation R | +| ~(Not (body B) (universe R))~ | Negation (closed-world over R) | +| ~(And (B1 B2 ...))~ | All must hold | +| ~(Or (B1 B2 ...))~ | At least one must hold | +| ~(Exists (variable v) (quantifier R) (body B))~ | ∃ v ∈ R such that B holds | +| ~(Forall (variable v) (quantifier R) (body B))~ | ∀ v ∈ R, B holds | + +Bindings map target-relation attribute names to values drawn from the +tuple being checked: + +| Binding expr | Meaning | +|---------------------+--------------------------------| +| ~(Var "attr")~ | Value of ~attr~ from the tuple | +| ~(Const (Int N))~ | Literal integer N | +| ~(Const (Str "s"))~ | Literal string s | +| ~(Const (Float f))~ | Literal float f | + +* Examples + +** Foreign key + +#+begin_src sexp +(CreateRelation (name "Department") (schema ((dept_id "integer") (dept_name "string")))) +(CreateRelation (name "Employee") (schema ((emp_id "integer") (emp_name "string") (dept_id "integer")))) + +(RegisterConstraint + (constraint_name "fk_employee_dept") + (relation_name "Employee") + (body (MemberOf + (target "Department") + (binding ((dept_id (Var "dept_id"))))))) +#+end_src + +** Range check + +#+begin_src sexp +(CreateRelation (name "Result") (schema ((student_id "integer") (score "integer")))) + +(RegisterConstraint + (constraint_name "score_range") + (relation_name "Result") + (body (And + ((MemberOf (target "greater_than_or_equal_natural") + (binding ((left (Var "score")) (right (Const (Int 0)))))) + (MemberOf (target "less_than_or_equal_natural") + (binding ((left (Var "score")) (right (Const (Int 100)))))))))) +#+end_src + +** Existential (FK through a join) + +A ~Suite~ is only valid if its room belongs to a building with more +than 3 floors: + +#+begin_src sexp +(CreateRelation (name "Building") (schema ((building_id "integer") (building_name "string") (floors "integer")))) +(CreateRelation (name "Room") (schema ((room_id "integer") (building_id "integer") (floor "integer")))) +(CreateRelation (name "Suite") (schema ((suite_id "integer") (room_id "integer") (suite_name "string")))) + +(RegisterConstraint + (constraint_name "suite_in_tall_building") + (relation_name "Suite") + (body + (Exists (variable "r") (quantifier "Room") + (body + (Exists (variable "b") (quantifier "Building") + (body + (And + ((MemberOf (target "Room") + (binding ((room_id (Var "room_id"))))) + (MemberOf (target "Building") + (binding ((building_id (Var "r.building_id"))))) + (MemberOf (target "greater_than_natural") + (binding ((left (Var "b.floors")) + (right (Const (Int 3)))))))))))))) +#+end_src + +Note: quantifier variables are namespaced — attributes from variable +~r~ are accessed as ~r.attr_name~ inside nested scopes. + +* See also + +- ~lib/icl/~ — AST, parser, executor +- ~lib/constraint.ml~ — runtime constraint representation and evaluator +- ~docs/icl-quantification.org~ — full runtime model for ~Exists~/~Forall~ +- ~docs/constraints.org~ — conceptual background diff --git a/docs/karuta-integration.org b/docs/karuta-integration.org index a144a25..0642254 100644 --- a/docs/karuta-integration.org +++ b/docs/karuta-integration.org @@ -14,10 +14,26 @@ Here's an overview of the sublanguages and how they are manifested in Karuta: - Pure querying, total/terminating subset; - No user recursion with no self references. -** DCL (Data Constraint Language) +** ICL (Integrity Control Language) - Integrity rules (key, FK-like, checks, assertions, aggregates-for-integrity). - Semantically predicates, but with enforcement timing (on write/commit), not free query operators. +- Implemented in =lib/icl/= (=Ast=, =Parser=, =Executor=). + +** DCL (Database Control Language) + +- Branch management: create/checkout branches, query HEAD and tip hashes. +- Merge: 3-way merge of two branch tips with configurable conflict strategy (=PreferLeft=, =PreferRight=, =RevertToAncestor=). +- Implemented in =lib/dcl/= (=Ast=, =Parser=, =Executor=). +- Example commands: + #+begin_src sexp + (CreateBranch (name "feature") (tip "")) + (Checkout "feature") + (GetHead) + (GetBranchTip "main") + (UpdateBranchTip (name "main") (tip "")) + (Merge (left "main") (right "feature") (strategy PreferLeft)) + #+end_src ** DML (Data Manipulation Language) @@ -35,7 +51,7 @@ Here's an overview of the sublanguages and how they are manifested in Karuta: ** PPL (Procedural Predicate Language) - Stored procedures/functions, recursion allowed, orchestration logic. -- Can call DRL/DML/DCL-aware operations, but not all PPL predicates are DRL-safe. +- Can call DRL/DML/ICL/DCL-aware operations, but not all PPL predicates are DRL-safe. ** ACL (Authorization/Policy Language) (optional early, important later) @@ -62,21 +78,21 @@ Here's an overview of the sublanguages and how they are manifested in Karuta: person[string, natural] :: sakura:persisted person[Name, Age] :- valid_age[Age]. - % DCL + % ICL another-constraint[list[person], string, natural] :: sakura:constraint another-constraint[[], _, _]. another-constraint[[person[Name, Age]|Rest], Whatever1, Whatever2] :- (eq[Name, Whatever1] ; !eq[Name, Whatever1], !eq[Age, Whatever2]), another-constraint[Rest, Whatever1, Whatever2]. - % DCL + % ICL my-predicate[int, string, nat] :: sakura:constraint my-predicate[Arg1, Arg2, Arg3] :- another-module:my-predicate[Arg1, Arg2, Arg3], on[insert, update], timing[immediate]. - % DCL + % ICL valid_age/1 :: sakura:constraint valid_age[Age] with [karuta, sakura] :- nat[Age], diff --git a/docs/n-way-binding.org b/docs/n-way-binding.org index 39c9d65..85dc0e3 100644 --- a/docs/n-way-binding.org +++ b/docs/n-way-binding.org @@ -1,9 +1,9 @@ -#+TITLE: N-Way Binding in DCL Constraints +#+TITLE: N-Way Binding in ICL Constraints #+DATE: 2026-03-11 * Overview -The DCL constraint language supports quantified membership checks via ~Exists~ and ~Forall~. +The ICL constraint language supports quantified membership checks via ~Exists~ and ~Forall~. This document illustrates the hotel/building/room/suite example to motivate n-ary quantification and show how 3-wise (and deeper) relational composition is expressed. @@ -72,7 +72,7 @@ to fire when suites referencing its rooms are inserted. ((suite_id (Int 1003)) (room_id (Int 102)) (suite_name (Str "Deluxe")) (capacity (Int 3)))))) #+end_src -* DCL — Constraints +* ICL — Constraints Binary FK constraints compose to enforce referential integrity along the chain ~Suite → Room → Building~. Each link is declared independently. @@ -202,5 +202,5 @@ bound to variable ~x~. Without namespacing, ~extend_tuple~ would overwrite the incoming tuple's attributes with same-named attributes from the quantifier row, silently making ~Var~ resolve to -the wrong scope. See ~lib/constraint.ml~ and ~docs/dcl-quantification.org~ for a full +the wrong scope. See ~lib/constraint.ml~ and ~docs/icl-quantification.org~ for a full account of this failure mode and the provenance TODO. -- cgit v1.2.3