2026-07-20T05:47:31Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3111 2024-03-06T10:33:50Z ddc:004 open_access

Natural Inductive Theorems for Higher-Order Rewriting Aoto, Takahito Yamada, Toshiyuki Chiba, Yuki Inductive Theorems Higher-Order Equational Logic Simply-Typed S-Expression Rewriting Systems Term Rewriting Systems 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Takahito Aoto and Toshiyuki Yamada and Yuki Chiba 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.107 urn:nbn:de:0030-drops-31119 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.107 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode