23rd International Conference on Rewriting Techniques and Applications (RTA'12)

Document

Complete Volume

DOI: 10.4230/LIPIcs.RTA.2012

LIPIcs, Volume 15, RTA'12, Complete Volume

Authors: Ashish Tiwari

Abstract

LIPIcs, Volume 15, RTA'12, Complete Volume

Cite as

23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{tiwari:LIPIcs.RTA.2012,
  title =	{{LIPIcs, Volume 15, RTA'12, Complete Volume}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012},
  URN =		{urn:nbn:de:0030-drops-41090},
  doi =		{10.4230/LIPIcs.RTA.2012},
  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

DOI: 10.4230/LIPIcs.RTA.2012.i

RTA 2012 Proceedings Frontmatter

Authors: Ashish Tiwari

Abstract

Frontmatter, Table of Contents, Conference Organization, External Reviewers, Author Index.

Cite as

23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. i-xiii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{tiwari:LIPIcs.RTA.2012.i,
  author =	{Tiwari, Ashish},
  title =	{{RTA 2012 Proceedings Frontmatter}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{i--xiii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.i},
  URN =		{urn:nbn:de:0030-drops-35033},
  doi =		{10.4230/LIPIcs.RTA.2012.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Conference Organization, External Reviewers, Author Index, RTA 2012, proceedings}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.RTA.2012.1

Computational Real Algebraic Geometry in Practice (Invited Talk)

Authors: Hirokazu Anai

Abstract

Real algebraic geometry deals with the solution set of (possibly quantified) systems of polynomial equations and/or inequalities over the real numbers, which arise frequently in science and engineering. Main concern in real algebraic geometry is to determine the properties of the solution sets such as non-emptiness, dimension and quantifier free description as a semi-algebraic set. Such tasks are carried out by symbolic and algebraic algorithms:cylindrical algebraic decomposition (CAD) or quantifier elimination (QE). Various algorithms and deep complexity results about CAD and QE have been studied during the last several decades. Moreover, practically efficient software systems of QE have been developed and also are applied to many nontrivial application problems. In this talk we explain several algorithms of CAD and QE together with their engineering applications.

Cite as

Hirokazu Anai. Computational Real Algebraic Geometry in Practice (Invited Talk). In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{anai:LIPIcs.RTA.2012.1,
  author =	{Anai, Hirokazu},
  title =	{{Computational Real Algebraic Geometry in Practice}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{1--1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.1},
  URN =		{urn:nbn:de:0030-drops-34784},
  doi =		{10.4230/LIPIcs.RTA.2012.1},
  annote =	{Keywords: real algebraic geometry, quantifier elimination, cylindrical algebraic decomposition, symbolic optimization}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.RTA.2012.2

Rho-Calculi for Computation and Logic (Invited Talk)

Authors: Claude Kirchner

Abstract

The rho-calculi provide enlightening concepts for both computing and reasoning as well as their combination. They consist in the generalization of lambda-calculus to structures like terms, propositions or graphs and we will show how their interrelations with deduction provide powerful frameworks for the next generation of proof assistants.

Cite as

Claude Kirchner. Rho-Calculi for Computation and Logic (Invited Talk). In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 2-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kirchner:LIPIcs.RTA.2012.2,
  author =	{Kirchner, Claude},
  title =	{{Rho-Calculi for Computation and Logic}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{2--4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.2},
  URN =		{urn:nbn:de:0030-drops-34796},
  doi =		{10.4230/LIPIcs.RTA.2012.2},
  annote =	{Keywords: rewriting calculus, rho-calculus, deduction modulo}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.RTA.2012.5

Dictionary-Based Tree Compression (Invited Talk)

Authors: Sebastian Maneth

Abstract

Trees are a ubiquitous data structure in computer science. LISP, for instance, was designed to manipulate nested lists, that is, ordered unranked trees. Already at that time, DAGs were used to detect common subexpression, a process known as "hash consing." In a DAG every distinct subtree is represented only once (but can be referenced many times) and hence it constitutes a dictionary-based compression method for ordered trees. In our compression scenario we distinguish two kinds of ordered trees: binary and unranked. The latter appear naturally as representation of XML document structures. We survey these dictionary-based compression methods for ordered trees: (1) DAGs, (2) hybrid DAGs, (3) straight-line context-free tree grammars ("SLT grammars"). We compare the minimal DAG of an unranked tree with the minimal DAG of its binary tree encoding. The latter is obtained by identifying first children of the unranked tree with left children of the binary tree, and next-siblings with the right children. For XML document trees, unranked DAGs are usually smaller than encoded binary DAGs. We show that this holds for arbitrary unranked trees, on average. We also present the "hybrid DAG"; its size lower-bounds those of the binary and unranked DAGs. Finding a smallest SLT grammar for a given tree is NP-complete. We discuss two linear-time approximation algorithms: BPLEX and TreeRePair. For typical XML document trees, TreeRePair produces SLT grammars that are only one fourth of the size of the minimal DAG, and which contain approximately 3$% of the edges of the original tree. As far as we know, this gives rise to the smallest existing pointer-based tree representation. We show that some basic algorithms can be computed directly on the compressed trees, without prior decompression. Examples include the execution of different kinds of tree automata, and the real-time traversal of the original tree. It is even possible to evaluate simple XPath queries directly on the SLT grammars, using deterministic node-selecting tree automata. In this way, impressive speed-ups are achieved over existing XPath evaluators, while at the same time the memory requirement is slashed to only a few percent. For more complex XPath queries that require nondeterministic node-selecting tree automata, efficient evaluation over SLT grammars remains a difficult challenge.

Cite as

Sebastian Maneth. Dictionary-Based Tree Compression (Invited Talk). In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, p. 5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{maneth:LIPIcs.RTA.2012.5,
  author =	{Maneth, Sebastian},
  title =	{{Dictionary-Based Tree Compression}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{5--5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.5},
  URN =		{urn:nbn:de:0030-drops-34802},
  doi =		{10.4230/LIPIcs.RTA.2012.5},
  annote =	{Keywords: Tree grammars, tree automata, straight-line programs}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.6

An Abstract Factorization Theorem for Explicit Substitutions

Authors: Beniamino Accattoli

Abstract

We study a simple form of standardization, here called factorization, for explicit substitutions calculi, i.e. lambda-calculi where beta-reduction is decomposed in various rules. These calculi, despite being non-terminating and non-orthogonal, have a key feature: each rule terminates when considered separately. It is well-known that the study of rewriting properties simplifies in presence of termination (e.g. confluence reduces to local confluence). This remark is exploited to develop an abstract theorem deducing factorization from some axioms on local diagrams. The axioms are simple and easy to check, in particular they do not mention residuals. The abstract theorem is then applied to some explicit substitution calculi related to Proof-Nets. We show how to recover standardization by levels, we model both call-by-name and call-by-value calculi and we characterize linear head reduction via a factorization theorem for a linear calculus of substitutions.

Cite as

Beniamino Accattoli. An Abstract Factorization Theorem for Explicit Substitutions. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 6-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{accattoli:LIPIcs.RTA.2012.6,
  author =	{Accattoli, Beniamino},
  title =	{{An Abstract Factorization Theorem for Explicit Substitutions}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{6--21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.6},
  URN =		{urn:nbn:de:0030-drops-34813},
  doi =		{10.4230/LIPIcs.RTA.2012.6},
  annote =	{Keywords: lambda-calculus, Standardization, Explicit Substitutions, Abstract rewriting, Diagrammatic reasoning}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.22

On the Invariance of the Unitary Cost Model for Head Reduction

Authors: Beniamino Accattoli and Ugo Dal Lago

Abstract

The lambda-calculus is a widely accepted computational model of higher-order functional programs, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational difficulty of reducing lambda-terms to their normal form is typically studied by reasoning on concrete implementation algorithms. In this paper, we show that when head reduction is the underlying dynamics, the unitary cost model is indeed invariant. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the lambda-calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies the unitary cost model is invariant, if any.

Cite as

Beniamino Accattoli and Ugo Dal Lago. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 22-37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.RTA.2012.22,
  author =	{Accattoli, Beniamino and Dal Lago, Ugo},
  title =	{{On the Invariance of the Unitary Cost Model for Head Reduction}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{22--37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.22},
  URN =		{urn:nbn:de:0030-drops-34820},
  doi =		{10.4230/LIPIcs.RTA.2012.22},
  annote =	{Keywords: lambda calculus, cost models, explicit substitutions, implicit computational complexity}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.38

A Term Rewriting System for Kuratowski's Closure-Complement Problem

Authors: Osama Al-Hassani, Quratul-ain Mahesar, Claudio Sacerdoti Coen, and Volker Sorge

Abstract

We present a term rewriting system to solve a class of open problems that are generalisations of Kuratowski's closure-complement theorem. The problems are concerned with finding the number of distinct sets that can be obtained by applying combinations of axiomatically defined set operators. While the original problem considers only closure and complement of a topological space as operators, it can be generalised by adding operators and varying axiomatisation. We model these axioms as rewrite rules and construct a rewriting system that allows us to close some so far open variants of Kuratowski's problem by analysing several million inference steps on a typical personal computer.

Cite as

Osama Al-Hassani, Quratul-ain Mahesar, Claudio Sacerdoti Coen, and Volker Sorge. A Term Rewriting System for Kuratowski's Closure-Complement Problem. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 38-52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{alhassani_et_al:LIPIcs.RTA.2012.38,
  author =	{Al-Hassani, Osama and Mahesar, Quratul-ain and Sacerdoti Coen, Claudio and Sorge, Volker},
  title =	{{A Term Rewriting System for Kuratowski's Closure-Complement Problem}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{38--52},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.38},
  URN =		{urn:nbn:de:0030-drops-34838},
  doi =		{10.4230/LIPIcs.RTA.2012.38},
  annote =	{Keywords: Kuratowski's closure-complement problem, Rewriting system}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.53

Term Rewriting Systems as Topological Dynamical Systems

Authors: Soren Bjerg Andersen and Jakob Grue Simonsen

Abstract

Topological dynamics is, roughly, the study of phenomena related to iterations of continuous maps from a metric space to itself. We show how the rewrite relation in term rewriting gives rise to dynamical systems in two distinct, natural ways: (A) One in which any deterministic rewriting strategy induces a dynamical system on the set of finite and infinite terms endowed with the usual metric, and (B) one in which the unconstrained rewriting relation induces a dynamical system on sets of sets of terms, specifically the set of compact subsets of the set of finite and infinite terms endowed with the Hausdorff metric. For both approaches, we give sufficient criteria for the induced systems to be well-defined dynamical systems and for (A) we demonstrate how the classic topological invariant called topological entropy turns out to be much less useful in the setting of term rewriting systems than in symbolic dynamics.

Cite as

Soren Bjerg Andersen and Jakob Grue Simonsen. Term Rewriting Systems as Topological Dynamical Systems. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 53-68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{andersen_et_al:LIPIcs.RTA.2012.53,
  author =	{Andersen, Soren Bjerg and Simonsen, Jakob Grue},
  title =	{{Term Rewriting Systems as Topological Dynamical Systems}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{53--68},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.53},
  URN =		{urn:nbn:de:0030-drops-34841},
  doi =		{10.4230/LIPIcs.RTA.2012.53},
  annote =	{Keywords: Term rewriting, dynamical systems, topology, symbolic dynamics}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.69

Infinitary Term Graph Rewriting is Simple, Sound and Complete

Authors: Patrick Bahr

Abstract

Based on a simple metric and a simple partial order on term graphs, we develop two infinitary calculi of term graph rewriting. We show that, similarly to infinitary term rewriting, the partial order formalisation yields a conservative extension of the metric formalisation of the calculus. By showing that the resulting calculi simulate the corresponding well-established infinitary calculi of term rewriting in a sound and complete manner, we argue for the appropriateness of our approach to capture the notion of infinitary term graph rewriting.

Cite as

Patrick Bahr. Infinitary Term Graph Rewriting is Simple, Sound and Complete. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 69-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.RTA.2012.69,
  author =	{Bahr, Patrick},
  title =	{{Infinitary Term Graph Rewriting is Simple, Sound and Complete}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{69--84},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.69},
  URN =		{urn:nbn:de:0030-drops-34857},
  doi =		{10.4230/LIPIcs.RTA.2012.69},
  annote =	{Keywords: term graphs, infinitary rewriting}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.85

Axiomatic Sharing-via-Labelling

Authors: Thibaut Balabonski

Abstract

A judicious use of labelled terms makes it possible to bring together the simplicity of term rewriting and the sharing power of graph rewriting: this has been known for twenty years in the particular case of orthogonal first-order systems. The present paper introduces a concise and easily usable axiomatic presentation of sharing-via-labelling techniques that applies to higher-order term rewriting as well as to non-orthogonal term rewriting. This provides a general framework for the sharing of subterms and keeps the formalism as simple as term rewriting.

Cite as

Thibaut Balabonski. Axiomatic Sharing-via-Labelling. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 85-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{balabonski:LIPIcs.RTA.2012.85,
  author =	{Balabonski, Thibaut},
  title =	{{Axiomatic Sharing-via-Labelling}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{85--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.85},
  URN =		{urn:nbn:de:0030-drops-34868},
  doi =		{10.4230/LIPIcs.RTA.2012.85},
  annote =	{Keywords: Sharing, Abstract term rewriting, Graphs, Higher order, Non-orthogonality}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.101

On the Decidability Status of Reachability and Coverability in Graph Transformation Systems

Authors: Nathalie Bertrand, Giorgio Delzanno, Barbara König, Arnaud Sangnier, and Jan Stückrath

Abstract

We study decidability issues for reachability problems in graph transformation systems, a powerful infinite-state model. For a fixed initial configuration, we consider reachability of an entirely specified configuration and of a configuration that satisfies a given pattern (coverability). The former is a fundamental problem for any computational model, the latter is strictly related to verification of safety properties in which the pattern specifies an infinite set of bad configurations. In this paper we reformulate results obtained, e.g., for context-free graph grammars and concurrency models, such as Petri nets, in the more general setting of graph transformation systems and study new results for classes of models obtained by adding constraints on the form of reduction rules.

Cite as

Nathalie Bertrand, Giorgio Delzanno, Barbara König, Arnaud Sangnier, and Jan Stückrath. On the Decidability Status of Reachability and Coverability in Graph Transformation Systems. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 101-116, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.RTA.2012.101,
  author =	{Bertrand, Nathalie and Delzanno, Giorgio and K\"{o}nig, Barbara and Sangnier, Arnaud and St\"{u}ckrath, Jan},
  title =	{{On the Decidability Status of Reachability and Coverability in  Graph Transformation Systems}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{101--116},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.101},
  URN =		{urn:nbn:de:0030-drops-34871},
  doi =		{10.4230/LIPIcs.RTA.2012.101},
  annote =	{Keywords: decidability, reachability, graph transformation, coverability}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.117

Normalisation for Dynamic Pattern Calculi

Authors: Eduardo Bonelli, Delia Kesner, Carlos Lombardi, and Alejandro Rios

Abstract

The Pure Pattern Calculus (PPC) extends the lambda-calculus, as well as the family of algebraic pattern calculi, with first-class patterns; that is, patterns can be passed as arguments, evaluated and returned as results. The notion of matching failure of the PPC not only provides a mechanism to define functions by pattern matching on cases but also supplies PPC with parallel-or-like, non-sequential behaviour. Therefore, devising normalising strategies for PPC to obtain well-behaved implementations turns out to be challenging. This paper focuses on normalising reduction strategies for PPC. We define a (multistep) strategy and show that it is normalising. The strategy generalises the leftmost-outermost strategy for lambda-calculus and is strictly finer than parallel-outermost. The normalisation proof is based on the notion of necessary set of redexes, a generalisation of the notion of needed redex encompassing non-sequential reduction systems.

Cite as

Eduardo Bonelli, Delia Kesner, Carlos Lombardi, and Alejandro Rios. Normalisation for Dynamic Pattern Calculi. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 117-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bonelli_et_al:LIPIcs.RTA.2012.117,
  author =	{Bonelli, Eduardo and Kesner, Delia and Lombardi, Carlos and Rios, Alejandro},
  title =	{{Normalisation for Dynamic Pattern Calculi}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{117--132},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.117},
  URN =		{urn:nbn:de:0030-drops-34889},
  doi =		{10.4230/LIPIcs.RTA.2012.117},
  annote =	{Keywords: Pattern calculi, reduction strategies, sequentiality, neededness}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.133

A Semantic Proof that Reducibility Candidates entail Cut Elimination

Authors: Denis Cousineau and Olivier Hermant

Abstract

Two main lines have been adopted to prove the cut elimination theorem: the syntactic one, that studies the process of reducing cuts, and the semantic one, that consists in interpreting a sequent in some algebra and extracting from this interpretation a cut-free proof of this very sequent. A link between those two methods was exhibited by studying in a semantic way, syntactical tools that allow to prove (strong) normalization of proof-terms, namely reducibility candidates. In the case of deduction modulo, a framework combining deduction and rewriting rules in which theories like Zermelo set theory and higher order logic can be expressed, this is obtained by constructing a reducibility candidates valued model. The existence of such a pre-model for a theory entails strong normalization of its proof-terms and, by the usual syntactic argument, the cut elimination property. In this paper, we strengthen this gate between syntactic and semantic methods, by providing a full semantic proof that the existence of a pre-model entails the cut elimination property for the considered theory in deduction modulo. We first define a new simplified variant of reducibility candidates à la Girard, that is sufficient to prove weak normalization of proof-terms (and therefore the cut elimination property). Then we build, from some model valued on the pre-Heyting algebra of those WN reducibility candidates, a regular model valued on a Heyting algebra on which we apply the usual soundness/strong completeness argument. Finally, we discuss further extensions of this new method towards normalization by evaluation techniques that commonly use Kripke semantics.

Cite as

Denis Cousineau and Olivier Hermant. A Semantic Proof that Reducibility Candidates entail Cut Elimination. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 133-148, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{cousineau_et_al:LIPIcs.RTA.2012.133,
  author =	{Cousineau, Denis and Hermant, Olivier},
  title =	{{A Semantic Proof that Reducibility Candidates entail Cut Elimination}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{133--148},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.133},
  URN =		{urn:nbn:de:0030-drops-34899},
  doi =		{10.4230/LIPIcs.RTA.2012.133},
  annote =	{Keywords: cut elimination, reducibility candidates, (pre-)Heyting algebras}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.149

One-context Unification with STG-Compressed Terms is in NP

Authors: Carles Creus, Adria Gascon, and Guillem Godoy

Abstract

One-context unification is an extension of first-order term unification in which a variable of arity one standing for a context may occur in the input terms. This problem arises in areas like program analysis, term rewriting and XML processing and is known to be solvable in nondeterministic polynomial time. We prove that this problem can be solved in nondeterministic polynomial time also when the input is compressed using Singleton Tree Grammars (STG's). STG's are a grammar-based compression method for terms that generalizes the directed acyclic graph representation. They have been recently considered as an efficient in-memory representation for large terms, since several operations on terms can be performed efficiently on their STG representation without a prior decompression.

Cite as

Carles Creus, Adria Gascon, and Guillem Godoy. One-context Unification with STG-Compressed Terms is in NP. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 149-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{creus_et_al:LIPIcs.RTA.2012.149,
  author =	{Creus, Carles and Gascon, Adria and Godoy, Guillem},
  title =	{{One-context Unification with STG-Compressed Terms is in NP}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{149--164},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.149},
  URN =		{urn:nbn:de:0030-drops-34902},
  doi =		{10.4230/LIPIcs.RTA.2012.149},
  annote =	{Keywords: Term Unification, Compression, Grammars}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.165

Deciding Confluence of Ground Term Rewrite Systems in Cubic Time

Authors: Bertram Felgenhauer

Abstract

It is well known that the confluence property of ground term rewrite systems (ground TRSs) is decidable in polynomial time. For an efficient implementation, the degree of this polynomial is of great interest. The best complexity bound in the literature is given by Comon, Godoy and Nieuwenhuis (2001), who describe an O(n^5) algorithm, where n is the size of the ground TRS. In this paper we improve this bound to O(n^3). The algorithm has been implemented in the confluence tool CSI.

Cite as

Bertram Felgenhauer. Deciding Confluence of Ground Term Rewrite Systems in Cubic Time. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 165-175, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{felgenhauer:LIPIcs.RTA.2012.165,
  author =	{Felgenhauer, Bertram},
  title =	{{Deciding Confluence of Ground Term Rewrite Systems in Cubic Time}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{165--175},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.165},
  URN =		{urn:nbn:de:0030-drops-34918},
  doi =		{10.4230/LIPIcs.RTA.2012.165},
  annote =	{Keywords: confluence, ground rewrite systems, decidability, polynomial time}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.176

Polynomial Interpretations for Higher-Order Rewriting

Authors: Carsten Fuhs and Cynthia Kop

Abstract

The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed lambda-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool Wanda.

Cite as

Carsten Fuhs and Cynthia Kop. Polynomial Interpretations for Higher-Order Rewriting. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 176-192, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{fuhs_et_al:LIPIcs.RTA.2012.176,
  author =	{Fuhs, Carsten and Kop, Cynthia},
  title =	{{Polynomial Interpretations for Higher-Order Rewriting}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{176--192},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.176},
  URN =		{urn:nbn:de:0030-drops-34924},
  doi =		{10.4230/LIPIcs.RTA.2012.176},
  annote =	{Keywords: higher-order rewriting, termination, polynomial interpretations, weakly monotonic algebras, automation}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.193

On Soundness Conditions for Unraveling Deterministic Conditional Rewrite Systems

Authors: Karl Gmeiner, Bernhard Gramlich, and Felix Schernhammer

Abstract

We study (un)soundness of transformations of conditional term rewriting systems (CTRSs) into unconditional term rewriting systems (TRSs). The focus here is on analyzing (un)soundness of so-called unravelings, the most basic and natural class of such transformations. We extend our previous analysis from normal 1-CTRSs to the more general class of deterministic CTRSs (DCTRSs) where extra variables in right-hand sides of rules are allowed to a certain extent. We prove that the previous soundness results based on weak left-linearity and on right-linearity can be extended from normal 1-CTRSs to DCTRSs. Counterexamples show that such an extension to DCTRSs does not work for the previous criteria which were based on confluence and on non-erasingness, not even for right-stable systems. Yet, we prove weaker versions of soundness criteria based on confluence and on non-erasingness. Finally, we compare our approach and results with other recently established soundness criteria for unraveling DCTRSs.

Cite as

Karl Gmeiner, Bernhard Gramlich, and Felix Schernhammer. On Soundness Conditions for Unraveling Deterministic Conditional Rewrite Systems. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 193-208, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{gmeiner_et_al:LIPIcs.RTA.2012.193,
  author =	{Gmeiner, Karl and Gramlich, Bernhard and Schernhammer, Felix},
  title =	{{On Soundness Conditions for Unraveling Deterministic Conditional Rewrite Systems}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{193--208},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.193},
  URN =		{urn:nbn:de:0030-drops-34936},
  doi =		{10.4230/LIPIcs.RTA.2012.193},
  annote =	{Keywords: Conditional term rewriting system (CTRS), deterministic CTRS, transformation, simulation, soundness}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.209

Reinterpreting Compression in Infinitary Rewriting

Authors: Jeroen Ketema

Abstract

Departing from a computational interpretation of compression in infinitary rewriting, we view compression as a degenerate case of standardisation. The change in perspective comes about via two observations: (a) no compression property can be recovered for non-left-linear systems and (b) some standardisation procedures, as a "side-effect", yield compressed reductions.

Cite as

Jeroen Ketema. Reinterpreting Compression in Infinitary Rewriting. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 209-224, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{ketema:LIPIcs.RTA.2012.209,
  author =	{Ketema, Jeroen},
  title =	{{Reinterpreting Compression in Infinitary Rewriting}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{209--224},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.209},
  URN =		{urn:nbn:de:0030-drops-34948},
  doi =		{10.4230/LIPIcs.RTA.2012.209},
  annote =	{Keywords: term rewriting, infinitary rewriting, compression, standardisation}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.225

Finite Models vs Tree Automata in Safety Verification

Authors: Alexei Lisitsa

Abstract

In this paper we deal with verification of safety properties of term-rewriting systems. The verification problem is translated to a purely logical problem of finding a finite countermodel for a first-order formula, which is further resolved by a generic finite model finding procedure. A finite countermodel produced during successful verification provides with a concise description of the system invariant sufficient to demonstrate a specific safety property. We show the relative completeness of this approach with respect to the tree automata completion technique. On a set of examples taken from the literature we demonstrate the efficiency of finite model finding approach as well as its explanatory power.

Cite as

Alexei Lisitsa. Finite Models vs Tree Automata in Safety Verification. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 225-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{lisitsa:LIPIcs.RTA.2012.225,
  author =	{Lisitsa, Alexei},
  title =	{{Finite Models vs Tree Automata in Safety Verification}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{225--239},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.225},
  URN =		{urn:nbn:de:0030-drops-34959},
  doi =		{10.4230/LIPIcs.RTA.2012.225},
  annote =	{Keywords: term-rewriting systems, safety verification, first-order logic, finite model finding}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.240

Triangulation in Rewriting

Authors: Vincent van Oostrom and Hans Zantema

Abstract

We introduce a process, dubbed triangulation, turning any rewrite relation into a confluent one. It is more direct than usual completion, in the sense that objects connected by a peak are directly related rather than their normal forms. We investigate conditions under which this process preserves desirable properties such as termination.

Cite as

Vincent van Oostrom and Hans Zantema. Triangulation in Rewriting. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 240-255, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{vanoostrom_et_al:LIPIcs.RTA.2012.240,
  author =	{van Oostrom, Vincent and Zantema, Hans},
  title =	{{Triangulation in Rewriting}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{240--255},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.240},
  URN =		{urn:nbn:de:0030-drops-34964},
  doi =		{10.4230/LIPIcs.RTA.2012.240},
  annote =	{Keywords: triangulation,codeterminism,completion,(co)confluence,(co)termination}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.256

Turing-Completeness of Polymorphic Stream Equation Systems

Authors: Christian Sattler and Florent Balestrieri

Abstract

Polymorphic stream functions operate on the structure of streams, infinite sequences of elements, without inspection of the contained data, having to work on all streams over all signatures uniformly. A natural, yet restrictive class of polymorphic stream functions comprises those definable by a system of equations using only stream constructors and destructors and recursive calls. Using methods reminiscent of prior results in the field, we first show this class consists of exactly the computable polymorphic stream functions. Using much more intricate techniques, our main result states this holds true even for unary equations free of mutual recursion, yielding an elegant model of Turing-completeness in a severely restricted environment and allowing us to recover previous complexity results in a much more restricted setting.

Cite as

Christian Sattler and Florent Balestrieri. Turing-Completeness of Polymorphic Stream Equation Systems. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 256-271, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{sattler_et_al:LIPIcs.RTA.2012.256,
  author =	{Sattler, Christian and Balestrieri, Florent},
  title =	{{Turing-Completeness of Polymorphic Stream Equation Systems}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{256--271},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.256},
  URN =		{urn:nbn:de:0030-drops-34970},
  doi =		{10.4230/LIPIcs.RTA.2012.256},
  annote =	{Keywords: turing-completeness, polymorphic stream functions}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.272

Matching of Compressed Patterns with Character-Variables

Authors: Manfred Schmidt-Schauß

Abstract

We consider the problem of finding an instance of a string-pattern s in a given string under compression by straight line programs (SLP). The variables of the string pattern can be instantiated by single characters. This is a generalisation of the fully compressed pattern match, which is the task of finding a compressed string in another compressed string, which is known to have a polynomial time algorithm. We mainly investigate patterns s that are linear in the variables, i.e. variables occur at most once in s, also known as partial words. We show that fully compressed pattern matching with linear patterns can be performed in polynomial time. A polynomial-sized representation of all matches and all substitutions is also computed. Also, a related algorithm is given that computes all periods of a compressed linear pattern in polynomial time. A technical key result on the structure of partial words shows that an overlap of h+2 copies of a partial word w with at most h holes implies that w is strongly periodic.

Cite as

Manfred Schmidt-Schauß. Matching of Compressed Patterns with Character-Variables. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 272-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{schmidtschau:LIPIcs.RTA.2012.272,
  author =	{Schmidt-Schau{\ss}, Manfred},
  title =	{{Matching of Compressed Patterns with Character-Variables}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{272--287},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.272},
  URN =		{urn:nbn:de:0030-drops-34981},
  doi =		{10.4230/LIPIcs.RTA.2012.272},
  annote =	{Keywords: matching, grammar-based compression, partial words}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.288

Meaningless Sets in Infinitary Combinatory Logic

Authors: Paula Severi and Fer-Jan de Vries

Abstract

In this paper we study meaningless sets in infinitary combinatory logic. So far only a handful of meaningless sets were known. We show that there are uncountably many meaningless sets. As an application to the semantics of finite combinatory logics, we show that there exist uncountably many combinatory algebras that are not a lambda algebra. We also study ways of weakening the axioms of meaningless sets to get, not only sufficient, but also necessary conditions for having confluence and normalisation.

Cite as

Paula Severi and Fer-Jan de Vries. Meaningless Sets in Infinitary Combinatory Logic. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 288-304, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{severi_et_al:LIPIcs.RTA.2012.288,
  author =	{Severi, Paula and de Vries, Fer-Jan},
  title =	{{Meaningless Sets in Infinitary Combinatory Logic}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{288--304},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.288},
  URN =		{urn:nbn:de:0030-drops-34993},
  doi =		{10.4230/LIPIcs.RTA.2012.288},
  annote =	{Keywords: Infinitary Rewriting, Combinatory Logic, Meaningless Sets, Confluence, Normalisation}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.305

A Rewriting Framework for Activities Subject to Regulations

Authors: Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, Carolyn Talcott, and Ranko Perovic

Abstract

Activities such as clinical investigations or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols, and activities can form the foundation for automated assistants to aid planning, monitoring, and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, that is, they may have different outcomes whenever applied. We demonstrate how specifications in our model can be straightforwardly mapped to the rewriting logic language Maude, and how one can use existing techniques to improve performance. Finally, we also determine the complexity of the plan compliance problem, that is, finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, that is, their pre and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects.

Cite as

Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, Carolyn Talcott, and Ranko Perovic. A Rewriting Framework for Activities Subject to Regulations. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 305-322, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kanovich_et_al:LIPIcs.RTA.2012.305,
  author =	{Kanovich, Max and Ban Kirigin, Tajana and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn and Perovic, Ranko},
  title =	{{A Rewriting Framework for Activities Subject to Regulations}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{305--322},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.305},
  URN =		{urn:nbn:de:0030-drops-35000},
  doi =		{10.4230/LIPIcs.RTA.2012.305},
  annote =	{Keywords: Multiset Rewrite Systems, Collaborative Systems, Applications of Rewrite Systems, Clinical Investigations, Maude}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.323

Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus

Authors: Kazushige Terui

Abstract

Consider the following problem: given a simply typed lambda term of Boolean type and of order r, does it normalize to "true"? A related problem is: given a term M of word type and of order r together with a finite automaton D, does D accept the word represented by the normal form of M? We prove that these problems are n-EXPTIME complete for r=2n+2, and n-EXPSPACE complete for r=2n+3. While the hardness part is relatively easy, the membership part is not so obvious; in particular, simply applying beta reduction does not work. Some preceding works employ semantic evaluation in the category of sets and functions, but it is not efficient enough for our purpose. We present an algorithm for the above type of problem that is a fine blend of beta reduction, Krivine abstract machine and semantic evaluation in a category based on preorders and order ideals, also known as the Scott model of linear logic. The semantic evaluation can also be presented as intersection type checking.

Cite as

Kazushige Terui. Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 323-338, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{terui:LIPIcs.RTA.2012.323,
  author =	{Terui, Kazushige},
  title =	{{Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{323--338},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.323},
  URN =		{urn:nbn:de:0030-drops-35012},
  doi =		{10.4230/LIPIcs.RTA.2012.323},
  annote =	{Keywords: simply typed lambda calculus, computational complexity, denotational semantics, intersection types}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.339

On the Formalization of Termination Techniques based on Multiset Orderings

Authors: René Thiemann, Guillaume Allais, and Julian Nagele

Abstract

Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination proofs, we have added them to the Isabelle Formalization of Rewriting. To this end, it was required to extend the existing formalization on multiset orderings towards a generalized multiset ordering. Afterwards, the soundness proofs of both techniques have been established, although only after fixing some definitions. Concerning efficiency, it is known that the search for suitable parameters for both techniques is NP-hard. We show that checking the correct application of the techniques--where all parameters are provided--is also NP-hard, since the problem of deciding the generalized multiset ordering is NP-hard.

Cite as

René Thiemann, Guillaume Allais, and Julian Nagele. On the Formalization of Termination Techniques based on Multiset Orderings. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 339-354, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.RTA.2012.339,
  author =	{Thiemann, Ren\'{e} and Allais, Guillaume and Nagele, Julian},
  title =	{{On the Formalization of Termination Techniques based on Multiset Orderings}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{339--354},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.339},
  URN =		{urn:nbn:de:0030-drops-35029},
  doi =		{10.4230/LIPIcs.RTA.2012.339},
  annote =	{Keywords: formalization, term rewriting, termination, orderings}
}

LIPIcs, Volume 15

23rd International Conference on Rewriting Techniques and Applications (RTA'12)

Event

Editor

Publication Details

Access Numbers

Documents

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Filters

Thanks for your feedback!

Could not send message