#+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.
