ABSTRACT. Critical pairs are a minimal representation of two conflicting transformations of a given structure. Their origin goes back to 1970, when Knuth and Bendix introduced them as a tool for proving local confluence of term rewriting systems. In graph transformation, the first notion of critical pairs was presented in the early 90's by Plump.  Since then, and especially in the last few years, other notions of critical pairs have been presented. In this talk, I will review these various notions, together with their associated results.

ABSTRACT. Rewriting with graphs enjoys a long history in computer science, graphs being used to represent not only data structures, but also program structures, and even computational models. Termination and confluence techniques have been elaborated for various generalizations of trees, such as rational trees, directed acyclic graphs, lambda terms and lambda graphs. But the design of tools for rewriting arbitrary graphs has made little progress beyond various categorical definitions dating from the mid seventies and the study of the particular families of graphs listed above. This paper describes the generalization of term rewriting techniques to a general class of multigraphs that we call drags, viz. finite, directed, ordered (multi-)graphs. To this end, we develop a rich algebra of drags which allows us to view graph rewriting in exactly the same way as we view term rewriting.

ABSTRACT. We describe a mathematical framework for equational reasoning about infinite families of string diagrams which is amenable to computer automation. The framework is based on context-free families of string diagrams which we represent using context-free graph grammars. We model equations between infinite families of diagrams using rewrite rules between context-free grammars. Our framework represents equational reasoning about concrete string diagrams and context-free families of string diagrams using double-pushout rewriting on graphs and context-free graph grammars respectively. We prove that our representation is sound by showing that it respects the concrete semantics of string diagrammatic reasoning and we show that our framework is appropriate for software implementation by proving important decidability properties.

ABSTRACT. We generalize the ordinal diagram system (a strong non-monotonic ordinal notation system) of Takeuti in a quasi-well-ordering form. We sketch two ways of showing well-quasi-orderedness; one by means of Dershowitz-Tzameret’s version of tree-embedding theorem with gap-condition (on the path comparable trees), the other by means of the generalized system of transfinite inductive definition. Although the ordinal diagrams (and other strong ordinal notation systems) could be a good tool for termination proof for certain pattern-based rewrite rule programs, there are some difficulties in applying them, at a slight look; the traditional termination proof paradigm of term rewrite theory uses the monotonicity property and the substitution property, but the strong ordering systems do not have them in general. In this paper, we note some possible uses of the strong well-quasi-ordinal systems for termination proofs by taking an example of pattern-based rewrite rules from the hydra game (of Buchholz).

ABSTRACT. Highlighting the usefulness of graph techniques for problems that have
been approached predominantly as questions about terms, I want to
explain two examples from my past and current work: increasing sharing
in functional programs, and tackling problems about Milner's process
interpretation of regular expressions. The unifying element consists in
modeling terms by term graphs or transition graphs with structure
constraints (higher-order features or labelings with added conditions),
and in being able to go back and forth between terms and graphs.

The first example concerns the definition, and efficient implementation
of maximal sharing for the higher-order terms in the lambda calculus
with letrec. Jan Rochel and I showed that higher-order terms can be
represented by, appropriately defined, higher-order term graphs, that
those can be encoded as first-order term graphs, and that these can in
turn be represented as deterministic finite-state automata (DFAs). Via
these correspondences and DFA minimization, maximal shared forms of
higher-order terms can be computed.

The setting for the second illustration is the process interpretation
of regular expressions, which yields nondeterministic finite-state
automata (NFAs) whose equality is studied under bisimulation. Unlike
for the standard language interpretation, not every NFA can be
expressed by a regular expression. I will explain Milner's
recognizability and axiomatization problems, and some of the results/
partial results that have been obtained. Finally I will explain my
current approach in work together with Wan Fokkink: inspired by
Milner's notion of `loop' we use labelings of process graphs that
witness direct expressibility by a regular expression.
 

ABSTRACT. Term graph rewriting is important as ``conceptual implementation'' of the execution of functional programs, and of data-flow optimisations in compilers. One way to define term graph transformation rule application is via the well-established and intuitively accessible double-pushout (DPO) approach; we present a new result proving semantics preservation for such DPO-based term graph rewriting.

ABSTRACT. We introduce the derivation reduction problem, the undecidable problem of finding a finite subset of a set of clauses such that the whole set can be derived using SLD-resolution. We also study the derivation reducibility of various fragments of second-order Horn logic using a graph encoding technique, with particular applications in the field of Inductive Logic Programming.

ABSTRACT. We examine the process involved in the design and implementation of a port-graph model to be used for the analysis of an agent-based "rational negligence" model, rational negligence being the term used to describe the phenomenon that occurred during the financial crisis of 2008 where investors chose to trade asset-backed securities without performing independent evaluations of the underlying assets thus aiding in heightening the need for more effective and transparent tools in the modelling of the capital markets.

Graph Transformation Systems (GTS) are natural verification and validation tools: they provide visual, intuitive representations of complex systems while specifying the dynamic behaviour of the system in a formal way. In this paper we propose to use a declarative language, based on strategic port-graph rewriting, a particular kind of graph transformation system where port-graph rewriting rules are controlled by user-defined strategies, as a visual modelling tool to analyse a credit derivative market.

ABSTRACT. We present a new approach to the logical design of relational databases, based on strategic port graph rewriting. We show how to model relational schemata as attributed port graphs and provide port graph rewriting rules to perform computations on functional dependencies. Using these rules we present a strategic graph program to find the transitive closure of a set of functional dependencies. This program is sound, complete and terminating, given the restriction that there are no cyclical dependencies in the schema.

ABSTRACT. Term rewriting systems have a simple syntax and semantics and allow for straightforward proofs of correctness. However, they lack the efficiency of imperative programming languages. We define a term rewriting programming style that is designed to be translatable into efficient imperative languages, to obtain proofs of correctness together with efficient execution. This language is designed to facilitate translations into correct programs in imperative languages with assignment statements, iteration, recursion, arrays, pointers, and side effects. Though it is not included in the extended abstract, versions of the language with and without destructive operations such as array assignment are developed, and the relationships between them are sketched. General properties of a translation that suffice to prove correctness of translated programs from correctness of rewrite programs are presented.