Natural inductive theorems for higher-order Rewriting

Takahito Aoto, Toshiyuki Yamada, Yuki Chiba

研究成果: Conference contribution

抄録

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

本文言語English
ホスト出版物のタイトル22nd International Conference on Rewriting Techniques and Applications, RTA 2011
ページ107-121
ページ数15
DOI
出版ステータスPublished - 2011 12 1
イベント22nd International Conference on Rewriting Techniques and Applications, RTA 2011 - Novi Sad, Serbia
継続期間: 2011 5 302011 6 1

出版物シリーズ

名前Leibniz International Proceedings in Informatics, LIPIcs
10
ISSN(印刷版)1868-8969

Other

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

ASJC Scopus subject areas

  • Software

フィンガープリント 「Natural inductive theorems for higher-order Rewriting」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル