Skip to main content


Potentially idiosyncratic notation used throughout the rest of the pages.


When the integer \(X\) appears in a context where a set is expected, it is taken to mean \(\{ 0, \ldots, X-1 \}\). F.ex. \(A \times 2 = A \times \{0,1\}\).

When an index \(i \in \{ 0, 1 \}\) appears primed, \(i^\prime\) it is taken to mean \(i\)'s complement in \(\{ 0, 1 \}\).


A variable \(x\) inhabits some set \(X\). Its valuation is denoted \(?x\). The valuation is assumed to change in discrete steps, and the trace of the variable is the sequence \(\{ ?x^{t} \ldots \}\),with \(t \in \N\). If the superscript is omitted \(?x\) typically refers to the latest valuation of the trace. \(?x \in X\) is taken to mean a variable \(x\) in \(X\).

If a variable \(?p \in P\), is a tuple, \(?(x,y) \in X \times Y\) the same notation is used on the components of the tuple, ie \(?p^t\), \(?(x,y)^t\) and \((?x^t,?y^t)\) all convey the same meaning.

Higher order functions

A higher order function is a function, \(f \colon A \to G\), where \(g \in G\) are themselves functions, \(g \colon B \to C\). It is denoted here with \(f \colon A \to B \to C\), ie \(\to\) is right-associative in this context.


The junction of a directed graph, \(G = (V,E)\), is a set of incident edges, \(y \subseteq E\). Two edges, \(e_0 = (v_{00},v_{01})\), \(e_1 = (v_{10},v_{11})\), are said to be incident if source or target is equal, ie \((v_{00} = v_{10} \lor v_{01} = v_{11})\). The junctions, \(Y = \{ y \ldots \}\), are found by taking the transitive closure of this incidence relation on \(E\). Note that \(\bigcup \limits_{y \in Y} = E\) and \(y_0 \neq y_1 \implies y_0 \cap y_1 = \emptyset\).

\(V(y)\) denotes vertices incident to \(e \in y\), \(V^0(y)\) denotes sources in \(e \in y\), and \(V^1(y)\) denotes targets. \(y^0(v)\) denotes the junction containing the edges whose target is \(v\), and \(y^1(v)\) denotes the junction containing the edges whose source is \(v\).

Lets clarify with an example, the graph \(G_0\):

\begin{equation*} \begin{gathered} G_0 = (V_0,E_0) \\ V_0 = \{ v_i \mid i \in 4 \}\\ E_0 = \{ (v_0,v_2),(v_1,v_2),(v_2,v_3) \} \\ \end{gathered} \end{equation*}

Or, as a diagram:

G0v_0 v0v_2 v2v_0:e->v_2:w v_1 v1v_1:e->v_2:w v_3 v3v_2:e->v_3:w

Here are some sample results for \(G_0\) using the definitions above:

\begin{equation*} \begin{aligned} Y &= \{ \{e_0,e_1 \}, \{e_2\} \} \\ V^0(y_0) &= \{ v_0, v_2 \} \\ V^1(y_1) &= \{ v_3 \} \\ y^0(v_2) &= y_0 \\ y^0(v_0) &= \emptyset \end{aligned} \end{equation*}