update docs with partial bindings

1 files changed, 17 insertions, 14 deletions

diff --git a/docs/maintenance.org b/docs/maintenance.org
index 42b5075..519ea37 100644
--- a/docs/maintenance.org
+++ b/docs/maintenance.org
@@ -26,15 +26,18 @@ the states before and after the commit, operator by operator.
   did not hold before. It loses the projection of a tuple in =Δp⁻= only
   if no other tuple of =p= projects to the same tuple, which is the
   problem [[*Counting][counting]] solves.
+- =Where (p, b)= changes as =p= does, keeping only the changed tuples
+  that agree with =b=.
 - A join, once [[file:../lib/evaluators/FOL.ml][FOL]] has one, gains =ΔR⁺ ⋈ S= and =R ⋈ ΔS⁺=, against the
   right states. Computing =ΔR⁺ ⋈ S= means asking =S= for the tuples that
   agree with each inserted tuple of =R= on the join attributes.
 
 That last question binds some attributes of =S= and leaves the rest
-free. It is the partial binding that no operation in RNT can ask
-today, the gap [[file:modes.org::*Reachable bindings][reachable bindings]] describes. Without it, the only way
-to compute a delta through a join is to read =S= whole, which is
-recomputation by another name.
+free. FOL states it as =Where (S, b)=, for the binding =b= each inserted
+tuple puts on the join attributes, and answers it from the index of a
+stored =S=, as [[file:partial-bindings.org][partial bindings]] describes. Without the index, the only
+way to compute a delta through a join would be to read =S= whole, which
+is recomputation by another name.
 
 * Counting
 Deletion through a projection needs to know how many tuples of the input
@@ -65,26 +68,26 @@ delta rules, stopped at the first tuple. Full maintenance adds
 deletions, counts and storage on top of it.
 
 * What it needs
-Some pieces are shared with incremental denial checking.
+Two pieces both depend on are in place: FOL's =Where=, which restricts a
+plan to a binding and pushes it down to the stored relations, and
+indexes, which answer such a restriction by lookup rather than by a
+filtered scan. Other pieces are shared with incremental denial checking.
 
-1. A binding-aware read, which every relation implements and FOL passes
-   through its plans, to compute deltas through joins.
-2. Indexes, so that such a read is a lookup on a substantial relation
-   rather than a filtered scan.
-3. Read sets, so that RNT knows which relations a derived relation
+1. Read sets, so that RNT knows which relations a derived relation
    reads and how their attributes line up with its own, and can tell
    which relations a commit touches.
-4. Tuple deltas. [[file:../lib/kernel/Path.mli][Path.diff]] names the relations that changed between
+2. Tuple deltas. [[file:../lib/kernel/Path.mli][Path.diff]] names the relations that changed between
    two states, and skips subtrees with equal addresses. The tuples that
    changed inside a relation can be found the same way, by diffing its
    two tuple sets, since a prolly tree shares every unchanged subtree.
    RNT does not expose that diff yet.
+3. Joins in FOL, since the deltas worth computing run through them.
 
 Others belong to maintenance alone.
 
-5. Materialization, so that a derived relation can be stored with its
-   tuples and counts, and read like a substantial relation.
-6. Deletion rules and counts, as above.
+4. Materialization, so that a derived relation can be stored with its
+   tuples, counts and indexes, and read like a substantial relation.
+5. Deletion rules and counts, as above.
 
 * When maintenance runs
 A commit would apply its changes to the base relations, maintain every