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

TL;DR

This paper introduces an inversion tool for conditional term rewriting systems, demonstrating its effectiveness through experiments with the Ackermann function, and showing how inversion techniques can reduce search space.

Contribution

It presents a new inversion tool for conditional rewriting systems, including various inverter types, and applies it to Ackermann function inversion as a case study.

Findings

Polyvariant inversion reduces search space.

Input-output set propagation improves efficiency.

Full and partial inversions are feasible for Ackermann.

Abstract

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.