General
This site provides supporting material for the paper Certification of Nontermination Proofs using Strategies and Nonlooping Derivations by Julian Nagele, René Thiemann, and Sarah Winkler.In the paper we present an Isabelle/HOL formalization of an extended repertoire of nontermination techniques. First, we formalized techniques for nonlooping TRSs. Second, the available strategies include (an extended version of) forbidden patterns, which does in particular cover outermost and context-sensitive rewriting. Finally, a mechanism to support partial nontermination proofs allows to further extend the applicability of the proof checker CeTA.
Formalization
All relevant theories are available within the IsaFoR directory of the sources of IsaFoR/CeTA v2.14.1. A compilation of the Isabelle sources requires Isabelle 2013-2 and the corresponding archive of formal proofs (version afp-2014-02-19 or later). There are also binaries for CeTA available.
To inspect the theories like Forbidden_Patterns.thy, one has to add the following line into ~/.isabelle/Isabelle2013-2/etc/settings:
init_component "/the/path/to/afp-2014-02-19"Afterwards one can navigate into the IsaFoR directory and invoke
/the/path/to/Isabelle2013-2/bin/isabelle jedit -d . -l QTRS Forbidden_Patterns.thyFor further compilation instructions, we refer to the README-file within the IsaFoR-sources.
Experiments
Examples
Here are some examples from the paper, plus their certified nontermination proofs. All of the following proofs are provided in the certification problem format (CPF). For all examples we provide automatically generated proofs, but in cases where these proofs are overly complex we additionally provide small hand written proofs which correspond more to the proofs which are described in the paper.| TRS | hand written proof | automatic proof | description |
| map | – | NO | The TRS for map, i.e., Example 1 with the strategy as described in Example 3. |
| run_again1 | NO | NO | The TRS R of Example 13, where R' contains rules for the Ackermann function. |
| run_again2 | NO | NO | The TRS R of Example 13, where R' contains rules to compute square roots. Proving nontermination of R' is as hard as showing that sqrt(2) is irrational. |
| rewrite1 | NO | NO | The TRS R of Example 16, with R' for Ackermann as in run_again1. |
| rewrite2 | NO | NO | The TRS R of Example 16, with R' for square roots as in run_again2. |
| nonloop | – | NO | The TRS R of Example 17 for innermost rewriting. |