RTA on Sunday, July 11th

09:00‑10:00 Session 1
Chair: Georg Moser
Location: AT LT3
09:00 Patrick Bahr
Partial Order Infinitary Term Rewriting and Böhm Trees

In this paper we investigate an alternative model of infinitary term rewriting. Instead of a metric, a partial order on terms is employed to formalise the notion of (strong) convergence. We compare this partial order convergence of orthogonal term rewriting systems to the usual metric convergence of the corresponding Böhm extensions. The Böhm extension of a term rewriting system contains additional rules to equate so-called root-active terms. The core result of this paper is that reachability w.r.t.\ partial order convergence coincides with reachability w.r.t.\ metric convergence in the Böhm extension. This result is used to show that, unlike in the metric model, orthogonal systems are infinitarily confluent and infinitarily normalising in the partial order model. Moreover, we obtain, as in the metric model, a compression lemma. A corollary of this lemma is that reachability w.r.t.\ partial order convergence is a conservative extension of reachability w.r.t.\ metric convergence.

09:30 Hans Zantema and Matthias Raffelsieper
Proving Productivity in Infinite Data Structures

For a general class of infinite data structures including streams, binary trees, and the combination of finite and infinite lists, we investigate a notion of productivity. This generalizes stream productivity. We develop a general technique to prove productivity based on proving context-sensitive termination, by which the power of present termination tools can be exploited. For cases where the approach does not apply directly, we develop transformations extending the power of the basic approach. We present a tool combining all these ingredients that can prove productivity of a wide range of examples fully automatically.

10:30‑12:30 Session 2
Chair: Johannes Waldmann
Location: AT LT3
10:30 Marc Sylvestre, Irène Durand and Géraud Sénizergues
Termination of linear bounded term rewriting systems

For the whole class of linear term rewriting systems and for each integer k, we define k-bounded rewriting as a restriction of the usual notion of rewriting. We show that the problem of the existence of an infinite k-bounded derivation, called the k-bounded termination problem, is decidable. The k-bounded class (BO(k)) is, by definition, the set of linear systems for which every derivation can be replaced by a k-bounded derivation. In general, the k-bounded termination problem for BO(k) systems is not equivalent to the termination problem. This leads us to define more restricted classes for which those problems are equivalent: the classes BOLP(k) of k-bounded systems that have the length preservation property. By definition, a system is BOLP(k) if every derivation of length n can be replaced by a k-bounded derivation of length n. We define the class BOLP of bounded systems that have the length preservation property as the union of all the BOLP(k) classes. The class BOLP contains (strictly) several already known classes of systems: the inverse left-basic semi-Thue systems, the linear growing term rewriting systems, the inverse Linear-Finite-Path-Ordering systems, the strongly bottom-up systems.

11:00 Christian Sternagel and René Thiemann
Certified Subterm Criterion and Certified Usable Rules

In this paper we present our formalization of two important termination techniques for term rewrite systems: the subterm criterion and the reduction pair processor in combination with usable rules. For both techniques we developed executable check functions in the theorem prover Isabelle/HOL which can certify the correct application of these techniques in some given termination proof. As there are several variants of usable rules we designed our check function in such a way that it accepts all known variants, even those which are not explicitly spelled out in previous papers.

We integrated our formalization in the publicly available IsaFoR-library. This led to a significant increase in the power of CeTA, the corresponding certified termination proof checker that is extracted from IsaFoR.

11:30 Friedrich Neurauter and Aart Middeldorp
Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers

Polynomial interpretations are a useful technique for proving termination of term rewrite systems. They come in various flavors: polynomial interpretations with real, rational and integer coefficients. In 2006, Lucas proved that there are rewrite systems that can be shown polynomially terminating by polynomial interpretations with real coefficients, but cannot be shown polynomially terminating using polynomials with rational coefficients only. He also proved a similar theorem with respect to the use of rational coefficients versus integer coefficients. In this paper, we present alternative proofs of Lucas' theorems, which are both shorter and simpler than the original proofs. Moreover, we show that polynomial interpretations with real or rational coefficients do not subsume polynomial interpretations with integer coefficients, contrary to what is commonly believed. Finally, we also show that polynomial interpretations with real coefficients subsume polynomial interpretations with rational coefficients.

12:00 Carsten Otto, Marc Brockschmidt, Christian von Essen and Jürgen Giesl
Automated Termination Analysis of Java Bytecode by Term Rewriting

We present an automated approach to prove termination of Java Bytecode (JBC) programs by automatically transforming them to term rewrite systems (TRSs). In this way, the numerous techniques and tools developed for TRS termination can now be used for imperative object-oriented languages like Java, which can be compiled into JBC.

14:00‑15:00 FLoC Plenary Talks: tribute to Amir and Robin
Chair: Moshe Vardi
Location: George Square Lecture Theatre
14:00 David Harel (Weizmann Institute of Science)
Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's.
14:30 Gordon Plotkin (University of Edinburgh)
Robin Milner, a Craftsman of Tools for the Mind.
15:30‑17:20 Session 3
Chair: Dan Dougherty
Location: AT LT3
15:30 Alexander Koller and Stefan Thater
Underspecified computation of normal forms

We show how to compute readings of ambiguous natural language sentences that are minimal in some way. Formally, we consider the problem of computing, out of a set C of trees and a rewrite system R, those trees in C that cannot be rewritten into a tree in C. We solve the problem for sets of trees that are described by semantic representations typically used in computational linguistics, and a certain class of rewrite systems that we use to approximate entailment, and show how to compute the irreducible trees efficiently by intersecting tree automata. Our algorithm solves the problem of computing weakest readings that has been open for 25 years in computational linguistics.

16:00 Karl Gmeiner, Bernhard Gramlich and Felix Schernhammer
On (Un)Soundness of Unravelings

We revisit (un)soundness of transformations of conditional into unconditional rewrite systems. The focus here is on so-called unravelings, the most simple and natural kind of such transformations, for the class of normal conditional systems without extra variables. By a systematic and thorough study of existing counterexamples and of the potential sources of unsoundness we obtain several new positive and negative results. In particular, we prove the following new results: Confluence, non-erasingness and weak left-linearity (of a given conditional system) each guarantee soundness of the unraveled version w.r.t. the original one. The latter result substantially extends the only known sufficient criterion for soundness, namely left-linearity. Furthermore, by means of counterexamples we refute various other tempting conjectures about sufficient conditions for soundness.

16:30 Adrian Riesco, Alberto Verdejo and Narciso Marti-Oliet
Declarative Debugging of Missing Answers for Maude Specifications

Declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows the statement of membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, that correspond to transitions between states and can be nondeterministic. In this paper we propose a calculus that allows to infer normal forms and least sorts with the equational part, and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented a declarative debugger for Maude, a high-performance system based on rewriting logic, whose use is illustrated with an example.

17:00 Mark Hills and Grigore Rosu
A Rewriting Logic Semantics Approach to Modular Program Analysis

Based on work in rewriting logic semantics, K provides a powerful logic for defining the semantics of programming languages. Using standard term rewriting techniques, language definitions in K can be executed, providing semantics-based language interpreters. While most work in this area has focused on providing a standard execution semantics for a language, it is also possible to use K to define an abstract semantics, useful for program analysis. This paper describes one technique for defining such a semantics, called policy frameworks. In policy frameworks, an analysis-generic, modular framework is first defined for a language. Individual analyses, called policies, are then defined as extensions of this framework, with each policy defining analysis-specific semantic rules and an annotation language which, in combination with support in the language front-end, allows users to annotate program types and functions with information used during program analysis. To illustrate how one would create both a policy framework and individual policies an example framework and two policies are defined for SILF (Hills, Serbanuta and Rosu, 2007), a simple imperative language with functions, global variables, and arrays. A policy framework for C (Hills, Chen and Rosu, 2008) is also discussed briefly, illustrating that policy frameworks can scale to handle complex programs in realistic languages.