Ulysse Le Huitouze and René Thiemann:
Core matrix interpretations for proving termination of term rewrite systems
Matrix interpretations are powerful techniques for proving termination of term rewrite systems. Among them, the original paper that introduced the matrix interpretation technique, originally aimed at string rewriting, also described sets of matrices that inherently provide a well-founded relation and its required monotonic properties, simplifying proofs. To the extent of our knowledge, these special sets of matrices have not yet explicitly been used in a term rewriting setting. We report on the generalisation of these sets of matrices to a term rewriting setting. All results have been formalised in Isabelle/HOL and are integrated in the CeTA certifier.
Etienne Payet
Non-Termination of Term Rewrite Systems Using Pattern Unfolding
We present a revisit, based on a new unfolding technique, of an approach introduced in term rewriting for the automatic detection of non-looping non-termination from patterns of rules.
Nils Lommen, Éléanore Meyer and Jürgen Giesl
Control-Flow Refinement for Complexity Analysis of Probabilistic Programs
Recently, we showed how to use control-flow refinement (CFR) to improve automatic complexity analysis of integer programs. While up to now CFR was limited to classical programs, we extend CFR to probabilistic programs and show its soundness for complexity analysis. To demonstrate its benefits, we implemented our new CFR technique in our complexity analysis tool KoAT.
Nils Lommen, Éléanore Meyer and Jürgen Giesl
KoAT: An Automatic Complexity Analysis Tool for (Probabilistic) Integer Programs
KoAT is an automated tool for inferring runtime and size bounds – and proving termination – of (probabilistic) integer programs by analyzing program fragments in a modular way and combining their bounds. It uses multiphase linear ranking functions to capture execution ``phases’’ of loops and a technique for so-called triangular weakly non-linear loops (twn-loops), enabling the analysis of programs with non-linear arithmetic.
Éléanore Meyer and Jürgen Giesl
Deciding Termination of Simple Randomized Loops
We show that universal positive almost sure termination (UPAST) is decidable for a class of simple randomized programs, i.e., it is decidable whether the expected runtime of such a program is finite for all inputs. Our class contains all programs that consist of a single loop, with a linear loop guard and a loop body composed of two linear commuting and diagonalizable updates. In each iteration of the loop, the update to be carried out is picked at random, according to a fixed probability. We show the decidability of UPAST for this class of programs, where the program’s variables and inputs may range over various sub-semirings of the real numbers. In this way, we extend a line of research initiated by Tiwari in 2004 into the realm of randomized programs.
Johannes Niederhauser and Aart Middeldorp
NCPO goes Beta-Eta-Long Normal Form
We adapt our recently introduced higher-order reduction order NCPO to beta-eta-long normal forms which makes it directly applicable to Nipkow’s higher-order rewrite systems.
Jan-Christoph Kassing, Grigory Vartanyan and Jürgen Giesl
A Dependency Pair Framework for Relative Termination of Term Rewriting
Problem 106 of the RTA List of Open Problems asks for an adaption of dependency pairs for relative termination of term rewrite systems (TRSs). Here, infinite rewrite sequences are allowed, but one wants to prove that a certain subset of the rewrite rules cannot be used infinitely often. Dependency pairs were recently adapted to annotated dependency pairs (ADPs) to prove almost-sure termination of probabilistic TRSs. In this talk, we present an adaption of ADPs for relative termination. We implemented our relative ADP framework in our tool AProVE and evaluate it in comparison to other tools for relative termination of TRSs.
Florian Frohn, Carsten Fuhs, Jürgen Giesl, Jan-Christoph Kassing and Nils Lommen
AProVE: Becoming Open Source and Recent Improvements
AProVE (Automated Program Verification Environment) is a tool for fully automatic program verification. More precisely, AProVE is able to analyze termination, complexity, and safety of different programming languages, e.g., Java, C, Haskell, and Prolog. To ensure the correctness of its analysis, AProVE can generate certificates that can be checked by external certification tools.
Jan-Christoph Kassing and Jürgen Giesl
Modularity of Termination in Probabilistic Term Rewriting
We investigate the modularity of probabilistic notions of termination in term rewriting. In the probabilistic setting, there are several interesting termination properties: Almost-sure termination (termination with probability 1), positive almost-sure termination (finite expected runtime of each rewrite sequence), and strong almost-sure termination (expected runtime is bounded by a constant for each start term). A property is called modular if it is preserved for certain unions of probabilistic term rewrite systems. We show that these three termination properties have different modularity behavior for innermost rewriting. Utilizing known relations between innermost and full probabilistic rewriting allows us to obtain modularity results for full probabilistic rewriting as well.
René Thiemann
A New Proof for Soundness of Right-Forward Closures for Termination Analysis
We consider the termination problem of term rewrite systems (TRSs). Dershowitz proved that termination starting from arbitrary terms is equivalent to termination starting from all terms in the right-forward closure (RFC), provided that the TRS is right-linear or orthogonal. In this paper we provide a new proof of this result, and also include a later result that one can weaken orthogonality to locally confluent overlay TRSs. All proofs have been verified in Isabelle/HOL.
Vincent van Oostrom
Disjunctive Termination for Affluent Families
We introduce affluence, a condition on composition that entails a finite family of rewrite relations is terminating iff its is disjunctive termination, and relate it to jumping. Our proofs transform infinite reductions in the family union into such in family members, by induction on family size.
Dieter Hofbauer and Johannes Waldmann
Cetera: Certified Termination with Agda
We report on Cetera, a program and library for checking termination certificates for string rewriting. The library is certified in the dependently typed proof language Agda, and we extract Haskell code for the program. For now, Cetera contains well-founded monotone monoids (instantiated to weights and standard matrices) and allows modular removal of rules (by relative termination). We are currently working on the RFC (right hand sides of forward closures) theorem. Proofs in Agda are constructive, so they sometimes differ from standard presentation.
Raúl Gutiérrez and Salvador Lucas
MU-TERM GTRS: A Tool for Proving Termination of Generalized Term Rewriting Systems
We present MU-TERM GTRS, a tool designed to prove termination of Generalized Term Rewriting Systems (GTRSs). In these systems, rewriting computations are defined by rules that may include conditions expressed using atoms defined by Horn clauses—particularly conditions involving reachability, joinability, and conversion.
Termination control is enhanced through the use of a replacement map, which explicitly specifies the argument positions of function symbols where rewriting is allowed.
GTRSs offer a powerful framework for modeling computations in advanced reduction-based languages such as Maude.
Carsten Fuhs, Liye Guo and Cynthia Kop
Dependendy Pairs for Innermost Constrained Higher-Order Rewriting
Logically constrained simply-typed term rewriting systems (LCSTRSs) provide a form of rewriting geared towards analysis of programs with higher-order features and both algebraic and primitive data types. Termination of LCSTRSs has been studied for full rewriting without strategy assumptions. This extended abstract adapts the higher-order constrained Dependency Pair framework for innermost termination, which implies termination under call-by-value evaluation. The DP framework for innermost termination effectively handles universal computability. This provides a foundation for open-world termination analysis of programs using call-by-value evaluation via LCSTRSs.
Reinis Cirpons, James D. Mitchell and Finn L. Smith
Off with the head: termination provers and the word problem for 1-relation monoids
In this talk I will showcase a new set of SRS termination problems arising from the word problem in 1-relation monoids. The word problem is a central object of study in combinatorial semigroup theory. Despite being undecidable in general, its decidability is open when restricted to 1-relation monoids. Motivated by recent efforts in solving this problem, we launched a quantitative investigation with the goal of formally proving as many small instances of the 1-relation monoid word problem as possible. This naturally lead us to utilize termination provers to solve SRS arising from many challenging instances. This is joint work with Florent Hivert (Université Paris Saclay), Assia Mahboubi (Nantes Université), Guillaume Melquiond (Université Paris Saclay), James D. Mitchell (University of St Andrews) and Finn L. Smith (University of St Andrews).
Alfons Geser
On Closures in String Rewriting
The set of overlap closures can be characterized as the semantics of composition trees. Rewrite systems for composition trees can be used to prove that the existence of loops entails the existence of looping forward closures, or to prove the correctness of a characterization of the set of right-hand sides of closures.