update docs with partial bindings

1 files changed, 15 insertions, 10 deletions

diff --git a/docs/denial.org b/docs/denial.org
index d79a394..31d5a58 100644
--- a/docs/denial.org
+++ b/docs/denial.org
@@ -170,18 +170,23 @@ those tuples, with the other shelf free, is the whole incremental check.
 It is the insertion-only case of [[file:maintenance.org][incremental maintenance]], which covers
 the delta rules it reuses.
 
-RNT cannot ask that today. The question binds some attributes of the
-denial and leaves others free, and no operation produces the tuples of
-a relation under a partial binding. This is the gap that [[file:modes.org::*Reachable bindings][reachable
-bindings]] describes. Closing it takes three pieces.
-
-1. A binding-aware read, which every relation implements and FOL passes
-   through its plans.
-2. Indexes, so that a substantial relation answers such a read by
-   lookup rather than by filtering a scan.
-3. Read sets, so that RNT knows which relations a denial reads and how
+The question binds some attributes of the denial and leaves others
+free. FOL can state it as a =Where= over the denial's plan, which it
+pushes down to the stored relations and answers from their indexes, as
+[[file:partial-bindings.org][partial bindings]] describes. A denial that binds attributes of its own,
+such as =Where (Base book, {title: "Codd"})=, is already judged that way,
+reading only the index entries it binds. Checking incrementally still
+takes four pieces.
+
+1. Read sets, so that RNT knows which relations a denial reads and how
    their attributes line up with the denial's, and can turn an inserted
    tuple into bindings on each denial it touches.
+2. Tuple deltas, so that a commit names the tuples it inserted.
+3. A check offered by the evaluator, since the kernel knows no rule
+   language and cannot derive the restriction for a program it cannot
+   read.
+4. Joins in FOL, since this denial and most others worth checking
+   incrementally join two relations.
 
 ** Denials do not protect themselves
 A commit that removes a denial and breaks its rule is judged on the