IEICE Transactions on Information and Systems

IEICE Transactions on Information and Systems 2007 E90-D(4):707-715; doi:10.1093/ietisy/e90-d.4.707

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by KUSAKARI, K. Articles by CHIBA, Y. Search for Related Content Social Bookmarking          What's this?

Copyright © 2007 The Institute of Electronics, Information and Communication Engineers

Regular Section -- Papers -- Computation and Computational Models

A Higher-Order Knuth-Bendix Procedure and Its Applications

Keiichirou KUSAKARI¹ and Yuki CHIBA²

¹ The author is with the Graduate School of Information Science, Nagoya University, Nagoya-shi, 464–8603 Japan. E-mail: kusakari{at}is.nagoya-u.ac.jp, ² The author is with Research Institute of Electrical Communication, Tohoku University, Sendai-shi, 980–8577 Japan. E-mail: chiba{at}nue.riec.tohoku.ac.jp

The completeness (i.e. confluent and terminating) property is an important concept when using a term rewriting system (TRS) as a computational model of functional programming languages. Knuth and Bendix have proposed a procedure known as the KB procedure for generating a complete TRS. A TRS cannot, however, directly handle higher-order functions that are widely used in functional programming languages. In this paper, we propose a higher-order KB procedure that extends the KB procedure to the framework of a simply-typed term rewriting system (STRS) as an extended TRS that can handle higher-order functions. We discuss the application of this higher-order KB procedure to a certification technique called inductionless induction used in program verification, and its application to fusion transformation, a typical kind of program transformation.

Key Words: simply-typed term rewriting system, higher-order KB procedure, inductive theorem, inductionless induction, fusion transformation

---

Manuscript received December 17, 2004. Manuscript revised June 19, 2006.

References

[1] T. Aoto, T. Yamada, and Y. Toyama, "Proving inductive theorems of higher-order functional programs," Proc. Forum on Information Technology 2003 (FIT2003), Information Technology Letters, vol.2, pp.21–22, 2003.

[2] T. Aoto, T. Yamada, and Y. Toyama, "Inductive theorems for higher-order rewriting," Proc. 15th Int. Conf. on Rewriting Techniques and Applications (RTA 2004), LNCS 3091, pp.269–284, 2004.

[3] F. Baader and T. Nipkow, Term Rewriting and All That, Cambridge University Press, 1998.

[4] L. Bachmair and N. Dershowitz, "Equational inference, canonical proofs, and proof orderings," J. ACM, vol.41, no.2, pp.236–276, 1994.

[5] F. Bellegarde, "Automating synthesis by completion," Journees Francophones des Langages Applicatifs, pp.177–203, 1995.

[6] A. Bouhoula, "Automated theorem proving by test set induction," J. Symbolic Computation, vol.23, pp.47–77, 1997.

[7] R.S. Boyer and J.S. Moore, A Computational Logic, Academic Press, NewYork, 1979.

[8] W.-N. Chin, "Safe fusion of functional expressions II: Further improvements," J. Functional Programming, vol.4, no.4, pp.515–555, 1994.

[9] L. Fribourg, "A strong restriction of the inductive completion procedure," J. Symbolic Computation, vol.8, pp.253–276, 1989.

[10] G. Huet and J.M. Hullot, "Proof by induction in equational theories with constructors," J. Comput. Syst. Sci., vol.25, pp.239–266, 1982.

[11] Y. Itoh, K. Kusakari, and Y. Toyama, "On the termination of program fusion based on completion procedure," IEICE Technical Report, COMP2002-84, March 2003.

[12] D. Kapur, P. Narendran, and H. Zhang, "Proof by induction using test sets," Proc. 8th Int. Conf. on Automated Deduction (CADE-8), LNCS 230, pp.99–117, 1986.

[13] R. Kennaway, J.W. Klop, M.R. Sleep, and F.J. de Vries, "Comparing curried and uncurried rewriting," J. Symbolic Computation, vol.21, no.1, pp.15–39, 1996.

[14] D.E. Knuth and P.B. Bendix, "Simple word problems in universal algebra," in ed. J. Leech, Computational Problems in Abstract Algebra, pp.263–297, Pergamon Press, Oxford, U.K., 1970.

[15] H. Koike and Y. Toyama, "Comparison between inductionless induction and rewriting induction," JSSST Computer Software, vol.17, no.6, pp.1–12, 2000.

[16] K. Kusakari, "On proving termination of term rewriting systems with higher-order variables," IPSJ Trans. Programming, vol.42, no.SIG 7 (PRO 11), pp.35–45, 2001.

[17] K. Kusakari, "Higher-order path orders based on computability," IEICE Trans. Inf. & Syst., vol.E87-D, no.2, pp.352–359, Feb. 2004.

[18] K. Kusakari, M. Sakai, and T. Sakabe, "Primitive inductive theorems bridge implicit induction methods and inductive theorems in higher-order rewriting," IEICE Trans. Inf. & Syst., vol.E88-D, no.12, pp.2715–2726, Dec. 2005.[Abstract/Free Full Text]

[19] D.R. Musser, "On proving induction properties of abstract data types," Proc. 7th ACM Symp. Principles of Programming Languages, pp.154–162, 1980.

[20] H. Seidl and M.H. Sørensen, Constraints to Stop Deforestation, Science of Computer Programming 32(1-3), pp.73–107, 1998.

[21] Y. Toyama, "How to prove equivalence of term rewriting systems without induction," Theor. Comput. Sci., vol.90, no.2, pp.369–390, 1991.

[22] P. Wadler, "Deforestation: Transforming programs to eliminate trees," Theor. Comput. Sci., vol.73, pp.231–248, 1990.

CiteULike    Connotea    Del.icio.us    What's this?

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by KUSAKARI, K. Articles by CHIBA, Y. Search for Related Content Social Bookmarking          What's this?