Natural inductive theorems for higher-order Rewriting

Takahito Aoto, Toshiyuki Yamada, Yuki Chiba

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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

Original languageEnglish
Title of host publication22nd International Conference on Rewriting Techniques and Applications, RTA 2011
Pages107-121
Number of pages15
DOIs
Publication statusPublished - 2011 Dec 1
Event22nd International Conference on Rewriting Techniques and Applications, RTA 2011 - Novi Sad, Serbia
Duration: 2011 May 302011 Jun 1

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume10
ISSN (Print)1868-8969

Other

Other22nd International Conference on Rewriting Techniques and Applications, RTA 2011
CountrySerbia
CityNovi Sad
Period11/5/3011/6/1

Keywords

  • Higher-order equational logic
  • Inductive Theorems
  • Simply-typed S-expression rewriting systems
  • Term rewriting systems

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Natural inductive theorems for higher-order Rewriting'. Together they form a unique fingerprint.

Cite this