An Isabelle/HOL Formalization of Rewriting 
for Certified Tool Assertions 

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.thy
in 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.thy
For 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