TY - GEN
T1 - Natural inductive theorems for higher-order Rewriting
AU - Aoto, Takahito
AU - Yamada, Toshiyuki
AU - Chiba, Yuki
PY - 2011/12/1
Y1 - 2011/12/1
N2 - The notion of inductive theorems is well-established in first-order term rewriting. In higherorder 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).
AB - The notion of inductive theorems is well-established in first-order term rewriting. In higherorder 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).
KW - Higher-order equational logic
KW - Inductive Theorems
KW - Simply-typed S-expression rewriting systems
KW - Term rewriting systems
UR - http://www.scopus.com/inward/record.url?scp=84880191341&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84880191341&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.RTA.2011.107
DO - 10.4230/LIPIcs.RTA.2011.107
M3 - Conference contribution
AN - SCOPUS:84880191341
SN - 9783939897309
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 107
EP - 121
BT - 22nd International Conference on Rewriting Techniques and Applications, RTA 2011
T2 - 22nd International Conference on Rewriting Techniques and Applications, RTA 2011
Y2 - 30 May 2011 through 1 June 2011
ER -