Inversion Framework: Reasoning about Inversion by Conditional Term Rewriting Systems

Maja Hanne Kirkeby, Robert Glück

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

Abstract

We introduce a language-independent framework for reasoning about program inverters by conditional term rewriting systems. These systems can model the three fundamental forms of inversion, i.e., full, partial and semi-inversion, in declarative languages.

The correctness of the generic inversion algorithm introduced in this contribution is proven for all well-behaved rule inverters, and we demonstrate that this class of inverters encompasses several of the inversion algorithms published throughout the past years.

This new generic approach enables us to establish fundamental properties, e.g., orthogonality, for entire classes of well-behaved full inverters, partial inverters and semi-inverters regardless of their particular local rule inverters. We study known inverters as well as classes of inverters that yield left-to-right deterministic systems; left-to-right determinism is a desirable property, e.g., for functional programs; however, at the same time it is not generally a property of inverted systems. This generic approach enables a more systematic design of program inverters and fills a gap in our knowledge of program inversion.
Original languageEnglish
Title of host publicationPPDP '20: Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming
Number of pages14
Place of PublicationNew York
PublisherAssociation for Computing Machinery
Publication date1 Sep 2020
Pages1-14
Article number9
ISBN (Electronic)978-1-4503-8821-4
DOIs
Publication statusPublished - 1 Sep 2020
Event22nd International Symposium on Principles and Practice of Declarative Programming - Online
Duration: 8 Sep 202010 Sep 2020
Conference number: 22
http://www.cse.chalmers.se/~abela/ppdp20/

Symposium

Symposium22nd International Symposium on Principles and Practice of Declarative Programming
Number22
LocationOnline
Period08/09/202010/09/2020
OtherOnline conference
Internet address

Cite this