Published: 11th February 2011 DOI: 10.4204/EPTCS.48 ISSN: 2075-2180 |
Preface Rachid Echahed | |
Invited Presentation:
On the Observable Behavior of Graph Transformation Systems Reiko Heckel | 1 |
Invited Presentation:
From Infinitary Term Rewriting to Cyclic Term Graph Rewriting and back Patrick Bahr | 2 |
Term Graph Rewriting and Parallel Term Rewriting Andrea Corradini and Frank Drewes | 3 |
Invited Presentation:
Nominal Graphs Maribel Fernández | 19 |
Rule-based transformations for geometric modelling Thomas Bellet, Agnès Arnould and Pascale Le Gall | 20 |
Dependently-Typed Formalisation of Typed Term Graphs Wolfram Kahl | 38 |
PORGY: Strategy-Driven Interactive Transformation of Graphs Oana Andrei, Maribel Fernández, Hélène Kirchner, Guy Melançon, Olivier Namet and Bruno Pinaud | 54 |
A new graphical calculus of proofs Sandra Alves, Maribel Fernández and Ian Mackie | 69 |
Repetitive Reduction Patterns in Lambda Calculus with letrec (Work in Progress) Jan Rochel and Clemens Grabmayer | 85 |
This volume contains the proceedings of the Sixth
International Workshop on Computing with Terms and Graphs (TERMGRAPH 2011). The
workshop took place in Saarbruecken, Germany, on
April 2nd, 2011, as part of the fourteenth edition of the European Joint Conferences
on Theory and Practice of Software (ETAPS 2011).
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 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) and in York
(2009).
These proceedings contain six accepted papers and the
abstracts of three 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, proof methods, semantics as well
as application issues of term graph transformation.
We would like to thank all who contributed to the
success of TERMGRAPH 2011, 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 ETAPS 2011
organizing committee for their help in organizing TERMGRAPH 2011 at Saarbruecken, Germany.
February, 2011
Rachid Echahed
Program chair of TERMGRAPH2011
Program committee of TERMGRAPH 2011
Paolo Baldan University of Padova,
Italy
Andrea Corradini University
of Pisa, Italy
Frank Drewes Umea University, Sweden
Rachid Echahed CNRS,
LIG Lab., Grenoble, France (chair)
Tetsuo Ida University of Tsukuba, Japan
Wolfram Kahl McMaster University, Canada
Ian Mackie Ecole Polytechnique, France
Detlef Plump University of York, UK
While modelling or testing
component-based or service-oriented applications we often complement the
external perspective, describing the system in terms of its interactions, by
the internal one specifying its implementation. To formalise
this view, a graph transformation system is seen as an encapsulated component:
The implementation, described by type graph and rules, is equipped with an
interface (a signature of rules with parameters) defining possible
observations. We use this model to study the conditions under which
observations of interactions denote faithfully the internal concurrent
processes in the system.
The approach is based on observing
implementation-level dependencies and conflicts in terms of critical pairs, and
requiring that labels preserve these dependencies. Besides establishing the
fundamental relationship between transformations and observations, we
investigate possible applications in testing and software evolution.
This is a joint work with Tamim
Khan (University of Leicester, UK) and Rodrigo Machado (Universidade Federal do
Rio Grande do Sul, Porto Allegre, Brazil).
Cyclic term graph rewriting has been shown to be
adequate for simulating certain forms of infinitary
term rewriting. These forms are, however, quite restrictive and it would be beneficial
to lift these restriction at least for a limited class of rewriting systems. In
order to better understand the correspondences between infinite reduction
sequences over terms and finite reductions over cyclic term graphs, we explore
different variants of infinitary term graph rewriting
calculi.
To this end, we study different modes of convergence
for term graph rewriting that generalise the modes of
convergence usually considered in infinitary term
rewriting. After discussing several different alternatives, we identify a
complete semilattice on term graphs and derive from
it a complete metric space on term graphs. Equipped with these structures, we
can --analogously to the term rewriting case-- define both a metric and a
partial order model of infinitary term graph
rewriting. The resulting calculi of infinitary term
graph rewriting reveal properties similar to the corresponding infinitary term rewriting calculi.
Nominal syntax is an extension of standard,
first-order syntax that provides support for the specification of operators
with binding, thanks to an abstraction construct and the axiomatisation
of the alpha-equivalence relation. Nominal equivalence/unification/rewriting
are generalisations of the standard notions of
syntactic equivalence/unification/rewriting, to take into account
alpha-equivalence.
In this talk we will explore the relationships between
nominal and graph-based calculi, which have also been proposed as a
representation of systems with binding. On one hand, we will go from nominal
terms to nominal graphs -a graphical representation of nominal terms- and use
them to give a quadratic nominal unification algorithm (one of the most
efficient algorithms available so far to solve unification problems modulo
alpha). On the other hand, we will show that nominal syntax can be used to give
a formal, algebraic account of a general class of graph rewriting systems.