Rewriting Techniques and Applications: 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009 Proceedings

This book constitutes the refereed proceedings of the 20th International Conference on Rewriting Techniques and Applications, RTA 2009, held in Brasília, Brazil, during June 29 - July 1, 2009. The 22 revised full papers and four system descriptions presented were carefully reviewed and selected from 59 initial submissions. The papers cover current research on all aspects of rewriting including typical areas of interest such as applications, foundational issues, frameworks, implementations, and semantics. Table of Contents Cover Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29-July 1, 2009, Proceedings ISBN-10 3642023479 ISBN-13 9783642023477 Preface Organization Table of Contents Automatic Termination * Introduction * Automata, Rewriting, ...and Termination? * Weighted Automata ... * ... for Termination of Rewriting * Matrix Interpretations * Weighted Tree Automata * Half-Strict Semirings * Match Heights * Constraint Solving * Automata Completion * Matrix Termination Hierarchy * Weighted Automata for Derivational Complexity * References Loops under Strategies * Introduction * Loops * Deciding Outermost Loops * Deciding Solvability of Extended Matching Problems * Deciding Solvability of Extended Identity Problems * Empirical Results * Conclusion and Future Work * References Proving Termination of Integer Term Rewriting * Introduction * Integer Term Rewriting * Integer Dependency Pair Framework * Conditional Constraints * Generating I-Interpretations * Experiments and Conclusion * References Dependency Pairs and Polynomial Path Orders * Introduction * The Polynomial Path Order on Sequences * Complexity Analysis Based on the Dependency Pair Method * The Polynomial Path Order over Quasi-precedences * Dependency Pairs and Polynomial Path Orders * Experimental Results * Conclusion * References Unique Normalization for Shallow TRS * Preliminaries * Decidability of UN for Shallow and Linear TRS + Preliminary Results + Necessary and Sufficient Conditions for UN + Decision of UN * Undecidability of UN for Flat and Right-Linear TRS * References The Existential Fragment of the One-Step Parallel Rewriting Theory * Introduction * Preliminaries + One-Step Parallel Rewriting Theory * The Undecidability Construction + Left-Terminal Turing Machines + Rewriting and LTTM * Discussion * References Proving Confluence of Term Rewriting Systems Automatically * Introduction * Preliminaries * Direct Methods * Divide and Conquer Methods + Persistent Decomposition + Layer-Preserving Decomposition + Commutative Decomposition * Implementation and Experiments * Conclusion * References A Proof Theoretic Analysis of Intruder Theories * Introduction * Intruder Deduction Under AC Convergent Theories * Cut Elimination for {\mathcal S} * Normal Derivations and Decidability * Some Example Theories * Combining Disjoint Convergent Theories * Conclusion and Related Work * References Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case * Introduction * Modeling and Some Undecidability Results + Protocols + Related classes * Results on Unification * The Normalization Algorithm * Conclusion * References Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions * Introduction * Rewriting and Security + Term Rewriting + A Relevant Equational Theory + Semantic Subterms + Deducibility Constraints * The Four Main Properties + Locality + Conservativity + Finite Variant Property + A Decision Algorithm for Deducibility Constraints * Pure Deducibility Constraints + Reduction to Three Recipe Types + Guessing Top Symbols and Equalities + Stabilizing the Root Symbol + Eliminating Variables from Left Hand Sides: Reducing Deducibility Constraints to Linear Diophantine Equations + Turning Deduction Constraints into Linear Diophantine Equations + Solving the System of Equations * Conclusion * References YAPA: A Generic Tool for Computing Intruder Knowledge * Introduction * Preliminaries + Term Algebra + Rewriting + Equational Theories * Deducibility and Static Equivalence + Deducibility, Recipes + Static Equivalence, Visible Equations * Main Procedure + Decompositions of Rewrite Rules + Transformation Rules + Application to Deduction and Static Equivalence * Soundness and Completeness of the Saturation * Termination and Non-failure + A Syntactic Criterion to Prevent Failure + Termination * Implementation: The YAPA Tool * References Well-Definedness of Streams by Termination * Introduction * Streams: Specifications and Models * The Observational Variant * The Main Theorem * Data Independent Stream Functions * Fixpoints * Conclusions * References Modularity of Convergence in Infinitary Rewriting * Introduction * Basic Definitions and Results about Convergence * Infinitary Term Rewriting * Counterexamples and Near Counterexamples * Definitions and Observations Useful for Both Proofs * Modularity of Convergence * Modularity of Strong Convergence * Conclusion * References A Heterogeneous Pushout Approach to Term-Graph Transformation * Introduction * Graphs * Rewriting * Examples * Related Work * Conclusion * References An Explicit Framework for Interaction Nets * Introduction * Permutations and Partial Injections + Permutations + Partial Injections + Execution + $w$-Permutations and Ex-Composition * The Statics of Interaction Nets + Representation + Morphisms of Nets and Renaming * Tools of the Trade + Gluing and Cutting + Interfaces and Contexts * Dynamics * Interaction Nets are the {\sf E}x-Collapse of Axiom/Cut Nets + Definition and Juxtaposition + {\sf E}x-collapse * Conclusion * References Dual Calculus with Inductive and Coinductive Types * Introduction * Dual Calculus {\tt DC} * Dual Calculus {\sf DC}$_{\mu\nu} with Inductive and Coinductive Types * Examples * Second-Order Dual Calculus {\tt DC}2 * Strong Normalization of {\tt DC}$_{\mu\nu} * References Comparing Böhm-Like Trees * Introduction * Preliminaries * Infinitary Rewriting + Axioms + Meaningful Terms + Böhm-Like Trees + Extending $U$ with $\perp$ + Examples * Comparison + From Infinitary Rewriting to Direct Approximants + From Direct Approximants to Infinitary Rewriting * Conclusion * References The Derivational Complexity Induced by the Dependency Pair Method * Introduction * Dependency Pairs * Progenitor and Progeny * Dependency Pairs and Complexity * The Lower Bound * Conclusion * References Local Termination * Introduction * Preliminaries * Local Termination * Local Relative Termination * Stepwise Removal of Rules * Via Models from Local to Global Termination * Quasi-models for Local Termination * Conclusion * References VMTL-A Modular Termination Laboratory * Introduction and Overview * Preliminaries + The Context-Sensitive Dependency Pair Framework * User Interface + User Defined Strategies * VMTL API + Adding New Dependency Pair Processors + Adding New Transformations + Customizing Output Formatting * Termination of CTRSs * Implementation Details and Benchmarks * Conclusion, Related and Future Work * References Tyrolean Termination Tool 2 * Introduction * Design + Command Line Interface + Web Interface * The Strategy Language + Syntax + Semantics + Specification and Configuration * A Selection of Implemented Techniques * ${\sf T_{T}T}_{2}$ in Action * Future Work * Conclusion * References From Outermost to Context-Sensitive Rewriting * Introduction * Preliminaries * Transformation by Dynamic Labeling * Constructing Suitable Algebras * Minimizing Algebras * Two Versions of Dynamic Labeling * Discussion * References A Fully Abstract Semantics for Constructor Systems * Introduction * Preliminaries * A Semantics for CS + SCTerms: The Pieces of the Semantics + A Proof Calculus + Relation with Rewriting * Full Abstraction * Conclusions * References The $\Pi^{0}_{2}$-Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity) * (Uniform) Undecidability in Term Rewriting * Preliminaries + Turing Machines + The Arithmetical Hierarchy and $\Pi^{0}_{2}$ * Encoding Turing Machines + Adding Rules for Ground-WCR and CR: the Encoding $\triangle$g(M) * $\Pi^{0}_{2}$-Completeness of the Standard Properties + (Ground-)Local Confluence + (Ground-)Confluence + Normalization + Termination + Completeness * $\Pi^{0}_{2}$-Completeness of Productivity (of Stream Specifications) * References Unification in the Description Logic EL * Introduction * Unification in {\mathcal EL} * Equivalence and Subsumption in {\mathcal EL} * An {\mathcal EL}-Unification Problem of Type Zero * The Decision Problem * Unification in Semilattices with Monotone Operators * Conclusion * References Unification with Singleton Tree Grammars * Introduction + Outline of the Algorithm * Preliminaries * Basic Operations with STG and SCFG + Known Results + Finding the First Different Position of Two Terms + Application of Substitutions and a Notion of Restricted Depth * A Polynomial Time Algorithm for First-Order Unification with STG * Conclusion and Further Research * References Unification and Narrowing in Maude 2.4 * Introduction * Unification * Narrowing * Other Available Features * Some Applications * References Author Index