LIPIcs, Volume 10

22nd International Conference on Rewriting Techniques and Applications (RTA'11)



Thumbnail PDF

Event

RTA 2011, May 30 to June 1, 2011, Novi Sad, Serbia

Editor

Manfred Schmidt-Schauss

Publication Details

  • published at: 2011-04-26
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
  • ISBN: 978-3-939897-30-9
  • DBLP: db/conf/rta/rta2011

Access Numbers

Documents

No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 10, RTA'11, Complete Volume

Authors: Manfred Schmidt-Schauß


Abstract
LIPIcs, Volume 10, RTA'11, Complete Volume

Cite as

22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Copy BibTex To Clipboard

@Proceedings{schmidtschau:LIPIcs.RTA.2011,
  title =	{{LIPIcs, Volume 10, RTA'11, Complete Volume}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011},
  URN =		{urn:nbn:de:0030-drops-41045},
  doi =		{10.4230/LIPIcs.RTA.2011},
  annote =	{Keywords: Programming Techniques, Software Engineering, Programming Languages, Computation by Abstract Devices, Analysis of Algorithms and Problem Complexity Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Symbolic and Algebraic Manipulation, Artificial Intelligence}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Conference Organization

Authors: Manfred Schmidt-Schauss


Abstract
Frontmatter, Table of Contents, Preface, Conference Organization

Cite as

22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. i-xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{schmidtschauss:LIPIcs.RTA.2011.i,
  author =	{Schmidt-Schauss, Manfred},
  title =	{{Frontmatter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{i--xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.i},
  URN =		{urn:nbn:de:0030-drops-31099},
  doi =		{10.4230/LIPIcs.RTA.2011.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Conference Organization}
}
Document
Tree Automata, (Dis-)Equality Constraints and Term Rewriting: What's New?

Authors: Sophie Tison


Abstract
Connections between Tree Automata and Term Rewriting are now well known. Whereas tree automata can be viewed as a subclass of ground rewrite systems, tree automata are successfully used as decision tools in rewriting theory. Furthermore, applications, including rewriting theory, have influenced the definition of new classes of tree automata. In this talk, we will first present a short and not exhaustive reminder of some fruitful applications of tree automata in rewriting theory. Then, we will focus on extensions of tree automata, specially tree automata with local or/and global (dis-)equality constraints: we will emphasize new results, compare different extensions, and sketch some applications.

Cite as

Sophie Tison. Tree Automata, (Dis-)Equality Constraints and Term Rewriting: What's New?. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{tison:LIPIcs.RTA.2011.1,
  author =	{Tison, Sophie},
  title =	{{Tree Automata, (Dis-)Equality Constraints and Term Rewriting: What's New?}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{1--2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.1},
  URN =		{urn:nbn:de:0030-drops-31404},
  doi =		{10.4230/LIPIcs.RTA.2011.1},
  annote =	{Keywords: Tree Automata, Constraints, Term Rewriting}
}
Document
Rewriting in Practice

Authors: Ashish Tiwari


Abstract
We discuss applications of rewriting in three different areas: design and analysis of algorithms, theorem proving and term rewriting, and modeling and analysis of biological processes.

Cite as

Ashish Tiwari. Rewriting in Practice. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 3-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{tiwari:LIPIcs.RTA.2011.3,
  author =	{Tiwari, Ashish},
  title =	{{Rewriting in Practice}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{3--8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.3},
  URN =		{urn:nbn:de:0030-drops-31326},
  doi =		{10.4230/LIPIcs.RTA.2011.3},
  annote =	{Keywords: Rewriting, Polynomial constraints, Biochemical reaction networks}
}
Document
Combining Proofs and Programs

Authors: Stephanie Weirich


Abstract
Programming languages based on dependent type theory promise two great advances: flexibility and security. With the type-level computation afforded by dependent types, algorithms can be more generic, as the type system can express flexible interfaces via programming. Likewise, type-level computation can also express data structure invariants, so that programs can be proved correct through type checking. Furthermore, despite these extensions, programmers already know everything. Via the Curry-Howard isomorphism, the language of type-level computation and the verification logic is the programming language itself. There are two current approaches to the design of dependently-typed languages: Coq, Epigram, Agda, which grew out of the logics of proof assistants, require that all expressions terminate. These languages provide decidable type checking and strong correctness guarantees. In contrast, functional programming languages, like Haskell and Omega, have adapted the features dependent type theories, but retain a strict division between types and programs. These languages trade termination obligations for more limited correctness assurances. In this talk, I present a work-in-progress overview of the Trellys project. Trellys is new core language, designed to provide a smooth path from functional programming to dependently-typed programming. Unlike traditional dependent type theories and functional languages, Trellys allows programmers to work with total and partial functions uniformly. The language itself is composed of two fragments that share a common syntax and overlapping semantics: a simple logical language that guarantees total correctness and an expressive call-by-value programming language that guarantees types safety but not termination. Importantly, these two fragments interact. The logical fragment may soundly reason about effectful, partial functions. Program values may be used as evidence by the logic. We call this principle freedom of speech: whereas proofs themselves must terminate, they must be allowed to reason about any function a programmer might write. To retain consistency, the Trellys type system keeps track of where potentially non-terminating computations may appear, so that it can prevent them from being used as proofs.

Cite as

Stephanie Weirich. Combining Proofs and Programs. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, p. 9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{weirich:LIPIcs.RTA.2011.9,
  author =	{Weirich, Stephanie},
  title =	{{Combining Proofs and Programs}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{9--9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.9},
  URN =		{urn:nbn:de:0030-drops-31398},
  doi =		{10.4230/LIPIcs.RTA.2011.9},
  annote =	{Keywords: Dependent types, functional programming}
}
Document
FAST: An Efficient Decision Procedure for Deduction and Static Equivalence

Authors: Bruno Conchinha, David A. Basin, and Carlos Caleiro


Abstract
Message deducibility and static equivalence are central problems in symbolic security protocol analysis. We present FAST, an efficient decision procedure for these problems under subterm-convergent equational theories. FAST is a C++ implementation of an improved version of the algorithm presented in our previous work. This algorithm has a better asymptotic complexity than other algorithms implemented by existing tools for the same task, and FAST's optimizations further improve these complexity results. We describe here the main ideas of our implementation and compare its performance with competing tools. The results show that our implementation is significantly faster: for many examples, FAST terminates in under a second, whereas other tools take several minutes.

Cite as

Bruno Conchinha, David A. Basin, and Carlos Caleiro. FAST: An Efficient Decision Procedure for Deduction and Static Equivalence. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 11-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{conchinha_et_al:LIPIcs.RTA.2011.11,
  author =	{Conchinha, Bruno and Basin, David A. and Caleiro, Carlos},
  title =	{{FAST: An Efficient Decision Procedure for Deduction and Static Equivalence}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{11--20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.11},
  URN =		{urn:nbn:de:0030-drops-31369},
  doi =		{10.4230/LIPIcs.RTA.2011.11},
  annote =	{Keywords: Efficient algorithms, Equational theories, Deducibility, Static equivalence, Security protocols}
}
Document
Automated Certified Proofs with CiME3

Authors: Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain


Abstract
We present the rewriting toolkit CiME3. Amongst other original features, this version enjoys two kinds of engines: to handle and discover proofs of various properties of rewriting systems, and to generate Coq scripts from proof traces given in certification problem format in order to certify them with a skeptical proof assistant like Coq. Thus, these features open the way for using CiME3 to add automation to proofs of termination or confluence in a formal development in the Coq proof assistant.

Cite as

Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 21-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{contejean_et_al:LIPIcs.RTA.2011.21,
  author =	{Contejean, \'{E}velyne and Courtieu, Pierre and Forest, Julien and Pons, Olivier and Urbain, Xavier},
  title =	{{Automated Certified Proofs with CiME3}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{21--30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.21},
  URN =		{urn:nbn:de:0030-drops-31192},
  doi =		{10.4230/LIPIcs.RTA.2011.21},
  annote =	{Keywords: Rewriting, Formal Proof, Proof Automation, Proof Assistant}
}
Document
Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6

Authors: Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer, and Carolyn Talcott


Abstract
This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax cup E), the E,Ax-variants of a term t are understood as the set of all pairs consisting of a substitution sigma and the E,Ax-canonical form of t sigma. The equational theory (Ax cup E ) has the finite variant property if there is a finite set of most general variants. We have added support in Maude 2.6 for: (i) order-sorted unification modulo associativity, commutativity and identity, (ii) variant generation, (iii) order-sorted unification modulo finite variant theories, and (iv) narrowing-based symbolic reachability modulo finite variant theories. We also explain how these features have a number of interesting applications in areas such as unification theory, cryptographic protocol verification, business processes, and proofs of termination, confluence and coherence.

Cite as

Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer, and Carolyn Talcott. Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 31-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{duran_et_al:LIPIcs.RTA.2011.31,
  author =	{Duran, Francisco and Eker, Steven and Escobar, Santiago and Meseguer, Jose and Talcott, Carolyn},
  title =	{{Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{31--40},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.31},
  URN =		{urn:nbn:de:0030-drops-31211},
  doi =		{10.4230/LIPIcs.RTA.2011.31},
  annote =	{Keywords: Rewriting logic, narrowing, unification, variants}
}
Document
Termination Analysis of C Programs Using Compiler Intermediate Languages

Authors: Stephan Falke, Deepak Kapur, and Carsten Sinz


Abstract
Modeling the semantics of programming languages like C for the automated termination analysis of programs is a challenge if complete coverage of all language features should be achieved. On the other hand, low-level intermediate languages that occur during the compilation of C programs to machine code have a much simpler semantics since most of the intricacies of C are taken care of by the compiler frontend. It is thus a promising approach to use these intermediate languages for the automated termination analysis of C programs. In this paper we present the tool KITTeL based on this approach. For this, programs in the compiler intermediate language are translated into term rewrite systems (TRSs), and the termination proof itself is then performed on the automatically generated TRS. An evaluation on a large collection of C programs shows the effectiveness and practicality of KITTeL on "typical" examples.

Cite as

Stephan Falke, Deepak Kapur, and Carsten Sinz. Termination Analysis of C Programs Using Compiler Intermediate Languages. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 41-50, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{falke_et_al:LIPIcs.RTA.2011.41,
  author =	{Falke, Stephan and Kapur, Deepak and Sinz, Carsten},
  title =	{{Termination Analysis of C Programs Using Compiler Intermediate Languages}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{41--50},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.41},
  URN =		{urn:nbn:de:0030-drops-31232},
  doi =		{10.4230/LIPIcs.RTA.2011.41},
  annote =	{Keywords: termination analysis; C programs; compiler intermediate languages}
}
Document
First-Order Unification on Compressed Terms

Authors: Adrià Gascón, Sebastian Maneth, and Lander Ramos


Abstract
Singleton Tree Grammars (STGs) have recently drawn considerable attention. They generalize the sharing of subtrees known from DAGs to sharing of connected subgraphs. This allows to obtain smaller in-memory representations of trees than with DAGs. In the past years some important tree algorithms were proved to perform efficiently (without decompression) over STGs; e.g., type checking, equivalence checking, and unification. We present a tool that implements an extension of the unification algorithm for STGs. This algorithm makes extensive use of equivalence checking. For the latter we implemented two variants, the classical exact one and a recent randomized one. Our experiments show that the randomized algorithm performs better. The running times are also compared to those of unification over uncompressed trees.

Cite as

Adrià Gascón, Sebastian Maneth, and Lander Ramos. First-Order Unification on Compressed Terms. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 51-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{gascon_et_al:LIPIcs.RTA.2011.51,
  author =	{Gasc\'{o}n, Adri\`{a} and Maneth, Sebastian and Ramos, Lander},
  title =	{{First-Order Unification on Compressed Terms}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{51--60},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.51},
  URN =		{urn:nbn:de:0030-drops-31263},
  doi =		{10.4230/LIPIcs.RTA.2011.51},
  annote =	{Keywords: unification, matching, grammars, compression, STG, system C++}
}
Document
Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus

Authors: Niels Bjørn Bugge Grathwohl, Jeroen Ketema, Jens Duelund Pallesen, and Jakob Grue Simonsen


Abstract
We present Anagopos, an open source tool for visualizing reduction graphs of terms in lambda calculus and term rewriting. Anagopos allows step-by-step generation of reduction graphs under six different graph drawing algorithms. We provide ample examples of graphs drawn with the tool.

Cite as

Niels Bjørn Bugge Grathwohl, Jeroen Ketema, Jens Duelund Pallesen, and Jakob Grue Simonsen. Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 61-70, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{grathwohl_et_al:LIPIcs.RTA.2011.61,
  author =	{Grathwohl, Niels Bj{\o}rn Bugge and Ketema, Jeroen and Pallesen, Jens Duelund and Simonsen, Jakob Grue},
  title =	{{Anagopos: A Reduction Graph Visualizer for Term Rewriting and Lambda Calculus}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{61--70},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.61},
  URN =		{urn:nbn:de:0030-drops-31286},
  doi =		{10.4230/LIPIcs.RTA.2011.61},
  annote =	{Keywords: term rewriting, lambda calculus, reduction graphs, visualization}
}
Document
Maximal Completion

Authors: Dominik Klein and Nao Hirokawa


Abstract
Given an equational system, completion procedures compute an equivalent and complete (terminating and confluent) term rewrite system. We present a very simple and efficient completion procedure, which is based on MaxSAT solving. Experiments show that the procedure is comparable to recent powerful completion tools.

Cite as

Dominik Klein and Nao Hirokawa. Maximal Completion. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 71-80, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{klein_et_al:LIPIcs.RTA.2011.71,
  author =	{Klein, Dominik and Hirokawa, Nao},
  title =	{{Maximal Completion}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{71--80},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.71},
  URN =		{urn:nbn:de:0030-drops-31295},
  doi =		{10.4230/LIPIcs.RTA.2011.71},
  annote =	{Keywords: Term Rewriting, Knuth-Bendix Completion, Multi-completion}
}
Document
CRSX - Combinatory Reduction Systems with Extensions

Authors: Kristoffer H. Rose


Abstract
Combinatory Reduction Systems with Extensions (CRSX) is a system available from http://crsx.sourceforge.net and characterized by the following properties: - Higher-order rewriting engine based on pure Combinatory Reduction Systems with full strong reduction (but no specified reduction strategy). - Rule and term syntax based on lambda-calculus and term rewriting conventions including Unicode support. - Strict checking and declaration requirements to avoid idiosyncratic errors in rewrite rules. - Interpreter is implemented in Java 5 and usable stand-alone as well as from an Eclipse plugin (under development). - Includes a custom parser generator (front-end to JavaCC parser generator) designed to ease parsing directly into higher-order abstract syntax (as well as permitting the use of custom syntax in rules files). - Experimental (and evolving) sort system to help rule management. - Compiler from (well-sorted deterministic subset of) CRSX to stand-alone C code.

Cite as

Kristoffer H. Rose. CRSX - Combinatory Reduction Systems with Extensions. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 81-90, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{rose:LIPIcs.RTA.2011.81,
  author =	{Rose, Kristoffer H.},
  title =	{{CRSX - Combinatory Reduction Systems with Extensions}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{81--90},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.81},
  URN =		{urn:nbn:de:0030-drops-31301},
  doi =		{10.4230/LIPIcs.RTA.2011.81},
  annote =	{Keywords: Higher-Order Rewriting, Compilers}
}
Document
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems

Authors: Takahito Aoto and Yoshihito Toyama


Abstract
We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and usual termination. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into terminating part and possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.

Cite as

Takahito Aoto and Yoshihito Toyama. A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 91-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.RTA.2011.91,
  author =	{Aoto, Takahito and Toyama, Yoshihito},
  title =	{{A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{91--106},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.91},
  URN =		{urn:nbn:de:0030-drops-31105},
  doi =		{10.4230/LIPIcs.RTA.2011.91},
  annote =	{Keywords: Confluence, Completion, Equational Term Rewriting Systems, Confluence Modulo Equations}
}
Document
Natural Inductive Theorems for Higher-Order Rewriting

Authors: Takahito Aoto, Toshiyuki Yamada, and Yuki Chiba


Abstract
The notion of inductive theorems is well-established in first-order term rewriting. In higher-order term rewriting, in contrast, it is not straightforward to extend this notion because of extensionality (Meinke, 1992). When extending the term rewriting based program transformation of Chiba et al. (2005) to higher-order term rewriting, we need extensibility, a property stating that inductive theorems are preserved by adding new functions via macros. In this paper, we propose and study a new notion of inductive theorems for higher-order rewriting, natural inductive theorems. This allows to incorporate properties such as extensionality and extensibility, based on simply typed S-expression rewriting (Yamada, 2001).

Cite as

Takahito Aoto, Toshiyuki Yamada, and Yuki Chiba. Natural Inductive Theorems for Higher-Order Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 107-121, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.RTA.2011.107,
  author =	{Aoto, Takahito and Yamada, Toshiyuki and Chiba, Yuki},
  title =	{{Natural Inductive Theorems for Higher-Order Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{107--121},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.107},
  URN =		{urn:nbn:de:0030-drops-31119},
  doi =		{10.4230/LIPIcs.RTA.2011.107},
  annote =	{Keywords: Inductive Theorems, Higher-Order Equational Logic, Simply-Typed S-Expression Rewriting Systems, Term Rewriting Systems}
}
Document
A Path Order for Rewrite Systems that Compute Exponential Time Functions

Authors: Martin Avanzini, Naohi Eguchi, and Georg Moser


Abstract
In this paper we present a new path order for rewrite systems, the exponential path order EPO*. Suppose a term rewrite system is compatible with EPO*, then the runtime complexity of this rewrite system is bounded from above by an exponential function. Furthermore, the class of function computed by a rewrite system compatible with EPO* equals the class of functions computable in exponential time on a Turing machine.

Cite as

Martin Avanzini, Naohi Eguchi, and Georg Moser. A Path Order for Rewrite Systems that Compute Exponential Time Functions. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 123-138, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{avanzini_et_al:LIPIcs.RTA.2011.123,
  author =	{Avanzini, Martin and Eguchi, Naohi and Moser, Georg},
  title =	{{A Path Order for Rewrite Systems that Compute Exponential Time Functions}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{123--138},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.123},
  URN =		{urn:nbn:de:0030-drops-31127},
  doi =		{10.4230/LIPIcs.RTA.2011.123},
  annote =	{Keywords: Runtime Complexity, Exponential Time Functions, Implicit Computational Complexity}
}
Document
Modes of Convergence for Term Graph Rewriting

Authors: Patrick Bahr


Abstract
Term graph rewriting provides a simple mechanism to finitely represent restricted forms of infinitary term rewriting. The correspondence between infinitary term rewriting and term graph rewriting has been studied to some extent. However, this endeavour is impaired by the lack of an appropriate counterpart of infinitary rewriting on the side of term graphs. We aim to fill this gap by devising two modes of convergence based on a partial order resp. a metric on term graphs. The thus obtained structures generalise corresponding modes of convergence that are usually studied in infinitary term rewriting. We argue that this yields a common framework in which both term rewriting and term graph rewriting can be studied. In order to substantiate our claim, we compare convergence on term graphs and on terms. In particular, we show that the resulting infinitary calculi of term graph rewriting exhibit the same correspondence as we know it from term rewriting: Convergence via the partial order is a conservative extension of the metric convergence.

Cite as

Patrick Bahr. Modes of Convergence for Term Graph Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 139-154, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.RTA.2011.139,
  author =	{Bahr, Patrick},
  title =	{{Modes of Convergence for Term Graph Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{139--154},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.139},
  URN =		{urn:nbn:de:0030-drops-31131},
  doi =		{10.4230/LIPIcs.RTA.2011.139},
  annote =	{Keywords: term graphs, partial order, metric, infinitary rewriting, graph rewriting}
}
Document
Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

Authors: Marc Brockschmidt, Carsten Otto, and Jürgen Giesl


Abstract
In earlier work we presented an approach to prove termination of non-recursive Java Bytecode (JBC) programs automatically. Here, JBC programs are first transformed to finite termination graphs which represent all possible runs of the program. Afterwards, the termination graphs are translated to term rewrite systems (TRSs) such that termination of the resulting TRSs implies termination of the original JBC programs. So in this way, existing techniques and tools from term rewriting can be used to prove termination of JBC automatically. In this paper, we improve this approach substantially in two ways: (1) We extend it in order to also analyze recursive JBC programs. To this end, one has to represent call stacks of arbitrary size. (2) To handle JBC programs with several methods, we modularize our approach in order to re-use termination graphs and TRSs for the separate methods and to prove termination of the resulting TRS in a modular way. We implemented our approach in the tool AProVE. Our experiments show that the new contributions increase the power of termination analysis for JBC significantly.

Cite as

Marc Brockschmidt, Carsten Otto, and Jürgen Giesl. Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 155-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{brockschmidt_et_al:LIPIcs.RTA.2011.155,
  author =	{Brockschmidt, Marc and Otto, Carsten and Giesl, J\"{u}rgen},
  title =	{{Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{155--170},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.155},
  URN =		{urn:nbn:de:0030-drops-31146},
  doi =		{10.4230/LIPIcs.RTA.2011.155},
  annote =	{Keywords: termination, Java Bytecode, term rewriting, recursion}
}
Document
Rewriting-based Quantifier-free Interpolation for a Theory of Arrays

Authors: Roberto Bruttomesso, Silvio Ghilardi, and Silvio Ranise


Abstract
The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier-free interpolants in general. In this paper, we show that, with a minor extension to the theory of arrays, it is possible to obtain quantifier-free interpolants. We prove this by designing an interpolating procedure, based on solving equations between array updates. Rewriting techniques are used in the key steps of the solver and its proof of correctness. To the best of our knowledge, this is the first successful attempt of computing quantifier-free interpolants for a theory of arrays.

Cite as

Roberto Bruttomesso, Silvio Ghilardi, and Silvio Ranise. Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 171-186, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{bruttomesso_et_al:LIPIcs.RTA.2011.171,
  author =	{Bruttomesso, Roberto and Ghilardi, Silvio and Ranise, Silvio},
  title =	{{Rewriting-based Quantifier-free Interpolation for a Theory of Arrays}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{171--186},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.171},
  URN =		{urn:nbn:de:0030-drops-31155},
  doi =		{10.4230/LIPIcs.RTA.2011.171},
  annote =	{Keywords: rewriting, interpolation, arrays, model-checking}
}
Document
Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars

Authors: Jonathan Kochems and C.H. Luke Ong


Abstract
The collecting semantics of a program defines the strongest static property of interest. We study the analysis of the collecting semantics of higher-order functional programs, cast as left-linear term rewriting systems. The analysis generalises functional flow analysis and the reachability problem for term rewriting systems, which are both undecidable. We present an algorithm that uses indexed linear tree grammars (ILTGs) both to describe the input set and compute the set that approximates the collecting semantics. ILTGs are equi-expressive with pushdown tree automata, and so, strictly more expressive than regular tree grammars. Our result can be seen as a refinement of Jones and Andersen's procedure, which uses regular tree grammars. The main technical innovation of our algorithm is the use of indices to capture (sets of) substitutions, thus enabling a more precise binding analysis than afforded by regular grammars. We give a simple proof of termination and soundness, and demonstrate that our method is more accurate than other approaches to functional flow and reachability analyses in the literature.

Cite as

Jonathan Kochems and C.H. Luke Ong. Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 187-202, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{kochems_et_al:LIPIcs.RTA.2011.187,
  author =	{Kochems, Jonathan and Ong, C.H. Luke},
  title =	{{Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{187--202},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.187},
  URN =		{urn:nbn:de:0030-drops-31167},
  doi =		{10.4230/LIPIcs.RTA.2011.187},
  annote =	{Keywords: Flow analysis, reachability, collecting semantics, higher-order program, term rewriting, indexed linear tree grammar}
}
Document
Higher Order Dependency Pairs for Algebraic Functional Systems

Authors: Cynthia Kop and Femke van Raamsdonk


Abstract
We extend the termination method using dynamic dependency pairs to higher order rewriting systems with beta as a rewrite step, also called Algebraic Functional Systems (AFSs). We introduce a variation of usable rules, and use monotone algebras to solve the constraints generated by dependency pairs. This approach differs in several respects from those dealing with higher order rewriting modulo beta (e.g. HRSs).

Cite as

Cynthia Kop and Femke van Raamsdonk. Higher Order Dependency Pairs for Algebraic Functional Systems. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 203-218, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.RTA.2011.203,
  author =	{Kop, Cynthia and van Raamsdonk, Femke},
  title =	{{Higher Order Dependency Pairs for Algebraic Functional Systems}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{203--218},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.203},
  URN =		{urn:nbn:de:0030-drops-31177},
  doi =		{10.4230/LIPIcs.RTA.2011.203},
  annote =	{Keywords: higher order rewriting, termination, dynamic dependency pairs}
}
Document
Anti-Unification for Unranked Terms and Hedges

Authors: Temur Kutsia, Jordi Levy, and Mateu Villaret


Abstract
We study anti-unification for unranked terms and hedges that may contain term and hedge variables. The anti-unification problem of two hedges ~s_1 and ~s_2 is concerned with finding their generalization, a hedge ~q such that both ~s_1 and ~s_2 are instances of ~q under some substitutions. Hedge variables help to fill in gaps in generalizations, while term variables abstract single (sub)terms with different top function symbols. First, we design a complete and minimal algorithm to compute least general generalizations. Then, we improve the efficiency of the algorithm by restricting possible alternatives permitted in the generalizations. The restrictions are imposed with the help of a rigidity function that is a parameter in the improved algorithm and selects certain common subsequences from the hedges to be generalized. Finally, we indicate a possible application of the algorithm in software engineering.

Cite as

Temur Kutsia, Jordi Levy, and Mateu Villaret. Anti-Unification for Unranked Terms and Hedges. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 219-234, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{kutsia_et_al:LIPIcs.RTA.2011.219,
  author =	{Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{Anti-Unification for Unranked Terms and Hedges}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{219--234},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.219},
  URN =		{urn:nbn:de:0030-drops-31181},
  doi =		{10.4230/LIPIcs.RTA.2011.219},
  annote =	{Keywords: Anti-unification, generalization, unranked terms, hedges, software clones.}
}
Document
Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity

Authors: Georg Moser and Andreas Schnabl


Abstract
We study the complexity of rewrite systems shown terminating via the dependency pair framework using processors for reduction pairs, dependency graphs, or the subterm criterion. The complexity of such systems is bounded by a multiple recursive function, provided the complexity induced by the employed base techniques is at most multiple recursive. Moreover this upper bound is tight.

Cite as

Georg Moser and Andreas Schnabl. Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 235-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{moser_et_al:LIPIcs.RTA.2011.235,
  author =	{Moser, Georg and Schnabl, Andreas},
  title =	{{Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{235--250},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.235},
  URN =		{urn:nbn:de:0030-drops-31208},
  doi =		{10.4230/LIPIcs.RTA.2011.235},
  annote =	{Keywords: Complexity, DP Framework, Multiple Recursive Functions}
}
Document
Revisiting Matrix Interpretations for Proving Termination of Term Rewriting

Authors: Friedrich Neurauter and Aart Middeldorp


Abstract
Matrix interpretations are a powerful technique for proving termination of term rewrite systems, which is based on the well-known paradigm of interpreting terms into a domain equipped with a suitable well-founded order, such that every rewrite step causes a strict decrease. Traditionally, one uses vectors of non-negative numbers as domain, where two vectors are in the order relation if there is a strict decrease in the respective first components and a weak decrease in all other components. In this paper, we study various alternative well-founded orders on vectors of non-negative numbers based on vector norms and compare the resulting variants of matrix interpretations to each other and to the traditional approach. These comparisons are mainly theoretical in nature. We do, however, also identify one of these variants as a proper generalization of traditional matrix interpretations as a stand-alone termination method, which has the additional advantage that it gives rise to a more powerful implementation.

Cite as

Friedrich Neurauter and Aart Middeldorp. Revisiting Matrix Interpretations for Proving Termination of Term Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 251-266, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{neurauter_et_al:LIPIcs.RTA.2011.251,
  author =	{Neurauter, Friedrich and Middeldorp, Aart},
  title =	{{Revisiting Matrix Interpretations for Proving Termination of Term Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{251--266},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.251},
  URN =		{urn:nbn:de:0030-drops-31222},
  doi =		{10.4230/LIPIcs.RTA.2011.251},
  annote =	{Keywords: term rewriting, termination, matrix interpretations}
}
Document
Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity

Authors: Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe


Abstract
Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound for every CTRS w.r.t. reduction, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for deterministic CTRSs is sound w.r.t. reduction if the corresponding unraveled TRSs are left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling.

Cite as

Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe. Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 267-282, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{nishida_et_al:LIPIcs.RTA.2011.267,
  author =	{Nishida, Naoki and Sakai, Masahiko and Sakabe, Toshiki},
  title =	{{Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{267--282},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.267},
  URN =		{urn:nbn:de:0030-drops-31244},
  doi =		{10.4230/LIPIcs.RTA.2011.267},
  annote =	{Keywords: conditional term rewriting, program transformation}
}
Document
Program Inversion for Tail Recursive Functions

Authors: Naoki Nishida and German Vidal


Abstract
Program inversion is a fundamental problem that has been addressed in many different programming settings and applications. In the context of term rewriting, several methods already exist for computing the inverse of an injective function. These methods, however, usually return non-terminating inverted functions when the considered function is tail recursive. In this paper, we propose a direct and intuitive approach to the inversion of tail recursive functions. Our new technique is able to produce good results even without the use of an additional post-processing of determinization or completion. Moreover, when combined with a traditional approach to program inversion, it constitutes a promising approach to define a general method for program inversion. Our experimental results confirm that the new technique compares well with previous approaches.

Cite as

Naoki Nishida and German Vidal. Program Inversion for Tail Recursive Functions. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 283-298, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{nishida_et_al:LIPIcs.RTA.2011.283,
  author =	{Nishida, Naoki and Vidal, German},
  title =	{{Program Inversion for Tail Recursive Functions}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{283--298},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.283},
  URN =		{urn:nbn:de:0030-drops-31253},
  doi =		{10.4230/LIPIcs.RTA.2011.283},
  annote =	{Keywords: term rewriting, program transformation, termination}
}
Document
Refinement Types as Higher-Order Dependency Pairs

Authors: Cody Roux


Abstract
Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of rewrite systems; however its extension to higher-order rewrite systems is still the subject of active research. We observe that a variant of refinement types allows us to express a form of higher-order dependency pair method: from the rewrite system labeled with typing information, we build a type-level approximated dependency graph, and describe a type level embedding preorder. We describe a syntactic termination criterion involving the graph and the preorder, which generalizes the simple projection criterion of Middeldorp and Hirokawa, and prove our main result: if the graph passes the criterion, then every well-typed term is strongly normalizing.

Cite as

Cody Roux. Refinement Types as Higher-Order Dependency Pairs. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 299-312, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{roux:LIPIcs.RTA.2011.299,
  author =	{Roux, Cody},
  title =	{{Refinement Types as Higher-Order Dependency Pairs}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{299--312},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.299},
  URN =		{urn:nbn:de:0030-drops-31273},
  doi =		{10.4230/LIPIcs.RTA.2011.299},
  annote =	{Keywords: Dependency Pairs, Higher-Order, Refinement Types}
}
Document
Weakening the Axiom of Overlap in Infinitary Lambda Calculus

Authors: Paula Severi and Fer-Jan de Vries


Abstract
In this paper we present a set of necessary and sufficient conditions on a set of lambda terms to serve as the set of meaningless terms in an infinitary bottom extension of lambda calculus. So far only a set of sufficient conditions was known for choosing a suitable set of meaningless terms to make this construction produce confluent extensions. The conditions covered the three main known examples of sets of meaningless terms. However, the much later construction of many more examples of sets of meaningless terms satisfying the sufficient conditions renewed the interest in the necessity question and led us to reconsider the old conditions. The key idea in this paper is an alternative solution for solving the overlap between beta reduction and bottom reduction. This allows us to reformulate the Axiom of Overlap, which now determines together with the other conditions a larger class of sets of meaningless terms. We show that the reformulated conditions are not only sufficient but also necessary for obtaining a confluent and normalizing infinitary lambda beta bottom calculus. As an interesting consequence of the necessity proof we obtain for infinitary lambda calculus with beta and bot reduction that confluence implies normalization.

Cite as

Paula Severi and Fer-Jan de Vries. Weakening the Axiom of Overlap in Infinitary Lambda Calculus. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 313-328, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{severi_et_al:LIPIcs.RTA.2011.313,
  author =	{Severi, Paula and de Vries, Fer-Jan},
  title =	{{Weakening the Axiom of Overlap in Infinitary Lambda Calculus}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{313--328},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.313},
  URN =		{urn:nbn:de:0030-drops-31312},
  doi =		{10.4230/LIPIcs.RTA.2011.313},
  annote =	{Keywords: Infinitary Lambda Calculus, Confluence, Normalization}
}
Document
Modular and Certified Semantic Labeling and Unlabeling

Authors: Christian Sternagel and René Thiemann


Abstract
Semantic labeling is a powerful transformation technique to prove termination of term rewrite systems. The dual technique is unlabeling. For unlabeling it is essential to drop the so called decreasing rules which sometimes have to be added when applying semantic labeling. We indicate two problems concerning unlabeling and present our solutions. The first problem is that currently unlabeling cannot be applied as a modular step, since the decreasing rules are determined by a semantic labeling step which may have taken place much earlier. To this end, we give an implicit definition of decreasing rules that does not depend on any knowledge about preceding labelings. The second problem is that unlabeling is in general unsound. To solve this issue, we introduce the notion of extended termination problems. Moreover, we show how existing termination techniques can be lifted to operate on extended termination problems. All our proofs have been formalized in Isabelle/HOL as part of the IsaFoR/CeTA project.

Cite as

Christian Sternagel and René Thiemann. Modular and Certified Semantic Labeling and Unlabeling. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 329-344, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{sternagel_et_al:LIPIcs.RTA.2011.329,
  author =	{Sternagel, Christian and Thiemann, Ren\'{e}},
  title =	{{Modular and Certified Semantic Labeling and Unlabeling}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{329--344},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.329},
  URN =		{urn:nbn:de:0030-drops-31333},
  doi =		{10.4230/LIPIcs.RTA.2011.329},
  annote =	{Keywords: semantic labeling, certification, term rewriting, unlabeling}
}
Document
Type Preservation as a Confluence Problem

Authors: Aaron Stump, Garrin Kimmell, and Roba El Haj Omar


Abstract
This paper begins with recent work by Kuan, MacQueen, and Findler, which shows how standard type systems, such as the simply typed lambda calculus, can be viewed as abstract reduction systems operating on terms. The central idea is to think of the process of typing a term as the computation of an abstract value for that term. The standard metatheoretic property of type preservation can then be seen as a confluence problem involving the concrete and abstract operational semantics, viewed as abstract reduction systems (ARSs). In this paper, we build on the work of Kuan et al. by showing show how modern ARS theory, in particular the theory of decreasing diagrams, can be used to establish type preservation via confluence. We illustrate this idea through several examples of solving such problems using decreasing diagrams. We also consider how automated tools for analysis of term-rewriting systems can be applied in testing type

Cite as

Aaron Stump, Garrin Kimmell, and Roba El Haj Omar. Type Preservation as a Confluence Problem. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 345-360, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{stump_et_al:LIPIcs.RTA.2011.345,
  author =	{Stump, Aaron and Kimmell, Garrin and El Haj Omar, Roba},
  title =	{{Type Preservation as a Confluence Problem}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{345--360},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.345},
  URN =		{urn:nbn:de:0030-drops-31343},
  doi =		{10.4230/LIPIcs.RTA.2011.345},
  annote =	{Keywords: Term rewriting, Type Safety, Confluence}
}
Document
Left-linear Bounded TRSs are Inverse Recognizability Preserving

Authors: Irène Durand and Marc Sylvestre


Abstract
Bounded rewriting for linear term rewriting systems has been defined in (I. Durand, G. Sénizergues, M. Sylvestre. Termination of linear bounded term rewriting systems. Proceedings of the 21st International Conference on Rewriting Techniques and Applications) as a restriction of the usual notion of rewriting. We extend here this notion to the whole class of left-linear term rewriting systems, and we show that bounded rewriting is effectively inverse-recognizability preserving. The bounded class (BO) is, by definition, the set of left-linear systems for which every derivation can be replaced by a bottom-up derivation. The class BO contains (strictly) several classes of systems which were already known to be inverse-recognizability preserving: the left-linear growing systems, and the inverse right-linear finite-path overlapping systems.

Cite as

Irène Durand and Marc Sylvestre. Left-linear Bounded TRSs are Inverse Recognizability Preserving. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 361-376, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{durand_et_al:LIPIcs.RTA.2011.361,
  author =	{Durand, Ir\`{e}ne and Sylvestre, Marc},
  title =	{{Left-linear Bounded TRSs are Inverse Recognizability Preserving}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{361--376},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.361},
  URN =		{urn:nbn:de:0030-drops-31350},
  doi =		{10.4230/LIPIcs.RTA.2011.361},
  annote =	{Keywords: Term Rewriting, Preservation of Recognizability, Rewriting Strategies}
}
Document
Labelings for Decreasing Diagrams

Authors: Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp


Abstract
This paper is concerned with automating the decreasing diagrams technique of van Oostrom for establishing confluence of term rewrite systems. We study abstract criteria that allow to lexicographically combine labelings to show local diagrams decreasing. This approach has two immediate benefits. First, it allows to use labelings for linear rewrite systems also for left-linear ones, provided some mild conditions are satisfied. Second, it admits an incremental method for proving confluence which subsumes recent developments in automating decreasing diagrams. The techniques proposed in the paper have been implemented and experimental results demonstrate how, e.g., the rule labeling benefits from our contributions.

Cite as

Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp. Labelings for Decreasing Diagrams. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 377-392, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{zankl_et_al:LIPIcs.RTA.2011.377,
  author =	{Zankl, Harald and Felgenhauer, Bertram and Middeldorp, Aart},
  title =	{{Labelings for Decreasing Diagrams}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{377--392},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.377},
  URN =		{urn:nbn:de:0030-drops-31378},
  doi =		{10.4230/LIPIcs.RTA.2011.377},
  annote =	{Keywords: term rewriting, confluence, decreasing diagrams, labeling}
}
Document
Proving Equality of Streams Automatically

Authors: Hans Zantema and Joerg Endrullis


Abstract
Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. In this paper we focus on equality of streams, more precisely, for a given set of equations two stream terms are said to be equal if they are equal in every model satisfying the given equations. We investigate techniques for proving equality of streams suitable for automation. Apart from techniques that were already available in the tool CIRC from Lucanu and Rosu, we also exploit well-definedness of streams, typically proved by proving productivity. Moreover, our approach does not restrict to behavioral input format and does not require termination. We present a tool Streambox that can prove equality of a wide range of examples fully automatically.

Cite as

Hans Zantema and Joerg Endrullis. Proving Equality of Streams Automatically. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 393-408, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{zantema_et_al:LIPIcs.RTA.2011.393,
  author =	{Zantema, Hans and Endrullis, Joerg},
  title =	{{Proving Equality of Streams Automatically}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{393--408},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.393},
  URN =		{urn:nbn:de:0030-drops-31381},
  doi =		{10.4230/LIPIcs.RTA.2011.393},
  annote =	{Keywords: streams}
}

Filters


Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail