-------------------------------------------------------------------------------- Minutes of the Second Workshop of the IFIP WG-1.6 on Term Rewriting University of East Anglia, Norwich, U.K. July 9, 2000 -------------------------------------------------------------------------------- Agenda 1. Progress reports. 1.1. Declarative Debugging of Lazy Narrowing Computations, Mario Rodríguez-Artalejo. 1.2. On Ordering Constraints, Michaël Rusinowitch. 1.3. Progress reports on Maude and ELAN, Maude: José Meseguer, ELAN: Hélène Kirchner. 1.4. Efficient Implementation, Applications and Complexity of Rewriting, Rakesh Verma. 2. Business session. 3. General discussion. 4. Rewriting and higher-order features. 4.1. The Rewrite Calculus as a Uniform View of Rewriting and Lambda-Calculus, Claude Kirchner. 4.2. General discussion on that topic. Chaired by Claude Kirchner. Participants: Leo Bachmair, Corrado Böhm, Nachum Dershowitz, Richard Kennaway, Claude Kirchner (WG Vice-Chair), Hélène Kirchner, José Meseguer, Aart Middeldorp, Mario Rodríguez Artalejo, Michaël Rusinowitch, Yoshihito Toyama, Femke van Raamsdonk (representing Jan Wilhem Klop) , Rakesh Verma (Invited), Laurent Vigneron (WG Secretary), Uwe Waldmann (representing Harald Ganzinger). Meeting opened at 9:00 Meeting closed at 18:00. -------------------------------------------------------------------------------- 1. Progress reports. 1.1. Declarative Debugging of Lazy Narrowing Computations, Mario Rodríguez-Artalejo (Madrid). Declarative debugging is used in logic programming and can be applied to lazy functional (logic) programs. Lazy narrowing calculus is used to formalize computations; a proof tree is extracted (using formal methods) from the narrowing computations, and simplified to get a computation tree. This technique is used for detecting wrong answers in a set of declarative conditional rewrite rules. This consists in checking the correctness of the nodes of the tree w.r.t the intended model. A buggy node is a wrong node with correct sons. 1.2. On Ordering Constraints, Michaël Rusinowitch (Nancy). The Recursive Path Ordering (RPO) is one of the most used ordering since it gives simple syntactic conditions for orienting equations as rules. An optimal way to apply RPO is to orient an equation u=v as u->v if for all ground substitutions \theta, u\theta >{rpo} v\theta. When the precedence is total this amounts to checking the unsatisfiability of the ordering constraint v >{rpo} u or u ={rpo} v. Ordering constraints based on RPO and its variants also allow us to express theorem-proving strategies such as ordered resolution, ordered paramodulation and unfailing completion. RPO constraint solving has been shown NP-complete for a total precedence (joint work with P. Narendran and R. Verma). In the unary (and total) case the whole first-order theory is decidable using tree automata techniques (joint work with P. Narendran). 1.3. Progress reports on Maude and ELAN, Maude: José Meseguer (Menlo Park), ELAN: Hélène Kirchner (Nancy). Maude (maude.csl.sri.com) is a system and language implementing rewriting logic. This interpreter can be used as an execution specification language, and a programming language. It is reflexive, and includes many tools: an inductive theorem prover, a Church-Rosser checker, many translators,... It permits to associate an executable formal semantics in rewriting logic to software architecture, object-oriented designs and distributed components. It is used for giving a formal analysis of communication systems. Some extensions are considered: an extension supporting mobile computations, a compiler, a theorem-proving environment. ELAN (www.loria.fr/ELAN) is an environment for specifying and prototyping deduction systems. The interpreter and the compiler permit to consider non-deterministic calculi. It uses ASF+SDF parsing tools for EFIX, an intermediate format for ELAN based on A-terms, and a new parser generating EFIX. ELAN is used for equational reasoning with CoQ: ELAN finds a computation, and CoQ checks it. ELAN is also used in the CoFI working group for executing CASL specifications. Many tools have been realised in ELAN: a library for automata construction and manipulation; a general framework of Constraint Logic Programming; a predicate prover; a propositional sequent calculus; completion procedures for rewrite systems; several examples of constraint solvers; a calculus of explicit substitutions (the first-order rewrite system lambda-sigma that mimics lambda-calculus), opening the way of implementing higher-order logic programming languages via a first-order setting. Current investigations are done on various enrichments of languages: objects and constraints are added in objects and rules for the study of production rules systems. The rewriting calculus rho-calculus provides a promising framework for integrating lambda-calculus rewriting, non-determinism and objects. 1.4. Efficient Implementation, Applications and Complexity of Rewriting, Rakesh Verma (Houston). LRR is a laboratory for rapid term rewriting. It is based on a term graph interpreter and Smaran, a congruence-closure based system for equational computations. It contains many optimisations: encoding of strings, recursion, built-in data types, discrimination trees for matching, congruence closure, dependency lists,... About complexity, there are still many unknown results, even for ground rewriting (e.g. confluence). 2. Business session. * Shall we join the IFCoLog initiative? The rewriting community has been contacted by the IFCoLog representatives, in order to know if it will be willing to join the initiative. The question has been redirected to the two current representative organisations of the rewriting community: the RTA organizing committee that will rise the point at the RTA2000 general assembly and to our IFIP working group. The International Federation for Computational Logic (www.ifcolog.org), whose President is Dana Scott, is an association that has the object to advance and promote world-wide research and education in all areas of computational logic. The discussion about this association raises various points: - it has to be a light structure for a better representation of the community in the large. - IFCoLog may not bring financial facilities, but this could be an important "label" to add when asking subsidies. - it will allow to bridge together the various aspects of computational logic and to promote the ideas at the educational level as well as at the political level. The question about the existence of FLoC is raised. Is this conference going to disappear in favor of a federated computational logic conference that would hold every 4 or 5 years? After discussions, all the present members of the WG are in favor to have term rewriting represented in the IFCoLog initiative. The question is raised of the best way to reflect this engagement from the IFIP point of view. The question will be asked to the TC1 chairman, Giorgio Ausiello. * The point on many workshops concerned with rewriting. This year, there are several workshops concerned with rewriting: 1st Workshop on Rule-Based Constraint Reasoning and Programming (CL'2000), 2nd Workshop on Rule-Based Constraint Reasoning and Programming (CP'2000), Workshop on Rule-Based Programming (PLI'2000), Workshop on Rewriting Logic and its Applications (WRLA'2000). These 4 workshops are grouped in 6 months! Do we need to have a coordination between these workshops? The general opinion is that this rise of direct interest to rewriting is an healthy indicator of the research activities around rewriting. 3 of these workshops are organised as conferences adjacent workshops which is a nice way to promote the ideas in related areas and this should be encouraged. We have to try to avoid overlaps, and to find joint events (like RTA) where these workshops can be from time to time (e.g. every 3 or 4 years) in direct contact with the main core of the rewriting community. This rises the point of the relationship between RTA and the other rewrite concern events. The fact that several of these workshops have published proceedings may explain the small number of submissions to RTA. In addition, theoretical papers are currently predominant at RTA. The RTA community should also think on how to attract people who use rewriting for applications. * Next meeting. The next meeting of the WG will hold with RTA in Israel (May 21-24, 2001), and there is a preference to have it after the conference. * Actions to promote rewriting in the large. Several suggestions are done. - To elaborate material around the complementary needs to have gentle introductory to the field and some handbook in rewriting. Three possibilities: a paper book; a dynamic electronic book; tutorials. - This is also very important to promote the existing tools related to rewriting, explaining the role of each and the applications they can handle. This list existing already in the Rewriting Home Page (RHP, www.rewriting.org), we have to promote this page. - Rewriting being a natural technique, an experience would be to take as "clients" kids of 12 years old, and to define tools that would use mouse oriented rewrite systems. The purpose is to make understand that the arrow is powerful in many different ways. - We also need pointers to courses on the RHP. - If we really want to promote rewriting in the industry, we have to consider that we need a different approach. This means that we need to adapt to each kind of public. This discussion leads to the proposition to have a group of persons elaborating on the idea of an electronic book. Corrado Böhm, Claude Kirchner, José Meseguer, Femke van Raamsdonk and Rakesh Verma will discuss about its contents. 3. General discussion: Where is rewriting going? Claude and Corrado presented respectively the opinions of David Plaisted and Marisa Venturini Zilli. Some participants agree that most of the main questions in the domain have been solved. Some on the contrary believe that important questions are far to be solved. Points that are mentioned are to improve the actual standards in complexity; to get new algorithmic results. There are also many applications of rewriting, but no real breakthrough. Though rewriting is a notion present in many areas, but it is not always a research point by itself. Does it have to? Rewriting is a very simple mechanism that subsumes many techniques. It is not known enough as a translation tool. For attracting new researchers in our domain, we need to apply rewriting in other domains, such as biological computing. This may be achieved by defining a general tool for symbolic computing, hiding the techniques behind, since term rewriting may be difficult to "sell" as it is. In addition, rewriting has shown its usefulness as a programming paradigm (cf. ASF+SDF, ELAN, Maude), but programming with rewrite rules has to be learned and we need to define a methodology for rule-based specification and programming. Also, term rewriting is not taught enough. Why is it not explicitely in each computer science curricula? There is no undergraduate book on term rewriting. This would be easy to find mathematical examples illustrating its main notions. To sum up: Rewriting is an excellent model of computation as well as programming paradigm: as stated by Corrado, "rewriting is the best way to bridge the gap between syntax and semantics". Important directions are: - the extreme importance of applications and transfers to industry and other fields (find killer applications!), - Application/link with bio-informatics, - Rewriting with complexity awareness, - Proof techniques for non necessarily equationally interpreted rewriting, - Education oriented activities, - Methodology. 4. Rewriting and higher-order features. 4.1. The Rewriting Calculus as a Uniform View of Rewriting and Lambda-Calculus, Claude Kirchner (Nancy). The principle is to use a proof by rewriting as a function. Applying a rule to a term may give several results, or none. So rules applications and results have to be explicit objects, rho-terms. The lambda-calculus, rewriting and conditional rewriting have natural encoding in the rho-calculus. This gives a functional view of rewriting. 4.2. General discussion on that topic. The relationships between the rewriting and the higher-order logic communities are numerous. Concepts that bridge the concepts of rewriting and higher-order features (CRS, HRS, ERC, rewriting calculus, ...) are developing and a better understanding of their relationship has to be developed. --------------------------------------------------------------------------------