WST on Thursday, July 15th

Several termination techniques for rewrite systems are nowadays implemented in automated termination tools, which of course may contain bugs and thus, deliver faulty termination proofs. This motivates to certify these proofs automatically using some proof assistant like Coq or Isabelle. Here, the necessary termination techniques of that proof must have been formalized and then for certification it suffices to check the correct application of these techniques in a given proof.

When formalizing polynomial orders for arbitrary carriers (which satisfy some axioms) it turned out that our theorems are even more general than those which are known from the literature. For example, we lifted polynomials with negative constants to an arbitrary carrier, resulting in polynomials with negative constants over matrices over the rationals. Another example is the merge of the arctic semiring and the arctic semiring below zero into one semiring which strictly subsumes both arctic semirings.

As all these techniques are available in our certifier CeTA we encourage tool authors to extend their termination techniques to increase their power, certified.

We present our work in progress concerning the logical foundations of the analysis of termination for imperative recursive programs. The analysis is based on forward symbolic execution \cite{360252} and functional semantics. The distinctive feature of our approach is the formulation of {\em the termination condition as an induction principle} developed from the structure of the program with respect to iterative structures (recursive calls and {\tt while} loops). Moreover the termination condition insures the existence and the uniqueness of the function implemented by the program. Note that the existence is not automatic, because a recursive program corresponds, logically, to an implicit definition. It is interesting that this inductive termination condition can be also used for proving the uniqueness of the function as well as the total correctness of the program. We show in this paper how to prove the existence of the implemented function in the case of primitive recursive functions (programs without nested recursion). The method can be applied however to all imperative recursive programs, where recursive calls are outside the loops. For other programs, termination analysis appears to involve co-recursive functions and it is subject to further investigation. The methods presented here are under implementation in the {\em Theorema} system \cite{RISC2487}.

Inspired by binary counting we present and analyze a small length preserving terminating string rewriting system with several nice properties, in particular having derivations of exponential length. These observations are the key for a recent proof that a particular kind of RNA-editing admits a sequence of modifications that essentially requires an exponential number of steps.

In this note we present the Exponential Path Order EPO*. Inspired by a novel term rewriting characterisation of the exponential time functions FEXP, this order is carefully trimmed so that we believe that compatibility of TRSs implies exponentially bounded runtime complexity. Moreover, the order is complete in the sense that every exponential time function can be expressed by a TRS compatible with an instance of EPO*.

The work on EPO* is still unfinished, but we strongly believe that above mentioned results are correct.

In this note we present two proofs that the derivational complexity of the bits function is linear. The first proof is intuitive but not very suitable for implementation while the second one has been found automatically. Using the second proof idea allows the complexity tool CaT to show linear derivational complexity of the bits function for which no other current contemporary analyzer can infer a polynomial upper bound. In the second part of this note we generalize the weight gap principle of (Hirokawa and Moser, 2008).

We study the derivational complexity induced by the dependency pair method, enhanced with the dependency graph refinement and the subterm criterion, allowing relative removal of rules, for base orders inducing linear derivational complexity. If relative rule removal is allowed, we get a multiply recursive upper bound, otherwise the bound is primitive recursive.

Recently, the problem of proving outermost termination has been addressed mainly by methods relying on transformations. Here we describe a more direct approach inspired by the well-known dependency pair framework. The basic idea is to enrich dependency pairs by an additional component, namely the calling context of the corresponding recursive function call. Then one can use the additional contextual information to model DP chains adhering to certain strategies (e.g. the outermost strategy). Additionally, existing methods of the ordinary DP approach can partly be reused. Building upon this framework of contextual DPs, we describe a DP processor exploiting the additional contextual information. Basically, this processor analyzes nested contexts accumulated by consecutive DPs on DP chain candidates for (certain) redexes. If such a redex is found, the chain candidate is not a proper chain. Finally, we provide some empirical evaluation of our approach.

We present a termination method for left-linear Higher-order Rewrite Systems (HRSs) that are algebraic using a higher-order generalization of dependency pairs with argument filterings.

Building on CPO, the computability path ordering well-founded on a simply typed lambda structure due to Blanqui, Jouannaud and Rubio (CSL'08), we define PCPO, which is well-founded on the set of polymorphic lambda terms, hence its name. This is a new important step towards our challenge: to develop a well-founded order on the set of terms of the calculus of constructions, allowing to reduce strong normalization proofs of logical calculi to ordering comparisons of their computational rules.

We sketch the strong normalization proof, which uses an interesting new formulation of reducibility candidates "a la Girard" allowing for type-decreasing (and even kind-decreasing) rules.

We show how abstract combinatorial commutation properties for separating well-foundedness of unions of relations can be applied to generic path orderings used in termination proofs.