We introduce Check-Transfer-Enforce Systems (CTEs) as a general model of behavior of (semi-)autonomous agents, based on the idea of distinguishing the ability of an agent to change its state from the actual changes that can be performed under contextual constraints. In this model, based on many-sorted term algebras, a Request-Guarantee (qg)-agent is characterised by a collection of moves specifying which terms are requested to be present in the current state of the agents and which terms are guaranteed to be present in the successor state, if the move is executed. We show how this approach allows an encoding and a generalisation of a number of well-known existing models. The approach is naturally extended to the case of pairs of communicating qg-agents. An abstract view of the approach can be given in the setting of enriched categories.

Zoom meeting registration link

YouTube live stream

Software systems and the artifacts they consist of often exist in many different variants. When creating new variants, developers typically rely on the “clone and own” strategy of copying and modifying existing variants, a simple and intuitive approach with significant long-term disadvantages. In this talk, I present a line of work on supporting variants in software engineering by explicitly addressing variability as a feature in graph transformations. I focus on three transformation scenarios: one where the input graph has variability (representing the established notion of a software product line), one where rules have variability (leading to variability-based rules), and a combination of the first two scenarios. Each scenario is supported with formal constructions, efficient transformation algorithms, and tool support. Our work shows that a systematic way of supporting variability in transformations can improve the maintainability and the performance of a software system.

Zoom meeting registration link

YouTube live stream

Libraries of machine checked code are, nowadays, organized around hierarchies of algebraic structures. Unfortunately the language of Type Theory and the features provided by the Coq system make the construction of a hierarchy hard even for expert users. The difficulty begins with the non-orthogonal choices, between storing information as record fields or parameters, and between using type classes and canonical structures for inference. To this, one may add the concerns about performance and about the usability, by a non expert, of the final hierarchy.

HB gives the library designer a language to describe the building blocks of algebraic structures and to assemble them into a hierarchy. Similarly it provides the final user linguistic constructs to build instances (examples) of structures and to teach the elaborator of Coq how to take advantage of this knowledge during type inference. Finally HB lets the library designer improve the usability of his library by providing alternative interfaces to the primitive ones, a feature that can also be used to accommodate changes to the hierarchy without breaking user code.

This is a joint work with Kazuhiko Sakaguchi and Enrico Tassi.

Zoom meeting registration link

YouTube live stream

Computational notebooks (CNs) have gained popularity in data science, artificial intelligence, and engineering. CNs are used to document experiments and make them repeatable by incorporating executable segments and renderings of computational results. Unfortunately, computations by graph transformations are not supported by current CNs. In order to close this gap, we have developed GRAPEPress, a tool that combines the GRAPE graph transformation language with the CN tool Gorilla. This talk introduces the GRAPE language as well as its integration with the CN tool Gorilla.

Zoom meeting registration link

YouTube live stream

SMTCoq is a tool to make the Coq proof assistant and SMT solvers cooperate, with the same degree of confidence as Coq. In this talk, I will give an overview of its potential:

* checking SMT answers, both in Coq and externally using the Coq extraction mechanism

* importing SMT problems as Coq theorems

* calling SMT solvers to ease Coq proof building, in a ongoing project called Sniper.

An API to build first-order SMTCoq terms and formulas is also under progress, in order to have an easy access to SMTCoq internal functionalities.

Zoom meeting registration link

YouTube live stream

This talk marks the beginning of GReTA-ExACT, a new online working group within the GReTA community. The aim of this working group will consist in providing an interdisciplinary forum for exploring the diverse aspects of applied category theory relevant in graph transformation systems and their generalizations, in developing a methodology for formalizing diagrammatic proofs as relevant in rewriting theories via proof assistants such as Coq, and in establishing a community-driven wiki system and repository for mathematical knowledge in our research field (akin to a domain-specific Coq-enabled variant of the nLab). A further research question will consist in exploring the possibility for deriving reference prototype implementations of concrete rewriting systems (e.g., over multi- or simple directed graphs) directly from the category-theoretical semantics, in the spirit of the translation-based approaches as in [1],[2] (utilizing theorem provers such as Microsoft Z3).

In the first part of this talk, I will provide an illustrated tour of broad scope of mathematical concepts in modern categorical rewriting theories, ranging over the definitions of Double-Pushout (DPO) and Sesqui-Pushout (SqPO) semantics to the notions of concurrency and associativity theorems, their proofs (illustrating a particular type of diagrammatic reasoning on commutative diagrams), the theory of tracelets, their Hopf algebras and decomposition spaces, certain concepts of opfibrations and finally double-categorical structures that are currently under active investigation (joint work with Paul-André Melliès and Noam Zeilberger). In the second part of the talk, I will outline a proposal for the new GReTA-ExACT online working group format.

References:

[1] R. Heckel, L. Lambers, M.G. Saadat, “Analysis of Graph Transformation Systems: Native vs Translation-based Techniques”, EPTCS 309, 2019, pp. 1-22. http://dx.doi.org/10.4204/EPTCS.309.1

[2] N. Behr, R. Heckel, M.G. Saadat, “Efficient Computation of Graph Overlaps for Rule Composition: Theory and Z3 Prototyping”, EPTCS 330, 2020, pp. 126–144. http://dx.doi.org/10.4204/EPTCS.330.8

Zoom meeting registration link

YouTube live stream

This event will consist of two talks: “Investigating claimed Advantages and Disadvantages of Model Transformation Languages” (by Stefan Höppner) and “Current State of Performance Engineering of Model Transformations” (by Raffaela Groner). Please refer to https://www.irif.fr/~greta/event/2021-oct-08 for the respective abstracts.

Zoom meeting registration link

YouTube live stream

In the first part of the talk, I will present generalized maps that represent quasi-manifolds through their subdivision into topological cells (vertices,edges, faces, volumes). We defined generalized maps as constrained labeled graphs. Arc labels encode topological relations of the subparts modeled object while node labels describe the geometric data used to represent the object. Modeling operations are designed regardless of the object's underlying topology. Therefore, we generalize DPO rules with a functorial approach to encode semi-global relabeling with a product operation. Rules and their extensions (called rule schemes) are considered valid if any application to a well-formed graph results in an equally well-formed graph. We provide set-theoric conditions on rules and rule schemes to ensure the preservation of the model consistency. In the second part of the talk, I will present how this approach allows the design of geometric modelers (software used to create and edit geometric objects) in Jerboa. The set-theoric conditions can be checked via graph traversal in Jerboa's rule editor to ensure that the code derived from the rule will never break the model. The generated code can be used as an add-on in other software or Jerboa's generic viewer. 

Zoom meeting registration link

YouTube live stream

Reverse-mode automatic differentiation, especially in the presence of complex language features, is notoriously hard to implement correctly, and most implementations focus on differentiating straight-line imperative first-order code. Generalisations exist, however, that can tackle more advanced features; for example, the algorithm described by Pearlmutter and Siskind in their 2008 paper can differentiate higher-order functions written in a pure functional language. We show that AD algorithms can benefit enormously from being translated into the language of string diagrams in two steps: first, we describe a Pearlmutter-Siskind style AD algorithm as a set of rules for transforming hierarchical graphs; rules which can -and indeed have been- be implemented correctly and efficiently for a non-trivial language. Then, we present a proof of soundness for it by reducing the above rewrite rules to a suitable graphical version of the axioms of Cartesian reverse differential categories, expressed as string diagrams.

Zoom meeting registration link

YouTube live stream

Quantum circuits give a de facto “assembly language” for quantum computation. Hence, the design, optimisation, and verification of quantum circuits is an important task in developing efficient, correct software to run on quantum computers. In this talk, I will survey some of the latest developments in applying the ZX-calculus - a graphical theory of interacting quantum processes - to three important problems in quantum software: the optimisation of quantum circuits, functional verification of circuits, and development of heuristics for efficient classical simulation.

Zoom registration

YouTube live stream

A celebrated theorem of Chandra and Merlin states that Conjunctive Queries inclusion is decidable. Its proof transforms logical formulas to hypergraphs: each query has a natural model – a kind of graph – and query inclusion reduces to the existence of a graph homomorphism between natural models. In this talk, we introduce the diagrammatic language Graphical Conjunctive Queries (GCQ) and show that it has the same expressivity as Conjunctive Queries. GCQ terms are string diagrams, and their algebraic structure allows us to derive a sound and complete axiomatisation of query inclusion, which turns out to be exactly Carboni and Walters’ notion of cartesian bicategory of relations. Our completeness proof exploits the combinatorial nature of string diagrams as (certain cospans of) hypergraphs: Chandra and Merlin’s insights inspire a theorem that relates such cospans with spans. Completeness and decidability of the (in)equational theory of GCQ follow as a corollary. Categorically speaking, our contribution is a model-theoretic completeness theorem of free cartesian bicategories (on a relational signature) for the category of sets and relations.

Zoom registration

YouTube live stream

We propose an abstract notion of networks of exchanges modelling the global money market of decentralised finance. We formalise routing and arbitrage on such networks as convex optimisation problems. We provide bounds with closed formulas in the specific case of “constant product” automated markets and a restricted form of cyclic arbitrage. We compute the associated lower bounds on actual data derived from the Ethereum blockchain. (joint work with Hamza El Khalloufi and Julien Prat)

Zoom registration

YouTube live stream

Graph rewriting systems are naturally endowed with a notion of parallelism due to the locality of the effect of rules. These aspects have been studied in the classical theory from an interleaving perspective, based on sequential independence, shift equivalence and related notions. In the last three decades the theory has been enriched with notions, constructions and results which provide a direct account of causality and non-determinism in graph derivations, borrowed from (and extending) the theory of Petri Nets. In the talk I will present a personal overview of the development of this theory starting from the basic structural relation between nets and graph rewriting systems, and I will survey some more recent developments.

Zoom registration

YouTube live stream

A vast swath of computation and computer science theory takes place on combinatorial data structures, which are often presented as variations on the theme of graphs. Catlab.jl is a Julia package for computational category theory, which includes an implementation of C-Sets, also known as copresheafs or category actions. C-Sets always form an adhesive category and can be used for general rewriting systems. This talk will present the theory and implementation of C-Sets along with some examples. In particular, Colored Graphs and String Diagrams (syntax for symmetric monoidal categories) will be shown.

Zoom registration

YouTube live stream

About the speaker:

Stephen Wolfram is the creator of Mathematica, Wolfram|Alpha and the Wolfram Language; the author of “A New Kind of Science”; the originator of the Wolfram Physics Project; and the founder and CEO of Wolfram Research. Over the course of more than four decades, he has been a pioneer in the development and application of computational thinking—and has been responsible for many discoveries, inventions and innovations in science, technology and business.

Zoom registration

YouTube live stream

String diagrams are an elegant, convenient and powerful syntax for arrows of symmetric monoidal categories. In recent years, they have been used as compositional descriptions of computational systems from various fields, including quantum foundations, linear algebra, control theory, automata theory, concurrency theory, and even linguistics. All of these applications rely on diagrammatic reasoning, which is to string diagrams as equational reasoning is to ordinary terms.

If we are to take string diagrams out of research papers and into practical applications, we need understand how to implement diagrammatic reasoning. This is the focus of my talk.

There is a tight correspondence between symmetric monoidal categories where every object has a coherent special Frobenius algebra structure and categories of cospans of hypergraphs. This correspondence, therefore, takes us from a topological understanding of string diagrams to a combinatorial data-structure-like description. Moreover, diagrammatic reasoning translates via this correspondence exactly to DPO rewriting with interfaces.

The obvious follow-up question is: how much of this correspondence survives if we drop the assumption about Frobenius structure? Can we use this correspondence to implement diagrammatic reasoning on vanilla symmetric monoidal categories? The answer is yes, but we need to restrict the kinds of cospans we consider: the underlying hypergraph has to be acyclic and satisfy an additional condition called monogamy. Moreover, we must restrict the DPO rewriting mechanism to a variant that we call convex DPO rewriting. The good news is that none of these modifications come with a significant algorithmic cost.

The material in this talk is joint work with Filippo Bonchi, Fabio Gadducci, Aleks Kissinger and Fabio Zanasi, and has been published in a series of papers:

- “Rewriting modulo symmetric monoidal structure”, Proceedings of LiCS 2016

- “Confluence of Graph Rewriting with Interfaces”, Proceedings of ESOP 2017

- “Rewriting with Frobenius”, Proceedings of LiCS 2018

YouTube recording

This talk will summarize some recent results obtained in connection with the Wolfram Physics Project: a systematic attempt to reduce fundamental physics to the problem of hypergraph rewriting. Specifically, we will discuss the construction of an efficient hypergraph rewriting scheme using the formalism of Wolfram model multiway systems, with a categorical semantics defined via double-pushout rewrites over selective adhesive categories, and equipped with a dagger-symmetric monoidal structure that exhibits surprising formal connections to categorical quantum mechanics. We will also demonstrate that, by equipping such a multiway system with an additional notion of causal structure (defined via the semantics of precausal categories), we are able to introduce new inference rules of selective resolution, paramodulation and factoring that generalize the standard Knuth-Bendix completion rules for term rewriting systems, and significantly improve the efficiency of automated diagrammatic reasoning algorithms over hypergraphs. Time permitting, we will discuss some near-term practical applications of these methods for quantum information theory (allowing for more efficient diagrammatic simplification of quantum circuits), as well as numerical general relativity (allowing for more explicit numerical simulation of graph-theoretic models of space and time).

YouTube recording

In the first part of the presentation, some aspects of formal graph language theory are discussed. A few variants of graph grammars were introduced in the early 1970s as generalizations of Chomsky grammars. This first step into a formal graph language theory was further developed by the investigation of edge and hyperedge replacement on one hand and on some variants of node replacement on the other hand starting in the late 1970s. Since then, a good number of structural and decidability properties were proved. In particular, it turned out that hyperedge replacement grammars behave to a large degree in a context-free manner. In the second part of the presentation, the novel approach of fusion grammars is surveyed.

A fusion grammar is a hypergraph grammar which provides a start hypergraph of small connected components. To derive hypergraphs, connected components can be copied multiple times and can be fused by the application of fusion rules (where such an application removes two complementary hyperedges and merges their attachment vertices). The generated hypergraph language contains all terminal connected components of derived hypergraphs. The main results for various kinds of fusion grammars concern their generative power.

YouTube live stream recording

Double Pushout (DPO) rewriting, the dominant model for graph rewriting, emerged in the early 70’s, strongly influenced at that time by graph grammars. Developed by Hartmut Ehrig and his many collaborators, graph rewriting was from the beginning based on category theory, with the major insight that the two basic rewriting constructions, namely matching and replacement, were intimately related to graph morphisms and their pushouts. A new model has emerged recently, so-called Composition based rewriting (Core), in which rewriting is based on a composition operator over directed rooted labelled graphs (drags), so that matching a drag G against a drag L amounts to compose L with some context drag C, and rewriting G with L → R to compose R with C. We will describe Core for drags before to relate it precisely to DPO and extend it to adhesive categories of graphs and beyond. We will also show how to define composition abstractly in any category of graphs satisfying appropriate properties among which adhesivity (wrt monomorphisms). Major differences between DPO and Core will be discussed.

YouTube live stream recording

This will be an overview of our ongoing work on fast graph programs in the language GP 2. We will present programs which in some cases match the time complexity of graph algorithms in imperative languages. In other cases we need to assume that input graphs have a bounded degree, to reach the speed of conventional algorithms.

YouTube live stream recording

An overview presentation of the work we have been doing over the past years on MDEOptimiser, a tool that uses evolutionary search over EMF models to solve multi-objective optimisation problems. Graph transformations are used to encode mutation operators, opening interesting opportunities for automatically generating domain-specific mutation operators.

YouTube live recording

Confluence has been studied for graph transformation since several decades now. Confluence analysis has been applied, for example, to determining uniqueness of model transformation results in model-driven engineering. It is strongly related to conflict analysis for graph transformation, i.e. detecting and inspecting all possible conflicts that may occur for a given set of graph transformation rules. The latter finds applications, for example, in software analysis and design. Both conflict and confluence analysis rely on the existence and further analysis of a finite and representative set of conflicts for a given set of graph transformation rules.

Traditionally, the set of critical pairs has been shown to constitute such a set. It is representative in the sense that for each conflict a critical pair exists, representing the conflict in a minimal context, such that it can be extended injectively to this conflict (M-completeness). Recently, it has been shown that initial conflicts constitute a considerably reduced subset of critical pairs, being still representative in a slightly different way. In particular, for each conflict there exists a unique initial conflict that can be extended (possibly non-injectively) to the given conflict (completeness). Compared to the set of critical pairs, the smaller set of initial conflicts allows for more efficient conflict as well as confluence analysis.

We continue by demonstrating that initial conflicts (critical pairs) are minimally complete (resp. minimally M-complete), and thus are both optimally reduced w.r.t. representing conflicts in a minimal context via general (resp. injective) extension morphisms. We proceed with showing that it is impossible to generalize this result to the case of rules with application conditions (equivalent to FOL on graphs). We therefore revert to a symbolic setting, where finiteness and minimal (M-)completeness can again be guaranteed. Finally, we describe important special cases (e.g. rules with negative application conditions), where we are able to obtain minimally complete (resp. M-complete) sets of conflicts in the concrete setting again.

YouTube live recording of the seminar

Program transformations are frequently developed, e.g., to realize programming language extensions or dynamic program analyses such as profiling. They are typically implemented by manipulating bytecode as the availability of source code is not guaranteed. There are standard libraries such as ASM that are typically used for implementing Java bytecode manipulations. To check their correctness, they are usually tested by applying them to different programs, running the manipulated programs and observing their behaviors. As part of the second step, the Java virtual machine verifies the bytecode, which can uncover errors in the bytecode introduced by the manipulation. That approach uses different technologies that are not well linked making the process of developing and testing bytecode manipulations difficult. In this talk, we intend to perform bytecode manipulation by using concepts and techniques of model-driven engineering. We are convinced that the declarative nature of model transformation rules allows the debugging and analyzing of bytecode manipulations in more details than classically done. Following this path, a meta-model for bytecode is needed including OCL constraints for bytecode verification. We show that basing bytecode manipulation on model transformation can provide more immediate guidance and feedback to the developer, especially when model transformation is formally based on graph transformation. Bytecode verification can take place directly in the manipulated model with the help of OCL checking, eliminating the need to use multiple technologies. In some cases, it is even possible to automatically determine application conditions under which bytecode manipulations are correct by construction; then bytecode verification after a bytecode manipulation can be avoided altogether.

YouTube live recording of the seminar