General
This site provides supporting material for the paper Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs by Christian Sternagel and René Thiemann. In the paper we present an Isabelle/HOL formalization of several kinds of interpretations which can be used within termination and complexity proofs.Formalization
All relevant theories are available within the IsaFoR directory of the sources of IsaFoR/CeTA v2.13. Compilation of the Isabelle sources requires Isabelle 2013-2 and the corresponding archive of formal proofs (version afp-2014-02-11 or later). There are also binaries for CeTA available.
To inspect the theories add the following line to ~/.isabelle/Isabelle2013-2/etc/settings
init_component "$AFP/afp-2014-02-11"where $AFP is the local path to afp-2014-02-11. Then add $ISABELLE_HOME/bin/ to your path and invoke the following command from inside the IsaFoR directory
isabelle jedit -d . -l QTRS Poly_Order.thyin order to view theories that are part of IsaFoR (like Poly_Order.thy). For theories that are part of the archive of formal proofs (like Matrix/Matrix_Comparison) do the following instead
isabelle jedit -d . -l HOL-Lib $AFP/thys/Matrix/Matrix_Comparison.thyFor further compilation instructions, we refer to the README file of IsaFoR.
Example proofs
Monotone algebras in the form of interpretations are used in several termination and complexity proofs. For example, several termination and complexity proofs that have been generated during the annual termination competitions contain interpretations. Due to our formalization, all proofs from the competition that are provided in the certification problem format can be certified by CeTA.
Whereas the tools in the competition produced over 10,000 proofs, in the following table we provide a small collection of examples from the literature which illustrate the variety of interpretations that occur in termination and complexity proofs.
| Input proof | Description |
|---|---|
| ag_3.10 | proof of TTT2 of example 3.10 of Aarts-Giesl collection; matrix interpretations over the naturals |
| luc_ex2 | proof within example 2 from [20]; uses rational numbers |
| luc_ex4 | proof within example 4 from [20]; uses rational numbers |
| luc_ex5 | proof of TTT2 for example 5 from [20]; uses rational matrix interpretations |
| luc_rat | proof of TTT2 for example Rrat from [19]; requires rationals, example cannot be proven terminating if polynomials are restricted to naturals |
| luc_real | proof of TTT2 for example Rreal from [19]; requires reals, example cannot be proven terminating if polynomials are restricted to rationals |
| nzm_r123 | proof for R1 ∪ R2 ∪ R3 from [23]; requires advanced monotonicity criteria for nonlinear polynomials on the naturals |
| nm_r1 | proof of TTT2 for R1 from [22]; matrix interpretation over the rationals, example cannot be proven terminating using matrix interpretations over the naturals |
| nm_r2 | proof of TTT2 for R2 from [22]; matrix interpretation over the reals, example cannot be proven terminating using matrix interpretations over the rationals |
| nm_t2 | proof of TTT2 for T2 from [22]; matrix interpretation of dimension 2, example cannot be proven terminating using matrix interpretations with dimension 1 |
| nm_t2 | proof of TTT2 for T3 from [22]; matrix interpretation of dimension 3, example cannot be proven terminating using matrix interpretations with dimension 2 |
| kw08_ex11 | proof of TTT2 for example 11 from [15]; uses monotone arctic matrix interpreations over the naturals |
| kw08_ex11b | proof of TTT2 for an extended variant of example 11 from [15]; here we use monotone arctic interpretations although the initial signature contains a binary symbol. Further note that the standard variable condition of TRSs is not satisfied. |
| kw08_ex13 | proof of TTT2 for example 13 from [15]; uses arctic matrix interpreations over the naturals as reduction pair |
| kw08_ex15 | proof of TTT2 for example 15 from [15]; uses arctic interpreations below zero. Already makes use of our generalization (the interpretation for cond is not absolute positive and violates condition in [15], Thm. 14.) |
| bouchare16 | proof of TTT2 employing the technique of [8] to remove all non-usable rules and all strictly oriented rules by monotone and Ce-compatible arctic interpretations. |
| zk10_lem5_2 | proof of CaT for an example from [33]; requires modularity criterion of [33], and according to [33], the modularity result is essential to show quadratic complexity via triangular matrix interpretations. |
| double | proof of CaT showing linear runtime complexity of doubling via linear polynomial interpretation |
| times | proof of CaT showing quadratic runtime complexity of multiplication via nonlinear polynomial interpretation |
| fgf | proof of CaT showing quadratic runtime complexity using interpretations over the rationals. |
Bibliography
| [8] |
J. Giesl, R. Thiemann, and P. Schneider-Kamp.
The dependency pair framework: Combining techniques for automated termination proofs. In Proc. 11th LPAR, volume 3452 of LNAI, pages 301-331. Springer, 2005. doi:10.1007/978-3-540-32275-7_21 |
| [15] |
A. Koprowski and J. Waldmann.
Arctic termination ldots below zero. In Proc. 24th RTA, volume 5117 of LNCS, pages 202-216. Springer, 2008. doi:10.1007/978-3-540-70590-1_14 |
| [19] |
S. Lucas.
On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. Appl. Algebr. Eng. Comm., 17(1):49-73, 2006. doi:10.1007/s00200-005-0189-5 |
| [20] |
S. Lucas.
Practical use of polynomials over the reals in proofs of termination. In Proc. 9th PPDP, pages 39-50. ACM, 2007. doi:10.1145/1273920.1273927 |
| [22] |
F. Neurauter and A. Middeldorp.
On the domain and dimension hierarchy of matrix interpretations. In Proc. 18th LPAR, volume 7180 of LNCS, pages 320-334. Springer, 2012. doi:10.1007/978-3-642-28717-6_25 |
| [23] |
F. Neurauter, H. Zankl, and A. Middeldorp.
Monotonicity criteria for polynomial interpretations over the naturals. In Proc. 5th IJCAR, volume 6173 of LNAI, pages 502-517. Springer, 2010. doi:10.1007/978-3-642-14203-1_42 |
| [33] |
H. Zankl and M. Korp.
Modular complexity analysis via relative complexity. In Proc. 21st RTA, volume 6 of LIPIcs, pages 385-400. Schloss Dagstuhl, 2010. doi:10.4230/LIPIcs.RTA.2010.385 |
Generated by bbl2html.awk v1.2c