#+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
