#+TITLE: Modes * Extension and intension A relation can be known in two ways. Its [[https://en.wikipedia.org/wiki/Extensional_and_intensional_definitions][extension]] is the set of tuples it holds, and a tuple belongs to it if it is among them. Its intension is the predicate those tuples satisfy, and a tuple belongs to it if the predicate says so. A finite relation can be answered from either. A relation of [[https://en.wikipedia.org/wiki/Aleph_number][countably infinite]] cardinality can only be answered from its intension, since enumerating it never ends. A reader that waits for the end of an endless relation hangs, so RNT has to know before reading whether a read ends, and whether a relation can decide membership at all. Modes are how a relation says so. A mode states what a relation can answer under a given binding of its attributes, and says nothing of whether the answer comes from the extension or the intension. The idea comes from logic languages such as Mercury, where a predicate declares its [[https://mercurylang.org/information/doc-latest/mercury_ref/Modes.html][modes]], which arguments must be bound for a call, and its [[https://mercurylang.org/information/doc-latest/mercury_ref/Determinism.html][determinism]], how many solutions such a call has. * A mode [[file:../lib/concepts/Mode.mli][Mode]] describes one with two fields. #+begin_src ocaml type mode = {bound: attributes; yields: Cardinality.t} #+end_src Given values for the attributes in =bound=, the relation produces every tuple that agrees with them, and there are at most =yields= of them. [[file:../lib/concepts/Cardinality.mli][Cardinality]] has four classes, =Empty=, =Bounded n=, =Finite= and =Countable=. Every class but =Countable= is exhaustible, meaning that enumeration ends. A relation declares its modes through the [[file:../lib/protocols/Relation.mli][Relation]] protocol. #+begin_src ocaml method modes : (Concepts.Mode.t, Concepts.Condition.condition) result #+end_src * Generation under a binding A mode declared for =B= also serves any binding that includes =B=. The relation produces the tuples that agree with =B= and drops those that disagree with the extra values, so it produces no more than before. =Mode.generation modes bound= is therefore the tightest =yields= among the modes whose =bound= is a subset of the binding. It is =None= when no mode applies, and then the relation cannot be asked under that binding at all. This differs from =Countable=, where the relation can be asked but its answer never ends. =Mode.exhaustible= tells whether the generation ends. * Membership Deciding whether a tuple belongs to a relation means asking the relation with every attribute bound. A relation is a set, so at most one tuple agrees with a full binding, and a mode over every attribute yields =Bounded 1=. That mode is a direct test, an intension. A relation without one can still decide by producing the tuples under a smaller binding and comparing each, provided that production ends, which is deciding by extension. In principle, then, a relation decides membership exactly when it is exhaustible with every attribute bound, and extension and intension are the same question asked under different bindings. * Reachable bindings The principle above is wider than what RNT can do today. The [[file:../lib/protocols/Relation.mli][Relation]] and [[file:../lib/protocols/Enumerable.mli][Enumerable]] protocols reach exactly two bindings. - =enumerate= produces tuples with nothing bound, so it realizes the modes whose =bound= is empty. - =contains= answers with every attribute bound, so it realizes the modes whose =bound= is every attribute. 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. An ephemeral relation takes an optional membership test from whoever builds it, through =EphemeralRelation.instantiate ?decide=. - With a test, =contains= uses it. - Without one, =contains= enumerates the relation and compares, but only when =Mode.exhaustible modes ∅= holds, meaning its generation with nothing bound ends. - Otherwise it fails with =undecidable-membership= and does not enumerate. This is the case when that generation is =Countable=, or when no mode has an empty =bound=. A relation that declares ={all; Bounded 1}= promises a direct test, so whoever builds it must give it one. Nothing checks that promise yet. The evaluator protocol has no membership method. An ephemeral relation generated by a program answers =contains= the way it answers =modes=. It invokes the program, asks the relation the program returns, and releases it. That result is a relation the evaluator built, and the 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, 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}=. An ephemeral relation generated by a [[file:../lib/kernel/Program.ml][program]] knows its modes only from the relation the program returns, so asking for them invokes the program and asks the result. Invoking is lazy. An [[file:evaluators.org][evaluator]] builds the result without reading tuples, and FOL reads tuples only when the result is enumerated. A program with no state to run within fails with =unbound-program=, just as reading its relation would. A relation that declares no modes cannot be asked under any binding. * Modes of a FOL plan [[file:../lib/evaluators/FOL.ml][FOL]] computes the modes of a plan alongside its heading, before it 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 =a= that =b= binds, has the modes of =r= with =a= taken out of each =bound=, by =Mode.given=. The binding supplies its value, and the index produces the tuples, so ={a; Finite}= becomes ={∅; Finite}=. The other attributes of =b= only filter what the index produces, so they stay bound. - 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. 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 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. 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 needs the end. Asking such a projection whether it holds a tuple fails with =undecidable-membership=. * Indexes A substantial relation keeps an index on each attribute =a=, a tree keyed by the hash of the 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 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. Admission asks a denial for its modes first and refuses one that does not end. =Relation.read= does not check them yet.