Published: 25th February 2013|
|Preface Rachid Echahed and Detlef Plump|
|On the Concurrent Semantics of Transformation Systems with Negative Application Conditions Andrea Corradini||1|
|Programming Language Semantics using K - true concurrency through term graph rewriting- Traian Florin Serbanuta||2|
|Non-simplifying Graph Rewriting Termination Guillaume Bonfante and Bruno Guillaume||4|
|Convergence in Infinitary Term Graph Rewriting Systems is Simple (Extended Abstract) Patrick Bahr||17|
|Linear Compressed Pattern Matching for Polynomial Rewriting (Extended Abstract) Manfred Schmidt-Schauss||29|
|Evaluating functions as processes Beniamino Accattoli||41|
|Term Graph Representations for Cyclic Lambda-Terms Clemens Grabmayer and Jan Rochel||56|
|Bigraphical Nets Maribel Fernández, Ian Mackie and Matthew Walker||74|
This volume contains the proceedings of the Seventh International Workshop on Computing with Terms and Graphs (TERMGRAPH 2013). The workshop took place in Rome, Italy, on March 23rd, 2013, as part of the sixteenth edition of the European Joint Conferences on Theory and Practice of Software (ETAPS 2013).
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, as witnessed by the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the modelling of biological or chemical abstract machines, and 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 this workshop is 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.
Previous editions of TERMGRAPH series were held in Barcelona (2002), in Rome (2004), in Vienna (2006), in Braga (2007), in York (2009) and in Saarbrücken (2011).
These proceedings contain six accepted papers and the abstracts of two invited talks. All submissions were subject to careful refereeing. The topics of accepted papers range over a wide spectrum, including theoretical aspects of term graph rewriting, concurrency, semantics as well as application issues of term graph transformation.
We would like to thank all who contributed to the success of TERMGRAPH 2013, especially the Program Committee for their valuable contributions to the selection process as well as the contributing authors. We would like also to express our gratitude to all members of the ETAPS 2013 organizing committee for their help in organizing TERMGRAPH 2013.
|February, 2013||Rachid Echahed and Detlef Plump|
|Patrick Bahr||University of Copenhagen, Denmark|
|Paolo Baldan||University of Padova, Italy|
|Frank Drewes||Umea University, Sweden|
|Rachid Echahed||CNRS, University of Grenoble, France (co-chair)|
|Maribel Fernandez||King's College London, UK|
|Clemens Grabmayer||Utrecht University, the Netherlands|
|Wolfram Kahl||McMaster University, Canada|
|Ian Mackie||Ecole Polytechnique, France|
|Detlef Plump||University of York, UK (co-chair)|
Thibaut Balabonski, Simon Gay, Dimitri Hendriks and Yuhang Zhao
A rich concurrent semantics has been developed along the years for graph transformation systems, often generalizing in non-trivial ways concepts and results fist introduced for Petri nets. Besides the theoretical elegance, the concurrent semantic has potential applications in verification, e.g. in partial order reduction or in the use of finite prefixes of the unfolding for model checking. In practice (graph) transformation systems are often equipped with Negative Application Conditions, that describe forbidden contexts for the application of a rule. The talk will summarize some recent results showing that if the NACs are sufficiently simple ("incremental") the concurrent semantics lifts smoothly to systems with NACs, but the general case requires original definitions and intuitions.
This is a joint work with Reiko Heckel, Frank Hermann, Susann Gottmann and Nico Nachtigall
Developed as a rewriting formalism for describing the operational semantics of programming languages, the K framework [8, 9, 10] proposes a new notation for (term) rewrite rules which identifies a read-only context (or interface) which is not changed by a rewrite rule. This allows for enhancing the transition system to model one-step concurrency with sharing of resources such as concurrent reads of the same memory location and concurrent writes of distinct memory locations.
Given that graph transformations offer theoretical support for achieving parallel rewriting with sharing of resources [2, 5, 4], and that the term-graph rewriting approaches were developed as sound and complete means of representing and implementing rewriting [1, 7, 3, 6], it seems natural to give semantics to K through term-graph rewriting. However, the existing term-graph rewriting approaches aim at efficiency: rewrite common subterms only once, without attempting to use context-sharing information for enhancing the potential for concurrency. Consequently, the concurrency achieved by current term-graph rewriting approaches is no better than that of standard rewriting. Moreover, the efficiency gained by sharing subterms can inhibit behaviors in non-deterministic (e.g., concurrent) systems.
This talk summarizes the efforts of endowing K with a (novel) term-graph rewriting semantics developed with the aim of capturing the intended concurrency the K framework . Challenges encountered during this process and ideas for future development are presented and proposed for discussion.
 Hendrik Pieter Barendregt, Marko C. J. D. van Eekelen, John R. W. Glauert, Richard Kennaway, Marinus J. Plasmeijer & M. Ronan Sleep (1987): Term Graph Rewriting. In: PARLE, pp. 141-158.
 Hartmut Ehrig & Hans-Joerg Kreowski (1976): Parallelism of Manipulations in Multidimensional Information Structures. In: MFCS, LNCS 45, pp. 284-293.
 Annegret Habel, Hans-Joerg Kreowski & Detlef Plump (1987): Jungle Evaluation. In: ADT, LNCS 332, pp. 92-112.
 Annegret Habel, Juergen Mueller & Detlef Plump (2001): Double-pushout graph transformation revisited. Mathematical Structures in Computer Science 11(5), pp. 637-688.
 Hans-Joerg Kreowski (1977): Transformations of Derivation Sequences in Graph Grammars. In: FCT'77, pp. 275-286.
 Masahito Kurihara & Azuma Ohuchi (1995): Modularity in Noncopying Term Rewriting. J. of TCS 152(1), pp. 139-169.
 Detlef Plump (1993): Hypergraph rewriting: critical pairs and undecidability of confluence. In: Term graph rewriting: theory and practice, John Wiley and Sons Ltd., pp. 201-213.
 Grigore Rosu (2003): CS322, Fall 2003 - Programming Language Design: Lecture Notes. Technical Report UIUCDCS-R-2003-2897, University of Illinos at Urbana Champaign. Lecture notes of a course taught at UIUC.
 Grigore Rosu & Traian Florin Serbanuta (2010): An Overview of the K Semantic Framework. J. of Logic and Algebraic Programming 79(6), pp. 397-434.
 Traian Florin Serbanuta (2010): A Rewriting Approach to Concurrent Programming Language Design and Semantics. Ph.D. thesis, University of Illinois.
 Traian Florin Serbanuta & Grigore Rosu (2012): A Truly Concurrent Semantics for the K Framework Based on Graph Transformations. In Hartmut Ehrig, Gregor Engels, Hans-Joerg Kreowski & Grzegorz Rozenberg, editors: ICGT, Lecture Notes in Computer Science 7562, Springer, pp. 294-310. Available at http://dx.doi.org/10.1007/978-3-642-33654-6_20.