Let $⟨{\omega }_1,\dots ,{\omega }_k⟩\in Seq(\Omega )$. Define the function

$${\mathrm{s}}^{\mathrm{-}}:Seq(\Omega )⟶Seq(\Omega )\cup \{\perp \}$$ by: $$\begin{array}{c}\hfill s^{-}(⟨{\omega }_1,\dots ,{\omega }_k⟩)=⟨{\omega }_1,\dots ,{\omega }_{k-1}⟩,k\ge 2,\hfill \\ \hfill s^{-}(⟨\omega ⟩)=⟨⟩,\hfill \\ \hfill s^{-}(⟨⟩)=\perp \hfill \end{array}$$

For each element $v\in V_{\mathrm{c}}$, define a possibly empty finite set of the element’s arguments, denoted by $args(v)$.

The cardinality of this set is called the arity of $v$: $$arity(v)=|args(v)|.$$

The arguments of an element $v$ are represented as ordered pairs $<v,i>$, consecutively indexed from $1$ to $arity(v)$: $$args(v)=\{<v,i>\mid 1\le i\le arity(v)\}.$$

Let $$A=\bigcup _{v\in V_{\mathrm{c}}}args(v)$$ be the set of all argument tokens.

Argument tokens are distinct from model elements and literals: $$A\cap (V\cup L)=\varnothing .$$

For an argument token $a=<v,i>\in A$, define $$argOwner(a)=v$$ and $$argPos(a)=i.$$

For each element $v\in V_{\mathrm{c}}$, define a (possibly empty) finite set of internal property assignments, denoted by $props(v)$.

If there exists a unique $\mathrm{d}\mathrm{f}$-relation $v\stackrel{\mathrm{d}\mathrm{f}}{⟶}w$, then $$props(v)\subseteq args(w)\times (V_{\mathrm{c}}\cup V_{\mathrm{\kappa }}\cup L),$$ and property assignment is functional in its first coordinate: $$\forall <a_1,{\alpha }_1>,<a_2,{\alpha }_2>\in props(v):a_1=a_2\Rightarrow {\alpha }_1={\alpha }_2.$$

Otherwise, $$props(v)=\varnothing .$$

Let $v\in V_{\mathrm{c}}$. The argument-correspondence data carried by $v$ determine a map $argMap(v)$.

If a unique $\mathrm{d}\mathrm{f}$-relation $v\stackrel{\mathrm{d}\mathrm{f}}{⟶}w$ exists, then $$argMap(v):\{1,\dots ,arity(v)\}⟶\{1,\dots ,arity(w)\}\cup \{\perp \}.$$ Otherwise, $$argMap(v):\{1,\dots ,arity(v)\}⟶\{\perp \}.$$

A variorum state is a pair

$$\begin{array}{c}\hfill \Sigma =(V,E),\hfill \\ \hfill \hfill \end{array}$$ where $V$ is a finite set of structured model elements carrying the type, argument, argument-correspondence, and property data defined in sections B–D, and $E$ is the finite set of typed relations defined in section C.

The functions $t$, $args$, $arity$, $props$, $argOwner$, $argPos$, and $argMap$, and the sets $V_{\mathrm{r}}$, $V_{\mathrm{c}}$, $V_{\mathrm{\kappa }}$, and $A$, are induced by $V$.

A variorum state is valid if and only if it satisfies the following rules E1-E14.

Define the sets of root and situated elements by:

$$\begin{array}{c}\hfill V_{\mathrm{r}\mathrm{o}\mathrm{o}\mathrm{t}}=\{v\in V_{\mathrm{\kappa }}\mid \nexists e\in E_{\mathrm{p}\mathrm{u}}\mathrm{\text{with}}source(e)=v\}\hfill \\ \hfill V_{\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{u}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{d}}=\{v\in V_{\mathrm{c}}\cup V_{\mathrm{\kappa }}\mid \exists e\in E_{\mathrm{p}\mathrm{u}}\mathrm{\text{with}}source(e)=v\}\hfill \end{array}$$

Define $$\begin{array}{c}\hfill (v\mathrm{\text{is root}}):=v\in V_{\mathrm{r}\mathrm{o}\mathrm{o}\mathrm{t}}\hfill \end{array}$$ and

$$\begin{array}{c}\hfill (v\mathrm{\text{is situated}}):=v\in V_{\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{u}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{d}}\hfill \end{array}$$

Let $v_1,v_k\in V$. A placement path from $v_1$ to $v_k$ is a finite sequence of elements $⟨v_1,\dots ,v_k⟩\in Seq(V_{\mathrm{c}}\cup V_{\mathrm{\kappa }})$ with $k\ge 2$ such that $(v_i,v_{i+1})\in E_{\mathrm{p}\mathrm{u}}$ for all $i=1,\dots ,k-1$.

A placement path $⟨v_1,\dots ,v_k⟩$ is forward-maximal iff there is no $w\in V$ with $(v_k,w)\in E_{\mathrm{p}\mathrm{u}}$.

For all $x\in V_{\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{u}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{d}}$, define $parent(x)$ by:

$$\begin{array}{c}\hfill parent(x)=y\mathrm{\text{where}}(x,y)\in E_{\mathrm{p}\mathrm{u}}\hfill \end{array}$$

For convenience, define the function

$$pu\_path:V\times V⟶Seq(V)$$ by: $$\begin{array}{c}\hfill pu\_path(v,w)=⟨v,\dots ,w⟩,\mathrm{\text{the unique placement path from}}v\mathrm{\text{to}}w\mathrm{\text{, if such a path exists,}}\hfill \\ \hfill pu\_path(v,w)=⟨⟩,\mathrm{\text{if no placement path from}}v\mathrm{\text{to}}w\mathrm{\text{exists}}\hfill \end{array}$$ For $v\in V$, define the backward $\mathrm{p}\mathrm{u}$-reachable set rooted at $v$ as the set of all elements $w\in V$, different from $v$, for which there exists a placement path from $w$ to $v$. Denote it by

$$\begin{array}{c}\hfill R_{\mathrm{p}\mathrm{u}}(v):=\{w\in V\mid pu\_path(w,v)\ne ⟨⟩,\mathrm{\text{with}}w\ne v\}\hfill \end{array}$$

$$\begin{array}{c}\hfill \forall (r,x)\in E_{\mathrm{c}\mathrm{b}},referent(x)=r,\hfill \\ \hfill \forall x\in V:\nexists r\in V_{\mathrm{r}}\mathrm{\text{such that}}(r,x)\in E_{\mathrm{c}\mathrm{b}},referent(x)=\perp .\hfill \end{array}$$

Define the sets of origin and derived elements by:

$$\begin{array}{c}\hfill V_{\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{i}\mathrm{n}}=\{v\in V_{\mathrm{c}}\mid \exists e\in E_{\mathrm{d}\mathrm{f}}\mathrm{\text{with}}target(e)=v\wedge \nexists e\in E_{\mathrm{d}\mathrm{f}}\mathrm{\text{with}}source(e)=v\}\hfill \\ \hfill V_{\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{d}}=\{v\in V_{\mathrm{c}}\mid \exists e\in E_{\mathrm{d}\mathrm{f}}\mathrm{\text{with}}source(e)=v\}\hfill \end{array}$$ Define

$$\begin{array}{c}\hfill (v\mathrm{\text{is origin}}):=v\in V_{\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{i}\mathrm{n}}\hfill \end{array}$$ and

$$\begin{array}{c}\hfill (v\mathrm{\text{is derived}}):=v\in V_{\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{d}}\hfill \end{array}$$

Let $c_1,c_k\in V_{\mathrm{c}}$. A derivation path from $c_1$ to $c_k$ is a finite sequence of concepts $⟨c_1,\dots ,c_k⟩\in Seq(V_{\mathrm{c}})$ with $k\ge 2$ such that $(c_i,c_{i+1})\in E_{\mathrm{d}\mathrm{f}}$ for all $i=1,\dots ,k-1$.

A derivation path $⟨c_1,\dots ,c_k⟩$ is forward-maximal iff there is no $w\in V_{\mathrm{c}}$ with $(c_k,w)\in E_{\mathrm{d}\mathrm{f}}$.

For $c\in V_{\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{d}}$, let $⟨c,c_1,\dots ,c_k⟩$, with $k\ge 1$, be the (unique) forward-maximal derivation path starting at $c$. Define:

$$\begin{array}{c}\hfill A_{\mathrm{d}\mathrm{f}}(c)=\{c_1,c_2,\dots ,c_k\}\hfill \end{array}$$ to be the forward df-reachability set starting at $c$.

For $c\notin V_{\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{d}}$,

$$\begin{array}{c}\hfill A_{\mathrm{d}\mathrm{f}}(c)=\varnothing \hfill \end{array}$$

For $x\in V$, define $predecessor(x)$ by:

$$\begin{array}{c}\hfill predecessor(x)=y,\mathrm{\text{if}}x\in V_{\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{d}}\mathrm{\text{and}}(x,y)\in E_{\mathrm{d}\mathrm{f}},\hfill \\ \hfill predecessor(x)=\perp ,\mathrm{\text{if}}x\notin V_{\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{d}}.\hfill \end{array}$$

For convenience, define the function

$$df\_path:V\times V⟶Seq(V)$$ by: $$\begin{array}{c}\hfill df\_path(v,w)=⟨v,\dots ,w⟩,\mathrm{\text{the unique derivation path from}}v\mathrm{\text{to}}w\mathrm{\text{, if such a path exists,}}\hfill \\ \hfill df\_path(v,w)=⟨⟩,\mathrm{\text{if no derivation path from}}v\mathrm{\text{to}}w\mathrm{\text{exists}}\hfill \end{array}$$ For $v\in V$, define the backward $\mathrm{d}\mathrm{f}$-reachable set originating at $v$ as the set of all elements $w\in V$ for which a $\mathrm{d}\mathrm{f}$-path from $w$ to $v$ exists, and denote it by $R_{\mathrm{d}\mathrm{f}}(v):=\{w\in V\mid df\_path(w,v)\ne ⟨⟩\}$.

A meaning function on $M$ is a deterministic function $$\mu :M⟶𝒟(M).$$ A defining equation for $\mu (x)$ specifies the dependency term $\mu (x)\in 𝒟(M)$. If its right-hand side contains previously defined operations, rather than or in addition to dependency-term notation, these are evaluated first.

For a dependency term $d\in 𝒟(M)$, $atoms(d)$ is the set of all members of $M$ that occur in $d$.

For $x,y\in M$, $y$ $\mu$-affects $x$ if and only if $y$ occurs in the dependency term $\mu (x)$: $$y\mu \mathrm{\text{-affects}}x\iff y\in atoms(\mu (x)).$$ When $\mu$ is clear from the context, we may write “$y$ affects $x$” instead of “$y$ $\mu$-affects $x$”.

Let $${𝒯}^d=\{{\mathrm{p}\mathrm{u}}^d,{\mathrm{c}\mathrm{b}}^{-d},{\mathrm{d}\mathrm{f}}^d,{\mathrm{a}\mathrm{o}}^d,{\mathrm{a}\mathrm{p}}^d,{\mathrm{b}}^d,{\mathrm{f}}^d,{\mathrm{r}}^d\}$$ be the set of potentially semantic dependency labels.

Define the function $$argPred:A⟶A\cup \{\perp \}$$ as follows:

Let $a=<v,j>\in A$, so that $argOwner(a)=v$ and $argPos(a)=j$.

If there exists a df-edge $v\stackrel{\mathrm{d}\mathrm{f}}{⟶}w$ and $argMap(v)(j)=i\ne \perp$, then $$argPred(a)=<w,i>\in args(w)\subseteq A.$$ Otherwise, that is, if no such edge exists, or if $argMap(v)(j)=\perp$, $$argPred(a)=\perp .$$

Let $\Sigma =(V,E)$ be a valid variorum state. A pair $(M,{\Omega }^d)$, where $M$ is a meaning-bearer set as defined in G1 and ${\Omega }^d\subseteq {𝒯}^d$ is a semantic activation scheme, is an admissible semantic basis for $\Sigma$ if and only if: $$\begin{array}{cc}\hfill & M\cap V\ne \varnothing ,\hfill \\ \hfill & {\mathrm{p}\mathrm{u}}^d\in {\Omega }^d,\hfill \\ \hfill & {\mathrm{a}\mathrm{p}}^d\in {\Omega }^d\Rightarrow {\mathrm{d}\mathrm{f}}^d\in {\Omega }^d\wedge {\mathrm{a}\mathrm{o}}^d\in {\Omega }^d,\hfill \\ \hfill & {\mathrm{b}}^d\in {\Omega }^d\Rightarrow {\mathrm{a}\mathrm{p}}^d\in {\Omega }^d,\hfill \\ \hfill & {\mathrm{b}}^d\in {\Omega }^d\iff {\mathrm{f}}^d\in {\Omega }^d\iff {\mathrm{r}}^d\in {\Omega }^d,\hfill \\ \hfill & M\cap V_{\mathrm{r}}\ne \varnothing \iff {\mathrm{c}\mathrm{b}}^{-d}\in {\Omega }^d,\hfill \\ \hfill & M\cap A\ne \varnothing \iff {\mathrm{a}\mathrm{o}}^d\in {\Omega }^d,\hfill \\ \hfill & \forall \tau \in {\Omega }^d\forall x,y\in V\cup A,(x,\tau ,y)\in {\hat{E}}_{\tau }^d\Rightarrow x,y\in M.\hfill \end{array}$$

Let $\Sigma =(V,E)$ be a valid variorum state, and let $(M,{\Omega }^d)$ be an admissible semantic basis for $\Sigma$. For every $\tau \in {𝒯}^d$, define $$E_{\tau }^d={\hat{E}}_{\tau }^d\mathrm{\text{if}}\tau \in {\Omega }^d,E_{\tau }^d=\varnothing \mathrm{\text{if}}\tau \notin {\Omega }^d.$$ The primary dependency graph is the directed, typed graph $${𝒢}^d=(M,E^d),$$ where $$E^d=E_{\mathrm{p}\mathrm{u}}^d\cup E_{\mathrm{c}{\mathrm{b}}^{\mathrm{-}}}^d\cup E_{\mathrm{d}\mathrm{f}}^d\cup E_{\mathrm{a}\mathrm{o}}^d\cup E_{\mathrm{a}\mathrm{p}}^d\cup E_{\mathrm{b}}^d\cup E_{\mathrm{f}}^d\cup E_{\mathrm{r}}^d\subseteq M\times {𝒯}^d\times M.$$

Let ${𝒢}^d=(M,E^d)$ be a primary dependency graph. Define the dependency-type function: $$t^d:E^d⟶{𝒯}^d$$ by: $$t^d((x,\tau ,y))=\tau .$$

Let ${𝒢}^d=(M,E^d)$ and ${{𝒢}^{\prime }}^d=(M^{\prime },{E^{\prime }}^d)$ be directed typed dependency graphs, such as primary dependency graphs or their restrictions, where $E^d\subseteq M\times {𝒯}^d\times M$ and ${E^{\prime }}^d\subseteq M^{\prime }\times {𝒯}^d\times M^{\prime }$.

A dependency-graph isomorphism $$\phi :{𝒢}^d⟶{{𝒢}^{\prime }}^d$$ is a bijection $\phi :M⟶M^{\prime }$ such that, for all $u,v\in M$ and every $\tau \in {𝒯}^d$, $$(u,\tau ,v)\in E^d\iff (\phi (u),\tau ,\phi (v))\in {E^{\prime }}^d.$$ When ${𝒢}^d={{𝒢}^{\prime }}^d$, a dependency-graph isomorphism is called a dependency-graph automorphism.

Let ${𝒢}^d=(M,E^d)$ be a primary dependency graph with dependency-type function $t^d:E^d⟶{𝒯}^d$. For $x\in M$, define the semantic signature as: $${𝒮}^d(x)=\{<\mathrm{o}\mathrm{u}\mathrm{t},\tau ,y>\mid y\in M,(x,\tau ,y)\in E^d\}\cup \{<\mathrm{i}\mathrm{n},\tau ,y>\mid y\in M,(y,\tau ,x)\in E^d\}.$$

A semantic configuration is a triple $$C=(\Sigma ,M,{\Omega }^d),$$ where $\Sigma$ is a valid variorum state, and $(M,{\Omega }^d)$ is an admissible semantic basis for $\Sigma$.

Let $x_1,x_k\in M$. A forward semantic path from $x_1$ to $x_k$ is a finite sequence $⟨x_1,\dots ,x_k⟩$ of $k\ge 2$ members of $M$, such that for all $i=1,\dots ,k-1$ there exists $\tau \in {𝒯}^d$ with $$(x_i,\tau ,x_{i+1})\in E^d.$$ Let $ℛ{𝒢}^d$ denote the set of all forward semantic paths over ${𝒢}^d$, and let $${ℛ}^{+}{𝒢}^d(x)=\{y\mid \exists ⟨x,\dots ,y⟩\in ℛ{𝒢}^d\},$$ $${ℛ}^{-}{𝒢}^d(x)=\{y\mid \exists ⟨y,\dots ,x⟩\in ℛ{𝒢}^d\}$$ denote the sets of all meaning bearers that can be semantically reached from $x$ and from which $x$ can be semantically reached, respectively.

For $x\in M$, let $$𝒩{𝒢}^d(x)=\{x\}\cup {ℛ}^{+}{𝒢}^d(x)\cup {ℛ}^{-}{𝒢}^d(x).$$

Let ${𝒢}^d[x]$ be the restriction of ${𝒢}^d$ to $𝒩{𝒢}^d(x)$. That is, $${𝒢}^d[x]=(𝒩{𝒢}^d(x),E^d[x]),$$ where $$E^d[x]=\{(u,\tau ,v)\in E^d\mid u,v\in 𝒩{𝒢}^d(x)\}.$$ The dependency-type function on ${𝒢}^d[x]$ is the restriction of $t^d$ to $E^d[x]$.

Let $C$ be a semantic configuration and let $x\in M_C$. The pair $$({𝒢}_C^d[x],x)$$ is called the pointed dependency graph at $x$.

Let $C$ and $C^{\prime }$ be semantic configurations, and let $x\in M_C$ and $x^{\prime }\in M_{C^{\prime }}$. A pointed dependency-graph isomorphism from $({𝒢}_C^d[x],x)$ to $({𝒢}_{C^{\prime }}^d[x^{\prime }],x^{\prime })$ is a dependency-graph isomorphism $$\psi :{𝒢}_C^d[x]⟶{𝒢}_{C^{\prime }}^d[x^{\prime }]$$ such that $\psi (x)=x^{\prime }$.

Let $\Sigma =(V,E)$ and ${\Sigma }^{\prime }=(V^{\prime },E^{\prime })$ be variorum states, not necessarily distinct, with element sets $V$ and $V^{\prime }$, relation sets $E$ and $E^{\prime }$, and argument-token sets $A$ and $A^{\prime }$ induced from $V$ and $V^{\prime }$, respectively.