Abstract

Unravelings constitute a class of program transformations to model conditional rewrite systems as standard term rewrite systems. Key properties of unravelings are soundness and completeness with respect to reductions, in the sense that rewrite sequences in the unraveled system correspond to rewrite sequences in the conditional system and vice versa. While the latter is easily satisfied, the former holds only under certain conditions and is notoriously difficult to prove. This paper describes an Isabelle formalization of both properties. The soundness proof is based on the approach by Nishida, Sakai, and Sakabe (2012) but we also contribute to the theory by showing it applicable to a larger class of unravelings.

Based on our formalization we developed the first certifier to check output of conditional rewrite tools. In particular, quasi-decreasingness proofs by AProVE and conditional confluence proofs by ConCon can be certified.

BibTeX

@inproceedings{SWRT-FROCOS2015,
  author    = "Sarah Winkler and Ren{\'e} Thiemann",
  title     = "Formalizing Soundness and Completeness of Unravelings",
  booktitle = "Proceedings of the 10th International Symposium on Frontiers
               of Combining Systems (FroCoS 2015)",
  editor    = "Carsten Lutz and Silvio Ranise",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 9322,
  pages     = "239--255",
  year      = 2015,
  doi       = "10.1007/978-3-319-24246-0_15"
}