QuabeC

Peter Seymour

2 March 2009

Last Updated: 15 July 2009

1 Introduction

QuabeC stands for Querying and updating a ⇝ b edges with Constraints where a ⇝ b refers to a general asymmetric 2-place relation: there is an edge from a to b.

The system provides a multi-versioned external storage mechanism. The underlying data structure is intentionally simple but more complicated structures can be built on top of it yielding a rich modelling platform.

2 Data Structure

Data is stored as sequences of graphs each consisting of directed edges over an infinitely countable set of nodes called atoms referred to by 𝔸. Atoms are either named by an arbitrary length string over a fixed alphabet or are anonymous. There is a bijection between the set of all strings and the named atoms so that where an atom has a name it is unique amongst all the other names. Similarly there is a bijection between the anonymous atoms and the natural numbers. These two mappings induce a total order by placing anonymous atoms in order before the named atoms taken in lexicographic order. Each data graph is a model for a first-order language where the atoms are the domain and the edges define a relation. It is helpful to consider a concrete model of each graph as a subset of all the edges, written G ⊆ 𝔸 × 𝔸. Then in terms of the language:

G ⊨ a ⇝ b ⇔ (a, b) ∈ G

It is important to note that it is the graph edges which define the state since the nodes are universally fixed across all graphs. A sequence of graphs represents an enumeration of its versions. Multiple sequences can be used to permit distinct datasets and branching. These will be written as ∅, G_{1}, G_{2}, . . .. Where ∅ denotes the empty graph from which all other graphs will evolve.

3 Query Languange

To describe this structure is an accompanying predicate calculus ℒ_{Q} which allows queries over the data structure. A query is a well-formed formula whose result depends on the number of free variables present. If there are no free variables in the query (a closed formula) then it is either true or false. If there is one free variable then the result is the set containing all atoms which satisfy the formula. Where there are two or more free variables the result is a set of tuples. The free variables in a formula are ordered so it is always possible to define such tuples.

3.1 Well-formed Formulæ

The alphabet of symbols is as follow:

x, x_{1}, x_{2}, …; a, a_{1}, a_{2}, …; ˆ1, ˆ2, …; …  variables
“a”, “ab”, …  constants
=, <, @^{e}, Λ_{a_{1}}^{e}, Λ_{a_{2}}^{e}, …; ϕ^{e}, ϕ_{1}^{e}, ϕ_{2}^{e}, …; φ^{e}, φ_{1}^{e}, φ_{2}^{e}, …; …  predicates
(,), ,  punctuation
¬, ∧  connectives
∀  quantifier

Well formed formulæ (abrreviated to wff ) are built-up from atomic formulæ using the connectives. Variables range over the atoms and occur in a wff either bound or free. Bound variables must fall under the scope of a quantifier. The free variables are labelled by n̂ to simplify binding rules. The constants denote specific named atoms.

3.1.1 Construction

A term is defined by:

1. A variable is a term.

2. A constant is a term.

An atomic formula is defined by:

1. If ϕ^{e} is a predicate and t_{1}, …, t_{e} are terms then ϕ^{e}(t_{1}, …, t_{e}) is an atomic formula.

2. If x and y are terms then x = y is an atomic formula.

3. If x and y are terms then x < y is an atomic formula.

4. If p and t_{1}, …, t_{e} are terms then @^{e}(p, t_{1}, …, t_{e}) is an atomic formula.

A wff is defined by:

1. All atomic forumulæ are wff s.

2. If 𝒜 and ℬ are wff s then (¬𝒜),(𝒜 ∧ ℬ) and (∀x)𝒜 are wff s where x is any variable.

3. The set of wff s is generated from the above.

3.1.2 Custom Predicates

A wff can be considered as a predicate taking as many arguments as it has distinct free variables. If a wff has no free variables then it is closed. The superscript e on a predicate letter denotes the number of arguments that the predicate accepts. This can be thought of as the type of the predicate or as we shall see later the type of a set-abstract. For example:

ϕ^{2} = (ˆ1 ⇝ ˆ2) ∧ (ˆ1 ⇝ “quabec”)

The free variables can be bound by application as in:

ϕ(x, y) = (x ⇝ y) ∧ (x ⇝ “quabec”)

3.1.3 Atom Ordering

The pre-defined 2-place predicate < orders the atoms such that anonymous atoms appear before named atoms and named atoms appear in lexicographic order. Anonymous atoms are unordered in ℒ_{Q} even though the model provides a total order. The equality predicate = behaves as expected.

3.1.4 Interpreter

The interpreter predicate @^{e} for e ≥ 0 interprets the name of its first argument as a wff with the remaining e arguments (if any) bound to the free variables. This is always false for anonymous atoms, named atoms that do not denote a wff or misapplication of arguments.

3.2 Simulataneous Satisfaction

For each atom F there is a predicate Λ_{F}^{e} which uses F to define a range of atoms to be simultaneously interpreted. If F is a named atom whose name denotes a wff of exactly one free variable then Λ_{F}^{e} is evaluated as

Λ_{F (p)}^{e}(x^{e}) = (∀p)(F (p) → @^{e}(p, x^{e}))

Should F not be of the specified form the predicate is false.

3.2.1 Truth

Any closed wff consitutes a truth statement since it can be evaluated as true or false for any given model G.

G ⊨ ϕ

3.2.2 Set Abstraction

Reference to a subset of the atoms is achieved using a non-closed wff. Each combination of atoms satisfying the predicate forms a tuple. The full set of these tuples is the set-abstract.

S_{ϕ^{e}} = {x^{e}|ϕ^{e}(x^{e})}

Where x^{e} is either a tuple of e elements or a single variable if e = 1. These set-abstracts are unordered in ℒ_{Q} but are ordered in the model.

3.3 Syntactic Extensions

The following set of definitions are syntactic and allow a more natural construction of wff. The use of the superscript e allows predicates and the set-abstracts they define to have a definite type. Certain pieces of syntax rely on types matching so variables can also be typed to make this explicit. This typing of variables is not part of the syntax so x^{1} should be read as x and x^{e} as (x_{1}, …, x_{e}). Where types are obvious they will be omitted.

To ease clarity predicates can be defined outside of any wff. When they are used in a wff they would be applied by substitution with all free variables replaced by bound terms. For instance:

ϕ = ¬(ˆ1 < ˆ2)
ϕ(“a”, ˆ1)

When defining a predicate the use of the enumerated free variables can be replaced by an explicit argument list. Similarly the result of the query is the set of all atom tuples satisfying the final wff. The above exmple can be re-written as:

pred ϕ(x, y) = ¬(x < y)
{x|ϕ(“a”, x)}

Variables can similarly be declared for simple substitution in the resulting wff.

var t = “a”
pred ϕ(x, y) = ¬(x < y)
{x|ϕ(t, x)}

Finally set-abstracts can be brought out.

var t = “a”
pred ϕ(x, y) = ¬(x < y)
set S = {x|ϕ(t, x)}
S

3.3.1 Definitions The following are to be taken as equivalent atomic formulæ:

\begin{matrix}x ≠ y ≡ & ¬(x = y) \\ x > y ≡ & y < x \\ x ≤ y ≡ & ¬(y < x) \\ x ≥ y ≡ & ¬(x < y) \\ x ∼ y ≡ & ¬(y < x) ∧ ¬(x < y) \\ x^{e} = y^{e} ≡ & (x_{1} = y_{1}) ∧ … \\ x^{e} ≠ y^{e} ≡ & (x_{1} ≠ y_{1}) ∨ … \\ x^{e} < y^{e} ≡ & (x_{1} < y_{1}) ∨ ((x_{1} = y_{1}) ∧ ((x_{2} < y_{2}) ∨ …) ) \\ ϕ^{e}(x^{e}) ≡ & ϕ^{e}(x_{1}, …, x_{e}) \\ ⊤ ≡ & “0” < “1” \\ ⊥ ≡ & ¬⊤ \\ @p(x^{e}) ≡ & @(p, x_{1}, …, x_{e}) \end{matrix}

The following are to be taken as equivalent wff s:

\begin{matrix}𝒜 ∨ ℬ ≡ & ¬(¬𝒜 ∧ ¬ℬ) \\ 𝒜 → ℬ ≡ & ¬𝒜 ∨ ℬ \\ 𝒜 ← ℬ ≡ & ℬ → 𝒜 \\ 𝒜 ↔ ℬ ≡ & (𝒜 → ℬ) ∧ (𝒜 ← ℬ) \\ (∃x)𝒜 ≡ & ¬(∀x)¬𝒜 \\ (∀x^{e})𝒜 ≡ & (∀x_{1}) … (∀x_{e})𝒜 \\ (∃x^{e})𝒜 ≡ & (∃x_{1}) … (∃x_{e})𝒜 \end{matrix}

The following are wff s defined by set-abstracts:

\begin{matrix}S_{ϕ^{e}} ≡ & \{x^{e}|ϕ(x^{e})\} \\ x^{e} ∈ S_{ϕ^{e}} ≡ & ϕ^{e}(x^{e}) \\ x^{e} ∉ S_{ϕ^{e}} ≡ & ¬ϕ^{e}(x^{e}) \\ S_{ϕ^{e}} ⊆ S_{φ^{e}} ≡ & (∀x^{e})(ϕ^{e} → φ^{e}) \\ S_{ϕ^{e}} ⊇ S_{φ^{e}} ≡ & (∀x^{e})(ϕ^{e} ← φ^{e}) \\ S_{ϕ^{e}} = S_{φ^{e}} ≡ & (∀x^{e})(ϕ^{e} ↔ φ^{e}) \\ S_{ϕ^{e}} ∩ S_{φ^{e}} ≡ & \{x^{e}|ϕ^{e} ∧ φ^{e}\} \\ S_{ϕ^{e}} ∪ S_{φ^{e}} ≡ & \{x^{e}|ϕ^{e} ∨ φ^{e}\} \\ S_{ϕ^{e}} \ S_{φ^{e}} ≡ & \{x^{e}|ϕ^{e} ∧ ¬φ^{e}\} \\ ∅^{e} ≡ & \{x^{e}|⊥\} \\ 𝔸^{e} ≡ & \{x^{e}|⊤\} \\ \{a^{e}\} ≡ & \{x^{e}|x^{e} = a^{e}\} \\ \{a^{e}, b^{e}, …\} ≡ & \{x^{e}|x^{e} = a^{e} ∨ x^{e} = b^{e} ∨ …\} \end{matrix}

3.3.2 Reusable Queries

Consider a predicate that determines whether an atom is anonymous, x < “”.

var isanon = “ˆ1 < “””
set S = {x|@isanon(x)}
S

This works precisely because the atoms are immutable so the reference in the var clause can hold across queries.

Alternatively useful queries can be stored as part of the data structure, “isanon” ⇝ “ˆ1 < “””. Traditional databases offer views which can also be replicated by applying @ to an atom representing a set-abstract. The @ predicate acts as a very powerful interpreter of the query language.

In fact it can be argued that it is too powerful since it can effectively build uncomputable sets. This is the motivation for introducing simultaneous satisfaction as a weaker replacement. Any predicate determining formulæ to be interpreted will either generate a finite or infinte set. In the first case each case can be checked whereas in the latter the satisfaction must fail since there will always be one failing formula. If there were not a failing formula we would have computed an infinte set of valid formulæ in a single wff which cannot be the case.

4 Higher Order Relations

Since having only a 2-place relation is too restrictive for many uses we propose here a general n-place relation as a further extension. Given a and b such that a ⇝ b we write r : ⟨a b⟩ ≡ a ⇝ r ∧r ⇝ b and ⟨a b⟩ ≡ (∃r)r : ⟨a b⟩ for some atom r. The intention is to let r be anonymous and represent the relation between a and b so it can in turn be used within other relations. Taking this relation as a base we can specify high order relations as follows:

r_{n} : … r_{1} : ⟨a_{n} … a_{1}⟩ ≡ r_{n} : ⟨a_{n} r_{n−1}⟩ ∧ r_{n−1} : … r_{1} : ⟨a_{n−1} … a_{1}⟩
r_{n−1} : … r_{1} : ⟨a_{n} … a_{1}⟩ ≡ (∃r_{n})r_{n} : … r_{1} : ⟨a_{n} … a_{1}⟩
…
⟨a_{n} … a_{1}⟩ ≡ (∃r_{n}) … (∃r_{1})r_{n} : … r_{1} : ⟨a_{n} … a_{1}⟩

As a further extension whenever we see such a relation used in a position where an atom would be expected as in ϕ(r) then we write:

ϕ(⟨a b⟩) ≡ (∃r)r : ⟨a b⟩ ∧ ϕ(r)

Analogous forms apply for nested structures.

One way to view this structure is as special form of tree over the atoms where fresh anonymous atoms are introduced at the nodes and the root node is the representative. Any tree structure can be modelled since there is no problem with nesting these n-place relations. As an example ⟨⟨a b⟩ ⟨c d⟩⟩ is perfectly legal.

a b c d The special syntax ⟨a b …⟩ represents a degenerate tree called a list.

a b

5 Natural Form

Putting together all the pieces allows for a very natural data form. Each concept in the logical model should have an associated atom. Sometimes it makes sense to name the concept but in other cases a concept is more sensibly referenced by its position in the topology.

The concept of “mass” for instance can easily be named but an instance of a more general concept for example a particular person may not have a unique name. In the latter case an anonymous atom represents the concept and its relations define it uniquely by imbuing it with properties such as age etc. This doesn’t mean there is no concept of identity rather there is no named reference to it.

We can represent a class as an atom and have the concept of class membership as another. So we could use an atom “in” for membership and another for the class as in “People”. Then for x to be a person the following must hold:

⟨x “in” “P eople”⟩

The membership concept is resuable as in ⟨x “in” “Cats”⟩ We can enquire about all people using a set abstract {x|⟨x “in” “P eople”⟩}. People can have properties such as age ⟨x “hasage” “30”⟩. It might be necessary to find all people under a certain age. This can be accomplished by establishing a numeric type within the current structure. If it is to be used in comparisons then it must obey <. This does not naturally occur but [1] gives a series of numeric types and composite types that will obey <. In which case assume \overline{30} is in such a form then all young people is given by:

\{(x, n)|⟨x “in” “P eople”⟩ ∧ ⟨x “hasage” n⟩ ∧ n < \overline{30}\}

It’s worth noting that if ⟨a b c⟩ and ⟨a b⟩ hold then {x|⟨a x⟩} = {⟨b c⟩, b}. This logically makes sense when viewed as predicates on a but might not be intended. One way to differentiate is to see that ⟨b c⟩ is anonymous whereas b is possibly not.

6 Update Language

The query language views the data structure as static and produces no side effects. This is desirable especially when the @ predicate can mimic dynamic behaviour. However, at some point data needs to be created and changed. This is achieved using a simple update language. Since there are only atoms and edges it is relatively simple. If a concept is logically mutable it should be an atom in its own right referencing its state. For example moving from ⟨a “hasprop” b_{1}⟩ to ⟨a “hasprop” b_{2}⟩.

An update works on edges by specifying what should hold after the update has been made irrespective of what held before. This is accomplished in a similar manner to set abstraction except the selection is over relations not atoms. To produce an edge between two atoms we use the following primitive edge set statement.

[a ⇝ b|⊤]

Similarly to remove a relation [¬a ⇝ b|⊤]. As a language extension [ϕ|⊤] can be written as [ϕ]. The statement on the right-hand side is any wff from ℒ_{Q}. The statement on the left-hand side is composed of atoms, ∧, ¬, edge sets and anonymous-selection. Any of the extensions to ℒ_{Q} that use these components may also be considered valid. The interpretation of ∧ is that both statements to its left and right will be satisfied after the update.

The result of an update is an edge set containing edges that should be present after the update and those that should not. This could be in conflict e.g. [a ⇝ b ∧ ¬a ⇝ b]. In this instance the update fails and no change will be observed. An update statement will not directly change the underlying data model but forms the first of two distinct phases. The first determines the edge set on a static view of the data whereas the second enforces this edge set by producing a change set which will remove existing edges and create edges that don’t already exist.

Consider [¬(a ⇝ b ∧ b ⇝ a)]. Without the negation this is only satisfied by adding the two relations. In its negative sense either or both relation could be removed and the statement will hold after the update. Since making a choice would introduce indeterminism into the update language both are chosen. Therefore it simply reverses the satisfaction of each component, ¬a ⇝ b ∧ ¬b ⇝ a. Notice that this implies the former and is fully determined. We can now interpret p ∨ q as ¬(¬p ∧ ¬q) which conforms to its use in the query language. An unfortunate consequence is that certain logically correct updates will not be deterministic and hence not permitted.

[a ⇝ b ∨ ¬a ⇝ b]

Anonymous-selection is a powerful technique to add relations in a declarative way. All anonymous atoms can only be referenced through a query that looks into the atom’s local topology. To introduce such an atom requires constructing that topology on a fresh atom. An anonymous selection takes the form of a qunatifier (+r)ϕ where ϕ is any valid left-hand side statement. It is to be interpreted that an anonymous atom r will be selected such that it satisfies ¬(∃t)(r ⇝ t ∨ t ⇝ r) before the update and is distinct from all other such selections. It can be considered a fresh atom and since the anonymous atoms are well-ordered this selection process can always be made.

We now look at two standard uses for the quantifier. This is best seen using an example shown as a graph. Initially there will be two atoms a and b with no edges between them.

a b The first update associates to each of them a new anonymous atom of their own.

[(+r)(r ⇝ x)|x ∈ {a, b}]

a b The second update associates to each of them a new anonymous atom shared between them.

[(+r)[r ⇝ x|x ∈ {a, b}]]

a b Further applications cause more new atoms to be associated.

a b a b To produce idempotent updates the right-hand side of the edge set can be used to query for the desired relation.

[(+r)(r ⇝ a)|¬(∃t)(t ⇝ a)]

To generalise this we extend the syntax with a new quantifier (∗r) such that the following equivalences hold:

[(∗r)ϕ(r)|φ] ≡ [(+r)ϕ(r)|φ ∧ ¬(∃t)ϕ(t)]
(∗r)[ϕ(r)|φ] ≡ (+r)[ϕ(r)|φ ∧ ¬(∃t)ϕ(t)]

This all leads up to some tidy definitions concerning the higher-order relations. Suppose we wish to assert ⟨a b⟩ and ⟨a b c⟩ respectively then the following updates achieve them:

[(∗r)(r : ⟨a b⟩)] ≡ [(∗r)(a ⇝ r ∧ r ⇝ b)]

[(∗r_{1})(∗r_{2})(r_{1} : r_{2} : ⟨a b c⟩)] ≡ [(∗r_{1})(∗r_{2})(a ⇝ r_{1} ∧ r_{1} ⇝ r_{2} ∧ b ⇝ r_{2} ∧ r_{2} ⇝ c)]

This can be more consisely written if we are not interested in using some of the new atoms representing the relations.

[∗⟨a b⟩] ≡ [(∗r)(r : ⟨a b⟩)]
[∗⟨a b c⟩] ≡ [(∗r_{1})(∗r_{2})(r_{1} : r_{2} : ⟨a b c⟩)]

7 Graph Evolution

This sections looks at how a graph evolves when updates are applied. All queries are against a specific version of a specific graph. We begin by considering each step along a graph sequence. Then we can can build from here to look at the relationship between sequences and applying updates concurrently.

7.1 Physical Change Sets

The state of the model at any sequence point t is simply the set G_{t} of edges that exist between atom pairs. An update takes the form (U_{t}^{+}, U_{t}^{−}), where an edge in U_{t}^{+} is to exist after an update, an edge U_{t}^{−} is to not exist and all the rest are to remain unaltered. A change set on the other hand determines how G_{t+1} is to be constructed from G_{t} by toggling the membership for certain edges. We therefore represent a change set as Δ_{t} ⊆ 𝔸^{2} such that:

Δ_{t} = (U_{t}^{+} ∩ \overline{G_{t}}) ∪ (U_{t}^{−} ∩ G_{t})

See appendix A for notation. The following then holds:

G_{t+1} = (G_{t} ∪ Δ_{t}) \ (G_{t} ∩ Δ_{t}) = G_{t} ⊕ Δ_{t}

The properties of the change set operator ⊕ are also detailed in appendix A.

A sequence of change sets Δ_{0} … Δ_{t−1} fully determines G_{t} by induction if it is assumed that G_{0} = ∅. Therefore:

G_{t} = ⨁_{0≤i<t} Δ_{i}

These are referred to as the physical change sets because they take a graph through its successive versions one at a time building on the previous. Since they fully determine G_{t} we can view each graph sequence as its sequence of change sets ⟨Δ_{0}, …, Δ_{t}, …⟩.

7.2 Branching

All graphs grow from a common root ∅ but they can also branch at later points. Consider ⟨Δ_{0}^{A}, Δ_{1}^{A}, …⟩ and ⟨Δ_{0}^{A}, Δ_{1}^{B}, …⟩ as change sets for graph sequences of ⟨A_{i}⟩ and ⟨B_{i}⟩ respectively. As shown in the diagram the graph sequence ⟨B_{i}⟩ inherits its first change from ⟨A_{i}⟩ (it branches from A at version 1).

\begin{matrix}∅ \\ A_{1} \\ A_{2} \\ B_{2} \end{matrix}

We can say Δ_{0}^{B} = Δ_{0}^{A} and more generally if B branches from A at t then Δ_{i}^{B} = Δ_{i}^{A} ∀i < t. To express this branching directly we write:

A_{0} = ∅ [branch point]
A_{1} = A_{0} ⊕ Δ_{0}^{A}
A_{2} = A_{1} ⊕ Δ_{1}^{A}

B_{0} = A_{0}
B_{1} = A_{1} [branch point]
B_{2} = B_{1} ⊕ Δ_{1}^{B}

Since ∅ is a common root for all graphs we can talk about the graph tree which considers all branches (graph sequences) as part of a single structure.

7.3 Merging

Given a graph G_{t} consider Δ_{t}^{A} and Δ_{t}^{B} which are physical change sets applied to G_{t} to form two branches A_{t+1} and B_{t+1}. Under what circumstances can these branches be merged to produce G_{t+1}? It is desirable that the results of changes occurring to G_{t} by Δ_{t}^{A} and Δ_{t}^{B} be jointly preserved in G_{t+1}. Without loss of generality we apply Δ_{t}^{A} first and then ensure that those edges which will be changed by Δ_{t}^{B} have not already been altered by Δ_{t}^{A}. This is expressed as follows using the change set restriction operator G ↾_{X}= (G ∩ X, \overline{G} ∩ X):

(G_{t} ⊕ Δ_{t}^{A}) ↾_{Δ_{t}^{B}}= G_{t} ↾_{Δ_{t}^{B}}

This necessitates two conditions

(G_{t} ⊕ Δ_{t}^{A}) ∩ Δ_{t}^{B} = G_{t} ∩ Δ_{t}^{B}  (by definition)
(G_{t} ∩ Δ_{t}^{B}) ⊕ (Δ_{t}^{A} ∩ Δ_{t}^{B}) = G_{t} ∩ Δ_{t}^{B}  (by (Δ5))
Δ_{t}^{A} ∩ Δ_{t}^{B} = ∅  (apply ⊕(G_{t} ∩ Δ_{t}^{B}))

and

\overline{(G_{t} ⊕ Δ_{t}^{A})} ∩ Δ_{t}^{B} = \overline{G_{t}} ∩ Δ_{t}^{B}  (by definition)
(\overline{G_{t}} ⊕ Δ_{t}^{A}) ∩ Δ_{t}^{B} = \overline{G_{t}} ∩ Δ_{t}^{B}  (by (Δ2))
(\overline{G_{t}} ⊕ Δ_{t}^{B}) ∩ (Δ_{t}^{A} ∩ Δ_{t}^{B}) = \overline{G_{t}} ∩ Δ_{t}^{B}  (by (Δ5))
Δ_{t}^{A} ∩ Δ_{t}^{B} = ∅  (apply ⊕(G_{t} ∩ Δ_{t}^{B}))

So we can proceed to define a change set merge operator ⊎ such that:

X ⊎ Y = X ⊕ Y where X ∩ Y = ∅

otherwise a conflict occurs and no merging can proceed.

As an example consider a graph with a two edges “a” ⇝ “1” and “b” ⇝ “1”. Then the change sets {(“a”, “1”), (“a”, “2”)} and {(“b”, “1”), (“b”, “2”)} can be merged without conflict and increment the two counters. However, the change sets {(“a”, “1”), (“a”, “2”)} and {(“a”, “2”), (“a”, “3”)} can be applied in sequence but would cause a merge conflict.

It should be noted that even if a merge conflict doesn’t arise that consistency could still be violated since the edges involved in the query part of the update are not checked for conflict. This would occur if one update relies on reading (but not changing) an edge that is then changed by another change set. These two change sets could still be merged but certain properties that exist after each taken in isolation may not be preserved. So it can be said that the merge operator handles write conflicts but not read conflicts. Indeed this is true of all the change set operators, they handle the physical aspects of the graph tree evolution. Any logical aspects should be enforced by constraints which are discussed later.

7.4 Logical Change Sets

From the building blocks of physical changes sets we can look at logical change sets which consist of one or more phyiscal changes sets rolled up. For instance:

δ_{t,t+k} = Δ_{t} ⊕ … ⊕ Δ_{t+k−1}

These can be treated just like physical change sets with regard to merging and branching. Notice that changes can occur during a logical change set that would normally conflict in merging but so long as these changes are later reversed within that logical change set no conflict will occur.

The generalised merge rule is:

G_{t+1} = G_{t} ⊕ (δ_{t,t+k_{1}}^{1} ⊎ … ⊎ δ_{t,t+k_{n}}^{n})

Despite each branch moving multiple versions, the merged branch is only advanced once since only one change set is applied to it.

7.5 Grafting

So far merging of branches has been shown to be possible where a common branch point is identified. However, it may be the case that a section of a graph sequence represented as a logical change set needs to be applied to another branch where no common root can be established at the point of the change set. Since change sets are not idempotent it is necessary to carry over some of the original graph structure to ensure the change set is correctly applied. Consider two graph branches G_{r} and H_{s} where a common root only exists strictly before min(r, s) (remembering that all branches have ∅ as a common root). Then δ_{s,s+k}^{H} can be applied to G_{r} only if the following condition holds:

G_{r} ↾_{δ_{s,s+k}^{H}}= H_{s} ↾_{δ_{s,s+k}^{H}}

This ensures the change set is applied under the same conditions on both branches. It trivially holds where r = s and the branching is coming from a common root so merging is a special case. Since δ_{s,s+k}^{H} is recoverable from H_{s} ↾_{δ_{s,s+k}^{H}} (see appendix A) only the latter is necessary for the definition of the graft. We can write a change set grafting operator G_{r} ↖ X as follows:

G_{r} ↖ H_{s} ↾_{δ_{s,s+k}^{H}}= G_{r} ⊕ δ_{s,s+k}^{H} where G_{r} ↾_{δ_{s,s+k}^{H}}= H_{s} ↾_{δ_{s,s+k}^{H}}

7.6 Undo

This simple case is handled by reapplying the last change set to undo its effects. In symbols this amounts to G ⊕ X ⊕ X = G.

8 Serialisation Strategies

The previous section covered all the necessary algebra to extensively handle branching, merging and grafting in a very general manner. However, at no point was there any consideration for the overall evolution of the graph tree in real time. This would be the case for any realisation of QuabeC as a database system.

The abstraction we use in this section is that of a sequence of requests arriving at the graph tree. Simultaneous requests are arbitrarily ordered to simplify the model. We write G_{r}^{read} and G_{w}^{write} as the read node and write node respectively for a request. For a query request there is simply the read node and a query formula. There is no issue of conflict with multiple query requests so long as their read nodes exist.

An update request requires a query request and a write node to apply the resulting change set to. This write node must be a leaf in the graph tree so it can be immediately applied. Given that grafting is possible the read node and write node are independent so long as the grafting conditions hold.

The next stage is to develop an algorithm for determining the read and write nodes for incoming requests. It is not feasible for a requesting system to know precisely which nodes it needs since it may require the ‘latest’ or ‘next’ node on a given branch. We label each branch with a simple name where there are as many branches as there are leaf nodes. This means that non-leaf nodes are not uniquely named since each branch name labels all nodes from the leaf to the root. The algorithm works with a triple of data (G^{read}, k, G^{write}).

(G^{read}, k, G^{write}) → \{ \begin{matrix}(G_{k}^{read}, G_{w}^{write}) & 0 < k ≤ r \\ (G_{r}^{read}, G_{w}^{write}) & k = 0 \\ (G_{w+k}^{read}, G_{w}^{write}) & −w ≤ k < 0 \\ failure & otherwise \end{matrix}

Where w is the next available write sequence number on G^{write} and r is largest sequence number on G^{read}. If G^{write} does not exist it is created as a new branch such that G_{r}^{write} = G_{r}^{read} and w = r + 1. If updates are handled serially then w = r + 1 but introducing the notion that updates can be occuring concurrently allows for a wider variety of interpretations. For instance (G, −1, G) is a serial update on G that waits for all current updates to finish (G_{w−1}^{read} may not yet exist although it will be scheduled for creation). A nonwaiting update would take the form (G, 0, G) and a simple branch (G, 0, G′) where G′ does not exist. If G′ ≠ G exists then the last update would be a graft.

The algorithm is both lock-free and wait-free since a natural order is assigned to each update and no update can prevent another finishing for any more than a finite period. This is a direct consequence of updates being of finite duration.

8.1 Long Transactions

Long transactions can be implemented in a non-blocking way by breaking them into smaller updates. Each part would specify the same fixed read node and rely on merging to detect write conflicts.

A greater degree of security can be obtained by implementing a locking or versioning mechanism within the graph structure. The simplest example is a counter. By ensuring that the long transaction is the sole incrementer of a given counter it can be sure of its own consistency. However, in the face of failure it would have to implement its own rollback procedure. This may not always be possible but is an essential problem whose only alternative is to lock some section of the graph at the risk it is never released. Note that this strategy can also be enforced so long as all updates go through a single coordinator which is a suggested strategy for using QuabeC. See section 11 for more details.

9 An Alternative Representation

The underlying graph is potentially countably infinite. Consider [r ⇝ “x”], this will associate each atom with “x” creating one edge per atom. However, viewed another way the graph structure is always determined by a finite number of finite update formulæ. So there is at least one finite representation of any potential graph, namely, the sequence of updates creating it.

We now look at how to construct queries and updates as solutions to satisfaction problems. To simplify this construction we associate each atom with an element of ℤ such that the anonymous atoms are all negative and each named atom retains its lexicographic order under the usual integer order. This means “” becomes 0 and to disambiguate the old ordering we write <_{𝔸}. This forces an order on the anonymous atoms which simplifies the following constructions. In this simpler model a graph is a subset of ℤ × ℤ.

9.1 Queries

A query is an expression of the form {(x_{1}, …, x_{n})|ϕ} where ϕ has n free variables. If ϕ has m quantifiers then its bound variables are x_{n+1}, …, x_{n+m} all distinct from each other.

9.1.1 Reduction We first recursively re-write ϕ according to the following rules to bring it into prenex disjunctive normal form.

• Reduce ϕ to its canonical form by removing all uses of extensions.

• Replace each occurrence of ¬(∀x_{i})(ϕ) with (∃x_{i})(¬ϕ).

• Replace each occurrence of ¬(∃x_{i})(ϕ) with (∀x_{i})(¬ϕ).

• Replace each occurrence of ¬¬ϕ with ϕ.

• Replace each occurrence of x <_{𝔸} y with x < y ∧ ¬(y < 0).

• Replace each occurrence of ¬(x = y) with (x < y) ∨ (y < x).

• Replace each occurrence of ¬(x < y) with (y < x) ∨ (x = y).

• Replace each occurrence of ¬(x ⇝ y) with x ⇝̸ y.

• Replace each occurrence of (ϕ ∨ φ) ∧ φ with (ϕ ∧ φ) ∨ (ϕ ∧ φ).

• Replace each occurrence of ¬(ϕ ∧ φ) with ¬ϕ ∨ ¬φ.

• Replace each occurrence of ¬(ϕ ∨ φ) with ¬ϕ ∧ ¬φ.

• Replace each occurrence of Λ_{F (p)}^{e}(x^{e}) depending on F:

– F is not a valid 1 place predicate, replace by ⊥.

– F is satisfied by an infinite set of atoms, replace by ⊥.

– F is satisfied by known p_{1}, …, p_{n}, replace by @p_{1}(x^{e})∧…∧@p_{n}(x^{e}). The resulting query takes the form:

{(x_{1}, …, x_{n})|(Q_{n+1} … Q_{n+m})(C_{1} ∨ … ∨ C_{r})}

Where each Q_{i} is either ∀ or ∃ and there are no occurrences of ¬. Each C_{i} is the conjuction of atomic formulæ of x_{i} or integer constants involving <,=,⇝ or ⇝̸ only.

In this first step we assume the query is over G_{0} = ∅ so a further reduction can be done such that all occurrences of x ⇝̸ y are removed and any C_{i} with an occurrence of x ⇝ y is completely removed. We now have a fixed model over ℤ × ℤ which will form the basis for arbitrary updates.

The next step involves building a graph for each conjunctive clause C as follows:

1. Create an equivalence class X = {x_{i}} for each x_{i}.

2. For each occurrence of x < y in C assign an edge from X containing x to Y containing y. (X and Y maybe the same).

3. For each occurrence of x = y combine X containing x to Y containing y to form a single class.

Call this graph R which may not be fully connected. If any class in R contains two differing constants or if R contains a cycle then C is false and can be removed entirely.

We now proceed to define lower and upper bounds lb and ub on each class X in R.

lb(X) = \{ \begin{matrix}κ − \frac{1}{2} & κ ∈ ℤ \\ min(\{lb(Y)|Y → X\}) \\ −∞ & otherwise \end{matrix}

ub(X) = \{ \begin{matrix}κ + \frac{1}{2} & κ ∈ ℤ \\ max(\{ub(Y)|X → Y \}) \\ ∞ & otherwise \end{matrix}

This is sufficient to generate all tuples of the inner expression as follows. The tuples satisfying each C_{i} are the cartesian product of all the sub-tuples generated by each connected subgraph. Variables occurring within any X are bounded in (lb(X), ub(X)). They are also constrained by variables in classes leading from and to that class as well as variables and constants in their own class. The total tuple set is the union of the tuples generated by each C_{i}.

For example the following generates tuples (x_{1}, x_{2}, x_{3}, x_{4}, 7) such that x_{1} < x_{2} and x_{3} = x_{4} < 7 along with (x_{1}, x_{2}, x_{3}, x_{4}, x_{5}) such that 0 < x_{1} < 5.

x1 x2 x3 x4 x5 7 0 x1 5

9.1.2 Quantification

Given the above graph construction we can see that within any conjuction term C a given variable x is bounded within a known interval. We aim to remove the innermost quantifier.

We proceed by forming sub-intervals {J_{j}} of ℤ for x by taking the end points of all intervals which bound x across all the graphs along with −∞ and ∞. Each interval I is then the union of some subset of the {J_{j}}. Suppose I = J_{1} ∪ J_{2} then:

ϕ = x ∈ I ∧ ϕ = (x ∈ J_{1} ∧ ϕ) ∨ (x ∈ J_{2} ∧ ϕ)

If for some J there is no I that contains it we include:

x ∈ J ∧ x < x

To keep the graph representation in accordance with this re-write new variants will need to be formed. For each graph find the class X containing x and produce variants for each J ⊆ I by including constant bounds. This requires adding {lb(J)} → X → {ub(J)}. Note that constants can appear in multiple equivalence classes without harm.

We handle the two sorts of quantifier differently.

Universal Quantification

Consider a simple case (∀x)((x ∈ J_{1} ∧ ϕ_{1}(x, y)) ∨ (x ∈ J_{2} ∧ ϕ_{2}(x, y))) such that {J_{1}, J_{2}} is a partition of ℤ. The aim is to generate all y that satisfy this formula. This is equivalent to the following chain of formulæ:

(∀x)((x ∈ J_{1} ∨ x ∈ J_{2}) ∧ (x ∈ J_{2} ∨ ϕ_{1})∧
(x ∈ J_{1} ∨ ϕ_{2}) ∧ (ϕ_{1} ∨ ϕ_{2})) expansion
(∀x)((x ∈ J_{2} ∨ ϕ_{1}) ∧ (x ∈ J_{1} ∨ ϕ_{2}) ∧ (ϕ_{1} ∨ ϕ_{2})) J_{1} ∪ J_{2} = ℤ
(∀x)((x ∈ J_{1} → ϕ_{1}(x, y)) ∧ (x ∈ J_{2} → ϕ_{2}(x, y)) ∧ (ϕ_{1} ∨ ϕ_{2})) ℤ \ J_{1} = J_{2}
(∀x)(x ∈ J_{1} → ϕ_{1}(x, y)) ∧ (∀x)(x ∈ J_{2} → ϕ_{2}(x, y)) implication

This result can be extended for more than two terms. To solve for y we look at the constraints on ϕ_{1} when x ∈ I_{1} simultaneously with the analogous case for ϕ_{2}.

For each J_{j} there will be one or more corresponding graph variants produced above. We consider each possible combination such that there is exactly one graph variant for each J_{j}. Universal quantification requires satisfaction across all of ℤ. For each combination the identity above is used to combine the graph variants and remove x. Then the disjunction of all combinations is taken as the result. Each graph is pre-processed in effect calculating (∀x)(x ∈ J → ϕ).

• Step 1 Find the class X containing x and ensure X = {x} (or if it contains a constant then J = {x}).

• Step 2 For each Y such that Y → X add Y → {lb(X)}.

• Step 3 For each Y such that X → Y add {ub(X)} → Y.

Across all variants merge all classes which share members and bring over all edges. Cycles and conflicts with distinct constants appearing in the same class are resolved by skipping the affected combination (there may be not valid combinations). Lower and upper bounds are now re-calculated and any empty intervals also result in the affected combination being skipped.

Existential Quantification

This situation is easier. Again consider a simple case (∃x)((x ∈ J_{1} ∧ ϕ_{1}(x, y)) ∨ (x ∈ J_{2} ∧ ϕ_{2}(x, y))) but this time J_{1} and J_{2} do not need to form a partition, they could even be equal. This is equivalent to:

(∃x)(x ∈ J_{1} ∧ ϕ_{1}(x, y)) ∨ (∃x)(x ∈ J_{2} ∧ ϕ_{2}(x, y))

Each graph is processed as follows but no new disjunction needs to be taken.

• Step 1 Find the class X containing x.

• Step 2 For each Y such that Y → X add Y → {ub(X)}.

• Step 3 For each Y such that X → Y add {lb(X)} → Y.

Cycles and conflicts can’t occur but empty intervals result in the graph being removed from the disjunction.

9.1.3 Resulting Structure

The final situation is a graph representation in the same form as before but with all references to x resolved. The method is repeated until all quantifiers are resolved arriving at a graph representation which can generate all tuples.

9.2 Updates

Take an update of the form [x ⇝ y|ϕ] this is calculated as a query {(x, y)|ϕ}. Similarly [¬x ⇝ y|ϕ] uses the same query. Any update [R_{1} ∧ R_{2}|ϕ] can use the union of queries for each component update. Updates are a restricted form of queries where only two variables occur. We can now study updates in this context. The graph representation used for queries reveals enough information to fully describe updates as queries over two variables x and y. Conjunctions are handled as the union of the resulting subsets of ℤ×ℤ. Anonymous selection is handled by preselecting a batch of atoms and re-writing the formulæ.

Any graph with only x, y and constants appearing can only take one of the forms described next.

9.2.1 Unrelated

Each of x and y appear in their own sub-graph. They can only have edges to and from classes containing a single constant and/or be in a class with a constant. If they appear in a class with a constant the constant can be removed and bounding classes used in place. If no bounds appear then dummy bounds of −∞ or ∞ can be introduced. The only form remaining is:

κx 1 x κx 2 κ{y \atop 1} y κ{y \atop 2}

9.2.2 Related

In the second case we have x and y related by atomic formulæ.

• x < ⋯ < y

• y < ⋯ < x

• x = y

The dots arise since quantified variables could have left empty classes on paths between x and y. Should constants appear on such paths then x and y are really unrelated and fall into the first case. Define an edge label k by:

k = \{ \begin{matrix}n & x < z_{1} < … < z_{n−1} < y \\ 0 & x = y \\ −n & y < z_{1} < … < z_{n−1} < x \end{matrix}

There will also be constant bounds as before. This results in the following graph:

κx 1 x κx 2 κ{y \atop 1} y κ{y \atop 2} k

9.3 G_{1}

Now updates over G_{0} = ∅ have been covered the form of G_{1} is the union of graphs or their complements following 2 simple forms. From each of these forms it is easy to reconstruct a wff that represents them. These wff s are the logical form of G_{1} that can be substitued into queries whenever x_{i} ⇝ x_{j} or x_{i} ⇝̸ x_{j} occurs. The preceeding method of handling queries then carries over to subsequent graph updates.

This alternative representation demonstrates how a graph tree can remain finite.

10 Constraint Atoms

The flexibility of the data model poses a risk that the structure will become unmanageable and hard to understand. To prevent this a series of constraints can be imposed which will define a data schema. A constraint is represented by a truth statement held as an atom’s name. Only one atom needs to be proposed since it can combine the results of other constraint atoms. Let c_{1}, …, c_{n} be atoms whose names are valid truth statements posing as constraints. Then choose C such that:

var C = “c_{1} ∧ … ∧ c_{n}”

The constraint atom C will be used as a check to ensure consistency is maintained. This method is simple but any constraint changes will require proposing a new constraint atom. By using a Λ_{F (p)} predicate this can be avoided. Suppose that for any constraint atom c the relation ⟨c “in” “Constraints”⟩ holds. Then C can be chosen such that:

var F = “⟨ˆ1 “in” “Constraints”⟩”
var C = “Λ_{F (c)}(c)”

Should any constraint atom not contain a valid statement then the constraint fails. This prevents invalid contraints being formed since any update that introduces an invalid constraint will be undone. A constraint atom is specified as part of any update. Where the constraint fails the update is not applied but the sequence number on the branch is still incremented so as not to break the serialisation algorithm.

11 High-Level Usage

As presented QuabeC should be considered as a physical backend for a rich database system. It provides all the mechanisms required for extremely complex data management and evolution that encompasses common functions of databases and version control systems simultaneously. However, it doesn’t provide certain features such as security, locking, mirroring, backup, etc that maybe desired. All of these features can be built on top of QuabeC and are discussed here.

Each graph tree is considered to be an individual “database” and would have a dedicated co-ordinator responsible for assigning permissions to updates and queries. The co-ordinator’s role is to act as a single point of interaction with the graph tree by client systems. As requests arrive they can be re-directed to storage engines that manage subsets of the nodes on the tree. In this way it is possible to parallelise the system and prevent bottlenecks. To mirror the tree is paramount to sending each update request to an alternative instance in the same order they are processed in the master system. The co-ordinator will be reponsible for bundling constraints with requests to any branch since there maybe security concerns at this level.

Archiving maybe appropriate and can be managed by the coordinator. Pruning the tree from the root maintains the branch structure but prevents certain branch nodes being available. The co-ordinator can report errors arising from accessing non-existent nodes as it would if future nodes were referenced.

12 Implementation

This section sketches some ideas on implementation. The state of the graph tree is uniquely defined by the sequence of updates that lead up to its current structure. This can be used for physical storage. First create a string b-tree to map referenced atom names to a natural number. Anonymous atoms can be numbered more easily. Take each update and replace all atom references by the assigned number. Store both the pool of atom names and each update formula. As an update is committed entries are written to the string pool and then the update appended to the update log.

The database would be inefficient to handle like this so an in memory representaion is kept that is efficient to handle. Where this exceeds the memory bounds it can be paged to external storage as blocks. It doesn’t matter whether blocks are flushed often since the definitive tree state is held by the update log. On failure this can be consulted to repair the running representation. The blocks may contain some portion of an uncommitted update at any time without harm.

It’s not necessary to prematurely force blocks to external storage. By deferring this steps enables multiple blocks to be written without additional seeks. Crucially an update could incur as little cost as the single commit to the update log requiring only a single seek if it contains no new atom names.

If archiving occurs a check point of the running representation at the archive point can be made, the update log truncated and the string pool garbage collected. A second consideration is branching the update log but this is harder where grafting occurs.

The running representation will take the form of blocks handling various edges. Edges are not necessarily treated in isolation but in sets are discussed in section 9. For each edge set it is only necessary to record at what version it was toggled. At a branch point a link is made to its parent branch. When blocks are overfull the edge sets can spill into additional blocks such that like versions are held as closely together as possible. Searching back to the root for each query counting the number of times edges have been toggled can be avoided by keeping a status flag in each block for some known version.

A Δ-algebra

Some results about the Δ-algebra are given here. We write \overline{X} to mean the complement of X in 𝔸^{2}. The definition of the change set combine operator ⊕ is such that:

X ⊕ Y = (X ∪ Y) \ (X ∩ Y)

By definition we can see that X ⊕ Y = Y ⊕ X and X ⊕ X = ∅.

X ⊕ Y = (X ∪ Y) \ (X ∩ Y)
= (X ∪ Y) ∩ \overline{(X ∩ Y)}
= (X ∪ Y) ∩ (\overline{X} ∪ \overline{Y})  (Δ1)
= (X ∩ \overline{Y}) ∪ (\overline{X} ∩ Y)  (Δ2)

\overline{X ⊕ Y} = \overline{(X ∪ Y) ∩ (\overline{X} ∪ \overline{Y})}  (by (Δ1))
= \overline{(X ∪ Y)} ∪ \overline{(\overline{X} ∪ \overline{Y})}
= (\overline{X} ∩ \overline{Y}) ∪ (X ∩ Y)  (Δ3)
= (\overline{X} ∪ Y) ∩ (X ∪ \overline{Y})
= (\overline{X} ∪ Y) ∩ \overline{(\overline{X} ∪ Y)}
= \overline{X} ⊕ Y = X ⊕ \overline{Y}  (Δ4)

(X ⊕ Y) ⊕ Z = ((X ⊕ Y) ∩ \overline{Z}) ∪ (\overline{(X ⊕ Y)} ∩ Z)  (by (Δ2))
= ((X ∩ \overline{Y}) ∪ (\overline{X} ∩ Y) ∩ \overline{Z})∪  (by (Δ2))
((\overline{X} ∩ \overline{Y}) ∪ (X ∩ Y) ∩ Z)  (by (Δ3))
= (X ∩ \overline{Y} ∩ \overline{Z}) ∪ (\overline{X} ∩ Y ∩ \overline{Z})∪
(\overline{X} ∩ \overline{Y} ∩ Z) ∪ (X ∩ Y ∩ Z)
= X ⊕ (Y ⊕ Z)  (by symmettry)

(X ⊕ Y) ∩ Z = (X ∪ Y) ∩ \overline{(X ∩ Y)} ∩ Z
= ((X ∪ Y) ∩ Z) ∩ ((\overline{X} ∪ \overline{Y}) ∪ \overline{Z})  (Z ∩ \overline{Z} = ∅)
= ((X ∩ Z) ∪ (Y ∩ Z)) ∩ ((\overline{X} ∪ \overline{Z}) ∪ (\overline{Y} ∪ \overline{Z}))
= ((X ∩ Z) ∪ (Y ∩ Z)) ∩ (\overline{(X ∩ Z)} ∪ \overline{(Y ∩ Z)})
= ((X ∩ Z) ∪ (Y ∩ Z)) ∩ \overline{((X ∩ Z) ∩ (Y ∩ Z))}
= (X ∩ Z) ⊕ (Y ∩ Z)  (Δ5)

The definition of the change set restriction operator ↾_{X} is such that:

G ↾_{X}= (G ∩ X, \overline{G} ∩ X)

If G ↾_{X}= (A, B) then X = A ∪ B.

B Unresolved Questions

• Anonymous atoms could be exhausted by updates such as [x ⇝ x]. Should certain updates be denied?

• Can atoms be typed such that x^{t} implies x ⇝ t? eg. {x^{t}|ϕ(x)} ≡ {x|x ⇝ t∧ϕ(x)} and (∀x^{t})ϕ(x) ≡ (∀x)(x ⇝ t → ϕ(x)). This would force all graphs to be necessarily finite since atom ranges would be explicitly defined by their type.

• Could anonymous selection be made a right-hand side term?

• Do the merge conflict conditions work in all relevant situations? Certainly they do in transitions such as from a ⇝ 1 to a ⇝ 2 since it contains both a removal and an addition.

References

[1] “Efficient Lexicographic Encoding of Numbers”, Peter Seymour.