Lecture Notes ni Computer Science Edited by G. Goos and .J Hartmanis 355 .N ztiwohsreD (Ed.) gnitirweR seuqinhceT dna snoitacilppA 3rd Conference, International RTA-89 Chapel Hill, North Carolina, USA April 3-5, 1989 Proceedings galreV-regnirpS nilreB Heidelberg NewYork London Paris oykoT Editorial Board D. Barstow W. Brauer .P Brinch Hansen D. Gries D. Luckham C. Moler A. Pnueli G. Seegm~ller J. Stoer N. Wirth Editor Nachum Dershowitz Department of Computer Science, University of Illinois 1304 W. Springfield Ave., Urbana, IL 61801-2987, USA CR Subject Classification (1987): D.3, F.3.2, F.4, 1.1, 1.2.2-3 ISBN 3-540-51081-8 Springer-Verlag Berlin Heidelberg New York tSBN 0-387-51081-8 Springer-Verlag New York Berlin Heidelberg This work subject is to whole the whether reserved, All are copyright. rights or the of material part the rights concerned, is specifically of re*use reprinting, translation, of recitation, illustrations, broadcasting, reproduction on microfilms or ni storage in and ways, other data Duplication banks. of publication this or provisions the under permitted only is thereof parts of Copyright German the Law of September ,9 1965, ni June of version its ,42 always must fee copyright a and 1985, be act the prosecution under fall Violations paid. of Copyright German the Law. © Berlin Heidelberg Springer-Verlag 1989 Germany in Printed Hemsbach/Bergstr. Beltz, and binding: Druckhaus Printing 2145/3140-543210 - paper acid-free on Printed PREFACE This volume contains the proceedings of the Third International Conference on Rewriting Techniques and Applications (RTA-89). The conference was held April 3-5, 1989, in Chapel Hill, North Carolina, U.S.A. Professor Garrett Birkhoff of Harvard University delivered an invited lecture. The two previous conferences were held in France: • Dijon, May 1985 (Lecture Notes in Computer Science 202, Springer-Verlag); • Bordeaux, May 1987 (Lecture Notes in Computer Science 256, Springer-Verlag). For the third conference, papers were solicited in the following (or related) areas: Term rewriting systems Symbolic and algebraic computation Conditional rewriting Equational programming languages Graph rewriting and grammars Completion procedures Algebraic semantics Rewrite-based theorem proving Equational reasoning Unification and matching algorithms Lambda and combinatory calculi Term-based architectures The 34 regular papers in this volume were selected from 84 submissions by a ten- member committee, consisting of the following individuals: Bruno Courcelle (Bordeaux) Deepak Kaput (Albany) Nachum Dershowitz (Urbana) Claude Kirchner (Nancy) Jean Gallier (Philadelphia) Jan Willem Klop (Amsterdam) Jieh Hsiang (Stony Brook) Dallas Lankford (Ruston) Jean-Pierre Jouannaud (Orsay) Mark Stickel (Menlo Park) Each paper was graded by two to six people (committee members and outside referees). Also included in this volume are short descriptions of a dozen of the implemented equational reasoning systems demonstrated at the meeting. Local arrangements were organized by: David A. Plaisted Department of Computer Science Universitoyf North Carolina at Chapel Hill Chapel-Hill, NC 27599 U.S.A. The meeting was in cooperation with the Association for Computing Machinery and received support from the University of Illinois at Urbana-Champaign and the University of North Carolina at Chapel Hill. Nachum Dershowitz Program Chairperson the committee acknowledges the help of the following referees: Leo Bachmair A. Megrelis J. C. M. Baeten Yves Metivier M. Bezem Aart Middeldorp Maria Paola Bonacina David Musser Alexandre Boudet Paliath Narendran Hans-Jfirgen Burckert Tobias Nipkow Robert Cori Friedrich Otto Herv$ Devie Uday Reddy Francois Fages Jean-Luc R~my Isabelle Gnaedig Michael Rusinowitch Miki Hermann Manfred Schmidt-Schau$ Bharat Jayaraman Sabine Stiffer Simon Kaplan Jonathan Stillman StSphane Kaplan F.-J. de Vries H61~ne Kirchner R. C. de Vrijer Pierre Lescanne Hantao Zhang D. Luggiez CONTENTS Invited Lecture Rewriting Ideas from Universal Algebra (Abstract) Garrett Birkhoff .................................................................... 1 Regular Papers Characterizations of Unification Type Zero Franz Baader ...................................................................... 2 Proof Normalization for Resolution and Paramodulation Leo Bachmair ..................................................................... 51 Complete Sets of Reductions Modulo Associativlty, Commutativity and Identity Timothy B. Baird, Gerald E Peterson, Ralph W. ~Vilkerson ........................ 29 Completion-Time Optimization of Rewrite-Time Goal Solving Hubert Bertling, Harald Ganzinger ................................................ 45 Computing Ground Reducibility and Inductively Complete Positions Reinhard Biindgen, Wolfgang Kiichlin ............................................. 59 Inductive Proofs by Specification Transformations Hubert Comon .................................................................... 67 Narrowing and Unification in Functional Programming--An Evaluation Mechanism for Absolute Set Abstraction John Darlington, Yi-ke Guo ....................................................... 92 Simulation of Turing Machines by a Left-Linear Rewrite Rule Max Dauchet .................................................................... 901 Higher-order Unification with Dependent Function Types ConaI M. Elliott ................................................................. 121 An Overview of LP, The Larch Prover Stephen J. Garland, John V. Guttag .............................................. 731 Graph Grammars, A New Paradigm for Implementing Visual Languages Herbert GSttler .................................................................. 251 Termination Proofs and the Length of Derivations (Preliminary Version) Dieter Hofbauer, Clemens Lautemann ............................................ 167 Abstract Rewriting with Concrete Operators Stephane Kaplan, Christine Choppy .............................................. 871 On How to Move Mountains ~Assoclatively and Commutatively' Mike Lai ......................................................................... 187 Generalized GrSbner Bases: Theory and Applications. A Condensation Dallas Lankford .................................................................. 203 IV A Local Termination Property for Term Rewriting Systems Dana May Latch, Ron Sigal ...................................................... 222 An Equational Logic Sampler George F. MeNulty .............................................................. 234 Modular Aspects of Properties of Term Rewriting Systems Related to Normal Forms Aart Middetdorp ................................................................. 263 Priority Rewriting: Semantics, Confluence, and Conditionals Chilukuri K. Mohan ............................................................. 278 Negation with Logical Variables in ConditionM Rewriting Chilukuri K. Mohan, Mandayam K. Srivas ....................................... 292 Algebraic Semantics and Complexity ofT erm Rewriting Systems Tohru Naoi, Yasuyoshi Inagaki ................................................... 113 Optimization by Non-deterministic, Lazy Rewriting Sanjai Narain ................................................................... 623 Combining Matching Algorithms: The Regular Case Tobias Nipkow ................................................................... 343 Restrictions of Congruences Generated by Finite Canonical Strlng-Rewriting Systems ])biedrich Otto ................................................................... 953 Embedding with Patterns and Associated Recursive Path Ordering Laurence Puel ................................................................... 173 Rewriting Techniques for Program Synthesis Uday S. Reddy ................................................................... 388 Transforming Strongly Sequential Rewrite Systems with Constructors for Efficient Parallel Execution R. C. Sekar~ Shaunak Pawagi, I. V. Ramakrishnan ............................... 404 Efficient Ground Completion: An O(n log n) Algorithm for Generating Reduced Sets of Ground Rewrite Rules Equivalent to a Set of Ground Equations E Wayne Snyder ................................................................... 419 Extensions and Comparison of Simplification Orderings Joachim Steinbach ............................................................... 434 Classes of Equational Programs that Compile into Efficient Machine Code Robert L Strandh ................................................................ 449 Fair Termination is Decidable for Ground Systems Sophie Tison .................................................................... 462 Termination for the Direct Sum of Left-Linear Term Rewriting Systems (Preliminary Draft) Yoshihito Toyama, Jan Willem Klop, Hendrik Pieter Barendregt .................. 477 Conditional Rewrite Rule Systems with Built-In Arithmetic and Induction Sergey G. Vorobyov .............................................................. 492 VII Consider Only General Superpositions in Completion Procedures Hantao Zhang, Deepak Kaput .................................................... 513 System Descriptions Solving Systems of Linear Diophantine Equations and Word Equations Habib Abdulrab, Jean-Pierre Pdcuchet ............................................ 530 SbReve2: A Term Rewriting Laboratory with (AC-)Unfailing Completion Siva Anantharaman, Jieh Hsiang, Jalel Mzali ..................................... 533 THEOPOGLES -- An Efficient Theorem Prover Based on Rewrite-Techniques J. Avenhaus, J. Denzinger, J. 315ller ............................................. 538 COMTES -- An Experimental Environment for the Completion of Term Rewriting Systems Jiirgen Avenhaus, Klaus Madlener, Joachim Steinbach ............................ 542 ASSPEGIQUE: An Integrated Specification Environment Michel Bidoit, Francis Capy, Christine Choppy, Stephane Kaplan, Francoise Schlienger, Frederic Voisin ............................................. 547 KBlab: An Equational Theorem Prover for the Macintosh Maria Paola Bonacina, Giancarlo Sanna ......................................... 548 Fast Knuth-Bendix Completion: Summary Jim Christian .................................................................... 551 Compilation of Ground Term Rewriting Systems and Applications M. Dauchet, A. Deruyver ........................................................ 556 An Overview of Rewrite Rule Laboratory (RRL) Deepak Kaput, Hantao Zhang .................................................... 559 InvX: An Automatic Function Inverter H. Khoshnevisan, K. M. Sephton ................................................. 564 A Parallel Implementation o{ Rewriting and Narrowing Naomi Lindenstrauss ............................................................. 569 Morphocompletion for One-Relation Monoids John Pedersen ................................................................... 574 Author Index .................................................................. 579 Term Rewriting and Universal Algebra in Historical Perspective Invited Lecture m Garrett Birkhoff Harvard University Department of Mathematics Science Center 325 One Oxford Street Cambridge, MA 02138 USA Abstract "Term rewriting" is obviously concerned with the logic of algebra. Closely related to symbolic logic and mathematical linguistics, it derives much of its stimulus from the idea of exploiting the enormous power of modern computers. My talk will fall into two parts. The first part will review term rewriting from the general standpoint of "universal algebra" in historical perspective. The perspective suggests as especially interesting and/or challenging. Characterizations of Unification Type Zero Franz Baader IMMD 1, Universitiit Erlangen-Niimberg MartensstraBe 3, D-8520 Erlangen (West Germany) Abstract In the literature several methods have hitherto been used to show that an equational theo- ry has unification type zero. These methods depend on conditions which are candidates for alternative characterizations of unification type zero. In this paper we consider the logical connection between these conditions on the abstract level of partially ordered sets. Not all of them are really equivalent to type zero. The conditions may be regarded as tools which can be used to determine the unification type of given theories. They are also helpful in understanding what makes a theory to be of type zero. 1. Introduction. Let E be an equational theory and =E be the equality of terms, induced by E. A substitu- tion 0 is called an E-unifier of the terms s, tiff Os =E .Ot The set of all E-unifiers of s, t is denoted by UE(S,t). We are mostly interested in complete sets of E-unifiers, i.e. sets of E-unifiers from which UE(S,t ) may be generated by instantiation. More formally, we extend =E to UE(S,t) and define a quasi-ordering <E on UE(s,t) by YC =E 0 iff xO =E x0 for all variables x occurring in s or t. E<- 0 iff there exists a substitution ~ such that c 0 =E o ~. In this case ~ is called an E-instance of 0. As usual the quasi-ordering E<- induces an equivalence relation -E on UE(S,t), namely o --E 0 iff ~ E<- 0 and 0 <E ~. The ssalC-E=- of an E-unifier c of s, t shall be denoted by [~]. A complete set CUE(S,t) of E-unifiers of s, t is defined as (1) ~ CUE(S,t) UE(S,t ), (2) For all 0 ~ UE(S,t) there exists c ~ CUE(S,t) such that 0 E<- ~" A minimal complete set ~tUE(S,t) is a complete set of E-unifiers of s, t satisfying the mini- mality condition (3) For all c, 0 ~ ~tUE(S,t) c <E 0 implies c = 0. This notion was introduced by Plotkin (1972). In the same paper he conjectured that there exist an equational theory E and terms s, t such that ~tUE(S,t) does not exist. We say that such a theory has unification type zero. The first example of a type zero theory is due to Fages and Huet (1983). They constructed a theory E and terms s, t such that UE(S,t) contains a strictly increasing chain with respect to <E which is a complete set of E-uni- fiers of s, t. Under these circumstances, a complete set of E-unifiers can not satisfy the minimality condition. Schmidt-SchauB (1986) and the present author (1986) showed that the theory of idempotent semigroups is of unification type zero and in Baader (1987) I have proved that almost all varieties of idempotent semigroups are defined by type zero theories. In these cases, complete sets of unifiers are not simply chains. Thus other meth- ods had to be developed to obtain the results. In this paper we consider some of these methods and their logical connection. We shall thus obtain alternative characterizations of unification type zero and sufficient conditions ( resp. necessary conditions ) for a theory to be type zero. This provides tools which may be used to determine the unification types of given theories. It also helps to understand what it means that a theory is of type zero. 2. Minimal complete sets and maximal elements. For terms s, t the quasi-ordering E<- on UE(S,t) induces a partial ordering ( po ) < on U := { [~]; ~ ~ UE(S,t) ,} namely [c] <_ [x] iff ~ E<- .c" The existence of a set gUE(S,t) can be described with the help of the set of all <-maximal elements in U. But ftrst we extent the notion of complete and minimal complete sets to subsets of partially ordered sets ( see also Btittner (1986), Schmidt-Schaul3 (1986a) and Btirckert (1987)). Parts of our proofs can be done on this abstract level.