Skip to main content
SpringerLink
Log in

Partial Inversion of Constructor Term Rewriting Systems

  • Conference paper
Term Rewriting and Applications (RTA 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3467))

Included in the following conference series:

Abstract

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.

This work is partly supported by MEXT. KAKENHI #15500007 and #16300005.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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)

    Chapter  Google Scholar 

  2. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  3. Dershowitz, N., Mitra, S.: Jeopardy. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 16–29. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Hirokawa, N., Middeldorp, A.: Tsukuba termination tool. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 311–320. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming (1), 1–61 (1998)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. 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. 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 http://www.sakabe.i.is.nagoya-u.ac.jp/~nishida/papers/

  19. Ohlebusch, E.: Termination of logic programs: Transformational methods revisited. Applicable Algebra in Engineering, Communication and Computing 12, 73–116 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  20. Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  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, http://www.sakabe.i.is.nagoya-u.ac.jp/~sakai/papers/

  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. 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. 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)

    Chapter  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Graduate School of Information Science, Nagoya University, Furo-cho, Chikusa-ku, Nagoya, 464-8603, Japan

    Naoki Nishida, Masahiko Sakai & Toshiki Sakabe

Authors
  1. Naoki Nishida
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Masahiko Sakai
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Toshiki Sakabe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LuFG Informatik 2, RWTH Aachen University, Germany

    Jürgen Giesl

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nishida, N., Sakai, M., Sakabe, T. (2005). Partial Inversion of Constructor Term Rewriting Systems. In: Giesl, J. (eds) Term Rewriting and Applications. RTA 2005. Lecture Notes in Computer Science, vol 3467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32033-3_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-32033-3_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25596-3

  • Online ISBN: 978-3-540-32033-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation