diff options
Diffstat (limited to 'docs/modes.org')
| -rw-r--r-- | docs/modes.org | 67 |
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. |