Ebook: Term Rewriting and Applications: 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005. Proceedings

This volume contains the proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA2005),whichwasheldonApril19– 21, 2005, at the Nara-Ken New Public Hall in the center of the Nara National Park in Nara, Japan. RTA is the major forum for the presentation of research on all aspects of rewriting.PreviousRTAconferenceswereheldinDijon(1985),Bordeaux(1987), Chapel Hill (1989), Como (1991), Montreal (1993), Kaiserslautern (1995), Rutgers (1996), Sitges (1997), Tsukuba (1998), Trento (1999), Norwich (2000), Utrecht (2001), Copenhagen (2002), Valencia (2003), and Aachen (2004). This year, there were 79 submissions from 20 countries, of which 31 papers were accepted for publication (29 regular papers and 2 system descriptions). The submissions came from France (10 accepted papers of the 23.1 submitted papers), USA (5.6 of 11.7), Japan (4 of 9), Spain (2.7 of 6.5), UK (2.7 of 4.7), The Netherlands (1.7 of 3.8), Germany (1.3 of 2.3), Austria (1 of 1), Poland (1 of 1), Israel (0.5 of 0.8), Denmark (0.5 of 0.5), China (0 of 4), Korea (0 of 4), Taiwan (0 of 1.3), Australia (0 of 1), Brazil (0 of 1), Russia (0 of 1), Switzerland (0 of 1), Sweden (0 of 1), and Italy (0 of 0.3). Each submission was assigned to at least three Program Committee m- bers, who carefully reviewed the papers, with the help of 111 external referees.

---

This book constitutes the refereed proceedings of the 16th International Conference on Rewriting Techniques and Applications, RTA 2005, held in Nara, Japan in April 2005. The 29 revised full papers and 2 systems description papers presented together with 5 invited articles were carefully reviewed and selected from 79 submissions. All current issues in Rewriting are addressed, ranging from foundational and methodological issues to applications in various contexts; due to the fact that the first RTA conference was held 20 years ago, the conference offered 3 invited historical papers 2 of which are included in this proceedings. Table of Contents Cover Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings ISBN-10 3540255966 ISBN-13 9783540255963 Preface Conference Organization Table of Contents Confluent Term Rewriting Systems Generalized Innermost Rewriting * 1 Introduction * 2 Basic Notation * 3 Generalized Innermost Rewriting * 4 Avoiding Duplication * 5 Avoiding Root Overlaps * 6 Conclusions * References Orderings for Innermost Termination * 1 Introduction * 2 Preliminaries * 3 Characterizing Innermost Termination of Rewriting * 4 An Example of IP-Monotonic Ordering + 4.1 Innermost Stability for iRPO o Algorithm 1 + 4.2 Using iRPO for DP * 5 Conclusions * References Leanest Quasi-orderings * 1 Introduction * 2 A String Example * 3 Leanness * 4 Leanest * 5 Application to Binary Trees * 6 Conclusion * References Abstract Modularity * 1 Introduction * 2 Abstract Data Structures * 3 Abstract Rewriting * 4 Abstract Properties + 4.1 Abstract Confluence + 4.2 Abstract Strong Normalisation * 5 Abstract Combinators + 5.1 Ideal Monads * 6 Conclusion and Future Work * References Union of Equational Theories: An Algebraic Approach * 1 Monadic Theories vs Monoids * 2 Union of Monadic Theories vs Amalgam of Monoids * 3 The Solution via Bases * 4 Conservativity and Interpolation vs Embeddability of Amalgams * 5 Lifting * 6 Conclusions * References Equivariant Unification * 1 Introduction * 2 Background * 3 Permutation Graphs * 4 Equivariant Unification + 4.1 First Phase + 4.2 Second Phase * 5 Swapping-Free Equivariant Matching * 6 Related and Future Work * 7 Conclusions * References Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories * 1 Introduction * 2 Problem * 3 A Sort Theory Associated with an Equational Theory * 4 Sort -- A Procedure to Sort a Goal + Sort-Expansion of E o Sort-Expansion of the Goal * 5 A Separable Equational Theory * 6 Basic Mutation Refined with Sorts * 7 Redundancy of Rules and Determinism + 7.1 Collapsing Goal Equations o Sort Imitation + 7.2 When Decomposition Is Redundant + 7.3 Deterministic BSM with Sorts * 8 Conclusion * References Unification in a Class of Permutative Theories * 1 Introduction * 2 Unify-Stable Theories * 3 Unification in Unify-Stable Theories + 3.1 Notations and Generalities + 3.2 Transformation Rules + 3.3 Termination + 3.4 Completeness * 4 Optimization of the Algorithm * 5 Conclusion * References Dependency Pairs for Simply Typed Term Rewriting * 1 Introduction * 2 Preliminaries * 3 Chains of Minimal Non-terminating Terms * 4 Dependency Pairs * 5 Dependency Graph * 6 Subterm Criterion and Head Instantiation * 7 Experiments * 8 Concluding Remarks * References Universal Algebra for Termination of Higher-Order Rewriting * 1 Introduction + Contribution. + Organisation. + Future Work. * 2 Combinatory Reduction Systems + CRS. * 3 Structural CRSs * 4 Algebraic Semantics of Syntax + 4.1 Binding Algebras + 4.2 Algebra of Structural CRS Terms + 4.3 Algebraic Characterisation of Valuations + 4.4 Structural Valuations are Sufficient * 5 Algebraic Semantics of Rewriting * 6 Algebraic Semantics of Meta-rewriting + Rewriting on Meta-terms. * 7 Termination of Binding CRSs * References * Appendix: Elementary Description of The Category Set^F Quasi-interpretations and Small Space Bounds * 1 Introduction * 2 First Order Functional Programming + 2.1 Syntax of Programs + 2.2 Semantics * 3 Orderings + 3.1 Precedences and Ranks + 3.2 Termination Orderings o Lexicographic Path Ordering + 3.3 Quasi-interpretations * 4 Call-Trees * 5 Linear Space + 5.1 Unary k-Stack Turing Machines + 5.2 Simulation of Linspace by LPOQI+-Programs + 5.3 Computation of LPOQI+-Programs in Linear Space * 6 Logarithmic Space * 7 Polynomial Space + 7.1 Strict Quasi-interpretations + 7.2 Linear Systems * References A Sufficient Completeness Reasoning Tool for Partial Specifications * 1 Introduction * 2 Preliminaries * 3 A Partial Specification Example * 4 Sufficient Completeness for MEL Specifications * 5 The Maude Sufficient Completeness Tool + 5.1 The Maude Sufficient Completeness Analyzer o The Narrowing Procedure. o The Proof Obligation Generator. + 5.2 The Maude ITP * 6 Related Work * 7 Conclusions and Future Work * References Tyrolean Termination Tool * 1 Introduction * 2 Semi-automatic Mode * 3 Fully Automatic Mode * 4 Simply-Typed Applicative Rewrite Systems * 5 A Collection of Rewrite Systems as Input * 6 Some Implementation Details * 7 Comparison * References Call-by-Value Is Dual to Call-by-Name -- Reloaded * 1 Introduction * 2 The .µ-Calculus * 3 The Dual Calculus * 4 Translations * 5 Duality * References .µ-Calculus and Duality: Call-by-Name and Call-by-Value * 1 Introduction * 2 .µ-Calculus * 3 ..µ.µ-Calculus * 4 Translations Between .µ and ..µ.µ-Calculi * 5 Simulations Between .µ and ..µ.µ-Calculi * 6 Conclusion Reduction in a Linear Lambda-Calculus with Applications to Operational Semantics * 1 Introduction * 2 Lily and Its Operational Semantics * 3 A Linear Lambda-Calculus and Surface Reduction * 4 Proof of the Strictness Theorem * 5 Internal and Combined Reduction * 6 Call-by-Need Operational Semantics for Lily * 7 Linear Combinatory Algebras * References * A Outline Proof of Lemma 6.2 Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete * 1 Introduction * 2 Basic Definitions * 3 NP-Complete Varieties of the Satisfiability Problem * 4 Interpolation in the Linear Lambda Calculus * 5 Elimination of Constants * References Localized Fairness: A Rewriting Semantics * 1 Introduction * 2 Kripke Structures, LTL, and Rewrite Theories * 3 The Semantics of Localized Fairness * 4 Relative vs. Absolute LTL Semantics * 5 Concluding Remarks * References Partial Inversion of Constructor Term Rewriting Systems * 1 Introduction * 2 Preliminaries * 3 Partial-Inversion Compiler + 3.1 Definition of Partial-Inverses + 3.2 Idea of Partial Inversion + 3.3 Generation of Partial-Inverse CTRSs + 3.4 Unraveling to Unconditional Systems * 4 Computation of Partial-Inverse EV-TRSs + 4.1 On Extra Variables + 4.2 On Simulation-Incompleteness of Unraveling * 5 Improving Efficiency of Partial-Inverse Computation * 6 Related Works and Conclusion * References Natural Narrowing for General Term Rewriting Systems * 1 Introduction * 2 Preliminaries * 3 Generalizing Natural Narrowing * 4 Application Areas + 4.1 Symbolic Model Checking + 4.2 Theorem Proving * 5 Related Work * 6 Conclusions and Future Work * References The Finite Variant Property: How to Get Rid of Some Algebraic Properties * 1 Introduction * 2 Preliminaries + 2.1 Terms, Substitutions, Unification + 2.2 Equational Rewriting * 3 Narrowing + 3.1 Equational Narrowing + 3.2 Basic Narrowing * 4 Some Relevant Equational Theories + 4.1 Explicit Destructors + 4.2 Exclusive Or Theory (ACUN) + 4.3 Abelian Groups Theory (AG) + 4.4 Diffie-Hellman Theory (DH) + 4.5 Combinations * 5 The Finite Variant Property + 5.1 Definition and a First Characterization + 5.2 The Boundedness Condition * 6 Proving Boundedness + 6.1 The Case E'= 0 + 6.2 Non-orientable Axioms * 7 ACUNh Does Not Satisfy the Finite Variant Property * 8 Other Applications of the Finite Variant Property * 9 Conclusion * References Intruder Deduction for AC-Like Equational Theories with Homomorphisms * 1 Introduction * 2 A Dolev-Yao Model for Rewriting Modulo AC * 3 Locality and Complexity of Deduction Problems * 4 Proof Transformations * 5 Locality for the Rewrite System ACUNh + 5.1 Locality in the Binary Case + 5.2 Locality in the General Case * 6 One-Step Deducibility in Case of ACUNh * 7 Variants and Extensions + 7.1 The Rewrite System ACh + 7.2 The Rewrite System AGh + 7.3 Extension to an Encryption Operation Which is Homomorphic over bigotimes * 8 Conclusion * References Proving Positive Almost-Sure Termination * 1 Introduction * 2 Termination and Abstract Reduction Systems * 3 Stochastic Sequences and Markov Chains * 4 Foster's Theorem * 5 Probabilistic Abstract Reduction Systems * 6 Termination of a Probabilistic Abstract Reduction System * 7 Proving Positive Almost Sure Termination * 8 Probabilistic Rewrite Systems * 9 Termination of a Probabilistic Rewrite System * 10 Conclusion and Perspective * References Termination of Single-Threaded One-Rule Semi-Thue Systems * 1 Introduction * 2 Preliminaries + 2.1 Positions + 2.2 Chain Graphs + 2.3 Family Members * 3 Uniform Termination of One-Rule Single-Threaded Systems + 3.1 Single-Threadedness and Independence + 3.2 Simulation by a Pushdown Automaton * 4 Applications * 5 Conclusion * References On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems * 1 Introduction * 2 Preliminaries * 3 Enrichments of Rewriting Systems * 4 Compatible Tree Automata * 5 Constructing Compatible Automata * 6 Simulating Forward Closures by Rewriting * 7 Compatible Automata and Forward Closures * 8 Conclusion * References Twenty Years Later * 1 Introduction * 2 Basic Ordered Resolution and Paramodulation * 3 Rule-Based Programming * 4 Tree Automata * 5 Proof Assistants * 6 Conclusion * References Open. Closed. Open. * 1 Introduction * 2 Left-Linear Confluence * 3 One-Rule Termination * References A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code * 1 Introduction * 2 Example * 3 Types * 4 Machine Semantics as Hoare-Style Rules * 5 Encoding Machine Semantics Directly * 6 Example Revisited * 7 Discussion * References Extending the Explicit Substitution Paradigm * 1 Introduction * 2 The Calculus lambda lxr * 3 A Model for lambda lxr * 4 Recovering the l-Calculus * 5 Operational Properties * 6 Conclusion and Further Work * References Arithmetic as a Theory Modulo * 1 Deduction Modulo + 1.1 Identifying Propositions + 1.2 Model of a Theory Modulo + 1.3 Normalization in Deduction Modulo * 2 An Alternative Presentation of Arithmetic + 2.1 Heyting Arithmetic + 2.2 A Symbol for Predecessor + 2.3 A Symbol for Natural Numbers + 2.4 A Sort for Classes of Numbers * 3 Arithmetic in Deduction Modulo * 4 Cut Elimination * 5 A Predicative Cut Elimination Proof + 5.1 The Construction of Some Candidates + 5.2 A Pre-model * 6 The System T * References Infinitary Combinatory Reduction Systems * 1 Introduction * 2 Preliminaries * 3 (Meta-)Terms and Substitutions * 4 Infinitary Rewriting * 5 Developments + 5.1 Descendants and Residuals + 5.2 Complete Developments * 6 Further Directions * References Proof-Producing Congruence Closure * 1 Introduction * 2 Union-Find with Proofs + 2.1 Union-Find with an O(k logn) Explain Operation + 2.2 Union-Find with an O(k) Explain Operation * 3 Incremental Congruence Closure with Explain + 3.1 Initial Assumptions and Operations + 3.2 Implementation of Merge + 3.3 Complexity of Merge and AreCongruent? + 3.4 Implementation of Explain + 3.5 Complexity of Explain + 3.6 Quality of Explanations. Experiments o Proof Forests with Structural Classes as Nodes. * 4 Related and Future Work * References The Algebra of Equality Proofs * 1 Introduction * 2 Equality Proofs * 3 Algebraic Characterization of Theorem Equivalence * 4 Proof of Soundness * 5 Canonical Proofs and Completeness * 6 A Linear-Time Strategy for Canonizing Proofs * 7 Canonizing Proofs Without a Strategy * 8 Minimal Proofs from Union-Find * 9 Application to Cooperating Decision Procedures * 10 Conclusion and Future Work * References On Computing Reachability Sets of Process Rewrite Systems * 1 Introduction * 2 Models + 2.1 Process Terms + 2.2 Process Rewrite Systems + 2.3 Subclasses of PRS and Program Modeling * 3 Tree Automata-Based Symbolic Representations + 3.1 Preliminaries + 3.2 Commutative Hedge Automata o Sigma-Terms: o Definition of CH-Automata. + 3.3 CH-Automata for PRS Process Terms * 4 A Generic Construction of PRS Reachability Sets + 4.1 Preliminaries + 4.2 The Set of States + 4.3 Nested Prefix/Multiset Rewriting o Transitive Normal Form: o Rewrite System over the Alphabet of States: o Successor Closure: + 4.4 The Set of Transition Rules * 5 Application: Reachability Analysis of PRS + 5.1 Computing Reachability Sets of PAD Systems + 5.2 Global Model Checking for EF + 5.3 Integrating Reachability Analysis Procedures for Pushdown Systems and Petri Nets * 6 Conclusion * References Automata and Logics for Unranked and Unordered Trees * 1 Introduction * 2 Preliminaries + 2.1 The Tree Model + 2.2 An Algebraic View of Trees + 2.3 Arithmetical Formulas + 2.4 Presburger-Definable Sets and Multiset Languages * 3 MSO-Based Logics for Trees * 4 A Survey on PMSO-Complete Formalisms + 4.1 Presburger Tree Automata + 4.2 Rational-Multiset Tree Automata + 4.3 ACU Equational Tree Automata * 5 A Survey on CMSO-Complete Formalisms + 5.1 Algebraic Recognizability + 5.2 Recognizable-Multiset Tree Automata * 6 New Characterizations for PMSO Definable Sets + 6.1 Equational Tree Languages + 6.2 An Algebraic Characterization of PMSO Definability * 7 New Characterizations for CMSO Definable Sets + 7.1 CMSO-Definability and C-Recognizability + 7.2 CMSO-Definability and Presburger Tree Automata * 8 Some Characterizations for MSO Definable Sets + 8.1 MSO-Definability and Presburger Tree Automata + 8.2 MSO-Definability and Aperiodic-Recognizable Tree Automata + 8.3 An Algebraic Characterization of MSO Definability * References Author Index