----------------------------------------------------------------------
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.
----------------------------------------------------------------------