arXiv:2604.11454v1 [cs.DB] 13 Apr 2026
Foundations of the GraphAlg Language Daan de Graaf
Robert Brijder
Nikolay Yakovets
Abstract The GraphAlg domain-specific language for graph algorithms enables user-defined algorithms in graph databases. In this work we show how GraphAlg is built on top of the formal MATLANG language for matrix manipulation. Starting from MATLANG, we describe the extensions to MATLANG needed to derive GraphAlg Core, a simplified version of GraphAlg that is used as the internal representation in the GraphAlg compiler. Furthermore, we prove that any GraphAlg Core expression can be simulated in an extension of for-MATLANG that supports simultaneous induction.
1
Introduction
Graph algorithms are key components in many analytical workloads over graph data. Despite graph databases being the natural home for such data, typical graph query languages such as Cypher [6] or GQL [10] are unable to express algorithms such as PageRank or Weakly Connected Components, forcing users to export their graph data and process it in external tools. To bring user-defined algorithm support to graph databases, the GraphAlg language has been proposed [9]. GraphAlg is a domain-specific language for writing graph algorithms in the language of linear algebra. It is specifically designed to be embedded in databases: the GraphAlg compiler transforms programs into an extended relational algebra that can be executed by an existing relational query processing engine with minimal changes. The design of GraphAlg is based on MATLANG [1], a formal language for matrix manipulation. The MATLANG language follows a principled and minimal design suitable for high-level optimization, with an established connection to relational algebra [2], making it an ideal starting point for GraphAlg. In this work we describe and motivate a number of extensions to MATLANG for expressing a diverse set of graph algorithms, each adding a small feature to the previous extension, to eventually arrive at the GraphAlg Core language, a simplified version of the ‘full’ GraphAlg language. The GraphAlg compiler uses GraphAlg Core as its internal representation for GraphAlg programs, performing various analyses and optimizations such as constant propagation and sparsity analysis [4]. By formalizing the connection between GraphAlg Core and MATLANG, results from existing studies of MATLANG can be leveraged for GraphAlg. For
1
example, MATLANG has been shown to correspond to a natural fragment of relational algebra [2]. We establish in this work that GraphAlg Core expressions can be simulated in an extension of for-MATLANG that supports simultaneous induction (Corollary 1), suggesting that loop-free GraphAlg Core expressions translate to relational algebra. Indeed, we implement this exact translation in the GraphAlg compiler. Simultaneous Induction. Many graph algorithms require iteration, which is the primary reason that Cypher and GQL (language without loops or recursion) are insufficient. While iteration support in MATLANG has been previously studied [7, 8], the proposed extensions only allow a single matrix value to be carried over between loop iterations. Various graph algorithms, however, are naturally expressed using multiple state variables carried over between loop iterations, also called simultaneous induction. Our proposed extension sifor-MATLANG, based on for-MATLANG [8], adds support for simultaneous induction to MATLANG. Leader Election and Loop Decomposition. Another important problem in graph analytics is the selection of a representative vertex from a set, also called leader election. We observe that while MATLANG has no specific leader election operation, it can be simulated in sifor-MATLANG using the powerful loop construct. Conversely, if we do add a leader election primitive to the language, then the loop construct is unnecessarily powerful. We propose an extension that decomposes the expressive power of the sifor-MATLANG loop construct into two orthogonal constructs. The resulting dec-MATLANG language has simpler individual operations and can naturally express leader election, yet it has the same expressive power as sifor-MATLANG. Multiple Semirings. The next issue we face is that MATLANG expressions operate over a fixed semiring, while the natural semiring to use depends on the specific algorithm. Complex algorithms can even use multiple semirings at different stages, requiring casting of values between different semirings. We propose muse-MATLANG, an extension of dec-MATLANG that allows using multiple semirings within an expression. We find that, perhaps counterintuitively, this extension does not increase the expressive power of the language: museMATLANG and dec-MATLANG (and therefore also sifor-MATLANG) have equal expressive power. Executable Specification. The MATLANG language and its extensions mentioned above are all formal languages: some details of the languages are irrelevant to theoretical analysis, and are therefore only loosely defined. In particular, MATLANG does not specify the set Ω of allowed pointwise functions, or which semirings may be used. To create an executable specification of museMATLANG, we fix a particular Ω through a grammar, and define a set of semirings that is broad enough to support many graph algorithms. The resulting
2
language is GraphAlg Core, the small subset of GraphAlg that is used in the GraphAlg compiler for optimization. The remainder of this paper is organized as follows. In Section 2 we recall the definition of MATLANG, as well as the extension for-MATLANG that adds iteration in the form of a loop construct. Section 3 defines sifor-MATLANG, which adds simultaneous induction. In Section 4 we decompose this loop construct to obtain dec-MATLANG. Next, Section 5 proposes muse-MATLANG, allowing multiple semirings to be used within a single expression. We also show that muse-MATLANG and dec-MATLANG have equal expressive power. Finally, in Section 6 we introduce GraphAlg Core, fixing Ω and the set of supported semirings.
2
Preliminaries
We start by recalling MATLANG [1], followed by its extension for-MATLANG [8].
2.1
MATLANG
MATLANG is a formal language for matrix manipulation using common matrix operations and linear algebra. Previous work on MATLANG has studied its expressive power [1] and connection to relational algebra [2]. We assume a countably infinite set of matrix variables V that serve as the inputs to MATLANG expressions. We also assume a repertoire Ω of functions f : Rk → R, where R is a semiring. While we make no assumptions about R, previous works have used the complex numbers [1] or the real numbers [8] for R. The syntax of MATLANG expressions is defined by the following grammar: e ::= M ∈ V
(matrix variable)
|
T
e
(transpose)
|
1(e)
(one-vector)
|
diag(e)
(diagonalization of a vector)
|
e1 · e2
(matrix multiplication)
|
apply[f ](e1 , . . . , ek )
(pointwise application, f ∈ Ω)
The definition of MATLANG in [1] also includes a let binding expression let M = e1 in e2 for convenience. As noted in [1], this operation can be omitted without affecting the expressive power of the language, so we omit it from our definition. Type System We now recall the type system for MATLANG from [1]. We assume a sufficient supply of size symbols, denoted α, β, γ, that represent the number of rows or columns of a matrix (e.g., α × β). Together with an explicit 1, we can express 3
column vectors (α × 1), row vectors (1 × β) and scalars (1 × 1). A size term is either a size symbol or an explicit 1. Formally, a type is an ordered pair of size terms s1 and s2 , denoted s1 × s2 . A schema S is a function defined over a finite set of matrix variables M ⊂ V that assigns a type to each element of M. By S[M := α × β] we denote the schema obtained from S by mapping M to α × β. The type of an expression e with respect to a schema S, if it exists, is denoted by typeS (e). It is inductively defined as follows: • typeS (M ) := S(M ), for a matrix variable M ∈ M; • typeS (eT ) := β × α if typeS (e) = α × β; • typeS (1(e)) := α × 1 if typeS (e) = α × β; • typeS (diag(e)) := α × α, if typeS (e) = α × 1; • typeS (e1 · e2 ) := α × γ if typeS (e1 ) = α × β, and typeS (e2 ) = β × γ; • typeS (apply[f ](e1 , . . . , ek )) := α × β, if typeS (ei ) = α × β for all i ∈ {1, . . . , k} and f ∈ Ω. We call an expression e well-typed according to the schema S if typeS (e) exists. Semantics We denote the dimensions of a matrix A by dim(A) = m × n. An instance I over a schema S is a pair of functions I = (D, mat), where D maps size terms to matrix dimensions, and mat assigns a concrete matrix to each matrix variable M ∈ M, such that dim(mat(M )) = D(α) × D(β) if typeS (M ) = α × β. We use the notation I(M ) as a shorthand for mat(M ). By I[M := A] we denote the instance obtained from I by mapping matrix variable M to value A. We write (I[M1 := A])[M2 := B] as I[M1 := A, M2 := B]. The evaluation of an expression e with respect to an instance I, denoted by JeK(I), is inductively defined as: • JM K(I) := I(M ), for M ∈ M;
• JeT K(I) := JeK(I)T , which is the transpose of JeK(I);
• J1(e)K(I) is an m × 1 vector with value 1 at all positions, where JeK(I) is an m × n matrix; • Jdiag(e)K(I) is a matrix with the vector JeK(I) on its main diagonal, and zero in every other position; • Je1 · e2 K(I) := Je1 K(I) · Je2 K(I);
• Japply[f ](e1 , . . . , ek )K(I) is a matrix A of the same dimensions as Je1 K(I), and where Aij has the value f (Je1 K(I)ij , . . . , Jek K(I)ij ) 4
2.2
For-MATLANG
The language for-MATLANG [8] extends MATLANG by a construct that we call the canonical for loop. Its syntax is as follows: for v, X. e
(canonical for loop, with v, X ∈ V)
The associated typing rule is defined as: typeS (for v, X. e) := typeS (e), if typeS (e) = typeS (X) and typeS (v) = γ × 1 Let bni be the vector of dimension n with value 1 at position i and zero at all other positions. Such a vector is called canonical. Assuming I(v) is an n × 1 vector, Jfor v, X. eK(I) is defined iteratively as follows: • Let A0 be the zero matrix of the same size as I(X). • For i ∈ {1, . . . , n}, Ai := JeK(I[v := bni , X := Ai−1 ]). • Finally, Jfor v, X. eK(I) := An .
Intuitively, this loop construct repeatedly updates state variable X by evaluating e, where e is allowed to refer to the previous state of the loop as X. Additionally, e may refer to the canonical vector v. In the first iteration, v takes on value bn1 , in the second iteration bn2 , etc. We can define a variant of the above loop construct that initializes X to an arbitrary expression e0 rather than A0 . This variant, denoted for v, X := e0 . e, has the same expressive power as the zero-initialized loop construct[8].
3
Adding Simultaneous Induction
Many algorithms are naturally expressed using loops that update multiple state variables, also known as simultaneous induction. Simultaneous induction is usually supported in programming languages and in certain query languages [3]. For example, consider that a typical breadth first search algorithm requires keeping three pieces of state: 1. A queue of vertices to be visited; 2. The vertices that have been visited so far; and 3. The depth at which each vertex was first visited (or alternatively, a pointer to the parent vertex). The language for-MATLANG, however, only allows a single matrix to be carried from one iteration of a loop to the next. The lack of simultaneous induction makes it difficult, if not impossible, to express various commonly used algorithms in for-MATLANG. We discuss the implications for the expressive power of for-MATLANG in detail in Section 3.1. 5
We propose an extension of for-MATLANG, named ‘sifor-MATLANG’, that supports simultaneous induction. The sifor-MATLANG language is obtained from for-MATLANG, by modifying the loop definition to allow multiple loop variables: for v, {M1 := e′1 , . . . , Mm := e′m }(e1 , . . . , em ) The typing rule is modified accordingly: typeS (for v, {M1 := e′1 , . . . , Mm := e′m }(ed , e1 , . . . , em )) := τ1 , if τi := typeS (ei ) = typeS ′ (e′i ) for all i ∈ {1, . . . , m}, where S ′ := S[M1 := τ1 , . . . , Mm := τm ] and typeS (v) = γ × 1. Assuming that I(v) is an n × 1 vector, the semantics of the loop are defined iteratively as follows: • Let I0 := I[v := bn1 , M1 := Je1 K(I), . . . , Mm := Jem K(I)]
• For i ∈ {1, . . . , n}, let Ii := Ii−1 [v := bni+1 , M1 := Je′1 K(Ii−1 ), . . . , Mm := Je′m K(Ii−1 )]. • Finally, Jfor v, {M1 := e′1 , . . . , Mm := e′m }(e1 , . . . , em )K(I) := In (M1 ).
The loop body defines a number of loop variables m ≥ 1 that each consist of a binding variable Mi and a body expression e′i . Intuitively, before entering the loop, the binding variables are initialized as Mi := ei . Evaluation of the loop is similar to for-MATLANG, each time updating the binding variables with the results of the body expressions. The loop produces a single result matrix, which is the final value of M1 . The sifor-MATLANG language subsumes for-MATLANG. Lemma 1. The loop construct of for-MATLANG can be simulated using the loop construct of sifor-MATLANG. The above lemma follows directly from the following rewrite rule: for v, X := e0 . e ⇒ for v, {X := e}(e0 )
3.1
Does sifor-MATLANG Strictly Subsume for-MATLANG?
Adding simultaneous induction to a language does not always increase its expressive power. In first-order logic, for example, simultaneous induction can be simulated with induction on a single predicate [5, Chapter 8.2]. In this subsection we provide evidence to support the hypothesis that sifor-MATLANG indeed has greater expressive power than for-MATLANG. We consider possible strategies for simulating simultaneous induction with a single loop variable, and show that none of them are applicable to for-MATLANG. We use the following simple recurrence as an example, which assumes two arbitrary input matrices A and B:
6
C0 = A C1 = B Ci = Ci−2 · Ci−1 Encoding this recurrence in for-MATLANG would require the simulation of simultaneous induction, because the value of Ci relies on the value of two previous loop states Ci−2 and Ci−1 . For such a simulation to work, Ci−2 and Ci−1 must be encoded into a single matrix without loss of information. Below we consider different strategies for combining two matrices A and B into one, and show that none of them can be applied to for-MATLANG. Additional Attributes. In relational algebra, relations can have arbitrary arity. For the recurrence above, matrices A and B can be stored in relations with attributes (r, c, a) and (r, c, b), respectively. To combine the two, we can simply create a table with four attributes (r, c, a, b). In relational algebra, simultaneous induction therefore does not increase expressivity. Given that for-MATLANG has the same expressivity as a particular fragment of relational algebra [2], one might assume that the same holds in for-MATLANG. Crucially, however, in for-MATLANG the matrix type limits us to arity 3 [2], so the strategy of using additional attributes does not carry over to for-MATLANG. Matrix Concatenation. One might wonder whether in for-MATLANG two m × n matrices can be concatenated to form a single 2m × n (or m × 2n) matrix. However, given the type rules of for-MATLANG it is apparent that such a matrix cannot be constructed. Consider a schema S with a mapping for two matrix variables S[A := α × β] and S[B := γ × δ]. Then the only possible values of typeS (e) for arbitrary e are combinations of α, β, γ, δ and 1. Matrices must be constructed in terms of the dimensions of the inputs, and therefore concatenation of arbitrary matrices is impossible. Pairing. Two matrices A and B can be encoded in a single matrix using a pairing function π : R × R → R that maps each pair of elements (Aij , Bij ) into a distinct value. If π is an injective mapping, then applying π to matrices A and B gives a single matrix C from which both A and B can be recovered using the retraction of π. For finite semirings, however, it is easy to show that π cannot be injective. Let R be a finite semiring with cardinality |R|. Then there are |R|2 distinct values in the domain of π, but only |R| in the co-domain, which is insufficient to map each pair (Aij , Bij ) to a distinct value. The implications of this are especially damning for a software implementation of for-MATLANG, which would need to operate over fixed-size data types for performance. None of the strategies described above succeed in simulating simultaneous induction in for-MATLANG. This supports the hypothesis that because of its 7
support for simultaneous induction, the expressive power of sifor-MATLANG is indeed greater than for-MATLANG.
4
Decomposing the Loop Construct
The loop construct in sifor-MATLANG can be replaced by two natural constructs: A simpler loop definition without canonical vectors, as has been previously proposed in the context of MATLANG [7] and query languages in general [3], and an additional operation pickAny, a type of aggregation in relational algebra, that is independently useful for tasks such as leader election. This decomposition also has further advantages, which we discuss at length in Section 4.1. Before giving the loop definition, we first define the typing rule and semantics of the pickAny construct: typeS (pickAny(e)) := typeS (e) The expression pickAny(e) keeps the non-zero element with minimal column index of each row in e, setting all other entries to zero: JpickAny(e)K(I) is a matrix A of the same size as JeK(I), and where Aij is JeK(I)ij if JeK(I)ik = 0 for all k < j, and 0 otherwise.
For the updated loop construct, we drop the canonical vector v, and instead use an input expression ed to determine the number of iterations that the loop should run: for {M1 := e′1 , . . . , Mm := e′m }(ed , e1 , . . . , em ) The updated typing rule is as follows: typeS (for {M1 := e′1 , . . . , Mm := e′m }(ed , e1 , . . . , em )) := τ1 , if τi := typeS (ei ) = typeS ′ (e′i ) for all i ∈ {1, . . . , m}, where S ′ := S[M1 := τ1 , . . . , Mm := τm ] and typeS (ed ) = γ × 1. Assume that Jed K(I) is an n × 1 vector. The semantics are almost identical, except that Ii does not include a matrix variable mapping to a canonical vector: • Let I0 := I[M1 := Je1 K(I), . . . , Mm := Jem K(I)]
• For i = {1, . . . n}, let Ii := Ii−1 [M1 := Je′1 K(Ii−1 ), . . . , Mm := Je′m K(Ii−1 )].
• Finally, Jfor {M1 := e′1 , . . . , Mm := e′m }(ed , e1 , . . . , em )K(I) := In (M1 ).
We denote the language obtained from sifor-MATLANG by simplifying the loop construct and adding pickAny as dec-MATLANG. It turns out that these changes do not affect the expressive power of the language. Theorem 1. Languages sifor-MATLANG and dec-MATLANG have equal expressive power.
8
Proof. We give constructions showing that: (1) The loop construct of siforMATLANG can be expressed in dec-MATLANG; (2) The loop construct of decMATLANG can be expressed in sifor-MATLANG; and (3) The pickAny construct of dec-MATLANG is expressible in sifor-MATLANG. Simulating sifor-MATLANG loops in dec-MATLANG. The rewrite rule below shows how loops with canonical vectors as they appear in sifor-MATLANG can be expressed in dec-MATLANG. for v, {M1 := e′1 , . . . , Mm := e′m }(e1 , . . . , em ) ⇒ for { M1 := e′1 , . . . , Mm := e′m v := pickAny(V − v T )T V := V − v T }( v, e1 , . . . , e m , pickAny(1(v)T )T , 1(v)T ) The rewrite introduces two additional loop variables v and V , where v stores the current canonical vector, while V tracks which canonical vectors have been observed in previous iterations (corresponding to the zero values). Variable V must not appear in {M1 , . . . , Mm }. Because V is countably infinite, we can always find such a V . The input expressions to the loop initialize these as v := pickAny(1(v)T )T = [1 0 · · · 0]T and V := 1(v)T = [1 · · · 1]. After the first iteration, the variables are updated to v := pickAny(V − v T )T = [0 1 0 · · · 0]T and V := V − v T = [0 1 · · · 1], and so on. Simulating dec-MATLANG loops in sifor-MATLANG. dec-MATLANG loops are a simplification of sifor-MATLANG loops, which makes rewriting them to sifor-MATLANG trivial:
for
{M1 := e′1 , . . . , Mm := e′m }(v, e1 , . . . , em ) ⇒
for v,{M1 := e′1 , . . . , Mm := e′m }(
e1 , . . . , e m )
Simulating pickAny in sifor-MATLANG. pickAny(A) can be simulated using the for loop with canonical vectors of for-MATLANG (and by extension also in sifor-MATLANG). Let f ∈ Ω be the pointwise function defined as: ( p d=0 f (y, d, p) = y d ̸= 0 Then pickAny(A) can be simulated as:
9
pickAny(A) ⇒ let v = 1(A) in let w = 1(AT ) in let X = A in let Y = wT in let B = w · wT in for v, X. let R = v T · A in let F = for w, Y . let D = Y · B in let P = R · diag(w) in apply[f ](Y, D, P ) X +v·F Initial values are assigned to v, w, X, Y only to define their dimensions, as this is needed for type checking the for loops. The outer loop for v, X iterates over the input rows, while for w, Y iterates over the columns. Y contains the (partial) result for input row R. In the inner loop, we first detect (D) if we already have a value for the current row. This uses the matrix B, which broadcasts any nonzero value in Y to all positions in D. Then, we take the proposed (P ) value at position (v, w) in A, setting all other values to zero. Finally, the apply either picks the proposed value p if there is no value yet for the current row, or the existing value y otherwise. Other Language Constructs. All other language constructs from siforMATLANG and dec-MATLANG exist in both languages with the same semantics. Combining this with the rewrite rules derived above, we conclude that any welltyped sifor-MATLANG expression can be expressed in dec-MATLANG and vice versa.
4.1
Advantages of Loop Decomposition
A first advantage of the decomposition of the sifor-MATLANG loop construct is that it allows studying the individual contributions of the loop construct and of pickAny. Both the loop construct and the pickAny operation are known from the literature. The fragment of for-MATLANG that omits canonical vectors was first proposed in [7], and a similar loop construct has been defined for relational algebra [3]. The pickAny construct can be naturally expressed in an extension of relational algebra that includes aggregation. Let A be an adjacency matrix, and E the relation with attributes (row, col, value) that describes matrix A. Assuming an aggregate function ARGMIN(a, b) that returns the value a for which b is minimal, the expression pickAny(A) corresponds to the following SQL query: SELECT row, MIN(col), ARGMIN(value, col) FROM E
10
WHERE value <> 0 GROUP BY row Considering that the simulation of pickAny in sifor-MATLANG requires complex constructs such as nested for loops, a translation from a simulated pickAny expression in sifor-MATLANG to efficient relational algebra appears much more challenging. The pickAny operation has uses that go beyond the construction of canonical vectors. Consider the problem of finding weakly connected components in an undirected graph G. Recall that the weakly connected components of G partition the graph into disjoint subgraphs where the vertices within each subgraph are connected. If we pick a representative vertex for each connected component, a solution can be encoded as a function L : V → V that maps each vertex v in the graph to the representative vertex of the connected component of v, where V is the set of vertices of G. Assuming an adjacency matrix A that describes G, an algorithm for finding the weakly connected components is concisely expressed in dec-MATLANG as: WCC(A) = for {X := pickAny(X + (A · X))}(diag(1(A))) Where L(u) = v if WCC(A)uv = 1. The intuition behind this algorithm is as follows: The initial value of X is an identity matrix (written as diag(1(A))), representing the initial assumption that every vertex is in a distinct connected component. Inside the loop, A · X is a one-hop graph traversal step that for each vertex produces the representative vertices of its direct neighbors. The expression pickAny(X + (A · X)) states that for every vertex (i.e., every row), we pick the lowest label (i.e., the lowest column position) that appears among the immediate neighborhood (A · X) or the current label (X). Performing this repeatedly in a loop, the algorithm converges to a labeling X in at most |V | steps. The definition of WCC facilitates a straightforward translation into an extension of relational algebra that can be efficiently executed [9].
5
Semirings
MATLANG expressions operate over a fixed semiring, which in prior work has been the complex [1] or real numbers [8]. If instead we also allow other semirings to be used, thereby changing the semantics of matrix multiplication, we can elegantly express various useful algorithms. Example 1. Assuming the boolean semiring, the following algorithm computes the vertices reachable from a start vertex s in a graph with adjacency matrix A, where S is a column vector with value 1 at Ss and 0 at all other positions. reach(S, A) = for {R := R + (v T · A)T }(S, S) Vector R has value 1 at Ri if vertex i is reachable from s. The algorithm can be modified to compute the shortest paths from s to all other vertices in the graph, 11
simply by switching from the boolean to the tropical min-plus semiring [11]. In this case, Ri is the shortest distance from s to i, or ∞ if there is no path between s and i. Adjacency matrix A contains the edge weights (with ∞ at Auv if there is no edge from u to v). Vector S has value 0 at Ss and ∞ at all other positions. The example above motivates an extension of dec-MATLANG that allows using different semirings for different algorithms. Moreover, it is not difficult to imagine algorithms that use multiple semirings. The label propagation algorithm we implement in [9] defines its inputs and outputs over the integer semiring, but internally performs some operations over a tropical semiring. We show one such case in the example below. Example 2. Consider a vector V in the integer semiring from which we want to extract the maximum value. This is difficult to express in MATLANG and its extensions discussed so far. Summing over all values of V , however, is trivial because it uses the natural addition operator of the integer semiring: sum(V ) = 1(V )T · V If we permit casting values to different semirings, we can leverage that to implement the max function. Let castR→T be a family of functions that change the semiring R of the input value to semiring T . Then the maximum value of a vector V can be expressed as: max(V ) = sum(castZ+,× →Zmax,+ (V )) Vector V is cast from the integer to the tropical max-plus semiring, which uses the max operator for addition. Because of the semiring cast, the sum function computes the maximum instead of the sum.
Adding Multiple Semiring Support to MATLANG Casting does not need to be added as a new language construct. Instead, we generalize the apply construct to allow pointwise functions with different semirings for inputs and outputs. The hypothetical cast operation castR→T (e) from the example above is then expressed as apply[castR→T ](e). This approach does, however, require changing the data model to associate a semiring with each expression and matrix value. Let muse-MATLANG be the language obtained from dec-MATLANG with the following modifications. We assume a nonempty finite set SRing of semirings. In muse-MATLANG a type is an ordered triple s1 × s2 × r, where s1 and s2 are size terms as in MATLANG, and r ∈ SRing is a semiring. To allow pointwise functions that cast between semirings, we define repertoire Ω to be a set of functions f : R1 × · · · × Rk → Ro , where R1 , . . . , Rk and Ro are all (potentially distinct) semirings from SRing. The updated typing rules are presented below: • typeS (M ) := S(M ), for a matrix variable M ∈ M;
12
• typeS (eT ) := β × α × R if typeS (e) = α × β × R; • typeS (1(e)) := α × 1 × R if typeS (e) = α × β × R; • typeS (diag(e)) := α × α × R, if typeS (e) = α × 1 × R; • typeS (e1 · e2 ) := α × γ × R if typeS (e1 ) = α × β × R, and typeS (e2 ) = β × γ × R; • typeS (apply[f ](e1 , . . . , ek )) := α × β × Ro , if typeS (ei ) = α × β × Ri for all i ∈ [1 . . . k] and f : R1 × · · · × Rk → Ro is in Ω; • typeS (pickAny(e)) := α × β × R if typeS (e) = α × β × R; • typeS (for {M1 := e′1 , . . . , Mm := e′m }(ed , e1 , . . . , em )) := τ1 , if τi := typeS (ei ) = typeS ′ (e′i ) for all i ∈ {1, . . . , m}, where S ′ := S[M1 := τ1 , . . . , Mm := τm ] and typeS (ed ) = γ × 1 × Rd . The semantics of muse-MATLANG expressions are as expected. For example, the property that Je1 · e2 K(I) = Je1 K(I) · Je2 K(I) is maintained. The only difference is that where in dec-MATLANG there is one semiring R that defines the addition and multiplication operator (and the additive and multiplicative identities), in muse-MATLANG we use the semiring associated with the input.
Semiring Casting Does Not Add Expressivity Perhaps surprisingly, muse-MATLANG has the same expressive power as decMATLANG. Before proving this, we first define the following helper functions. We use for-MATLANG and sifor-MATLANG style loops with canonical vectors where this aids readability, noting that we have previously shown in Lemma 1 and Theorem 1 that such loops can be rewritten into dec-MATLANG. Function emax(V ) follows the definition given in [8], returning the last canonical vector: emax(V ) = let v = V in let X = V in for v, X. v The converse emin, which returns the first canonical vector, can be defined as emin(V ) = pickAny(1(V )T )T . We also take the definition of ordering matrix S≤ from [8]: 1 1 ··· 1 0 1 · · · 1 .. .. . . . . . 1 0 0 ··· 1 This matrix is obtained by evaluating the following function over a column vector V : 13
S≤ (V ) = let v = V in let X = diag(V ) in (for v, X. X + (X · emax(V ) + v) · v T + v · emax(V )T ) − 1(V ) · emax(V )T Note that S≤ (V ) evaluates to a square matrix whose the dimensions match the number of rows in V . The final subtraction term −1(V ) · emax(V )T is missing in [8], but is required to avoid some elements of the final matrix having value 2 rather than the expected 1. By subtracting the identity matrix, we obtain S< (V ) = S≤ (V ) − diag(1(V )). Based on S< (V ), we can define rotate(V ): rotate(V) = pickAny(S< (V )) + emax(V ) · emin(V )T The expression rotate(V ) evaluates to: 0 1 0 ··· .. . . . .. ... . . .. .. .. . . . .. 0 . 1
0
···
···
0 .. . 0 1 0
With the same dimensions as S≤ (V ). It is a permutation matrix with the property that when it is multiplied with a vector, it cyclically rotates all entries by one position up. For example, given V = [1 2 3]T , we have rotate(V ) · V = [2 3 1]T . Function sum[0, ⊕](V ) generalizes summation of (column) vector V to a scalar value. Parameters are the additive identity 0 and addition operator ⊕. sum[0, ⊕](V ) = let R = rotate(V ) in let X = for { X := apply[⊕](V, R · X) }(V, apply[0](V )) in emax(V )T · X The expression sum[0, ⊕](V ) evaluates to 0 ⊕ V1 ⊕ · · · ⊕ Vn , where V is an n × 1 vector. Repeated multiplication with permutation matrix R followed by element-wise addition ensure that all entries of X contain the sum of values in the vector, i.e., given V = [1 2 3]T we have X = [6 6 6]T . A final multiplication with emax(V )T extracts the last element of X (though since all values are equal, emin(V )T would also work). We are now ready to present the proof that muse-MATLANG has the same expressive power as dec-MATLANG. Recall that for any two sets X and Y , if X has cardinality no greater than Y (|X| ≤ |Y |), then there is an injective function 14
f from X to Y . The retraction g of f is a function from Y to X such that for all x ∈ X we have g(f (x)) = x. Note that if f is injective, then a retraction g exists. Theorem 2. Let e be a well-typed muse-MATLANG expression, and let SRing be the set of semirings used by e. Let T be a semiring in SRing such that for all R ∈ SRing we have |R| ≤ |T |. Then there exists an expression in dec-MATLANG defined over T that is equivalent to e. Proof. Let encR : R → T be an arbitrary injective function from R to T , and decR : T → R a retraction of encR . Let Ω be the pointwise function repertoire used in e, and let f : R1 × · · · × Rk → Ro be in Ω. Then we define: ⟨f ⟩(e1 , . . . , ek ) = enco (f (decR1 (e1 ), . . . , decRk (ek ))) Intuitively, ⟨f ⟩ is an encoded version of f operating in semiring T . Additionally, for any semiring R ∈ SRing, let ⊕R and ⊗R be the addition and multiplication operator of R, respectively. We define the following operators: e1 ⟨⊕R ⟩e2 = encR (decR (e1 ) ⊕R decR (e2 )) e1 ⟨⊗R ⟩e2 = encR (decR (e1 ) ⊗R decR (e2 )) Let ⟨Ω⟩ be the repertoire consisting of: • ⟨f ⟩ for all functions f ∈ Ω; • ⟨⊕R ⟩ and ⟨⊗R ⟩ for all RR ∈ SRing; • A helper function cond, defined as: ( y cond(w, x, y, z) = z
w=x w ̸= x
• A binary operator (−) for which the usual identities 0 − 0 = 1 − 1 = 0 and 1 − 0 = 1 hold. For other input values the behavior may be assumed as arbitrary. Because all functions in ⟨Ω⟩ are defined over T , ⟨Ω⟩ is indeed a repertoire for dec-MATLANG over T . We show that any muse-MATLANG expression can be rewritten into an equivalent dec-MATLANG expression over T with the repertoire ⟨Ω⟩. The proof now proceeds by induction on the structure of expressions. We give rewrite rules of the form OP(e) ⇒ OP′ (⟨e⟩) that describe how to rewrite muse-MATLANG constructs into dec-MATLANG under the induction hypothesis that inner museMATLANG expressions (e in this example) can be rewritten into semantically equivalent dec-MATLANG expressions (⟨e⟩), i.e., JeK(I) = decR (J⟨e⟩K(⟨I⟩)), where e is defined over semiring R, and instance ⟨I⟩ is defined as:
15
⟨I⟩(M ) = encR (A) if I(M ) = A and A is a matrix over semiring R Transpose, Diagonalization and Loops. A first observation is that the semantics of eT , diag(e) and loops is independent of the semirings associated with the inner expressions, and hence the rewrite rules for these expressions are trivial: eT ⇒ ⟨e⟩T diag(e) ⇒ diag(⟨e⟩) for {M1 := e′1 , . . . , Mm := e′m }(ed , e1 , . . . , em ) ⇒ for {M1 := ⟨e′1 ⟩, . . . , Mm := ⟨e′m ⟩}(⟨ed ⟩, ⟨e1 ⟩, . . . , ⟨em ⟩)
Pointwise Function Application. By definition of ⟨f ⟩, the rewrite rule for pointwise function application is defined as: apply[f ](e1 , . . . , ek ) ⇒ apply[⟨f ⟩](⟨e1 ⟩, . . . , ⟨ek ⟩) One-Vector. The expression 1(e) must be rewritten because it would fill the output vector with the multiplicative identity as defined by T , rather than the multiplicative identity of the semiring R (denoted 1R ) over which e is defined. To compensate we rewrite the expression as 1(e) ⇒ apply[λx. encR (1R )](1(⟨e⟩)) pickAny. The semantics of pickAny(e) depend on the additive identity 0R of the semiring R that e is defined over. Let 0T and 1T be the additive and multiplicative identities of semiring T , respectively. Then the rewrite rule is: pickAny(e) ⇒ apply[λv, p. cond(p, 1T , v, encR (0R ))]( ⟨e⟩, pickAny(apply[λv. cond(v, encR (0R ), 0T , 1T )](⟨e⟩))) Intuitively, the inner apply maps zero (according to R) entries in A to 0T , and all other values to 1T . Evaluating pickAny over this matrix returns a matrix with at most one entry per row with value 1T , at the first position where A has a non-zero value. Finally, the outer apply uses the result of pickAny as a mask to select which values from A to preserve, setting the others to 0R . Matrix Multiplication. The rewrite rule for matrix multiplication is nontrivial because it requires simulating an addition and multiplication operator that may be very different from the ones associated with semiring T . We define a helper function cellmul to compute a single value corresponding to Crc of matrix multiplication C = A · B given row Ar and column Bc , parameterized over the additive identity 0, addition operator ⊕ and multiplication operator ⊗:
16
cellmul[0, ⊕, ⊗](e1 , e2 ) = sum[0, ⊕](apply[⊗](eT1 , e2 )) By iterating over the rows of A and the columns of B we can express arbitrary matrix multiplication, computing the entries one by one: rowmul[0, ⊕, ⊗](e1 , e2 ) = let v = 1(eT2 ) in for v { X := let Bc = e2 · v in X + cellmul[0, ⊕, ⊗](e1 , Bc ) · v T }(apply[0](e1 · e2 )) matmul[0, ⊕, ⊗](e1 , e2 ) = let v = 1(e1 ) in for v { X := let Ar = v T · e1 in X + v · rowmul[0, ⊕, ⊗](Ar , e2 ) }(apply[0](e1 · e2 )) The rewrite rule for matrix multiplication e1 · e2 over semiring R is now simply: e1 · e2 ⇒ matmul[encR (0R ), ⟨⊕R ⟩, ⟨⊗R ⟩](⟨e1 ⟩, ⟨e2 ⟩) The above rewrite rules cover all language constructs in muse-MATLANG, and therefore we conclude that for any muse-MATLANG expression there exists an equivalent dec-MATLANG expression.
6
GraphAlg Core
We are now ready to define an instantiation of the muse-MATLANG language (defined in Section 5), called GraphAlg Core. GraphAlg Core is the simplified, or desugared, version of the GraphAlg language. GraphAlg Core not only serves as a vehicle for theoretical analysis: it is also used as an intermediate representation inside the GraphAlg compiler [4]. GraphAlg Core makes precise the following properties of the language that are irrelevant for theoretical analysis, but are necessary for an executable specification: • The repertoire Ω is defined by extending the grammar to include syntax for defining pointwise functions. An expression in this syntax is called a scalar expression. While Ω is not finite, execution platforms only need to support the fixed set of operations included in the syntax to execute arbitrary scalar expressions. • We fix the set of allowed semirings SRing to a number of semirings that are both highly relevant to the implementation of graph algorithms and practical to support across different execution platforms. 17
6.1
Syntax
The GraphAlg Core language syntax is obtained from muse-MATLANG, with the following additional syntax:
f ::=(C1 , . . . , Cn ) e
(pointwise function)
e ::= C
(scalar variable)
| r(l)
(scalar literal)
| e1 {+, ·, −, /, =} e2
(scalar arithmetic)
| cast(r, e)
(scalar cast)
We use the following notation: • e represents a scalar expression • C names a scalar value defined in a pointwise function. • l is a literal value such as 42, 3.14 or ‘true’. • r is a semiring from the set: SRing = {B∨,∧ , Z+,× , R+,× , Zmin,+ , Rmin,+ , Zmax,+ , Rmax,+ } This includes the boolean, integer and real semirings B∨,∧ , Z+,× and R+,× , respectively. For the integers and real numbers, their tropical min-plus and max-plus semirings are included as well. The min-plus semirings define the addition operator as min and multiplication as +, while the max-plus semirings use max and +.
6.2
Type System
The typing rules match those of muse-MATLANG except for apply[f ], where we now also need to check and infer the type of f . typeS (apply[(C1 , . . . , Ck ) e](E1 , . . . , Ek )) := α × β × Ro , if typeS (Ei ) = α × β × Ri for all i ∈ [1 . . . k] and typeSf (e) = 1 × 1 × Ro , where Sf = {C1 := 1 × 1 × R1 , . . . , Ck := 1 × 1 × Rk }; Typing rules for scalar expressions are presented below. Because scalar expressions always produce a 1 × 1 matrix, we write the type as R instead of 1 × 1 × R. • typeS (C) := typeS (C), for a matrix variable C ∈ M; • typeS (r(l)) := r if r ∈ SRing; • typeS (e1 + e2 ) := R if typeS (e1 ) = typeT (e2 ) = R; 18
• typeS (e1 · e2 ) := R if typeS (e1 ) = typeT (e2 ) = R; • typeS (e1 − e2 ) := R if typeS (e1 ) = typeS (e2 ) = R ∈ {Z+,× , R+,× }; • typeS (e1 /e2 ) := R+,× if typeS (e1 ) = typeS (e2 ) = R+,× ; • typeS (e1 = e2 ) := B∨,∧ if typeS (e1 ) = typeS (e2 ) = R; and • typeS (cast(r, e)) := r if r ∈ SRing and typeS (e) = R.
6.3
Semantics
Like the typing rules above, GraphAlg Core largely follows the semantics of muse-MATLANG. The semantics of apply[f ] and scalar expressions are defined as follows: • Japply[(C1 , . . . , Ck ) e](E1 , . . . , Ek )K(I) is a matrix A of the same size as Je1 K(I), and where Aij has the value JeK(Iij ), with Iij = {C1 := JE1 K(I)ij , . . . , Ck := JEk K(I)ij };
• Jr(l)K(I) := l
• Je1 + e2 K(I) := Je1 K(I) ⊕R Je2 K(I), with R the semiring of Je1 K(I). • Je1 · e2 K(I) := Je1 K(I) ⊗R Je2 K(I), with R the semiring of Je1 K(I) • Je1 − e2 K(I) := Je1 K(I) − Je2 K(I) • Je1 /e2 K(I) := Je1 K(I)/Je2 K(I)
• Je1 = e2 K(I) := Je1 K(I) = Je2 K(I)
• Jcast(r, e)K(I) := cast(R, r, JeK(I)), whose definition is given below. Casting Function cast(R, T, v) casts a value from semiring R to semiring T . A key rule in casting is additive identity preservation: If v = 0R , the value after casting is 0T (see the second rule below). This rule takes precedence over all rules that follow it. For the remaining casting rules, only the domain of the semiring is significant. To simplify the rule set, we write for example Z where any semiring over integers is accepted. cast(R, R, v) = v cast(R, r, 0R ) = 0r cast(R, B, v) = 1 if v ̸= 0R cast(B, r, 1) = 1r cast(Z, R, v) = v cast(R, Z, v) = ⌊v⌋
19
Preserving additive identities across casts is an important property for program optimization of matrices with sparse representations. GraphAlg is designed to support efficient execution over sparse matrix representations that store only non-zero elements (values that are not the additive identity). Because of additive identity preservation, casting a sparse matrix to a different semiring only requires updating non-zero elements, because implicit zeros in the input remain zero in the output.
6.4
Relation to MATLANG
We can now formalize the relation between GraphAlg Core and (for-)MATLANG. When for-MATLANG is extended to support simultaneous induction (the language sifor-MATLANG), it is powerful enough to simulate GraphAlg Core expressions. Corollary 1. For any GraphAlg Core expression e, there exists an expression e′ in sifor-MATLANG that simulates e.
sifor-MATLANG ≡ dec-MATLANG ≡ muse-MATLANG ≡ GraphAlg Core (simultaneous induction)
for-MATLANG (for loops)
MATLANG
Figure 1: Expressive-power hierarchy underlying Corollary 1. MATLANG is extended by for-MATLANG (adding a canonical for-loop, Section 2), which is in turn subsumed by sifor-MATLANG (adding simultaneous induction, Section 3). By Theorem 1 and Theorem 2, dec-MATLANG and muse-MATLANG have the same expressive power as sifor-MATLANG. GraphAlg Core (Section 6) instantiates muse-MATLANG with a fixed repertoire Ω and semiring set; the containment chain shown here holds when this instantiation propagates to the other languages as described in Theorems 1 and 2. Proof. By definition of GraphAlg Core, e is a valid muse-MATLANG expression. Then by Theorem 2, there exists an expression e∗ in dec-MATLANG that is equivalent to e. Furthermore, by Theorem 1 there exists an expression e′ in sifor-MATLANG that simulates e∗ . Figure 1 situates these languages in the wider hierarchy built on top of MATLANG.
20
References [1] Robert Brijder, Floris Geerts, Jan Van Den Bussche, and Timmy Weerwag. On the Expressive Power of Query Languages for Matrices. ACM Trans. Database Syst., 44(4):15:1–15:31, October 2019. [2] Robert Brijder, Marc Gyssens, and Jan Van den Bussche. On matrices and K-relations. Annals of Mathematics and Artificial Intelligence, 90(2):181– 210, March 2022. [3] Ashok K. Chandra. Programming primitives for database languages. In Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’81, pages 50–62, New York, NY, USA, January 1981. Association for Computing Machinery. [4] Daan de Graaf. wildarch/graphalg, February 2026. original-date: 2025-1009T14:03:07Z. [5] Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer Monographs in Mathematics. Springer, Berlin, Heidelberg, 1995. [6] Nadime Francis, Alastair Green, Paolo Guagliardo, Leonid Libkin, Tobias Lindaaker, Victor Marsault, Stefan Plantikow, Mats Rydberg, Petra Selmer, and Andrés Taylor. Cypher: An Evolving Query Language for Property Graphs. In Proceedings of the 2018 International Conference on Management of Data, SIGMOD ’18, pages 1433–1445, New York, NY, USA, May 2018. Association for Computing Machinery. [7] Floris Geerts, Thomas Muñoz, Cristian Riveros, Jan Van den Bussche, and Domagoj Vrgoč. Matrix Query Languages. SIGMOD Rec., 50(3):6–19, December 2021. [8] Floris Geerts, Thomas Muñoz, Cristian Riveros, and Domagoj Vrgoč. Expressive Power of Linear Algebra Query Languages. In Proceedings of the 40th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS’21, pages 342–354, New York, NY, USA, June 2021. Association for Computing Machinery. [9] Daan de Graaf, Robert Brijder, Soham Chakraborty, George Fletcher, Bram van de Wall, and Nikolay Yakovets. Algorithm Support for Graph Databases, Done Right, January 2026. arXiv:2601.06705 [cs]. [10] ISO. Information technology — Database languages — GQL, April 2024. [11] Jeremy Kepner and John Gilbert, editors. Graph Algorithms in the Language of Linear Algebra. Software, Environments, and Tools. Society for Industrial and Applied Mathematics, January 2011.
21