Volume
LIPIcs, Volume 10
22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Event
RTA 2011, May 30 to June 1, 2011, Novi Sad, SerbiaEditor
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
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 10, RTA'11, Complete Volume
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
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?
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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}
}