Volume
LIPIcs, Volume 36
26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Event
RTA 2015, June 29 to July 1, 2015, Warsaw, PolandEditor
Publication Details
- published at: 2015-06-18
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-85-9
- DBLP: db/conf/rta/rta2015
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 36, RTA'15, Complete Volume
Abstract
LIPIcs, Volume 35, RTA'15, Complete Volume
Cite as
26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@Proceedings{fernandez:LIPIcs.RTA.2015,
title = {{LIPIcs, Volume 36, RTA'15, Complete Volume}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015},
URN = {urn:nbn:de:0030-drops-52620},
doi = {10.4230/LIPIcs.RTA.2015},
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
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fernandez:LIPIcs.RTA.2015.i,
author = {Fern\'{a}ndez, Maribel},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {i--xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.i},
URN = {urn:nbn:de:0030-drops-51837},
doi = {10.4230/LIPIcs.RTA.2015.i},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Port Graphs, Rules and Strategies for Dynamic Data Analytics - Extended Abstract (Invited Talk)
Abstract
In the context of understanding, planning and anticipating the behaviour of complex systems, such as biological networks or social networks, this paper proposes port graphs, rules and strategies, combined in strategic rewrite programs, as foundational ingredients for interactive and visual programming and shows how they can contribute to dynamic data analytics.
Cite as
Hélène Kirchner. Port Graphs, Rules and Strategies for Dynamic Data Analytics - Extended Abstract (Invited Talk). In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kirchner:LIPIcs.RTA.2015.1,
author = {Kirchner, H\'{e}l\`{e}ne},
title = {{Port Graphs, Rules and Strategies for Dynamic Data Analytics - Extended Abstract}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {1--4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.1},
URN = {urn:nbn:de:0030-drops-51842},
doi = {10.4230/LIPIcs.RTA.2015.1},
annote = {Keywords: Graphs, Rewrite Rules, Strategic Rewriting}
}
Document
Invited Talk
Matching Logic - Extended Abstract (Invited Talk)
Abstract
This paper presents matching logic, a first-order logic (FOL)
variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives and quantifiers,
but no difference is made between function and predicate symbols.
In models, a pattern evaluates into a power-set domain (the set of values that match it), in contrast to FOL where functions and predicates map into a regular domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have a rewrite-based operational semantics.
Cite as
Grigore Rosu. Matching Logic - Extended Abstract (Invited Talk). In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 5-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{rosu:LIPIcs.RTA.2015.5,
author = {Rosu, Grigore},
title = {{Matching Logic - Extended Abstract}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {5--21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.5},
URN = {urn:nbn:de:0030-drops-51859},
doi = {10.4230/LIPIcs.RTA.2015.5},
annote = {Keywords: Program logic, First-order logic, Rewriting, Verification}
}
Document
Invited Talk
Executable Formal Models in Rewriting Logic (Invited Talk)
Abstract
Formal executable models provide a means to gain insights into the behavior of complex distributed systems. Ideas can be prototyped and assurance gained by carrying out analyses at different levels of fidelity: searching for desirable or undesirable behaviors, determining effects of perturbing the system, and eventually investing effort to carry out formal proofs of key properties. This modeling approach applies to a wide range of systems, including a variety of protocols and networked cyber-physical systems. It is also emerging as an important tool in understanding many different aspects of biological systems.
Rewriting logic (RWL) is a formalism that is well-suited to developing and working with formal executable models. In RWL term rewriting is used to represent both structure (equational properties and functions) and transformation / behavior. Logics and inference systems can be naturally represented in RWL, as can the structure and behavior of distributed systems both engineered and natural.
Maude is a high performance realization of Rewriting Logic. Maude specifications are naturally executable and the Maude environment provides a variety analysis tools to reason about properties of models. These include reachability analysis, symbolic execution (narrowing), and model-checking. In addition, Maude is reflective. This provides a powerful mechanism for extension.
The talk will present a sampling of executable specifications using Maude and its extensions.
Cite as
Carolyn Talcott. Executable Formal Models in Rewriting Logic (Invited Talk). In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, p. 22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{talcott:LIPIcs.RTA.2015.22,
author = {Talcott, Carolyn},
title = {{Executable Formal Models in Rewriting Logic}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {22--22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.22},
URN = {urn:nbn:de:0030-drops-51861},
doi = {10.4230/LIPIcs.RTA.2015.22},
annote = {Keywords: Executable model, formal analysis, rewriting logic}
}
Document
Certification of Complexity Proofs using CeTA
Abstract
Nowadays certification is widely employed by automated termination tools for term rewriting, where certifiers support most available techniques. In complexity analysis, the situation is quite different. Although tools support certification in principle, current certifiers implement only the most basic technique,
namely, suitably tamed versions of reduction orders. As a consequence, only a small fraction of the proofs generated by state-of-the-art complexity tools can be certified. To improve upon this situation, we formalized a framework for the certification
of modular complexity proofs and incorporated it into CeTA. We
report on this extension and present the newly supported techniques
(match-bounds, weak dependency pairs, dependency tuples, usable rules, and usable replacement maps), resulting in a significant increase in the number of certifiable complexity proofs. During our work we detected conflicts in theoretical results as well as bugs in
existing complexity tools.
Cite as
Martin Avanzini, Christian Sternagel, and René Thiemann. Certification of Complexity Proofs using CeTA. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 23-39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{avanzini_et_al:LIPIcs.RTA.2015.23,
author = {Avanzini, Martin and Sternagel, Christian and Thiemann, Ren\'{e}},
title = {{Certification of Complexity Proofs using CeTA}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {23--39},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.23},
URN = {urn:nbn:de:0030-drops-51875},
doi = {10.4230/LIPIcs.RTA.2015.23},
annote = {Keywords: complexity analysis, certification, match-bounds, weak dependency pairs, dependency tuples, usable rules, usable replacement maps}
}
Document
Dismatching and Local Disunification in EL
Abstract
Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic EL to disunification since negative constraints on unifiers can be used to avoid unwanted unifiers. While decidability of the solvability of general EL-disunification problems remains an open problem, we obtain NP-completeness results for two interesting special cases: dismatching problems, where one side of each negative constraint
must be ground, and local solvability of disunification problems, where we restrict the attention to solutions that are built from so-called atoms occurring in the input problem. More precisely, we first show that dismatching can be reduced to local disunification, and then provide two complementary NP-algorithms for finding local solutions of (general) disunification problems.
Cite as
Franz Baader, Stefan Borgwardt, and Barbara Morawska. Dismatching and Local Disunification in EL. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 40-56, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{baader_et_al:LIPIcs.RTA.2015.40,
author = {Baader, Franz and Borgwardt, Stefan and Morawska, Barbara},
title = {{Dismatching and Local Disunification in EL}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {40--56},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.40},
URN = {urn:nbn:de:0030-drops-51884},
doi = {10.4230/LIPIcs.RTA.2015.40},
annote = {Keywords: Unification, Description Logics, SAT}
}
Document
Nominal Anti-Unification
Abstract
We study nominal anti-unification, which is concerned with computing
least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and alpha-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems where generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.
Cite as
Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal Anti-Unification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 57-73, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{baumgartner_et_al:LIPIcs.RTA.2015.57,
author = {Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
title = {{Nominal Anti-Unification}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {57--73},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.57},
URN = {urn:nbn:de:0030-drops-51895},
doi = {10.4230/LIPIcs.RTA.2015.57},
annote = {Keywords: Nominal Anti-Unification, Term-in-context, Equivariance}
}
Document
A faithful encoding of programmable strategies into term rewriting systems
Abstract
Rewriting is a formalism widely used in computer science and
mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and declarative rewriting strategies are used to control their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific strategies have been studied. We propose in this paper a generic encoding of classic control and traversal strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain term rewriting system. The encoding is proven sound and complete and, as a direct consequence, established termination methods used for term rewriting systems can be applied to analyze the termination of strategy controlled term rewriting systems. The corresponding implementation in Tom generates term rewriting systems compatible with the syntax of termination tools such as AAProVE and TTT2, tools which turned out to be very effective in (dis)proving the termination of the generated term rewriting systems. The approach can also be seen as a generic strategy compiler which can be integrated into languages providing pattern matching primitives; this has been experimented for
Tom and performances comparable to the native Tom strategies have been observed.
Cite as
Horatiu Cirstea, Serguei Lenglet, and Pierre-Etienne Moreau. A faithful encoding of programmable strategies into term rewriting systems. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 74-88, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{cirstea_et_al:LIPIcs.RTA.2015.74,
author = {Cirstea, Horatiu and Lenglet, Serguei and Moreau, Pierre-Etienne},
title = {{A faithful encoding of programmable strategies into term rewriting systems}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {74--88},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.74},
URN = {urn:nbn:de:0030-drops-51908},
doi = {10.4230/LIPIcs.RTA.2015.74},
annote = {Keywords: Programmable strategies, termination, term rewriting systems}
}
Document
Presenting a Category Modulo a Rewriting System
Abstract
Presentations of categories are a well-known algebraic tool to provide descriptions of categories by the means of generators, for objects and morphisms, and relations on morphisms. We generalize here this notion, in order to consider situations where the objects are considered modulo an equivalence relation (in the spirit of rewriting modulo), which is described by equational generators. When those form a convergent (abstract) rewriting system on objects, there are three very natural constructions that can be used to define the category which is described by the presentation: one is based on restricting to objects which are normal forms, one consists in turning equational generators into identities (i.e. considering a quotient category), and one consists in formally adding inverses to equational generators (i.e. localizing the category). We show that, under suitable coherence conditions on the presentation, the three constructions coincide, thus generalizing celebrated results on presentations of groups. We illustrate our techniques on a non-trivial example, and hint at a generalization for 2-categories.
Cite as
Florence Clerc and Samuel Mimram. Presenting a Category Modulo a Rewriting System. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 89-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{clerc_et_al:LIPIcs.RTA.2015.89,
author = {Clerc, Florence and Mimram, Samuel},
title = {{Presenting a Category Modulo a Rewriting System}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {89--105},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.89},
URN = {urn:nbn:de:0030-drops-51916},
doi = {10.4230/LIPIcs.RTA.2015.89},
annote = {Keywords: presentation of a category, quotient category, localization, residuation}
}
Document
Confluence of nearly orthogonal infinitary term rewriting systems
Abstract
We give a relatively simple coinductive proof of confluence, modulo
equivalence of root-active terms, of nearly orthogonal infinitary
term rewriting systems. Nearly orthogonal systems allow certain root
overlaps, but no non-root overlaps. Using a slightly more complicated method we also show confluence modulo equivalence of
hypercollapsing terms. The condition we impose on root overlaps is
similar to the condition used by Toyama in the context of finitary
rewriting.
Cite as
Lukasz Czajka. Confluence of nearly orthogonal infinitary term rewriting systems. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 106-126, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{czajka:LIPIcs.RTA.2015.106,
author = {Czajka, Lukasz},
title = {{Confluence of nearly orthogonal infinitary term rewriting systems}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {106--126},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.106},
URN = {urn:nbn:de:0030-drops-51929},
doi = {10.4230/LIPIcs.RTA.2015.106},
annote = {Keywords: infinitary rewriting, confluence, coinduction}
}
Document
No complete linear term rewriting system for propositional logic
Abstract
Recently it has been observed that the set of all sound linear inference rules in propositional logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-) linear rewrite rule. This raises the question of whether there is a rewriting system on linear terms of propositional logic that is sound and complete for the set of all such rewrite rules. We show in this paper that, as long as reduction steps are polynomial-time decidable, such a rewriting system does not exist unless coNP=NP.
We draw tools and concepts from term rewriting, Boolean function theory and graph theory in order to access the required intermediate results. At the same time we make several connections between these areas that, to our knowledge, have not yet been presented and constitute a rich theoretical framework for reasoning about linear TRSs for propositional logic.
Cite as
Anupam Das and Lutz Straßburger. No complete linear term rewriting system for propositional logic. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 127-142, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.RTA.2015.127,
author = {Das, Anupam and Stra{\ss}burger, Lutz},
title = {{No complete linear term rewriting system for propositional logic}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {127--142},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.127},
URN = {urn:nbn:de:0030-drops-51935},
doi = {10.4230/LIPIcs.RTA.2015.127},
annote = {Keywords: Linear rules, Term rewriting, Propositional logic, Proof theory, Deep inference}
}
Document
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning
Abstract
We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.
Cite as
Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 143-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{endrullis_et_al:LIPIcs.RTA.2015.143,
author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra},
title = {{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {143--159},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.143},
URN = {urn:nbn:de:0030-drops-51949},
doi = {10.4230/LIPIcs.RTA.2015.143},
annote = {Keywords: infinitary rewriting, coinduction}
}
Document
Proving non-termination by finite automata
Abstract
A new technique is presented to prove non-termination of term rewriting. The basic idea is to find a non-empty regular language of terms that is closed under rewriting and does not contain normal forms. It is automated by representing the language by a tree automaton with a fixed number of states, and expressing the mentioned requirements in a SAT formula. Satisfiability of this formula implies non-termination. Our approach succeeds for many examples where all earlier techniques fail, for instance for the S-rule from combinatory logic.
Cite as
Jörg Endrullis and Hans Zantema. Proving non-termination by finite automata. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 160-176, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{endrullis_et_al:LIPIcs.RTA.2015.160,
author = {Endrullis, J\"{o}rg and Zantema, Hans},
title = {{Proving non-termination by finite automata}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {160--176},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.160},
URN = {urn:nbn:de:0030-drops-51952},
doi = {10.4230/LIPIcs.RTA.2015.160},
annote = {Keywords: non-termination, finite automata, regular languages}
}
Document
Reachability Analysis of Innermost Rewriting
Abstract
We consider the problem of inferring a grammar describing the output of a functional program given a grammar describing its input. Solutions to this problem are helpful for detecting bugs or proving safety properties of functional programs and, several rewriting tools exist for solving this problem. However, known grammar inference techniques are not able to take evaluation strategies of the program into account. This yields very imprecise results when the evaluation strategy matters. In this work, we adapt the Tree Automata Completion algorithm to approximate accurately the set of
terms reachable by rewriting under the innermost strategy. We prove that the proposed technique is sound and precise w.r.t. innermost rewriting. The proposed algorithm has been implemented in the Timbuk reachability tool. Experiments show that it noticeably improves the accuracy of static analysis for functional programs using the call-by-value evaluation strategy.
Cite as
Thomas Genet and Yann Salmon. Reachability Analysis of Innermost Rewriting. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 177-193, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{genet_et_al:LIPIcs.RTA.2015.177,
author = {Genet, Thomas and Salmon, Yann},
title = {{Reachability Analysis of Innermost Rewriting}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {177--193},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.177},
URN = {urn:nbn:de:0030-drops-51968},
doi = {10.4230/LIPIcs.RTA.2015.177},
annote = {Keywords: term rewriting systems, strategy, innermost strategy, tree automata, functiona l program, static analysis}
}
Document
Network Rewriting II: Bi- and Hopf Algebras
Abstract
Bialgebras and their specialisation Hopf algebras are algebraic
structures that challenge traditional mathematical notation, in that they sport two core operations that defy the basic functional
paradigm of taking zero or more operands as input and producing one
result as output. On the other hand, these peculiarities do not
prevent studying them using rewriting techniques, if one works within an appropriate network formalism rather than the traditional term formalism. This paper restates the traditional axioms as rewriting systems, demonstrating confluence in the case of bialgebras and finding the (infinite) completion in the case of Hopf algebras. A noteworthy minor problem solved along the way is that of constructing a quasi-order with respect to which the rules are compatible.
Cite as
Lars Hellström. Network Rewriting II: Bi- and Hopf Algebras. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 194-208, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hellstrom:LIPIcs.RTA.2015.194,
author = {Hellstr\"{o}m, Lars},
title = {{Network Rewriting II: Bi- and Hopf Algebras}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {194--208},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.194},
URN = {urn:nbn:de:0030-drops-51975},
doi = {10.4230/LIPIcs.RTA.2015.194},
annote = {Keywords: confluence, network, PROP, Hopf algebra}
}
Document
Leftmost Outermost Revisited
Abstract
We present an elementary proof of the classical result that the
leftmost outermost strategy is normalizing for left-normal orthogonal rewrite systems. Our proof is local and extends to hyper-normalization and weakly orthogonal systems. Based on the new proof, we study basic normalization, i.e., we study normalization if the set of considered starting terms is restricted to basic terms. This allows us to weaken the left-normality restriction. We show that the leftmost outermost strategy is hyper-normalizing for basically left-normal orthogonal rewrite systems. This shift of focus greatly extends the applicability of the classical result, as evidenced by the experimental data provided.
Cite as
Nao Hirokawa, Aart Middeldorp, and Georg Moser. Leftmost Outermost Revisited. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 209-222, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hirokawa_et_al:LIPIcs.RTA.2015.209,
author = {Hirokawa, Nao and Middeldorp, Aart and Moser, Georg},
title = {{Leftmost Outermost Revisited}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {209--222},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.209},
URN = {urn:nbn:de:0030-drops-51986},
doi = {10.4230/LIPIcs.RTA.2015.209},
annote = {Keywords: term rewriting, strategies, normalization}
}
Document
Conditional Complexity
Abstract
We propose a notion of complexity for oriented conditional term rewrite systems. This notion is realistic in the sense that it measures not only successful computations but also partial computations that result in a failed rule application. A transformation to unconditional context-sensitive rewrite systems is
presented which reflects this complexity notion, as well as a technique to derive runtime and derivational complexity bounds for the latter.
Cite as
Cynthia Kop, Aart Middeldorp, and Thomas Sternagel. Conditional Complexity. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 223-240, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kop_et_al:LIPIcs.RTA.2015.223,
author = {Kop, Cynthia and Middeldorp, Aart and Sternagel, Thomas},
title = {{Conditional Complexity}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {223--240},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.223},
URN = {urn:nbn:de:0030-drops-51999},
doi = {10.4230/LIPIcs.RTA.2015.223},
annote = {Keywords: conditional term rewriting, complexity}
}
Document
Constructing Orthogonal Designs in Powers of Two: Gröbner Bases Meet Equational Unification
Abstract
In the past few decades, design theory has grown to encompass a wide variety of research directions. It comes as no surprise that applications in coding theory and communications continue to arise,
and also that designs have found applications in new areas. Computer science has provided a new source of applications of designs, and simultaneously a field of new and challenging problems in design theory. In this paper, we revisit a construction for orthogonal designs using the multiplication tables of Cayley-Dickson algebras of dimension $2^n$. The desired orthogonal designs can be described by a system of equations with the aid of a Groebner basis computation. For orders greater than 16 the combinatorial explosion of the problem gives rise to equations that are unfeasible to be handled by traditional search algorithms. However, the structural properties of the designs make this problem possible to be tackled in terms of rewriting techniques, by equational unification. We establish connections between central concepts of design theory and equational unification where equivalence operations of designs point to the computation of a minimal complete set of unifiers. These connections make viable the computation of some types of orthogonal designs that have not been found before with the aforementioned algebraic modelling.
Cite as
Ilias Kotsireas, Temur Kutsia, and Dimitris E. Simos. Constructing Orthogonal Designs in Powers of Two: Gröbner Bases Meet Equational Unification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 241-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kotsireas_et_al:LIPIcs.RTA.2015.241,
author = {Kotsireas, Ilias and Kutsia, Temur and Simos, Dimitris E.},
title = {{Constructing Orthogonal Designs in Powers of Two: Gr\"{o}bner Bases Meet Equational Unification}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {241--256},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.241},
URN = {urn:nbn:de:0030-drops-52006},
doi = {10.4230/LIPIcs.RTA.2015.241},
annote = {Keywords: Orthogonal designs, unification theory, algorithms, Groebner bases}
}
Document
Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules
Abstract
We describe how to utilize redundant rewrite rules, i.e., rules that can be simulated by other rules, when (dis)proving confluence of term rewrite systems. We demonstrate how automatic confluence provers benefit from the addition as well as the removal of redundant rules. Due to their simplicity, our transformations were easy to formalize in a proof assistant and are thus amenable to certification. Experimental results show the surprising gain in power.
Cite as
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 257-268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{nagele_et_al:LIPIcs.RTA.2015.257,
author = {Nagele, Julian and Felgenhauer, Bertram and Middeldorp, Aart},
title = {{Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {257--268},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.257},
URN = {urn:nbn:de:0030-drops-52010},
doi = {10.4230/LIPIcs.RTA.2015.257},
annote = {Keywords: term rewriting, confluence, automation, transformation}
}
Document
Certified Rule Labeling
Abstract
The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams for the first time. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.
Cite as
Julian Nagele and Harald Zankl. Certified Rule Labeling. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 269-284, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{nagele_et_al:LIPIcs.RTA.2015.269,
author = {Nagele, Julian and Zankl, Harald},
title = {{Certified Rule Labeling}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {269--284},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.269},
URN = {urn:nbn:de:0030-drops-52024},
doi = {10.4230/LIPIcs.RTA.2015.269},
annote = {Keywords: term rewriting, confluence, decreasing diagrams, certification}
}
Document
Transforming Cycle Rewriting into String Rewriting
Abstract
We present new techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main technique is to transform cycle rewriting into string rewriting and then apply state of the art techniques to prove termination of the string rewrite system.
We present three such transformations, and prove for all of them that they are sound and complete. Apart from this transformational approach, we extend the use of matrix interpretations as was studied before. We present several experiments showing that often our new techniques succeed where earlier techniques fail.
Cite as
David Sabel and Hans Zantema. Transforming Cycle Rewriting into String Rewriting. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 285-300, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{sabel_et_al:LIPIcs.RTA.2015.285,
author = {Sabel, David and Zantema, Hans},
title = {{Transforming Cycle Rewriting into String Rewriting}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {285--300},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.285},
URN = {urn:nbn:de:0030-drops-52032},
doi = {10.4230/LIPIcs.RTA.2015.285},
annote = {Keywords: rewriting systems, string rewriting, termination}
}
Document
Confluence of Orthogonal Nominal Rewriting Systems Revisited
Abstract
Nominal rewriting systems (Fernandez, Gabbay, Mackie, 2004;
Fernandez, Gabbay, 2007) have been introduced as a new framework
of higher-order rewriting systems based on the nominal approach
(Gabbay, Pitts, 2002; Pitts, 2003), which deals with variable
binding via permutations and freshness conditions on atoms.
Confluence of orthogonal nominal rewriting systems has been shown in
(Fernandez, Gabbay, 2007). However, their definition of
(non-trivial) critical pairs has a serious weakness so that the
orthogonality does not actually hold for most of standard nominal
rewriting systems in the presence of binders. To overcome this
weakness, we divide the notion of overlaps into the self-rooted and
proper ones, and introduce a notion of alpha-stability which
guarantees alpha-equivalence of peaks from the self-rooted
overlaps. Moreover, we give a sufficient criterion for uniformity and alpha-stability. The new definition of orthogonality and the
criterion offer a novel confluence condition effectively applicable to many standard nominal rewriting systems. We also report on an
implementation of a confluence prover for orthogonal nominal rewriting systems based on our framework.
Cite as
Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama. Confluence of Orthogonal Nominal Rewriting Systems Revisited. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 301-317, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{suzuki_et_al:LIPIcs.RTA.2015.301,
author = {Suzuki, Takaki and Kikuchi, Kentaro and Aoto, Takahito and Toyama, Yoshihito},
title = {{Confluence of Orthogonal Nominal Rewriting Systems Revisited}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {301--317},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.301},
URN = {urn:nbn:de:0030-drops-52042},
doi = {10.4230/LIPIcs.RTA.2015.301},
annote = {Keywords: Nominal rewriting, Confluence, Orthogonality, Higher-order rewriting, alpha-equivalence}
}
Document
Matrix Interpretations on Polyhedral Domains
Abstract
We refine matrix interpretations for proving termination and complexity bounds of term rewrite systems we restricting them to domains that satisfy a system of linear inequalities. Admissibility of such a restriction is shown by certificates whose validity can be expressed as a constraint program. This refinement is orthogonal to other features of matrix interpretations (complexity bounds, dependency pairs), but can be used to improve complexity bounds, and we discuss its relation with the usable rules criterion. We present an implementation and experiments.
Cite as
Johannes Waldmann. Matrix Interpretations on Polyhedral Domains. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 318-333, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{waldmann:LIPIcs.RTA.2015.318,
author = {Waldmann, Johannes},
title = {{Matrix Interpretations on Polyhedral Domains}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {318--333},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.318},
URN = {urn:nbn:de:0030-drops-52059},
doi = {10.4230/LIPIcs.RTA.2015.318},
annote = {Keywords: termination of term rewriting, matrix interpretations, constraint programming, linear inequalities}
}
Document
Inferring Lower Bounds for Runtime Complexity
Abstract
We present the first approach to deduce lower bounds for innermost runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing techniques that compute upper complexity
bounds. The key idea of our approach is to generate suitable families of rewrite sequences of a TRS and to find a relation between the length of such a rewrite sequence and the size of the first term in the sequence. We implemented our approach in
the tool AProVE and evaluated it by extensive experiments.
Cite as
Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, and Thomas Ströder. Inferring Lower Bounds for Runtime Complexity. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 334-349, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{frohn_et_al:LIPIcs.RTA.2015.334,
author = {Frohn, Florian and Giesl, J\"{u}rgen and Hensel, Jera and Aschermann, Cornelius and Str\"{o}der, Thomas},
title = {{Inferring Lower Bounds for Runtime Complexity}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {334--349},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.334},
URN = {urn:nbn:de:0030-drops-52068},
doi = {10.4230/LIPIcs.RTA.2015.334},
annote = {Keywords: Term Rewriting, Runtime Complexity, Lower Bounds, Induction}
}
Document
A Simple and Efficient Step Towards Type-Correct XSLT Transformations
Abstract
XSLT 1.0 is a standardized functional programming language and widely used for defining transformations on XML models and documents, in many areas of industry and publishing. The problem of XSLT type checking is to verify that a given transformation, when applied to an input which conforms to a given structure definition, e.g. an XML DTD, will always produce an output which adheres to a second structure definition. This problem is known to be undecidable for the full range of XSLT and document structure definition languages. Either one or both of them must be significantly restricted, or only approximations can be calculated.
The algorithm presented here takes a different approach towards type
correct XSLT transformations. It does not consider the type of the input document at all. Instead it parses the fragments of the result document contained verbatim in the transformation code and verifies that these can potentially appear in the result language, as defined by a given DTD. This is a kind of abstract interpretation, which can be executed on the fly and in linear time when parsing the XSLT program. Generated error messages are located accurately to a child subsequence of a single result element node.
Apparently the method eliminates a considerable share of XSLT programming errors, on the same order of magnitude as a full fledged global control-flow analysis.
Cite as
Markus Lepper and Baltasar Trancón y Widemann. A Simple and Efficient Step Towards Type-Correct XSLT Transformations. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 350-364, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{lepper_et_al:LIPIcs.RTA.2015.350,
author = {Lepper, Markus and Tranc\'{o}n y Widemann, Baltasar},
title = {{A Simple and Efficient Step Towards Type-Correct XSLT Transformations}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {350--364},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.350},
URN = {urn:nbn:de:0030-drops-52078},
doi = {10.4230/LIPIcs.RTA.2015.350},
annote = {Keywords: XSLT, type checking, abstract interpretation}
}
Document
DynSem: A DSL for Dynamic Semantics Specification
Abstract
The formal semantics of a programming language and its implementation are typically separately defined, with the risk of
divergence such that properties of the formal semantics are not properties of the implementation. In this paper, we present DynSem, a domain-specific language for the specification of the dynamic semantics of programming languages that aims at supporting both formal reasoning and efficient interpretation. DynSem supports the specification of the operational semantics of a language by means of statically typed conditional term reduction rules. DynSem supports concise specification of reduction rules by providing implicit build and match coercions based on reduction arrows and implicit term constructors. DynSem supports modular specification by adopting implicit propagation of semantic components from I-MSOS, which allows omitting propagation of components such as environments and stores from rules that do not affect those. DynSem supports the declaration of native operators for delegation of aspects of the semantics to an external definition or implementation. DynSem supports the definition of auxiliary meta-functions, which can be
expressed using regular reduction rules and are subject to semantic component propagation. DynSem specifications are executable through automatic generation of a Java-based AST interpreter.
Cite as
Vlad Vergu, Pierre Neron, and Eelco Visser. DynSem: A DSL for Dynamic Semantics Specification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 365-378, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{vergu_et_al:LIPIcs.RTA.2015.365,
author = {Vergu, Vlad and Neron, Pierre and Visser, Eelco},
title = {{DynSem: A DSL for Dynamic Semantics Specification}},
booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages = {365--378},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-85-9},
ISSN = {1868-8969},
year = {2015},
volume = {36},
editor = {Fern\'{a}ndez, Maribel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.365},
URN = {urn:nbn:de:0030-drops-52080},
doi = {10.4230/LIPIcs.RTA.2015.365},
annote = {Keywords: programming languages, dynamic semantics, reduction semantics, semantics engineering, IDE, interpreters, modularity}
}