IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: May 31, 2004 (Aachen, Germany) Chair: Claude Kirchner Secretary: Laurent Vigneron Participants: F. Baader, D. Dougherty (invited), J. Giesl, B. Gramlich, T. Ida, C. Kirchner, H. Kirchner, J. W. Klop, P. Lescanne, S. Lucas, A. Middeldorp, F. Otto, M. Schmidt-Schauss, R. Thiemann (invited), Y. Toyama, V. van Oostrom, F. van Raamsdonk, L. Vigneron, H. Zantema ---------------------------------------------------------------------- Agenda: 1. Progress Reports 2. Technical Presentations 3. Teaching Issues 4. General Discussion on Foreseeing Challenges for Rewriting 5. Business Meeting ---------------------------------------------------------------------- 1. Progress reports ----------------------------------------- * Femke van Raamsdonk: for the Netherlands Presentation of the different activities in each domain: Termination: iterative path orders; application of termination to liveness issues; TORPA, a tool for termination of string rewriting. Semantics: validity is derivability is convertibility; Boehm-like trees for term rewriting systems. Background: residual algebras; decomposition orders; proof systems for recursive types. Varia: match bound techniques; undecidable approximations; reduction cycles. Higher-order rewriting: optimal implementation of lambda-calculus; erasure and termination in higher-order rewriting; higher-order rewriting with types and arities; well-foundedness of HORPO in Coq. ----------------------------------------- * Friedrich Otto: for Kassel Presentation of a recent work on invariant properties in string-rewriting systems (done with Kobayashi and Pride), and of XSSR, an experimental system for string rewriting. ----------------------------------------- * Manfred Schmidt-Schauss: for Frankfurt The main research domains are listed: - Unification: bounded higher-order (with K. Schulz, Munich) - Context matching (with J. Stuber, Nancy) - Monadic second-order unification (with J. Levy, M. Villaret, Barcelona) - Operational semantics of higher-order languages using small-step semantics: focus on higher-order, non-determinism, sharing ----------------------------------------- * Claude Kirchner: for Nancy The research groups in Nancy working on domains related to term rewriting are: Adage, Calligramme, Cassis, Modbio, Protheo. The work done by the Protheo group concerns the follogins subjects. Rewriting calculus: - as a general framework embedding rewriting and lambda-calculus: type systems, normalization, graph rewriting calculus, models of the rewriting calculus Rewriting and production systems: - collaboration with the "constraints" project and ILOG - which semantics? - which proof system? ELAN and TOM: - ELAN3: stable and maintained version - ELAN-Coq: skeptical cooperation scheme for AC equational reasoning - TOM v2.0, Eclipse plug-in; towards formal islands Objectives: adding rewriting to many languages: JTOM (TOM for Java), JTOM for XML, CTOM (TOM for C), CamlTOM Proofs: - Coq modulo - Proof terms for termination (polynomial interpretation) Applications: - modelling chemical reactions - web (Rewerse NoE) - termination (Cariboo, Types for termination) ----------------------------------------- Salvador Lucas: for Valencia In Valencia, the ELP group contains 25 people, including 14 PhD strudents. Its main research topic is about extensions of logic programming. Its ongoing collaborations concern the following topics: - declarative debugging of TRS - debugging of WWW sites - termination of Maude pgs - termination fo context rewriting And the hot rewriting topics are: - termination of Maude programs - extension of Maude (on-demand evaluation, narrowing) - implementation of CSRPO onto MU-TERM - interoperability of tools (.NET, XML+WWW) - termination of Haskell programs - extension of Curry (natural narrowing) - termination techniques for model-checking of tccp programs ---------------------------------------------------------------------- 2. Technical Presentations * On the connection between higher-order rewriting and operational semantics by Manfred Schmidt-Schauss * Some formal calculi for modeling programming languages by Dan Dougherty * New Result on Combining Decision Procedures for the Word Problem and Related Problems by Franz Baader (joint work with Silvio Ghilardi and Cesare Tinelli) ---------------------------------------------------------------------- 3. Teaching Issues Each participant explains shortly the teaching issues in his/her university. * in Aachen: The term rewriting lecture is popular, as graduate course, because students follow some theoretical courses as undergraduate. Contents: parts of Baader-Nipkow book. A lot of students complete their master thesis in this domain. Lambda-calculus is teached as part of functional languages course. * at ENS Lyon: Three courses are related to term rewriting: logic (proof theory, connection proof-computation); rewriting (Baader-Nipkow book, Groebner bases,...); semantics (explicit substitutions). * in Tsukuba: Term rewriting is teached as part of the functional programming course. * in Insbruck: Term rewriting is teached for undergraduate students (for attracting them for masterdegree). * in Dresden: There is an international master course in computational logic, attracting many foreign students. Courses on term rewriting are all based on the Baader-Nipkow book. However, a lot of students do not follow theoretical courses, so there are very few PhD students in this domain. * in Worcester: Very few students follow theoretical courses, because this is difficult to find a job after a PhD in a theoretical domain. The main course related to term rewriting is on logic for computer science. * in Amsterdam: There is one course on term rewriting and several related courses (process algebra, model checking, co-inductive techniques, ...). * in Utrecht: Students in cognitive science follow two courses related to term rewriting: types theory; optimal implementation of lambda-calculus. * in Sendai: Students are interesting by big applied projects, and only graduate students have a term rewriting course. * in Vienna: The only course that is related to term rewriting is on computation intelligence, and contains parts on logic and lambda-calculus. * in Nancy: At the master level, one course devotes 10 hours to rewriting. Several others use the concept. ---------------------------------------------------------------------- 4. General Discussion on Foreseeing Challenges for Rewriting The discussion about the main challenges related to term rewriting raises the following research topics: - graph theory - non-termination problems (bisimulation, ...) - first-order termination (Isabelle) - use of object calculus - combination problems for non-disjoint signatures - the rewriting calculus - programs transformation - properties of rewriting when no termination or confluence (properties of reachability, strategies): formal framework needed - to mix logical deduction with statistical information (useful for decision making) - abstract knowledge - modularity and strategies: non disjoint unions (non left-linear rewriting) - transformation from ML programs to rewriting rules (priorities lost) - technical implementations of term rewriting About teaching, the following points are discussed: - teaching term rewriting is very important - to provide graphic supports (more attractive for students), with macromedia animation for example The term rewriting community has to enlarge its scope concerning: - applications: they exist, so we need to attract industrial partners - other communities: higher-order, biology, web semantic, ... this relation has to be based on stable tools, so we have to develop more of them Pierre Lescanne raises the problem that the rewriting mailing list has become a list for announcing events; this is no more a forum of discussion. Its has to be reactivated, like the list of open problems that is not developed as it should be. Concerning attracting applications, Franz Baader proposes to permit the publication of application papers, even if they have already been published in application conferences. And papers submitted to RTA can be of related domains, as soon as their basis is rewriting. A remark is done on the expression "term rewriting": this is not very positive and attractive. How could it be possible to improve this? Finally, thanks to this IFIP working group, our community is recognized by theoretical science. So we have to use this for attracting related domains and applications. ---------------------------------------------------------------------- 5. Business meeting ----------------------------------------- * News from the IFIP: The 2004 IFIP World Computer Congress will hold in Toulouse, August 22-27: it will contain many events, including the third international conference on Theoretical Computer Science, and a TC1 meeting. ----------------------------------------- * Membership: Some of the members of the group have not participated to meetings for years. So we are going to apply the membership rules and exclude them. Some other members have agreed to leave the group, such as U.Martin, M.Venturilli. J.Avenhaus has retired but wants to keep in touch. The proposal to have him as an honorary member is proposed and accepted. Other proposed honorary members: G.Huet, U.Montanari. About future new members, they have to be invited several times, so it would be better if we could contact them early enough before the meeting, for being sure that they can come. ----------------------------------------- * Rewriting activities: For RDP 2004, the federated conference on rewriting, deduction and programming, there has been 108 participants (73 for RTA). The most represented countries are: Germany+France, USA, The Netherlands, Japan, Spain. There has been less submissions compared to previous years, and there has also been less participants. In 2004, there has been a lot of wokshops related to rewriting: - WRLA (during ETAPS): 5th workshop on rewriting logic and its applications (40 participants) - Unif (during IJCAR): 24 participants - RULE (during RDP): 5th workshop on rule-based programs (30 participants) - WRS (during RDP): 4th workshop on reduction strategies in rewriting and programming (30 participants) - WST (during RDP): 7th workshop on termination (35 participants) - TERMGRAPH (during ICGT): 2nd workshop on term graph rewriting ESSLLI 2004: the 16th european summer school in logic, language and information will hold in Nancy (France) on August 9-20. Several lectures related to term rewriting will be given there. In 2005, the conference RTA will be part of RDP, together with TLCA. It will hold in Nara (Japan) on April 19-23. Note that the deadline for papers submission is very early: November 12. The proposition of organizing a summer school on rewriting is raised. The main difficulty when organizing such event is to find funds. Femke van Raamsdonk and Pierre Lescanne will try to get information on this. ----------------------------------------- * Information on the web: http://plateforme-qsl.loria.fr/Plate-forme QSL/index.php?Language=1 This is the address of the repository on term rewriting. It contains systems and lecture notes. However, it needs more input and it has to be referenced in more web pages. The members of the group are invited to send new documents and softwares to the webmaster (Mohamed.El-Habib@loria.fr). Pierre Lescanne has done a web page containing hardly findable papers. This page has been added in the online bibliographies citations on the rewriting home page (http://www.rewriting.org). Ralf Treinen needs to update the web page on open problems (see http://www.rewriting.org). Everybody is invited to send some to him (treinen@lsv.ens-cachan.fr). ----------------------------------------- * Next working group workshop: The next meeting of this IFIP working group will hold in Nara (Japan), as part of RDP, with the RTA and TLCA conferences. ----------------------------------------------------------------------