Document Open Access Logo

Inverse Unfold Problem and Its Heuristic Solving

Authors Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, Naoki Nishida

PDF
Thumbnail PDF

File

OASIcs.WPTE.2014.27.pdf
  • Filesize: 0.51 MB
  • 12 pages

Document Identifiers

Author Details

Masanori Nagashima
Tomofumi Kato
Masahiko Sakai
Naoki Nishida

Cite AsGet BibTex

Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, and Naoki Nishida. Inverse Unfold Problem and Its Heuristic Solving. In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. 27-38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/OASIcs.WPTE.2014.27

Abstract

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.
Keywords
  • program transformation
  • unfolding
  • conditional term rewriting system

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jesús Manuel Almendros-Jiménez and Germán Vidal. Automatic partial inversion of inductively sequential functions. In Zoltán Horváth, Viktória Zsók, and Andrew Butterfield, editors, Proc. of 18th International Symposium on Implementation and Application of Functional Languages, volume 4449 of Lecture Notes in Computer Science, pages 253-270, 2007. Google Scholar
  2. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  3. David Basin and Toby Walsh. Difference matching. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Computer Science, pages 295-309. Springer, 1992. Google Scholar
  4. N. Bensaou and Irène Guessarian. Transforming constraint logic programs. Theoretical Computer Science, 206(1-2):81-125, 1998. Google Scholar
  5. Jan A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32(3):323-362, 1986. Google Scholar
  6. Rod M. Burstall and John Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44-67, 1977. Google Scholar
  7. Sandro Etalle and Maurizio Gabbrielli. Transformations of CLP modules. Theoretical Computer Science, 166(1-2):101-146, 1996. Google Scholar
  8. Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. Transformation rules for locally stratified constraint logic programs. In Maurice Bruynooghe and Kung-Kiu Lau, editors, Program Development in Computational Logic, volume 3049 of Lecture Notes in Computer Science, pages 77-89. Springer, 2004. Google Scholar
  9. Harald Ganzinger. Order-sorted completion: The many-sorted way. Theoretical Computer Science, 89(1):3-32, 1991. Google Scholar
  10. Robert Glück and Masahiko Kawabe. A method for automatic program inversion based on LR(0) parsing. Fundamenta Informmaticae, 66(4):367-395, 2005. Google Scholar
  11. Tadashi Kanamori and Kenji Horiuchi. Construction of logic programs based on generalized unfold/fold rules. In Jean-Louis Lassez, editor, Proceedings of the 4th International Conference on Logic Programming, pages 744-768, 1987. Google Scholar
  12. Michael J. Maher. A transformation system for deductive database modules with perfect model semantics. Theoretical Computer Science, 110(2):377-403, 1993. Google Scholar
  13. Aart Middeldorp and Erik Hamoen. Completeness results for basic narrowing. Applicable Algebra in Engineering, Communication and Computing, 5:213-253, 1994. Google Scholar
  14. Masanori Nagashima, Masahiko Sakai, and Toshiki Sakabe. Determinization of conditional term rewriting systems. Theoretical Computer Science, 464:72-89, 2012. Google Scholar
  15. Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe. Partial inversion of constructor term rewriting systems. In Jürgen Giesl, editor, Proc. of the 16th Int'l Conf. on Rewriting Techniques and Applications, volume 3467 of LNCS, pages 264-278. Springer, 2005. Google Scholar
  16. Naoki Nishida and Germán Vidal. Program inversion for tail recursive functions. In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, volume 10 of LIPIcs, pages 283-298. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
  17. Naoki Nishida and Germán Vidal. Computing more specific versions of conditional rewriting systems. In Elvira Albert, editor, Revised Selected Papers of the 22nd International Symposium on Logic-Based, volume 7844 of Lecture Notes in Computer Science, pages 137-154, 2013. Google Scholar
  18. Minami Niwa, Naoki Nishida, and Masahiko Sakai. Extending matching operation in grammar program for program inversion. In Elvira Albert, editor, Informal Proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012), pages 130-139, 2012. Google Scholar
  19. Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002. Google Scholar
  20. Alberto Pettorossi, Maurizio Proietti, and Valerio Senni. Constraint-based correctness proofs for logic program transformations. Formal Aspects of Computing, 24(4-6):569-594, 2012. Google Scholar
  21. Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, and I. V. Ramakrishnan. Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. International Journal of Foundations of Computer Science, 13(3):387-403, 2002. Google Scholar
  22. Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, and I. V. Ramakrishnan. An unfold/fold transformation framework for definite logic programs. ACM Transactions on Programming Languages and Systems, 26(3):464-509, 2004. Google Scholar
  23. David Sands. Total correctness by local improvement in the transformation of functional programs. ACM Trans. on Programming Languages and Systems, 18(2):175-234, 1996. Google Scholar
  24. Taisuke Sato. Equivalence-preserving first-order unfold/fold transformation systems. Theoretical Computer Science, 105(1):57-84, 1992. Google Scholar
  25. Hirohisa Seki. Unfold/fold transformation of general logic programs for the well-founded semantics. Journal of Logic Programming, 16(1):5-23, 1993. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact