Inversion framework: reasoning about inversion by conditional term rewriting systems
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Inversion framework : reasoning about inversion by conditional term rewriting systems. / Kirkeby, Maja Hanne; Glück, Robert.
PPDP '20: Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming. Association for Computing Machinery, 2020.Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Inversion framework
T2 - 22nd International Symposium on Principles and Practice of Declarative Programming - PPDP '20
AU - Kirkeby, Maja Hanne
AU - Glück, Robert
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
U2 - 10.1145/3414080.3414089
DO - 10.1145/3414080.3414089
M3 - Article in proceedings
BT - PPDP '20: Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming
PB - Association for Computing Machinery
Y2 - 8 September 2020 through 10 September 2020
ER -
ID: 249396044