Sets

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

Variables

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.

Graphs

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\):

Or, as a diagram:

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