RTA on Monday, August 14th

Invited Talk (09:00‑10:00)
Chair: Alberto Rubio

09:00‑10:00

Jurgen Giesl (RWTH Aachen) Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages [pdf] There are many powerful techniques for automated termination analysis of term rewriting. However, up to now they have hardly been used for real programming languages. We present a new approach which permits the application of existing techniques from term rewriting in order to prove termination of programs in the functional language Haskell. In particular, we show how termination techniques for ordinary rewriting can be used to handle those features of Haskell which are missing in term rewriting (e.g., lazy evaluation, polymorphic types, and higher-order functions). We implemented our results in our termination prover AProVE and successfully evaluated them on existing Haskell-libraries.

Break (10:00‑10:30)

Session 7: Termination (10:30‑12:00)
Chair: Hans Zantema

10:30‑11:00	Nao Hirokawa (University of Innsbruck) Aart Middeldorp (University of Innsbruck) Predictive Labeling Semantic labeling is a transformation technique for proving the termination of rewrite systems. The semantic part is given by a quasi-model of the rewrite rules. In this paper we present a variant of semantic labeling in which the quasi-model condition is only demanded for the usable rules induced by the labeling. Our variant is less powerful in theory but maybe more useful in practice.
11:00‑11:30	Dieter Hofbauer (Univ. Kassel) Johannes Waldmann (HTWK Leipzig, FB IMN) Termination of String Rewriting with Matrix Interpretations A rewriting system can be shown terminating by an order-preserving mapping into a well-founded domain. We present an instance of this scheme for string rewriting where the domain is a set of square matrices of natural numbers, equipped with a well-founded ordering that is not total. The coefficients of the matrices can be found via a transformation to a boolean satisfiability problem. The matrix method also supports relative termination, thus it fits with the dependency pair method as well. Our implementation is able to automatically solve hard termination problems.
11:30‑12:00	Yi Wang (Nagoya University) Masahiko Sakai (Graduate School of Infomation Science, Nagoya University) Decidability of Termination for Semi-Constructor TRSs, Left-Linear Shallow TRSs and Related Systems In this research, we study several more general classes of term rewriting systems and prove that termination is a decidable property for these classes. By showing the decidability of the existence of the cycling dependency chains, we prove that termination is decidable for semi-constructor case, the class of which is a superclass of right-ground TRSs. By analyzing the argument propagation cycling in the dependency graph and checking the reachability between two terms by tree automata techniques, we claim that termination is also decidable for left-linear shallow TRSs. Moreover, we explore the potentiality of the method for left-linear shallow case to cover right-linear shallow case and to generalize to growing TRSs. We also find some new interesting non-looping examples in addition to the only one known so far given by Zantema and propose new definitions to classify these non-looping examples.
12:00‑12:30	Olivier Bournez (LORIA) Florent Garnier (LORIA) Proving Positive Almost Sure Termination Under Strategies In last RTA, we introduced the notion of probabilistic rewrite systems and we gave some conditions entailing termination of those systems within a finite mean number of reduction steps. Termination was considered under arbitrarily unrestricted policies. Policies correspond to strategies for non-probabilistic rewrite systems. In this paper, we argue through several examples that this is often more natural or useful to restrict policies to a subclass. We introduce the notion of positive almost sure termination under policy, and we provide sufficient criteria to prove termination of a given probabilitic rewrite system under policy. This is illustrated with several examples.

Lunch break (12:30‑14:00)

Session 8: Higher-Order Rewriting and Unification (14:00‑15:30)
Chair: Aart Middeldorp

14:00‑14:30	Harrie Jan Sander Bruggink (Utrecht University) A Proof of Finite Family Developments for Higher-Order Rewriting using a Prefix Property A prefix property is the property that, given a reduction, the ancestor of a prefix of the target is a prefix of the source. In this paper we prove a prefix property for the class of Higher-Order Rewriting Systems with patterns (HRSs), by reducing it to a similar prefix property of a λ-calculus with explicit substitutions. This prefix property is then used to prove that Higher-order Rewriting Systems enjoy Finite Family Developments. This property states, that reductions in which the creation depth of the redexes is bounded are finite, and is a useful tool to prove various properties of HRSs.
14:30‑15:00	Jean-Pierre Jouannaud (École Polytechnique) Albert Rubio (Technical University of Catalunya) Higher-Order Orderings for Normal Rewriting We extend the termination proof methods based on reduction orderings to higher-order rewriting systems ā la Nipkow using higher-order pattern matching for firing rules, and accomodate for any use of eta, as a reduction, as an expansion or as an equation. As a main novelty, we provide with a mecanism for transforming any reduction ordering including beta-reduction, such as the higher-order recursive path ordering, into a reduction ordering for proving termination of rewriting ā la Nipkow. Non-trivial examples are carried out.
15:00‑15:30	Jordi Levy (IIIA - CSIC) Manfred Schmidt-Schauss (Institut für Informatik, FB Informatik und Mathematik, Johann Wolfgang Goethe-Universität) Mateu Villaret (Informātica i Matemātica Aplicada - Universitat de Girona) Bounded Second-Order Unification is NP-Complete Bounded Second-Order Unification is the problem of deciding, for a given second-order equation t = u and a positive integer m, whether there exists a unifier sigma such that, for every second-order variable F, the term instantiated for F has at most m occurrences of bound variables. It is already known that Bounded Second-Order Unification is decidable and NP-hard, whereas general Second-Order Unification is undecidable. We prove that Bounded Second-Order Unification is NP-complete, provided m is given in unary encoding, by proving that a size-minimal solution can be represented in polynomial space, and then applying a generalization of Plandowski's polynomial algorithm that compares compacted terms in polynomial time.