Preface

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.

Program Committee

• Andrea Corradini [co-chair], Dipartimento di Informatica, Pisa, Italy
• Maribel Fernández, King's College London, UK
• Ian Mackie, École Polytechnique, France
• Detlef Plump, University of York, UK
• Femke van Raamsdonk, Vrije Universtiteit Amsterdam, The Netherlands
• Hans Zantema [co-chair], Eindhoven University of Technology, The Netherlands

Termination of Graph and Term Graph Rewriting

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.

Non-Termination of Cycle Rewriting by Finite Automata

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.

References

1. H. P. Barendregt (1984): The Lambda Calculus, its Syntax and Semantics, revised edition. Studies in Logic and The Foundations of Mathematics 103, North-Holland, doi:1016/B978-0-444-87508-2.50006-X.
2. H.P. Barendregt, J. Endrullis, J.W. Klop and J. Waldmann (2016): Dance of the Starlings. To be published.
3. N. Eén and A. Biere (2005): Effective Preprocessing in SAT through Variable and Clause Elimination. In: Proc. Conf. on Theory and Applications of Satisfiability Testing (SAT'05), LNCS 3569, Springer, pp. 61-75, doi:10.1007%2F11499107_5.
4. F. Emmes, T. Enger and J. Giesl (2012): Proving Non-looping Non-termination Automatically. In: International Joint Conference on Automated Reasoning (IJCAR 2012), LNCS 7364, Springer, pp. 225-240, doi:10.1007%2F978-3-642-31365-3_19.
5. J. Endrullis, H. Geuvers and H. Zantema (2009): Degrees of Undecidability in Term Rewriting. In: Proc. Int. Workshop on Computer Science Logic (CSL 2009), LNCS 5771, Springer, pp. 255-270, doi:10.1007/978-3-642-04027-6_20.
6. J. Endrullis, R.C. deVrijer and J. Waldmann (2010): Local Termination: Theory and Practice. Logical Methods in Computer Science 6(3), doi: 10.2168/LMCS-6(3:20)2010.
7. J. Endrullis and H. Zantema (2015): Proving Non-Termination by Finite Automata. In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics, Schloss Dagstuhl, doi:10.4230/LIPIcs.RTA.2015.160.
8. A. Geser & H. Zantema (1999): Non-looping String Rewriting. RAIRO Theoretical Informatics and Applications 33(3), pp. 279-302, doi:10.1051/ita:1999118.
9. J. Waldmann (1998): The Combinator S. Ph.D. thesis, Friedrich-Schiller-Universität Jena.

   ---