----------------------------------------------------------------------
IFIP Working Group 1.6 on Term Rewriting
Report of the annual meeting: June 2, 2011 (Novi Sad, Serbia)
Chair: Juergen Giesl
Secretary: Peter Schneider-Kamp
13 Participants:
Takahito Aoto (for Yoshihito Toyama)
Santiago Escobar (for Salvador Lucas)
Juergen Giesl
Bernhard Gramlich
Pierre Lescanne
Aart Middeldorp
Georg Moser
Kristoffer Rose (invited)
Masahiko Sakai (invited)
Manfred Schmidt-Schauss
Aaron Stump (invited)
Johannes Waldmann
Hans Zantema
----------------------------------------------------------------------
Agenda:
1. Technical Presentations
2. International School on Rewriting (ISR)
3. Business Meeting
----------------------------------------------------------------------
1. Technical presentations
* Kristoffer Rose: Implementation Tricks That Make CRSX Tick
In this presentation I will walk through the implementation tricks used
in the CRSX (http://crsx.sourceforge.net) implementation of higher-order
rewriting to make rewriting work fast for rules that specify compilers
with symbol tables and syntax-directed rewrite schemes using higher-order
facilities, such as substitution for inlining and templates, and direct
manipulation of scopes and registers as first-class values. The tricks
include
(1) The role of sorts with linearity.
(2) Bound variable reuse.
(3) Weakness markers.
(4) Using forcer rules to avoid duplication of work.
(5) Parallellism in rewriting.
(6) Completion for almost-orthogonal pattern compilation.
I will also show how (some of) these tricks show up in generated C code
for rules.
* Manfred Schmidt-Schauss: Unification, Matching, and Rewriting of
Compressed Terms
An overview of the recent developments in efficient algorithms on
grammar-compressed terms is given.
This comprises: first-order unification, first-order matching using
singleton tree grammars (STGs); an extension of congruence closure
for efficiently solving the word problem of STG-compressed terms
w.r.t. a set of compressed ground term equations; and efficient variants
of term rewriting under STG-compression.
* Masahiko Sakai: CNFs with Elementary Symmetric Clauses and Their SAT
Solving
We introduces clauses, called ESk-clauses or simply ES-clauses, defined
based on elementary symmetric functions that return true if and only if
exactly k inputs are true. By summarizing some (OR-)clauses in CNF with
the equivalent ES-clause, we often obtain a shorter representation.
In this talk, we present an idea that incorporates the extension into a
two-literal-watching based practical solver, like Minisat, and give
some experimental results. We employed a hybrid one that deals
with OR-clauses by a two-literal-watching method and with ES-clauses by a
full-watching method. We implemented this hybrid mechanism into
Minisat, and the experiments show that this works nicely.
* Hans Zantema: Triangulation
Let ->_1 and ->_2 be terminating relations on a finite set satisfying
(1) every element has at most one incoming ->_1 arrow, and
(2) if a ->_2 b then there exists a c with c -> a and c -> b.
Here -> denotes the union of ->_1 and ->_2. Then -> is terminating.
In this presentation this property will be proved, and some extensions
to infinite sets will be discussed. In particular, we will sketch a proof
that triangulation preserves termination of codeterministic relations.
Here codeterministic means the above mentioned property (1), and
triangulation is a simplified version of completion: where in completion
for a pattern a <- o -> b the normal forms of a and b are ordered with
respect to some well-founded order, in triangulation the elements a
and b are ordered themselves.
This is joint work with Vincent van Oostrom.
* Johannes Waldmann: How 1000 people produced 3786 relative termination
problems in 72 hours
The yearly ICFP programming contest was run by HTWK Leipzig in 2010, and
the topic was (unsurprisingly) "relative termination of string rewriting
by matrices". Of course it wasn't that obvious to the participants, as we
added two levels of severe obfuscation. But once these entry barriers were
cracked, participants had to solve and pose termination problems. A subset
of those problems created by contest participants had been used in the 2010
Termination Competition, and it proved to be quite hard for current
termination tools. We report on interesting observations that could lead
to new insights in how to find matrix interpretations, and how to construct
hard termination problems. We also discuss an open problem on matrix
interpretations and linear derivational complexity.
http://www2010.icfpcontest.org/
* Aaron Stump: Harnessing the Power of Term Rewriting Theory for New
Applications
Over many years, term rewriting has developed a very deep body of theoretical
work on topics like termination and confluence. More recently, this work has
been complemented by highly sophisticated tools, such as termination checkers
and confluence checkers, implementing that theory. In this talk, I consider
some new applications for both the theory and the tools, in analysis of type
systems and in parsing. I will present preliminary results extending our
RTA '11 paper "Type Preservation as a Confluence Problem" to more advanced type
systems, in particular, Curry-style System F (also known as lambda-2). I will
also sketch ideas on applying termination and confluence checkers to
parsing.
* Bernhard Gramlich: On (Un)Soundness of Unraveling Deterministic
Conditional Rewrite Systems
We study (un)soundness of transformations of conditional term rewriting
systems (CTRSs) into unconditional term rewriting systems (TRSs). From
a logical as well as operational point of view soundness and completeness
of such transformations are indispensable. The focus here is on analyzing
(un)soundness of so-called unravelings, the most basic and natural class
of such transformations. We extend our previous analysis from normal
1-CTRSs to the more general class of deterministic CTRSs (DCTRSs) where
extra variables in right-hand sides are allowed to a certain extent.
We sketch how our previous soundness results based on weak left-linearity
and on right-linearity can indeed be extended from normal 1-CTRSs to DCTRSs.
Counterexamples show that such an extension to DCTRSs does not work for the
previous criteria which were based on confluence and on non-erasingness,
not even for right-stable systems. Yet, we prove a weaker soundness result
for confluent right-stable CTRSs, namely soundness w.r.t. reduction to
normal form. Finally we compare our approach and results with related ones,
especially with [Nishida et al./RTA'11].
(Joint work with Karl Gmeiner and Felix Schernhammer)
* Aart Middeldorp: Confluence Competition 2012
In this talk I outline ideas for an upcoming confluence competition.
----------------------------------------------------------------------
2. International School on Rewriting (ISR)
* Santiago Escobar: Report on ISR 2012
- ISR will take place on July 16-20, 2012 in Valencia.
- There will again be two tracks (one for newcomers and an advanced one focusing on more
recent developments).
- ISR will honor Alan Turing in his Centennial Year.
- A detailed schedule can be found on the web.
- ISR will take place in the university of Valencia, with good connections to the
city center and the airport.
- Valencia has good airline connections that make it easy to reach from almost
every location.
- Accomodation will be provided in university residences.
- The estimated amount needed to fund the lecturers is 6000 Euro.
- The estimated registration fees will be 500 Euro for students with single room
accomodation, 428 Euro for students with double room accomodation, 600 Euro for
non-students with single room accomodation, and 528 Euro for non-students with
double room accomodation.
* Comments from the audience:
- Will there be ECTS certificates for the courses? (J. Waldmann)
- Will there be exams for the basic track? (H. Zantema)
- It should be encouraged that lecturers stay for the whole week, not just
for the days of their course. (A. Middeldorp)
- It would be good to split lectures so that they take place on several
days. (J. Waldmann)
- Will the courses include homework exercises? (J. Giesl)
- Will the students receive printouts of the slides? (A. Middeldorp)
- It would be good to distribute posters to advertise the school. (G. Moser)
* Aart Middeldorp: Report of the Chair of the ISR Steering Committee
- The report on ISR 2010 was already given at the last meeting; no further report
on ISR 2010 will be provided.
- In 2013, a report on ISR 2012 is expected.
- The next ISR after the one in 2012 is scheduled for 2014. A call for proposals
will be issued before spring 2012.
- It would be desirable to find a location outside of Europe.
- A repository of information should be created for future organizers of ISR (containing
slides of lectures, information on the budget, lists of participants, etc.)
- It would be desirable to make the slides of lectures available online (after the
school). They could be hosted on the website of the IFIP-WG and there could be a link
from the rewriting homepage to that site.
- Every WG member should send at least one student to the school.
----------------------------------------------------------------------
3. Business meeting
- There was consensus that the next IFIP WG 1.6 meeting should take
place together with the next RTA in Nagoya (Japan).
- Membership issues were discussed and Kristoffer Rose was invited as a new member
to the WG after having been invited to the meetings in 2010 and 2011.
- Since the term of Juergen Giesl as the chair of the WG ends this autumn, there will be
an election of the chair, organized by the secretary of the WG.
- There was agreement that non-members of the WG should be allowed to attend the meeting
of the WG, except for the business meeting.
- Several suggestions were made for the program of future WG meetings:
* The meeting could be shortened to half a day.
* There should be less technical talks and more discussions (probably panel
discussions) and/or position statements.
* Before the meeting, there could be a call for discussion topics.
----------------------------------------------------------------------