An Inversion Tool for Conditional Term Rewriting Systems - A Case Study of Ackermann Inversion

Maria Bendix Mikkelsen
(DIKU, University of Copenhagen, Denmark)
Robert Glück
(DIKU, University of Copenhagen, Denmark)
Maja H. Kirkeby
(Roskilde University, Denmark)

We report on an inversion tool for a class of oriented conditional constructor term rewriting systems. Four well-behaved rule inverters ranging from trivial to full, partial and semi-inverters are included. Conditional term rewriting systems are theoretically well founded and can model functional and non- functional rewrite relations. We illustrate the inversion by experiments with full and partial inversions of the Ackermann function. The case study demonstrates, among others, that polyvariant inversion and input-output set propagation can reduce the search space of the generated inverse systems.

In Alexei Lisitsa and Andrei P. Nemytykh: Proceedings of the 9th International Workshop on Verification and Program Transformation (VPT 2021), Luxembourg, Luxembourg, 27th and 28th of March 2021, Electronic Proceedings in Theoretical Computer Science 341, pp. 33–41.
Published: 6th September 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.341.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org