IFIP-WG1.6 on Saturday, July 10th

09:00‑10:00 Session 1
Location: IF 1.15
09:00 Kristoffer Rose
Compromising Rewriting (Abstract)

This talk presents an overview of the theoretic aspect of my (so far) five year effort to make the CRSX combinatory reduction systems higher order rewriting engine useable for specifying all aspects of optimizing compilers as abstractly as possible without losing the ability to generate executable production compilers directly from the specification source.

09:30 Beniamino Accattoli and Delia Kesner
The structural lambda-calculus

Inspired from a recent graphical formalism for lambda-calculus based on linear logic technology, we introduce an untyped structural lambda-calculus, called lambda_j, which combines actions at a distance with exponential rules decomposing the substitution by means of weakening, contraction and derelicition. First, we prove some fundamental properties such as confluence and preservation of beta-strong normalisation. Secondly, we use lambda_j to describe known notions of developments and superdevelopments, as well as a new more general one, called here XL-superdevelopment. Then, we show how to reformulate Regnier's sigma-equivalence on lambda_j so that it becomes a strong bisimulation. Finally, we show that explicit composition or de-composition of substitutions can be added to lambda_j still preserving beta-strong normalisation.

10:30‑12:30 Session 2
Location: IF 1.15
10:30 Georg Moser
Complexity Analysis of Programs by Rewriting

In this talk I will first report on recent work in complexity of term rewrite system. In particular I want to mention two recent result that bring us a bit closer to the goal of making complexity analysis of rewrite systems more "modern" and "useful".

In the remainder of the talk I will report on work in progress on the the complexity analysis of Java ByteCode programs by rewriting.

11:00 Salvador Lucas
Matrix interpretations over the rationals and matrix interpretations over the naturals

Matrix interpretations generalize linear polynomial interpretations and have been proved useful in the implementation of tools for automatically proving termination of Term Rewriting Systems (TRSs). In view of the successful use of rational coefficients when polynomial interpretations are used in proofs of termination of rewriting, we have recently generalized traditional matrix interpretations (using natural numbers in the matrix entries) to incorporate real numbers. However, recent results which formally prove that, under some conditions, linear polynomials over the rationals are strictly more powerful than linear polynomials over the naturals for proving termination of rewrite systems failed to be extended to matrix interpretations. We report on some progress regarding this problem.

11:30 Bernhard Gramlich
Conditional via Unconditional Rewriting - Some Recent Developments

Conditional term rewriting systems (CTRSs) naturally arise in many settings, but are well-known to be substantially more complex and involved than unconditional ones (TRSs), concerning both the theoretical analysis and their practical realization. For this reason, various transformational approaches have been designed in the past in order to simulate CTRSs via TRSs. These approaches are appealing in the sense that the rich knowledge about unconditional term rewriting and its implementation becomes readily applicable for conditional rewriting. On the other hand, various basic issues and questions about such transformational approaches are still not yet fully understood.

In the talk we will report on our recent and ongoing research efforts that concentrate on some crucial questions in the area. First of all, we will sketch a unifying framework for such transformations that covers most of the existing approaches. One major advantage of this general approach is a systematic and unified terminology for properties of such transformations, e.g. preservation properties like soundness and completeness. Second, we will deal with the precise relationships between (properties of) CTRSs and their transformed TRSs and show that via imposing certain (context-sensitivity) restrictions on rewriting in the transformed TRSs remarkably precise relationships and characterizations become possible. Finally, we will also discuss one of the main inherent problems of such transformational approaches, namely unsoundness (w.r.t. simulating the original system), in more depth. Via a refined analysis we are able to shed some new light on the essential sources of this unsoundness phenomenon and to derive a couple of new sufficient conditions that guarantee soundness of the underlying transformation.

12:00 Hans Zantema
Proving equality of infinite terms: co-inductive theorem proving

Inductive theorem proving serves for proving equality of finite terms automatically. But how to prove equality of infinite terms? For instance, one can define the infinite stream 01010101... by alt = 0:1:alt. Alternatively, one can define it as zip(zeros,ones), where zip, zeros and ones are defined by zeros = 0:zeros, ones = 1:ones, zip(x:xs,ys) = x:zip(ys,xs). How to prove equalities like alt = zip(zeros,ones) automatically?

In this presentation we will discuss a number of options. One way to prove s = t for ground terms s,t is to show that the equations for s have a unique solution, and t satisfies these equations. Another approach is in constructing a bisimulation relation. Finally one can use circular coinduction as developed by G. Rosu, and for which D. Lucanu and G. Rosu developed their tool circ. Most of these techniques are based on rewriting and equational reasoning.

14:00‑15:00 Session 3
Location: IF 1.15
14:00 Maribel Fernandez
PORGY: a strategy driven interactive environment for visualisation and transformation of graphs

PORGY is an interactive visual environment for graph transformations based on rewrite rules and controlled by strategies. For instance, in such a setting, we can model interaction networks or biochemical pathways whose states are represented by port graphs and evolutions are driven by rules and strategies. The visualisation features provide the user with useful insights on possible behaviours of the model and its properties. We will describe a strategy language to control rule applications, the structures used to represent execution traces and navigate in the derivation history, and various ways to visualise port graphs and rewrite rules.

The design and implementation of PORGY is currently under way, as part of the PORGY project (INRIA and King's College London: Oana Andrei, Maribel Fernandez, Helene Kirchner, Guy Melancon, Olivier Namet, Bruno Pinaud).

14:30 Tetsuo Ida
Graph Rewriting in Computational Origami

The talk is about the application of rewriting techniques to modeling geometrical construction, in particular origami (paper fold). Origami construction is a finite sequence of fold steps, each consisting in finding a fold line, dividing origami faces and rotating the faces along the fold line. We model origami paper by a set F of faces over which we specify relations of superposition S and adjacency A, thereby defining a structure (F, S, A), to be called abstract origami.A fold line is determined by a specific parametrized fold method. In each step of the construction, the structure of origami is changed; some faces are divided and moved, new faces are created and hence the relations over the faces change. The origami construction is therefore modeled as rewrite sequences of abstract origamis. To reason about specific properties of the origami construction and to implement the construction computationally, we concretize the abstract origami as a labeled hypergraph and the rewrite sequence as a graph rewriting of the labeled hypergraphs. We explain some of the algorithms developed for the graph rewritings and show the visualization of the process of graph rewriting in some classical origami constructions.

15:30‑17:30 Session 4
Location: IF 1.15
15:30 Temur Kutsia
Parameterized Generalization of Unranked Terms

We develop a generalization (anti-unification) algorithm for unranked terms, which is parameterized by a relation on strings, called the rigidity relation. The terms may contain individual and sequence variables. At each step, the algorithm should decide which subsequence of subterms of the given terms is to be (structurally) retained in the generalization. This sequence is determined by the rigidity relation on the strings of top function symbols of those subterms. Sequence variables help to fill in gaps in the generalization, and individual variables abstract single (sub)terms with different top function symbols.

Varying the rigidity relation, one can obtain generalizations with different structural properties. Our algorithm is designed to compute least general generalizations modulo the given rigidity relation. The techniques can be useful is software code clone detection, where different rigidity relations can facilitate finding clones of different types.

This is a joint work with Jordi Levy and Mateu Villaret.

16:00 Helene Kirchner
Operational Specification and Verification of Security Policies

We propose a formal framework for the specification and validation of security policies. A security policy responds to the authorization requests of a system according to a certain number of rules and to the configuration of the system at the moment of the request. A system constrained by a security policy consists of two parts: on one hand, the set of rules describing the way the decisions are taken and on the other hand, the information used by the rules and the way they evolve in the system. We call the former the policy rules and the latter the security system. Policy rules are constrained rewrite rules, whose constraints are safe first-order formulas on finite domains, which provides enhanced expressive power compared to classical security policy specification approaches like the ones using Datalog, for example. Our specifications have an operational semantics based on transition and rewriting systems and are thus executable. This framework also provides a common formalism to define, compare and compose security systems and policies. We define transformations over security systems in order to perform validation of classical security properties.

16:30 Maria Paola Bonacina
Research activities related to term rewriting at the Universita` degli Studi di Verona

I have not had the pleasure to participate in the meeting of the IFIP Working Group 1.6 on Term Rewriting since its 2002 edition. Therefore, in this talk I'll give a short overview of my research program in recent years. I'll briefly mention recently published results and current directions, including: * Rewrite-based satisfiability procedures for theories and combinations of theories [joint works with Alessandro Armando, Mnacho Echenim, Silvio Ranise and Stephan Schulz]. * Rewrite-based decision procedures for satisfiability [joint work with Mnacho Echenim]. * Canonicity for ground Horn theories, including implicational systems [joint work with Nachum Dershowitz]. * Decision procedures for satisfiability, which integrate an SMT-solver, a rewrite-based engine and speculative inferences [joint work with Chris Lynch and Leonardo de Moura]. * Semantically-guided goal-sensitive theorem proving [joint work with David Plaisted]. For each topic I'll highlight the role played by rewriting. If time allows it, I may select one of this topics and discuss it further.

17:00 Vincent van Oostrom. Report on ISR 2010 and Discussion on ISR
17:15 Business Meeting