-------------------------------------------------------------------------------- Minutes of the Third Workshop of the IFIP WG-1.6 on Term Rewriting University of Utrecht, Utrecht, The Netherlands May 25, 2001 -------------------------------------------------------------------------------- Agenda 1. Progress reports. 1.1. Deciding the confluence of GTRS in PTIME, Robert Nieuwenhuis. 1.2. Computing BDDs by rewriting, Hans Zantema. 1.3. Rewriting activities in Valencia, Salvador Lucas. 1.4. Progress report on rewriting activities in Japan, Yoshihito Toyama. 1.5. Progress report on rewriting activities in Austria, Bernhard Gramlich. 1.6. About 2 applications of rewriting: multiplying by 11 and Origami, Corrado Boehm. 1.7. On applying dependency pairs to process verification, Juergen Giesl. 2. Business session. 3. How to promote rewriting in the large? 4. Panel: On applications of rewriting. Chaired by Claude Kirchner. Participants: Franz Baader, Corrado Böhm, Nachum Dershowitz, Jürgen Giesl (invited), Bernhard Gramlich (invited), Thomas Hillenbrand (representing Harald Ganzinger), Tetsuo Ida, Claude Kirchner (Vice-Chairman), Jan Willem Klop, Sébastien Limet (representing Siva Anantharaman), Salvador Lucas (invited), Aart Middeldorp, Robert Nieuwenhuis, Vincent van Oostrom, David Plaisted, Yoshihito Toyama, Laurent Vigneron (Secretary), Hans Zantema. Meeting opened at 9:00 Meeting closed at 17:10. -------------------------------------------------------------------------------- 1. Progress reports. 1.1. Deciding the confluence of GTRS in PTIME, Robert Nieuwenhuis (Barcelona). (joint work with H. Comon and G. Godoy) Termination and confluence are undecidable in general. In the ground case, termination is PTIME [Plaisted 93], and confluence is decidable [Dauchet et al. 87, Oyamaguchi 87] in exponential time. The question is: what is the exact complexity of deciding confluence of ground term rewriting systems (GTRS)? Many attempts have been done, based on rewriting suffixes and considering stable prefixes (for strings). The first presented result is an algorithm in PTIME for strings rewriting systems. It is based on the following ideas: - to transform a rewrite system R into a system where the left-hand sides are subterms of R (Plaisted's idea), - to apply reductions in order to always increase the length of the stable prefix. A PTIME algorithm has been designed for full GTRS: - to apply three PTIME transformations: Curry form (one binary operator + constants), shallow rules, Plaisted's transformation, - to decide in PTIME if the binary operator becomes stable only by rewriting in its arguments, - to check the necessary conditions for confluence, - to test in PTIME if the sides of the rewrite system are deeply joinable. The exact complexity obtained is PTIME-hardness for strings, and PTIME-completeness for strings and terms. 1.2. Computing BDDs by rewriting, Hans Zantema (Eindoven). Decision trees can be written as terms, since a decision tree can be seen as a Boolean function. Sharing subtrees consists in building a directed acyclic gragh, and to solve a binary decision diagram (BDD). The main problem is to get a unique representation. By ordering atoms, we get ordered BDD (OBDD). But we need maximally shared OBDD, and without simplifiable subtrees. This corresponds to reduced OBDD (ROBDD). Each Boolean function has a unique representation by a ROBDD. This result follows from the termination and confluence of a TRS transforming a BDD into an OBDD. Note that standard ROBDD computation has polynomial complexity. However, the satisfiability of BDDs is NP-hard, and BDDs can be of exponential size. 1.3. Rewriting activities in Valencia, Salvador Lucas (Valencia). The rewriting activities in Valencia have started in the 70s with the collaboration of Isidro Ramos with Claude Pair (Nancy). They worked on algebraic methodologies, types and logics. This collaboration between Valencia and Nancy has continued in the 80s with Miguel Muñoz and Jean-Pierre Jouannaud. María Alpuente is now at the head of the ELP group. The main topics of this group concern programming languages: - semantics of the integration: formalization, optimization strategies based on incremental narrowing, semantics of narrowing computations, - program analysis: abstract narrowing for testing equational satisfiability, - program transformation: partial evaluation of functional logic programs, - inductive programming in functional logic programs, and applications in software engineering, - rewriting techniques in programming: context sensitive rewriting (CSR), termination, semantics of rewriting computations, rewriting strategies. The ELP group has many collaborations in Europe, plus some in the USA and in Japan. It is involved in several national and international projects. The ongoing work concerning rewriting includes: - innermost termination of CSR, - comparison of models for rewriting with syntactic replacement restrictions, - termination of OBJ programs, - decidability issues in transfinite rewriting, - analysis of program properties using rewriting semantics. 1.4. Progress report on rewriting activities in Japan, Yoshihito Toyama (Sendai). A lot of groups, all over Japan, work on rewriting. Twice a year, there is a common meeting (plus some invited foreigners), where each participant gives a talk. The scope of this meeting concerns: TRS, lambda-calculus, type theory, proof theory, functional programming, logic programming, automated deduction, ... The main topics developed in Japan are: - reduction strategies for TRS (most use tree automatas), - termination, - narrowing (conditional TRS, lazy conditional narrowing), - higher-order: simply typed TRS, HRPO, theory of typed HRS, - infinite lambda-calculus, transfinite reduction, - Church-Rosser property, - modular: top-down labelling, disjoint GRS, and many other topic related to concurrence,... The most well-known systems developed in Japan are CafeOBJ (JAIST) and CFLP (Tsukuba). Note that the international workshop on Rewriting in Proof and Computation (RPC) will take place in Sendai, Oct. 25-27, 2001. 1.5. Progress report on rewriting activities in Austria, Bernhard Gramlich (Vienna). The number of universities with research in computer science, rewriting/equational theory, or theory is very low in Austria. There are mainly three: TU Wien, U. Wien, U. Linz/RISC. Another university is getting concerned: U. Innsbruck. Main researchers in Linz: Buchberger, Winkler. Topics: symbolic computation, Groebner bases,... Main researcher in U. Wien: Friedman. Topic: set theory. The main center of research is the TU Wien, where people work on: - equational reasoning: meta terms, unification theory, equational problems (algorithms and complexity), rewriting, deduction, strategies (Salzer, Pichler, Gramlich), - proof theory: model construction and representation for clause sets, semantics trees, induction (Fermüller, Leitsch,...), - automata, formal languages (Kuide), - functional logic programming (Krall,...), - logic, databases, AI, knowledge representation (Gottlob,...). So the main domains are: proof theory, mathematical logic, non-classical logic(s), databases and complexity. But rewriting and equational reasoning are underrepresented. 1.6. About 2 applications of rewriting: multiplying by 11 and Origami, Corrado Boehm (Roma). The first presentation is a functional description of number stacks: rewrite rules describing addition of numbers represented by stacks of digits. Question: is multiplication by 11 simpler tan addition? Answer: yes, with one more memory. The second presentation concerns geometrical origami. Functions are described like agents. For example, the intersection of two lines, the line passing through two points, the perpendicular of a line passing through a point wrt. another point,... This permits to represent second and third degree problems. Therefore, constructing 3D origami solved third degree problems. This is exemplified with the construction of a paper glass. 1.7. On applying dependency pairs to process verification, Juergen Giesl (Aachen). (joint work with Thomas Arts) Process verification consists in testing the termination of a conditional TRS. Messages are sent to the process, it computes something, then sends the results. The problem is that the size of the messages sent is limited. What cannot be sent is stored in the process. Because of those stores, one needs to send empty messages to the processes for emptying their memory. The verification of a process is coded as a conditional TRS left-right decreasing, but proving its termination is difficult. The CTRS is transformed into a TRS, and its innermost termination is proved using dependency pairs: there should be no innermost infinite chain of dependency pairs. Narrowing is used for breaking cycles (some pairs are deleted, other are added). But this is valid only for non-overlapping systems. For overlapping systems, innermost termination does not imply termination. So a solution is to use narrowing, rewriting, and instantiation of dependency pairs. The application of this technique concerns properties that are not set, ie. to verify that something will happen. 2. Business session. * Election: Jieh Hsiang has decided to leave the chair of the group. There was one candidate, Claude Kirchner. Nachum Dershowitz has organised the elections by e-mail. From 43 members, there has been 37 votes: 34 in favor; 1 abstention; 2 additional votes are questionable. So Claude Kirchner has been proposed as new chairman of the group to the TC1 chair, Giorgio Ausiello. * Evolution of the working group members: - Some members are not active. People missing three consecutive meetings can loose their membership. This will be decided at each meeting. A possibility is to have honorary members. - Some people are interested to join the working group. The main problem is to know the rules to follow. Do we have to set criteria? (number of invitations to the group meetings, number of publications in the field, recommandation of current members,...) * Next meeting: it will take place the day after the next RTA (July 25, 2002), in Copenhagen (Denmark); but we have to ask it to the FLoC organizers. In this meeting, the talks should be about collaborations, and research in some countries. 3. How to promote rewriting in the large? There are two levels of promotion: - internal: to put together examples, counter-examples, systems, so that it can be easily found and completed, - external: to promote rewriting in other research domains; to attract students; to show to the general public that rewriting is used everywhere. For this, several propositions are done: - to create a database of examples and counter-examples, starting with very simple examples taken in recent books; other examples may be added by students. The best medium for this would be a web page. Some of us have already some examples, but they need to be maintained. - to create a rewrite laboratory, essentially for teaching. Its minimal requirements are: Knuth-Bendix procedure, computation of canonical forms,... The main problems for creating this tool is to decide what to put inside, who is going to implement it, and who is going to maintain it. Some systems like this have already been designed (eg. RRL), but they are no more maintained. - to compete with other scientific domains. - to promote books/surveys for undergraduate, but to impose a course at this level is difficult. One of the best way to promote rewriting is to create an e-book: it is incremental, easy to consult. Some people are interested to contribute. But for realizing it, we need a steering committee, able to find specialists for writing chapters. The organization of the e-book itself is to be discussed: shall we follow the historical development? And it has not to be in competition with existing books. The last point that is mentioned is to use more often the rewriting list, maintained by Pierre Lescanne (rewriting@ens-lyon.fr). 4. Panel: On applications of rewriting. The main remarks are that the 'A' of RTA is not considered enough: we have to present papers about applications, to involve industrials (in the program committee, for instance), and to invite industrials. A challenge would be that all of us write an application paper within two years. --------------------------------------------------------------------------------