|
Published: 25th February 2013 DOI: 10.4204/EPTCS.110 ISSN: 2075-2180 |
| 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 [11]. Challenges encountered during this
process and ideas for future development are presented and proposed for
discussion.
References
[1] 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.
[2] Hartmut Ehrig & Hans-Joerg Kreowski (1976): Parallelism of Manipulations in
Multidimensional Information Structures. In: MFCS, LNCS 45, pp. 284-293.
[3] Annegret Habel, Hans-Joerg Kreowski & Detlef Plump
(1987): Jungle Evaluation. In: ADT, LNCS 332, pp. 92-112.
[4] Annegret Habel, Juergen Mueller & Detlef Plump (2001): Double-pushout
graph transformation revisited. Mathematical Structures in Computer Science
11(5), pp. 637-688.
[5] Hans-Joerg Kreowski (1977): Transformations of Derivation Sequences in
Graph Grammars. In: FCT'77, pp. 275-286.
[6] Masahito Kurihara &
Azuma Ohuchi (1995): Modularity in Noncopying Term
Rewriting. J. of TCS 152(1), pp. 139-169.
[7] 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.
[8] 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.
[9] Grigore Rosu & Traian Florin Serbanuta (2010): An Overview of the K Semantic Framework.
J. of Logic and Algebraic Programming 79(6), pp. 397-434.
[10] Traian Florin Serbanuta (2010): A Rewriting Approach to Concurrent
Programming Language Design and Semantics. Ph.D. thesis,
University of Illinois.
[11] 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.