Partial Inversion of Constructor Term Rewriting Systems

  • Naoki Nishida
  • Masahiko Sakai
  • Toshiki Sakabe
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


Partial-inversion compilers generate programs which compute some unknown inputs of given programs from a given output and the rest of inputs whose values are already given. In this paper, we propose a partial-inversion compiler of constructor term rewriting systems. The compiler automatically generates a conditional term rewriting system, and then unravels it to an unconditional system. To improve the efficiency of inverse computation, we show that innermost strategy is usable to obtain all solutions if the generated system is right-linear.


Normal Form Logic Program Partial Evaluation Unknown Input Ground Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abramov, S., Glück, R.: The universal resolving algorithm: Inverse computation in a functional language. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 187–212. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  2. 2.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)Google Scholar
  3. 3.
    Dershowitz, N., Mitra, S.: Jeopardy. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 16–29. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. 4.
    Durán, F., Lucas, S., Meseguer, J., Marché, C., Urbain, X.: Proving termination of membership equational programs. In: Proceedings of the ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, pp. 147–158. ACM Press, New York (2004)CrossRefGoogle Scholar
  5. 5.
    Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Glück, R., Kawabe, M.: A program inverter for a functional language with equality and constructors. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 246–264. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Harrison, P.G.: Function inversion. In: Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation, pp. 153–166. North-Holland, Amsterdam (1988)Google Scholar
  8. 8.
    Hirokawa, N., Middeldorp, A.: Tsukuba termination tool. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 311–320. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Hu, Z., Mu, S.-C., Takeichi, M.: A programmable editor for developing structured documents based on bidirectional transformations. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, pp. 178–189. ACM Press, New York (2004)CrossRefGoogle Scholar
  10. 10.
    Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)Google Scholar
  11. 11.
    Khoshnevisan, H., Sephton, K.M.: InvX: An automatic function inverter. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 564–568. Springer, Heidelberg (1989)Google Scholar
  12. 12.
    Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming (1), 1–61 (1998)Google Scholar
  13. 13.
    Lucas, S.: mu-term: A tool for proving termination of context-sensitive rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 200–209. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Marchiori, M.: Unravelings and ultra-properties. In: Hanus, M., Rodríguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol. 1139, pp. 107–121. Springer, Heidelberg (1996)Google Scholar
  15. 15.
    Nishida, N., Sakai, M., Sakabe, T.: Generation of inverse term rewriting systems for pure treeless functions. In: Proceedings of the International Workshop on Rewriting in Proof and Computation, Sendai, Japan, pp. 188–198 (2001)Google Scholar
  16. 16.
    Nishida, N., Sakai, M., Sakabe, T.: Narrowing-based simulation of term rewriting systems with extra variables and its termination proof. In: Functional and Constraint Logic Programming. ENTCS, vol. 86(3), p. 18. Elsevier, Amsterdam (2003)Google Scholar
  17. 17.
    Nishida, N., Sakai, M., Sakabe, T.: On simulation-completeness of unraveling for conditional term rewriting systems. Technical Report SS 2004-18 of IEICE, 25–30 (2004)Google Scholar
  18. 18.
    Nishida, N., Sakai, M., Sakabe, T.: Partial inversion of constructor term rewriting systems. Full version of this paper including the proofs of theorems (2005), Available from
  19. 19.
    Ohlebusch, E.: Termination of logic programs: Transformational methods revisited. Applicable Algebra in Engineering, Communication and Computing 12, 73–116 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  21. 21.
    Okamoto, K., Sakai, M., Sakabe, T.: Completeness of innermost strategy for inside- LR-joinable right-linear terminating TRSs. In: Record of 2003 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers. (2003) 564 (in Japanese). This is an extended result of [23], and the English version of this paper is available from,
  22. 22.
    Romanenko, A.: Inversion and metacomputation. In: Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation. SIGPLAN Notices, vol. 26, pp. 12–22. ACM Press, New York (1991)Google Scholar
  23. 23.
    Sakai, M., Okamoto, K., Sakabe, T.: Innermost reductions find all normal forms on right-linear terminating overlay TRSs. In: Proceedings of the 3rd International Workshop on Reduction Strategies in Rewriting and Programming, Valencia, Spain, pp. 79–88 (2003)Google Scholar
  24. 24.
    Secher, J.P., Sørensen, M.H.: From checking to inference via driving and dag grammars. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation. SIGPLAN Notices, vol. 37, pp. 41–51. ACM, New York (2002)CrossRefGoogle Scholar
  25. 25.
    Toyama, Y.: Confluent term rewriting systems with membership conditions. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol. 308, pp. 228–241. Springer, Heidelberg (1988)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Naoki Nishida
    • 1
  • Masahiko Sakai
    • 1
  • Toshiki Sakabe
    • 1
  1. 1.Graduate School of Information ScienceNagoya UniversityNagoyaJapan

Personalised recommendations