Published: 10th September 2016 DOI: 10.4204/EPTCS.225 ISSN: 2075-2180 |
Preface Andrea Corradini and Hans Zantema | 1 |
Invited Presentation:
Termination of Graph and Term Graph Rewriting Barbara König | 2 |
Invited Presentation:
Non-Termination of Cycle Rewriting by Finite Automata Jörg Endrullis | 3 |
Compiling Process Networks to Interaction Nets Ian Mackie | 5 |
In-place Graph Rewriting with Interaction Nets Ian Mackie and Shinya Sato | 15 |
Kruskal's Tree Theorem for Acyclic Term Graphs Georg Moser and Maria A. Schett | 25 |
Reasoning about Graph Programs Detlef Plump | 35 |
Token-passing Optimal Reduction with Embedded Read-back Anton Salikhmetov | 45 |
Efficient Completion of Weighted Automata Johannes Waldmann | 55 |
TERMGRAPH 2016 took place in Eindhoven (NL) on April 8, 2016, as a one-day satellite event of ETAPS 2016. Previous editions of the TERMGRAPH workshops series took place in Barcelona (2002), Rome (2004), Vienna (2006), Braga (2007), York (2009), Saarbrücken (2011), Rome (2013), and Vienna (2014).
Research in term and graph rewriting ranges from theoretical questions to practical issues. Computing with graphs handles the sharing of common subexpressions in a natural and seamless way, and improves the efficiency of computations in space and time. Sharing is ubiquitous in several research areas, for instance: the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the modelling of biological or chemical abstract machines, the implementation techniques of programming languages: many implementations of functional, logic, object-oriented, concurrent and mobile calculi are based on term graphs. Term graphs are also used in automated theorem proving and symbolic computation systems working on shared structures.
The aim of TERMGRAPH 2016 was to bring together researchers working in different domains on term and graph transformation and to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in term graph rewriting.
Topics of interest for the workshop include all aspects of term graphs and sharing of common subexpressions in rewriting, programming, automated reasoning and symbolic computation.
The present volume contains the six contributions presented during the workshop: they were selected by the Program Committee according to originality, significance, and general interest. In addition to these presentations, the programme included two invited lectures, by Barbara König and Jörg Endrullis, whose abstracts are included as well.
Joint work with H.J. Sander Bruggink, Dennis Nolte, Hans Zantema
We introduce techniques for proving uniform termination of graph transformation systems, based on matrix interpretations for string rewriting. We generalize this technique by adapting it to graph rewriting instead of string rewriting and by generalizing to ordered semirings. In this way we obtain a framework which is based - depending on the semiring - on so-called tropical, arctic and arithmetic type graphs. These type graphs can be used to assign weights to graphs and to show that these weights decrease in every rewriting step in order to prove termination. We present an example involving counters and discuss the implementation in the tool Grez. Furthermore we discuss applications to showing termination for term graph rewriting.
This talk is based on two papers which appeared in IFIP-TCS '14 and ICGT '15.
In this tutorial we explain a technique from [7] for proving (non-looping) non-termination of term rewriting systems based on finite automata, and we propose an extension of the approach for proving non-termination of cycle rewriting. Note that non-termination is an undecidable property [5].
The usual method for proving non-termination of term rewriting systems are looping reductions, that is, rewrite sequences of the form t →^{+} C[tσ]. However, there are non-terminating term rewriting systems that do not admit such looping rewrite sequences, see e.g. [8]. A famous example is the S-combinator from Combinatory Logic with the rewrite rule Sxyz → xz(yz) [1, 9, 6, 2]. Surprisingly, there are hardly any techniques [4, 7] available for proving non-termination in the absence of loops.
The approach that we present, employs finite automata as certificates of non-termination. The basic idea is to find a finite automaton accepting a language that is weakly closed under rewriting: every term s in the language must admit some rewrite step s → t such that t is again in the language. We encode these requirements as satisfiability problems and employ SAT solvers [3] for searching suitable automata. In the termination competition 2015, this approach has succeeded in proving non-termination of 31 string and term rewriting systems for which all other termination tools have failed. In particular, it is the first automated technique to prove non-termination of the S-rule.
Finally, we discuss how this technique can be extended to proving non-termination of cycle rewriting. Cycle rewriting a special case of graph rewriting where the graphs have the form of a cycle. Roughly speaking, a cycle is a word whose start and end have been connected.