pith. sign in

arxiv: 2604.11454 · v1 · submitted 2026-04-13 · 💻 cs.DB · cs.PL

Foundations of the GraphAlg Language

Daan de Graaf , Robert Brijder , Nikolay Yakovets This is my paper

Pith reviewed 2026-05-10 15:50 UTC · model grok-4.3

classification 💻 cs.DB cs.PL
keywords GraphAlgMATLANGgraph algorithmsmatrix manipulationdatabase languagesquery languagessimultaneous inductionsimulation
0
0 comments X

The pith

GraphAlg Core expressions can be simulated using simultaneous induction in an extended for-MATLANG.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes the formal foundations for GraphAlg, a language that lets users define algorithms inside graph databases, by deriving it from the MATLANG language for matrix manipulation. It details the extensions required to produce GraphAlg Core, the simplified form used inside the GraphAlg compiler. The central proof shows that every GraphAlg Core expression has an equivalent form in for-MATLANG once that language is extended with simultaneous induction. This connection matters because it lets properties and results from matrix computation be carried over to graph database algorithms. A reader would care because it supplies a rigorous basis for implementing, verifying, and optimizing user-defined graph algorithms.

Core claim

Starting from MATLANG, the extensions needed to derive GraphAlg Core are described. It is proven that any GraphAlg Core expression can be simulated in an extension of for-MATLANG that supports simultaneous induction.

What carries the argument

The extensions to MATLANG that produce GraphAlg Core together with the simulation of those expressions inside for-MATLANG augmented with simultaneous induction.

If this is right

  • Graph database algorithms can be compiled to equivalent matrix manipulations.
  • Analysis and optimization methods developed for matrix languages become applicable to GraphAlg programs.
  • Correctness of GraphAlg implementations can be checked by appealing to the simulation equivalence.
  • The internal representation used by the GraphAlg compiler rests on a formally justified translation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Matrix-algebra libraries and accelerators could be reused to run GraphAlg programs efficiently.
  • Similar matrix-based foundations may be useful for other database languages that handle graphs or relations.
  • Induction mechanisms in matrix languages could be studied specifically for their power to express graph traversals.

Load-bearing premise

The extensions to MATLANG are sufficient and faithful to capture every essential graph-specific feature of GraphAlg.

What would settle it

A single GraphAlg Core expression for which no equivalent simulation can be written in the version of for-MATLANG that adds simultaneous induction.

Figures

Figures reproduced from arXiv: 2604.11454 by Daan de Graaf, Nikolay Yakovets, Robert Brijder.

Figure 1
Figure 1. Figure 1: Expressive-power hierarchy underlying Corollary 1. [PITH_FULL_IMAGE:figures/full_fig_p020_1.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper claims that GraphAlg, a DSL for user-defined graph algorithms in databases, is founded on the MATLANG matrix manipulation language. Starting from MATLANG, it defines extensions needed to obtain GraphAlg Core (a simplified internal representation used by the GraphAlg compiler) and proves via inductive definitions on syntax and semantics that every GraphAlg Core expression can be simulated in an extension of for-MATLANG supporting simultaneous induction.

Significance. If the simulation result holds, the work provides a rigorous formal bridge between a practical graph-algorithm DSL and an established matrix language, which may support verification, optimization, and semantic analysis of graph computations. The explicit inductive construction and simulation proof constitute a clear strength for a foundations paper in database languages.

major comments (1)
  1. The central simulation theorem (that every GraphAlg Core expression is equivalent to a program in the extended for-MATLANG with simultaneous induction) is load-bearing; the manuscript must demonstrate that the chosen extensions faithfully encode all graph-specific primitives (adjacency, traversal, etc.) without introducing semantic gaps or omitting cases. The inductive argument on syntax and semantics should be checked for completeness across all Core constructs.
minor comments (2)
  1. Clarify the precise relationship between 'MATLANG', 'for-MATLANG', and the 'extension of for-MATLANG' in the abstract and introduction; the terminology appears inconsistent at first reading.
  2. Ensure that the inductive definitions are accompanied by explicit statements of the base cases and the handling of simultaneous induction to aid readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their positive recommendation and for recognizing the value of the simulation result as a formal bridge between GraphAlg and MATLANG. We address the single major comment below.

read point-by-point responses

  1. Referee: The central simulation theorem (that every GraphAlg Core expression is equivalent to a program in the extended for-MATLANG with simultaneous induction) is load-bearing; the manuscript must demonstrate that the chosen extensions faithfully encode all graph-specific primitives (adjacency, traversal, etc.) without introducing semantic gaps or omitting cases. The inductive argument on syntax and semantics should be checked for completeness across all Core constructs.

    Authors: We agree that the simulation theorem is central. The manuscript derives GraphAlg Core from MATLANG via targeted extensions that directly encode graph primitives: adjacency is represented as a matrix obtained from the input graph representation, and traversal operations are expressed using matrix multiplication combined with the simultaneous induction construct to handle recursive or iterative definitions without semantic gaps. The proof is by structural induction over the syntax of all GraphAlg Core expressions. Base cases cover atomic matrix operations and literals; inductive cases explicitly construct equivalent extended for-MATLANG programs for every graph-specific construct (adjacency extraction, traversal steps, etc.), preserving semantics by definition. The induction is exhaustive over the complete syntax of Core, with no cases omitted, as verified during the proof development. revision: no

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper starts from the external, pre-existing MATLANG language for matrix manipulation, describes syntactic and semantic extensions needed to obtain GraphAlg Core, and supplies an explicit inductive simulation proof that every Core expression is equivalent to a program in the extended for-MATLANG. No step reduces a claimed prediction or result to a fitted parameter, self-definition, or load-bearing self-citation; the derivation chain is self-contained against the external MATLANG baseline and the stated inductive construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard formal language theory and induction principles with no free parameters or invented entities; the paper adds controlled extensions to an existing language rather than postulating new objects.

axioms (1)
  • standard math Standard semantics and inductive definitions in formal language theory
    The simulation proof necessarily relies on these background results from logic and language theory.

pith-pipeline@v0.9.0 · 5373 in / 1247 out tokens · 37638 ms · 2026-05-10T15:50:23.533324+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

12 extracted references · 12 canonical work pages

  1. [1]

    On the Expressive Power of Query Languages for Matrices.ACM Trans

    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

    work page 2019

  2. [2]

    On matrices and K-relations.Annals of Mathematics and Artificial Intelligence, 90(2):181– 210, March 2022

    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

    work page 2022

  3. [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

    work page 1981

  4. [4]

    wildarch/graphalg, February 2026

    Daan de Graaf. wildarch/graphalg, February 2026. original-date: 2025-10- 09T14:03:07Z

    work page 2026

  5. [5]

    Springer Monographs in Mathematics

    Heinz-Dieter Ebbinghaus and J¨ org Flum.Finite Model Theory. Springer Monographs in Mathematics. Springer, Berlin, Heidelberg, 1995

    work page 1995

  6. [6]

    Cypher: An Evolving Query Language for Property Graphs

    Nadime Francis, Alastair Green, Paolo Guagliardo, Leonid Libkin, To- bias Lindaaker, Victor Marsault, Stefan Plantikow, Mats Rydberg, Pe- tra Selmer, and Andr´ es Taylor. Cypher: An Evolving Query Language for Property Graphs. InProceedings of the 2018 International Conference on Management of Data, SIGMOD ’18, pages 1433–1445, New York, NY, USA, May 2018...

    work page 2018

  7. [7]

    Matrix Query Languages.SIGMOD Rec., 50(3):6–19, December 2021

    Floris Geerts, Thomas Mu˜ noz, Cristian Riveros, Jan Van den Bussche, and Domagoj Vrgoˇ c. Matrix Query Languages.SIGMOD Rec., 50(3):6–19, December 2021

    work page 2021

  8. [8]

    Expressive Power of Linear Algebra Query Languages

    Floris Geerts, Thomas Mu˜ noz, Cristian Riveros, and Domagoj Vrgoˇ c. Expressive Power of Linear Algebra Query Languages. InProceedings of the 40th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS’21, pages 342–354, New York, NY, USA, June

    work page

  9. [9]

    Association for Computing Machinery

    work page

  10. [10]

    Algorithm Support for Graph Databases, Done Right, January 2026

    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]

    work page arXiv 2026

  11. [11]

    Information technology — Database languages — GQL, April 2024

    ISO. Information technology — Database languages — GQL, April 2024

    work page 2024

  12. [12]

    Software, Environments, and Tools

    Jeremy Kepner and John Gilbert, editors.Graph Algorithms in the Lan- guage of Linear Algebra. Software, Environments, and Tools. Society for Industrial and Applied Mathematics, January 2011. 21

    work page 2011