Symbols and Notations

$𝔸$

Universe of identifiers / atomic names (catalog names, labels, property keys, column names).

$𝕃\subseteq 𝔸$

Universe of label names.

$𝕂\subseteq 𝔸$

Universe of property keys (property names).

$𝕀$

Universe of globally unique graph-element identifiers.

$𝕋$

Universe of types (static, dynamic, and base types).

$𝕍$

Universe of material values together with the null value.

$\mathrm{null}$

Distinguished null value NULL.

$\mathbb{N}$

Natural numbers.

$\infty$

Infinity (used for implementation-defined maxima and unbounded path-pattern or RPE repetition).

${\mathbb{Z}}_{>0}$

Positive integers.

$X^{\ast }$

Set of finite sequences over $X$, including the empty sequence.

$\mathcal{P}(X)$

Powerset of $X$.

$\mathcal{M}(X)$

Bag/multiset of elements from $X$ (multiplicity function over $X$).

${\mathcal{M}}_{\mathrm{fin}}(X)$

Finite bag/multiset over $X$.

$\rightharpoonup$

Partial function / partial map.

$\mapsto$

Mapping constructor (e.g., $k\mapsto w$).

$\triangleq$

Definitional equality.

$⟦\cdot ⟧$

Denotation / semantic evaluation function.

$⊢$

Typing / judgment turnstile.

$\vDash$

Satisfaction relation.

$⊑$

Subtype relation.

$\mathrm{\Xi }$

Static type environment.

$G$

A (GQL) property graph.

$V\subseteq 𝕀$

Finite set of node identifiers.

$E\subseteq 𝕀$

Finite set of edge identifiers, disjoint from $V$ (multigraph permitted).

${\lambda }_V:V\to \mathcal{P}(𝕃)$

Node label map.

${\lambda }_E:E\to \mathcal{P}(𝕃)$

Edge label map.

${\rho }_V:V\to (𝕂\rightharpoonup 𝕍)$

Node property map.

${\rho }_E:E\to (𝕂\rightharpoonup 𝕍)$

Edge property map.

$\mathrm{src},\mathrm{dst}:E\to V$

Edge endpoint functions; for an undirected edge their order is representational only.

$\to ,\leftrightarrow$

Directed / undirected edge markers.

$\mathrm{dir}:E\to \{\to ,\leftrightarrow \}$

Edge directedness (directed/undirected).

${ℝ}_{\mathrm{cat}}$

Syntactically well-formed catalog object references of the GQL grammar.

$\mathbb{Q}$

Globally resolved references to catalog objects.

$\mathrm{Catalog}$

Abstract carrier of well-formed hierarchical GQL-catalogs.

$\mathcal{C}$

Catalog (logical collection of named GQL objects).

$\mathcal{X}$

Active context (catalog + working schema + working graph site).

$\mathrm{WSR}$

Working schema reference (default parent for relative catalog-object references).

$\mathrm{WG}$

Working graph site, occupied by a graph reference value whose referent is the working graph.

$\Re$

Resolution environment (used by typing judgments).

$\mathrm{Loc}$

Local map of parameters and binding variables used while typing expressions; catalog procedure references use catalog resolution.

${\mathrm{resolve}}_S(\mathcal{X},r)$

Resolution of syntactic catalog reference $r\in {ℝ}_{\mathrm{cat}}$ to a globally resolved reference of sort $S$.

$\mathrm{BT}$

Domain of descriptor-bearing binding tables.

$\mathrm{BindingTables}:\mathbb{Q}\rightharpoonup \mathrm{BT}$

Derived catalog projection from resolved binding-table references to binding-table objects.

$\mathrm{SCX}$

Session context containing the session authorization identifier, principal, time zone, session schema and graph, parameters, list behavior, transaction and request context, and termination flag.

$\mathrm{ListBeh}$

Session list-behavior policy for offset/ordinal indexing, negative indices, and out-of-range behavior; it does not govern list unwinding.

$T,\mathrm{BT}\in \mathrm{BT}$

Binding-table objects.

${\mathrm{BT}}_{\mathrm{unit}}$

Unit binding table containing one empty record; distinct from an empty binding table.

${\tau }_{\mathrm{rec}}$

Record type of a binding table.

$\mathrm{fields}({\tau }_{\mathrm{rec}})$

Declared field-name set of record type ${\tau }_{\mathrm{rec}}$.

${\mathrm{Rec}}_{{\tau }_{\mathrm{rec}}}$

Set of records inhabiting record type ${\tau }_{\mathrm{rec}}$.

$T=⟨{\tau }_{\mathrm{rec}},B,\mathrm{ord},\mathrm{pcs}⟩$

Binding table represented by its record type, finite record multiset, ordering component, and preferred column-name sequence.

$B\in {\mathcal{M}}_{\mathrm{fin}}({\mathrm{Rec}}_{{\tau }_{\mathrm{rec}}})$

Underlying finite multiset of record occurrences.

$\mathrm{supp}(B)$

Support of bag $B$: the set of elements with positive multiplicity.

$1[P]$

Indicator of proposition $P$: $1$ if $P$ holds and $0$ otherwise.

$\mathrm{ord}$

Either the unordered marker or an ordering of the record occurrences of $B$.

$\mathrm{pcs}$

Preferred column-name sequence: not set or a permutation of the table’s column names.

$\mathrm{bag}(T)=⟨{\tau }_{\mathrm{rec}},B⟩$

Order-insensitive bag projection; it is not the complete binding-table object.

$\mathrm{cols}(T)$

Column set of binding table $T$.

$C_{\mathrm{new}}$

Newly introduced columns (e.g., by a pattern).

$\mathrm{PPat},\mathrm{GPat},\mathrm{GPBT}$

Sets of well-formed path patterns, graph patterns, and graph pattern binding tables.

$\Gamma \in \mathrm{GPat}$

Graph pattern, including an optional WHERE clause but not a YIELD clause.

${\mathrm{\Delta }}_{\mathrm{gpbt}}\in \mathrm{GPBT}$

Graph pattern binding table: a graph pattern with an explicit or implicit YIELD clause; the subscript distinguishes it from an update delta.

$\mathrm{vars}(\Gamma ),{\mathrm{vars}}_{\exp }(\Gamma )$

Declared and exposed graph-pattern variables, including non-value subpath markers.

${\mathrm{vars}}_{\mathrm{bind}}(\Gamma ),{\mathrm{vars}}_{\exp }^{\mathrm{bind}}(\Gamma )$

All and exposed value-bearing node, edge, and path variables.

$D_{\mathrm{expo}},D_{\mathrm{ref}}$

Exposure degree; and reference degree, which is undefined for non-referenceable subpath variables.

$\mathrm{bind}(h)$

Binding extracted from match $h$ and restricted to variables exported by the pattern.

${\mathrm{GPBT}}_{{\mathrm{\Delta }}_{\mathrm{gpbt}}}(T)$

Graph-pattern binding-table operator for graph pattern binding table ${\mathrm{\Delta }}_{\mathrm{gpbt}}$.

$\mathrm{MatchStmt}$

Abstract domain of match statements.

$\mathrm{MatchOp},\mathrm{MatchBlock}$

Abstract domains of match operators and match blocks.

$\mathcal{Q}\in \mathrm{MatchBlock}$

Match-block metavariable, distinguished from bags $\mathcal{B}$ used by the binding-table algebra.

$⟦\mathrm{Match}({\mathrm{\Delta }}_{\mathrm{gpbt}}){⟧}_{\mathrm{match}}$

Denotation of MATCH as a binding-table transformer.

${\sigma }_{\phi },{\pi }_X$

Selection and projection operators.

$⋊⋉$

Bag natural join.

$\uplus$

Bag union, adding record multiplicities.

$\mu \sim \nu ,\mu \bigsqcup \nu$

Compatibility and merge of record mappings.

${\mathcal{B}}_1{⋊⋉}_{𝜃}{\mathcal{B}}_2$

Guarded bag join: natural join followed by filtering with guard $𝜃$.

$<msub><mrow>⊲</mrow><mrow>𝜃</mrow></msub>$

Left outer join with guard $𝜃$.

${\mathrm{OptExpand}}_{\mathcal{F}}(T)$

Per-record optional expansion of $T$ by correlated binding-table transformer $\mathcal{F}$.

${\mathrm{Out}}_{\mathcal{F}}(\mu )$

New-column output of correlated transformer $\mathcal{F}$ for one incoming record occurrence $\mu$.

${\mathrm{unnest}}_{n:L}(T)$

FOR/list-unnesting operator, binding $n$ to each list element occurrence in field $L$.

$\mathrm{hdr}(\mathcal{B})$

Variables in the declared record type of bag-valued binding-table representation $\mathcal{B}$.

${\pi }_L,\ominus ,{\mathrm{pad}}_R$

Left-variable projection, bag difference on left projections, and null-padding of right-only variables.

$\mathcal{E}$

Static environment for variables, parameters, functions, and relevant catalog objects.

$\mathrm{Dyn}=(G,{\mu }_o)$

Dynamic subquery environment: current graph and current outer-row mapping.

$\mathrm{WALK}$

Path mode: walk (default).

$\mathrm{TRAIL}$

Path mode: trail.

$\mathrm{ACYCLIC}$

Path mode: acyclic path.

$\mathrm{SIMPLE}$

Path mode: simple path.

$M,\mathrm{mode},\mathrm{pm}$

Generic path-mode parameters.

$\mathrm{Path}(G)$

Set of finite graph paths in $G$, represented by alternating node/edge sequences.

$\mathrm{PathVal}$

Carrier of material GQL path values, which encapsulate path-element reference lists.

$w\in \mathrm{Path}(G)$

Graph path or RPE witness.

$p\in \mathrm{PathVal}\cup \{\mathrm{null}\}$

Material or null path value.

${\mathrm{ok}}_M(w)$

Predicate that graph path $w$ satisfies path mode $M$.

$\mathrm{head}(w),\mathrm{tail}(w)$

First- and last-node accessors for a graph path or RPE witness $w$.

$\mathrm{len}(w)$

Edge-step length of a graph path or RPE witness $w$.

$\mathrm{PEL}(p),\mathrm{len}(p)$

Path-element list and edge length of path value $p$.

$\mathrm{nodes}(p),\mathrm{edges}(p)$

Node- and edge-list accessors for a path value.

$\mathrm{head}(p),\mathrm{tail}(p)$

First- and last-node accessors for a path value.

$p\circ q$

Concatenation of path values whose boundary node references have the same referent.

${\mathrm{\Sigma }}_L$

Finite alphabet of edge-label names used by the auxiliary RPE calculus.

$r,R$

Regular path expressions.

$𝜀$

Auxiliary zero-edge regular path expression.

$\delta ,S_{\delta }$

Step predicate and graph-induced ternary step relation.

$\psi :\mathrm{Path}(G)\to \{\top <!--\; FUNCTION\; APPLICATION\; -->,\perp \}$

Boolean path predicate used to guard an auxiliary regular path expression.

$\mathit{⟦r}{⟧}_G^{\mathrm{mode}}$

Bag denotation of $r$ over graph $G$ under the selected path mode.

${\cup }_{\mathrm{ms}},{\cup }_{\mathrm{set}}$

Multiset and set alternation of regular path expressions.

${⋊⋉}_{\bowtie }$

Bag join on a shared endpoint with path-witness concatenation.

$\mathrm{Der}(R,\mathrm{pm})$

Successful auxiliary derivation trees for $R$ under $\mathrm{pm}$.

${\chi }_{\mathrm{sp}}(d),{\equiv }_{\mathrm{sp}}$

Subpath-marker trace of derivation $d$, and equality modulo the same endpoint/path/marker trace.

$\mathrm{Cand}(R,\mathrm{pm})$

Candidate set obtained by quotienting successful derivations while retaining multiset-alternation marker distinctions.

${\mathrm{\Pi }}_{u,v}(\mathrm{Cand}(R,\mathrm{pm}))$

Endpoint-partition subset of $\mathrm{Cand}(R,\mathrm{pm})$ for fixed endpoints $u,v\in V$.

$s$

Selective path-search selector; $\kappa$ is reserved for GQLSTATUS codes.

${\mathrm{SPSP}}_s(\cdot )$

Selective path-search prefix operator with selector $s$.

$\mathrm{ALL}\mathrm{PATHS}$

Non-selective path-search prefix: return all paths; it is not an SPSP.

${\mathrm{ANY}}_N\mathrm{PATHS}$

SPSP form: return any $N$ paths.

${\mathrm{SHORTEST}}_N\mathrm{PATHS}$

SPSP form: return $N$ shortest paths.

${\mathrm{SHORTEST}}_N\mathrm{GROUPS}$

SPSP form: return $N$ shortest groups (partition-wise).

$\mathrm{\Omega }$

Abstract store state used by expression and query evaluation.

${\eta }_g,{\eta }_r$

Global and row environments.

$⇝\subseteq 𝕋\times 𝕋$

Partial implicit-cast relation.

$⟨\mathrm{\Omega },{\eta }_g,{\eta }_r⟩⊢E\Downarrow u$

Expression-evaluation judgment, producing a value or error.

$\mathrm{Var}$

Universe of variables used by expression and graph-pattern semantics.

$\mu :\mathrm{Var}\rightharpoonup 𝕍$

Partial variable binding.

$\mathit{⟦\varphi }{⟧}_{G,\mu }^{\mathrm{tv}}$

Three-valued denotation of predicate $\varphi$.

$\top <!--\; FUNCTION\; APPLICATION\; -->$

True.

$\perp$

False.

$U$

Unknown (Kleene 3-valued logic).

${𝔹}_3=\{\top <!--\; FUNCTION\; APPLICATION\; -->,\perp ,U\}$

Three-valued Boolean domain (true/false/unknown).

$\preccurlyeq ,\prec$

Applicable weak order on comparable values and its strict part.

${\approx }_{\mathrm{nd}}$

Recursive GQL not-distinct relation used by grouping and duplicate treatment.

$K=⟨k_1,\dots <!--\; FUNCTION\; APPLICATION\; -->,k_s⟩$

Ordered sequence of grouping keys; $⟨⟩$ denotes global aggregation.

${\kappa }_K(r)$

Grouping-key tuple extracted from record $r$ in the order fixed by $K$.

${(B_i)}_{i\in I}$

Pairwise disjoint group subbags induced by not-distinct grouping-key tuples.

$B_i{⊑}_{\mathrm{bag}}B$

Subbag relation: every record multiplicity in $B_i$ is at most its multiplicity in $B$.

$F$

Aggregator mapping a finite input bag to one aggregate result.

${\gamma }_{\stackrel{}{g\to };\stackrel{}{h\to }}(B)$

Combined grouping and grouped-projection operator.

${\mathrm{Enum}}_{\mathrm{impl}}(B)$

Implementation-dependent enumeration of an unordered bag’s record occurrences.

${\mathrm{ORDER}\mathrm{BY}}_{\stackrel{}{o\to }}(B)$

Ordered binding table obtained using sort-specification list $\stackrel{}{o\to }$.

${\mathrm{OFFSET}}_o(S)$

Sequence slicing by offset $o$.

${\mathrm{LIMIT}}_{\ell }(S)$

Sequence slicing by limit $\ell$.

${𝕋}_{\mathrm{prop}}\subseteq 𝕋$

Property value types supported by the implementation’s conformance claim.

${𝕋}_{\mathrm{scal}},{𝕋}_{\mathrm{coll}}$

Selected scalar and collection fragments of ${𝕋}_{\mathrm{prop}}$.

$\mathit{⟦\tau ⟧}\subseteq 𝕍$

Denotation of supported property value type $\tau$ (admissible values).

$\mathrm{LIST}⟨\tau ⟩$

Homogeneous list type constructor.

$\mathrm{NodeRef},\mathrm{EdgeRef}$

Reference value types whose referents are nodes and edges, respectively.

$\mathrm{Opt}(\tau )$

Meta-level shorthand for a value type containing $\mathrm{null}$; not a GQL type constructor.

$⊒$

Widening preorder on declarations/types (based on denotations).

$c:⟦{\tau }_0⟧\rightharpoonup ⟦{\tau }_1⟧$

Partial cast between value types.

${\mathbb{N}}_N$

Universe of node-type names.

${\mathbb{N}}_E$

Universe of edge-type names.

${\mathbb{N}}_G$

Universe of graph-type names.

${\mathbb{N}}_{\mathrm{graph}}$

Universe of graph-entry names.

$\mathrm{NDesc}$

Reduced book-level node-type descriptor representation $⟨N,L_N,{\mathrm{ptype}}_N⟩$ contained in a graph type.

$\mathrm{ETypeDesc}$

Reduced book-level edge-type descriptor representation $⟨\mathrm{ET},L_E,{\mathrm{kind}}_E,{\mathrm{endSpec}}_E,{\mathrm{ptype}}_E⟩$ contained in a graph type.

$\mathrm{\Sigma }$

Reduced book-level structural graph-type component $⟨\mathrm{NDecls},\mathrm{EDecls},\mathrm{NodeKLS},\mathrm{EdgeKLS}⟩$.

$\mathrm{NDecls},\mathrm{EDecls}$

Finite node- and edge-type maps inside $\mathrm{\Sigma }$, not top-level catalogs.

$\mathrm{NodeKLS},\mathrm{EdgeKLS}$

Node and edge key-label-set dictionaries inside $\mathrm{\Sigma }$.

$\mathrm{GTypeDesc}$

Reduced book-level graph-type descriptor representation $⟨\mathrm{\Sigma },{\mathcal{I}}_{\mathrm{GT}}⟩$.

$\mathrm{GraphEntry}$

Book-level abstraction $⟨G,{\mathrm{GT}}^{?},{\mathcal{I}}_G⟩$ of a stored-graph descriptor: graph, optional constraining graph-type reference, and direct constraints.

$\mathrm{GE}=⟨G,{\mathrm{GT}}^{?},{\mathcal{I}}_G⟩$

Active graph entry used by conformance, constraint-validation, and data-modification rules.

$\mathrm{none}$

Marker that a graph entry has no constraining graph type.

$\mathrm{Graphs},\mathrm{GraphTypes}$

Derived catalog projections for graphs and graph types after standard reference resolution.

$\mathrm{GT}$

Globally resolved graph-type reference.

${\mathrm{resolve}}_{\mathrm{GraphType}}$

Applied to $(\mathcal{C},\mathrm{GT})$, resolves a graph type to its static descriptor ${\mathrm{\Sigma }}_{\mathrm{GT}}$ and constraint dictionary ${\mathcal{I}}_{\mathrm{GT}}$.

${\mathrm{ptype}}_T:𝕂\rightharpoonup {𝕋}_{\mathrm{prop}}$

Static property signature of type descriptor $T$.

$v::N,e::\mathrm{ET}$

Conformance judgments: node $v$ conforms to node type $N$, and edge $e$ conforms to edge type $\mathrm{ET}$.

${\mathcal{I}}_{\mathrm{GT}},{\mathcal{I}}_G$

Named constraint dictionaries owned by a graph type and directly by a graph, respectively.

${\mathcal{I}}_{\mathrm{direct}}(\mathrm{GE})$

Range of the constraint dictionary defined directly on graph entry $\mathrm{GE}$.

${\mathcal{I}}_{\mathrm{active}}(\mathrm{GE})$

Direct constraints of graph entry $\mathrm{GE}$ together with constraints of its constraining graph type, when present.

$\mathrm{Sch}$

Schema state extracted from the catalog for the schema-evolution model.

$\mathrm{absent}$

Sentinel for the absence of a property; it is not a GQL value.

$\mathrm{CDesc}$

Carrier of key- and unique-constraint descriptors.

$\chi =⟨P,\stackrel{}{c¯}⟩$

Key specification: deterministic constraint graph pattern and key value component sequence.

$t_{\chi }(b)$

Key tuple obtained from binding $b$ according to key specification $\chi$.

$\approx$

Recursive GQL not-distinct relation on values and, pointwise, key tuples.

$\mathrm{nullContaining}(v)$

Predicate that value $v$ recursively contains the null value.

$\mathrm{CBNF}(C),\mathrm{CSNF}(S)$

Deterministic normal forms of constraint body $C$ and complete constraint specification $S$.

$\sigma \mathsf{storeAssignableTo}\tau$

Applicable GQL store-assignment compatibility check from source type $\sigma$ to target type $\tau$.

${\mathrm{\Sigma }}_{\mathrm{typing}}({\mathrm{GT}}^{?})$

Graph-type-conformance clause for an optional constraining graph-type reference.

$⟦\mathrm{GE}⟧$

Graph-type-conformance clause and direct key/unique constraints of graph entry $\mathrm{GE}$.

$\mathcal{T}$

Finite typing environment for binding variables in the effect judgments.

$𝔈$

Carrier of static effects.

${𝜀}_{\mathrm{eff}}$

Static effect set; the empty effect denotes write-purity in this metamodel.

$e_{\mathrm{eff}}$

Primitive effect element.

$\mathrm{\Sigma };\mathcal{T}⊢S:{𝜀}_{\mathrm{eff}}$

Effect typing judgment for a query or data-modifying statement.

$\mathrm{ok}$

Meta-level well-formedness judgment for primitive actions.

$\mathrm{peff}(a)$

Primitive-effect extractor for an action $a$.

${\bigsqcup }_{\mathrm{eff}},{\bigsqcup <!--\; FUNCTION\; APPLICATION\; -->}_{\mathrm{eff}}$

Binary and finite indexed joins in the effect algebra.

$e_1{\le }_{\mathrm{eff}}{e}_2$

Effect ordering: $e_2$ is a less specific abstraction of $e_1$.

$\mathrm{MayConflict}({𝜀}_{\mathrm{eff},1},{𝜀}_{\mathrm{eff},2})$

Static conflict-approximation predicate between effects.

${\top <!--\; FUNCTION\; APPLICATION\; -->}_{\Lambda }$

Unknown or unconstrained label-set abstraction.

$\mathrm{CreateV}[{\Lambda }_V]$

Primitive effect: create a vertex (with label-set parameter $\Lambda$).

$\mathrm{DeleteV}[{\Lambda }_V]$

Primitive effect: delete a vertex (with label-set parameter $\Lambda$).

$\mathrm{CreateE}[{\Lambda }_E]$

Primitive effect: create an edge (with label-set parameter ${\Lambda }_E$).

$\mathrm{DeleteE}[{\Lambda }_E]$

Primitive effect: delete an edge (with label-set parameter ${\Lambda }_E$).

$V,E$

Sort tags: vertex/edge (used in effect constructors).

$\mathrm{Set}(X,k)$

Primitive effect: set property $k$ on sort $X\in \{V,E\}$.

$\mathrm{ClearProps}(X)$

Primitive effect: clear all properties on sort $X\in \{V,E\}$.

$\mathrm{RemProp}(X,k)$

Primitive effect: remove property $k$ on sort $X\in \{V,E\}$.

$\mathrm{AddLbl}(X,\ell )$

Primitive effect: add label $\ell$ on sort $X\in \{V,E\}$.

$\mathrm{RemLbl}(X,\ell )$

Primitive effect: remove label $\ell$ on sort $X\in \{V,E\}$.

$\mathcal{K}$

Implementation configuration record (implementation-defined choices).

$G_{\mathrm{cur}}$

Current working graph in data-modification rules; distinct from the acronym CG (Conceptual Graph).

${\mathrm{RefTy}}_V,{\mathrm{RefTy}}_E$

Reference value types for nodes/edges (implementation-defined).

${\mathrm{LabMin}}_V,{\mathrm{LabMax}}_V$

Supported min/max node-label counts.

${\mathrm{LabMin}}_E,{\mathrm{LabMax}}_E$

Supported min/max edge-label counts.

${\mathrm{PropMax}}_V,{\mathrm{PropMax}}_E$

Supported maximum property counts for nodes/edges.

$\mathrm{\Delta }$

Coalesced update delta of compatible primitive mutations.

$\oplus$

Apply a delta to a graph/store state (state update operator).

$\mathrm{insNode}(v,\Lambda ,P)$

Primitive mutation: insert node $v$ with labels $\Lambda$ and properties $P$.

$\mathrm{delNode}(v)$

Primitive mutation: delete node $v$.

$\mathrm{insEdge}(e,\Lambda ,P,u,v,d)$

Primitive mutation: insert an edge with labels, properties, endpoints, and directedness $d$.

$\mathrm{delEdge}(e)$

Primitive mutation: delete edge $e$.

$\mathrm{setPropV},\mathrm{setPropE}$

Grounded setters for vertex/edge properties (template grounding).

$\mathrm{clearPropsV},\mathrm{clearPropsE}$

Grounded operations that clear all vertex/edge properties for a set-all-properties item.

$\mathrm{delPropV},\mathrm{delPropE}$

Grounded deleters for vertex/edge properties (template grounding).

$\mathrm{addLabelV},\mathrm{addLabelE}$

Grounded add-label operations (vertex/edge).

$\mathrm{delLabelV},\mathrm{delLabelE}$

Grounded remove-label operations (vertex/edge).

${\mathrm{ground}}_{\mu }(\cdot )$

Grounding of an update atom by evaluating expressions under binding $\mu$.

${\mathrm{WS}}_{\mu }(U)$

Per-binding write-set (list of grounded operations produced by template $U$ under $\mu$).

${\mathrm{\Delta }}_U:={⊞<!--\; FUNCTION\; APPLICATION\; -->}_{\mu \in \mathcal{M}}{\mathrm{WS}}_{\mu }(U)$

Staged delta obtained by folding the write-set coalescer over bindings.

$⊞$

Deterministic partial write-set coalescer, distinct from bag union and diagnostic disjoint sum.

${\mathrm{ok}}_{\mathrm{GE}}(G,\mathrm{\Delta })$

Predicate that the post-state satisfies the graph’s direct constraints and conforms to its constraining graph type, when present.

$\mathrm{PDesc}$

Compact lookup-augmented representation $⟨p,\stackrel{}{x_j:{\tau }_j¯},\stackrel{}{x_m^{\prime }:{\tau }_m^{\prime }=d_m¯},{\tau }_{\mathrm{res}},\mathrm{kind}⟩$ of a named-procedure catalog entry.

$\mathrm{BT}⟨\stackrel{}{z_i:{\upsilon }_i¯}⟩$

Material procedure binding-table result type with named, typed result fields.

${\tau }_{\mathrm{res}}$

Procedure result type; for a CALL-statement, a material type $\mathrm{BT}⟨\stackrel{}{z_i:{\upsilon }_i¯}⟩$ or the empty type.

$\stackrel{}{e¯}\mathrm{assignableTo}(\stackrel{}{\tau ¯},\stackrel{}{{\tau }^{\prime }¯})$

Componentwise assignment-compatibility check for actual procedure arguments and mandatory/optional parameter types.

$\mathrm{sig}(\mathrm{PDesc})$

Core procedure signature derived from a named-procedure descriptor.

$\mathrm{Procs}:\mathbb{Q}\rightharpoonup \mathrm{PDesc}$

Catalog projection mapping qualified procedure references to named-procedure descriptors.

${\mathrm{resolve}}_{\mathrm{Proc}}(\mathcal{X},p)$

Resolution of procedure reference $p$ in active context $\mathcal{X}$.

$\mathrm{Tx}=⟨u,\mathrm{iso},\stackrel{}{P¯},\mathrm{SP}⟩$

Transaction: session authorization identifier, isolation choice, sequence of procedure executions, and optional extension state $\mathrm{SP}$ for savepoints outside the GQL core.

$\mathrm{\Delta }(B)$

Update sequence (delta) produced by executing program/block $B$.

$◇$

Ordered composition of deltas.

$\mathrm{Committed}({\mathrm{\Omega }}^{\prime })$

Successful commit outcome with resulting store state ${\mathrm{\Omega }}^{\prime }$.

$\mathrm{RolledBack}(\mathrm{\Omega })$

Successful rollback outcome leaving the original store state.

$\mathrm{Aborted}(\kappa )$

Failed transaction outcome carrying status code $\kappa$.

${\mathrm{\Omega }}_{\mathrm{init}},{\mathrm{\Omega }}_{\mathrm{final}}$

Initial/final store states in a serializability argument.

$\rho$

Permutation witnessing serializability of committed transactions.

${\mathrm{\Omega }}_i^{\mathrm{base}}$

Base store state visible to statement $S_i$; snapshot selection outside the serializable core is implementation-defined.

${\mathrm{\Delta }}_{<i}={\mathrm{\Delta }}_1◇\cdots ◇{\mathrm{\Delta }}_{i-1}$

Transaction-local cumulative delta preceding statement $S_i$.

${\mathrm{\Omega }}_i^{\mathrm{vis}}={\mathrm{\Omega }}_i^{\mathrm{base}}\oplus {\mathrm{\Delta }}_{<i}$

Store state read by statement $S_i$.

$\mathit{𝔸𝕀𝔻}$

Universe of authorization identifiers.

$\mathit{ℝ𝕆𝕃𝔼}$

Universe of roles.

$\mathit{𝕆𝔹𝕁}$

Universe of authorization targets (complete catalog or data objects in the core model).

$\mathit{\mathbb{P}ℝ𝕀𝕍}$

Universe of privileges; modeled as a finite poset.

$⟨\mathit{\mathbb{P}ℝ𝕀𝕍},\le ⟩$

Privilege poset (dominance order).

$\bigsqcup <!--\; FUNCTION\; APPLICATION\; -->P$

Join (least upper bound) of a finite privilege set $P\subseteq \mathit{\mathbb{P}ℝ𝕀𝕍}$.

$\mathcal{Z}$

Authorization state (set of role/grant facts).

$\mathrm{hasRole}(u,r)$

Fact: authorization identifier $u\in \mathit{𝔸𝕀𝔻}$ has role $r$.

$\mathrm{grant}(g,x,\varpi ,o)$

Fact: grantor $g$ grants privilege $\varpi$ on object $o$ to grantee $x$.

$\mathrm{eff}(u,o)$

Effective privilege of authorization identifier $u$ on object $o$.

$\Theta ;𝔖⊢S:\tau ⊳{\mathrm{\Pi }}_S$

Authorization typing judgment producing privilege obligations, with binding and static schema/type contexts.

${\mathrm{\Pi }}_S\subseteq \mathit{\mathbb{P}ℝ𝕀𝕍}\times \mathit{𝕆𝔹𝕁}$

Obligation set (required privileges on objects).

$(u,o)\in \mathrm{available}$

Complete GQL-object $o$ is available to authorization identifier $u\in \mathit{𝔸𝕀𝔻}$.

$\mathrm{txMode}$

Current transaction access mode, $\mathrm{RO}$ or $\mathrm{RW}$.

${\varpi }_{\mathit{match}},{\varpi }_{\mathit{insert}}$

Representative privilege tokens used in obligation rules (match/insert).

$\mathrm{Err}$

Carrier of abstract exception-condition tokens.

$e_{\mathrm{err}}\in \mathrm{Err}$

Exception-condition token used by the diagnostic metamodel.

$\mathrm{GQLStatus}$

Opaque carrier of GQL-status objects.

$\zeta ,\stackrel{}{\zeta ¯}$

Primary GQL-status object and finite list of additional GQL-status objects.

$\mathrm{Fail}(e_{\mathrm{err}},\zeta ,\stackrel{}{\zeta ¯})$

Failed outcome: exception condition and status objects, with no result.

$\coprod$

Disjoint sum used in diagnostic result domains.

$\mathrm{RegularResult}=𝕍\coprod \mathrm{BT}$

Carrier of regular results: values or binding tables.

$\mathrm{Result}=\mathrm{RegularResult}\coprod \{\mathrm{omitted}\}$

Carrier of regular and omitted results.

$\mathrm{Succ}=\{\mathrm{Ok}(R,\zeta ,\stackrel{}{\zeta ¯})\mid R\in \mathrm{Result}\}$

Carrier of successful outcomes with their result and status objects.

$\mathrm{Res}=\mathrm{Succ}\coprod \mathrm{Fail}$

Execution-outcome carrier combining successful and failed outcomes.

$\mathit{ℂℍ}$

Alphabet of status-code characters.

$\mathit{ℂ𝕃𝔸𝕊𝕊}$

Status “class” strings (length 2).

$\mathit{𝕊𝕌𝔹ℂ𝕃𝔸𝕊𝕊}$

Status “subclass” strings (length 3).

$\mathit{𝕊𝕋𝔸𝕋𝕌𝕊}\subseteq {\mathit{ℂℍ}}^5$

Status-code space (GQLSTATUS codes).

$\kappa \in \mathit{𝕊𝕋𝔸𝕋𝕌𝕊}$

A status code identifying a condition.

${\kappa }_{\mathrm{ok}},{\kappa }_{\mathrm{ok}\text{\_}\mathrm{omitted}}$

Status codes 00000 (successful completion with a regular result) and 00001 (successful completion with an omitted result).

${\kappa }_{\mathrm{warning}},{\kappa }_{\mathrm{no}\text{\_}\mathrm{data}}$

Status codes 01000 (completion with a warning) and 02000 (completion with an empty result).

$\cdot$

String concatenation.

$\kappa =c_{\kappa }\cdot s_{\kappa }$

Unique factorization into class and subclass parts.

$\mathrm{class}(\kappa )$

Extract class part of status code $\kappa$.

$\mathrm{subclass}(\kappa )$

Extract subclass part of status code $\kappa$.

$\mathrm{cat}(\kappa )$

Category function for status codes.

$S,W,N,I,X$

Status categories (successful, warning, no-data, informational, exception), as used by $\mathrm{cat}(\kappa )$.

${\mathit{𝕊𝕋𝔸𝕋𝕌𝕊}}_{\mathrm{compl}}$

Completion-condition code subset.

${\mathit{𝕊𝕋𝔸𝕋𝕌𝕊}}_{\mathrm{exc}}$

Exception-condition code subset.

${\mathit{𝕊𝕋𝔸𝕋𝕌𝕊}}_{\mathrm{info}}$

Informational-condition code subset.

${\mathit{𝕊𝕋𝔸𝕋𝕌𝕊}}_{\mathrm{std}}$

Standard-assigned status-code subset.

${\mathit{𝕊𝕋𝔸𝕋𝕌𝕊}}_{\mathrm{impl}}$

Implementation-defined status-code subset.

$\mathrm{code}:\mathrm{Err}\to {\mathit{𝕊𝕋𝔸𝕋𝕌𝕊}}_{\mathrm{exc}}$

Total mapping from error tokens to exception-condition GQLSTATUS codes.

$\mathrm{NLOGSPACE},\mathrm{NP}$

Nondeterministic logarithmic-space and nondeterministic polynomial-time classes.

$\mathrm{PTIME},\mathrm{PSPACE}$

Polynomial-time and polynomial-space classes.

$2\mathrm{EXPTIME}$

Double-exponential-time complexity class.

$\mathcal{A}\mathcal{L}\mathcal{C}\mathcal{I}$

Description logic $\mathcal{A}\mathcal{L}\mathcal{C}$ extended with inverse roles.

$\mathcal{A}\mathcal{L}\mathcal{C}\mathcal{Q}$

Description logic $\mathcal{A}\mathcal{L}\mathcal{C}$ extended with qualified number restrictions.

$\mathcal{A}\mathcal{L}\mathcal{C}\mathcal{Q}\mathcal{I}$

Description logic $\mathcal{A}\mathcal{L}\mathcal{C}$ extended with qualified number restrictions and inverse roles.

$\#\mathrm{Datalog}$

Fully compositional graph-to-graph language used in the cited extension proposal.