update docs with partial bindings

1 files changed, 42 insertions, 25 deletions

diff --git a/docs/modes.org b/docs/modes.org
index 2337b29..1cd5905 100644
--- a/docs/modes.org
+++ b/docs/modes.org
@@ -70,14 +70,21 @@ The principle above is wider than what RNT can do today. The
 - =contains= answers with every attribute bound, so it realizes the
   modes whose =bound= is every attribute.
 
-No operation produces the tuples that agree with a partial binding. A
-relation may declare a mode such as ={title; Finite}=, and
-=Mode.generation= takes it into account, but nothing in RNT can act on
-it. In particular, a relation cannot decide membership through a mode
-with a partial binding. It decides only by its own test, or by
-enumerating with nothing bound. A partial mode becomes usable once
-there is an operation that produces tuples under a binding, which is
-also what [[*Indexes][indexes]] need.
+Neither produces the tuples that agree with a partial binding, and RNT
+does not ask every relation for them. A binding is a condition on
+tuples, and conditions belong to a query language, as [[file:partial-bindings.org::*Where a binding belongs][partial bindings]]
+explains. Two pieces reach partial bindings instead.
+
+- A substantial relation offers =lookup= through the [[file:../lib/protocols/Indexed.mli][Indexed]] protocol,
+  the tuples whose attribute =a= holds a given value, read from its
+  index on =a=. That realizes its mode ={a; Finite}=.
+- A FOL =Where= restricts a plan to the tuples that agree with a
+  binding, and reads an index when its input offers one, as [[*Modes of a FOL plan][the modes
+  of a FOL plan]] describe.
+
+A mode with a partial =bound= that neither reaches is still declared and
+unused. A relation still decides membership only by its own test, or by
+enumerating with nothing bound.
 
 * How contains decides
 A substantial relation looks the tuple up by its hash.
@@ -104,9 +111,10 @@ evaluator gave it whatever test it could.
 
 * What relations declare
 A substantial relation stores its tuples in a set keyed by the hash of
-each whole tuple. It declares ={∅; Finite}= for enumerating that set,
-and ={all; Bounded 1}= for the lookup by hash, which needs every
-attribute to compute the hash.
+each whole tuple, and keeps an [[*Indexes][index]] on each attribute. It declares
+={∅; Finite}= for enumerating that set, ={all; Bounded 1}= for the lookup
+by hash, which needs every attribute to compute the hash, and
+={a; Finite}= for the index on each attribute =a=.
 
 An ephemeral relation that =EphemeralRelation.literal= builds from =n=
 tuples declares ={∅; Bounded n}=.
@@ -127,23 +135,34 @@ executes anything, and records them on each relation it derives.
 - =Base r= has the modes of =r=.
 - =Project (p, A)= keeps the modes of =p= whose =bound= lies within
   =A=, with the same =yields=.
+- =Where (Base r, b)=, when =r= offers an index on an attribute =b=
+  binds, has the modes of =r= with the attributes of =b= taken out of
+  each =bound=, by =Mode.given=. The binding supplies their values, and
+  the index produces the tuples, so ={a; Finite}= becomes ={∅; Finite}=.
+- Any other =Where (p, b)= keeps the modes of =p=, since it can only
+  filter what =p= enumerates.
 
 A projection never yields more tuples than its input, so =yields=
 carries over. A mode that needs an attribute outside =A= no longer
-applies, because a tuple of the projection holds no value for it.
+applies, because a tuple of the projection holds no value for it. A
+restriction never yields more tuples than its input either.
 
 Take =book(title, author)= as a substantial relation, projected on
 =title=. Asking whether ={title: "Codd"}= belongs to the projection
 asks whether some book has that title, by any author. The lookup by
-hash needs the author to hash the whole tuple, so the projection keeps
-only ={∅; Finite}=.
+hash needs the author to hash the whole tuple, so the projection loses
+it, and keeps ={∅; Finite}= and the mode ={title; Finite}= of the index
+on =title=.
 
 FOL gives a membership test only where it has one. The relation it
 derives for =Base r= takes the =contains= of =r= as its test, so FOL
 over a substantial relation still looks tuples up by hash. The relation
 it derives for a projection has no test, so its =contains= enumerates
 the projection, which reads all of =book=, and compares. That ends
-because =book= is finite.
+because =book= is finite. Asking the same question as
+=Where (Project (book, title), {title: "Codd"})= reads only the index
+entries for ="Codd"=, since FOL pushes the restriction below the
+projection when the projection keeps every attribute it binds.
 
 A projection of a =Countable= relation stays =Countable=. FOL still
 streams it, since a projection reads one tuple at a time and never
@@ -151,14 +170,11 @@ needs the end. Asking such a projection whether it holds a tuple fails
 with =undecidable-membership=.
 
 * Indexes
-An index on an attribute =a= would be a tree keyed by the value of =a=
-and the hash of the tuple, and would add the mode ={a; Finite}=. A
-projection that keeps =a= keeps that mode, so with one index per
-attribute every membership question could stay a lookup. That takes two
-things RNT does not have, the index trees and an operation that
-produces tuples under a partial binding, as [[*Reachable bindings][reachable bindings]]
-explains. Without the operation, the mode an index adds would be
-declared and never used.
+A substantial relation keeps an index on each attribute =a=, a tree
+keyed by the encoded value of =a= and the hash of the tuple, and each
+adds the mode ={a; Finite}=. A projection that keeps =a= keeps that mode,
+and a FOL =Where= that binds =a= reads only the matching entries.
+[[file:partial-bindings.org][Partial bindings]] describes how the indexes are stored, read and built.
 
 Modes carry no cost. A lookup and a full scan both appear as an
 exhaustible generation, and choosing between them belongs to whatever
@@ -167,5 +183,6 @@ plans the query.
 * Where exhaustion matters
 Only a reader that runs a relation to its end needs it exhaustible.
 =Relation.read= drains a relation, and admission drains every [[file:denial.org][denial]]
-that holds a tuple, so both hang on a =Countable= relation. Neither
-checks modes yet. Denials will check them once they are reworked.
+that holds a tuple, so both hang on a =Countable= relation. Admission
+asks a denial for its modes first and refuses one that does not end.
+=Relation.read= does not check them yet.