1 Search Results for "Yamada, Toshiyuki"


Document
Natural Inductive Theorems for Higher-Order Rewriting

Authors: Takahito Aoto, Toshiyuki Yamada, and Yuki Chiba

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)


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

Cite as

Takahito Aoto, Toshiyuki Yamada, and Yuki Chiba. Natural Inductive Theorems for Higher-Order Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 107-121, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.RTA.2011.107,
  author =	{Aoto, Takahito and Yamada, Toshiyuki and Chiba, Yuki},
  title =	{{Natural Inductive Theorems for Higher-Order Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{107--121},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.107},
  URN =		{urn:nbn:de:0030-drops-31119},
  doi =		{10.4230/LIPIcs.RTA.2011.107},
  annote =	{Keywords: Inductive Theorems, Higher-Order Equational Logic, Simply-Typed S-Expression Rewriting Systems, Term Rewriting Systems}
}
  • Refine by Author
  • 1 Aoto, Takahito
  • 1 Chiba, Yuki
  • 1 Yamada, Toshiyuki

  • Refine by Classification

  • Refine by Keyword
  • 1 Higher-Order Equational Logic
  • 1 Inductive Theorems
  • 1 Simply-Typed S-Expression Rewriting Systems
  • 1 Term Rewriting Systems

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2011

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail