Abstract

Term rewriting in the presence of associative and commutative function symbols constitutes a highly expressive model of computation, which is for example well suited to reason about parallel computations. However, it is well known that the standard notion of termination does not apply any more: any term rewrite system containing a commutativity rule is nonterminating. Thus, instead of adding AC-rules to a rewrite system, we switch to the notion of AC-termination. AC-termination can for example be shown using AC-compatible reduction orders. One specific example of such an order is ACKBO. We present our Isabelle/HOL formalization of the ACKBO order. On an abstract level this gives us a mechanized proof of the fact that ACKBO is indeed an AC-compatible reduction order. Moreover, we integrated corresponding check functions into the verified certifier CeTA. This has the more practical consequence of enabling the machine certification of AC-termination proofs generated by automated termination tools.

BibTeX

@inproceedings{ALCS-CPP19,
  author    = "Alexander Lochmann and Christian Sternagel",
  title     = "Certified {ACKBO}",
  booktitle = "Proceedings of the 8th International Conference on Certified Programs and Proofs",
  editor    = "Assia Mahboubi and Magnus O. Myreen",
  pages     = "144--151",
  year      = 2019,
  doi       = "10.1145/3293880.3294099"
}