----------------------------------------------------------------------
IFIP Working Group 1.6 on Term Rewriting
Report of the annual meeting: July 13, 2014 (Vienna, Austria)
Chair: Juergen Giesl
Secretary: Peter Schneider-Kamp
more than 29 participants, including:
Takahito Aoto (invited)
Mauricio Ayala-Rincon
Maria Paola Bonacina
Roberto di Cosmo
Nachum Dershowitz
Dan Dougherty
Gilles Dowek (invited)
Maribel Fernandez
Alfons Geser
Juergen Giesl
Nao Hirokawa (invited)
Delia Kesner
Gerwin Klein
Florent Jacquemard (invited)
Claude Kirchner
Helene Kirchner
Jose Meseguer
Aart Middeldorp
Georg Moser
Vincent van Oostrom
David Plaisted
Femke van Raamsdonk
Kristoffer Rose
Dana Scott
Sophie Tison
Yoshihito Toyama
Ralf Treinen
Claus-Peter Wirth
Hans Zantema
----------------------------------------------------------------------
Agenda:
1. Presentation by Takahito Aoto
2. International School on Rewriting (ISR)
3. Presentation by Gilles Dowek
4. Presentation by Maria Paola Bonacina
5. Presentation by Claude Kirchner and Discussion on Massive Open Online
Courses and Overlay Journals
6. Presentation by Nao Hirokawa
7. Presentation by Florent Jacquemard
8. Discussion on the Future of RTA
9. Discussion on the List of Open Problems in Rewriting
10. Business Meeting
----------------------------------------------------------------------
1. Takahito Aoto and Sorin Stratulat: Decision Procedures for Proving Inductive Theorems
without Induction
Automated inductive reasoning for term rewriting has been extensively studied in
the literature. Classes of equations and term rewriting systems (TRSs) with decidable
inductive validity have been identified and used to automatize the inductive reasoning. In
this talk, a new approach for deciding inductive theorems of TRSs is described. In
particular, we give procedures for deciding the inductive validity of equations in some
standard TRSs on natural numbers and lists. Our essential idea is to use the validity in
the initial algebras of TRSs, instead of validity guaranteed by existence of inductive
proofs. Contrary to previous decidability results, our procedures can automatically decide
without involving induction reasoning the inductive validity of arbitrary equations for
these TRSs, that is, without imposing any syntactical restrictions on the form of
equations.
----------------------------------------------------------------------
2. Aart Middeldorp: International School on Rewriting (ISR)
* Aart Middeldorp (ISR SC Chair): Overview on the history and organisation of ISR
* Mauricio Ayala-Rincon: Report on ISR 2014
- Carlos Castro is the main organizer of ISR 2014
- Mauricio Ayala-Rincon is a member of the organization committee.
- ISR will take place on August 25-29 in Valparaiso, Chile - a week before
WoLLIC (which is on September 1-4).
- The lecturers for the basic track will be Aart Middeldorp and Sarah Winkler.
The lecturers for the advanced track will be Mauricio Ayala-Rincon, Eduardo Bonelli,
Claude Kirchner, Helene Kirchner, Pierre-Etienne Moreau, Camilo Rocha, and
Johannes Waldmann.
- The lecturers have to pay their trips themselves, but the organizers pay the local
costs.
- The registration fee for students is 300 US$ for early registrations and 400 US$ for
late registrations.
- Up to now there are very few registrations (6 for the basic track and 5 for the
advanced track). The goal is to obtain at least 10 participants for each track.
- The problem is that students only get funding if they have a poster or talk at the
school. To solve this, the school could include a poster session where students can
present their posters.
- Aart Middeldorp suggests to include exams for the beginner track such that students can
obtain credits for their studies. However, Mauricio Ayala-Rincon does not think that
there will be exams at ISR 2014.
* Alfons Geser: Report on ISR 2015
- Alfons Geser and Johannes Waldmann will organize ISR 2015 in Leipzig, Germany.
- There will again be a basic track (with Aart Middeldorp as lecturer) and an advanced
track. A call for proposals for the advanced track has been issued.
- The date will be August 10-14, 2015. This is a week after CADE in Berlin.
- The date conflicts with the date of the ESSLLI summer school.
- The registration fee for students will be 300 Euro.
- Claude Kirchner suggests to make the material from the lectures freely available and to
use it for MOOCs. Alfons Geser has objections since then this material could be accessed
without fees. Gilles Dowek suggests that lecturers should give their courses twice (once
for the students at ISR and once for a video recording that is made available online).
* Gerwin Klein: Proposal for ISR 2016 in Sydney, Australia
- The proposal is to organize ISR 2016 in Sydney. The organizer would be Gabriele Keller
(University of New South Wales, UNSW)
- The UNSW is one of Australia's top universities with more than 50,000 students.
- ISR could be held on campus, where seminar rooms would be available for free.
- The university is located near the city center and the beach. It is easy to reach by
public transport.
- There are many restaurants nearby with lunch for approx. 10 AUS$.
- The basic track would be held as a UNSW course. There would be assignments during the
course and an exam after ISR.
- Accommodation would cost around 60-80 AUS$.
- The proposed date would be the last week of February or the week of July, 17. The date
should be left open until the dates of conferences in the same period is known.
- A registration fee for students only has to be imposed if the lecturers need funding.
- There will also be (some) lecturers from Australia. UNSW and NICTA offer a lot of
expertise in formal methods, verification, and functional programming.
- No co-location with other workshops or schools is currently planned.
- Video recording of the lectures might be possible.
- The proposal is accepted unanimously by the audience.
----------------------------------------------------------------------
3. Gilles Dowek and Ying Jiang: Rewriting, Proofs and Transition Systems
We give a new proof of the decidability of reachability in alternating pushdown
systems, showing that it is a simple consequence of a cut-elimination theorem for some
logic.
----------------------------------------------------------------------
4. Maria Paola Bonacina and David Plaisted: Semantically-Guided Goal-Sensitive Theorem
Proving
SGGS, for Semantically-Guided Goal-Sensitive theorem proving, is a new inference
system for first-order logic. It was inspired by the idea of generalizing to first-order
logic the model-based style of the Davis-Putnam-Logemann-Loveland (DPLL) procedure for
propositional logic. Model-based reasoning is a key feature of SAT solvers, SMT solvers,
and model-constructing decision procedures for specific theories, and a crucial ingredient
to their practical success. However, model-based reasoning in first-order logic is
challenging, because the logic is only semi-decidable, the search space is infinite, and
model representation is harder than in the propositional case. SGGS meets the challenge by
realizing a seemingly rare combination of properties: it is model-based a la DPLL;
semantically guided by an initial interpretation, to avoid blind guessing in an infinite
search space; proof confluent, to avoid backtracking, which may be cumbersome for
first-order problems; goal-sensitive, which is important when there are many axioms or a
large knowledge base; and it uses unification to avoid enumeration of ground terms, which
is inefficient, especially for rich signatures. In terms of operations, SGGS combines
instance generation, resolution, and constraints, in a model-centric approach: it uses
sequences of constrained clauses to represent models, instance generation to extend the
model, resolution and other inferences to repair it. This talk advertises SGGS to the
rewriting community, presenting the main ideas in the method: a main direction for future
work is extension to first-order logic with equality, which requires rewrite-based
reasoning. A manuscript including all aspects of SGGS, the technical details, the proofs
of refutational completeness and goal-sensitivity, a comparison with other work (e.g.,
resolution with set of support, the disconnection calculus, the model evolution calculus,
the Inst-Gen method) and more references, is available.
----------------------------------------------------------------------
5. Claude Kirchner: Impacts of the Digital Revolution on two Main Activities of
Scientists: Teaching and Publishing
- The talk is followed by a discussion on massive open online courses and overlay
journals.
- Existing academic social networks like Mendeley and ResearchGate are presented and
discussed.
- Claude Kirchner reports on the EPISCIENCES platform implemented by INRIA to create
overlay journals on top of public archives like arXiV and HAL.
- Here, authors put their papers on public archives and then ask an editorial board of an
overlay journal to evaluate it. Following the reviews, the authors can revise their
paper, but all versions remain accessible to the public. Final accepted versions are
marked accordingly.
----------------------------------------------------------------------
6. Nao Hirokawa, Aart Middeldorp and Georg Moser: Basic Normalization
The Normalization Theorem (O'Donnell 1977) states that for every left-normal
orthogonal rewrite system, the leftmost outermost strategy reduces any term to the normal
form if it exists. Although the theorem ensures the normalization property of important
systems like Combinatory Logic, the left-normality condition rules out many functional
programs. We revisit the problem to seek a solution for normalization of the leftmost
outermost strategy.
----------------------------------------------------------------------
7. Florent Jacquemard, Jean Bresson and Pierre Donat-Bouillud: Rhythm Tree Rewriting
In traditional western music notation, the durations of notes are expressed
hierarchically by recursive subdivisions. This led naturally to a tree representation of
melodies widespread in systems for assistance to music authoring. We will see how term
rewriting techniques can be applied to computer music problems, in particular to the
problem of rhythm quantization: the transcription of a sequence of dates (real time
values) into a music score. Besides the question of rhythm representation, an interesting
problem in this context is the design and concise description of large rewrite rule sets
and decision problems for these descriptions.
----------------------------------------------------------------------
8. Georg Moser: Discussion on the Future of RTA
- There is concern about the lack of application papers at RTA.
- At RTA 2015, there should be 3 categories for papers: full papers, system descriptions,
and application papers.
- Juergen Giesl remarks that a similar discussion already took place at the last meeting
of the IFIP WG 1.6 and that the steering committee had agreed to inform Gilles Dowek (the
PC Chair of RTA 2014) accordingly, but nothing had happened.
- Jean-Pierre Jouannaud instead suggests to invite researchers to RTA in order to extend
rewriting to new directions.
- Gilles Dowek would like to clarify what is meant by "applications" in this context.
- Juergen Giesl states that clear criteria are needed to define what is expected from
papers in the different categories. These criteria are needed both for the authors and
the referees.
- Jean-Pierre Jouannaud remarks that the reviews at RTA are often harsher than at other
more prestigious conferences.
- It is discussed whether there should be quotas for application papers, but Georg Moser
is not in favor of it.
- Kristoffer Rose points out that application papers should not be marked as such in the
proceedings. They should have the same status as full papers.
- Helene Kirchner says that that there are areas that use rewriting, but whose topics are
very far away from RTA. It is not clear why RTA should attract these papers.
- Jose Meseguer mentions that we should also be open for new research directions.
- Gilles Dowek thinks that potential authors hardly read the call-for-papers. One should
rather focus on certain applications (e.g., bio-informatics or music) and address people
from these areas directly.
- Nachum Dershowitz discusses the potential restriction that PC members may only submit
application papers.
- Maribel Fernandez suggests to highlight a certain sub-area each year for RTA.
----------------------------------------------------------------------
9. Nachum Dershowitz & Hans Zantema: Open Problems in Rewriting
- Hans Zantema explains the list of open problems in rewriting which exists since RTA
1995.
- Since 2012, Hans Zantema maintains the list (he took it over from Ralf Treinen).
- Ralf Treinen had developed a system for automating tasks concerned with the maintenance
of the list, but this is difficult to use for others.
- Nachum Dershowitz asked his admins who managed to get the system running again.
- In the last years, there were no reactions and no new problems submitted. Most of the
problems are from the 90s.
- Nachum Dershowitz suggests to switch to a wiki-system with a moderator.
- Jean-Pierre Jouannaud thinks that someone should write a paper on the open problems of
the last RTA(s).
- Gilles Dowek suggests to mark the 5 most important open problems on the list.
- Ralf Treinen asks which motivation people could have to submit open problems. They might
do it in order to get cited.
- Gilles Dowek remarks that open problems should be clear questions and not problems that
just require that some topic should be investigated.
- The audience votes the suggestion to switch to a wiki-system. There are 9 Yes votes, 3
No votes, and 1 Abstain vote. Nachum Dershowitz takes the initiative and will be the
moderator of the wiki.
----------------------------------------------------------------------
10. Juergen Giesl: Business Meeting
- Nao Hirokawa is invited as a new member to the WG after having been invited to the
meetings in 2012 and 2014.
- Florent Jacquemard is invited as a new member to the WG after having been invited to the
meetings in 2013 and 2014.
- Before the meeting in 2013, the strict rule was announced that the membership expires
for members who are not present at 3 meetings in a row. Therefore, members who do not
attend any of the meetings in 2013, 2014, and 2015 will be removed from the WG after the
meeting in 2015.
- Those member that are "at risk" (i.e., who would be removed if they do not attend the
meeting in 2015) should be informed by email well in advance before the meeting in
2015. In this way, they can still attend the meeting in order to remain in the WG.
- There is an unanimous vote that the next IFIP WG 1.6 meeting should take place at
RTA/TLCA in June 2015 in Warsaw, Poland.
- Juergen Giesl reports on the IFIP conferences.
- Since Juergen Giesl's second term as chair of the WG expires this year, he cannot
be re-elected anymore. He will therefore organize the election of the next chair of the
WG this fall.
- Jose Meseguer suggests to discuss over the email list who might become honorary member
instead of being removed from the WG.
- Juergen Giesl suggests to contact researchers that would be removed and if they are
really still interested in rewriting, one could offer them to stay in the WG.
- Georg Moser would like to have more young people in the WG.
- Kristoffer Rose and Georg Moser would like the WG to take over the rewriting homepage.
----------------------------------------------------------------------