Extension and intension

A relation can be known in two ways. Its 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 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 modes, which arguments must be bound for a call, and its determinism, how many solutions such a call has.

A mode

Mode describes one with two fields.

type mode = {bound: attributes; yields: Cardinality.t}

Given values for the attributes in bound, the relation produces every tuple that agrees with them, and there are at most yields of them. 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 Relation protocol.

method modes : (Concepts.Mode.t, Concepts.Condition.condition) result

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 Relation and 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.

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 need.

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. It declares {∅; Finite} for enumerating that set, and {all; Bounded 1} for the lookup by hash, which needs every attribute to compute the hash.

An ephemeral relation that EphemeralRelation.literal builds from n tuples declares {∅; Bounded n}.

An ephemeral relation generated by a 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 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

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.

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.

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}.

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.

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

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 explains. Without the operation, the mode an index adds would be declared and never used.

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 denial that holds a tuple, so both hang on a Countable relation. Neither checks modes yet. Denials will check them once they are reworked.