---------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: July 10, 2010 (Edinburgh, UK) Chair: Juergen Giesl Secretary: Peter Schneider-Kamp 20 Participants: Maria Paola Bonacina Dan Dougherty Maribel Fernandez Juergen Giesl Bernhard Gramlich Tetsuo Ida Delia Kesner Helene Kirchner Salvador Lucas Christopher Lynch Aart Middeldorp Georg Moser (invited) Vincent van Oostrom Femke van Raamsdonk Kristoffer Rose (invited) Manfred Schmidt-Schauss Peter Schneider-Kamp Ralf Treinen Johannes Waldmann Hans Zantema ---------------------------------------------------------------------- Agenda: 1. Technical Presentations 2. International School on Rewriting (ISR) 3. Business Meeting ---------------------------------------------------------------------- 1. Technical presentations * Kristoffer Rose: Compromising Rewriting 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. * 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. * Georg Moser: Complexity Analysis of Programs by Rewriting In this talk I will first report on recent work in complexity of term rewrite systems. In particular I want to mention two recent results 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. * 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. * 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. * 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. * 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). * 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. * 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. This is joint work with Tony Bourdier, Horatiu Cirstea, and Mathieu Jaume. * Maria Paola Bonacina: Rewriting for Satisfiability Modulo Theories Advanced applications of theorem proving in analysis and synthesis of programs, such as invariant checking and invariant generation, require reasoning on problems that mix first-order logic, free symbols, equality, at least linear arithmetic, other first-order theories with symbols defined by axioms. Thus, there is a growth of theorem provers that integrate generic reasoning in first-order logic with equality, where rewriting plays a fundamental role, with specialized reasoning (e.g., DPLL(Gamma+T), LASCA, SUP(LA), SMELS). In this talk we will present DPLL(Gamma+T) and its proof of refutational completeness. This requires to instantiate classical rewriting concepts such as fairness and saturation, in a new context, where they get combined with new notions, such as variable-inactivity and smooth sets, and ingredients from other sorts of theorem proving such as iterative deepening. ---------------------------------------------------------------------- 2. International School on Rewriting (ISR) * Vincent van Oostrom: Report on ISR 2010 and Discussion on ISR A report on the International Summer School on Rewriting in Utrecht (The Netherlands) preceding FLoC 2010 was given. There was a broad geographic distribution of students, but few from outside Europe. The school had 48 registrations and 44 particpants attended the summer school. The basic and the advanced track were successfully completed by 21 participants each. The setup was similar to ISR in Obergurgl, but compressed into 5 days for organizational reasons. This did not allow for an excursion which was compensated by watching the soccer half finals. Otherwise, the integration into the Utrecht summer school was a good idea as this big summer school (130 courses, more than 2000 students) took over a lot of the organizational burden. There was evaluation feedback from 20 participants with the only major problem mentioned being the heat during this unusually hot early July. The buildings were not equipped for this, as weather normally is much cooler. Otherwise, the students were quite active and positive about their experience. The idea to have exercises seemed to be successful. * Aart Middeldorp: - no response to the initial call for locations for ISR 2012 - Leipzig and Valencia were proposed in second round * Johannes Waldmann: Proposal for ISR 2012 in Leipzig (Germany) - use regular lecture halls and seminar rooms on the campus - after July 23 due to lectures - lunch in the canteen for EUR 8 including salad, dessert, and drinks - accomodation in nearby (5 min walking) hotel for EUR 65 single, EUR 80 double, including breakfast - nice environment with student cafes, clubs, cinemas, ... - good public transportation, easy to reach by trains and planes - 7 days, four slots of 90 minutes - two tracks (basic/advanced) - 50 slots, 5 slots per lecture, 10 lecturers - max 25 students per track - per student EUR 150 (+ 300 for hotel) - lecturer EUR 100 (+ 200 hotel + 400 travel) - 5 students per lecturer implies EUR 300 per students - experience with WScT 08, WST 09, "Haskell in Leipzig", Mathematics Summer School - organizing team: Johannes + administration + students * Salvador Lucas: Proposal for ISR 2012 in Valencia (Spain) - June or July, best second half of July - main campus instead of city centre - sunny, green, quiet place for activities and leisure - well-connected with metro+tram and bus, easy to reach by plane - use regular classrooms of the university - computer labs available if needed - there is air-conditioning - no practical limit on the size of the groups - food in the canteen, price unclear, very nearby - accomodation in university residence (10 min walking) - one week duration - organization: ELP group (more than 5 persons) - estimated fee: EUR 366 single room, EUR 450 double room (including EUR 60 for excursion, excluding cost for lecturer, hopefully taken by institute) - nice leisure possibilities (park and cultural sites, beach very close, city centre) * There is a vote between the two proposals and Valencia is elected as the location for ISR 2012. * The Steering Committee of ISR is changed as follows: Salvador Lucas (as organizer of ISR 2012) joins the SC and Chris Lynch leaves the SC. ---------------------------------------------------------------------- 3. Business meeting * Juergen Giesl: next meeting of the IFIP working group There was consensus that the next IFIP WG 1.6 meeting should take place together with the next RTA in Novi Sad (Serbia). * Juergen Giesl: New members Georg Moser was invited as a new member to the WG after having been invited to the meetings in 2009 and 2010. * Ralf Treinen: RTA List of Open Problems Ralf presented current problems with RTA Loop being inactive. Ideas and proposals are invited. Ralf can be contacted personally or through email. ----------------------------------------------------------------------