Natural Inductive Theorems for Higher-Order Rewriting
Abstract
The notion of inductive theorems is well-established in first-order term rewriting. In higher-order term rewriting, in contrast, it is not straightforward to extend this notion because of extensionality (Meinke, 1992). When extending the term rewriting based program transformation of Chiba et al. (2005) to higher-order term rewriting, we need extensibility, a property stating that inductive theorems are preserved by adding new functions via macros. In this paper, we propose and study a new notion of inductive theorems for higher-order rewriting, natural inductive theorems. This allows to incorporate properties such as extensionality and extensibility, based on simply typed S-expression rewriting (Yamada, 2001).
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/10287
Journal
-
- Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
-
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA'11) 10 107-121, 2011-04-26
Schloss Dagstuhl
- Tweet
Keywords
Details 詳細情報について
-
- CRID
- 1050574047132206208
-
- NII Article ID
- 120006675017
-
- ISSN
- 18688969
-
- Web Site
- http://hdl.handle.net/10119/10287
-
- Text Lang
- en
-
- Article Type
- conference paper
-
- Data Source
-
- IRDB
- CiNii Articles
- KAKEN