Kaliningraph: A Type Family of Algebraic Graphs

This library implements a new computational model which we call graph computation. In contrast with prior work, e.g., Turing's machine and Church's -calculus, the advantage of this model is that it can be directly translated to iterated matrix multiplication on GPUs and has many desirable algebraic properties. Furthermore, it offers a natural way to express algebraic circuits, neural networks, factor graphs, proof networks, and enjoys many connections to programming language theory, automata theory and category theory.

Kaliningraph currently supports backpropagation in Kotlin. Efforts to lower other propagation schemes, e.g., belief propagation, uncertainty propagation, unit propagation, survey propagation and constraint propagation are ongoing. All of these schemes operate according to a principle known as message passing and are in general known to be Turing complete. This unification allows us to study many common problems in related domains using well-studied tools from arithmetic circuit complexity, to spectral and algebraic graph theory.

Installation

Kaliningraph is hosted on Maven Central.

Gradle

kotlin dependencies { implementation("ai.hypergraph:kaliningraph:0.1.8") }

Maven

xml <dependency> <groupId>ai.hypergraph</groupId> <artifactId>kaliningraph</artifactId> <version>0.1.8</version> </dependency>

Jupyter notebook

To access notebook support, use the following line magic:

@file:DependsOn("ai.hypergraph:kaliningraph:0.1.8")

For more information, explore our tutorials:

• Hello Kaliningraph.ipynb
• Program Graphs.ipynb

Graphs, inductively

What are graphs? A graph is a (possibly empty) set of vertices.

What are vertices? A vertex is a unique label with neighbors (possibly containing itself).

What are neighbors? Neighbors are a graph.

Circuits, inductively

What is a circuit? A circuit is either:

• A Boolean logic gate (e.g., and, or, not)
• A circuit that takes two inputs and swaps them (a, b) -> (b, a)
• A circuit that takes one input and gives one output a -> b
• The serial composition of two circuits (a->c, c->d) -> (a->d)
• The parallel composition of two circuits (a->b, c->d) -> (a, b) -> (c, d)

Getting started

Run the demo via ./gradlew jvmTest --tests "ai.hypergraph.kaliningraph.HelloKaliningraph" to get started.

Usage

Kaliningraph treats string adjacency and graph adjacency as the same. To construct a graph, simply enumerate walks.

This can be done using a raw string, in which case unique characters will form the vertex set. Whitespace delimits walks:

kotlin val graph = LabeledGraph { "abcde ace" }

Vertices can also be linked via the - operator. The graph builder DSL provides a small alphabet:

kotlin val graph = LabeledGraph { a - b - "c" - d - e; a - c - e }

This is equivalent to:

kotlin val abcde = LabeledGraph { a - b - c - d - e } val ace = LabeledGraph { a - "c" - e } val graph = abcde + ace

Equality is supported using the Weisfeiler-Lehman test:

kotlin val x = LabeledGraph { a - b - c - d - e; a - c - e } val y = LabeledGraph { b - c - d - e - f; b - d - f } assertEquals(x == y) // true

Visualization

Kaliningraph supports a number of graph visualizations.

Graphviz

Graph visualization is made possible thanks to KraphViz.

```kotlin val de = LabeledGraph { d - e } val dacbe = LabeledGraph { d - a - c - b - e } val dce = LabeledGraph { d - c - e }

val abcd = LabeledGraph { a - b - c - d } val cfde = LabeledGraph { c - "a" - f - d - e }

val dg = LabeledGraph(dacbe, dce, de) + Graph(abcd, cfde) dg.show() ```

Running the above snippet will cause the following figure to be rendered in the browser:

Matrix form

Graph visualization in both DOT and adjacency matrix format is supported.

| DOT Graph | Matrix | |:---------------------------------------------|:--------------------------------------------| | | |

It is also possible to visualize the state and transition matrices and step through the graph (./gradlew jsBrowserRun --continuous).

Computation graph

Computational notebooks prototyping is also supported.

Notebook { a = b + c f = b - h }.show()

The above snippet should display something like the following:

Translation

Bidirectional translation to various graph formats, including Graphviz, JGraphT, Tinkerpop and RedisGraph is supported:

kotlin val g = LabeledGraph { a - b - c - a } .toJGraphT().toKaliningraph() .toTinkerpop().toKaliningraph() .toGraphviz().toKaliningraph()

Code2Vec

Code2Vec generation and visualization is supported. The following demo was generated using message passing on the adjacency matrix, for graphs of varying height. The technique to create the embeddings is described here. We use TSNE to visualize the resulting vectors in 2D, and can clearly distinguish the clusters.

Automata-based RegEx

A regex to NFA compiler is provided. To run the demo, run ./gradlew RegexDemo. You should see something like this:

Research questions

• What is the best way to represent a graph?
  • Type family
  • Matrix semiring
  • Kernel embedding
• Is it possible to statically check tensor arithmetic in the Kotlin type system?
  • Church arithmetic
  • Binary arithmetic
  • Decimal arithmetic
  • Multidimensional arrays
• How computationally powerful is matrix multiplication?
  • Can we do SAT/SMT solving using a matrix semiring?
  • What does asymptotically optimal CFG parsing look like? (e.g., Valiant)
  • Can we simulate finite automata / regular expressions?
• Is subgraph isomorphism feasible using random walks?
  • Treat graph as a sequence and run string convolution
  • Generate lazy random walk and halt after K steps
  • Convolve permuted variants of query in parallel
  • Need some kind of label permutation / edit distance metric
• How do we represent a tensor/hypergraph?
  • Naperian functor
  • Sparse recursive dictionary
• How could we implement graph grammars/rewriting?
  • Rewrites as string substitution on the random walk sequence
  • Reconstruct graph from rewritten string using adjacency matrix
  • ~~Is there an algebraic definition for graph grammars?~~
  • ~~Maybe graph convolution. How to encode rewrites as a kernel?~~
  • ~~Rectangular matrix multiplication or square with upper bound?~~
  • ~~May be possible to represent using tensor contraction~~
  • Need to look into hyperedge replacement grammars
  • How do we identify confluent rewrite systems?
• What are the advantages and disadvantages of graph rewriting?
  • Graphs as vertices and rewrites as edges in a nested graph?
  • Reduction/canonicalization versus expansion graph grammar
• What happens if we represent the graph as a symbolic matrix?
  • Could we propagate functions instead of just values?
  • What if matrix elements were symbolic expressions? (cf. KeOps)
  • Should we represent the whole matrix as a big bold symbol?
• Is there an efficient way to parallelize arithmetic circuits?
  • Translate formula graph to matrix using Miller's evaluator
  • How to distribute the work evenly across sparse matrices
• What are some good way to visualize random walks?
  • Display states, transitions and graph occupancy side-by-side
• Is there a connection between linear algebra and -calculus?
  • expressions can be represented as a graph/matrix
  • Maybe Arrighi and Dowek (2017) have the answer?
  • Look into optimal beta reduction and Lamping's optimal reduction algorithm

References

Knowledge graphs

• Organizing Math as a Rule-based Decision Tree, Rich et al. (2018)
• GOOL: a generic object-oriented language, Carette et al. (2020)
• ProbOnto 2.5: Ontology and Knowledge Base of Probability Distributions, Maciej et al. (2016)
• Metamath Proof Explorer, Megill (2006)
• The Empirical Metamathematics of Euclid and Beyond, Wolfram (2020)
• Metafore della Matematica, Bo (2014)

Graph theory

• Solutio problematis ad geometriam situs pertinentis, Euler (1741)
• Account of the Icosian Calculus, Hamilton (1858)
• Mathematical Foundations of the GraphBLAS, Kepner et al. (2016)
• Graph Algorithms in the Language of Linear Algebra, Kepner and Gilbert (2011)
• Graphs, Dioids and Semirings. New Models and Algorithms, Gondran and Minoux (2008)
• Path Problems in Networks, Baras and Theodorakopoulos (2010)
• Parallel Matrix and Graph Algorithms, Dekel et al. (1981)

Graph learning

• Graph Representation Learning, Hamilton (2020)
• Spectral Graph Theory with Applications to ML, Miller (2020)
• Neural Execution of Graph Algorithms, Velikovi et al. (2020)

Functional graphs

• Functional programming with structured graphs, Oliveira and Cook (2012)
• Think Like a Vertex, Behave Like a Function! A Functional DSL for Vertex-Centric Big Graph Processing, Emoto et al. (2016)
• Inductive Graphs and Functional Graph Algorithms, Erwig (2001)
• Fully Persistent Graphs Which One To Choose?, Erwig (1997)
• The Program Dependence Graph and its Use for Optimization, Ferrante et al. (1987)

Graph rewriting

• Factor Graph Grammars, Chiang and Riley (2020)
• Seam: Provably Safe Local Edits on Graphs, Papadakis et al. (2017)
• Equational term graph rewriting, Ariola and Klop (1997)
• Bisimilarity in Term Graph Rewriting, Ariola et al. (2000)
• LEAN: An intermediate language based on graph rewriting, Barendregt et al. (1988)
• An Algorithm for Optimal Lambda Calculus Reduction, Lamping (1990)
• A New Implementation Technique for Applicative Languages, Turner (1979)
• A Reformulation of Matrix Graph Grammars with Boolean Complexes, Velasco and de Lara (2009)
• Towards a GPU-based implementation of interaction nets, Jiresch (2012)

Unification

• A Catalogue of Canonical Term Rewriting Systems, Hullot (1980)
• Graph Unification and Matching, Plump and Habel (1996)
• Unification with Drags, Jouannaud and Orejas (2020)
• The identity problem for elementary functions and constants, Richardson and Fitch (1994)
• Duplicate code detection using anti-unification, Bulychev and Minea (2008)

Termination checking

• Proving Termination of Graph Transformation Systems using Weighted Type Graphs over Semirings, Bruggink (2015)
• Termination of string rewriting with matrix interpretations, Hofbauer (2006)
• Matrix Interpretations for Proving Termination of Term Rewriting, Endrullis et al. (2007)
• Graph Path Orderings, Dershowitz and Jouannaud (2019)

Algebra

• Algebraic Property Graphs, Shinavier and Wisnesky (2020)
• Algebraic Graphs with Class (Functional Pearl), Mokhov (2017)
• Algebra of Parameterised Graphs, Mokov and Khomenko (2014)
• Fun with Semirings, Dolan (2013)
• Introduction to Algebraic Theory of Graph Grammars, Erhig (1978)
• Drags: A Simple Algebraic Framework For Graph Rewriting, Dershowitz and Jouannaud (2018)
• An Algebraic Theory of Graph Reduction, Arnborg (1993)
• Lineal: A linear-algebraic -calculus, Arrighi and Dowek (2017)
• Graph products, Wikipedia
• Graphs and Geometry, Lovsz (2019)

Circuits

• Reductions between Families of Polynomials in Theory and in Practice, Valiant, Hyafil et al.
• Efficient parallel evaluation of straight-line code and arithmetic circuits, Miller (1986)
• Algebraic Decision Diagrams and Their Applications, Bahar et al. (1997)
• Arithmetic Circuit Verification Based on Word-Level Decision Diagrams, Chen (1998)
• An Efficient Graph Representation for Arithmetic Circuit Verification, Chen and Bryant (2001)
• A Top-Down Compiler for Sentential Decision Diagrams, Oztok and Darwiche (2015)
• Representations of Elementary Functions Using Edge-Valued MDDs, Nagayama and Sasao (2007)
• Complexities of Graph-Based Representations for Elementary Functions, Nagayama and Sasao (2008)
• Numerical Function Generators Using LUT Cascades, Sasao and Nagayama (2007)

Propagation

• Unifying Graph Convolutional Neural Networks and Label Propagation, Wang and Leskovec (2020)
• Equilibrium Propagation: Bridging the Gap between Energy-Based Models and Backpropagation Scellier and Bengio (2017)
• Expectation Propagation for Approximate Bayesian Inference, Minka (2001)
• Propagation Networks: A Flexible and Expressive Substrate for Computation, Radul (2009)
• The Art of the Propagator, Radul and Sussman (2009)
• Fusion, propagation, and structuring in belief networks, Pearl (1986)

Random walks

• Random Walks on Graphs: A Survey, Lovsz (1993)
• String Edit Distance, Random Walks and Graph Matching, Kelly and Hancock (2002)
• Exact and Approximate Graph Matching Using Random Walks, Gori and Maggini (2005)
• Reweighted random walks for graph matching, Cho and Lee (2010)
• Small Subgraphs in the trace of a random walk, Krivelevich and Michaeli (2018)
• Biased random walk on the trace of a biased random walk on the trace of..., Crydon and Holmes (2019)
• KnightKing: A Fast Distributed Graph Random Walk Engine, Yang et al. (2019)
• Graph Learning with 1D Convolutions on Random Walks, Toenshoff et al. (2021)

Software engineering

• Getting F-Bounded Polymorphism into Shape, Tate (2014)
• Frequent Subgraph Analysis and its Software Engineering Applications, Henderson (2017)
• Semantic Enrichment of Data Science Code, Patterson (2020)
• Finally, a Polymorphic Linear Algebra Language, Shaikhha and Parreaux (2019)
• Towards an API for the Real Numbers, Boehm (2020)

Proof search

• Generative Language Modeling for Automated Theorem Proving, Polu et al. (2020)
• Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic, Sekiyama et al. (2020)
• Can Neural Networks Learn Symbolic Rewriting?, Piotrowski et al. (2020)
• Tree Neural Networks in HOL4, Gauthier (2020)
• Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs, Li et al. (2020)

Code search

• Approximate Online Pattern Matching in Sub-linear Time, Chakraborty et al. (2018)
• Improved online algorithms for jumbled matching, Ghuman et al. (2018)
• Parallelizing Exact and Approximate String Matching via Inclusive Scan on a GPU, Mitani et al. (2017)
• A Novel Algorithm for Online Inexact String Matching and its FPGA Implementation, Cinti et al. (2019)
• Context-Free Path Querying by Matrix Multiplication, Azimov and Grigorev (2018)
• Code Search on Bytecode for Mobile App Development, Nguyen et al. (2019)
  • Uses a HMM to model transitions between method calls

Word problems

• The problem of solvability of equations in a free semigroup, Makanin (1977)
• Word equations with length constraints: whats decidable?, Ganesh et al. (2012)
• On Solving Word Equations Using SAT, Day et al. (2019)
• TRAU: SMT solver for string constraints, Abdulla et al. (2018)
• A Survey on String Constraint Solving, Amadini (2021)

Software

Graphs

• KeOps - Dense, sparse and symbolic tensor library
• Alga - a library for algebraic construction and manipulation of graphs in Haskell
• Bifurcan - high-quality JVM implementations of immutable data structures
• Kraphviz - Graphviz with pure Java
• JGraLab - a Java graph library implementing TGraphs: typed, attributed, ordered, and directed graphs (paper)
• GraphBLAS - open effort to define standard building blocks for graph algorithms in the language of linear algebra
• GraphBLAST - High-Performance Linear Algebra-based Graph Primitives on GPUs

Rewriting

• Grez - graph transformation termination checker (manual)
• GP2 - Rule-based graph programming language
• AGG - development environment for attributed graph transformation systems supporting an algebraic approach to graph transformation (manual)
• Henshin - an IDE for developing and simulating triple graph grammars (TGGs) (manual)
• JavaSMT - Unified Java API for SMT solvers

Automata

• roll-library
• dk.brics.automata
• LearnLib

Special thanks

The following individuals have helped inspire this project through their enthusiasm and thoughtful feedback. Please check out their work.

• Jin Guo
• Xujie Si
• Andrey Mokhov
• Fabian Muehlboeck
• Ben Greenman
• Dave Keenan
• John Tromp