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.