ABSTRACT. The concept of ‘syntax’ is commonly understood as the structure hidden in linear sequences of tokens, which in language and logic we commonly call ‘terms’. However, for the purpose of analysis and transformation, compilers use more efficient data structures to represent syntax, namely graphs. The gap between the linear (term) and graph syntax is elegantly bridged by a third formalism, namely that of string diagrams, a planar representation of terms in the categorical representation of syntax. In this talk I will show how the interplay of terms, graphs, and diagrams can help specify and implement complex analyses and transformations in compilers for higher-order programming languages, such as type inference, automatic differentiation, or closure conversion. This methodology is at the foundation of a new industrial-strength compiler being implemented currently at Huawei. Most of the material I will discuss is based on the recent tutorial paper “Hierarchical string diagrams and applications” jointly with Fabio Zanasi (https://arxiv.org/abs/2305.18945) about to appear as a CUP monograph.

ABSTRACT. Graph Neural Networks are deep learning models designed to process graph-structured data. Most modern GNNs operate by message passing: node representations are updated through repeated rounds of aggregating and combining information from neighboring nodes. This makes them well suited to applications involving relational and networked structures, and also places them naturally in dialogue with topics from graph rewriting and graph-based computation. In this talk, we present recent results on the relationship between Graph Neural Networks and formal logic, with the choice of topics guided by the speaker's own research in the area. We introduce logics that precisely capture the expressive power of certain classes of integer-valued GNNs, and show how GNN computations can be translated into logical formulas. We also discuss variants of GNNs over finite computer number formats. These logical characterizations provide a foundation for formal verification, allowing us to establish complexity bounds for key reasoning problems about GNN behavior.

ABSTRACT. We present function-constructor nets, a Turing-complete subset of interaction nets in which agents are partitioned into functions and constructors, inducing a notion of observable output whilst preserving the permutation equivalence of reduction sequences and hence the potential for parallel execution. We then introduce FLIN, a language with a functional-style syntax for programming such nets, and describe several extensions to the core language to improve expressiveness and practicality. Finally, we present a prototype implementation that demonstrates the viability of the approach.

ABSTRACT. Linearization is essentially a program transformation in whose output all uses of input-bound variables correspond to different inputs, and which preserves the computational content of the original program. It can be syntactic, when applied to every subterm, or semantic, when applied only to functions which are used during reduction. One known example of semantic linearization is Weak Linearization, based on the maximal reduction strategy and which may not terminate when the program loops. The question we intend to answer here is this: how can we make such a linearization finer, so that we can get partial linearizations which work even in cases where the term is not strongly normalizing? In this paper we define a new linearization technique that answers the previous question using a linearization parametrized by a finite sequence of redexes, which is based on the idea of approaching the term as a tree.

ABSTRACT. We retrace some history of using term graphs for implementing β-reduction in the λ-calculus. We refactor the following three high-lights from that history, illustrated by a prototype implementation: - the classical (first) term graph implementation (Wadsworth), of β-reduction which we refactor through a term graph implementation IMP of a well-behaved (e.g., orthogonal) class of TRSs; - implementing β-reduction through repeated weak-reduction (De Bruijn (Automath),Peyton Jones,Coquand,Grégoire & Leroy,Balabonski,...), which we show can be performed on IMP; - implementing needed β-reduction (Huet & Lévy, Barendregt, Kennaway, Klop, Sleep,...) through a strategy for IMP that we dub α-spine. By making use of union-find techniques for it, normal order reduction is shown to be linearly implementable.

ABSTRACT. Sands' notion of improvement asserts that one program has the same behaviour and requires less execution time compared to another program. Aiming at a robust and automatable methodology of proving improvement, we develop rewriting systems that uses combinatorially-structured graphs, are mathematically solid, and are as expressive as second-order term rewriting. We introduce term-rewriting notions of variable binding, substitution and contexts, to Double Pushout rewriting of hypergraphs. Variable binding is represented simply by extra incidence, with the help of criteria to ensure well-formed binding. We demonstrate our rewriting systems by showing two-way simulation results for Hamana's second-order computational systems, and Alvarez-Picallo et al.'s string-diagram rewriting in a monoidal closed category.

ABSTRACT. This paper explores how concepts from hypergraphs and term graphs can be productively applied to structural proof theory. By treating the sequents that encode proof search states as ordered hypergraphs---where eigenvariables represent nodes and relations represent directed edges---inference rules can directly capture rewriting dynamics. We demonstrate how modern proof-theoretic advances, including linear logic, focusing, synthetic inference rules, and binder mobility, provide a formal foundation for exploiting these graph structures. Ultimately, this work suggests that integrating hypergraph representations into proof theory can enhance the design and implementation of automated and interactive theorem provers.

ABSTRACT. A process interpretation of regular expressions was first studied in Milner (1984), where they were called star expressions. Milner gave a sound axiomatization for bisimilarity of the process interpretation of star expressions, leaving the problem of completeness open. Recently, Grabmayer & Fokkink (2020) gave a partial solution for 1-free star expressions via LLEE charts. We propose a new class of charts, based on reducible graphs, an important class of graphs in compiler engineering. These graphs can be characterized via a structural property and via graph transformations; we leverage both to construct a simple completeness proof for strongly normed 1-free star expressions. We hope to extend this work in progress to a full completeness proof, and are interested in other applications of structural characterizations in term graph rewriting.

ABSTRACT. We report on work in progress on the characterisation of the structure of process graphs that are process interpretations of regular expressions. Hereby we only aim to recognise the structure of graphs in the image of the interpretation (modulo isomorphism), without permitting to extend this image modulo bisimilarity (or another congruence) as in Milner's process semantics of regular expressions. At the previous workshop we presented the result that, for a slightly more compact variant of the process interpretation as is commonly used, the image of `under-star-1-free' regular expressions is closed under the operation of bisimulation collapse. Here we report two significant extensions that we work out now, and at the moment can only label as statements. First, a finite process graph is isomorphic to a compact process interpretation of an under-star-1-free regular expression if and only if it satisfies the Loop Existence and Elimination property (LEE). Second, a finite process graph G is isomorphic to a compact process interpretation of a regular expression if and only if G satisfies a generalisation 1-LEE, which requires that LEE holds for a representation of G with 1-transitions (empty steps).