An inversion tool for conditional term rewriting systems – A case study of Ackermann inversion

Maria Bendix Mikkelsen, Robert Glück, Maja H. Kirkeby

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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 nonfunctional 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.

Original languageEnglish
Title of host publicationProceedings of the 9th International Workshop on Verification and Program Transformation
EditorsAlexei Lisitsa, Andrei P. Nemytykh
Number of pages9
PublisherEPTCS
Publication date6 Sept 2021
Pages33-41
DOIs
Publication statusPublished - 6 Sept 2021
Event9th International Workshop on Verification and Program Transformation, VPT 2021 - Virtual, Luxembourg, Luxembourg
Duration: 27 Mar 202128 Mar 2021

Conference

Conference9th International Workshop on Verification and Program Transformation, VPT 2021
Country/TerritoryLuxembourg
CityVirtual, Luxembourg
Period27/03/202128/03/2021
SeriesElectronic Proceedings in Theoretical Computer Science, EPTCS
Number341
ISSN2075-2180

Keywords

  • Case study
  • Program inversion
  • Program transformation
  • Term rewriting systems

Cite this