-------------------------------------------------------------------------------- Minutes of the Fourth Workshop of the IFIP WG-1.6 on Term Rewriting Copenhagen, Denmark July 25, 2002 -------------------------------------------------------------------------------- Agenda 1. Progress reports. 1.1. Modular Termination Proofs Using Dependency Pairs, Jürgen Giesl. 1.2. On Modularity in Context-sensitive Rewriting, Bernhard Gramlich. 1.3. Deciding satisfiability problems by rewrite-based deduction: experiments in the theory of arrays, Maria Paola Bonacina. 1.4. Progress report, Nachum Dershowitz. 1.5. Lambda-calculus with end-of-scope, Vincent van Oostrom. 1.6. Computational restrictions of rewriting in functional programming, Salvador Lucas. 2. Business session. Chaired by Claude Kirchner. Participants: Franz Baader, Maria Paola Bonacina, Nachum Dershowitz, Jürgen Giesl (invited), Bernhard Gramlich (invited), Jean-Pierre Jouannaud, Claude Kirchner (Chairman), Hélène Kirchner, Salvador Lucas (invited), Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, Yoshihito Toyama, Laurent Vigneron (Secretary). Meeting opened at 9:00 Meeting closed at 17:00 -------------------------------------------------------------------------------- 1. Progress reports. 1.1. Modular Termination Proofs Using Dependency Pairs, Jürgen Giesl (Aachen). The dependency pair approach allows automated termination and innermost termination proofs for many term rewriting systems for which such proofs were not possible before. The motivation for this approach is that virtually all previous techniques for automated termination proofs of term rewriting systems were based on simplification orderings. In practice, however, many rewrite systems are not simply terminating, i.e., their termination cannot be verified by any simplification ordering. The dependency pair approach has been refined in order to prove termination in a modular way. This refinement, permitting the use of several different orderings in one termination proof, is inevitable in order to verify the termination of large rewrite systems occurring in practice. New modularity results based on dependency pairs are presented. First, the well-known modularity of simple termination for disjoint unions can be extended to DP quasi-simple termination, i.e., to the class of rewrite systems where termination can be shown automatically by the dependency pair technique in combination with quasi-simplification orderings. Second, the refinement of the dependency pair approach yields new modularity criteria for innermost termination, extending previous results in this area. In particular, existing results for modularity of innermost termination can easily be shown to be direct consequence of these new criteria. 1.2. On Modularity in Context-sensitive Rewriting, Bernhard Gramlich (Vienna). Context-sensitive rewriting (CSR) has recently emerged as an interesting and flexible paradigm that provides a bridge between the abstract world of general rewriting and the (more) applied setting of declarative specification and programming languages such as OBJ*, CafeOBJ, ELAN, and Maude. A natural approach to study properties of programs written in these languages is to model them as context-sensitive rewriting systems. Here we are especially interested in proving termination of such systems, and thereby providing methods to establish termination of e.g. OBJ* programs. For proving termination of context-sensitive rewriting, there exist a few transformation methods, that reduce the problem to termination of a transformed ordinary term rewriting system (TRS). These transformations, however, have some serious drawbacks. In particular, most of them do not seem to support a modular analysis of the termination problem. We show that a substantial part of the well-known theory of modular term rewriting can be extended to CSR, via a thorough analysis of the additional complications arising from context-sensitivity. More precisely, we mainly concentrate on termination (properties). The obtained modularity results correspond nicely to the fact that in the above languages the modular design of programs and specifications is explicitly promoted, since it can now also be complemented by modular analysis techniques 1.3. Deciding satisfiability problems by rewrite-based deduction: experiments in the theory of arrays, Maria Paola Bonacina (The University of Iowa). Joint work with Alessandro Armando, Silvio Ranise, Michael Rusinowitch, Aditya Sehgal. Satisfiability procedures are a key component of verification tools. The endeavour of designing, proving correct, and implementing a satisfiability procedure for each decidable theory of interest is far from simple. Most problems involve more than one theory, needing to combine satisfiability procedures. Using a theorem prover, with the union of the theories in input, is simpler, and does not require theory-specific completeness proofs, assuming the theorem proving strategy is sound and complete. If the theorem-proving strategy is guaranteed to terminate on the theories of interest, it is in itself a decision procedure. Such termination results were recently obtained for ordering-based strategies, with a paramodulation-based inference system, on the theories of lists, arrays with extensionality and their combination, among others. Termination achieved, the issue of efficiency remains. We propose two sets of synthetic benchmarks in the theory of arrays with extensionality, and we report on experiments showing that a theorem prover - the E system - compares successfully with the state-of-the-art validity checker CVC. This offers evidence that an approach based on general-purpose deduction may be both practical and theoretically elegant. 1.4. Progress report, Nachum Dershowitz (Tel Aviv). Presentation of the last books published concerning calendar calculations, based on constraints solving. Presentation of the ongoing works and cooperations. 1.5. Lambda-calculus with end-of-scope, Vincent van Oostrom (Utrecht). Presentation of an extension of the lambda-calculus with an end-of-scope operator, which came up naturally, while extending the optimal first-order setting to higher-order. The rough idea is that a role of the lambda is to open a scope and it is only natural to introduce an explicit operator to end a scope. The nice thing is that (an extension of) beta-reduction can be defined which is confluent without alpha-reduction. Alpha reduction is only needed when removing end-of-scopes. This calculus is halfway toward an optimal implementation of the lambda calculus: for that also the explicit operators for (un)sharing, the so-called fan-in and fan-out, need to be introduced. The proofs have been realized in Coq. 1.6. Computational restrictions of rewriting in functional programming, Salvador Lucas (Valencia). Given a term rewriting system, the definition of a strategy over this system should always preserve normal forms. When this is not the case, one should talk about computational restrictions, for which one can define strategies. Using computational restrictions, the termination of (functional) programs corresponds to termination of strategic rewriting, and the semantics of (functional) programs corresponds to infinitary normalizing strategies. Computational restrictions on rewriting are a trade off between termination and correctness/completeness. Some examples of computational restrictions are strategy annotations, just-in-time annotations, on-demand strategy annotations, and context-sensitive rewriting. 2. Business meeting. ** Rewriting events: In the past year, with the following abbreviations, S: submissions IP: invited presentations T: tutorials PL: panel list SP: system presentations RP: regular presentations we had: - Conference on Rewriting Techniques and Applications (RTA'02, Copenhagen, Jul. 21-24, 2002): 49 S, 3 IP, 4 SP, 22 RP Proceedings: LNCS 2378 - Workshop on Rule-Based Programming (Rule'01, Firenze, Sept. 4, 2001): 14 S, 11 RP Proceedings: ENTCS volume 59-4 (all presented papers) - Workshop on Reduction Strategies in Rewriting and Programming (WRS'01, Utrecht, May 26, 2001): 6 S, 2 IP, 3 PL, 6 RP Proceedings: ENTCS volume 57 (all presented papers) - Workshop on Reduction Strategies in Rewriting and Programming (WRS'02, Copenhagen, Jul. 21, 2002): 10 S, 2 IP, 8 RP Proceedings: ENTCS volume 70-6 - Workshop on Termination (WST'01, Utrecht, May 20-21, 2001): 21 RP - Workshop on Rewriting in Proof and Computation (RCP'01, Sendai, Oct. 25-27, 2001): 9 IP, 12 RP - Workshop on rewriting logic and applications (WRLA'02, Pisa, Sept. 19-21, 2002): 17 S, 3 IP, 4 T, 4 SP, 12 RP For a total of 129 submissions (of course there may be redondancies) 104 regular presentations 23 invited presentations Some workshops do even publish their proceedings. This confirms the good health of rewriting activities. The multiplicity of rewrite events allows to spread the rewriting publications is related areas. We should consequently take care to maintain the main conference RTA with a good level of submissions and of participants. Group members are invited to stimulate their collegues to submit their best paper to RTA! In 2003, RTA will be part of RDP (Federated Conference on Rewriting, Deduction and Programming) in Valencia, Spain, together with TLCA, FTP and some other workshops (including the next meeting of this IFIP working group). In 2004, RTA will be in Aachen, Germany. ** E-book on Rewriting: To initiate the work on the e-book, the idea to set up a database of examples with references and keywords raises. Femke van Raamsdonk will collect these examples and the access to the database will be done in XML. Members of the group who are interested have to contact Femke. From the general discussion on the e-book, several ideas emerge: - An editorial board should certainly be set up, - The contents of the book will have to be different from the published paper books. ** A new book is going to be published soon and is presented by Vincent: "Term Rewriting Systems", Cambridge University Press, by Terese (editors M. Bezem, J.W. Klop and R.C. de Vrijer, Amsterdam). ** Renewal of group membership: Some members of this IFIP working group being non-active (wrt. the group), we have defined the following policy: " After 3 years of not participating to a group meeting, a member is asked to confirm his involvement in the working group or to leave his place to allow for the admission of new members." The list of members concerned will be set annually and the chair of the working group will be in charge to ask them for their further involvement. Honorary Members will also be proposed and ratified by the active members. The integration of new researchers will be done after two invitations in a meeting, after approval by the group members. This year, four researchers are added: - Femke van Raamsdonk (http://www.cs.vu.nl/~femke/), - Jürgen Giesl (http://www-i2.informatik.rwth-aachen.de/giesl/), - Bernhard Gramlich (http://www.logic.at/staff/gramlich/), - Salvador Lucas (http://www.dsic.upv.es/users/elp/slucas.html). ======================================================================== The next WG1.6 meeting will be held during the RDP joint conference in Valencia, Spain, Thursday 12, June 2003. Even if there are several other quite interesting meetings in parallel, please make a priority to attend the workshop. ======================================================================== ---------------------------- Calendar of RDP'03 ------------------------------ June 2003 sun mon tue wed thu fri sat m=morning 8 9 10 11 12 13 14 a=afternoon e=evening RTA ma ma m TLCA ma m ma FTP ma ma ma WG 1.6 ma RULE ma UNIF ma ma WFLP ma ma WRS ma WST ma ma Excursion a Joint inv. speaker m Dinner e TLCA bussiness m. e RTA bussiness m. e FTP bussiness m. e ------------------------------------------------------------------------------