2026-10-09T10:49:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4584 2024-03-06T09:29:34Z ddc:004 open_access

Inverse Unfold Problem and Its Heuristic Solving Nagashima, Masanori Kato, Tomofumi Sakai, Masahiko Nishida, Naoki program transformation unfolding conditional term rewriting system Unfold/fold transformations have been widely studied in various programming paradigms and are used in program transformations, theorem proving, and so on. This paper, by using an example, show that restoring an one-step unfolding is not easy, i.e., a challenging task, since some rules used by unfolding may be lost. We formalize this problem by regarding one-step program transformation as a relation. Next we discuss some issues on a specific framework, called pure-constructor systems, which constitute a subclass of conditional term rewriting systems. We show that the inverse of T preserves rewrite relations if T preserves rewrite relations and the signature. We propose a heuristic procedure to solve the problem, and show its successful examples. We improve the procedure, and show examples for which the improvement takes effect. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Masanori Nagashima and Tomofumi Kato and Masahiko Sakai and Naoki Nishida 2014 Is Part Of OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.WPTE.2014.27 urn:nbn:de:0030-drops-45848 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.27 eng https://creativecommons.org/licenses/by/3.0/legalcode